From 2d053ad479758a01d42838152e516262d1bf160e Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 2 Jan 2011 01:49:16 +0000 Subject: [PATCH] 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 --- src/simplifier/bvsolver.cpp | 72 ++++--------------------------------- src/simplifier/bvsolver.h | 65 ++++++++++++++++----------------- 2 files changed, 39 insertions(+), 98 deletions(-) diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index bcd4783..7735599 100644 --- 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 4773824..bbfd560 100644 --- 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 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& 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 -- 2.47.3