bv: Assert input facts on user-level 0. (#6515)

The bitblast solver currently uses solving under assumptions for all facts that are sent to the bit-vector solver. For input facts on user-level 0 we can however assert the fact to the SAT solver, which allows the SAT solver to do more preprocessing. This PR adds the option to assert user-level 0 input facts, which is disabled by default.

11 files changed, 161 insertions, 14 deletions

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 3172f8d5f..34bdfcdaa 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -243,3 +243,11 @@ name   = "Bitvector theory"
   name = "simple"
   help = "Enables simple bitblasting solver with proof support."
 
+[[option]]
+  name       = "bvAssertInput"
+  category   = "regular"
+  long       = "bv-assert-input"
+  type       = "bool"
+  default    = "false"
+  help       = "assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver"
+
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index a9ee25c11..f4aa04e4d 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -531,12 +531,12 @@ protected:
     bool     isPropagated     (Var x) const; // Does the variable have a propagated variables
     bool     isPropagatedBy   (Var x, const Clause& c) const; // Is the value of the variable propagated by the clause Clause C
 
-    int      level            (Var x) const;
-    int      user_level       (Var x) const; // User level at which this variable was asserted
-    int      intro_level      (Var x) const; // User level at which this variable was created
     int      trail_index      (Var x) const; // Index in the trail
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
 public:
+    int      level            (Var x) const;
+    int      user_level       (Var x) const; // User level at which this variable was asserted
+    int      intro_level      (Var x) const; // User level at which this variable was created
     bool     withinBudget     (uint64_t amount)      const;
     bool withinBudget(Resource r) const;
 
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index b09ffd685..293e7175b 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -259,6 +259,16 @@ bool MinisatSatSolver::isDecision(SatVariable decn) const {
   return d_minisat->isDecision( decn );
 }
 
+int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const
+{
+  return d_minisat->level(v);
+}
+
+int32_t MinisatSatSolver::getIntroLevel(SatVariable v) const
+{
+  return d_minisat->intro_level(v);
+}
+
 SatProofManager* MinisatSatSolver::getProofManager()
 {
   return d_minisat->getProofManager();
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index a4bd1e7a0..0e6ca28b8 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -85,6 +85,10 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
 
   bool isDecision(SatVariable decn) const override;
 
+  int32_t getDecisionLevel(SatVariable v) const override;
+
+  int32_t getIntroLevel(SatVariable v) const override;
+
   /** Retrieve a pointer to the unerlying solver. */
   Minisat::SimpSolver* getSolver() { return d_minisat; }
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 70401c56d..63591e74b 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -340,6 +340,20 @@ bool PropEngine::isDecision(Node lit) const {
   return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable());
 }
 
+int32_t PropEngine::getDecisionLevel(Node lit) const
+{
+  Assert(isSatLiteral(lit));
+  return d_satSolver->getDecisionLevel(
+      d_cnfStream->getLiteral(lit).getSatVariable());
+}
+
+int32_t PropEngine::getIntroLevel(Node lit) const
+{
+  Assert(isSatLiteral(lit));
+  return d_satSolver->getIntroLevel(
+      d_cnfStream->getLiteral(lit).getSatVariable());
+}
+
 void PropEngine::printSatisfyingAssignment(){
   const CnfStream::NodeToLiteralMap& transCache =
     d_cnfStream->getTranslationCache();
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 631317c2d..a12816906 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -157,6 +157,22 @@ class PropEngine
   bool isDecision(Node lit) const;
 
   /**
+   * Return the current decision level of `lit`.
+   *
+   * @param lit: The node in question, must have an associated SAT literal.
+   * @return Decision level of the SAT variable of `lit` (phase is disregarded),
+   *         or -1 if `lit` has not been assigned yet.
+   */
+  int32_t getDecisionLevel(Node lit) const;
+
+  /**
+   * Return the user-context level when `lit` was introduced..
+   *
+   * @return User-context level or -1 if not yet introduced.
+   */
+  int32_t getIntroLevel(Node lit) const;
+
+  /**
    * Checks the current context for satisfiability.
    *
    */
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 1c64c92c2..963810594 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -168,6 +168,16 @@ class CDCLTSatSolverInterface : public SatSolver
 
   virtual bool isDecision(SatVariable decn) const = 0;
 
+  /**
+   * Return the current decision level of `lit`.
+   */
+  virtual int32_t getDecisionLevel(SatVariable v) const { return -1; }
+
+  /**
+   * Return the user-context level when `lit` was introduced..
+   */
+  virtual int32_t getIntroLevel(SatVariable v) const { return -1; }
+
   virtual std::shared_ptr<ProofNode> getProof() = 0;
 
 }; /* class CDCLTSatSolverInterface */
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index ecf2bafb6..b01ba2580 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -34,7 +34,9 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s,
       d_nullRegistrar(new prop::NullRegistrar()),
       d_nullContext(new context::Context()),
       d_bbFacts(s->getSatContext()),
+      d_bbInputFacts(s->getSatContext()),
       d_assumptions(s->getSatContext()),
+      d_assertions(s->getSatContext()),
       d_invalidateModelCache(s->getSatContext(), true),
       d_inSatMode(s->getSatContext(), false),
       d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
@@ -76,6 +78,23 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
     }
   }
 
+  NodeManager* nm = NodeManager::currentNM();
+
+  /* Process input assertions bit-blast queue. */
+  while (!d_bbInputFacts.empty())
+  {
+    Node fact = d_bbInputFacts.front();
+    d_bbInputFacts.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->convertAndAssert(bb_fact, false, false);
+    }
+    d_assertions.push_back(fact);
+  }
+
   /* Process bit-blast queue and store SAT literals. */
   while (!d_bbFacts.empty())
   {
@@ -87,7 +106,6 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
       d_bitblaster->bbAtom(fact);
       Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
       d_cnfStream->ensureLiteral(bb_fact);
-
       prop::SatLiteral lit = d_cnfStream->getLiteral(bb_fact);
       d_factLiteralCache[fact] = lit;
       d_literalFactCache[lit] = fact;
@@ -106,25 +124,51 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
   {
     std::vector<prop::SatLiteral> unsat_assumptions;
     d_satSolver->getUnsatAssumptions(unsat_assumptions);
-    Assert(unsat_assumptions.size() > 0);
 
-    std::vector<Node> conflict;
-    for (const prop::SatLiteral& lit : unsat_assumptions)
+    Node conflict;
+    // Unsat assumptions produce conflict.
+    if (unsat_assumptions.size() > 0)
     {
-      conflict.push_back(d_literalFactCache[lit]);
-      Debug("bv-bitblast") << "unsat assumption (" << lit
-                           << "): " << conflict.back() << std::endl;
+      std::vector<Node> conf;
+      for (const prop::SatLiteral& lit : unsat_assumptions)
+      {
+        conf.push_back(d_literalFactCache[lit]);
+        Debug("bv-bitblast")
+            << "unsat assumption (" << lit << "): " << conf.back() << std::endl;
+      }
+      conflict = nm->mkAnd(conf);
     }
-
-    NodeManager* nm = NodeManager::currentNM();
-    d_im.conflict(nm->mkAnd(conflict), InferenceId::BV_BITBLAST_CONFLICT);
+    else  // Input assertions produce conflict.
+    {
+      std::vector<Node> assertions(d_assertions.begin(), d_assertions.end());
+      conflict = nm->mkAnd(assertions);
+    }
+    d_im.conflict(conflict, InferenceId::BV_BITBLAST_CONFLICT);
   }
 }
 
 bool BVSolverBitblast::preNotifyFact(
     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 {
-  d_bbFacts.push_back(fact);
+  Valuation& val = d_state.getValuation();
+
+  /**
+   * Check whether `fact` is an input assertion on user-level 0.
+   *
+   * If this is the case we can assert `fact` to the SAT solver instead of
+   * using assumptions.
+   */
+  if (options::bvAssertInput() && val.isSatLiteral(fact)
+      && !val.isDecision(fact) && val.getDecisionLevel(fact) == 0
+      && val.getIntroLevel(fact) == 0)
+  {
+    d_bbInputFacts.push_back(fact);
+  }
+  else
+  {
+    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 36c06209a..f98121a63 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -33,6 +33,8 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
+class BBRegistrar;
+
 /**
  * Bit-blasting solver with support for different SAT back ends.
  */
@@ -94,6 +96,7 @@ class BVSolverBitblast : public BVSolver
 
   /** Used for initializing `d_cnfStream`. */
   std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
+
   std::unique_ptr<context::Context> d_nullContext;
 
   /** SAT solver back end (configured via options::bvSatSolver. */
@@ -108,9 +111,19 @@ class BVSolverBitblast : public BVSolver
    */
   context::CDQueue<Node> d_bbFacts;
 
+  /**
+   * Bit-blast queue for user-level 0 input facts sent to this solver.
+   *
+   * Get populated on preNotifyFact().
+   */
+  context::CDQueue<Node> d_bbInputFacts;
+
   /** Corresponds to the SAT literals of the currently asserted facts. */
   context::CDList<prop::SatLiteral> d_assumptions;
 
+  /** Stores the current input assertions. */
+  context::CDList<Node> d_assertions;
+
   /** Flag indicating whether `d_modelCache` should be invalidated. */
   context::CDO<bool> d_invalidateModelCache;
 
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 937fcd5fa..621f89539 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -188,6 +188,18 @@ bool Valuation::isDecision(Node lit) const {
   return d_engine->getPropEngine()->isDecision(lit);
 }
 
+int32_t Valuation::getDecisionLevel(Node lit) const
+{
+  Assert(d_engine != nullptr);
+  return d_engine->getPropEngine()->getDecisionLevel(lit);
+}
+
+int32_t Valuation::getIntroLevel(Node lit) const
+{
+  Assert(d_engine != nullptr);
+  return d_engine->getPropEngine()->getIntroLevel(lit);
+}
+
 unsigned Valuation::getAssertionLevel() const{
   Assert(d_engine != nullptr);
   return d_engine->getPropEngine()->getAssertionLevel();
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index a1a3db706..7438279b1 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -185,6 +185,22 @@ public:
   bool isDecision(Node lit) const;
 
   /**
+   * Return the current decision level of `lit`.
+   *
+   * @param lit: The node in question, must have an associated SAT literal.
+   * @return Decision level of the SAT variable of `lit` (phase is disregarded),
+   *         or -1 if `lit` has not been assigned yet.
+   */
+  int32_t getDecisionLevel(Node lit) const;
+
+  /**
+   * Return the user-context level when `lit` was introduced..
+   *
+   * @return User-context level or -1 if not yet introduced.
+   */
+  int32_t getIntroLevel(Node lit) const;
+
+  /**
    * Get the assertion level of the SAT solver.
    */
   unsigned getAssertionLevel() const;