diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-28 09:53:58 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-28 15:40:22 -0700 |
commit | af950306f906801dbc3411e57bf74c77f2578ba1 (patch) | |
tree | 3e3c1556b68f04435ae3a30fbd4733f81ae6c43f /src/theory/booleans | |
parent | 6a2148c3cfb20928b2e721726345ea96149154d9 (diff) |
Move flag needsFinish from SMT engine to circuit propagator.
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 40 |
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(); } |