View Source cure_guard_smt (cure v0.7.0)
Enhanced SMT Guard Verification
Phase 4 enhancement for guard analysis using Z3 SMT solver.
Features
Guard Completeness Verification
Prove that guards cover all possible input cases:
def abs(x: Int): Int when x >= 0 = x
def abs(x: Int): Int when x < 0 = -x
% SMT proves: ∀x. (x >= 0) ∨ (x < 0) ✅ CompleteCounterexample Generation
Find inputs not covered by any guard:
def sign(x: Int): Int when x > 0 = 1
def sign(x: Int): Int when x < 0 = -1
% SMT finds: x = 0 is uncovered ⚠️Guard Consistency Verification
Detect contradictory or unreachable guards:
def foo(x: Int): Int when x > 0 and x < 0 = 1
% SMT proves: ∀x. ¬(x > 0 ∧ x < 0) ❌ InconsistentSubsumption Detection
Find guards subsumed by earlier guards:
def foo(x: Int): Int when x > 0 = x
def foo(x: Int): Int when x > 5 = x * 2
% SMT proves: (x > 5) ⊆ (x > 0) ⚠️ Clause 2 unreachableSMT Integration
Uses Z3 via the cure_smt_process module:
- Generates SMT-LIB 2.0 queries
- Handles integer and boolean constraints
- Provides counterexamples when available
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()}.