diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/node_algorithm.cpp | 32 | ||||
-rw-r--r-- | src/expr/node_algorithm.h | 8 | ||||
-rw-r--r-- | src/printer/dagification_visitor.cpp | 54 | ||||
-rw-r--r-- | src/printer/dagification_visitor.h | 7 |
4 files changed, 88 insertions, 13 deletions
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 25ffb0778..841f9ea28 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -236,6 +236,38 @@ bool getFreeVariables(TNode n, return !fvs.empty(); } +bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs) +{ + std::unordered_set<TNode, TNodeHashFunction> visited; + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + std::unordered_set<TNode, TNodeHashFunction>::iterator itv = + visited.find(cur); + if (itv == visited.end()) + { + if (cur.isVar()) + { + vs.insert(cur); + } + else + { + for (const TNode& cn : cur) + { + visit.push_back(cn); + } + } + visited.insert(cur); + } + } while (!visit.empty()); + + return !vs.empty(); +} + void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms) { std::unordered_set<TNode, TNodeHashFunction> visited; diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 656f162ae..727f5ba75 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -73,6 +73,14 @@ bool getFreeVariables(TNode n, bool computeFv = true); /** + * Get all variables in n. + * @param n The node under investigation + * @param vs The set which free variables are added to + * @return true iff this node contains a free variable. + */ +bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs); + +/** * For term n, this function collects the symbols that occur as a subterms * of n. A symbol is a variable that does not have kind BOUND_VARIABLE. * @param n The node under investigation diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index cf5f35457..a024c97a7 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -17,6 +17,8 @@ #include "printer/dagification_visitor.h" #include "context/context.h" +#include "expr/node_algorithm.h" +#include "expr/node_manager_attributes.h" #include "theory/substitutions.h" #include <sstream> @@ -24,18 +26,20 @@ namespace CVC4 { namespace printer { -DagificationVisitor::DagificationVisitor(unsigned threshold, std::string letVarPrefix) : - d_threshold(threshold), - d_letVarPrefix(letVarPrefix), - d_nodeCount(), - d_top(), - d_context(new context::Context()), - d_substitutions(new theory::SubstitutionMap(d_context)), - d_letVar(0), - d_done(false), - d_uniqueParent(), - d_substNodes() { - +DagificationVisitor::DagificationVisitor(unsigned threshold, + std::string letVarPrefix) + : d_threshold(threshold), + d_letVarPrefix(letVarPrefix), + d_nodeCount(), + d_reservedLetNames(), + d_top(), + d_context(new context::Context()), + d_substitutions(new theory::SubstitutionMap(d_context)), + d_letVar(0), + d_done(false), + d_uniqueParent(), + d_substNodes() +{ // 0 doesn't make sense AlwaysAssertArgument(threshold > 0, threshold); } @@ -51,8 +55,28 @@ bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) { { // for quantifiers, we visit them but we don't recurse on them visit(current, parent); + + // search for variables that start with the let prefix + std::unordered_set<TNode, TNodeHashFunction> vs; + expr::getVariables(current, vs); + for (const TNode v : vs) + { + const std::string name = v.getAttribute(expr::VarNameAttr()); + if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0) + { + d_reservedLetNames.insert(name); + } + } return true; } + else if (current.isVar()) + { + const std::string name = current.getAttribute(expr::VarNameAttr()); + if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0) + { + d_reservedLetNames.insert(name); + } + } // don't visit variables, constants, or those exprs that we've // already seen more than the threshold: if we've increased // the count beyond the threshold already, we've done the same @@ -137,7 +161,11 @@ void DagificationVisitor::done(TNode node) { // construct the let binder std::stringstream ss; - ss << d_letVarPrefix << d_letVar++; + do + { + ss.str(""); + ss << d_letVarPrefix << d_letVar++; + } while (d_reservedLetNames.find(ss.str()) != d_reservedLetNames.end()); Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME); // apply previous substitutions to the rhs, enabling cascading LETs diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h index 18f31e662..6df5f32b4 100644 --- a/src/printer/dagification_visitor.h +++ b/src/printer/dagification_visitor.h @@ -21,6 +21,7 @@ #include <string> #include <unordered_map> +#include <unordered_set> #include <vector> #include "expr/node.h" @@ -69,6 +70,12 @@ class DagificationVisitor { std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount; /** + * The set of variable names with the let prefix that appear in the + * expression. + */ + std::unordered_set<std::string> d_reservedLetNames; + + /** * The top-most node we are visiting. */ TNode d_top; |