Move flag needsFinish from SMT engine to circuit propagator.

1 files changed, 25 insertions, 15 deletions

diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 94ea95793..bd6da8742 100644
--- 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(); }