Moved some things around in the preprocessor. Now theory preprocessing gets

called before ite simplification unless arithrewriteequality is on

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7cac970f8be795d4221fd5736512519f735d64fc..4887ef540a1207a9825d11d2b4765595335c0756 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -248,6 +248,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_problemExtended(false),
   d_queryMade(false),
   d_needPostsolve(false),
+  d_earlyTheoryPP(true),
   d_timeBudgetCumulative(0),
   d_timeBudgetPerCall(0),
   d_resourceBudgetCumulative(0),
@@ -489,6 +490,10 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
     NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq;
   }
+  // Turn off early theory preprocessing if arithRewriteEq is on
+  if (NodeManager::currentNM()->getOptions()->arithRewriteEq) {
+    d_earlyTheoryPP = false;
+  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const SExpr& value)
@@ -1149,19 +1154,6 @@ void SmtEnginePrivate::simplifyAssertions()
 
     Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
 
-    if(!Options::current()->lazyDefinitionExpansion) {
-      Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
-      TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime);
-      hash_map<TNode, Node, TNodeHashFunction> cache;
-      for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-        d_assertionsToPreprocess[i] =
-          expandDefinitions(d_assertionsToPreprocess[i], cache);
-      }
-    }
-    
-    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
-
     if(Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) {
       // Perform non-clausal simplification
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
@@ -1178,11 +1170,22 @@ void SmtEnginePrivate::simplifyAssertions()
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
+    // Theory preprocessing
+    if (d_smt.d_earlyTheoryPP) {
+      TimerStat::CodeTimer codeTimer(d_smt.d_theoryPreprocessTime);
+      // Call the theory preprocessors
+      d_smt.d_theoryEngine->preprocessStart();
+      for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
+        d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
+      }
+    }
+
+    // ITE simplification
     if(Options::current()->doITESimp) {
-      // ite simplification
       simpITE();
     }
 
+    // Unconstrained simplification
     if(Options::current()->unconstrainedSimp) {
       unconstrainedSimp();
     }
@@ -1197,16 +1200,6 @@ void SmtEnginePrivate::simplifyAssertions()
       d_smt.d_userContext->pop();
     }
 
-    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
-
-    if(Options::current()->doStaticLearning) {
-      // Perform static learning
-      Trace("simplify") << "SmtEnginePrivate::simplify(): "
-                        << "performing static learning" << endl;
-      staticLearning();
-    }
-
   } catch(TypeCheckingExceptionPrivate& tcep) {
     // Calls to this function should have already weeded out any
     // typechecking exceptions via (e.g.) ensureBoolean().  But a
@@ -1292,9 +1285,25 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
-  // Simplify the assertions
+  if(!Options::current()->lazyDefinitionExpansion) {
+    Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
+    TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime);
+    hash_map<TNode, Node, TNodeHashFunction> cache;
+    for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+      d_assertionsToPreprocess[i] =
+        expandDefinitions(d_assertionsToPreprocess[i], cache);
+    }
+  }
+    
   simplifyAssertions();
 
+  if(Options::current()->doStaticLearning) {
+    // Perform static learning
+    Trace("simplify") << "SmtEnginePrivate::simplify(): "
+                      << "performing static learning" << endl;
+    staticLearning();
+  }
+
   // any assertions beyond realAssertionsEnd _must_ be introduced by
   // removeITEs().
   int realAssertionsEnd = d_assertionsToCheck.size();
@@ -1313,6 +1322,9 @@ void SmtEnginePrivate::processAssertions() {
     removeITEs();
   }
 
+  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
   // begin: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 #ifdef CVC4_ASSERTIONS
@@ -1323,14 +1335,6 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
-  if(Dump.isOn("assertions")) {
-    // Push the simplified assertions to the dump output stream
-    for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-      Dump("assertions")
-        << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr()));
-    }
-  }
-
   {
     TimerStat::CodeTimer codeTimer(d_smt.d_theoryPreprocessTime);
     // Call the theory preprocessors
@@ -1340,6 +1344,14 @@ void SmtEnginePrivate::processAssertions() {
     }
   }
 
+  if(Dump.isOn("assertions")) {
+    // Push the simplified assertions to the dump output stream
+    for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
+      Dump("assertions")
+        << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr()));
+    }
+  }
+
   // Push the formula to decision engine
   Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
   d_smt.d_decisionEngine->addAssertions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0873aea96a213cd41ccb8850a039beaaeb3d60f2..11f3bdcb927e1d5ba9bfb3d3c4959ce3af714e77 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -163,6 +163,11 @@ class CVC4_PUBLIC SmtEngine {
    */
   bool d_needPostsolve;
 
+  /*
+   * Whether to call theory preprocessing during simplification - on by default* but gets turned off if arithRewriteEq is on
+   */
+  bool d_earlyTheoryPP;
+
   /** A user-imposed cumulative time budget, in milliseconds.  0 = no limit. */
   unsigned long d_timeBudgetCumulative;
   /** A user-imposed per-call time budget, in milliseconds.  0 = no limit. */