Add option to track and notify from CNF stream (#5708)

This adds functionality to CNF stream to allow e.g. TheoryProxy to be notified when a formula is asserted (not just literals).

This will be required for SAT relevancy.

No behavior changes in this PR.

9 files changed, 61 insertions, 13 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index e5b778365..6a4990c2b 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -46,14 +46,15 @@ CnfStream::CnfStream(SatSolver* satSolver,
                      context::Context* context,
                      OutputManager* outMgr,
                      ResourceManager* rm,
-                     bool fullLitToNodeMap,
+                     FormulaLitPolicy flpol,
                      std::string name)
     : d_satSolver(satSolver),
       d_outMgr(outMgr),
       d_booleanVariables(context),
+      d_notifyFormulas(context),
       d_nodeToLiteralMap(context),
       d_literalToNodeMap(context),
-      d_fullLitToNodeMap(fullLitToNodeMap),
+      d_flitPolicy(flpol),
       d_registrar(registrar),
       d_name(name),
       d_cnfProof(nullptr),
@@ -203,6 +204,13 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister
                << push;
   Assert(node.getKind() != kind::NOT);
 
+  // if we are tracking formulas, everything is a theory atom
+  if (!isTheoryAtom && d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY)
+  {
+    isTheoryAtom = true;
+    d_notifyFormulas.insert(node);
+  }
+
   // Get the literal for this node
   SatLiteral lit;
   if (!hasLiteral(node)) {
@@ -226,7 +234,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister
   }
 
   // If it's a theory literal, need to store it for back queries
-  if ( isTheoryAtom || d_fullLitToNodeMap || (Dump.isOn("clauses")) ) {
+  if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK
+      || (Dump.isOn("clauses")))
+  {
     d_literalToNodeMap.insert_safe(lit, node);
     d_literalToNodeMap.insert_safe(~lit, node.notNode());
   }
@@ -268,6 +278,11 @@ void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
   }
 }
 
+bool CnfStream::isNotifyFormula(TNode node) const
+{
+  return d_notifyFormulas.find(node) != d_notifyFormulas.end();
+}
+
 void CnfStream::setProof(CnfProof* proof) {
   Assert(d_cnfProof == NULL);
   d_cnfProof = proof;
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index e92532f08..90ed1b9cd 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -25,6 +25,7 @@
 #ifndef CVC4__PROP__CNF_STREAM_H
 #define CVC4__PROP__CNF_STREAM_H
 
+#include "context/cdhashset.h"
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
@@ -41,6 +42,17 @@ namespace prop {
 
 class ProofCnfStream;
 
+/** A policy for how literals for formulas are handled in cnf_stream */
+enum class FormulaLitPolicy : uint32_t
+{
+  // literals for formulas are notified
+  TRACK_AND_NOTIFY,
+  // literals for formulas are added to node map
+  TRACK,
+  // literals for formulas are kept internal (default)
+  INTERNAL,
+};
+
 /**
  * Implements the following recursive algorithm
  * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
@@ -74,7 +86,8 @@ class CnfStream {
    * @param outMgr Reference to the output manager of the smt engine. Assertions
    * will not be dumped if outMgr == nullptr.
    * @param rm the resource manager of the CNF stream
-   * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping.
+   * @param flpol policy for literals corresponding to formulas (those that are
+   * not-theory literals).
    * @param name string identifier to distinguish between different instances
    * even for non-theory literals.
    */
@@ -83,7 +96,7 @@ class CnfStream {
             context::Context* context,
             OutputManager* outMgr,
             ResourceManager* rm,
-            bool fullLitToNodeMap = false,
+            FormulaLitPolicy flpol = FormulaLitPolicy::INTERNAL,
             std::string name = "");
   /**
    * Convert a given formula to CNF and assert it to the SAT solver.
@@ -133,6 +146,16 @@ class CnfStream {
    */
   void getBooleanVariables(std::vector<TNode>& outputVariables) const;
 
+  /**
+   * For SAT/theory relevancy. Returns true if node is a "notify formula".
+   * Returns true if node is formula that we are being notified about that
+   * is not a theory atom.
+   *
+   * Note this is only ever true when the policy passed to this class is
+   * FormulaLitPolicy::TRACK_AND_NOTIFY.
+   */
+  bool isNotifyFormula(TNode node) const;
+
   /** Retrieves map from nodes to literals. */
   const CnfStream::NodeToLiteralMap& getTranslationCache() const;
 
@@ -189,6 +212,9 @@ class CnfStream {
   /** Boolean variables that we translated */
   context::CDList<TNode> d_booleanVariables;
 
+  /** Formulas that we translated that we are notifying */
+  context::CDHashSet<Node, NodeHashFunction> d_notifyFormulas;
+
   /** Map from nodes to literals */
   NodeToLiteralMap d_nodeToLiteralMap;
 
@@ -200,7 +226,7 @@ class CnfStream {
    * theory lits.  This is true if e.g. replay logging is on, which
    * dumps the Nodes corresponding to decision literals.
    */
-  const bool d_fullLitToNodeMap;
+  const FormulaLitPolicy d_flitPolicy;
 
   /** The "registrar" for pre-registration of terms */
   Registrar* d_registrar;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index ca29e604f..12246be41 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -274,7 +274,8 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo
     polarity .push(sign);
     decision .push();
     trail    .capacity(v+1);
-    theory   .push(isTheoryAtom);
+    // push whether it corresponds to a theory atom
+    theory.push(isTheoryAtom);
 
     setDecisionVar(v, dvar);
 
@@ -306,7 +307,6 @@ void Solver::resizeVars(int newSize) {
     polarity.shrink(shrinkSize);
     decision.shrink(shrinkSize);
     theory.shrink(shrinkSize);
-
   }
 
   if (Debug.isOn("minisat::pop")) {
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 00d68cf80..8fa489f65 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -390,7 +390,12 @@ protected:
     ClauseAllocator     ca;
 
     // CVC4 Stuff
-    vec<bool>           theory;           // Is the variable representing a theory atom
+    /**
+     * A vector determining whether each variable represents a theory atom.
+     * More generally, this value is true for any literal that the theory proxy
+     * should be notified about when asserted.
+     */
+    vec<bool> theory;
 
     enum TheoryCheckType {
       // Quick check, but don't perform theory reasoning
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 8352373c5..eeb879a2b 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -94,7 +94,7 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::CnfStream(
-      d_satSolver, d_registrar, userContext, &d_outMgr, rm, true);
+      d_satSolver, d_registrar, userContext, &d_outMgr, rm, FormulaLitPolicy::TRACK);
 
   d_theoryProxy = new TheoryProxy(this,
                                   d_theoryEngine,
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 046ad4b1b..44db8a3cd 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -18,6 +18,7 @@
 
 #include "cvc4_private.h"
 #include "options/bv_options.h"
+#include "options/smt_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_engine.h"
@@ -74,7 +75,7 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
                                         d_nullContext.get(),
                                         nullptr,
                                         rm,
-                                        false,
+                                        prop::FormulaLitPolicy::INTERNAL,
                                         "EagerBitblaster"));
 }
 
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 95d78c69b..7f38c61a2 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -85,7 +85,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
                                         d_nullContext.get(),
                                         nullptr,
                                         rm,
-                                        false,
+                                        prop::FormulaLitPolicy::INTERNAL,
                                         "LazyBitblaster"));
 
   d_satSolverNotify.reset(
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 44dc9555f..dbdb350b7 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -17,6 +17,7 @@
 #include "theory/bv/bv_eager_solver.h"
 
 #include "options/bv_options.h"
+#include "options/smt_options.h"
 #include "theory/bv/bitblast/aig_bitblaster.h"
 #include "theory/bv/bitblast/eager_bitblaster.h"
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 6f22d4520..227df458a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -16,6 +16,7 @@
 #include "theory/bv/theory_bv.h"
 
 #include "options/bv_options.h"
+#include "options/smt_options.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/bv_solver_simple.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -129,7 +130,6 @@ TrustNode TheoryBV::expandDefinition(Node node)
     case kind::BITVECTOR_UREM:
     {
       NodeManager* nm = NodeManager::currentNM();
-      unsigned width = node.getType().getBitVectorSize();
 
       Kind kind = node.getKind() == kind::BITVECTOR_UDIV
                       ? kind::BITVECTOR_UDIV_TOTAL