Enabling constant propagation

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5874692b548e53a53892e5fc96a95d1130be842a..3d2a971be8336d5a1a58305df0511830da6eb433 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -140,7 +140,7 @@ class SmtEnginePrivate {
    * then nothing has been pushed out yet. */
   context::CDO<theory::SubstitutionMap::iterator> d_lastSubstitutionPos;
 
-  static const bool d_doConstantProp = false;
+  static const bool d_doConstantProp = true;
 
   /**
    * Runs the nonclausal solver and tries to solve all the assigned
@@ -868,7 +868,6 @@ void SmtEnginePrivate::nonClausalSimplify() {
       learnedLiteralNew = constantPropagations.apply(learnedLiteral);
       if (learnedLiteralNew == learnedLiteral) {
         break;
-      }
       ++d_smt.d_numConstantProps;
       learnedLiteral = theory::Rewriter::rewrite(learnedLiteralNew);
     }
@@ -899,13 +898,14 @@ void SmtEnginePrivate::nonClausalSimplify() {
         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                           << "solved " << learnedLiteral << endl;
         Assert(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(learnedLiteral)).isConst());
-        vector<pair<Node, Node> > equations;
-        constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true);
-        if (equations.empty()) {
-          break;
-        }
-        Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
+        //        vector<pair<Node, Node> > equations;
+        //        constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true);
+        //        if (equations.empty()) {
+        //          break;
+        //        }
+        //        Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
         // else fall through
+        break;
       }
       case Theory::PP_ASSERT_STATUS_CONFLICT:
         // If in conflict, we return false
@@ -931,15 +931,16 @@ void SmtEnginePrivate::nonClausalSimplify() {
           Assert(!t.isConst());
           Assert(constantPropagations.apply(t) == t);
           Assert(d_topLevelSubstitutions.apply(t) == t);
-          vector<pair<Node,Node> > equations;
-          constantPropagations.simplifyLHS(t, c, equations, true);
-          if (!equations.empty()) {
-            Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
-            d_assertionsToPreprocess.clear();
-            d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
-            return;
-          }
-          d_topLevelSubstitutions.simplifyRHS(constantPropagations);
+          constantPropagations.addSubstitution(t, c, true, false, false);
+          // vector<pair<Node,Node> > equations;a
+          // constantPropagations.simplifyLHS(t, c, equations, true);
+          // if (!equations.empty()) {
+          //   Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
+          //   d_assertionsToPreprocess.clear();
+          //   d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+          //   return;
+          // }
+          // d_topLevelSubstitutions.simplifyRHS(constantPropagations);
         }
         else {
           // Keep the literal
@@ -967,6 +968,13 @@ void SmtEnginePrivate::nonClausalSimplify() {
         d_lastSubstitutionPos = pos;
         ++pos;
       }
+      newLeft = constantPropagations.apply((*pos).first);
+      if (newLeft != (*pos).first) {
+        newLeft = Rewriter::rewrite(newLeft);
+        Assert(newLeft == (*pos).second ||
+               (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
+      }
+      Assert(constantPropagations.apply((*pos).second) == (*pos).second);
     }
 
 #ifdef CVC4_ASSERTIONS
@@ -984,18 +992,18 @@ void SmtEnginePrivate::nonClausalSimplify() {
     for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
       Assert((*pos).second.isConst());
       Assert(Rewriter::rewrite((*pos).first) == (*pos).first);
-      Node newLeft = d_topLevelSubstitutions.apply((*pos).first);
-      if (newLeft != (*pos).first) {
-        newLeft = Rewriter::rewrite(newLeft);
-        Assert(newLeft == (*pos).second ||
-               (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
-      }
-      newLeft = constantPropagations.apply((*pos).first);
-      if (newLeft != (*pos).first) {
-        newLeft = Rewriter::rewrite(newLeft);
-        Assert(newLeft == (*pos).second ||
-               (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
-      }
+      // Node newLeft = d_topLevelSubstitutions.apply((*pos).first);
+      // if (newLeft != (*pos).first) {
+      //   newLeft = Rewriter::rewrite(newLeft);
+      //   Assert(newLeft == (*pos).second ||
+      //          (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
+      // }
+      // newLeft = constantPropagations.apply((*pos).first);
+      // if (newLeft != (*pos).first) {
+      //   newLeft = Rewriter::rewrite(newLeft);
+      //   Assert(newLeft == (*pos).second ||
+      //          (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
+      // }
       Assert(constantPropagations.apply((*pos).second) == (*pos).second);
     }
 #endif