Hack. The ITE context simplification blows out ff.stp, i.e. it takes > 5 minutes...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1254 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 5c4ca60f532f5ef122cf1b3946b58d44ac060790..0cb882a9cfbaa472e291f6cdf25fd7bc4a6d9483 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -98,7 +98,9 @@ public:
                ASTNode var = (BVEXTRACT == key.GetKind()) ? key[0] : key;
 
                if (var.GetKind() == SYMBOL && loops(var,value))
-                       return false;
+                       {
+                   return false;
+                       }
 
 
                if (!CheckSubstitutionMap(var) && key != value) {

diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h
index 47d38364eadf70701002393037cf18088464f388..9c19b147cb081545bc2357dfbe5dc9ad79433789 100644 (file)
--- a/src/simplifier/UseITEContext.h
+++ b/src/simplifier/UseITEContext.h
@@ -63,9 +63,13 @@ namespace BEEV
       if (n.isAtom())
         return n;
 
+      // Hacks to stop it blowing out..
       {
           if (visited[n]++ > 10)
             return n;
+
+          if (context.size() > 20)
+            return n;
       }
 
       ASTVec new_children;

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index c67f46670263fe44edfc36dfa50eb6130fbe6223..41d4715d9b84f0320bc3d6d31f8b5b65c4b56657 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -37,17 +37,34 @@
 //2. paper for actual solving procedure
 //
 //4. Outside the solver, Substitute and Re-normalize the input DAG
+
+
+// This has a "slow mode", that performs time-consuming substitutions.
+// In slow mode it does applySubstitutions as it goes, it
+// applies the Simplify functions, and it solves for "even" monomials.
+// If we're not in slow mode this might take longer to fixed point. For
+// instance given:
+// 0 = 4x1 + 3x2 + 2x3 + 1x4.
+// 0 = 4x1 + 8x2 + 6x3 + 5x4.
+// 0 = 1x1 + 2x2 + 7x3 + 5x4.
+// The first replacement may be for 3x2, because substitutions aren't being applied
+// then the next two will fail (because any monomial chosen will appear in the rhs).
+// After applying through the substitutions & simplifying. The second formula will
+// change from  0 = 4x1 + 8(-(1/3)(4x1 +  2x3 + 1x4)) + 6x3 + 5x4.
+// to having each variable appear only a single time, so it can be solved for.
+
+
+
 namespace BEEV
 {
        const bool flatten_ands = true;
-       const bool sort_extracts_last = false;
        const bool debug_bvsolver = false;
 
        // The simplify functions can increase the size of the DAG,
        // so we have the option to disable simplifications.
   ASTNode BVSolver::simplifyNode(const ASTNode n)
   {
-         if (!simplify)
+         if (!slow)
                  return n;
 
          if (n.GetType() == BOOLEAN_TYPE)
@@ -91,9 +108,11 @@ namespace BEEV
        assert(number_shifts >0); // shouldn't be odd.
   }
 
+  // This doesn't seem necessary for correctness, it just stops you checking the same values over and over..
   bool BVSolver::DoNotSolveThis(const ASTNode& var)
   {
-    return (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end());
+    return false;
+    //return (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end());
   }
 
   //chooses a variable in the lhs and returns the chosen variable
@@ -148,25 +167,12 @@ namespace BEEV
                // that the variable appears in none of them.
 
                ASTNode var = (SYMBOL == monom.GetKind())? monom: monom[0];
-               bool duplicated = false;
-               for (ASTVec::const_iterator it2 = c.begin(); it2 != itend; it2++)
-                       {
-                               if (it2 == it)
-                                       continue;
-                               if (vars.VarSeenInTerm(var,*it2))
-                               {
-                                       duplicated = true;
-                                       break;
-                               }
-                       }
-                       if (!duplicated)
+
                        {
                                outmonom = monom; //nb. monom not var.
                                chosen_symbol = true;
                                checked.insert(var);
                        }
-                       else
-                               o.push_back(monom);
         }
        else
                o.push_back(monom);
@@ -281,14 +287,6 @@ namespace BEEV
       {
           DoNotSolve_TheseVars.insert(lhs);
 
-        //input is of the form x = rhs first make sure that the lhs
-        //symbol does not occur on the rhs or that it has not been
-        //solved for
-        if (!single && vars.VarSeenInTerm(lhs, rhs))
-          {
-            //found the lhs in the rhs. Abort!
-            return eq;
-          }
 
         if (!_simp->UpdateSolverMap(lhs, rhs))
           {
@@ -614,15 +612,17 @@ namespace BEEV
     for (ASTVec::const_iterator and_child = c.begin(), and_end = c.end(); and_child
         != and_end; and_child++)
       {
+      ASTNode r = *and_child;
+      if (slow && changed) // Simplifier expects substitutions to be applied.
+        r = _simp->applySubstitutionMapUntilArrays(r);
 
-      ASTNode r = solveForXOR(!changed?*and_child:simplifyNode(_simp->applySubstitutionMapUntilArrays(*and_child)));
+      r = solveForXOR(!changed?r:simplifyNode((r)));
       if (r!=*and_child)
         changed=true;
       output_children.push_back(r);
       }
 
     return nf->CreateNode(AND, output_children);
-
   }
 
 
@@ -633,7 +633,7 @@ namespace BEEV
   {
       assert (_bm->UserFlags.wordlevel_solve_flag);
          ASTNode input = _input;
-         simplify = enable_simplify;
+         slow = enable_simplify;
 
     ASTNode output = input;
     if (CheckAlreadySolvedMap(input, output))
@@ -703,8 +703,14 @@ namespace BEEV
         which shouldn't be simplified.
           */
 
-       ASTNode aaa =  (any_solved && EQ == it->GetKind()) ? simplifyNode
-                       (_simp->applySubstitutionMapUntilArrays(*it)) : *it;
+        // simplifyNode expects substitutions to already be applied.
+        ASTNode aaa = *it;
+        if (EQ == it->GetKind() && any_solved)
+          {
+            if (slow)
+              aaa = _simp->applySubstitutionMapUntilArrays(aaa);
+            aaa = (any_solved && EQ == it->GetKind()) ? simplifyNode(aaa) : aaa;
+          }
 
         if (ASTFalse == aaa)
         {
@@ -847,7 +853,7 @@ namespace BEEV
     //         return input;
     //       }
 
-    if (!(EQ == input.GetKind() || AND == input.GetKind()))
+    if (slow || !(EQ == input.GetKind() || AND == input.GetKind()))
       {
         return input;
       }

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 1585bd3dcc7e5fdb4320bfaaef3888fb18a22450..0454b394df00b608009d2d6ee585f39d78f9fef5 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -115,7 +115,7 @@ namespace BEEV
 
     VariablesInExpression& vars;
 
-    bool simplify; //Whether to apply the simplifyTerm & simplifyFormula functions.
+    bool slow; //Whether to apply the simplifyTerm & simplifyFormula functions.
 
     ASTNode simplifyNode(const ASTNode n);
 
@@ -128,7 +128,7 @@ namespace BEEV
       ASTTrue = _bm->CreateNode(TRUE);
       ASTFalse = _bm->CreateNode(FALSE);
       ASTUndefined = _bm->CreateNode(UNDEFINED);
-      simplify=true;
+      slow=true;
       nf = new SimplifyingNodeFactory(*bm->hashingNodeFactory,*bm);
     };
 

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index ecc4c2230d9e355b612bdff20b541c580ddefba5..3b02959b271e5be351f09003362d4d35440a95bf 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -67,6 +67,14 @@ namespace BEEV
       {
         return false;
       }
+
+    if (!pushNeg && key.isSimplfied())
+      {
+        output = key;
+        return true;
+      }
+
+
     ASTNodeMap::iterator it, itend;
     it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key);
     itend = pushNeg ? SimplifyNegMap->end() : SimplifyMap->end();
@@ -106,11 +114,16 @@ namespace BEEV
     // to cache.
     if (0 == key.Degree())
       return;
-    
+
     if (pushNeg)
       (*SimplifyNegMap)[key] = value;
     else
       (*SimplifyMap)[key] = value;
+
+    if (!pushNeg && key == value)
+      {
+        key.hasBeenSimplfied();
+      }
   }
 
   // Substitution Map methods....
@@ -1661,6 +1674,9 @@ namespace BEEV
     if (n.isConstant())
       return true;
 
+    if (n.isSimplfied())
+      return true;
+
     //If it's a symbol that's not in the substitition Map.
     if (n.GetKind() == SYMBOL && CheckSubstitutionMap(n))
       return false;