bv: Expand bitblast proof steps in the proof post processor. (#6867)

This commit changes BV proof logging to record coarse-grained bit-blast steps during solving and expanding these steps on-demand in the proof post processor.

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index eb5d8e7afa109dc2f1f4df4127e4543c894896d0..2c04b9e763b4e412aae21982938a8c805e35ebd7 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -79,6 +79,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
         d_pfpp->setEliminateRule(PfRule::THEORY_REWRITE);
       }
     }
+    d_pfpp->setEliminateRule(PfRule::BV_BITBLAST);
   }
   d_false = NodeManager::currentNM()->mkConst(false);
 }

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 6498fa84fb5761f7b33ae1919dba60fba9f2d463..ad9a8f8449e306a2f074d24e33f77c9d96da7fd7 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -23,6 +23,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/builtin/proof_checker.h"
+#include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "util/rational.h"
@@ -1080,6 +1081,16 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
                           << std::endl;
     return sumBounds;
   }
+  else if (id == PfRule::BV_BITBLAST)
+  {
+    bv::BBProof bb(nullptr, d_pnm, true);
+    Node eq = args[0];
+    Assert(eq.getKind() == EQUAL);
+    bb.bbAtom(eq[0]);
+    Node bbAtom = bb.getStoredBBAtom(eq[0]);
+    bb.getProofGenerator()->addProofTo(eq[0].eqNode(bbAtom), cdp);
+    return eq;
+  }
 
   // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
 

diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index a55adaace3046733be82344f2484f964cb75a40a..ea7ba1a13a34a392af5d400cbf4ef212cabb28b2 100644 (file)
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -16,7 +16,6 @@
 
 #include <unordered_set>
 
-#include "options/proof_options.h"
 #include "proof/conv_proof_generator.h"
 #include "theory/theory_model.h"
 
@@ -68,10 +67,23 @@ std::unordered_map<Kind, PfRule, kind::KindHashFunction>
         {kind::BITVECTOR_ROTATE_LEFT, PfRule::BV_BITBLAST_ROTATE_LEFT},
 };
 
-BBProof::BBProof(TheoryState* state,
-                 ProofNodeManager* pnm,
-                 TConvProofGenerator* tcpg)
-    : d_bb(new BBSimple(state)), d_pnm(pnm), d_tcpg(tcpg)
+BBProof::BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained)
+    : d_bb(new BBSimple(state)),
+      d_pnm(pnm),
+      d_tcpg(pnm ? new TConvProofGenerator(
+                 pnm,
+                 nullptr,
+                 /* ONCE to visit each term only once, post-order.  FIXPOINT
+                  * could lead to infinite loops due to terms being rewritten
+                  * to terms that contain themselves */
+                 TConvPolicy::ONCE,
+                 /* STATIC to get the same ProofNode for a shared subterm. */
+                 TConvCachePolicy::STATIC,
+                 "BBProof::TConvProofGenerator",
+                 nullptr,
+                 false)
+                 : nullptr),
+      d_recordFineGrainedProofs(fineGrained)
 {
 }
 
@@ -83,9 +95,7 @@ void BBProof::bbAtom(TNode node)
   visit.push_back(node);
   std::unordered_set<TNode> visited;
 
-  bool fproofs =
-      options::proofGranularityMode() != options::ProofGranularityMode::OFF;
-  bool fpenabled = isProofsEnabled() && fproofs;
+  bool fpenabled = isProofsEnabled() && d_recordFineGrainedProofs;
 
   NodeManager* nm = NodeManager::currentNM();
 
@@ -183,7 +193,8 @@ void BBProof::bbAtom(TNode node)
       visit.pop_back();
     }
   }
-  if (isProofsEnabled() && !fproofs)
+  /* Record coarse-grain bit-blast proof step. */
+  if (isProofsEnabled() && !d_recordFineGrainedProofs)
   {
     Node node_tobv = getStoredBBAtom(node);
     d_tcpg->addRewriteStep(node,
@@ -210,6 +221,8 @@ bool BBProof::collectModelValues(TheoryModel* m,
   return d_bb->collectModelValues(m, relevantTerms);
 }
 
+TConvProofGenerator* BBProof::getProofGenerator() { return d_tcpg.get(); }
+
 bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
 
 }  // namespace bv

diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
index ef23c05c0fb4049882c0ed3489f138271f9c744b..86cbeae8175b931d8b0234ff9d82948019aa6553 100644 (file)
--- a/src/theory/bv/bitblast/proof_bitblaster.h
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -31,7 +31,7 @@ class BBProof
   using Bits = std::vector<Node>;
 
  public:
-  BBProof(TheoryState* state, ProofNodeManager* pnm, TConvProofGenerator* tcpg);
+  BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained);
   ~BBProof();
 
   /** Bit-blast atom 'node'. */
@@ -45,6 +45,8 @@ class BBProof
   /** Collect model values for all relevant terms given in 'relevantTerms'. */
   bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
 
+  TConvProofGenerator* getProofGenerator();
+
  private:
   /** Map node kinds to proof rules. */
   static std::unordered_map<Kind, PfRule, kind::KindHashFunction>
@@ -58,9 +60,11 @@ class BBProof
   /** The associated proof node manager. */
   ProofNodeManager* d_pnm;
   /** The associated term conversion proof generator. */
-  TConvProofGenerator* d_tcpg;
+  std::unique_ptr<TConvProofGenerator> d_tcpg;
   /** Map bit-vector nodes to bit-blasted nodes. */
   std::unordered_map<Node, Node> d_bbMap;
+
+  bool d_recordFineGrainedProofs;
 };
 
 }  // namespace bv

diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index a16bf7eb8bacb5da4fc62b666cc283948d498ca3..4216fa0875d63acb500463be0a31efa718993589 100644 (file)
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -70,20 +70,8 @@ BVSolverSimple::BVSolverSimple(TheoryState* s,
                                TheoryInferenceManager& inferMgr,
                                ProofNodeManager* pnm)
     : BVSolver(*s, inferMgr),
-      d_tcpg(pnm ? new TConvProofGenerator(
-                 pnm,
-                 nullptr,
-                 /* ONCE to visit each term only once, post-order.  FIXPOINT
-                  * could lead to infinite loops due to terms being rewritten
-                  * to terms that contain themselves */
-                 TConvPolicy::ONCE,
-                 /* STATIC to get the same ProofNode for a shared subterm. */
-                 TConvCachePolicy::STATIC,
-                 "BVSolverSimple::TConvProofGenerator",
-                 nullptr,
-                 false)
-                 : nullptr),
-      d_bitblaster(new BBProof(s, pnm, d_tcpg.get()))
+      d_pnm(pnm),
+      d_bitblaster(new BBProof(s, pnm, false))
 {
 }
 
@@ -98,13 +86,14 @@ void BVSolverSimple::addBBLemma(TNode fact)
   Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
   Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
 
-  if (d_tcpg == nullptr)
+  if (d_pnm == nullptr)
   {
     d_im.lemma(lemma, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
   }
   else
   {
-    TrustNode tlem = TrustNode::mkTrustLemma(lemma, d_tcpg.get());
+    TrustNode tlem =
+        TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
     d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
   }
 }
@@ -128,13 +117,14 @@ bool BVSolverSimple::preNotifyFact(
     NodeManager* nm = NodeManager::currentNM();
     Node lemma = nm->mkNode(kind::EQUAL, fact, n);
 
-    if (d_tcpg == nullptr)
+    if (d_pnm == nullptr)
     {
       d_im.lemma(lemma, InferenceId::BV_SIMPLE_LEMMA);
     }
     else
     {
-      TrustNode tlem = TrustNode::mkTrustLemma(lemma, d_tcpg.get());
+      TrustNode tlem =
+          TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
       d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA);
     }
 

diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index 2c23189db07025bf803c32ed67f6e659c49690af..0af4f5b893801ae9d3e787b8bf7f7622eb89d11c 100644 (file)
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -67,8 +67,8 @@ class BVSolverSimple : public BVSolver
    */
   void addBBLemma(TNode fact);
 
-  /** Proof generator. */
-  std::unique_ptr<TConvProofGenerator> d_tcpg;
+  /** Proof node manager. */
+  ProofNodeManager* d_pnm;
   /** Bit-blaster used to bit-blast atoms/terms. */
   std::unique_ptr<BBProof> d_bitblaster;
   /** Proof rule checker */

diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp
index 93ba9e67fd533b19b565b51babd7ec0278d7e9f5..711e9798caa49b7f3644cc6fc387a15883fb3d47 100644 (file)
--- a/src/theory/bv/proof_checker.cpp
+++ b/src/theory/bv/proof_checker.cpp
@@ -72,12 +72,10 @@ Node BVProofRuleChecker::checkInternal(PfRule id,
 {
   if (id == PfRule::BV_BITBLAST)
   {
-    BBSimple bb(nullptr);
     Assert(children.empty());
     Assert(args.size() == 1);
-    bb.bbAtom(args[0]);
-    Node n = bb.getStoredBBAtom(args[0]);
-    return args[0].eqNode(n);
+    Assert(args[0].getKind() == kind::EQUAL);
+    return args[0];
   }
   else if (id == PfRule::BV_BITBLAST_CONST || id == PfRule::BV_BITBLAST_VAR
            || id == PfRule::BV_BITBLAST_EQUAL || id == PfRule::BV_BITBLAST_ULT