Remove experimental code (that wasn't enabled). That doesn't help.

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 2a34fb18253212700bc669423efb99ebcee30933..b151e79ef66138848d269e31884f70bdacabf2d0 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -723,12 +723,12 @@ namespace BEEV
     for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
       {
                 /*
-        Calling simplifyFormula makes the required substitutions. For instance, if
+        Calling applySubstitutionMapUntilArrays makes the required substitutions. For instance, if
         first was : v = x,
         then if the next formula is: x = v
-        calling simplify on the second formula will convert it into "true", avoiding a cycle.
+        calling applySubstitutionMapUntilArrays on the second formula will convert it into "true", avoiding a cycle.
 
-        The problem with this is that Simplify___() doesn't normally simplify into array
+        The problem with this is that applySubstitutionMapUntilArrays() doesn't normally simplify into array
         operations. So given something like :
         a = b
         b = write(A,a,a)
@@ -738,53 +738,14 @@ namespace BEEV
         rewrite a=b through the second expression, giving:
         b = write(A,b,b),
         which shouldn't be simplified.
-
-        Simplifying through arrays is very expensive though. I know how to fix it, but
-        don't have time. Trev.
-                 */
-#if 1
+          */
         ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula(_simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it;
-      #else
-          ASTNode aaa = *it;
-
-          if (any_solved && EQ == aaa.GetKind())
-          {
-            bool found = false;
-
-            ASTNodeSet var;
-            SetofVarsSeenInTerm(aaa[0], var);
-
-            for (ASTNodeSet::const_iterator it = var.begin(); it != var.end(); it++)
-            if (_simp->CheckSubstitutionMap(*it))
-              {
-                found = true;
-                break;
-              }
-
-            if (!found)
-              {
-                var.clear();
-                SetofVarsSeenInTerm(aaa[1], var);
-
-                for (ASTNodeSet::const_iterator it = var.begin(); it != var.end(); it++)
-                if (_simp->CheckSubstitutionMap(*it))
-                  {
-                    found = true;
-                    break;
-                  }
-              }
-            if (found)
-              aaa = _simp->applySubstitutionMapUntilArrays(aaa);
-          }
-
-#endif
 
+        if (ASTFalse == aaa)
+               return ASTFalse; // shortcut. It's unsatisfiable.
 
-        //_bm->ASTNodeStats("Printing after calling simplifyformula
-        //inside the solver:", aaa);
         aaa = BVSolve_Odd(aaa);
 
-        //_bm->ASTNodeStats("Printing after oddsolver:", aaa);
         bool even = false;
         aaa = CheckEvenEqn(aaa, even);
         if (even)
@@ -800,7 +761,7 @@ namespace BEEV
           }
         if (ASTTrue == aaa)
                {
-                    any_solved=true;
+               any_solved=true;
                }
       }