# CSDL to Z3 Translation
## Overview
This document describes the translation strategy from CSDL AST to Z3 Python API calls. The translator takes a typed AST and generates Z3 solver code that can be executed to solve the constraint problem.
## Translation Architecture
```
┌─────────────┐ ┌──────────────┐ ┌─────────────┐ ┌──────────┐
│ Typed AST │────▶│ Z3 Context │────▶│ Z3 Solver │────▶│ Solution │
└─────────────┘ └──────────────┘ └─────────────┘ └──────────┘
│ │ │ │
│ │ │ │
Variables Constraints check_sat() model()
Functions Assertions optimize() values
```
## Z3 Context Management
```typescript
export class Z3Translator {
private variables: Map<string, string> = new Map(); // name -> Z3 variable
private functions: Map<string, FunctionDeclNode> = new Map();
private context: string[] = []; // Z3 Python code lines
constructor() {
this.initializeZ3();
}
private initializeZ3(): void {
this.context.push('from z3 import *');
this.context.push('');
this.context.push('# Create solver');
this.context.push('solver = Solver()');
this.context.push('');
}
public translate(ast: ProgramNode): string {
// Process declarations
for (const decl of ast.declarations) {
this.translateDeclaration(decl);
}
this.context.push('');
this.context.push('# Add constraints');
// Process constraints
for (const constraint of ast.constraints) {
this.translateConstraint(constraint);
}
// Add solving and model extraction
this.context.push('');
this.context.push('# Solve');
this.context.push('if solver.check() == sat:');
this.context.push(' m = solver.model()');
this.context.push(' print("Solution found:")');
this.context.push(' for var in m.decls():');
this.context.push(' print(f" {var.name()} = {m[var]}")');
this.context.push('else:');
this.context.push(' print("No solution exists")');
return this.context.join('\n');
}
private translateDeclaration(decl: ASTNode): void {
switch (decl.type) {
case 'VarDecl':
this.translateVarDecl(decl as VarDeclNode);
break;
case 'ConstDecl':
this.translateConstDecl(decl as ConstDeclNode);
break;
case 'FunctionDecl':
this.translateFunctionDecl(decl as FunctionDeclNode);
break;
case 'ConstraintTypeDecl':
this.translateConstraintTypeDecl(decl as ConstraintTypeDeclNode);
break;
}
}
private translateVarDecl(decl: VarDeclNode): void {
for (const name of decl.names) {
const z3Type = this.typeToZ3(decl.varType);
const z3Var = this.makeZ3Variable(name, z3Type);
this.variables.set(name, z3Var);
this.context.push(`${z3Var} = ${z3Type}('${name}')`);
if (decl.initializer) {
const z3Expr = this.translateExpression(decl.initializer);
this.context.push(`solver.add(${z3Var} == ${z3Expr})`);
}
}
}
private translateConstDecl(decl: ConstDeclNode): void {
const z3Expr = this.translateExpression(decl.value);
this.variables.set(decl.name, z3Expr);
this.context.push(`${decl.name} = ${z3Expr}`);
}
private translateFunctionDecl(decl: FunctionDeclNode): void {
this.functions.set(decl.name, decl);
// Create Z3 function declaration
const paramTypes = decl.params.map(p => this.typeToZ3(p.paramType));
const returnType = this.typeToZ3(decl.returnType);
this.context.push(`${decl.name}_func = Function('${decl.name}', ${paramTypes.join(', ')}, ${returnType})`);
// Add function body as constraints (for interpreted functions)
// For uninterpreted functions, this is skipped
if (decl.body) {
// This requires quantified constraints to define the function
// We'll add axioms for the function behavior
}
}
private translateConstraint(constraint: ASTNode): void {
switch (constraint.type) {
case 'Assert': {
const node = constraint as AssertNode;
const z3Expr = this.translateExpression(node.expr);
if (node.name) {
this.context.push(`# Constraint: ${node.name}`);
}
this.context.push(`solver.add(${z3Expr})`);
break;
}
case 'SoftConstraint': {
const node = constraint as SoftConstraintNode;
const z3Expr = this.translateExpression(node.expr);
if (node.name) {
this.context.push(`# Soft constraint: ${node.name} (weight: ${node.weight})`);
}
this.context.push(`solver.add_soft(${z3Expr}, ${node.weight})`);
break;
}
case 'CheckSat': {
const node = constraint as CheckSatNode;
const z3Expr = this.translateExpression(node.expr);
this.context.push(`# Check satisfiability`);
this.context.push(`print("Checking:", ${z3Expr})`);
break;
}
case 'Optimize': {
const node = constraint as OptimizeNode;
const z3Expr = this.translateExpression(node.expr);
// Switch to Optimize solver
if (!this.context.some(line => line.includes('opt = Optimize()'))) {
this.context.push('');
this.context.push('# Use optimization solver');
this.context.push('opt = Optimize()');
// Copy constraints from regular solver
this.context.push('for c in solver.assertions():');
this.context.push(' opt.add(c)');
}
if (node.direction === 'minimize') {
this.context.push(`opt.minimize(${z3Expr})`);
} else {
this.context.push(`opt.maximize(${z3Expr})`);
}
break;
}
default:
// Plain expression constraint
if ('type' in constraint) {
const z3Expr = this.translateExpression(constraint as ExprNode);
this.context.push(`solver.add(${z3Expr})`);
}
}
}
private translateExpression(expr: ExprNode): string {
switch (expr.type) {
case 'Literal':
return this.translateLiteral(expr as LiteralNode);
case 'Variable':
return this.translateVariable(expr as VariableNode);
case 'BinaryExpr':
return this.translateBinaryExpr(expr as BinaryExprNode);
case 'UnaryExpr':
return this.translateUnaryExpr(expr as UnaryExprNode);
case 'CallExpr':
return this.translateCallExpr(expr as CallExprNode);
case 'IndexExpr':
return this.translateIndexExpr(expr as IndexExprNode);
case 'IfExpr':
return this.translateIfExpr(expr as IfExprNode);
case 'QuantifiedExpr':
return this.translateQuantifiedExpr(expr as QuantifiedExprNode);
case 'ArrayLiteral':
return this.translateArrayLiteral(expr as ArrayLiteralNode);
case 'SetLiteral':
return this.translateSetLiteral(expr as SetLiteralNode);
default:
throw new Error(`Unknown expression type: ${(expr as any).type}`);
}
}
private translateLiteral(node: LiteralNode): string {
switch (node.valueType) {
case 'number':
return String(node.value);
case 'string':
return `StringVal("${node.value}")`;
case 'boolean':
return node.value ? 'True' : 'False';
default:
throw new Error(`Unknown literal type: ${node.valueType}`);
}
}
private translateVariable(node: VariableNode): string {
const z3Var = this.variables.get(node.name);
if (!z3Var) {
throw new Error(`Undefined variable: ${node.name}`);
}
return z3Var;
}
private translateBinaryExpr(node: BinaryExprNode): string {
const left = this.translateExpression(node.left);
const right = this.translateExpression(node.right);
switch (node.operator) {
// Arithmetic
case 'add': return `(${left} + ${right})`;
case 'subtract': return `(${left} - ${right})`;
case 'multiply': return `(${left} * ${right})`;
case 'divide': return `(${left} / ${right})`;
case 'div': return `(${left} / ${right})`; // Integer division
case 'mod': return `(${left} % ${right})`;
case 'power': return `(${left} ** ${right})`;
// Comparison
case 'eq': return `(${left} == ${right})`;
case 'ne': return `(${left} != ${right})`;
case 'lt': return `(${left} < ${right})`;
case 'le': return `(${left} <= ${right})`;
case 'gt': return `(${left} > ${right})`;
case 'ge': return `(${left} >= ${right})`;
// Logical
case 'and': return `And(${left}, ${right})`;
case 'or': return `Or(${left}, ${right})`;
case 'implies': return `Implies(${left}, ${right})`;
case 'iff': return `(${left} == ${right})`; // Logical equivalence
case 'xor': return `Xor(${left}, ${right})`;
// Bitwise
case 'bitAnd': return `(${left} & ${right})`;
case 'bitOr': return `(${left} | ${right})`;
case 'bitXor': return `(${left} ^ ${right})`;
case 'lshift': return `(${left} << ${right})`;
case 'rshift': return `LShR(${left}, ${right})`; // Logical shift right
case 'arshift': return `(${left} >> ${right})`; // Arithmetic shift right
default:
throw new Error(`Unknown binary operator: ${node.operator}`);
}
}
private translateUnaryExpr(node: UnaryExprNode): string {
const operand = this.translateExpression(node.operand);
switch (node.operator) {
case 'negate': return `(-${operand})`;
case 'not': return `Not(${operand})`;
case 'bitNot': return `(~${operand})`;
default:
throw new Error(`Unknown unary operator: ${node.operator}`);
}
}
private translateCallExpr(node: CallExprNode): string {
const args = node.args.map(arg => this.translateExpression(arg));
// Built-in functions
switch (node.callee) {
case 'abs': return `If(${args[0]} >= 0, ${args[0]}, -${args[0]})`;
case 'sqrt': return `Sqrt(${args[0]})`;
case 'min': return args.length === 2 ? `If(${args[0]} < ${args[1]}, ${args[0]}, ${args[1]})`
: `min(${args.join(', ')})`;
case 'max': return args.length === 2 ? `If(${args[0]} > ${args[1]}, ${args[0]}, ${args[1]})`
: `max(${args.join(', ')})`;
case 'floor': return `ToInt(${args[0]})`;
case 'ceil': return `ToInt(${args[0]} + 0.5)`; // Approximation
case 'round': return `ToInt(${args[0]} + 0.5)`;
// Array functions
case 'len':
case 'length':
return `Length(${args[0]})`;
case 'sum': {
// For arrays, we need to expand
// This assumes array length is known at compile time
return this.expandArraySum(args[0]);
}
case 'product': {
return this.expandArrayProduct(args[0]);
}
// String functions
case 'to_int': return `StrToInt(${args[0]})`;
case 'to_string': return `IntToStr(${args[0]})`;
case 'contains': return `Contains(${args[0]}, ${args[1]})`;
case 'starts_with': return `PrefixOf(${args[1]}, ${args[0]})`;
case 'ends_with': return `SuffixOf(${args[1]}, ${args[0]})`;
case 'matches': return `InRe(${args[0]}, Re(${args[1]}))`;
// Constraint patterns
case 'distinct':
case 'alldifferent':
return `Distinct(${args.join(', ')})`;
case 'increasing': {
// Generate pairwise constraints
const arr = args[0];
return this.expandIncreasing(arr, false);
}
case 'strictly_increasing': {
const arr = args[0];
return this.expandIncreasing(arr, true);
}
// User-defined functions
default: {
const funcDecl = this.functions.get(node.callee);
if (funcDecl) {
return `${node.callee}_func(${args.join(', ')})`;
}
throw new Error(`Unknown function: ${node.callee}`);
}
}
}
private translateIndexExpr(node: IndexExprNode): string {
const array = this.translateExpression(node.array);
const index = this.translateExpression(node.index);
return `${array}[${index}]`;
}
private translateIfExpr(node: IfExprNode): string {
const condition = this.translateExpression(node.condition);
const thenBranch = this.translateExpression(node.thenBranch);
const elseBranch = this.translateExpression(node.elseBranch);
return `If(${condition}, ${thenBranch}, ${elseBranch})`;
}
private translateQuantifiedExpr(node: QuantifiedExprNode): string {
// Create bound variable
const boundVar = `${node.variable}_bound`;
this.context.push(`${boundVar} = Int('${node.variable}_bound')`);
// Save old binding
const oldBinding = this.variables.get(node.variable);
this.variables.set(node.variable, boundVar);
// Translate body
const body = this.translateExpression(node.body);
// Translate domain constraints
const domainConstraints = this.translateDomain(node.domain, boundVar);
// Restore binding
if (oldBinding) {
this.variables.set(node.variable, oldBinding);
} else {
this.variables.delete(node.variable);
}
// Build quantified formula
const fullBody = domainConstraints
? `Implies(${domainConstraints}, ${body})`
: body;
if (node.quantifier === 'forall') {
return `ForAll([${boundVar}], ${fullBody})`;
} else {
return `Exists([${boundVar}], And(${domainConstraints}, ${body}))`;
}
}
private translateDomain(domain: DomainNode, variable: string): string {
switch (domain.type) {
case 'Range': {
const start = this.translateExpression(domain.start);
const end = this.translateExpression(domain.end);
const endOp = domain.exclusive ? '<' : '<=';
return `And(${variable} >= ${start}, ${variable} ${endOp} ${end})`;
}
case 'Set': {
const conditions = domain.elements.map(elem => {
const z3Elem = this.translateExpression(elem);
return `${variable} == ${z3Elem}`;
});
return `Or(${conditions.join(', ')})`;
}
case 'Variable': {
// Array or set iteration
// This is more complex and may require array theory
return ``; // Domain constraint handled separately
}
default:
throw new Error(`Unknown domain type: ${(domain as any).type}`);
}
}
private translateArrayLiteral(node: ArrayLiteralNode): string {
const elements = node.elements.map(e => this.translateExpression(e));
// Create array constant
const arrayName = this.generateTempName('arr');
this.context.push(`${arrayName} = Array('${arrayName}', IntSort(), IntSort())`);
// Set each element
for (let i = 0; i < elements.length; i++) {
this.context.push(`${arrayName} = Store(${arrayName}, ${i}, ${elements[i]})`);
}
return arrayName;
}
private translateSetLiteral(node: SetLiteralNode): string {
// Sets can be represented as boolean arrays or using set theory
const elements = node.elements.map(e => this.translateExpression(e));
// For now, use list representation
return `[${elements.join(', ')}]`;
}
private typeToZ3(type: TypeNode): string {
switch (type.name) {
case 'Int': return 'Int';
case 'Real': return 'Real';
case 'Bool': return 'Bool';
case 'String': return 'String';
case 'BitVec': return `BitVec(${type.size || 32})`;
case 'Array': {
if (type.params && type.params.length > 0) {
const elemType = this.typeToZ3(type.params[0]);
return `Array(IntSort(), ${elemType}Sort())`;
}
return 'Array(IntSort(), IntSort())';
}
default:
throw new Error(`Unknown type: ${type.name}`);
}
}
private makeZ3Variable(name: string, type: string): string {
// Sanitize name for Z3
return name.replace(/[^a-zA-Z0-9_]/g, '_');
}
private generateTempName(prefix: string): string {
const counter = this.variables.size;
return `${prefix}_${counter}`;
}
private expandArraySum(array: string): string {
// This is a placeholder - actual implementation would need array length
// In practice, we'd expand this during type checking when we know the array size
return `Sum([${array}[i] for i in range(length)])`;
}
private expandArrayProduct(array: string): string {
return `Product([${array}[i] for i in range(length)])`;
}
private expandIncreasing(array: string, strict: boolean): string {
const op = strict ? '<' : '<=';
return `And([${array}[i] ${op} ${array}[i+1] for i in range(length-1)])`;
}
}
```
## Translation Examples
### Example 1: Simple Constraint
**CSDL:**
```csdl
var x: Int
var y: Int
x + y == 10
x > y
```
**Z3 Python:**
```python
from z3 import *
# Create solver
solver = Solver()
# Variables
x = Int('x')
y = Int('y')
# Add constraints
solver.add((x + y) == 10)
solver.add(x > y)
# Solve
if solver.check() == sat:
m = solver.model()
print("Solution found:")
for var in m.decls():
print(f" {var.name()} = {m[var]}")
else:
print("No solution exists")
```
### Example 2: Quantified Constraint
**CSDL:**
```csdl
var arr: Array[Int]
const n: Int = 5
forall i in 0..n-1:
arr[i] >= 0
```
**Z3 Python:**
```python
from z3 import *
solver = Solver()
# Variables
arr = Array('arr', IntSort(), IntSort())
n = 5
# Quantified constraint
i_bound = Int('i_bound')
solver.add(ForAll([i_bound],
Implies(And(i_bound >= 0, i_bound <= n-1),
arr[i_bound] >= 0)))
# Solve
if solver.check() == sat:
m = solver.model()
print("Solution found:")
for var in m.decls():
print(f" {var.name()} = {m[var]}")
else:
print("No solution exists")
```
### Example 3: Optimization
**CSDL:**
```csdl
var x: Int
var y: Int
x >= 0
y >= 0
x + y >= 10
minimize: x + y
```
**Z3 Python:**
```python
from z3 import *
solver = Solver()
# Variables
x = Int('x')
y = Int('y')
# Add constraints
solver.add(x >= 0)
solver.add(y >= 0)
solver.add((x + y) >= 10)
# Use optimization solver
opt = Optimize()
for c in solver.assertions():
opt.add(c)
opt.minimize(x + y)
# Solve
if opt.check() == sat:
m = opt.model()
print("Optimal solution found:")
for var in m.decls():
print(f" {var.name()} = {m[var]}")
print(f" Objective value: {m.evaluate(x + y)}")
else:
print("No solution exists")
```
### Example 4: Bitvector Operations
**CSDL:**
```csdl
var a: BitVec[32]
var b: BitVec[32]
var result: BitVec[32]
result == a + b
# Check for overflow
var overflow: Bool = (a > 0 and b > 0 and result < 0) or
(a < 0 and b < 0 and result > 0)
check_sat: overflow
```
**Z3 Python:**
```python
from z3 import *
solver = Solver()
# Variables
a = BitVec('a', 32)
b = BitVec('b', 32)
result = BitVec('result', 32)
# Add constraints
solver.add(result == (a + b))
# Overflow detection
overflow = Or(
And(a > 0, b > 0, result < 0),
And(a < 0, b < 0, result > 0)
)
# Check satisfiability
print("Checking:", overflow)
solver.add(overflow)
if solver.check() == sat:
m = solver.model()
print("Overflow possible with:")
for var in m.decls():
print(f" {var.name()} = {m[var]}")
else:
print("No overflow possible")
```
## Optimization Strategies
### 1. Constraint Simplification
Before translation, simplify constraints:
- Constant folding: `2 + 3` → `5`
- Dead code elimination
- Logical simplification: `x and true` → `x`
### 2. Quantifier Instantiation
For bounded quantifiers with small domains, unroll:
```csdl
forall i in 0..2: arr[i] > 0
```
Becomes:
```python
solver.add(And(arr[0] > 0, arr[1] > 0, arr[2] > 0))
```
### 3. Array Theory Optimization
Use Z3's efficient array theory instead of expanding:
```python
# Instead of: arr[0] + arr[1] + ... + arr[n]
# Use: Sum with quantifier or Lambda expression
```
### 4. Type Coercion
Handle Int/Real coercion automatically:
```python
# x: Int, y: Real
# x + y becomes ToReal(x) + y
```
## Error Handling
### Translation Errors
```typescript
export class TranslationError extends Error {
constructor(
message: string,
public node: ASTNode,
public context: string
) {
super(message);
this.name = 'TranslationError';
}
}
```
### Common Translation Issues
1. **Unbounded Quantifiers**: Require finite domains
2. **Nonlinear Arithmetic**: May be undecidable
3. **Array Bounds**: Need known sizes for expansion
4. **Type Mismatches**: Caught in type checking phase
## Integration with MCP Server
```typescript
// In logicManager.ts
async function solveConstraints(input: string): Promise<LogicResult> {
try {
// 1. Lex and parse
const lexer = new Lexer(input);
const tokens = lexer.tokenize();
const parser = new Parser(tokens);
const ast = parser.parse();
// 2. Type check
const typeChecker = new TypeChecker();
const typedAst = typeChecker.check(ast);
// 3. Translate to Z3
const translator = new Z3Translator();
const z3Code = translator.translate(typedAst);
// 4. Execute Z3 (via subprocess or Z3 WASM)
const solution = await executeZ3(z3Code);
// 5. Format results
return {
status: 'success',
message: 'Constraint problem solved',
details: {
system: 'constraint',
solution: solution,
z3Code: z3Code,
}
};
} catch (error) {
return {
status: 'error',
message: error.message,
details: {
system: 'constraint',
errorType: error.name,
}
};
}
}
```
## Testing Strategy
### Unit Tests
```typescript
describe('Z3Translator', () => {
it('should translate variable declarations', () => {
const ast = parseCSL('var x: Int');
const translator = new Z3Translator();
const z3 = translator.translate(ast);
expect(z3).toContain("x = Int('x')");
});
it('should translate arithmetic constraints', () => {
const ast = parseCSL('var x, y: Int\nx + y == 10');
const translator = new Z3Translator();
const z3 = translator.translate(ast);
expect(z3).toContain('solver.add((x + y) == 10)');
});
it('should translate quantified expressions', () => {
const ast = parseCSL('var arr: Array[Int]\nforall i in 0..5: arr[i] > 0');
const translator = new Z3Translator();
const z3 = translator.translate(ast);
expect(z3).toContain('ForAll');
});
});
```
### Integration Tests
Test complete constraint problems end-to-end:
```typescript
describe('Constraint Solving Integration', () => {
it('should solve N-Queens for n=4', async () => {
const input = `
const n: Int = 4
var queens: Array[Int]
forall i in 0..n-1:
queens[i] >= 0 and queens[i] < n
forall i in 0..n-1:
forall j in i+1..n-1:
queens[i] != queens[j]
forall i in 0..n-1:
forall j in i+1..n-1:
abs(queens[i] - queens[j]) != abs(i - j)
`;
const result = await solveConstraints(input);
expect(result.status).toBe('success');
expect(result.details.solution).toBeDefined();
});
});
```
## Performance Considerations
### 1. Incremental Solving
For interactive use, maintain solver state:
```python
solver = Solver()
# Add base constraints
# User adds more constraints incrementally
solver.push()
solver.add(new_constraint)
result = solver.check()
solver.pop() # Backtrack if needed
```
### 2. Parallel Solving
For multiple constraint variants:
```typescript
const solvers = variants.map(v => createSolver(v));
const results = await Promise.all(solvers.map(s => s.solve()));
```
### 3. Timeout Handling
```python
solver.set('timeout', 5000) # 5 seconds
result = solver.check()
if result == unknown:
print("Timeout or undecidable")
```
## Future Enhancements
1. **SMT-LIB Export**: Generate SMT-LIB format for compatibility
2. **Proof Generation**: Extract unsatisfiable cores
3. **Model Enumeration**: Find multiple solutions
4. **Optimization Tuning**: Tactics and strategies
5. **Interactive Debugging**: Step-through constraint solving
## Conclusion
The Z3 translator provides a bridge from the human-friendly CSDL to the powerful Z3 SMT solver. By generating clean, efficient Z3 Python code, we enable solving complex constraint problems while maintaining the readability and ease of use that makes CSDL suitable for LLM generation.
