logicaffeine_tv/equiv.rs
1//! The SMT equivalence primitive, built on `logicaffeine_verify::check_equivalence`.
2
3use logicaffeine_verify::{check_equivalence, EquivalenceResult, VerifyExpr};
4
5/// Prove that a `Bool`-sorted `VerifyExpr` is valid (true under every assignment of its
6/// free variables).
7///
8/// Implemented as an equivalence check against the constant `true`: the backend asserts
9/// `¬(pred ↔ true)` and asks Z3 for a model. `Unsat` ⇒ the predicate is valid
10/// ([`EquivalenceResult::Equivalent`]); `Sat` ⇒ a counterexample assignment
11/// ([`EquivalenceResult::NotEquivalent`]).
12pub fn prove_valid(pred: &VerifyExpr) -> EquivalenceResult {
13 check_equivalence(pred, &VerifyExpr::bool(true), &[], 1)
14}
15
16/// True iff [`prove_valid`] proves the predicate.
17pub fn is_valid(pred: &VerifyExpr) -> bool {
18 matches!(prove_valid(pred), EquivalenceResult::Equivalent)
19}