This file contains theorems used for justifying the reflection procedure of bv_decide
.
theorem
Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRightNat_congr
(n w : Nat)
(x x' : BitVec w)
(h : x = x')
:
theorem
Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr
(n w : Nat)
(x x' : BitVec w)
(h1 : x = x')
:
theorem
Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr
(n w : Nat)
(x x' : BitVec w)
(h1 : x = x')
:
theorem
Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr
(n w : Nat)
(expr expr' : BitVec w)
(h : expr' = expr)
:
theorem
Std.Tactic.BVDecide.Reflect.BitVec.extract_congr
(start len w : Nat)
(x x' : BitVec w)
(h1 : x = x')
:
theorem
Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
(n w : Nat)
(x x' : BitVec w)
(h : x = x')
:
theorem
Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
(n w : Nat)
(x x' : BitVec w)
(h : x = x')
:
theorem
Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr
(b : Bool)
(e' : BitVec 1)
(h : e' = BitVec.ofBool b)
:
theorem
Std.Tactic.BVDecide.Reflect.verifyCert_correct
(cnf : Sat.CNF Nat)
(cert : String)
:
verifyCert cnf cert = true → cnf.Unsat
Verify that cert
is an UNSAT proof for the SAT problem obtained by bitblasting bv
.
Equations
Instances For
theorem
Std.Tactic.BVDecide.Reflect.unsat_of_verifyBVExpr_eq_true
(bv : BVLogicalExpr)
(c : String)
(h : verifyBVExpr bv c = true)
:
bv.Unsat