Fix a preprocessing performance issue.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2ba1ae7a92a995a0ad74f1cbe9ea784c835a334d..ca65ab1dfc2be35dc1d701ff5adf62f78607bd3e 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1753,6 +1753,17 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   // Resize the learnt
   d_nonClausalLearnedLiterals.resize(j);
 
+  //must add substitutions to model
+  TheoryModel* m = d_smt.d_theoryEngine->getModel();
+  if(m != NULL) {
+    for( SubstitutionMap::iterator pos = d_topLevelSubstitutions.begin(); pos != d_topLevelSubstitutions.end(); ++pos) {
+      Node n = (*pos).first;
+      Node v = (*pos).second;
+      Trace("model") << "Add substitution : " << n << " " << v << std::endl;
+      m->addSubstitution( n, v );
+    }
+  }
+
   hash_set<TNode, TNodeHashFunction> s;
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
     Node assertion = d_assertionsToPreprocess[i];

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index efbc42ebf17aa88707179c5722b9a10907602349..f85a5f3cd9d558ddd82e3e2eb165a43f597beafa 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -728,16 +728,6 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
 
   Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut);
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
-  //must add substitutions to model
-  theory::TheoryModel* m = getModel();
-  if( m ){
-    for( SubstitutionMap::iterator pos = substitutionOut.begin(); pos != substitutionOut.end(); ++pos) {
-      Node n = (*pos).first;
-      Node v = (*pos).second;
-      Trace("model") << "Add substitution : " << n << " " << v << std::endl;
-      m->addSubstitution( n, v );
-    }
-  }
   return solveStatus;
 }