View Source cure_smt_solver (cure v0.7.0)
SMT Solver Integration for Cure
This module provides integration with SMT (Satisfiability Modulo Theories) solvers for dependent type constraint verification and optimization. It supports multiple backend solvers including Z3, CVC5, and others.
Features
- Constraint Verification: Prove or disprove type constraints at compile time
- Constraint Simplification: Algebraic and SMT-based constraint simplification
- Guard Optimization: Eliminate redundant runtime checks
- Counterexample Generation: Provide examples when constraints fail
- Multiple Backends: Support for Z3, CVC5, and fallback to symbolic evaluation
Usage
Basic Constraint Checking
Constraint = #binary_op_expr{op = '>', left = VarN, right = Zero},
case cure_smt_solver:check_constraint(Constraint, Env) of
{sat, Model} -> % Constraint is satisfiable
io:format("Satisfiable with model: ~p~n", [Model]);
unsat -> % Constraint is unsatisfiable
io:format("Constraint cannot be satisfied~n");
unknown -> % Solver couldn't determine
io:format("Unknown, need runtime check~n")
end.Simplifying Constraints
% Simplify constraint using algebraic rules and SMT solver
Constraint = #binary_op_expr{op = '+', left = VarX, right = Zero},
Simplified = cure_smt_solver:simplify_constraint(Constraint, Env).
% => Returns VarX (since x + 0 = x)Proving Constraints
% Prove that n > 0 implies length(list) > 0
Result = cure_smt_solver:prove_implication(Antecedent, Consequent, Env).SMT Backend Selection
The module automatically selects available SMT solvers in order of preference:
- Z3 (if available)
- CVC5 (if available)
- Symbolic evaluation fallback
Constraint Translation
Cure constraints are translated to SMT-LIB format:
- Arithmetic: +, -, *, div, rem
- Comparisons: <, >, =<, >=, ==, /=
- Boolean: and, or, not
- Quantifiers: forall, exists (for dependent types)
Summary
Types
-type expr() :: #literal_expr{value :: term(), location :: term()} | #identifier_expr{name :: term(), location :: term()} | #function_call_expr{function :: term(), args :: term(), location :: term()} | #match_expr{expr :: term(), patterns :: term(), location :: term()} | #let_expr{bindings :: term(), body :: term(), location :: term()} | #binary_op_expr{op :: term(), left :: term(), right :: term(), location :: term()} | #unary_op_expr{op :: term(), operand :: term(), location :: term()} | #list_expr{elements :: term(), location :: term()} | #vector_expr{elements :: term(), location :: term()} | #tuple_expr{elements :: term(), location :: term()} | #record_expr{name :: term(), fields :: term(), location :: term()} | #field_access_expr{record :: term(), field :: term(), location :: term()} | #record_update_expr{name :: term(), base :: term(), fields :: term(), location :: term()} | #lambda_expr{params :: term(), body :: term(), location :: term()} | #forall_expr{variables :: term(), body :: term(), location :: term()} | #exists_expr{variables :: term(), body :: term(), location :: term()} | #fsm_spawn_expr{fsm_name :: term(), init_args :: term(), init_state :: term(), location :: term()} | #fsm_send_expr{target :: term(), message :: term(), location :: term()} | #fsm_receive_expr{patterns :: term(), timeout :: term(), location :: term()} | #fsm_state_expr{location :: term()} | #melquiades_send_expr{message :: term(), target :: term(), location :: term()} | #qualified_call_expr{trait_name :: term(), type_args :: term(), method_name :: term(), receiver :: term(), args :: term(), location :: term()}.