From 2f36da3428bcfff0d79c31b8726fd0d938355636 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 27 Jan 2011 02:38:19 +0000 Subject: [PATCH] Refactor. Split out the code to determine which variables are contained in an expression. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1094 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/VariablesInExpression.cpp | 168 ++++++++++++++++++++++ src/simplifier/VariablesInExpression.h | 62 ++++++++ src/simplifier/bvsolver.cpp | 174 ++--------------------- src/simplifier/bvsolver.h | 53 +------ 4 files changed, 248 insertions(+), 209 deletions(-) create mode 100644 src/simplifier/VariablesInExpression.cpp create mode 100644 src/simplifier/VariablesInExpression.h diff --git a/src/simplifier/VariablesInExpression.cpp b/src/simplifier/VariablesInExpression.cpp new file mode 100644 index 0000000..bf00316 --- /dev/null +++ b/src/simplifier/VariablesInExpression.cpp @@ -0,0 +1,168 @@ +/* + * VariablesInExpression.cpp + */ + +#include "VariablesInExpression.h" + +namespace BEEV { + +VariablesInExpression::VariablesInExpression() { + // TODO Auto-generated constructor stub + +} + +VariablesInExpression::~VariablesInExpression() { + set 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 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& 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::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 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 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; +} + +}; diff --git a/src/simplifier/VariablesInExpression.h b/src/simplifier/VariablesInExpression.h new file mode 100644 index 0000000..24aff63 --- /dev/null +++ b/src/simplifier/VariablesInExpression.h @@ -0,0 +1,62 @@ +/* + * 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 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& av); + + }; +}; + + + +#endif /* VARIABLESINEXPRESSION_H_ */ diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index a5509bd..ec6c7c5 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -97,7 +97,7 @@ namespace BEEV 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()); @@ -114,7 +114,7 @@ namespace BEEV SYMBOL == monom.GetKind() && !chosen_symbol && !DoNotSolveThis(monom) - && !VarSeenInTerm(monom,rhs) + && !vars.VarSeenInTerm(monom,rhs) ) || ( @@ -122,7 +122,7 @@ namespace BEEV && SYMBOL == monom[0].GetKind() && !chosen_symbol && !DoNotSolveThis(monom[0]) - && !VarSeenInTerm(monom[0],rhs) + && !vars.VarSeenInTerm(monom[0],rhs) ) ) { @@ -135,7 +135,7 @@ namespace BEEV { if (it2 == it) continue; - if (VarSeenInTerm(var,*it2)) + if (vars.VarSeenInTerm(var,*it2)) { duplicated = true; break; @@ -174,14 +174,14 @@ namespace BEEV && !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) )) ) { @@ -196,7 +196,7 @@ namespace BEEV && BVCONST == monom[1].GetKind() && zero == monom[2] && !DoNotSolveThis(monom[0]) - && !VarSeenInTerm(monom[0],rhs) + && !vars.VarSeenInTerm(monom[0],rhs) ) { outmonom = monom; @@ -210,7 +210,7 @@ namespace BEEV && 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; @@ -324,7 +324,7 @@ namespace BEEV //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; @@ -371,13 +371,13 @@ namespace BEEV 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; @@ -442,7 +442,7 @@ namespace BEEV 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); @@ -578,7 +578,7 @@ namespace BEEV { if (it2 == symbol_iterator) continue; - if (VarSeenInTerm(symbol, *it2)) + if (vars.VarSeenInTerm(symbol, *it2)) { duplicated = true; break; @@ -1065,154 +1065,6 @@ namespace BEEV } //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 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& 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::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 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 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 diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h index 981126f..8aba032 100644 --- a/src/simplifier/bvsolver.h +++ b/src/simplifier/bvsolver.h @@ -12,6 +12,7 @@ #include "simplifier.h" #include "Symbols.h" +#include "VariablesInExpression.h" namespace BEEV { @@ -71,38 +72,6 @@ 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 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& av); - - - ///////////////////////// @@ -149,9 +118,11 @@ namespace BEEV // 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); @@ -172,21 +143,7 @@ namespace BEEV { DoNotSolve_TheseVars.clear(); FormulasAlreadySolvedMap.clear(); - set 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() -- 2.47.3