From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 6 Jan 2022 20:05:04 +0000 (-0600)
Subject: Minor cleaning of non-clausal simplification (#7886)
X-Git-Tag: cvc5-1.0.0~593
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f207bf49a4f20bd58c2764a69357f425d9f0e363;p=cvc5.git

Minor cleaning of non-clausal simplification (#7886)
---

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<bool>(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<bool>(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<TrustNode>& getLearnedLiterals() { return d_learnedLiterals; }
 
-  /** Finish the computation and pop the internal context */
-  void finish();
-
   /** Assert for propagation */
   void assertTrue(TNode assertion);