# Constraint Specification DSL (CSDL)
## Overview
The Constraint Specification DSL (CSDL) is a domain-specific language designed for expressing constraints in a way that is:
- **Natural**: Easy for humans and LLMs to read and write
- **Precise**: Unambiguous semantics that translate directly to SMT solvers
- **Expressive**: Supports complex constraints across multiple theories
- **Safe**: Type-checked with early error detection
- **Extensible**: Support for custom constraints and functions
## Design Philosophy
### Core Principles
1. **Declarative over Imperative**: State what constraints exist, not how to solve them
2. **Type-Aware**: Support for rich type system with automatic inference
3. **Composable**: Build complex constraints from simple primitives
4. **Self-Documenting**: Readable syntax without extensive documentation
5. **LLM-Friendly**: Easy for Claude to generate from natural language
### Comparison with Existing Languages
| Feature | CSDL | SMT-LIB | MiniZinc | Python Z3 |
|---------|------|---------|----------|-----------|
| Readability | High | Low | High | Medium |
| LLM Generation | Excellent | Poor | Good | Good |
| Type Safety | Strong | Strong | Strong | Dynamic |
| Expressiveness | High | Highest | High | Highest |
| Learning Curve | Low | High | Medium | Medium |
## Syntax Specification
### Comments
```csdl
# Single-line comment
# Comments start with # and continue to end of line
```
### Variable Declarations
```csdl
# Type inference from value
var x = 42 # Int
var y = 3.14 # Real
var flag = true # Bool
# Explicit type annotation
var age: Int
var salary: Real
var active: Bool
var name: String
var scores: Array[Int]
# Multiple variables of same type
var a, b, c: Int
# Constants (immutable)
const PI: Real = 3.14159
const MAX_SIZE: Int = 1000
```
### Type System
#### Primitive Types
```csdl
Int # Mathematical integers (unbounded)
Real # Real numbers (floating-point)
Bool # Boolean values (true/false)
String # String values
BitVec[n] # Fixed-width bit vectors (e.g., BitVec[32])
```
#### Composite Types
```csdl
Array[T] # Arrays with integer indices
Tuple[T1, T2, ...] # Fixed-size tuples
Set[T] # Finite sets
Map[K, V] # Key-value mappings
```
#### Type Inference Rules
1. Numeric literals: `42` → Int, `3.14` → Real
2. Operations: Int + Int → Int, Int + Real → Real
3. Comparisons: T × T → Bool (for compatible T)
4. Arrays: Infer element type from usage
### Arithmetic Expressions
```csdl
# Basic operations
x + y # Addition
x - y # Subtraction
x * y # Multiplication
x / y # Division (Real result)
x div y # Integer division
x % y # Modulo
x ** y # Exponentiation
# Unary operations
-x # Negation
+x # Positive (no-op)
# Built-in functions
abs(x) # Absolute value
sqrt(x) # Square root
min(x, y, ...) # Minimum
max(x, y, ...) # Maximum
floor(x) # Floor function
ceil(x) # Ceiling function
round(x) # Rounding
# Operator precedence (high to low)
# 1. Function calls, array indexing
# 2. Exponentiation (**)
# 3. Unary +/-
# 4. Multiplication, division, modulo (*, /, div, %)
# 5. Addition, subtraction (+, -)
# 6. Comparisons (<, <=, >, >=, ==, !=)
# 7. Logical NOT (not, !)
# 8. Logical AND (and, &&)
# 9. Logical OR (or, ||)
# 10. Implication (=>)
# 11. Equivalence (<=>)
```
### Comparison Operators
```csdl
x == y # Equality
x != y # Inequality
x < y # Less than
x <= y # Less than or equal
x > y # Greater than
x >= y # Greater than or equal
```
### Logical Expressions
```csdl
# Logical operators (symbolic or word form)
p and q # Conjunction (also: p && q)
p or q # Disjunction (also: p || q)
not p # Negation (also: !p)
p => q # Implication (also: p implies q)
p <=> q # Equivalence (also: p iff q)
p xor q # Exclusive or
# Conditional expressions
if condition then expr1 else expr2
# Nested conditionals
if x > 0 then "positive"
else if x < 0 then "negative"
else "zero"
```
### Quantified Expressions
```csdl
# Universal quantification
forall x in domain: constraint
# Existential quantification
exists x in domain: constraint
# Domain specifications
forall i in 0..10: arr[i] >= 0 # Range (inclusive)
forall i in 0..<10: arr[i] >= 0 # Range (exclusive end)
forall x in [1, 2, 3, 5, 8]: P(x) # Explicit set
forall item in array: item > 0 # Array iteration
# Multiple quantifiers
forall i in 0..n:
forall j in 0..m:
matrix[i][j] >= 0
# Bounded quantification for decidability
forall x in 1..100: is_prime(x) => x % 2 != 0 or x == 2
```
### Array Operations
```csdl
# Array indexing
arr[i] # Get element at index i
arr[i] = value # Set element (in constraints, use arr[i] == value)
# Array properties
len(arr) # Length of array
arr.length # Alternative syntax
# Array operations
sum(arr) # Sum of all elements
product(arr) # Product of all elements
min(arr) # Minimum element
max(arr) # Maximum element
# Array predicates
all(arr, lambda x: x > 0) # All elements satisfy predicate
any(arr, lambda x: x > 0) # Some element satisfies predicate
none(arr, lambda x: x < 0) # No element satisfies predicate
# Array construction
var arr: Array[Int] = [1, 2, 3, 4, 5]
# Array comprehension
var squares = [i * i for i in 0..10]
var evens = [i for i in 0..100 if i % 2 == 0]
```
### String Operations
```csdl
# String properties
len(str) # Length of string
str.length # Alternative syntax
# String operations
str1 + str2 # Concatenation
str[i] # Character at index i
str[i..j] # Substring from i to j
# String predicates
str contains sub # Substring test
str starts_with pre # Prefix test
str ends_with suf # Suffix test
str matches regex # Regular expression match
# String functions
to_int(str) # Parse string to integer
to_string(x) # Convert value to string
```
### Set Operations
```csdl
# Set literals
var S: Set[Int] = {1, 2, 3, 4, 5}
# Set operations
x in S # Membership
S union T # Union
S intersect T # Intersection
S diff T # Difference
S.card() # Cardinality
S.empty() # Test if empty
# Set comprehension
var primes = {x for x in 2..100 if is_prime(x)}
```
### Built-in Constraint Patterns
```csdl
# All different constraint
distinct(x1, x2, x3, ..., xn)
alldifferent([x1, x2, x3, ..., xn])
# Cardinality constraints
atmost k of [c1, c2, ..., cn] # At most k constraints true
atleast k of [c1, c2, ..., cn] # At least k constraints true
exactly k of [c1, c2, ..., cn] # Exactly k constraints true
# Ordering constraints
increasing([x1, x2, ..., xn]) # x1 <= x2 <= ... <= xn
strictly_increasing([x1, x2, ..., xn]) # x1 < x2 < ... < xn
decreasing([x1, x2, ..., xn]) # x1 >= x2 >= ... >= xn
# Range constraints
x in_range [min, max] # min <= x <= max
x not_in_range [min, max] # x < min or x > max
```
## Constraint Specification
### Basic Constraints
```csdl
# Simple assertions
x > 0
y + z == 10
flag => (x != 0)
# Named constraints for reference
constraint positive_x: x > 0
constraint sum_ten: y + z == 10
```
### Conditional Constraints
```csdl
# If-then-else
if use_feature then feature_enabled else not feature_enabled
# Implication
x > 0 => y > 0
# Multiple conditions
if x > 100 then "large"
else if x > 10 then "medium"
else "small"
```
### Global Constraints
```csdl
# Assert: Must be satisfied (hard constraint)
assert: x + y == 10
assert positive: x > 0
# Soft constraints (for optimization)
soft: x > 10 # Default weight 1
soft expensive: cost < 100 weight 5
# Check satisfiability of specific formula
check_sat: (x > 0 and y > 0) or (x < 0 and y < 0)
```
### Optimization Objectives
```csdl
# Minimization
minimize: cost
minimize total_cost: x + y + z
# Maximization
maximize: profit
maximize efficiency: output / input
# Multi-objective (lexicographic order)
minimize: cost
maximize: quality
```
## User-Defined Functions
```csdl
# Function definition
function is_even(n: Int) -> Bool:
n % 2 == 0
function factorial(n: Int) -> Int:
if n <= 1 then 1
else n * factorial(n - 1)
# Recursive functions (with base case)
function gcd(a: Int, b: Int) -> Int:
if b == 0 then a
else gcd(b, a % b)
# Usage in constraints
assert: is_even(x)
assert: factorial(5) == 120
```
## Custom Constraint Types
```csdl
# Define reusable constraint pattern
constraint_type AllDifferent(vars: Array[Int]):
forall i in 0..len(vars)-1:
forall j in i+1..len(vars)-1:
vars[i] != vars[j]
constraint_type Ordered(vars: Array[Int]):
forall i in 0..len(vars)-2:
vars[i] <= vars[i+1]
# Usage
var a, b, c: Int
AllDifferent([a, b, c])
Ordered([a, b, c])
```
## Theory-Specific Extensions
### Bit Vectors
```csdl
var x: BitVec[32]
var y: BitVec[32]
# Bitwise operations
x & y # Bitwise AND
x | y # Bitwise OR
x ^ y # Bitwise XOR
~x # Bitwise NOT
x << n # Left shift
x >> n # Right shift (logical)
x >>> n # Right shift (arithmetic)
# Bit manipulation
x.extract(high, low) # Extract bits [high:low]
x.concat(y) # Concatenate bit vectors
x.rotate_left(n) # Rotate left
x.rotate_right(n) # Rotate right
```
### Algebraic Data Types
```csdl
# Define algebraic datatype
datatype List:
| Nil
| Cons(head: Int, tail: List)
datatype Tree:
| Leaf(value: Int)
| Node(left: Tree, right: Tree)
# Pattern matching
function length(lst: List) -> Int:
match lst:
case Nil: 0
case Cons(_, tail): 1 + length(tail)
```
### Uninterpreted Functions
```csdl
# Declare uninterpreted function
function hash(s: String) -> Int # No body = uninterpreted
# Constraints on uninterpreted functions
assert: hash("abc") == hash("abc") # Consistency
assert: "x" != "y" => hash("x") != hash("y") # Injectivity
```
## Error Handling and Validation
### Type Errors
```csdl
# Type mismatch error
var x: Int = "hello" # ERROR: Cannot assign String to Int
# Operation type error
var y: Bool = 5 + true # ERROR: Cannot add Int and Bool
```
### Validation Rules
1. **All variables must be declared before use**
```csdl
x > 0 # ERROR: x not declared
```
2. **Types must be compatible in operations**
```csdl
var x: Int
var s: String
x + s # ERROR: Cannot add Int and String
```
3. **Array indices must be Int**
```csdl
var arr: Array[Int]
arr[3.14] # ERROR: Array index must be Int
```
4. **Quantifier domains must be finite or bounded**
```csdl
forall x: x > 0 # ERROR: Unbounded quantification
forall x in 1..100: x > 0 # OK: Bounded
```
5. **Division by zero must be prevented**
```csdl
assert: y != 0
var result = x / y # OK: y != 0 is asserted
```
## Complete Examples
### Example 1: N-Queens Problem
```csdl
# Solve the N-Queens problem for 8x8 board
const n: Int = 8
var queens: Array[Int] # queens[i] = column position of queen in row i
# Each queen must be in a valid column
forall i in 0..n-1:
queens[i] >= 0 and queens[i] < n
# All queens in different columns
forall i in 0..n-1:
forall j in i+1..n-1:
queens[i] != queens[j]
# No diagonal attacks
forall i in 0..n-1:
forall j in i+1..n-1:
abs(queens[i] - queens[j]) != abs(i - j)
check_sat
```
### Example 2: Meeting Scheduler
```csdl
# Schedule 3 meetings without conflicts
var m1_start, m1_end: Int
var m2_start, m2_end: Int
var m3_start, m3_end: Int
# Working hours: 9 AM to 5 PM (minutes from midnight)
const WORK_START: Int = 540 # 9:00 AM
const WORK_END: Int = 1020 # 5:00 PM
const MIN_DURATION: Int = 30 # 30 minutes
# All meetings within work hours
forall start, end in [(m1_start, m1_end), (m2_start, m2_end), (m3_start, m3_end)]:
start >= WORK_START and end <= WORK_END
end >= start + MIN_DURATION
# No overlaps between meetings
function no_overlap(s1: Int, e1: Int, s2: Int, e2: Int) -> Bool:
e1 <= s2 or e2 <= s1
assert: no_overlap(m1_start, m1_end, m2_start, m2_end)
assert: no_overlap(m1_start, m1_end, m3_start, m3_end)
assert: no_overlap(m2_start, m2_end, m3_start, m3_end)
# Minimize total schedule length
minimize: max(m1_end, m2_end, m3_end) - min(m1_start, m2_start, m3_start)
```
### Example 3: Array Bounds Safety Verification
```csdl
# Verify array access is always safe
var arr: Array[Int]
const LENGTH: Int = 10
var index: Int
# Preconditions
assert: LENGTH > 0
assert: index >= 0
assert: index < LENGTH
# The access arr[index] is now provably safe
# Verify safety property
check_sat: index >= 0 and index < LENGTH # Should be SAT (valid)
```
### Example 4: Sudoku Solver
```csdl
# 9x9 Sudoku solver
const SIZE: Int = 9
const BOX_SIZE: Int = 3
var grid: Array[Array[Int]]
# Initialize with known values (0 = empty)
grid[0][0] == 5
grid[0][1] == 3
# ... more initial values ...
# All cells must be 1-9
forall i in 0..SIZE-1:
forall j in 0..SIZE-1:
if grid[i][j] == 0 then
grid[i][j] >= 1 and grid[i][j] <= SIZE
else
true # Keep initial value
# Row constraints: all different
forall i in 0..SIZE-1:
distinct([grid[i][j] for j in 0..SIZE-1])
# Column constraints: all different
forall j in 0..SIZE-1:
distinct([grid[i][j] for i in 0..SIZE-1])
# 3x3 box constraints: all different
forall box_row in 0..BOX_SIZE-1:
forall box_col in 0..BOX_SIZE-1:
var cells = [
grid[box_row * BOX_SIZE + i][box_col * BOX_SIZE + j]
for i in 0..BOX_SIZE-1
for j in 0..BOX_SIZE-1
]
distinct(cells)
check_sat
```
### Example 5: Package Dependency Resolver
```csdl
# Resolve package dependencies and conflicts
var pkg_a_version: Int # Versions: 1, 2, 3
var pkg_b_version: Int # Versions: 1, 2
var pkg_c_version: Int # Versions: 1, 2, 3
# Version constraints
pkg_a_version >= 1 and pkg_a_version <= 3
pkg_b_version >= 1 and pkg_b_version <= 2
pkg_c_version >= 1 and pkg_c_version <= 3
# Dependency: pkg_a v3 requires pkg_b v2
if pkg_a_version == 3 then pkg_b_version == 2 else true
# Conflict: pkg_b v1 conflicts with pkg_c v3
not (pkg_b_version == 1 and pkg_c_version == 3)
# Compatibility: pkg_a v1 only works with pkg_c v1 or v2
if pkg_a_version == 1 then pkg_c_version <= 2 else true
# Optimization: prefer latest versions
maximize: pkg_a_version + pkg_b_version + pkg_c_version
```
### Example 6: Overflow Detection
```csdl
# Detect integer overflow in 32-bit arithmetic
var a: BitVec[32]
var b: BitVec[32]
var sum: BitVec[32]
sum == a + b
# Define overflow conditions
var overflow: Bool =
(a.extract(31, 31) == 0 and # a is positive
b.extract(31, 31) == 0 and # b is positive
sum.extract(31, 31) == 1) or # sum is negative
(a.extract(31, 31) == 1 and # a is negative
b.extract(31, 31) == 1 and # b is negative
sum.extract(31, 31) == 0) # sum is positive
# Find inputs that cause overflow
check_sat: overflow
```
## Best Practices
### 1. Use Meaningful Names
```csdl
# Good
var num_employees: Int
var total_salary: Real
# Avoid
var x: Int
var y: Real
```
### 2. Add Comments
```csdl
# Calculate bonus based on performance
var bonus: Real
if performance_score >= 90 then
bonus == base_salary * 0.20 # 20% bonus for excellent
else if performance_score >= 75 then
bonus == base_salary * 0.10 # 10% bonus for good
else
bonus == 0 # No bonus
```
### 3. Factor Out Complex Constraints
```csdl
# Define reusable predicates
function is_valid_date(year: Int, month: Int, day: Int) -> Bool:
year >= 1900 and year <= 2100 and
month >= 1 and month <= 12 and
day >= 1 and day <= 31
# Use in constraints
assert: is_valid_date(birth_year, birth_month, birth_day)
```
### 4. Bound Quantifiers
```csdl
# Avoid unbounded quantification
forall x: P(x) # Undecidable in general
# Use bounded quantification
forall x in 1..1000: P(x) # Decidable
```
### 5. Use Type Annotations for Clarity
```csdl
# Explicit types make intent clear
function compute_average(values: Array[Int]) -> Real:
sum(values) / len(values)
```
## Integration with Logic-Thinking MCP Server
The CSDL will integrate with the existing logic-thinking MCP server as a new logic system:
```typescript
// New system type
export type LogicalSystem =
'syllogistic' | 'propositional' | 'predicate' | 'mathematical' |
'modal' | 'temporal' | 'fuzzy' | 'deontic' | 'constraint' | 'auto';
// New operations
export type Operation =
'validate' | 'formalize' | 'visualize' | 'solve' | 'optimize';
// Usage via MCP
{
"system": "constraint",
"operation": "solve",
"input": "var x, y: Int\nx + y == 10\nx > y\nminimize: x"
}
```
## Grammar Summary (EBNF)
```ebnf
program ::= (declaration | constraint)*
declaration ::= var_decl | const_decl | function_decl | constraint_type_decl
var_decl ::= 'var' identifier_list ':' type ('=' expr)?
const_decl ::= 'const' identifier ':' type '=' expr
function_decl ::= 'function' identifier '(' params ')' '->' type ':' expr
constraint_type_decl ::= 'constraint_type' identifier '(' params ')' ':' constraint*
constraint ::= 'assert' (':' identifier)? ':' expr
| 'soft' (':' identifier)? ':' expr ('weight' number)?
| 'check_sat' ':' expr
| 'minimize' (':' identifier)? ':' expr
| 'maximize' (':' identifier)? ':' expr
| expr
expr ::= logical_expr
logical_expr ::= comparison_expr (('and' | '&&' | 'or' | '||' | '=>' | '<=>') comparison_expr)*
comparison_expr ::= additive_expr (('==' | '!=' | '<' | '<=' | '>' | '>=') additive_expr)?
additive_expr ::= multiplicative_expr (('+' | '-') multiplicative_expr)*
multiplicative_expr ::= unary_expr (('*' | '/' | 'div' | '%') unary_expr)*
unary_expr ::= ('-' | 'not' | '!' | '~') unary_expr
| primary_expr
primary_expr ::= literal
| identifier
| identifier '(' expr_list ')'
| identifier '[' expr ']'
| 'if' expr 'then' expr 'else' expr
| 'forall' identifier 'in' domain ':' expr
| 'exists' identifier 'in' domain ':' expr
| '(' expr ')'
| '[' expr_list ']'
| '{' expr_list '}'
type ::= 'Int' | 'Real' | 'Bool' | 'String'
| 'BitVec' '[' number ']'
| 'Array' '[' type ']'
| 'Tuple' '[' type_list ']'
| 'Set' '[' type ']'
| identifier
domain ::= expr '..' expr
| expr '..<' expr
| '[' expr_list ']'
| identifier
literal ::= number | 'true' | 'false' | string
identifier_list ::= identifier (',' identifier)*
expr_list ::= expr (',' expr)*
type_list ::= type (',' type)*
params ::= identifier ':' type (',' identifier ':' type)*
```
## Conclusion
The Constraint Specification DSL (CSDL) provides a powerful, readable, and extensible way to express constraints for SMT solving. It balances the precision of SMT-LIB with the readability of natural language, making it ideal for both human users and LLM generation. The type system catches errors early, the syntax is familiar to programmers, and the extensibility mechanisms allow for domain-specific constraints without modifying the core language.
