From: trevor_hansen Date: Thu, 24 Jun 2010 11:38:31 +0000 (+0000) Subject: Speedup. Better cache the variables that are discovered when looking for duplicate... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=443d74017f4f8a4222622e5893314117e232a85a;p=francis%2Fstp.git Speedup. Better cache the variables that are discovered when looking for duplicate symbols. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@872 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/simplifier/Symbols.h b/src/simplifier/Symbols.h index 1a46ed9..adc0e2e 100644 --- a/src/simplifier/Symbols.h +++ b/src/simplifier/Symbols.h @@ -8,7 +8,6 @@ class Symbols { Symbols& operator =(const Symbols& other) { /*..*/} Symbols(const Symbols& other) {/*..*/} -// pair cache; public: const ASTNode found; @@ -19,6 +18,7 @@ class Symbols { Symbols(const ASTNode& n): found(n) { + assert(BEEV::SYMBOL == n.GetKind()); } // This will create an "empty" node if the array is empty. @@ -34,30 +34,14 @@ class Symbols { assert(children.size() != 1); } - bool isContained(const ASTNode& n) { -// if (cache.first == n) -// return cache.second; - - bool result = false; - if (!found.IsNull()) - result = (found == n); - else { - for (int i = 0; i < children.size(); i++) - if (children[i]->isContained(n)) - { - result = true; - break; - } - } -// cache = make_pair(n,result); - return result; + bool isLeaf() + { + return !found.IsNull(); } bool empty() const { return (found.IsNull() && children.size() == 0); } - - }; class SymbolPtrHasher diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index ffa1127..43c2676 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -1,6 +1,6 @@ // -*- c++ -*- /******************************************************************** - * AUTHORS: Vijay Ganesh + * AUTHORS: Vijay Ganesh, Trevor Hansen * * BEGIN DATE: November, 2005 * @@ -38,6 +38,7 @@ //4. Outside the solver, Substitute and Re-normalize the input DAG namespace BEEV { + //experimental options. Don't curerntly work. const bool flatten_ands = false; const bool sort_extracts_last = false; @@ -72,44 +73,8 @@ namespace BEEV && !CONSTANTBV::BitVector_bit_test(in.GetBVConst(), number_shifts); number_shifts++) { }; assert(number_shifts >0); // shouldn't be odd. - -#ifndef NDEBUG - // check that old == new. - unsigned t_number_shifts=0; - SplitEven_into_Oddnum_PowerOf2_OLD(in,t_number_shifts); - assert(number_shifts == t_number_shifts); -#endif } - //FIXME This is doing way more arithmetic than it needs to. - //accepts an even number "in", and splits it into an odd number and - //a power of 2. i.e " in = b.(2^k) ". returns the odd number, and - //the power of two by reference - ASTNode BVSolver::SplitEven_into_Oddnum_PowerOf2_OLD(const ASTNode& in, - unsigned int& number_shifts) - { - if (BVCONST != in.GetKind() || _simp->BVConstIsOdd(in)) - { - FatalError("BVSolver:SplitNum_Odd_PowerOf2: "\ - "input must be a BVCONST and even\n", in); - } - - unsigned int len = in.GetValueWidth(); - ASTNode zero = _bm->CreateZeroConst(len); - ASTNode two = _bm->CreateTwoConst(len); - ASTNode div_by_2 = in; - ASTNode mod_by_2 = - _simp->BVConstEvaluator(_bm->CreateTerm(BVMOD, len, div_by_2, two)); - while (mod_by_2 == zero) - { - div_by_2 = - _simp->BVConstEvaluator(_bm->CreateTerm(BVDIV, len, div_by_2, two)); - number_shifts++; - mod_by_2 = - _simp->BVConstEvaluator(_bm->CreateTerm(BVMOD, len, div_by_2, two)); - } - return div_by_2; - } //end of SplitEven_into_Oddnum_PowerOf2() #if 0 //Checks if there are any ARRAYREADS in the term, after the @@ -997,35 +962,41 @@ namespace BEEV return node; } - - bool BVSolver::VarSeenInTerm(const ASTNode& var, Symbols* term) + // Builds a set of the SYMBOLS that were found under the "term". The symbols are the union of "found" and + // all the sets : TermsAlreadySeen(av[0]) union ... TermsAlreadySeen(av[n])". + void BVSolver::VarSeenInTerm(Symbols* term, SymbolPtrSet& visited, ASTNodeSet& found, vector& av) { - SymbolPtrToNode::iterator it; + if (visited.find(term) != visited.end()) + { + return; + } + SymbolPtrToNode::const_iterator it; if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end()) { - if (it->second == var) - { - return false; - } + // We've previously built the set of variables below this "symbols". + // It's not added into "found" because its sometimes 70k variables + // big, and if there are no other symbols discovered it's a terrible + // waste to create a copy of the set. Instead we store (in effect) + // a pointer to the set. + av.push_back(term); + return; } - if (var == term->found) - { - return true; - } + if (term->isLeaf()) + { + found.insert(term->found); + return; + } for (vector::const_iterator it = term->children.begin(), itend = term->children.end(); it != itend; it++) { - if (VarSeenInTerm(var, *it)) - { - return true; - } + VarSeenInTerm(*it,visited,found,av); } - TermsAlreadySeenMap[term] = var; - return false; + visited.insert(term); + return; }//End of VarSeenInTerm bool BVSolver::VarSeenInTerm(const ASTNode& var, const ASTNode& term) @@ -1033,7 +1004,31 @@ namespace BEEV // This only returns true if we are searching for variables that aren't arrays. assert(var.GetKind() == SYMBOL && var.GetIndexWidth() == 0); BuildSymbolGraph(term); - return VarSeenInTerm(var,symbol_graph[term]); + + SymbolPtrSet visited; + ASTNodeSet symbols; + vector av; + VarSeenInTerm(symbol_graph[term],visited,symbols,av); + + bool result = (symbols.count(var) !=0); + for (int i =0 ; i < av.size();i++) + { + if (result) + break; + const ASTNodeSet& sym = TermsAlreadySeenMap.find(av[i])->second; + result |= (sym.find(var) !=sym.end()); + } + + if (visited.size() > 50) // No use caching it, unless we've done some work. + { + for (int i =0 ; i < av.size();i++) + { + const ASTNodeSet& sym = TermsAlreadySeenMap.find(av[i])->second; + symbols.insert(sym.begin(), sym.end()); + } + TermsAlreadySeenMap.insert(make_pair(symbol_graph[term],symbols)); + } + return result; } diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h index 580005c..0455a73 100644 --- a/src/simplifier/bvsolver.h +++ b/src/simplifier/bvsolver.h @@ -61,9 +61,10 @@ namespace BEEV //this map is useful while traversing terms and uniquely //identifying variables in the those terms. Prevents double //counting. - typedef HASHMAP< + + typedef HASHMAP< Symbols*, - ASTNode, + ASTNodeSet, SymbolPtrHasher > SymbolPtrToNode; SymbolPtrToNode TermsAlreadySeenMap; @@ -78,11 +79,6 @@ namespace BEEV //true else return false bool DoNotSolveThis(const ASTNode& var); - //traverses a term, and creates a multiset of all variables in the - //term. Does memoization to avoid double counting. - void VarsInTheTerm(const ASTNode& lhs, ASTNodeMultiSet& v); - void VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& v); - //choose a suitable var from the term ASTNode ChooseMonom(const ASTNode& eq, ASTNode& modifiedterm); //accepts an equation and solves for a variable or a monom in it @@ -98,13 +94,13 @@ namespace BEEV //bool CheckForArrayReads(const ASTNode& term); //bool CheckForArrayReads_TopLevel(const ASTNode& term); - //Creates new variables used in solving - ASTNode NewVar(unsigned int n); + typedef HASHSET SymbolPtrSet; //this function return true if the var occurs in term, else the //function returns false bool VarSeenInTerm(const ASTNode& var, const ASTNode& term); - bool VarSeenInTerm(const ASTNode& var, Symbols* term); + + void VarSeenInTerm(Symbols* term, SymbolPtrSet& visited, ASTNodeSet& found, vector& av); //takes an even number "in" as input, and returns an odd number @@ -117,9 +113,6 @@ namespace BEEV void SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, unsigned int& number_shifts); - ASTNode SplitEven_into_Oddnum_PowerOf2_OLD(const ASTNode& in, - unsigned int& number_shifts); - //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 @@ -155,30 +148,12 @@ namespace BEEV ASTTrue = _bm->CreateNode(TRUE); ASTFalse = _bm->CreateNode(FALSE); ASTUndefined = _bm->CreateNode(UNDEFINED); - } - ; - - void ClearAllCaches() - { - TermsAlreadySeenMap.clear(); - DoNotSolve_TheseVars.clear(); - FormulasAlreadySolvedMap.clear(); - //TermsAlreadySeenMap_ForArrays.clear(); - set deleted; - for (ASTNodeToNodes::iterator it = symbol_graph.begin(); it != symbol_graph.end(); it++) - { - if (deleted.find(it->second) == deleted.end()) - { - deleted.insert(it->second); - delete it->second; - } - } - } - - //Destructor + }; + + //Destructor ~BVSolver() { - ClearAllCaches(); + ClearAllTables(); } //Top Level Solver: Goes over the input DAG, identifies the @@ -187,9 +162,18 @@ namespace BEEV void ClearAllTables(void) { - DoNotSolve_TheseVars.clear(); - FormulasAlreadySolvedMap.clear(); - //TermsAlreadySeenMap_ForArrays.clear(); + TermsAlreadySeenMap.clear(); + DoNotSolve_TheseVars.clear(); + FormulasAlreadySolvedMap.clear(); + set deleted; + for (ASTNodeToNodes::iterator it = symbol_graph.begin(); it != symbol_graph.end(); it++) + { + if (deleted.find(it->second) == deleted.end()) + { + deleted.insert(it->second); + delete it->second; + } + } } //End of ClearAllTables() }; //end of class bvsolver