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/smt | |
parent | 6a2148c3cfb20928b2e721726345ea96149154d9 (diff) |
Move flag needsFinish from SMT engine to circuit propagator.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 02e9892e2..3bfde1839 100644 --- 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; } |