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.

7 files changed, 82 insertions, 27 deletions

diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index b3563bf28..0324f8128 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -61,6 +61,7 @@ CadicalSolver::CadicalSolver(StatisticsRegistry* registry,
       // Note: CaDiCaL variables start with index 1 rather than 0 since negated
       //       literals are represented as the negation of the index.
       d_nextVarIdx(1),
+      d_inSatMode(false),
       d_statistics(registry, name)
 {
 }
@@ -111,10 +112,10 @@ SatVariable CadicalSolver::falseVar() { return d_false; }
 
 SatValue CadicalSolver::solve()
 {
-  d_assumptions.clear();
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  d_assumptions.clear();
   SatValue res = toSatValue(d_solver->solve());
-  d_okay = (res == SAT_VALUE_TRUE);
+  d_inSatMode = (res == SAT_VALUE_TRUE);
   ++d_statistics.d_numSatCalls;
   return res;
 }
@@ -126,19 +127,25 @@ SatValue CadicalSolver::solve(long unsigned int&)
 
 SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
 {
-  d_assumptions.clear();
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  d_assumptions.clear();
   for (const SatLiteral& lit : assumptions)
   {
     d_solver->assume(toCadicalLit(lit));
     d_assumptions.push_back(lit);
   }
   SatValue res = toSatValue(d_solver->solve());
-  d_okay = (res == SAT_VALUE_TRUE);
+  d_inSatMode = (res == SAT_VALUE_TRUE);
   ++d_statistics.d_numSatCalls;
   return res;
 }
 
+bool CadicalSolver::setPropagateOnly()
+{
+  d_solver->limit("decisions", 0); /* Gets reset after next solve() call. */
+  return true;
+}
+
 void CadicalSolver::getUnsatAssumptions(std::vector<SatLiteral>& assumptions)
 {
   for (const SatLiteral& lit : d_assumptions)
@@ -154,13 +161,13 @@ void CadicalSolver::interrupt() { d_solver->terminate(); }
 
 SatValue CadicalSolver::value(SatLiteral l)
 {
-  Assert(d_okay);
+  Assert(d_inSatMode);
   return toSatValueLit(d_solver->val(toCadicalLit(l)));
 }
 
 SatValue CadicalSolver::modelValue(SatLiteral l)
 {
-  Assert(d_okay);
+  Assert(d_inSatMode);
   return value(l);
 }
 
@@ -169,7 +176,7 @@ unsigned CadicalSolver::getAssertionLevel() const
   Unreachable() << "CaDiCaL does not support assertion levels.";
 }
 
-bool CadicalSolver::ok() const { return d_okay; }
+bool CadicalSolver::ok() const { return d_inSatMode; }
 
 CadicalSolver::Statistics::Statistics(StatisticsRegistry* registry,
                                       const std::string& prefix)
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index 6a7258091..f8b2d3bcd 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -50,6 +50,7 @@ class CadicalSolver : public SatSolver
   SatValue solve() override;
   SatValue solve(long unsigned int&) override;
   SatValue solve(const std::vector<SatLiteral>& assumptions) override;
+  bool setPropagateOnly() override;
   void getUnsatAssumptions(std::vector<SatLiteral>& assumptions) override;
 
   void interrupt() override;
@@ -82,7 +83,7 @@ class CadicalSolver : public SatSolver
   std::vector<SatLiteral> d_assumptions;
 
   unsigned d_nextVarIdx;
-  bool d_okay;
+  bool d_inSatMode;
   SatVariable d_true;
   SatVariable d_false;
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 896233f41..d421155ae 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -81,6 +81,13 @@ public:
     return SAT_VALUE_UNKNOWN;
   };
 
+  /**
+   * Tell SAT solver to only do propagation on next solve().
+   *
+   * @return true if feature is supported, otherwise false.
+   */
+  virtual bool setPropagateOnly() { return false; }
+
   /** Interrupt the solver */
   virtual void interrupt() = 0;
 
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index d18b30430..93196fde4 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -132,6 +132,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     options::bvLazyRewriteExtf.set(false);
   }
 
+  /* Disable bit-level propagation by default for the BITBLAST solver. */
+  if (options::bvSolver() == options::BVSolver::BITBLAST)
+  {
+    options::bitvectorPropagate.set(false);
+  }
+
   if (options::solveIntAsBV() > 0)
   {
     // not compatible with incremental
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