Move ownership of DecisionEngine into PropEngine. (#3850)

This is in preparation of fixing the issue we currently have with reset-assertions.

This also removes a competition hack for QF_LRA.

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index dc798626ee18eda1ed389269a1b32d5761679dcd..7d31d930fa16fe53ccdabe6b42dac55d34aaca01 100644 (file)
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -56,20 +56,21 @@ void DecisionEngine::init()
   {
     ITEDecisionStrategy* ds =
       new decision::JustificationHeuristic(this, d_userContext, d_satContext);
-    enableStrategy(ds);
+    d_enabledStrategies.push_back(ds);
     d_needIteSkolemMap.push_back(ds);
   }
 }
 
-
-void DecisionEngine::enableStrategy(DecisionStrategy* ds)
+void DecisionEngine::shutdown()
 {
-  d_enabledStrategies.push_back(ds);
-}
+  Trace("decision") << "Shutting down decision engine" << std::endl;
 
-void DecisionEngine::clearStrategies(){
-  for(unsigned i = 0; i < d_enabledStrategies.size(); ++i){
-    delete d_enabledStrategies[i];
+  Assert(d_engineState == 1);
+  d_engineState = 2;
+
+  for (DecisionStrategy* s : d_enabledStrategies)
+  {
+    delete s;
   }
   d_enabledStrategies.clear();
   d_needIteSkolemMap.clear();

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 5ebcda8fe2346096dedeb3320be8d43a1b6f9a62..afa3063251a47534bf5606e6c4c0f1b58dba4b41 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -96,22 +96,12 @@ public:
   /* enables decision stragies based on options */
   void init();
 
-  /* clears all of the strategies */
-  void clearStrategies();
-
-
   /**
    * This is called by SmtEngine, at shutdown time, just before
    * destruction.  It is important because there are destruction
    * ordering issues between some parts of the system.
    */
-  void shutdown() {
-    Assert(d_engineState == 1);
-    d_engineState = 2;
-
-    Trace("decision") << "Shutting down decision engine" << std::endl;
-    clearStrategies();
-  }
+  void shutdown();
 
   // Interface for External World to use our services
 
@@ -170,11 +160,6 @@ public:
 
   // External World helping us help the Strategies
 
-  /** If one of the enabled strategies needs them  */
-  /* bool needIteSkolemMap() { */
-  /*   return d_needIteSkolemMap.size() > 0; */
-  /* } */
-
   /**
    * Add a list of assertions from an AssertionPipeline.
    */
@@ -208,14 +193,6 @@ public:
   Node getNode(SatLiteral l) {
     return d_cnfStream->getNode(l);
   }
-
-private:
-  /**
-   * Enable a particular decision strategy, also updating
-   * corresponding vector<DecisionStrategy*>-s is the engine
-   */
-  void enableStrategy(DecisionStrategy* ds);
-
 };/* DecisionEngine class */
 
 }/* CVC4 namespace */

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 70b1f70c24b4aaaba705cd17ce94be543fb327f9..b32a2a86fd139099b03be78c5cc2e5c58e17f685 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -45,7 +45,6 @@ class PreprocessingPassContext
 
   SmtEngine* getSmt() { return d_smt; }
   TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; }
-  DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; }
   prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; }
   context::Context* getUserContext() { return d_smt->d_userContext; }
   context::Context* getDecisionContext() { return d_smt->d_context; }

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 05704c0fa5885d352639b7eef2702acce82873e4..546567b98fe347560ba7d146257be5a9c49bc61f 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -75,14 +75,12 @@ public:
 };
 
 PropEngine::PropEngine(TheoryEngine* te,
-                       DecisionEngine* de,
                        Context* satContext,
-                       Context* userContext,
+                       UserContext* userContext,
                        std::ostream* replayLog,
                        ExprStream* replayStream)
     : d_inCheckSat(false),
       d_theoryEngine(te),
-      d_decisionEngine(de),
       d_context(satContext),
       d_theoryProxy(NULL),
       d_satSolver(NULL),
@@ -94,6 +92,9 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   Debug("prop") << "Constructing the PropEngine" << endl;
 
+  d_decisionEngine.reset(new DecisionEngine(satContext, userContext));
+  d_decisionEngine->init();  // enable appropriate strategies
+
   d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry());
 
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
@@ -102,7 +103,7 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   d_theoryProxy = new TheoryProxy(this,
                                   d_theoryEngine,
-                                  d_decisionEngine,
+                                  d_decisionEngine.get(),
                                   d_context,
                                   d_cnfStream,
                                   replayLog,
@@ -118,6 +119,7 @@ PropEngine::PropEngine(TheoryEngine* te,
 
 PropEngine::~PropEngine() {
   Debug("prop") << "Destructing the PropEngine" << endl;
+  d_decisionEngine->shutdown();
   delete d_cnfStream;
   delete d_registrar;
   delete d_satSolver;
@@ -142,6 +144,12 @@ void PropEngine::assertLemma(TNode node, bool negated,
   d_cnfStream->convertAndAssert(node, removable, negated, rule, from);
 }
 
+void PropEngine::addAssertionsToDecisionEngine(
+    const preprocessing::AssertionPipeline& assertions)
+{
+  d_decisionEngine->addAssertions(assertions);
+}
+
 void PropEngine::requirePhase(TNode n, bool phase) {
   Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << endl;
 

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 061fbbca6ba1dc4fe9217128f7f0845bba282481..707244ff5f77cbe7fa98d2fe7f163a6d77f26af0 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -27,6 +27,7 @@
 #include "expr/expr_stream.h"
 #include "expr/node.h"
 #include "options/options.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "proof/proof_manager.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
@@ -60,9 +61,8 @@ class PropEngine
    * Create a PropEngine with a particular decision and theory engine.
    */
   PropEngine(TheoryEngine*,
-             DecisionEngine*,
              context::Context* satContext,
-             context::Context* userContext,
+             context::UserContext* userContext,
              std::ostream* replayLog,
              ExprStream* replayStream);
 
@@ -104,6 +104,12 @@ class PropEngine
                    ProofRule rule,
                    TNode from = TNode::null());
 
+  /**
+   * Pass a list of assertions from an AssertionPipeline to the decision engine.
+   */
+  void addAssertionsToDecisionEngine(
+      const preprocessing::AssertionPipeline& assertions);
+
   /**
    * If ever n is decided upon, it must be in the given phase.  This
    * occurs *globally*, i.e., even if the literal is untranslated by
@@ -223,7 +229,7 @@ class PropEngine
   TheoryEngine* d_theoryEngine;
 
   /** The decision engine we will be using */
-  DecisionEngine* d_decisionEngine;
+  std::unique_ptr<DecisionEngine> d_decisionEngine;
 
   /** The context */
   context::Context* d_context;

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3e9b81263bbff98b45d09def3df4203a04f4b1e9..89f3acd56dee93ea6df253b1c045413a807572e2 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -850,7 +850,6 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_userLevels(),
       d_exprManager(em),
       d_nodeManager(d_exprManager->getNodeManager()),
-      d_decisionEngine(NULL),
       d_theoryEngine(NULL),
       d_propEngine(NULL),
       d_proofManager(NULL),
@@ -935,12 +934,8 @@ void SmtEngine::finishInit()
 
   Trace("smt-debug") << "Making decision engine..." << std::endl;
 
-  d_decisionEngine = new DecisionEngine(d_context, d_userContext);
-  d_decisionEngine->init();   // enable appropriate strategies
-
   Trace("smt-debug") << "Making prop engine..." << std::endl;
   d_propEngine = new PropEngine(d_theoryEngine,
-                                d_decisionEngine,
                                 d_context,
                                 d_userContext,
                                 d_private->getReplayLog(),
@@ -948,7 +943,6 @@ void SmtEngine::finishInit()
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(d_propEngine);
-  d_theoryEngine->setDecisionEngine(d_decisionEngine);
   Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
   d_theoryEngine->finishInit();
 
@@ -1033,9 +1027,6 @@ void SmtEngine::shutdown() {
   if(d_theoryEngine != NULL) {
     d_theoryEngine->shutdown();
   }
-  if(d_decisionEngine != NULL) {
-    d_decisionEngine->shutdown();
-  }
 }
 
 SmtEngine::~SmtEngine()
@@ -1092,8 +1083,6 @@ SmtEngine::~SmtEngine()
     d_theoryEngine = NULL;
     delete d_propEngine;
     d_propEngine = NULL;
-    delete d_decisionEngine;
-    d_decisionEngine = NULL;
 
     delete d_stats;
     d_stats = NULL;
@@ -3100,22 +3089,6 @@ Result SmtEngine::check() {
   d_private->processAssertions();
   Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
 
-  // Turn off stop only for QF_LRA
-  // TODO: Bring up in a meeting where to put this
-  if(options::decisionStopOnly() && !options::decisionMode.wasSetByUser() ){
-    if( // QF_LRA
-       (not d_logic.isQuantified() &&
-        d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
-        )){
-      if (d_private->getIteSkolemMap().empty())
-      {
-        options::decisionStopOnly.set(false);
-        d_decisionEngine->clearStrategies();
-        Trace("smt") << "SmtEngine::check(): turning off stop only" << endl;
-      }
-    }
-  }
-
   TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
 
   Chat() << "solving..." << endl;
@@ -3616,10 +3589,11 @@ void SmtEnginePrivate::processAssertions() {
   d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() );
 
   // Push the formula to decision engine
-  if(noConflict) {
+  if (noConflict)
+  {
     Chat() << "pushing to decision engine..." << endl;
     Assert(iteRewriteAssertionsEnd == d_assertions.size());
-    d_smt.d_decisionEngine->addAssertions(d_assertions);
+    d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions);
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0ef22f35386a66519a9b86808921d7eec6fa0d8c..1424352ef64cd9782d38cd1dac0bbcc2a01c41e2 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1059,9 +1059,7 @@ class CVC4_PUBLIC SmtEngine
   ExprManager* d_exprManager;
   /** Our internal expression/node manager */
   NodeManager* d_nodeManager;
-  /** The decision engine */
 
-  DecisionEngine* d_decisionEngine;
   /** The theory engine */
   TheoryEngine* d_theoryEngine;
   /** The propositional engine */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a39c014a6260e2df89bd0091e8d8561a9d082edc..60ad00fc5b0f8653219a85db3a342e50f1b5010b 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -315,7 +315,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
                            RemoveTermFormulas& iteRemover,
                            const LogicInfo& logicInfo)
     : d_propEngine(nullptr),
-      d_decisionEngine(nullptr),
       d_context(context),
       d_userContext(userContext),
       d_logicInfo(logicInfo),
@@ -1924,8 +1923,9 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // assert to decision engine
-  if(!removable) {
-    d_decisionEngine->addAssertions(additionalLemmas);
+  if (!removable)
+  {
+    d_propEngine->addAssertionsToDecisionEngine(additionalLemmas);
   }
 
   // Mark that we added some lemmas

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 1757d7a6d99124c96af54a870804dc037fc643b0..e8223f1a13352316f55b09006d697289b33df781 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -101,7 +101,6 @@ namespace theory {
   class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
 
-class DecisionEngine;
 class RemoveTermFormulas;
 
 /**
@@ -119,9 +118,6 @@ class TheoryEngine {
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;
 
-  /** Access to decision engine */
-  DecisionEngine* d_decisionEngine;
-
   /** Our context */
   context::Context* d_context;
 
@@ -505,11 +501,6 @@ class TheoryEngine {
     d_propEngine = propEngine;
   }
 
-  inline void setDecisionEngine(DecisionEngine* decisionEngine) {
-    Assert(d_decisionEngine == NULL);
-    d_decisionEngine = decisionEngine;
-  }
-
   /** Called when all initialization of options/logic is done */
   void finishInit();