bv: Add support for --bitblast=eager. (#6516)

This PR adds support for handling --bitblast=eager in the new bitblast solver.

3 files changed, 102 insertions, 15 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index b97c99eae..7c5d775ed 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -162,10 +162,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
           "Incremental eager bit-blasting is currently "
           "only supported for QF_BV. Try --bitblast=lazy.");
     }
-
-    // Force lazy solver since we don't handle EAGER_ATOMS in the
-    // BVSolver::BITBLAST solver.
-    opts.set(options::bvSolver, options::BVSolver::LAZY);
   }
 
   /* Only BVSolver::LAZY natively supports int2bv and nat2bv, for other solvers
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index b01ba2580..463a937fd 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -26,12 +26,54 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
+/**
+ * Bit-blasting registrar.
+ *
+ * The CnfStream calls preRegister() if it encounters a theory atom.
+ * This registrar bit-blasts given atom and remembers which bit-vector atoms
+ * were bit-blasted.
+ *
+ * This registrar is needed when --bitblast=eager is enabled.
+ */
+class BBRegistrar : public prop::Registrar
+{
+ public:
+  BBRegistrar(BBSimple* bb) : d_bitblaster(bb) {}
+
+  void preRegister(Node n) override
+  {
+    if (d_registeredAtoms.find(n) != d_registeredAtoms.end())
+    {
+      return;
+    }
+    /* We are only interested in bit-vector atoms. */
+    if ((n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
+        || n.getKind() == kind::BITVECTOR_ULT
+        || n.getKind() == kind::BITVECTOR_ULE
+        || n.getKind() == kind::BITVECTOR_SLT
+        || n.getKind() == kind::BITVECTOR_SLE)
+    {
+      d_registeredAtoms.insert(n);
+      d_bitblaster->bbAtom(n);
+    }
+  }
+
+  std::unordered_set<TNode>& getRegisteredAtoms() { return d_registeredAtoms; }
+
+ private:
+  /** The bitblaster used. */
+  BBSimple* d_bitblaster;
+
+  /** Stores bit-vector atoms encounterd on preRegister(). */
+  std::unordered_set<TNode> d_registeredAtoms;
+};
+
 BVSolverBitblast::BVSolverBitblast(TheoryState* s,
                                    TheoryInferenceManager& inferMgr,
                                    ProofNodeManager* pnm)
     : BVSolver(*s, inferMgr),
       d_bitblaster(new BBSimple(s)),
-      d_nullRegistrar(new prop::NullRegistrar()),
+      d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
       d_nullContext(new context::Context()),
       d_bbFacts(s->getSatContext()),
       d_bbInputFacts(s->getSatContext()),
@@ -61,7 +103,7 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s,
           smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
   }
   d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
-                                        d_nullRegistrar.get(),
+                                        d_bbRegistrar.get(),
                                         d_nullContext.get(),
                                         nullptr,
                                         smt::currentResourceManager()));
@@ -88,9 +130,16 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
     /* 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->convertAndAssert(bb_fact, false, false);
+      if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
+      {
+        handleEagerAtom(fact, true);
+      }
+      else
+      {
+        d_bitblaster->bbAtom(fact);
+        Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
+        d_cnfStream->convertAndAssert(bb_fact, false, false);
+      }
     }
     d_assertions.push_back(fact);
   }
@@ -103,10 +152,19 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
     /* 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);
+      prop::SatLiteral lit;
+      if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
+      {
+        handleEagerAtom(fact, false);
+        lit = d_cnfStream->getLiteral(fact[0]);
+      }
+      else
+      {
+        d_bitblaster->bbAtom(fact);
+        Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
+        d_cnfStream->ensureLiteral(bb_fact);
+        lit = d_cnfStream->getLiteral(bb_fact);
+      }
       d_factLiteralCache[fact] = lit;
       d_literalFactCache[lit] = fact;
     }
@@ -322,6 +380,32 @@ Node BVSolverBitblast::getValue(TNode node)
   return it->second;
 }
 
+void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact)
+{
+  Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
+
+  if (assertFact)
+  {
+    d_cnfStream->convertAndAssert(fact[0], false, false);
+  }
+  else
+  {
+    d_cnfStream->ensureLiteral(fact[0]);
+  }
+
+  /* convertAndAssert() does not make the connection between the bit-vector
+   * atom and it's bit-blasted form (it only calls preRegister() from the
+   * registrar). Thus, we add the equalities now. */
+  auto& registeredAtoms = d_bbRegistrar->getRegisteredAtoms();
+  for (auto atom : registeredAtoms)
+  {
+    Node bb_atom = d_bitblaster->getStoredBBAtom(atom);
+    d_cnfStream->convertAndAssert(atom.eqNode(bb_atom), false, false);
+  }
+  // Clear cache since we only need to do this once per bit-blasted atom.
+  registeredAtoms.clear();
+}
+
 }  // namespace bv
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index f98121a63..3da08f868 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -84,6 +84,14 @@ class BVSolverBitblast : public BVSolver
   Node getValue(TNode node);
 
   /**
+   * Handle BITVECTOR_EAGER_ATOM atoms and assert/assume to CnfStream.
+   *
+   * @param assertFact: Indicates whether the fact should be asserted (true) or
+   * assumed (false).
+   */
+  void handleEagerAtom(TNode fact, bool assertFact);
+
+  /**
    * Cache for getValue() calls.
    *
    * Is cleared at the beginning of a getValue() call if the
@@ -95,8 +103,7 @@ class BVSolverBitblast : public BVSolver
   std::unique_ptr<BBSimple> d_bitblaster;
 
   /** Used for initializing `d_cnfStream`. */
-  std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
-
+  std::unique_ptr<BBRegistrar> d_bbRegistrar;
   std::unique_ptr<context::Context> d_nullContext;
 
   /** SAT solver back end (configured via options::bvSatSolver. */