From f207bf49a4f20bd58c2764a69357f425d9f0e363 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 6 Jan 2022 14:05:04 -0600 Subject: [PATCH] Minor cleaning of non-clausal simplification (#7886) --- src/preprocessing/passes/non_clausal_simp.cpp | 33 ++++++++----------- src/smt/preprocessor.cpp | 10 ++---- src/theory/booleans/circuit_propagator.cpp | 10 ++++-- src/theory/booleans/circuit_propagator.h | 9 +---- 4 files changed, 23 insertions(+), 39 deletions(-) diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index ff672b368..89e40a0aa 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -68,20 +68,18 @@ PreprocessingPassResult NonClausalSimp::applyInternal( { d_preprocContext->spendResource(Resource::PreprocessStep); - theory::booleans::CircuitPropagator* propagator = - d_preprocContext->getCircuitPropagator(); - - for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + if (Trace.isOn("non-clausal-simplify")) { - Trace("non-clausal-simplify") << "Assertion #" << i << " : " - << (*assertionsToPreprocess)[i] << std::endl; + for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + Trace("non-clausal-simplify") + << "Assertion #" << i << " : " << (*assertionsToPreprocess)[i] + << std::endl; + } } - if (propagator->getNeedsFinish()) - { - propagator->finish(); - propagator->setNeedsFinish(false); - } + theory::booleans::CircuitPropagator* propagator = + d_preprocContext->getCircuitPropagator(); propagator->initialize(); // Assert all the assertions to the propagator @@ -111,7 +109,6 @@ PreprocessingPassResult NonClausalSimp::applyInternal( << "conflict in non-clausal propagation" << std::endl; assertionsToPreprocess->clear(); assertionsToPreprocess->pushBackTrusted(conf); - propagator->setNeedsFinish(true); return PreprocessingPassResult::CONFLICT; } @@ -174,7 +171,6 @@ PreprocessingPassResult NonClausalSimp::applyInternal( assertionsToPreprocess->clear(); Node n = NodeManager::currentNM()->mkConst(false); assertionsToPreprocess->push_back(n, false, false, d_llpg.get()); - propagator->setNeedsFinish(true); return PreprocessingPassResult::CONFLICT; } } @@ -208,7 +204,6 @@ PreprocessingPassResult NonClausalSimp::applyInternal( assertionsToPreprocess->clear(); Node n = NodeManager::currentNM()->mkConst(false); assertionsToPreprocess->push_back(n); - propagator->setNeedsFinish(true); return PreprocessingPassResult::CONFLICT; } default: @@ -247,11 +242,11 @@ PreprocessingPassResult NonClausalSimp::applyInternal( { // Keep the literal learned_literals[j++] = learned_literals[i]; - // Its a literal that could not be processed as a substitution or - // conflict. In this case, we notify the context of the learned - // literal, which will process it with the learned literal manager. - d_preprocContext->notifyLearnedLiteral(learnedLiteral); } + // Its a literal that could not be processed as a substitution or + // conflict. In this case, we notify the context of the learned + // literal, which will process it with the learned literal manager. + d_preprocContext->notifyLearnedLiteral(learnedLiteral); break; } } @@ -431,8 +426,6 @@ PreprocessingPassResult NonClausalSimp::applyInternal( assertionsToPreprocess->conjoin(replIndex, newConj, pg); } - propagator->setNeedsFinish(true); - // Note that typically ttls.apply(assert)==assert here. // However, this invariant is invalidated for cases where we use explicit // equality assertions for variables solved in incremental mode that already diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index d7167c04c..985e811ab 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -44,17 +44,11 @@ Preprocessor::Preprocessor(Env& env, d_exDefs(env), d_processor(env, stats) { -} -Preprocessor::~Preprocessor() -{ - if (d_propagator.getNeedsFinish()) - { - d_propagator.finish(); - d_propagator.setNeedsFinish(false); - } } +Preprocessor::~Preprocessor() {} + void Preprocessor::finishInit(TheoryEngine* te, prop::PropEngine* pe) { d_ppContext.reset(new preprocessing::PreprocessingPassContext( diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index b570b6b36..e12f5b521 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -56,10 +56,14 @@ CircuitPropagator::CircuitPropagator(Env& env, bool enableForward, bool enableBa { } -void CircuitPropagator::finish() +void CircuitPropagator::initialize() { - Trace("circuit-prop") << "FINISH" << std::endl; - d_context.pop(); + if (d_needsFinish) + { + d_context.pop(); + } + d_context.push(); + d_needsFinish = true; } void CircuitPropagator::assertTrue(TNode assertion) diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 01bc0ad35..bf299c0e1 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -78,17 +78,10 @@ class CircuitPropagator : protected EnvObj } // 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 initialize(); std::vector& getLearnedLiterals() { return d_learnedLiterals; } - /** Finish the computation and pop the internal context */ - void finish(); - /** Assert for propagation */ void assertTrue(TNode assertion); -- 2.30.2