Improvements.

* The BVSolver doesn't necessarily apply the simplify..() functions (which can increase the DAGs size).
* Unsimplified input doesn't cause it to fail.

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 56e2dabd3a412e75ff0bfeb01b98708eb5238d42..425d93d794795e62b911d74e0f1539496db32630 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -22,7 +22,9 @@
 //best-effort. it relies on the SAT solver to be complete.
 //
 //The BVSolver assumes that the input equations are normalized, and
-//have liketerms combined etc.
+//have liketerms combined etc. It won't fail if the input isn't
+// normalised. It just won't be able to simplify things, for example
+// it cant simplify (3*3)*x = y.
 //
 //0. Traverse top-down over the input DAG, looking for a conjunction
 //0. of equations. if you find one, then for each equation in the
@@ -41,6 +43,20 @@ namespace BEEV
        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)
+                 return n;
+
+         if (n.GetType() == BOOLEAN_TYPE)
+                 return _simp->SimplifyFormula(n,false,NULL);
+         else
+                 return _simp->SimplifyTerm(n);
+  }
+
+
   //check the solver map for 'key'. If key is present, then return the
   //value by reference in the argument 'output'
   bool BVSolver::CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output)
@@ -268,6 +284,7 @@ namespace BEEV
                lhs = eq[1];
                rhs = eq[0];
                eq = _bm->CreateNode(EQ, lhs, rhs); // If "return eq" is called, return the arguments in the correct order.
+               assert(BVTypeCheck(eq));
        }
 
     if (CheckAlreadySolvedMap(eq, output))
@@ -298,10 +315,12 @@ namespace BEEV
         //construct:  rhs - (lhs without the chosen monom)
         unsigned int len = lhs.GetValueWidth();
         leftover_lhs = 
-          _simp->SimplifyTerm(_bm->CreateTerm(BVUMINUS,
+          simplifyNode(_bm->CreateTerm(BVUMINUS,
                                                        len, leftover_lhs));
+        assert(BVTypeCheck(leftover_lhs));
         rhs =
-          _simp->SimplifyTerm(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs));
+                       simplifyNode(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs));
+        assert(BVTypeCheck(rhs));
         lhs = chosen_monom;
         single = true;
       } //end of if(BVPLUS ...)
@@ -310,8 +329,9 @@ namespace BEEV
       {
         //equation is of the form (-lhs0) = rhs
         ASTNode lhs0 = lhs[0];
-        rhs = _simp->SimplifyTerm(_bm->CreateTerm(BVUMINUS,
+        rhs = simplifyNode(_bm->CreateTerm(BVUMINUS,
                                                   rhs.GetValueWidth(), rhs));
+        assert(BVTypeCheck(rhs));
         lhs = lhs0;
       }
 
@@ -437,7 +457,7 @@ namespace BEEV
           ASTNode chosenvar = 
                          ChosenVar_Is_Extract ? lhs[1][0] : lhs[1];
           ASTNode chosenvar_value = 
-            _simp->SimplifyTerm(_bm->CreateTerm(BVMULT, 
+                         simplifyNode(_bm->CreateTerm(BVMULT,
                                                 rhs.GetValueWidth(), 
                                                 a, rhs));
 
@@ -449,11 +469,10 @@ namespace BEEV
               return eq;
             }
 
-          //rhs should not have arrayreads in it. it complicates matters
-          //during transformation
-          // if(CheckForArrayReads_TopLevel(chosenvar_value)) {
-          //            return eq;
-          //       }
+          // It fails if it's a full-bitwidth extract. These are rare, and won't be
+          // present after simplification. So ignore them for now.
+          if (ChosenVar_Is_Extract && lhs[0].GetValueWidth() == lhs.GetValueWidth())
+                 return eq;
 
           //found a variable to solve
           DoNotSolve_TheseVars.insert(chosenvar);
@@ -463,17 +482,20 @@ namespace BEEV
               return eq;
             }
 
+          cout << lhs;
           if (ChosenVar_Is_Extract)
             {
               const ASTNode& var = lhs[1][0];
 
-              ASTNode newvar = 
-                  _bm->CreateFreshVariable(0, var.GetValueWidth() - lhs[1].GetValueWidth(), "v_solver");
-              newvar = 
-                _bm->CreateTerm(BVCONCAT, 
-                                var.GetValueWidth(), 
-                                newvar, chosenvar_value);
-              _simp->UpdateSolverMap(var, newvar);
+                                 ASTNode newvar =
+                                         _bm->CreateFreshVariable(0, var.GetValueWidth() - lhs[1].GetValueWidth(), "v_solver");
+                                 newvar =
+                                       _bm->CreateTerm(BVCONCAT,
+                                                                       var.GetValueWidth(),
+                                                                       newvar, chosenvar_value);
+                                 assert(BVTypeCheck(newvar));
+                                 _simp->UpdateSolverMap(var, newvar);
+
             }
           output = ASTTrue;
           break;
@@ -643,7 +665,7 @@ namespace BEEV
         != and_end; and_child++)
       {
 
-      ASTNode r = solveForXOR(!changed?*and_child:_simp->SimplifyFormula(_simp->applySubstitutionMapUntilArrays(*and_child),false,NULL));
+      ASTNode r = solveForXOR(!changed?*and_child:simplifyNode(_simp->applySubstitutionMapUntilArrays(*and_child)));
       if (r!=*and_child)
         changed=true;
       output_children.push_back(r);
@@ -657,10 +679,11 @@ namespace BEEV
   //The toplevel bvsolver(). Checks if the formula has already been
   //solved. If not, the solver() is invoked. If yes, then simply drop
   //the formula
-  ASTNode BVSolver::TopLevelBVSolve(const ASTNode& _input)
+  ASTNode BVSolver::TopLevelBVSolve(const ASTNode& _input, const bool enable_simplify)
   {
       assert (_bm->UserFlags.wordlevel_solve_flag);
          ASTNode input = _input;
+         simplify = enable_simplify;
 
     ASTNode output = input;
     if (CheckAlreadySolvedMap(input, output))
@@ -733,8 +756,8 @@ namespace BEEV
         which shouldn't be simplified.
           */
 
-       ASTNode aaa =  (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula
-                       (_simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it;
+       ASTNode aaa =  (any_solved && EQ == it->GetKind()) ? simplifyNode
+                       (_simp->applySubstitutionMapUntilArrays(*it)) : *it;
 
         if (ASTFalse == aaa)
         {
@@ -1029,7 +1052,7 @@ namespace BEEV
                                                           low_minus_one, 
                                                           low_zero));
                 ASTNode lower_x =
-                  _simp->SimplifyTerm(_bm->CreateTerm(BVEXTRACT, 
+                               simplifyNode(_bm->CreateTerm(BVEXTRACT,
                                                       newlen, 
                                                       aaa[1], 
                                                       low_minus_one, 

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 7c958427f353551742ab659cd384fccd0ed2d1b9..7de29c941770cf78ee1366db37a006283bf48a9e 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -115,6 +115,10 @@ namespace BEEV
 
     VariablesInExpression& vars;
 
+    bool simplify;
+
+    ASTNode simplifyNode(const ASTNode n);
+
   public:
     //constructor
   BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp), vars(simp->getVariablesInExpression())
@@ -122,6 +126,7 @@ namespace BEEV
       ASTTrue = _bm->CreateNode(TRUE);
       ASTFalse = _bm->CreateNode(FALSE);
       ASTUndefined = _bm->CreateNode(UNDEFINED);
+      simplify=true;
     };
 
      //Destructor
@@ -132,7 +137,7 @@ namespace BEEV
 
     //Top Level Solver: Goes over the input DAG, identifies the
     //equation to be solved, solves them,
-    ASTNode TopLevelBVSolve(const ASTNode& a);
+    ASTNode TopLevelBVSolve(const ASTNode& a, const bool enable_simplify=true);
 
     void ClearAllTables(void)
     {