From bb6f5c090fff46190fbebfe3fe383491bd213dc1 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 30 Jan 2011 05:44:01 +0000 Subject: [PATCH] Improvement. Add substitution for variables by arbitary terms when creating substitution maps. The difficult part is check that substitutions don't create loops. This code replaces the old --config_full_bvsolve=1 option. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1098 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/RunTimes.h | 14 +- src/STPManager/STP.cpp | 40 +++-- src/simplifier/SubstitutionMap.cpp | 51 +++--- src/simplifier/SubstitutionMap.h | 196 ++++++++++++++++++++--- src/simplifier/VariablesInExpression.cpp | 83 ++++++---- src/simplifier/VariablesInExpression.h | 50 ++++-- src/simplifier/bvsolver.cpp | 6 +- src/simplifier/bvsolver.h | 6 +- src/simplifier/simplifier.h | 15 +- 9 files changed, 338 insertions(+), 123 deletions(-) diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h index b27441b..c9fe776 100644 --- a/src/AST/RunTimes.h +++ b/src/AST/RunTimes.h @@ -50,6 +50,8 @@ private: long getCurrentTime(); void addTime(Category c, long milliseconds); + long lastTime; + public: void addCount(Category c); @@ -57,7 +59,17 @@ public: void stop(Category c); void print(); - RunTimes(){} + void difference() + { + long val = getCurrentTime(); + std::cout << (val - lastTime) << "ms" << std::endl; + lastTime = val; + } + + RunTimes() + { + lastTime = getCurrentTime(); + } void clear() { diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 47a0fa9..1733ca8 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -108,19 +108,23 @@ namespace BEEV { simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); - bm->ASTNodeStats("after pure substitution: ", - simplified_solved_InputToSAT); - // Imagine: - // The simplifier simplifies (0 + T) to T - // Then bvsolve introduces (0 + T) - // Then CreateSubstitutionMap decides T maps to a constant, but leaving another (0+T). - // When we go to simplify (0 + T) will still be in the simplify cache, so will be mapped to T. - // But it shouldn't be T, it should be a constant. - // Applying the substitution map fixes this unusual case... expensively... - if (initialSize != simp->Return_SolverMap()->size()) - simplified_solved_InputToSAT = simp->applySubstitutionMapUntilArrays(simplified_solved_InputToSAT); + // The simplifier simplifies (0 + T) to T + // Then bvsolve introduces (0 + T) + // Then CreateSubstitutionMap decides T maps to a constant, but leaving another (0+T). + // When we go to simplify (0 + T) will still be in the simplify cache, so will be mapped to T. + // But it shouldn't be T, it should be a constant. + // Applying the substitution map fixes this case. + // + if (initialSize != simp->Return_SolverMap()->size()) + { + simplified_solved_InputToSAT = simp->applySubstitutionMapUntilArrays(simplified_solved_InputToSAT); + simp->haveAppliedSubstitutionMap(); + } + + bm->ASTNodeStats("after pure substitution: ", + simplified_solved_InputToSAT); simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, @@ -247,15 +251,21 @@ namespace BEEV { bm->counterexample_checking_during_refinement = true; } - if(bm->UserFlags.stats_flag) - simp->printCacheStatus(); - + // We are about to solve. Clear out all the memory associated with caches + // that we won't need again. simp->ClearCaches(); + simp->haveAppliedSubstitutionMap(); bm->ClearAllTables(); + + // Deleting it clears out all the buckets associated with hashmaps etc. too. delete bvsolver; bvsolver = new BVSolver(bm,simp); + if(bm->UserFlags.stats_flag) + simp->printCacheStatus(); + + // If it doesn't contain array operations, use ABC's CNF generation. if (!arrayops || !bm->UserFlags.arrayread_refinement_flag) { @@ -337,7 +347,7 @@ namespace BEEV { if(!bm->UserFlags.num_absrefine_flag) { - FatalError("TopLevelSTPAux: reached the end without proper conclusion:" + FatalError("TopLevelSTPAux: reached the end without proper conclusion:" "either a divide by zero in the input or a bug in STP"); //bogus return to make the compiler shut up return SOLVER_ERROR; diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index 6303505..53b01d0 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -19,26 +19,29 @@ SubstitutionMap::~SubstitutionMap() // This makes it easier to spot how long is spent in the simplifier. const bool simplify_during_create_subM = false; -//if a is READ(Arr,const) or SYMBOL, and b is BVCONST then return 1 -//if b is READ(Arr,const) or SYMBOL, and a is BVCONST then return -1 +//if a is READ(Arr,const) and b is BVCONST then return 1. +//if a is a symbol SYMBOL, return 1. +//if b is READ(Arr,const) and a is BVCONST then return -1 +// if b is a symbol return -1. // //else return 0 by default int TermOrder(const ASTNode& a, const ASTNode& b) { - Kind k1 = a.GetKind(); - Kind k2 = b.GetKind(); + const Kind k1 = a.GetKind(); + const Kind k2 = b.GetKind(); + + if (k1 == SYMBOL) + return 1; + + if (k2 == SYMBOL) + return -1; + //a is of the form READ(Arr,const), and b is const, or - //a is of the form var, and b is const if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && (k2 == BVCONST))) - // || k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() - // == BVCONST))) - return 1; - - if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2 || SYMBOL ==k2)) return 1; //b is of the form READ(Arr,const), and a is const, or @@ -49,31 +52,19 @@ int TermOrder(const ASTNode& a, const ASTNode& b) && b[1].GetKind() == BVCONST))) return -1; - if (SYMBOL == k2 - && (BVCONST == k1 - || TRUE == k1 - || FALSE == k1 - || SYMBOL == k1 - )) - return -1; - return 0; } //End of TermOrder() -//This finds everything which is: (= SYMBOL BVCONST), (READ SYMBOL BVCONST), + +//This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)), // (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL) // or (=SYMBOL BVCONST). -// The bvsolver goes to a lot more trouble to make similar substitutions, the -// main advantage that the below function has is that it doesn't need to check -// (much) if the symbol being substituted for is on the RHS. -//The UpdateSubstitionMap() function does all the checking that's needed. -// -//i.e. anything that has a termorder of 1 or -1. +// It tries to remove the conjunct, storing it in the substitutionmap. It replaces it in the +// formula by true. // The bvsolver puts expressions of the form (= SYMBOL TERM) into the solverMap. -ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransformer*at -) +ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransformer*at) { if (!bm->UserFlags.wordlevel_solve_flag) return a; @@ -152,8 +143,10 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransform if (CheckSubstitutionMap(symbol) || CheckSubstitutionMap(rhs)) return output; - (*SolverMap)[symbol] = bm->CreateNode(NOT,rhs); - return ASTTrue; + if (UpdateSolverMap(symbol, bm->CreateNode(NOT, rhs))) + return ASTTrue; + else + return output; } diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index d0aba07..a7935c6 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -9,12 +9,15 @@ #include "../AST/AST.h" #include "../STPManager/STPManager.h" #include "../AST/NodeFactory/SimplifyingNodeFactory.h" +#include "VariablesInExpression.h" namespace BEEV { class Simplifier; class ArrayTransformer; +const bool debug_substn = true; + class SubstitutionMap { ASTNodeMap * SolverMap; @@ -22,7 +25,28 @@ class SubstitutionMap { STPMgr* bm; ASTNode ASTTrue, ASTFalse, ASTUndefined; + // These are used to avoid substituting {x = f(y,z), z = f(x)} + typedef hash_map DependsType; + DependsType dependsOn; // The lhs depends on the variables in the rhs. + ASTNodeSet rhs; // All the rhs that have been seeen. + VariablesInExpression::SymbolPtrSet rhs_visited; // the rhs contains all the variables in here already. + + int loopCount; + public: + + // When the substitutionMap has been applied globally, then, + // these are no longer needed. + void haveAppliedSubstitutionMap() + { + dependsOn.clear(); + rhs.clear(); + rhs_visited.clear(); + } + + + VariablesInExpression vars; + SubstitutionMap(Simplifier *_simp, STPMgr* _bm) { simp = _simp; bm = _bm; @@ -32,11 +56,13 @@ public: ASTUndefined = bm->CreateNode(UNDEFINED); SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE); - + loopCount = 0; } - void clear() { + void clear() + { SolverMap->clear(); + haveAppliedSubstitutionMap(); } virtual ~SubstitutionMap(); @@ -52,10 +78,133 @@ public: return false; } + // Adds to the dependency graph that n0 depends on the variables in n1. + // It's not the transitive closure of the dependencies. Just the variables in the expression "n1". + // This is only needed as long as all the substitution rules haven't been written through. + void buildDepends(const ASTNode& n0, const ASTNode& n1) + { + if (n0.GetKind() != SYMBOL) + return; + + if (n1.isConstant()) + return; + + vector av; + vars.VarSeenInTerm(vars.getSymbol(n1), rhs_visited, rhs, av); + + sort(av.begin(), av.end()); + for (int i =0; i < av.size();i++) + { + if (i!=0 && av[i] == av[i-1]) + continue; // Treat it like a set of Symbol* in effect. + const ASTNodeSet& sym = *(vars.TermsAlreadySeenMap.find(av[i])->second); + rhs.insert(sym.begin(), sym.end()); + } + + assert (dependsOn.find(n0) == dependsOn.end()); + dependsOn.insert(make_pair(n0,vars.getSymbol(n1))); + } + + // Take the transitive closure of the varsToCheck. Storing the result in visited. + void loops_helper(const set& varsToCheck, set& visited) + { + set::const_iterator visitedIt = visited.begin(); + + set toVisit; + vector visitedN; + + // for each variable. + for (set::const_iterator varIt = varsToCheck.begin(); varIt != varsToCheck.end(); varIt++) + { + while (*visitedIt < *varIt && visitedIt != visited.end()) + visitedIt++; + + if (*visitedIt == *varIt) + continue; + + visitedN.push_back(*varIt); + DependsType::iterator it; + if ((it = dependsOn.find(*varIt)) != dependsOn.end()) + { + Symbols* s= it->second; + bool destruct; + ASTNodeSet* varsSeen = vars.SetofVarsSeenInTerm(s,destruct); + toVisit.insert(varsSeen->begin(), varsSeen->end()); + + if (destruct) + delete varsSeen; + } + } + + visited.insert(visitedN.begin(), visitedN.end()); + + visitedN.clear(); + + if (toVisit.size() !=0) + loops_helper(toVisit, visited); + } + + // If n0 is replaced by n1 in the substitution map. Will it cause a loop? + // i.e. will the dependency graph be an acyclic graph still. + // For example, if we have x = F(y,z,w), it would make the substitutionMap loop + // if there's already z = F(x). + bool loops(const ASTNode& n0, const ASTNode& n1) + { + if (n0.GetKind() != SYMBOL) + return false; // sometimes this function is called with constants on the lhs. + + if (n1.isConstant()) + return false; // constants contain no variables. Can't loop. + + // We are adding an edge FROM n0, so unless there is already an edge TO n0, + // there is no change it can loop. Unless adding this would add a TO and FROM edge. + if (rhs.find(n0) == rhs.end()) + { + return vars.VarSeenInTerm(n0,n1); + } + + if (n1.GetKind() == SYMBOL && dependsOn.find(n1) == dependsOn.end() ) + return false; // The rhs is a symbol and doesn't appear. + + if (debug_substn) + cout << loopCount++ << endl; + + bool destruct = true; + ASTNodeSet* dependN = vars.SetofVarsSeenInTerm(n1,destruct); + + if (debug_substn) + { + cout << n0 << " " << n1.GetNodeNum(); //<< " Expression size:" << bm->NodeSize(n1,true); + cout << "Variables in expression: "<< dependN->size() << endl; + } + + set depend(dependN->begin(), dependN->end()); + + if (destruct) + delete dependN; + + set visited; + loops_helper(depend,visited); + + bool loops = visited.find(n0) != visited.end(); + + if (debug_substn) + cout << "Visited:" << visited.size() << "Loops:" << loops << endl; + + return (loops); + } + //update solvermap with (key,value) pair bool UpdateSolverMap(const ASTNode& key, const ASTNode& value) { ASTNode var = (BVEXTRACT == key.GetKind()) ? key[0] : key; + + if (var.GetKind() == SYMBOL && loops(var,value)) + return false; + + if (!CheckSubstitutionMap(var) && key != value) { + //cerr << "from" << key << "to" < f(w,z,y), iff, + // 1) x doesn't appear in the rhs. + // 2) x hasn't already been stored in the substitution map. + // 3) none of the variables in the transitive closure of the rhs depend on x. bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1) { int i = TermOrder(e0, e1); if (0 == i) return false; - assert(e0 != e1); // One side should be a variable, the other a constant. + assert(e0 != e1); assert(e0.GetValueWidth() == e1.GetValueWidth()); assert(e0.GetIndexWidth() == e1.GetIndexWidth()); - if (SYMBOL == e1.GetKind() && CheckSubstitutionMap(e1)) + if (e0.GetKind() == SYMBOL) { - // if we didn't check this, scenarios like: - // a <-> b - // b <-> a - // would cause a loop. - return false; + if (CheckSubstitutionMap(e0)) + return false; // already in the map. + + if (loops(e0,e1)) + return false; // loops. + } + + if (e1.GetKind() == SYMBOL) + { + if (CheckSubstitutionMap(e1)) + return false; // already in the map. + + + if (loops(e1,e0)) + return false; // loops } //e0 is of the form READ(Arr,const), and e1 is const, or - //e0 is of the form var, and e1 is const + //e0 is of the form var, and e1 is a function. if (1 == i && !CheckSubstitutionMap(e0)) { - assert((e1.GetKind() == TRUE) || - (e1.GetKind() == FALSE) || - (e1.GetKind() == SYMBOL) || - (e1.GetKind() == BVCONST)); + buildDepends(e0,e1); (*SolverMap)[e0] = e1; return true; } @@ -107,10 +267,7 @@ public: //e1 is of the form READ(Arr,const), and e0 is const, or //e1 is of the form var, and e0 is const if (-1 == i && !CheckSubstitutionMap(e1)) { - assert((e0.GetKind() == TRUE) || - (e0.GetKind() == FALSE) || - (e0.GetKind() == SYMBOL) || - (e0.GetKind() == BVCONST)); + buildDepends(e1,e0); (*SolverMap)[e1] = e0; return true; } @@ -127,8 +284,7 @@ public: // Replace any nodes in "n" that exist in the fromTo map. // NB the fromTo map is changed. static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf); - - static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf, bool stopAtArrays); + static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf, bool stopAtArrays); }; diff --git a/src/simplifier/VariablesInExpression.cpp b/src/simplifier/VariablesInExpression.cpp index bf00316..36ecc2c 100644 --- a/src/simplifier/VariablesInExpression.cpp +++ b/src/simplifier/VariablesInExpression.cpp @@ -12,21 +12,13 @@ VariablesInExpression::VariablesInExpression() { } VariablesInExpression::~VariablesInExpression() { - 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; - } - } - - for (SymbolPtrToNode::iterator it = TermsAlreadySeenMap.begin(); it != TermsAlreadySeenMap.end() ; it++) - delete (it->second); - - symbol_graph.clear(); + ClearAllTables(); +} +void VariablesInExpression::insert(const ASTNode& n, Symbols *s) +{ + assert (s!= NULL); + symbol_graph.insert(make_pair(n.GetNodeNum(), s)); } // This builds a reduced version of a graph, where there @@ -34,9 +26,9 @@ VariablesInExpression::~VariablesInExpression() { // in the descendents changes. For example (EXTRACT 0 1 n) // will have the same "Symbols" node as n, because // no new symbols are introduced. -Symbols* VariablesInExpression::BuildSymbolGraph(const ASTNode& n) { - if (symbol_graph.find(n) != symbol_graph.end()) { - return symbol_graph[n]; +Symbols* VariablesInExpression::getSymbol(const ASTNode& n) { + if (symbol_graph.find(n.GetNodeNum()) != symbol_graph.end()) { + return symbol_graph[n.GetNodeNum()]; } Symbols* node; @@ -45,13 +37,13 @@ Symbols* VariablesInExpression::BuildSymbolGraph(const ASTNode& n) { // can ignore them. if (n.GetKind() == SYMBOL && n.GetIndexWidth() == 0) { node = new Symbols(n); - symbol_graph.insert(make_pair(n, node)); + insert(n, node); return node; } vector children; for (int i = 0; i < n.Degree(); i++) { - Symbols* v = BuildSymbolGraph(n[i]); + Symbols* v = getSymbol(n[i]); if (!v->empty()) children.push_back(v); } @@ -62,7 +54,7 @@ Symbols* VariablesInExpression::BuildSymbolGraph(const ASTNode& n) { } else node = new Symbols(children); - symbol_graph.insert(make_pair(n, node)); + insert(n, node); return node; } @@ -99,30 +91,41 @@ void VariablesInExpression::VarSeenInTerm(Symbols* term, SymbolPtrSet& visited, return; }//End of VarSeenInTerm -#if 0 -void VariablesInExpression::SetofVarsSeenInTerm(const ASTNode& term, ASTNodeSet& symbols) +ASTNodeSet * VariablesInExpression::SetofVarsSeenInTerm(Symbols* symbol, bool& destruct) { - assert(symbols.size() ==0); + assert(symbol != NULL); - BuildSymbolGraph(term); + SymbolPtrToNode::iterator it = TermsAlreadySeenMap.find(symbol); + + if ( it != TermsAlreadySeenMap.end()) + { + destruct = false; + return it->second; + } SymbolPtrSet visited; + ASTNodeSet *symbols = new ASTNodeSet(); vector av; - VarSeenInTerm(symbol_graph[term],visited,symbols,av); + VarSeenInTerm(symbol,visited,*symbols,av); for (int i =0; i < av.size();i++) { const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second; - symbols.insert(sym.begin(), sym.end()); + symbols->insert(sym.begin(), sym.end()); } - if (visited.size() > 50) // No use caching it, unless we've done some work. - { - TermsAlreadySeenMap.insert(make_pair(symbol_graph[term],symbols)); - } + destruct = true; + //TermsAlreadySeenMap.insert(make_pair(symbol,symbols)); + + return symbols; +} + +ASTNodeSet * VariablesInExpression::SetofVarsSeenInTerm(const ASTNode& term, bool& destruct) +{ + getSymbol(term); + return SetofVarsSeenInTerm(symbol_graph[term.GetNodeNum()], destruct); } -#endif bool VariablesInExpression::VarSeenInTerm(const ASTNode& var, const ASTNode& term) { @@ -131,12 +134,12 @@ bool VariablesInExpression::VarSeenInTerm(const ASTNode& var, if (term.isConstant()) return false; - BuildSymbolGraph(term); + getSymbol(term); SymbolPtrSet visited; ASTNodeSet *symbols = new ASTNodeSet(); vector av; - VarSeenInTerm(symbol_graph[term], visited, *symbols, av); + VarSeenInTerm(symbol_graph[term.GetNodeNum()], visited, *symbols, av); bool result = (symbols->count(var) != 0); @@ -144,13 +147,23 @@ bool VariablesInExpression::VarSeenInTerm(const ASTNode& var, //cerr << "av:" << av.size() << endl; //cerr << "Term is const" << term.isConstant() << endl; - if (visited.size() > 50) // No use caching it, unless we've done some work. + + if (visited.size() > 150) // No use caching it, unless we've done some work. { + sort(av.begin(), av.end()); + + //cout << "===" << endl; for (int i = 0; i < av.size(); i++) { + if (i!=0 && av[i] == av[i-1]) + continue; + const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second; + cout << "set: " << i << " " << sym.size() << endl; symbols->insert(sym.begin(), sym.end()); } - TermsAlreadySeenMap.insert(make_pair(symbol_graph[term], symbols)); + TermsAlreadySeenMap.insert(make_pair(symbol_graph[term.GetNodeNum()], symbols)); + //cout << "finish" << symbols->size() << endl; + //cout << "===" << endl; result = (symbols->count(var) != 0); } else { const int size = av.size(); diff --git a/src/simplifier/VariablesInExpression.h b/src/simplifier/VariablesInExpression.h index 24aff63..812dd3c 100644 --- a/src/simplifier/VariablesInExpression.h +++ b/src/simplifier/VariablesInExpression.h @@ -1,8 +1,6 @@ /* * VariablesInExpression.h * - * Created on: 27/01/2011 - * Author: thansen */ #ifndef VARIABLESINEXPRESSION_H_ @@ -11,15 +9,24 @@ #include "../AST/AST.h" #include "Symbols.h" -//#include "../STPManager/STPManager.h" -//#include "../AST/NodeFactory/SimplifyingNodeFactory.h" -//#include "SubstitutionMap.h" - namespace BEEV { class VariablesInExpression { +private: + VariablesInExpression(const VariablesInExpression&); + VariablesInExpression& operator=(const VariablesInExpression &); + + void insert(const ASTNode& n, Symbols *s); + + typedef HASHMAP< + int, + Symbols* + > ASTNodeToNodes; + ASTNodeToNodes symbol_graph; + + public: VariablesInExpression(); virtual ~VariablesInExpression(); @@ -28,14 +35,8 @@ public: // 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); + Symbols* getSymbol(const ASTNode& n); //this map is useful while traversing terms and uniquely //identifying variables in the those terms. Prevents double @@ -51,10 +52,29 @@ public: //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); + ASTNodeSet * SetofVarsSeenInTerm(const ASTNode& term, bool& destruct); + ASTNodeSet * SetofVarsSeenInTerm(Symbols* symbol, bool& destruct); void VarSeenInTerm(Symbols* term, SymbolPtrSet& visited, ASTNodeSet& found, vector& av); - }; + void ClearAllTables() + { + 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; + } + } + + for (SymbolPtrToNode::iterator it = TermsAlreadySeenMap.begin(); it + != TermsAlreadySeenMap.end(); it++) + delete (it->second); + + symbol_graph.clear(); + TermsAlreadySeenMap.clear(); + } +}; }; diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index 8602a7c..d3ee110 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -97,7 +97,7 @@ namespace BEEV assert(BVPLUS == lhs.GetKind()); //collect all the vars in the lhs and rhs - vars.BuildSymbolGraph(eq); + vars.getSymbol(eq); //handle BVPLUS case ASTVec c = FlattenKind(BVPLUS, lhs.GetChildren()); @@ -733,7 +733,7 @@ namespace BEEV which shouldn't be simplified. */ - ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula + ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula (_simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it; if (ASTFalse == aaa) @@ -793,7 +793,7 @@ namespace BEEV // Imagine in the last conjunct A is replaced by B. But there could // be variable A's in the first conjunct. This gets rid of 'em. output = _simp->applySubstitutionMapUntilArrays(output); - + _simp->haveAppliedSubstitutionMap(); UpdateAlreadySolvedMap(_input, output); _bm->GetRunTimes()->stop(RunTimes::BVSolver); diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h index 3c09896..7c95842 100644 --- a/src/simplifier/bvsolver.h +++ b/src/simplifier/bvsolver.h @@ -113,11 +113,11 @@ namespace BEEV //else returns FALSE bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output); - VariablesInExpression vars; + VariablesInExpression& vars; public: //constructor - BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp) + BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp), vars(simp->getVariablesInExpression()) { ASTTrue = _bm->CreateNode(TRUE); ASTFalse = _bm->CreateNode(FALSE); @@ -138,8 +138,6 @@ namespace BEEV { DoNotSolve_TheseVars.clear(); FormulasAlreadySolvedMap.clear(); - //TermsAlreadySeenMap.clear(); - } //End of ClearAllTables() }; //end of class bvsolver diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 271f238..e85572f 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -59,7 +59,7 @@ namespace BEEV ASTNode makeTower(const Kind k , const ASTVec& children); public: - + /**************************************************************** * Public Member Functions * ****************************************************************/ @@ -247,6 +247,12 @@ namespace BEEV return substitutionMap.Return_SolverMap(); } // End of SolverMap() + void haveAppliedSubstitutionMap() + { + substitutionMap.haveAppliedSubstitutionMap(); + } + + void ClearAllTables(void) { SimplifyMap->clear(); @@ -258,6 +264,7 @@ namespace BEEV substitutionMap.clear(); } + // These can be cleared (to save memory) without changing the answer. void ClearCaches() { @@ -265,6 +272,12 @@ namespace BEEV MultInverseMap.clear(); SimplifyMap->clear(); SimplifyNegMap->clear(); + getVariablesInExpression().ClearAllTables(); + } + + VariablesInExpression& getVariablesInExpression() + { + return substitutionMap.vars; } };//end of class Simplifier -- 2.47.3