A CDCL(T) SMT solver implementation designed for integration with programming language compilers, particularly those with complex type systems like Rust or similar languages.
- Efficient CDCL SAT Engine: Watched-literals propagation, conflict-driven clause learning with 1-UIP analysis
- EUF Theory Solver: Equality with Uninterpreted Functions using e-graphs (egg library)
- Smart Restarts: Geometric progression restart strategy with activity decay
- Advanced Clause Learning: Recursive domination-based clause minimization
- VSIDS Heuristics: Variable State Independent Decaying Sum decision heuristic
- Generic Identifier Support: Literals carry external identifiers (e.g., source spans) for precise error reporting
- Theory Solver Interface: Clean trait-based architecture for adding new theories
- Domain-Specific Heuristics: Pluggable decision heuristics (includes Flurry language example)
- Incremental Solving: Push/pop API for scoped assumptions
- Performance Metrics: Comprehensive timing and counter collection
- Model Extraction: Complete models including EUF representatives
- Unsat Core Generation: Minimal unsatisfiable core extraction for precise error reporting
- Theory Propagation: Bidirectional SAT ↔ Theory propagation
- Conflict Explanation: Theory-aware explanation generation using e-graph paths
use say_you::*;
// Create a formula builder
let mut builder: IrBuilder<u32> = IrBuilder::new();
// Add boolean variables
let p = builder.fresh_var("p", Some(1));
let q = builder.fresh_var("q", Some(2));
// Add clauses: (p ∨ q) ∧ (¬p ∨ q)
builder.add_clause(vec![
builder.lit_var(&p, false), // p
builder.lit_var(&q, false), // q
]);
builder.add_clause(vec![
builder.lit_var(&p, true), // ¬p
builder.lit_var(&q, false), // q
]);
// Create and run solver
let mut solver = Solver::from_ir(&builder);
match solver.solve() {
SolveResult::Sat(model) => {
println!("SAT! Model: {:?}", model);
}
SolveResult::Unsat { core } => {
println!("UNSAT! Core: {:?}", core);
}
}
// Print performance metrics
println!("{}", solver.metrics().report());// Create EUF terms and equalities
let mut builder: IrBuilder<u32> = IrBuilder::new();
let a = builder.t_var("a");
let b = builder.t_var("b");
let c = builder.t_var("c");
let f_a = builder.t_app("f", vec![a.clone()]);
let f_b = builder.t_app("f", vec![b.clone()]);
// Add equality constraints: a = b ∧ f(a) ≠ f(b)
builder.add_clause(vec![builder.lit_eq(a, b)]);
builder.add_clause(vec![builder.lit_eq(f_a, f_b).not()]);
let mut solver = Solver::from_ir(&builder);
// This will be UNSAT due to congruencelet mut solver = Solver::from_ir(&builder);
// Push scope
solver.push();
// Add temporary assumptions
// ... add more clauses ...
// Check satisfiability
let result = solver.solve();
// Pop back to previous state
solver.pop();The solver follows a modular CDCL(T) architecture:
┌─────────────────┐
│ Core Solver │ ← Main CDCL(T) loop, manages SAT/Theory coordination
├─────────────────┤
│ SAT Engine │ ← Watched-literals BCP, conflict analysis, learning
├─────────────────┤
│ Theory Solvers │ ← EUF (egg-based), extensible via TheorySolver trait
├─────────────────┤
│ Heuristics │ ← VSIDS, domain-specific decision strategies
├─────────────────┤
│ IR Builder │ ← Formula construction with generic identifiers
└─────────────────┘
ir: Formula representation with generic identifiers for source mappingsat: High-performance SAT engine with modern CDCL techniquestheory: Theory solver interface and EUF implementationcore: Main solver coordinating SAT and Theory layersheuristics: Pluggable decision strategiesmodel: Model extraction and representationmetrics: Performance monitoring and reporting
- Memory Efficient: Watched-literals minimize memory overhead
- Conflict-Driven: Aggressive clause learning with minimization
- Theory-Aware: Tight SAT-Theory integration minimizes overhead
- Incremental: Efficient push/pop operations for scoped solving
This solver is particularly well-suited for:
- Type Checking: Complex type system constraints with equality reasoning
- Program Verification: SMT queries arising from static analysis
- Constraint Solving: Mathematical constraint satisfaction with theories
- Interactive Tools: IDE integration requiring fast incremental solving
Implement the TheorySolver<ID> trait:
impl<ID: Identifier> TheorySolver<ID> for MyTheory {
fn assert_literal(&mut self, lit: &Literal<ID>) -> Result<TheoryEffect<ID>, TheoryConflict<ID>> {
// Handle theory-specific literals
}
fn propagate(&mut self) -> Vec<Literal<ID>> {
// Return theory consequences
}
fn explain(&mut self, lit: &Literal<ID>) -> Option<Clause<ID>> {
// Generate explanation for theory propagation
}
// ... snapshot/restore for incrementality
}Implement the DecisionHeuristic<ID> trait:
impl<ID: Identifier> DecisionHeuristic<ID> for MyHeuristic {
fn suggest_decision(&mut self, candidates: &[VarId], activities: &[f64]) -> Option<VarId> {
// Custom decision logic
}
fn bias_activities(&mut self, activities: &mut [f64]) {
// Boost/penalize specific variables
}
fn on_learned_clause(&mut self, clause: &Clause<ID>) {
// Learn from conflict patterns
}
}cargo test # Run unit tests
cargo test --release # Run performance tests
cargo run --example demo # Run example scenariosThe solver provides detailed metrics for optimization:
let metrics = solver.metrics();
println!("Decisions: {}", metrics.decisions);
println!("Conflicts: {}", metrics.conflicts);
println!("Solve time: {:.3}s", metrics.solve_time as f64 / 1_000_000_000.0);
println!("{}", metrics.report()); // Full reportContributions welcome! Areas of interest:
- Additional theory solvers (arithmetic, bit-vectors, arrays)
- Advanced restart strategies
- Parallel solving capabilities
- More sophisticated heuristics
- Performance optimizations