From: trevor_hansen Date: Sun, 30 Jan 2011 13:11:58 +0000 (+0000) Subject: * The -t option now tracks time spent applying the substitution map. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=fd7006a17b9e95b1f38f5a196725ef60d0a5ab19;p=francis%2Fstp.git * The -t option now tracks time spent applying the substitution map. * Some functions that should be private in the SubstitutionMap were made private. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1100 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp index 9c8b2bf..3b02cdc 100644 --- a/src/AST/RunTimes.cpp +++ b/src/AST/RunTimes.cpp @@ -16,7 +16,7 @@ #include "../sat/utils/System.h" // BE VERY CAREFUL> Update the Category Names to match. -std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement"}; +std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions"}; namespace BEEV { diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h index c9fe776..c2de931 100644 --- a/src/AST/RunTimes.h +++ b/src/AST/RunTimes.h @@ -31,7 +31,8 @@ public: CounterExampleGeneration, SATSimplifying, ConstantBitPropagation, - ArrayReadRefinement + ArrayReadRefinement, + ApplyingSubstitutions }; static std::string CategoryNames[]; diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index 53b01d0..fca5a83 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -185,14 +185,20 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransform ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) { + bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions); ASTNodeMap cache; - return replace(n,*SolverMap,cache,bm->defaultNodeFactory, false); + ASTNode result = replace(n,*SolverMap,cache,bm->defaultNodeFactory, false); + bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions); + return result; } ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n) { - ASTNodeMap cache; - return replace(n,*SolverMap,cache,bm->defaultNodeFactory, true); + bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions); + ASTNodeMap cache; + ASTNode result = replace(n,*SolverMap,cache,bm->defaultNodeFactory, true); + bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions); + return result; } ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, @@ -294,5 +300,121 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, return result; } +// 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 SubstitutionMap::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 SubstitutionMap::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 SubstitutionMap::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); + } }; diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index 657f278..b07a67c 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -33,6 +33,10 @@ class SubstitutionMap { int loopCount; + void buildDepends(const ASTNode& n0, const ASTNode& n1); + void loops_helper(const set& varsToCheck, set& visited); + bool loops(const ASTNode& n0, const ASTNode& n1); + public: // When the substitutionMap has been applied globally, then, @@ -44,7 +48,6 @@ public: rhs_visited.clear(); } - VariablesInExpression vars; SubstitutionMap(Simplifier *_simp, STPMgr* _bm) { @@ -78,121 +81,6 @@ 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) { @@ -215,8 +103,6 @@ public: return SolverMap; } // End of SolverMap() - - bool CheckSubstitutionMap(const ASTNode& key) { if (SolverMap->find(key) != SolverMap->end()) return true; @@ -284,7 +170,8 @@ 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); + };