--- /dev/null
+/*
+ * VariablesInExpression.cpp
+ */
+
+#include "VariablesInExpression.h"
+
+namespace BEEV {
+
+VariablesInExpression::VariablesInExpression() {
+ // TODO Auto-generated constructor stub
+
+}
+
+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();
+
+}
+
+// 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
+// no new symbols are introduced.
+Symbols* VariablesInExpression::BuildSymbolGraph(const ASTNode& n) {
+ if (symbol_graph.find(n) != symbol_graph.end()) {
+ return symbol_graph[n];
+ }
+
+ 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;
+}
+
+// Builds a set of the SYMBOLS that were found under the "term". The symbols are the union of "found" and
+// all the sets : TermsAlreadySeen(av[0]) union ... TermsAlreadySeen(av[n])".
+void VariablesInExpression::VarSeenInTerm(Symbols* term, SymbolPtrSet& visited,
+ ASTNodeSet& found, vector<Symbols*>& av) {
+ if (visited.find(term) != visited.end()) {
+ return;
+ }
+ SymbolPtrToNode::const_iterator it;
+ if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end()) {
+ // We've previously built the set of variables below this "symbols".
+ // It's not added into "found" because its sometimes 70k variables
+ // big, and if there are no other symbols discovered it's a terrible
+ // waste to create a copy of the set. Instead we store (in effect)
+ // a pointer to the set.
+ av.push_back(term);
+ return;
+ }
+
+ if (term->isLeaf()) {
+ found.insert(term->found);
+ return;
+ }
+
+ for (vector<Symbols*>::const_iterator it = term->children.begin(), itend =
+ term->children.end(); it != itend; it++) {
+ VarSeenInTerm(*it, visited, found, av);
+ }
+
+ visited.insert(term);
+ return;
+}//End of VarSeenInTerm
+
+#if 0
+void VariablesInExpression::SetofVarsSeenInTerm(const ASTNode& term, ASTNodeSet& symbols)
+{
+ assert(symbols.size() ==0);
+
+ BuildSymbolGraph(term);
+
+ SymbolPtrSet visited;
+
+ vector<Symbols*> av;
+ VarSeenInTerm(symbol_graph[term],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());
+ }
+
+ if (visited.size() > 50) // No use caching it, unless we've done some work.
+ {
+ TermsAlreadySeenMap.insert(make_pair(symbol_graph[term],symbols));
+ }
+}
+#endif
+
+bool VariablesInExpression::VarSeenInTerm(const ASTNode& var,
+ const ASTNode& term) {
+ // This only returns true if we are searching for variables that aren't arrays.
+ assert(var.GetKind() == SYMBOL && var.GetIndexWidth() == 0);
+ if (term.isConstant())
+ return false;
+
+ BuildSymbolGraph(term);
+
+ SymbolPtrSet visited;
+ ASTNodeSet *symbols = new ASTNodeSet();
+ vector<Symbols*> av;
+ VarSeenInTerm(symbol_graph[term], visited, *symbols, av);
+
+ bool result = (symbols->count(var) != 0);
+
+ //cerr << "visited:" << visited.size() << endl;
+ //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.
+ {
+ for (int i = 0; i < av.size(); i++) {
+ const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second;
+ symbols->insert(sym.begin(), sym.end());
+ }
+ TermsAlreadySeenMap.insert(make_pair(symbol_graph[term], symbols));
+ result = (symbols->count(var) != 0);
+ } else {
+ const int size = av.size();
+ for (int i = 0; i < size; i++) {
+ if (result)
+ break;
+ const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second;
+ result |= (sym.find(var) != sym.end());
+ }
+ delete symbols;
+ }
+ return result;
+}
+
+};
--- /dev/null
+/*
+ * VariablesInExpression.h
+ *
+ * Created on: 27/01/2011
+ * Author: thansen
+ */
+
+#ifndef VARIABLESINEXPRESSION_H_
+#define 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 {
+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);
+
+ //this map is useful while traversing terms and uniquely
+ //identifying variables in the those terms. Prevents double
+ //counting.
+
+ typedef HASHMAP<
+ Symbols*,
+ ASTNodeSet*,
+ SymbolPtrHasher
+ > SymbolPtrToNode;
+ SymbolPtrToNode TermsAlreadySeenMap;
+
+ //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);
+ void VarSeenInTerm(Symbols* term, SymbolPtrSet& visited, ASTNodeSet& found, vector<Symbols*>& av);
+
+ };
+};
+
+
+
+#endif /* VARIABLESINEXPRESSION_H_ */
assert(BVPLUS == lhs.GetKind());
//collect all the vars in the lhs and rhs
- BuildSymbolGraph(eq);
+ vars.BuildSymbolGraph(eq);
//handle BVPLUS case
ASTVec c = FlattenKind(BVPLUS, lhs.GetChildren());
SYMBOL == monom.GetKind()
&& !chosen_symbol
&& !DoNotSolveThis(monom)
- && !VarSeenInTerm(monom,rhs)
+ && !vars.VarSeenInTerm(monom,rhs)
)
||
(
&& SYMBOL == monom[0].GetKind()
&& !chosen_symbol
&& !DoNotSolveThis(monom[0])
- && !VarSeenInTerm(monom[0],rhs)
+ && !vars.VarSeenInTerm(monom[0],rhs)
)
)
{
{
if (it2 == it)
continue;
- if (VarSeenInTerm(var,*it2))
+ if (vars.VarSeenInTerm(var,*it2))
{
duplicated = true;
break;
&& !chosen_symbol
&& !DoNotSolveThis(var)
&& ((SYMBOL == var.GetKind()
- && !VarSeenInTerm(var,rhs)
+ && !vars.VarSeenInTerm(var,rhs)
)
|| (BVEXTRACT == var.GetKind()
&& SYMBOL == var[0].GetKind()
&& BVCONST == var[1].GetKind()
&& zero == var[2]
&& !DoNotSolveThis(var[0])
- && !VarSeenInTerm(var[0],rhs)
+ && !vars.VarSeenInTerm(var[0],rhs)
))
)
{
&& BVCONST == monom[1].GetKind()
&& zero == monom[2]
&& !DoNotSolveThis(monom[0])
- && !VarSeenInTerm(monom[0],rhs)
+ && !vars.VarSeenInTerm(monom[0],rhs)
)
{
outmonom = monom;
&& BVCONST == monom[0][1].GetKind()
&& zero == monom[0][2]
&& !DoNotSolveThis(monom[0][0])
- && !VarSeenInTerm(monom[0][0],rhs)
+ && !vars.VarSeenInTerm(monom[0][0],rhs)
)
{
outmonom = monom;
//input is of the form x = rhs first make sure that the lhs
//symbol does not occur on the rhs or that it has not been
//solved for
- if (!single && VarSeenInTerm(lhs, rhs))
+ if (!single && vars.VarSeenInTerm(lhs, rhs))
{
//found the lhs in the rhs. Abort!
return eq;
if (!(SYMBOL == lhs[0].GetKind()
&& BVCONST == lhs[1].GetKind()
&& zero == lhs[2]
- && !VarSeenInTerm(lhs[0], rhs)
+ && !vars.VarSeenInTerm(lhs[0], rhs)
&& !DoNotSolveThis(lhs[0])))
{
return eq;
}
- if (VarSeenInTerm(lhs[0], rhs))
+ if (vars.VarSeenInTerm(lhs[0], rhs))
{
DoNotSolve_TheseVars.insert(lhs[0]);
return eq;
a, rhs));
//if chosenvar is seen in chosenvar_value then abort
- if (VarSeenInTerm(chosenvar, chosenvar_value))
+ if (vars.VarSeenInTerm(chosenvar, chosenvar_value))
{
//abort solving
DoNotSolve_TheseVars.insert(lhs);
{
if (it2 == symbol_iterator)
continue;
- if (VarSeenInTerm(symbol, *it2))
+ if (vars.VarSeenInTerm(symbol, *it2))
{
duplicated = true;
break;
} //end of BVSolve_Even()
- // 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
- // no new symbols are introduced.
- Symbols* BVSolver::BuildSymbolGraph(const ASTNode& n)
- {
- if (symbol_graph.find(n) != symbol_graph.end())
- {
- return symbol_graph[n];
- }
-
- 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;
- }
-
- // Builds a set of the SYMBOLS that were found under the "term". The symbols are the union of "found" and
- // all the sets : TermsAlreadySeen(av[0]) union ... TermsAlreadySeen(av[n])".
- void BVSolver::VarSeenInTerm(Symbols* term, SymbolPtrSet& visited, ASTNodeSet& found, vector<Symbols*>& av)
- {
- if (visited.find(term) != visited.end())
- {
- return;
- }
- SymbolPtrToNode::const_iterator it;
- if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end())
- {
- // We've previously built the set of variables below this "symbols".
- // It's not added into "found" because its sometimes 70k variables
- // big, and if there are no other symbols discovered it's a terrible
- // waste to create a copy of the set. Instead we store (in effect)
- // a pointer to the set.
- av.push_back(term);
- return;
- }
-
- if (term->isLeaf())
- {
- found.insert(term->found);
- return;
- }
-
- for (vector<Symbols*>::const_iterator
- it = term->children.begin(), itend = term->children.end();
- it != itend; it++)
- {
- VarSeenInTerm(*it,visited,found,av);
- }
-
- visited.insert(term);
- return;
- }//End of VarSeenInTerm
-
-#if 0
- void BVSolver::SetofVarsSeenInTerm(const ASTNode& term, ASTNodeSet& symbols)
- {
- assert(symbols.size() ==0);
-
- BuildSymbolGraph(term);
-
- SymbolPtrSet visited;
-
- vector<Symbols*> av;
- VarSeenInTerm(symbol_graph[term],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());
- }
-
-
- if (visited.size() > 50) // No use caching it, unless we've done some work.
- {
- TermsAlreadySeenMap.insert(make_pair(symbol_graph[term],symbols));
- }
- }
-#endif
-
- bool BVSolver::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
- {
- // This only returns true if we are searching for variables that aren't arrays.
- assert(var.GetKind() == SYMBOL && var.GetIndexWidth() == 0);
- if (term.isConstant())
- return false;
-
- BuildSymbolGraph(term);
-
- SymbolPtrSet visited;
- ASTNodeSet *symbols = new ASTNodeSet();
- vector<Symbols*> av;
- VarSeenInTerm(symbol_graph[term],visited,*symbols,av);
-
- bool result = (symbols->count(var) !=0);
-
- //cerr << "visited:" << visited.size() << endl;
- //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.
- {
- for (int i =0 ; i < av.size();i++)
- {
- const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second;
- symbols->insert(sym.begin(), sym.end());
- }
- TermsAlreadySeenMap.insert(make_pair(symbol_graph[term],symbols));
- result = (symbols->count(var) !=0);
- }
- else
- {
- const int size = av.size();
- for (int i =0 ; i < size;i++)
- {
- if (result)
- break;
- const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second;
- result |= (sym.find(var) !=sym.end());
- }
- delete symbols;
- }
- return result;
- }
};//end of namespace BEEV
#include "simplifier.h"
#include "Symbols.h"
+#include "VariablesInExpression.h"
namespace BEEV
{
ASTNode BVSolve_Even(const ASTNode& eq);
ASTNode CheckEvenEqn(const ASTNode& input, bool& evenflag);
- /////////////////////////
- // 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);
-
- //this map is useful while traversing terms and uniquely
- //identifying variables in the those terms. Prevents double
- //counting.
-
- typedef HASHMAP<
- Symbols*,
- ASTNodeSet*,
- SymbolPtrHasher
- > SymbolPtrToNode;
- SymbolPtrToNode TermsAlreadySeenMap;
-
- //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);
- void VarSeenInTerm(Symbols* term, SymbolPtrSet& visited, ASTNodeSet& found, vector<Symbols*>& av);
-
-
- /////////////////////////
// With this option enabled, it will do it properly. And slowly!!
bool completelySubstitute;
+ VariablesInExpression vars;
+
public:
//constructor
- BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp)
+ BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp)
{
ASTTrue = _bm->CreateNode(TRUE);
ASTFalse = _bm->CreateNode(FALSE);
{
DoNotSolve_TheseVars.clear();
FormulasAlreadySolvedMap.clear();
- 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();
+ //TermsAlreadySeenMap.clear();
} //End of ClearAllTables()
projects / francis / stp.git / commitdiff