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.getLsbD_congr
(i w : Nat)
(e e' : BitVec w)
(h : e' = e)
:
theorem
Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr
(b : Bool)
(e' : BitVec 1)
(h : e' = BitVec.ofBool b)
:
Verify that cert
is an UNSAT proof for the SAT problem obtained by bitblasting bv
.