Merge branch 'master' into splitEqRew

1 files changed, 12 insertions, 26 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index dceeeae7a..5d185ad9d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -260,24 +260,6 @@ void TheoryEngine::eqNotifyNewClass(TNode t){
   }
 }
 
-void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
-  if (d_logicInfo.isQuantified()) {
-    d_quantEngine->eqNotifyPreMerge( t1, t2 );
-  }
-}
-
-void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
-  if (d_logicInfo.isQuantified()) {
-    d_quantEngine->eqNotifyPostMerge( t1, t2 );
-  }
-}
-
-void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
-  if (d_logicInfo.isQuantified()) {
-    d_quantEngine->eqNotifyDisequal( t1, t2, reason );
-  }
-}
-
 TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
                            RemoveTermFormulas& iteRemover,
@@ -292,7 +274,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_masterEqualityEngine(nullptr),
       d_masterEENotify(*this),
       d_quantEngine(nullptr),
-      d_decManager(new DecisionManager(context)),
+      d_decManager(new DecisionManager(userContext)),
       d_curr_model(nullptr),
       d_aloc_curr_model(false),
       d_curr_model_builder(nullptr),
@@ -900,7 +882,12 @@ TheoryModel* TheoryEngine::getBuiltModel()
   {
     // If this method was called, we should be in SAT mode, and produceModels
     // should be true.
-    AlwaysAssert(d_inSatMode && options::produceModels());
+    AlwaysAssert(options::produceModels());
+    if (!d_inSatMode)
+    {
+      // not available, perhaps due to interuption.
+      return nullptr;
+    }
     // must build model at this point
     d_curr_model_builder->buildModel(d_curr_model);
   }
@@ -923,6 +910,10 @@ bool TheoryEngine::presolve() {
   // Reset the interrupt flag
   d_interrupted = false;
 
+  // Reset the decision manager. This clears its decision strategies that are
+  // no longer valid in this user context.
+  d_decManager->presolve();
+
   try {
     // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -946,9 +937,6 @@ bool TheoryEngine::presolve() {
 }/* TheoryEngine::presolve() */
 
 void TheoryEngine::postsolve() {
-  // Reset the decision manager. This clears its decision strategies, which are
-  // user-context-dependent.
-  d_decManager->reset();
   // no longer in SAT mode
   d_inSatMode = false;
   // Reset the interrupt flag
@@ -1061,9 +1049,7 @@ Node TheoryEngine::ppTheoryRewrite(TNode term) {
 
   Node newTerm;
   // do not rewrite inside quantifiers
-  if (term.getKind() == kind::FORALL || term.getKind() == kind::EXISTS
-      || term.getKind() == kind::CHOICE
-      || term.getKind() == kind::LAMBDA)
+  if (term.isClosure())
   {
     newTerm = Rewriter::rewrite(term);
   }