Refactor. This shouldn't change anything

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index bcd4783decbc3ab97f2fc06c9ddde03819bc1825..7735599df150c6091f36b61ee2c0498ba174fde6 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -59,7 +59,8 @@ namespace BEEV
   void BVSolver::UpdateAlreadySolvedMap(const ASTNode& key, 
                                         const ASTNode& value)
   {
-    FormulasAlreadySolvedMap[key] = value;
+    assert(key.GetType() == BOOLEAN_TYPE);
+         FormulasAlreadySolvedMap[key] = value;
   } //end of UpdateAlreadySolvedMap()
 
   //accepts an even number "in", and returns the location of
@@ -75,72 +76,9 @@ namespace BEEV
        assert(number_shifts >0); // shouldn't be odd.
   }
 
-
-#if 0
-  //Checks if there are any ARRAYREADS in the term, after the
-  //alreadyseenmap is cleared, i.e. traversing a new term altogether
-  bool BVSolver::CheckForArrayReads_TopLevel(const ASTNode& term)
-  {
-    TermsAlreadySeenMap.clear();
-    return CheckForArrayReads(term);
-  }
-
-  //Checks if there are any ARRAYREADS in the term
-  bool BVSolver::CheckForArrayReads(const ASTNode& term)
-  {
-    ASTNode a = term;
-    ASTNodeMap::iterator it;
-    if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end())
-      {
-        //if the term has been seen, then _simply return true, else
-        //return false
-        if (ASTTrue == (it->second))
-          {
-            return true;
-          }
-        else
-          {
-            return false;
-          }
-      }
-
-    switch (term.GetKind())
-      {
-      case READ:
-        //an array read has been seen. Make an entry in the map and
-        //return true
-        TermsAlreadySeenMap[term] = ASTTrue;
-        return true;
-      default:
-        {
-          ASTVec c = term.GetChildren();
-          for (ASTVec::iterator 
-                 it = c.begin(), itend = c.end(); it != itend; it++)
-            {
-              if (CheckForArrayReads(*it))
-                {
-                  return true;
-                }
-            }
-          break;
-        }
-      }
-
-    //If control is here, then it means that no arrayread was seen for
-    //the input 'term'. Make an entry in the map with the term as key
-    //and FALSE as value.
-    TermsAlreadySeenMap[term] = ASTFalse;
-    return false;
-  } //end of CheckForArrayReads()
-#endif
-
   bool BVSolver::DoNotSolveThis(const ASTNode& var)
   {
-    if (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end())
-      {
-        return true;
-      }
-    return false;
+    return (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end());
   }
 
   //chooses a variable in the lhs and returns the chosen variable
@@ -157,12 +95,14 @@ namespace BEEV
     const ASTNode& lhs = lhsIsPlus? eq[0] : eq[1];
     const ASTNode& rhs = lhsIsPlus? eq[1] : eq[0];
 
+    assert(BVPLUS == lhs.GetKind());
+
     //collect all the vars in the lhs and rhs
     BuildSymbolGraph(eq);
     CountOfSymbols count(symbol_graph[eq]);
 
     //handle BVPLUS case
-    const ASTVec& c = lhs.GetChildren();
+    ASTVec c = FlattenKind(BVPLUS, lhs.GetChildren());
     ASTVec o;
     ASTNode outmonom = ASTUndefined;
     bool chosen_symbol = false;

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 47738244f1b81c699f5f02261a3d1a26883e932e..bbfd5603aa4cfe8969b1f30624145a4d0d736219 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -53,24 +53,6 @@ namespace BEEV
     //
     ASTNode ASTTrue, ASTFalse, ASTUndefined;
 
-    //Those formulas which have already been solved. If the same
-    //formula occurs twice then do not solve the second occurence, and
-    //instead drop it
-    ASTNodeMap FormulasAlreadySolvedMap;
-
-    //this map is useful while traversing terms and uniquely
-    //identifying variables in the those terms. Prevents double
-    //counting.
-
-    typedef HASHMAP<
-         Symbols*,
-         ASTNodeSet,
-         SymbolPtrHasher
-         > SymbolPtrToNode;
-       SymbolPtrToNode TermsAlreadySeenMap;
-
-       //ASTNodeMap TermsAlreadySeenMap_ForArrays;
-
     //solved variables list: If a variable has been solved for then do
     //not solve for it again
     ASTNodeSet DoNotSolve_TheseVars;
@@ -89,20 +71,41 @@ namespace BEEV
     ASTNode BVSolve_Even(const ASTNode& eq);
     ASTNode CheckEvenEqn(const ASTNode& input, bool& evenflag);
 
-    //Checks for arrayreads in a term. if yes then returns true, else
-    //return false
-    //bool CheckForArrayReads(const ASTNode& term);
-    //bool CheckForArrayReads_TopLevel(const ASTNode& term);
-
+    /////////////////////////
+    // When solving, we're interested in whether variables appear multiple times.
     typedef HASHSET<Symbols*,SymbolPtrHasher> SymbolPtrSet;
 
+       typedef HASHMAP<
+         ASTNode,
+         Symbols*,
+         ASTNode::ASTNodeHasher,
+         ASTNode::ASTNodeEqual> ASTNodeToNodes;
+         ASTNodeToNodes symbol_graph;
+
+         Symbols* BuildSymbolGraph(const ASTNode& n);
+
+           //this map is useful while traversing terms and uniquely
+           //identifying variables in the those terms. Prevents double
+           //counting.
+
+           typedef HASHMAP<
+                 Symbols*,
+                 ASTNodeSet,
+                 SymbolPtrHasher
+                 > SymbolPtrToNode;
+               SymbolPtrToNode TermsAlreadySeenMap;
+
     //this function return true if the var occurs in term, else the
     //function returns false
     bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
     void SetofVarsSeenInTerm(const ASTNode& term, ASTNodeSet& symbols);
-
     void VarSeenInTerm(Symbols* term, SymbolPtrSet& visited, ASTNodeSet& found, vector<Symbols*>& av);
 
+
+    /////////////////////////
+
+
+
     ASTNode solveForXOR(const ASTNode& n);
     ASTNode solveForAndOfXOR(const ASTNode& n);
 
@@ -116,6 +119,12 @@ namespace BEEV
     void SplitEven_into_Oddnum_PowerOf2(const ASTNode& in,
                                            unsigned int& number_shifts);
 
+
+    //Those formulas which have already been solved. If the same
+    //formula occurs twice then do not solve the second occurence, and
+    //instead drop it
+    ASTNodeMap FormulasAlreadySolvedMap;
+
     //Once a formula has been solved, then update the alreadysolvedmap
     //with the formula, and the solved value. The solved value can be
     //described using the following example: Suppose input to the
@@ -135,14 +144,6 @@ namespace BEEV
     //else returns FALSE
     bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output);
 
-       typedef HASHMAP<
-         ASTNode,
-         Symbols*,
-         ASTNode::ASTNodeHasher,
-         ASTNode::ASTNodeEqual> ASTNodeToNodes;
-         ASTNodeToNodes symbol_graph;
-
-         Symbols* BuildSymbolGraph(const ASTNode& n);
 
   public:
     //constructor