From 1302e3fb1ffdbed229112106932488e3fff6810c Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 14 Jun 2012 23:49:22 +0000
Subject: [PATCH] WIP

---
 src/decision/justification_heuristic.h |  2 +-
 src/smt/smt_engine.cpp                 | 27 +++++++++++++++++++-------
 2 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index b3cac0d8c..6c470e6df 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -153,9 +153,9 @@ public:
     // Save mapping between ite skolems and ite assertions
     for(IteSkolemMap::iterator i = iteSkolemMap.begin();
         i != iteSkolemMap.end(); ++i) {
-      Assert(i->second >= assertionsEnd && i->second < assertions.size());
       Debug("jh-ite") << " jh-ite: " << (i->first) << " maps to "
                       << assertions[(i->second)] << std::endl;
+      Assert(i->second >= assertionsEnd && i->second < assertions.size());
       d_iteAssertions[i->first] = assertions[i->second];
     }
   }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e3f549898..3f842bc73 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1237,6 +1237,7 @@ void SmtEnginePrivate::simplifyAssertions()
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
     }
 
+    Debug("smt") << "POST nonClasualSimplify" << std::endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -1250,16 +1251,28 @@ void SmtEnginePrivate::simplifyAssertions()
       }
     }
 
+    Debug("smt") << "POST theoryPP" << std::endl;
+    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
     // ITE simplification
     if(Options::current()->doITESimp) {
       simpITE();
     }
 
+    Debug("smt") << "POST iteSimp" << std::endl;
+    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
     // Unconstrained simplification
     if(Options::current()->unconstrainedSimp) {
       unconstrainedSimp();
     }
 
+    Debug("smt") << "POST unconstraintedSimp" << std::endl;
+    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
     if(Options::current()->repeatSimp && Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) {
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
                         << " doing repeated simplification" << std::endl;
@@ -1270,6 +1283,10 @@ void SmtEnginePrivate::simplifyAssertions()
       d_smt.d_userContext->pop();
     }
 
+    Debug("smt") << "POST repeatSimp" << std::endl;
+    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
   } catch(TypeCheckingExceptionPrivate& tcep) {
     // Calls to this function should have already weeded out any
     // typechecking exceptions via (e.g.) ensureBoolean().  But a
@@ -1343,6 +1360,9 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
+  // any assertions added beyond realAssertionsEnd must NOT affect the equisatisfiability
+  int realAssertionsEnd = d_assertionsToPreprocess.size();
+
   // Any variables of subtype types need to be constrained properly.
   // Careful, here: constrainSubtypes() adds to the back of
   // d_assertionsToPreprocess, but we don't need to reprocess those.
@@ -1374,10 +1394,6 @@ void SmtEnginePrivate::processAssertions() {
     staticLearning();
   }
 
-  // any assertions beyond realAssertionsEnd _must_ be introduced by
-  // removeITEs().
-  int realAssertionsEnd = d_assertionsToCheck.size();
-
   {
     TimerStat::CodeTimer codeTimer(d_smt.d_iteRemovalTime);
     // Remove ITEs, updating d_iteSkolemMap
@@ -1387,11 +1403,8 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if(Options::current()->repeatSimp) {
-    unsigned preReSimp = d_assertionsToCheck.size();
     d_assertionsToCheck.swap(d_assertionsToPreprocess);
     simplifyAssertions();
-    Assert(preReSimp == d_assertionsToCheck.size(),
-           "Can't add assertions here");
     removeITEs();
   }
 
-- 
2.30.2