Move flag needsFinish from SMT engine to circuit propagator.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 02e9892e2247637b5d01d5fbb2829c5a846bd159..3bfde1839733b5ed41603f0d236938a79df0154d 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -498,7 +498,6 @@ class SmtEnginePrivate : public NodeManagerListener {
 
   /** A circuit propagator for non-clausal propositional deduction */
   booleans::CircuitPropagator d_propagator;
-  bool d_propagatorNeedsFinish;
   std::vector<Node> d_boolVars;
 
   /** Assertions in the preprocessing pipeline */
@@ -612,7 +611,6 @@ class SmtEnginePrivate : public NodeManagerListener {
         d_listenerRegistrations(new ListenerRegistrationList()),
         d_nonClausalLearnedLiterals(),
         d_propagator(d_nonClausalLearnedLiterals, true, true),
-        d_propagatorNeedsFinish(false),
         d_assertions(d_smt.d_userContext),
         d_assertionsProcessed(smt.d_userContext, false),
         d_fakeContext(),
@@ -682,9 +680,9 @@ class SmtEnginePrivate : public NodeManagerListener {
   {
     delete d_listenerRegistrations;
 
-    if(d_propagatorNeedsFinish) {
+    if(d_propagator.getNeedsFinish()) {
       d_propagator.finish();
-      d_propagatorNeedsFinish = false;
+      d_propagator.setNeedsFinish(false);
     }
     d_smt.d_nodeManager->unsubscribeEvents(this);
   }
@@ -2931,9 +2929,10 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     Trace("simplify") << "Assertion #" << i << " : " << d_assertions[i] << std::endl;
   }
 
-  if(d_propagatorNeedsFinish) {
+  if (d_propagator.getNeedsFinish())
+  {
     d_propagator.finish();
-    d_propagatorNeedsFinish = false;
+    d_propagator.setNeedsFinish(false);
   }
   d_propagator.initialize();
 
@@ -2963,7 +2962,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
     d_assertions.clear();
     addFormula(falseNode, false, false);
-    d_propagatorNeedsFinish = true;
+    d_propagator.setNeedsFinish(true);
     return false;
   }
 
@@ -3008,7 +3007,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
         Assert(!options::unsatCores());
         d_assertions.clear();
         addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
-        d_propagatorNeedsFinish = true;
+        d_propagator.setNeedsFinish(true);
         return false;
       }
     }
@@ -3046,7 +3045,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
         Assert(!options::unsatCores());
         d_assertions.clear();
         addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
-        d_propagatorNeedsFinish = true;
+        d_propagator.setNeedsFinish(true);
         return false;
       default:
         if (d_doConstantProp && learnedLiteral.getKind() == kind::EQUAL && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst())) {
@@ -3248,7 +3247,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
                          Rewriter::rewrite(Node(learnedBuilder)));
   }
 
-  d_propagatorNeedsFinish = true;
+  d_propagator.setNeedsFinish(true);
   return true;
 }
 

diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 94ea95793f3867cfe6451e1f69cb646241d34fab..bd6da874273a3a97531ed30adc5693093f7e9ee1 100644 (file)
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -237,30 +237,40 @@ private:
   /** Whether to perform backward propagation */
   const bool d_backwardPropagation;
 
+  /* Does the current state require a call to finish()? */
+  bool d_needsFinish;
+
 public:
   /**
    * Construct a new CircuitPropagator.
    */
-  CircuitPropagator(std::vector<Node>& outLearnedLiterals,
-                    bool enableForward = true, bool enableBackward = true) :
-    d_context(),
-    d_propagationQueue(),
-    d_propagationQueueClearer(&d_context, d_propagationQueue),
-    d_conflict(&d_context, false),
-    d_learnedLiterals(outLearnedLiterals),
-    d_learnedLiteralClearer(&d_context, outLearnedLiterals),
-    d_backEdges(),
-    d_backEdgesClearer(&d_context, d_backEdges),
-    d_seen(&d_context),
-    d_state(&d_context),
-    d_forwardPropagation(enableForward),
-    d_backwardPropagation(enableBackward) {
-  }
+ CircuitPropagator(std::vector<Node>& outLearnedLiterals,
+                   bool enableForward = true,
+                   bool enableBackward = true)
+     : d_context(),
+       d_propagationQueue(),
+       d_propagationQueueClearer(&d_context, d_propagationQueue),
+       d_conflict(&d_context, false),
+       d_learnedLiterals(outLearnedLiterals),
+       d_learnedLiteralClearer(&d_context, outLearnedLiterals),
+       d_backEdges(),
+       d_backEdgesClearer(&d_context, d_backEdges),
+       d_seen(&d_context),
+       d_state(&d_context),
+       d_forwardPropagation(enableForward),
+       d_backwardPropagation(enableBackward),
+       d_needsFinish(false)
+ {
+ }
 
   // Use custom context to ensure propagator is reset after use
   void initialize()
   { d_context.push(); }
 
+  void setNeedsFinish(bool value) { d_needsFinish = value; }
+
+  bool getNeedsFinish() { return d_needsFinish; }
+
   void finish()
   { d_context.pop(); }