long getCurrentTime();
void addTime(Category c, long milliseconds);
+ long lastTime;
+
public:
void addCount(Category c);
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()
{
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,
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)
{
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;
// 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
&& 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;
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;
}
#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;
STPMgr* bm;
ASTNode ASTTrue, ASTFalse, ASTUndefined;
+ // These are used to avoid substituting {x = f(y,z), z = f(x)}
+ typedef hash_map<ASTNode, Symbols*,ASTNode::ASTNodeHasher> 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;
ASTUndefined = bm->CreateNode(UNDEFINED);
SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
-
+ loopCount = 0;
}
- void clear() {
+ void clear()
+ {
SolverMap->clear();
+ haveAppliedSubstitutionMap();
}
virtual ~SubstitutionMap();
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<Symbols*> 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<ASTNode>& varsToCheck, set<ASTNode>& visited)
+ {
+ set<ASTNode>::const_iterator visitedIt = visited.begin();
+
+ set<ASTNode> toVisit;
+ vector<ASTNode> visitedN;
+
+ // for each variable.
+ for (set<ASTNode>::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<ASTNode> depend(dependN->begin(), dependN->end());
+
+ if (destruct)
+ delete dependN;
+
+ set<ASTNode> 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" <<value;
+ buildDepends(key,value);
(*SolverMap)[key] = value;
return true;
}
return false;
}
+ // 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) {
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;
}
//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;
}
// 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);
};
}
VariablesInExpression::~VariablesInExpression() {
- set<Symbols*> 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
// 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;
// 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<Symbols*> 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);
}
} else
node = new Symbols(children);
- symbol_graph.insert(make_pair(n, node));
+ insert(n, node);
return node;
}
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<Symbols*> 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) {
if (term.isConstant())
return false;
- BuildSymbolGraph(term);
+ getSymbol(term);
SymbolPtrSet visited;
ASTNodeSet *symbols = new ASTNodeSet();
vector<Symbols*> av;
- VarSeenInTerm(symbol_graph[term], visited, *symbols, av);
+ VarSeenInTerm(symbol_graph[term.GetNodeNum()], visited, *symbols, av);
bool result = (symbols->count(var) != 0);
//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();
/*
* VariablesInExpression.h
*
- * Created on: 27/01/2011
- * Author: thansen
*/
#ifndef VARIABLESINEXPRESSION_H_
#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();
// When solving, we're interested in whether variables appear multiple times.
typedef HASHSET<Symbols*,SymbolPtrHasher> 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
//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<Symbols*>& av);
- };
+ void ClearAllTables()
+ {
+ set<Symbols*> 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();
+ }
+};
};
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());
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)
// 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);
//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);
{
DoNotSolve_TheseVars.clear();
FormulasAlreadySolvedMap.clear();
- //TermsAlreadySeenMap.clear();
-
} //End of ClearAllTables()
}; //end of class bvsolver
ASTNode makeTower(const Kind k , const ASTVec& children);
public:
-
+
/****************************************************************
* Public Member Functions *
****************************************************************/
return substitutionMap.Return_SolverMap();
} // End of SolverMap()
+ void haveAppliedSubstitutionMap()
+ {
+ substitutionMap.haveAppliedSubstitutionMap();
+ }
+
+
void ClearAllTables(void)
{
SimplifyMap->clear();
substitutionMap.clear();
}
+
// These can be cleared (to save memory) without changing the answer.
void ClearCaches()
{
MultInverseMap.clear();
SimplifyMap->clear();
SimplifyNegMap->clear();
+ getVariablesInExpression().ClearAllTables();
+ }
+
+ VariablesInExpression& getVariablesInExpression()
+ {
+ return substitutionMap.vars;
}
};//end of class Simplifier
projects / francis / stp.git / commitdiff