Add bit-level propagation support to BV bitblast solver. (#5906)

This commit adds support for bit-level propagation for the BV bitblast solver to quickly detect conflicts on effort levels != FULL. Bit-level propagation for the bitblast solver is by default disabled for now. Further, bit-blasting of facts is now handled more lazily with a bit-blast queue.

3 files changed, 53 insertions, 19 deletions

diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index 8eb209b53..551c18612 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -38,7 +38,7 @@ void BBSimple::bbAtom(TNode node)
           ? d_atomBBStrategies[normalized.getKind()](normalized, this)
           : normalized;
 
-  storeBBAtom(node, atom_bb);
+  storeBBAtom(node, Rewriter::rewrite(atom_bb));
 }
 
 void BBSimple::storeBBAtom(TNode atom, Node atom_bb)
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 0b5d4cfef..bf264f9cd 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -34,11 +34,15 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s,
       d_bitblaster(new BBSimple(s)),
       d_nullRegistrar(new prop::NullRegistrar()),
       d_nullContext(new context::Context()),
-      d_facts(s->getSatContext()),
+      d_bbFacts(s->getSatContext()),
+      d_assumptions(s->getSatContext()),
       d_invalidateModelCache(s->getSatContext(), true),
       d_inSatMode(s->getSatContext(), false),
       d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
-                : nullptr)
+                : nullptr),
+      d_factLiteralCache(s->getSatContext()),
+      d_literalFactCache(s->getSatContext()),
+      d_propagate(options::bitvectorPropagate())
 {
   if (pnm != nullptr)
   {
@@ -66,25 +70,35 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
 {
   if (level != Theory::Effort::EFFORT_FULL)
   {
-    return;
+    /* Do bit-level propagation only if the SAT solver supports it. */
+    if (!d_propagate || !d_satSolver->setPropagateOnly())
+    {
+      return;
+    }
   }
 
-  std::vector<prop::SatLiteral> assumptions;
-  std::unordered_map<prop::SatLiteral, TNode, prop::SatLiteralHashFunction>
-      node_map;
-  for (const TNode fact : d_facts)
+  /* Process bit-blast queue and store SAT literals. */
+  while (!d_bbFacts.empty())
   {
-    /* Bitblast fact */
-    d_bitblaster->bbAtom(fact);
-    Node bb_fact = Rewriter::rewrite(d_bitblaster->getStoredBBAtom(fact));
-    d_cnfStream->ensureLiteral(bb_fact);
+    Node fact = d_bbFacts.front();
+    d_bbFacts.pop();
+    /* Bit-blast fact and cache literal. */
+    if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
+    {
+      d_bitblaster->bbAtom(fact);
+      Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
+      d_cnfStream->ensureLiteral(bb_fact);
 
-    prop::SatLiteral lit = d_cnfStream->getLiteral(bb_fact);
-    assumptions.push_back(lit);
-    node_map.emplace(lit, fact);
+      prop::SatLiteral lit = d_cnfStream->getLiteral(bb_fact);
+      d_factLiteralCache[fact] = lit;
+      d_literalFactCache[lit] = fact;
+    }
+    d_assumptions.push_back(d_factLiteralCache[fact]);
   }
 
   d_invalidateModelCache.set(true);
+  std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
+                                            d_assumptions.end());
   prop::SatValue val = d_satSolver->solve(assumptions);
   d_inSatMode = val == prop::SatValue::SAT_VALUE_TRUE;
   Debug("bv-bitblast") << "d_inSatMode: " << d_inSatMode << std::endl;
@@ -98,7 +112,9 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
     std::vector<Node> conflict;
     for (const prop::SatLiteral& lit : unsat_assumptions)
     {
-      conflict.push_back(node_map[lit]);
+      conflict.push_back(d_literalFactCache[lit]);
+      Debug("bv-bitblast") << "unsat assumption (" << lit
+                           << "): " << conflict.back() << std::endl;
     }
 
     NodeManager* nm = NodeManager::currentNM();
@@ -109,7 +125,7 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
 bool BVSolverBitblast::preNotifyFact(
     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 {
-  d_facts.push_back(fact);
+  d_bbFacts.push_back(fact);
   return false;  // Return false to enable equality engine reasoning in Theory.
 }
 
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index d9b4a26e9..4eec45e4b 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -107,8 +107,15 @@ class BVSolverBitblast : public BVSolver
   /** CNF stream. */
   std::unique_ptr<prop::CnfStream> d_cnfStream;
 
-  /** Facts sent to this solver. */
-  context::CDList<Node> d_facts;
+  /**
+   * Bit-blast queue for facts sent to this solver.
+   *
+   * Get populated on preNotifyFact().
+   */
+  context::CDQueue<Node> d_bbFacts;
+
+  /** Corresponds to the SAT literals of the currently asserted facts. */
+  context::CDList<prop::SatLiteral> d_assumptions;
 
   /** Flag indicating whether `d_modelCache` should be invalidated. */
   context::CDO<bool> d_invalidateModelCache;
@@ -120,6 +127,17 @@ class BVSolverBitblast : public BVSolver
   std::unique_ptr<EagerProofGenerator> d_epg;
 
   BVProofRuleChecker d_bvProofChecker;
+
+  /** Stores the SatLiteral for a given fact. */
+  context::CDHashMap<Node, prop::SatLiteral, NodeHashFunction>
+      d_factLiteralCache;
+
+  /** Reverse map of `d_factLiteralCache`. */
+  context::CDHashMap<prop::SatLiteral, Node, prop::SatLiteralHashFunction>
+      d_literalFactCache;
+
+  /** Option to enable/disable bit-level propagation. */
+  bool d_propagate;
 };
 
 }  // namespace bv