#include "../AST/AST.h"
#include <cassert>
+#include "Symbols.h"
// Count the number of times each symbol appears in the input term.
// This can be expensive to build for large terms, so it's built lazily.
ASTNode::ASTNodeEqual> ASTNodeToIntMap;
ASTNodeToIntMap Vars;
- const ASTNode& top;
+ const Symbols* top;
bool loaded;
- ASTNodeSet visited;
-
// If no variables are found in "term", then it's cached---we don't need to visit there
// again. However, if it's true, we need to revisit (and hence recount), the next time it's
// encountered.
- bool VarsInTheTerm(const ASTNode& term) {
-
- if (visited.find(term) != visited.end())
- return false;
-
- bool found = false;
+ void VarsInTheTerm(const Symbols* term) {
+ assert(!term->empty());
- switch (term.GetKind()) {
- case BVCONST:
- return false;
- case SYMBOL:
- //cerr << "debugging: symbol added: " << term << endl;
- Vars[term]++;
- return true;
- case READ:
- //skip the arrayname, provided the arrayname is a SYMBOL
- //But we don't skip it if it's a WRITE function??
- if (SYMBOL == term[0].GetKind()) {
- found |= VarsInTheTerm(term[1]);
- } else {
- found |= VarsInTheTerm(term[0]);
- found |= VarsInTheTerm(term[1]);
- }
- break;
- default: {
- const ASTVec& c = term.GetChildren();
- for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it
- != itend; it++) {
- found |= VarsInTheTerm(*it);
- }
- break;
+ if (!term->found.IsNull())
+ {
+ Vars[term->found]++;
}
+ else
+ {
+ const vector<Symbols*>& c = term->children;
+ for (vector<Symbols*>::const_iterator it = c.begin(), itend = c.end(); it
+ != itend; it++)
+ {
+ VarsInTheTerm(*it);
+ }
}
-
- if (!found)
- visited.insert(term);
- return found;
} //end of VarsInTheTerm()
public:
- CountOfSymbols(const ASTNode& top_v) :
+ CountOfSymbols(const Symbols* top_v) :
top(top_v) {
loaded = false;
}
{
VarsInTheTerm(top);
loaded = true;
- visited.clear();
}
ASTNodeToIntMap::const_iterator it = Vars.find(m);
--- /dev/null
+#ifndef SYMBOLS_H
+#define SYMBOLS_H
+
+// Each node is either: empty, an ASTNode, or a vector of more than one child nodes.
+
+class Symbols {
+ private:
+ Symbols& operator =(const Symbols& other) { /*..*/}
+ Symbols(const Symbols& other) {/*..*/}
+
+// pair<ASTNode,bool> cache;
+ public:
+
+ const ASTNode found;
+ const vector<Symbols*> children;
+
+ Symbols() {
+ }
+
+ Symbols(const ASTNode& n): found(n)
+ {
+ }
+
+ // This will create an "empty" node if the array is empty.
+ Symbols(const vector<Symbols*>& s):
+ children(s.begin(), s.end())
+ {
+ // Children should never be empty. They shouldn't be children.
+ for(vector<Symbols*>::const_iterator it = children.begin(); it!= children.end(); it++)
+ {
+ assert(!(*it)->empty());
+ }
+
+ 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 empty() const {
+ return (found.IsNull() && children.size() == 0);
+ }
+
+
+ };
+
+class SymbolPtrHasher
+{
+public:
+ size_t operator()(const Symbols * n) const
+ {
+ return (size_t) n;
+ }
+ ;
+}; //End of ASTNodeHasher
+
+
+#endif
const ASTNode& rhs = eq[1];
//collect all the vars in the lhs and rhs
- CountOfSymbols count(eq);
+
+ BuildSymbolGraph(eq);
+ CountOfSymbols count(symbol_graph[eq]);
//handle BVPLUS case
const ASTVec& c = lhs.GetChildren();
return output;
} //end of BVSolve_Even()
- bool BVSolver::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
- {
- ASTNodeMap::iterator it;
- if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end())
- {
- if (it->second == var)
- {
- return false;
- }
- }
- if (var == term)
- {
- return true;
- }
+ // This builds a reduced version of a graph, where there
+ // is only a new node if the number of non-array SYMBOLS
+ // in the descendents changes. For example (EXTRACT 0 1 n)
+ // will have the same "Symbols" node as n, because there is
+ // no new symbols are introduced.
+ Symbols* BVSolver::BuildSymbolGraph(const ASTNode& n)
+ {
+ if (symbol_graph.find(n) != symbol_graph.end())
+ {
+ return symbol_graph[n];
+ }
- if (term.isConstant())
- return false;
+ Symbols* node;
+
+ // Note we skip array variables. We never solve for them so
+ // can ignore them.
+ if (n.GetKind() == SYMBOL && n.GetIndexWidth() == 0) {
+ node = new Symbols(n);
+ symbol_graph.insert(make_pair(n, node));
+ return node;
+ }
+
+ vector<Symbols*> children;
+ for (int i = 0; i < n.Degree(); i++) {
+ Symbols* v = BuildSymbolGraph(n[i]);
+ if (!v->empty())
+ children.push_back(v);
+ }
+
+ if (children.size() == 1) {
+ // If there is only a single child with a symbol. Then jump to it.
+ node = children.back();
+ }
+ else
+ node = new Symbols(children);
+
+ symbol_graph.insert(make_pair(n, node));
+
+ return node;
+ }
+
+
+ bool BVSolver::VarSeenInTerm(const ASTNode& var, Symbols* term)
+ {
+ SymbolPtrToNode::iterator it;
+ if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end())
+ {
+ if (it->second == var)
+ {
+ return false;
+ }
+ }
+
+ if (var == term->found)
+ {
+ return true;
+ }
+
+ for (vector<Symbols*>::const_iterator
+ it = term->children.begin(), itend = term->children.end();
+ it != itend; it++)
+ {
+ if (VarSeenInTerm(var, *it))
+ {
+ return true;
+ }
+ }
+
+ TermsAlreadySeenMap[term] = var;
+ return false;
+ }//End of VarSeenInTerm
+
+ bool BVSolver::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
+ {
+ BuildSymbolGraph(term);
+ return VarSeenInTerm(var,symbol_graph[term]);
+ }
- for (ASTVec::const_iterator
- it = term.begin(), itend = term.end();
- it != itend; it++)
- {
- if (VarSeenInTerm(var, *it))
- {
- return true;
- }
- }
- TermsAlreadySeenMap[term] = var;
- return false;
- }//End of VarSeenInTerm
};//end of namespace BEEV
#define BVSOLVER_H
#include "simplifier.h"
+#include "Symbols.h"
namespace BEEV
{
//this map is useful while traversing terms and uniquely
//identifying variables in the those terms. Prevents double
//counting.
- ASTNodeMap TermsAlreadySeenMap;
- //ASTNodeMap TermsAlreadySeenMap_ForArrays;
+ typedef HASHMAP<
+ Symbols*,
+ ASTNode,
+ SymbolPtrHasher
+ > SymbolPtrToNode;
+ SymbolPtrToNode TermsAlreadySeenMap;
+
+ //ASTNodeMap TermsAlreadySeenMap_ForArrays;
//solved variables list: If a variable has been solved for then do
//not solve for it again
//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);
+
//takes an even number "in" as input, and returns an odd number
//(return value) and a power of 2 (as number_shifts by reference),
//else returns FALSE
bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output);
+ typedef HASHMAP<
+ ASTNode,
+ Symbols*,
+ ASTNode::ASTNodeHasher,
+ ASTNode::ASTNodeEqual> ASTNodeToNodes;
+ ASTNodeToNodes symbol_graph;
+
+ Symbols* BuildSymbolGraph(const ASTNode& n);
+
public:
//constructor
BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp)
DoNotSolve_TheseVars.clear();
FormulasAlreadySolvedMap.clear();
//TermsAlreadySeenMap_ForArrays.clear();
+ for (ASTNodeToNodes::iterator it = symbol_graph.begin(); it != symbol_graph.end(); it++)
+ {
+ delete it->second;
+ }
}
//Top Level Solver: Goes over the input DAG, identifies the
projects / francis / stp.git / commitdiff