Revert "Move ownership of DecisionEngine into PropEngine. (#3850)"

This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b.

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

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index afa3063251a47534bf5606e6c4c0f1b58dba4b41..5ebcda8fe2346096dedeb3320be8d43a1b6f9a62 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -96,12 +96,22 @@ 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();
+  void shutdown() {
+    Assert(d_engineState == 1);
+    d_engineState = 2;
+
+    Trace("decision") << "Shutting down decision engine" << std::endl;
+    clearStrategies();
+  }
 
   // Interface for External World to use our services
 
@@ -160,6 +170,11 @@ 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.
    */
@@ -193,6 +208,14 @@ 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 b32a2a86fd139099b03be78c5cc2e5c58e17f685..70b1f70c24b4aaaba705cd17ce94be543fb327f9 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -45,6 +45,7 @@ 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 546567b98fe347560ba7d146257be5a9c49bc61f..05704c0fa5885d352639b7eef2702acce82873e4 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -75,12 +75,14 @@ public:
 };
 
 PropEngine::PropEngine(TheoryEngine* te,
+                       DecisionEngine* de,
                        Context* satContext,
-                       UserContext* userContext,
+                       Context* userContext,
                        std::ostream* replayLog,
                        ExprStream* replayStream)
     : d_inCheckSat(false),
       d_theoryEngine(te),
+      d_decisionEngine(de),
       d_context(satContext),
       d_theoryProxy(NULL),
       d_satSolver(NULL),
@@ -92,9 +94,6 @@ 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);
@@ -103,7 +102,7 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   d_theoryProxy = new TheoryProxy(this,
                                   d_theoryEngine,
-                                  d_decisionEngine.get(),
+                                  d_decisionEngine,
                                   d_context,
                                   d_cnfStream,
                                   replayLog,
@@ -119,7 +118,6 @@ PropEngine::PropEngine(TheoryEngine* te,
 
 PropEngine::~PropEngine() {
   Debug("prop") << "Destructing the PropEngine" << endl;
-  d_decisionEngine->shutdown();
   delete d_cnfStream;
   delete d_registrar;
   delete d_satSolver;
@@ -144,12 +142,6 @@ 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 707244ff5f77cbe7fa98d2fe7f163a6d77f26af0..061fbbca6ba1dc4fe9217128f7f0845bba282481 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -27,7 +27,6 @@
 #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"
@@ -61,8 +60,9 @@ class PropEngine
    * Create a PropEngine with a particular decision and theory engine.
    */
   PropEngine(TheoryEngine*,
+             DecisionEngine*,
              context::Context* satContext,
-             context::UserContext* userContext,
+             context::Context* userContext,
              std::ostream* replayLog,
              ExprStream* replayStream);
 
@@ -104,12 +104,6 @@ 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
@@ -229,7 +223,7 @@ class PropEngine
   TheoryEngine* d_theoryEngine;
 
   /** The decision engine we will be using */
-  std::unique_ptr<DecisionEngine> d_decisionEngine;
+  DecisionEngine* d_decisionEngine;
 
   /** The context */
   context::Context* d_context;

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 89f3acd56dee93ea6df253b1c045413a807572e2..3e9b81263bbff98b45d09def3df4203a04f4b1e9 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -850,6 +850,7 @@ 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),
@@ -934,8 +935,12 @@ 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(),
@@ -943,6 +948,7 @@ 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();
 
@@ -1027,6 +1033,9 @@ void SmtEngine::shutdown() {
   if(d_theoryEngine != NULL) {
     d_theoryEngine->shutdown();
   }
+  if(d_decisionEngine != NULL) {
+    d_decisionEngine->shutdown();
+  }
 }
 
 SmtEngine::~SmtEngine()
@@ -1083,6 +1092,8 @@ SmtEngine::~SmtEngine()
     d_theoryEngine = NULL;
     delete d_propEngine;
     d_propEngine = NULL;
+    delete d_decisionEngine;
+    d_decisionEngine = NULL;
 
     delete d_stats;
     d_stats = NULL;
@@ -3089,6 +3100,22 @@ 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;
@@ -3589,11 +3616,10 @@ 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_propEngine->addAssertionsToDecisionEngine(d_assertions);
+    d_smt.d_decisionEngine->addAssertions(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 1424352ef64cd9782d38cd1dac0bbcc2a01c41e2..0ef22f35386a66519a9b86808921d7eec6fa0d8c 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1059,7 +1059,9 @@ 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 60ad00fc5b0f8653219a85db3a342e50f1b5010b..a39c014a6260e2df89bd0091e8d8561a9d082edc 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -315,6 +315,7 @@ 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),
@@ -1923,9 +1924,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // assert to decision engine
-  if (!removable)
-  {
-    d_propEngine->addAssertionsToDecisionEngine(additionalLemmas);
+  if(!removable) {
+    d_decisionEngine->addAssertions(additionalLemmas);
   }
 
   // Mark that we added some lemmas

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e8223f1a13352316f55b09006d697289b33df781..1757d7a6d99124c96af54a870804dc037fc643b0 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -101,6 +101,7 @@ namespace theory {
   class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
 
+class DecisionEngine;
 class RemoveTermFormulas;
 
 /**
@@ -118,6 +119,9 @@ class TheoryEngine {
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;
 
+  /** Access to decision engine */
+  DecisionEngine* d_decisionEngine;
+
   /** Our context */
   context::Context* d_context;
 
@@ -501,6 +505,11 @@ 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();