From 900bbd46d35ec54fd6d25fb029bc746e1a8e350f Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 18 Feb 2012 12:37:48 +0000 Subject: [PATCH] Refactor - automatically layout code, and move one big function out of the header file. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1570 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/SubstitutionMap.cpp | 567 ++++++++++++++++------------- src/simplifier/SubstitutionMap.h | 351 ++++++++---------- 2 files changed, 468 insertions(+), 450 deletions(-) diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index 6d27bc9..9eea3e9 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -1,8 +1,3 @@ -/* - * substitutionMap.cpp - * - */ - #include "SubstitutionMap.h" #include "simplifier.h" #include "../AST/ArrayTransformer.h" @@ -10,15 +5,15 @@ namespace BEEV { -SubstitutionMap::~SubstitutionMap() -{ - delete SolverMap; - delete nf; -} + SubstitutionMap::~SubstitutionMap() + { + delete SolverMap; + delete nf; + } // if false. Don't simplify while creating the substitution map. // This makes it easier to spot how long is spent in the simplifier. -const bool simplify_during_create_subM = false; + const bool simplify_during_create_subM = false; //if a is READ(Arr,const) and b is BVCONST then return 1. //if a is a symbol SYMBOL, return 1. @@ -26,70 +21,65 @@ const bool simplify_during_create_subM = false; // if b is a symbol return -1. // //else return 0 by default -int TermOrder(const ASTNode& a, const ASTNode& b) -{ - const Kind k1 = a.GetKind(); - const Kind k2 = b.GetKind(); + int + TermOrder(const ASTNode& a, const ASTNode& b) + { + const Kind k1 = a.GetKind(); + const Kind k2 = b.GetKind(); - if (k1 == SYMBOL) - return 1; + if (k1 == SYMBOL) + return 1; - if (k2 == SYMBOL) - return -1; + if (k2 == SYMBOL) + return -1; + //a is of the form READ(Arr,const), and b is const, or + if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && (k2 == BVCONST))) + return 1; - //a is of the form READ(Arr,const), and b is const, or - if ((k1 == READ - && a[0].GetKind() == SYMBOL - && a[1].GetKind() == BVCONST - && (k2 == BVCONST))) - return 1; - - //b is of the form READ(Arr,const), and a is const, or - //b is of the form var, and a is const - if ((k1 == BVCONST) - && ((k2 == READ - && b[0].GetKind() == SYMBOL - && b[1].GetKind() == BVCONST))) - return -1; - - return 0; -} //End of TermOrder() + //b is of the form READ(Arr,const), and a is const, or + //b is of the form var, and a is const + if ((k1 == BVCONST) && ((k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST))) + return -1; + return 0; + } //End of TermOrder() // idempotent. -ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) -{ - bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions); - ASTNodeMap cache; - ASTNode result = replace(n,*SolverMap,cache,nf, false,false); - - // NB. This is an expensive check. Remove it after it's been idempotent - // for a while. - #ifndef NDEBUG - cache.clear(); - assert( result == replace(result,*SolverMap,cache,nf, false,false)); - #endif - - bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions); - return result; -} + ASTNode + SubstitutionMap::applySubstitutionMap(const ASTNode& n) + { + bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions); + ASTNodeMap cache; + ASTNode result = replace(n, *SolverMap, cache, nf, false, false); + + // NB. This is an expensive check. Remove it after it's been idempotent + // for a while. +#ifndef NDEBUG + cache.clear(); + assert( result == replace(result,*SolverMap,cache,nf, false,false)); +#endif + + bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions); + return result; + } // not always idempotent. -ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n) -{ - bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions); - ASTNodeMap cache; - ASTNode result = replace(n,*SolverMap,cache,nf, true,false); - bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions); - return result; -} - -ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, - ASTNodeMap& cache, NodeFactory * nf) -{ - return replace(n,fromTo,cache,nf,false,false); -} + ASTNode + SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n) + { + bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions); + ASTNodeMap cache; + ASTNode result = replace(n, *SolverMap, cache, nf, true, false); + bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions); + return result; + } + + ASTNode + SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory * nf) + { + return replace(n, fromTo, cache, nf, false, false); + } // NOTE the fromTo map is changed as we traverse downwards. // We call replace on each of the things in the fromTo map aswell. @@ -100,225 +90,288 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, // NB: You can't use this to map from "5" to the symbol "x" say. // It's optimised for the symbol to something case. -ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, - ASTNodeMap& cache, NodeFactory * nf, bool stopAtArrays , bool preventInfinite) -{ + ASTNode + SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory * nf, bool stopAtArrays, + bool preventInfinite) + { const Kind k = n.GetKind(); - if (k == BVCONST || k == TRUE || k == FALSE) - return n; + if (k == BVCONST || k == TRUE || k == FALSE) + return n; - ASTNodeMap::const_iterator it; + ASTNodeMap::const_iterator it; if ((it = cache.find(n)) != cache.end()) - return it->second; - - if ((it = fromTo.find(n)) != fromTo.end()) - { - const ASTNode& r = it->second; - assert(r.GetIndexWidth() == n.GetIndexWidth()); - ASTNode replaced = replace(r, fromTo, cache,nf,stopAtArrays,preventInfinite); - if (replaced != r) - fromTo[n] = replaced; - - cache.insert(make_pair(n,replaced)); - return replaced; - } - - // These can't be created like regular nodes are - if (k == SYMBOL ) - return n; - - const unsigned int indexWidth = n.GetIndexWidth(); - if (stopAtArrays && indexWidth > 0) // is an array. - { - return n; - } - - const ASTVec& children = n.GetChildren(); - assert(children.size() > 0); // Should have no leaves left here. - - ASTVec new_children; - new_children.reserve(children.size()); - - for (ASTVec::const_iterator it = children.begin(); it != children.end(); it++) - { - new_children.push_back(replace(*it, fromTo, cache,nf,stopAtArrays,preventInfinite)); - } - - assert(new_children.size() == children.size()); - - // This code short-cuts if the children are the same. Nodes with the same children, - // won't have necessarily given the same node if the simplifyingNodeFactory is enabled - // now, but wasn't enabled when the node was created. Shortcutting saves lots of time. - if (new_children == children) - { - cache.insert(make_pair(n,n)); - return n; - } - - ASTNode result; - const unsigned int valueWidth = n.GetValueWidth(); - - if (valueWidth == 0 ) // n.GetType() == BOOLEAN_TYPE - { - result = nf->CreateNode(k, new_children); - } - else - { - // If the index and value width aren't saved, they are reset sometimes (??) - result = nf->CreateArrayTerm(k,indexWidth, valueWidth,new_children); - } - - // We may have created something that should be mapped. For instance, - // if n is READ(A, x), and the fromTo is: {x==0, READ(A,0) == 1}, then - // by here the result will be READ(A,0). Which needs to be mapped again.. - // I hope that this makes it idempotent. - - if (fromTo.find(result) != fromTo.end()) - { - // map n->result, if running replace() on result gives us 'n', it will not infinite loop. - // This is only currently required for the bitblast equivalence stuff. - if (preventInfinite) - cache.insert(make_pair(n,result)); - - result = replace(result, fromTo, cache,nf,stopAtArrays,preventInfinite); - } - - assert(result.GetValueWidth() == valueWidth); - assert(result.GetIndexWidth() == indexWidth); - - // If there is already an "n" element in the cache, the maps semantics are to ignore the next insertion. - if (preventInfinite) - cache.erase(n); - - cache.insert(make_pair(n,result)); - return result; -} + return it->second; + + if ((it = fromTo.find(n)) != fromTo.end()) + { + const ASTNode& r = it->second; + assert(r.GetIndexWidth() == n.GetIndexWidth()); + ASTNode replaced = replace(r, fromTo, cache, nf, stopAtArrays, preventInfinite); + if (replaced != r) + fromTo[n] = replaced; + + cache.insert(make_pair(n, replaced)); + return replaced; + } + + // These can't be created like regular nodes are + if (k == SYMBOL) + return n; + + const unsigned int indexWidth = n.GetIndexWidth(); + if (stopAtArrays && indexWidth > 0) // is an array. + { + return n; + } + + const ASTVec& children = n.GetChildren(); + assert(children.size() > 0); + // Should have no leaves left here. + + ASTVec new_children; + new_children.reserve(children.size()); + + for (ASTVec::const_iterator it = children.begin(); it != children.end(); it++) + { + new_children.push_back(replace(*it, fromTo, cache, nf, stopAtArrays, preventInfinite)); + } + + assert(new_children.size() == children.size()); + + // This code short-cuts if the children are the same. Nodes with the same children, + // won't have necessarily given the same node if the simplifyingNodeFactory is enabled + // now, but wasn't enabled when the node was created. Shortcutting saves lots of time. + if (new_children == children) + { + cache.insert(make_pair(n, n)); + return n; + } + + ASTNode result; + const unsigned int valueWidth = n.GetValueWidth(); + + if (valueWidth == 0) // n.GetType() == BOOLEAN_TYPE + { + result = nf->CreateNode(k, new_children); + } + else + { + // If the index and value width aren't saved, they are reset sometimes (??) + result = nf->CreateArrayTerm(k, indexWidth, valueWidth, new_children); + } + + // We may have created something that should be mapped. For instance, + // if n is READ(A, x), and the fromTo is: {x==0, READ(A,0) == 1}, then + // by here the result will be READ(A,0). Which needs to be mapped again.. + // I hope that this makes it idempotent. + + if (fromTo.find(result) != fromTo.end()) + { + // map n->result, if running replace() on result gives us 'n', it will not infinite loop. + // This is only currently required for the bitblast equivalence stuff. + if (preventInfinite) + cache.insert(make_pair(n, result)); + + result = replace(result, fromTo, cache, nf, stopAtArrays, preventInfinite); + } + + assert(result.GetValueWidth() == valueWidth); + assert(result.GetIndexWidth() == indexWidth); + + // If there is already an "n" element in the cache, the maps semantics are to ignore the next insertion. + if (preventInfinite) + cache.erase(n); + + cache.insert(make_pair(n, result)); + 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; + void + SubstitutionMap::buildDepends(const ASTNode& n0, const ASTNode& n1) + { + if (n0.GetKind() != SYMBOL) + return; - if (n1.isConstant()) - return; + if (n1.isConstant()) + return; - vector av; - vars.VarSeenInTerm(vars.getSymbol(n1), rhs_visited, rhs, av); + 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. + 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. - ASTNodeSet* sym = (vars.TermsAlreadySeenMap.find(av[i])->second); - if(rhsAlreadyAdded.find(sym) != rhsAlreadyAdded.end()) - continue; - rhsAlreadyAdded.insert(sym); + ASTNodeSet* sym = (vars.TermsAlreadySeenMap.find(av[i])->second); + if (rhsAlreadyAdded.find(sym) != rhsAlreadyAdded.end()) + continue; + rhsAlreadyAdded.insert(sym); - //cout << loopCount++ << " "; - //cout << "initial" << rhs.size() << " Adding: " <size(); - rhs.insert(sym->begin(), sym->end()); - //cout << "final:" << rhs.size(); - //cout << "added:" << sym << endl; + //cout << loopCount++ << " "; + //cout << "initial" << rhs.size() << " Adding: " <size(); + rhs.insert(sym->begin(), sym->end()); + //cout << "final:" << rhs.size(); + //cout << "added:" << sym << endl; - } + } - assert (dependsOn.find(n0) == dependsOn.end()); - dependsOn.insert(make_pair(n0,vars.getSymbol(n1))); -} + 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(); + void + SubstitutionMap::loops_helper(const set& varsToCheck, set& visited) + { + set::const_iterator visitedIt = visited.begin(); - set toVisit; - vector visitedN; + set toVisit; + vector visitedN; - // for each variable. - for (set::const_iterator varIt = varsToCheck.begin(); varIt != varsToCheck.end(); varIt++) - { - while (visitedIt != visited.end() && *visitedIt < *varIt ) - visitedIt++; + // for each variable. + for (set::const_iterator varIt = varsToCheck.begin(); varIt != varsToCheck.end(); varIt++) + { + while (visitedIt != visited.end() && *visitedIt < *varIt) + visitedIt++; - if ((visitedIt != visited.end()) && *visitedIt == *varIt) - continue; + if ((visitedIt != visited.end()) && *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()); + 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; - } - } + if (destruct) + delete varsSeen; + } + } - visited.insert(visitedN.begin(), visitedN.end()); + visited.insert(visitedN.begin(), visitedN.end()); - visitedN.clear(); - - if (toVisit.size() !=0) - loops_helper(toVisit, visited); -} + 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 + 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); + } + + bool + SubstitutionMap::UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1) + { + int i = TermOrder(e0, e1); + if (0 == i) + return false; + + assert(e0 != e1); + assert(e0.GetValueWidth() == e1.GetValueWidth()); + assert(e0.GetIndexWidth() == e1.GetIndexWidth()); + + if (e0.GetKind() == SYMBOL) + { + if (CheckSubstitutionMap(e0)) + { + // e0 and e1 might both be variables, e0 is already substituted for, + // but maybe not e1. + if (e1.GetKind() == SYMBOL) + i = -1; + else + 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 a function. + if (1 == i && !CheckSubstitutionMap(e0)) + { + buildDepends(e0, e1); + (*SolverMap)[e0] = e1; + return true; + } + + //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)) + { + buildDepends(e1, e0); + (*SolverMap)[e1] = e0; + return true; + } + + return false; + } - 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 60b08f2..c1292bc 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -1,8 +1,3 @@ -/* - * substitutionMap.h - * - */ - #ifndef SUBSTITUTIONMAP_H_ #define SUBSTITUTIONMAP_H_ @@ -12,200 +7,170 @@ #include "VariablesInExpression.h" #include "../boost/noncopyable.hpp" -namespace BEEV { +namespace BEEV +{ -class Simplifier; -class ArrayTransformer; + class Simplifier; + class ArrayTransformer; + + const bool debug_substn = false; + + class SubstitutionMap : boost::noncopyable + { + + ASTNodeMap * SolverMap; + Simplifier *simp; + STPMgr* bm; + ASTNode ASTTrue, ASTFalse, ASTUndefined; + NodeFactory *nf; + + // 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. + set rhsAlreadyAdded; + VariablesInExpression::SymbolPtrSet rhs_visited; // the rhs contains all the variables in here already. + + 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); + + int substitutionsLastApplied; + public: + + bool + hasUnappliedSubstitutions() + { + return (substitutionsLastApplied != SolverMap->size()); + } + + // When the substitutionMap has been applied globally, then, + // these are no longer needed. + void + haveAppliedSubstitutionMap() + { + dependsOn.clear(); + rhs.clear(); + rhs_visited.clear(); + rhsAlreadyAdded.clear(); + substitutionsLastApplied = SolverMap->size(); + } + + VariablesInExpression vars; + + SubstitutionMap(Simplifier *_simp, STPMgr* _bm) + { + simp = _simp; + bm = _bm; + + ASTTrue = bm->CreateNode(TRUE); + ASTFalse = bm->CreateNode(FALSE); + ASTUndefined = bm->CreateNode(UNDEFINED); + + SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE); + loopCount = 0; + substitutionsLastApplied = 0; + nf = new SimplifyingNodeFactory(*bm->hashingNodeFactory, *bm); + } + + void + clear() + { + SolverMap->clear(); + haveAppliedSubstitutionMap(); + } + + virtual + ~SubstitutionMap(); + + //check the solver map for 'key'. If key is present, then return the + //value by reference in the argument 'output' + bool + CheckSubstitutionMap(const ASTNode& key, ASTNode& output) + { + ASTNodeMap::iterator it = SolverMap->find(key); + if (it != SolverMap->end()) + { + output = it->second; + return true; + } + return false; + } -const bool debug_substn = false; + //update solvermap with (key,value) pair + bool + UpdateSolverMap(const ASTNode& key, const ASTNode& value) + { + ASTNode var = (BVEXTRACT == key.GetKind()) ? key[0] : key; -class SubstitutionMap : boost::noncopyable -{ + if (var.GetKind() == SYMBOL && loops(var, value)) + return false; - ASTNodeMap * SolverMap; - Simplifier *simp; - STPMgr* bm; - ASTNode ASTTrue, ASTFalse, ASTUndefined; - NodeFactory *nf; - - // 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. - set rhsAlreadyAdded; - VariablesInExpression::SymbolPtrSet rhs_visited; // the rhs contains all the variables in here already. - - - 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); - - int substitutionsLastApplied; -public: - - bool hasUnappliedSubstitutions() - { - return (substitutionsLastApplied != SolverMap->size()); - } - - // When the substitutionMap has been applied globally, then, - // these are no longer needed. - void haveAppliedSubstitutionMap() - { - dependsOn.clear(); - rhs.clear(); - rhs_visited.clear(); - rhsAlreadyAdded.clear(); - substitutionsLastApplied = SolverMap->size(); - } - - VariablesInExpression vars; - - SubstitutionMap(Simplifier *_simp, STPMgr* _bm) - { - simp = _simp; - bm = _bm; - - ASTTrue = bm->CreateNode(TRUE); - ASTFalse = bm->CreateNode(FALSE); - ASTUndefined = bm->CreateNode(UNDEFINED); - - SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE); - loopCount = 0; - substitutionsLastApplied =0; - nf = new SimplifyingNodeFactory (*bm->hashingNodeFactory, *bm); - } - - void clear() - { - SolverMap->clear(); - haveAppliedSubstitutionMap(); - } - - virtual ~SubstitutionMap(); - - //check the solver map for 'key'. If key is present, then return the - //value by reference in the argument 'output' - bool CheckSubstitutionMap(const ASTNode& key, ASTNode& output) { - ASTNodeMap::iterator it = SolverMap->find(key); - if (it != SolverMap->end()) { - output = it->second; - return true; - } - return false; - } - - //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" <find(key) != SolverMap->end()) - return true; - else - return false; - } - - // It's depressingly expensive to perform all of the loop checks etc. - // If you use this function you are promising: - // 1) That UpdateSubstitutionMap(e0,e1) would have returned true. - // 2) That all of the substitutions will be written in fully before other code - bool UpdateSubstitutionMapFewChecks(const ASTNode& e0, const ASTNode& e1) + if (!CheckSubstitutionMap(var) && key != value) { - assert(e0.GetKind() == SYMBOL); - assert (!CheckSubstitutionMap(e0)); - (*SolverMap)[e0] = e1; - return true; + //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); - assert(e0.GetValueWidth() == e1.GetValueWidth()); - assert(e0.GetIndexWidth() == e1.GetIndexWidth()); - - if (e0.GetKind() == SYMBOL) - { - if (CheckSubstitutionMap(e0)) - { - // e0 and e1 might both be variables, e0 is already substituted for, - // but maybe not e1. - if (e1.GetKind() == SYMBOL) - i = -1; - else - 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 a function. - if (1 == i && !CheckSubstitutionMap(e0)) { - buildDepends(e0,e1); - (*SolverMap)[e0] = e1; - return true; - } - - //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)) { - buildDepends(e1,e0); - (*SolverMap)[e1] = e0; - return true; - } - - return false; - } - - ASTNode applySubstitutionMap(const ASTNode& n); - - ASTNode applySubstitutionMapUntilArrays(const ASTNode& n); - - // 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, bool preventInfiniteLoops); - - -}; + return false; + } //end of UpdateSolverMap() + + ASTNodeMap * + Return_SolverMap() + { + return SolverMap; + } // End of SolverMap() + + bool + CheckSubstitutionMap(const ASTNode& key) + { + if (SolverMap->find(key) != SolverMap->end()) + return true; + else + return false; + } + + // It's depressingly expensive to perform all of the loop checks etc. + // If you use this function you are promising: + // 1) That UpdateSubstitutionMap(e0,e1) would have returned true. + // 2) That all of the substitutions will be written in fully before other code + bool + UpdateSubstitutionMapFewChecks(const ASTNode& e0, const ASTNode& e1) + { + assert(e0.GetKind() == SYMBOL); + assert(!CheckSubstitutionMap(e0)); + (*SolverMap)[e0] = e1; + return true; + } + + // The substitutionMap will be updated, given x <-> 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); + + ASTNode + applySubstitutionMap(const ASTNode& n); + + ASTNode + applySubstitutionMapUntilArrays(const ASTNode& n); + + // 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, + bool preventInfiniteLoops); + + }; } ; -- 2.47.3