proofs: Properly track pre- and post-rewrites in bbAtom(). (#7147)

This commit refactors the proof bit-blaster to properly track the pre- and post-rewrites in bbAtom(). The individual bit-blast steps are recorded in a term conversion proof generator. The overall bit-blast proof is stored in a BitblastProofGenerator, which tracks the pre- and post-rewrite and includes the bit-blast proof of the TCPG.

3 files changed, 17 insertions, 0 deletions

diff --git a/test/regress/regress0/bv/bvproof1.smt2 b/test/regress/regress0/bv/bvproof1.smt2
new file mode 100644
index 000000000..a947aa84a
--- /dev/null
+++ b/test/regress/regress0/bv/bvproof1.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_BV)
+(set-info :status unsat)
+(declare-const x Bool)
+(check-sat-assuming ((not (bvuge (bvcomp (_ bv0 4) (_ bv0 4)) (ite x (_ bv1 1) (_ bv0 1))))))
diff --git a/test/regress/regress0/bv/bvproof2.smt2 b/test/regress/regress0/bv/bvproof2.smt2
new file mode 100644
index 000000000..f06194952
--- /dev/null
+++ b/test/regress/regress0/bv/bvproof2.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_ABV)
+(set-info :status unsat)
+(declare-const v (_ BitVec 1))
+(declare-const _v (_ BitVec 2))
+(declare-fun a () (Array (_ BitVec 3) (_ BitVec 2)))
+(assert (not (= (store (store (store a ((_ zero_extend 1) _v) (_ bv0 2)) (_ bv1 3) (_ bv0 2)) (_ bv0 3) (_ bv0 2)) (store (store (store (store a (_ bv0 3) (_ bv0 2)) ((_ zero_extend 2) v) (_ bv0 2)) (_ bv1 3) (_ bv0 2)) ((_ zero_extend 1) _v) (_ bv0 2)))))
+(check-sat)
diff --git a/test/regress/regress0/bv/bvproof3.smt2 b/test/regress/regress0/bv/bvproof3.smt2
new file mode 100644
index 000000000..5650bc5d6
--- /dev/null
+++ b/test/regress/regress0/bv/bvproof3.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --bitblast=eager
+(set-logic QF_BV)
+(set-info :status unsat)
+(declare-const x (_ BitVec 1))
+(assert (= (_ bv2 4) ((_ zero_extend 3) x)))
+(check-sat)