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;
std::unordered_set<Node, NodeHashFunction>& fvs,
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.
#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>
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);
}
{
// 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
// 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
--- /dev/null
+; COMMAND-LINE: --dump raw-benchmark --preprocess-only
+; SCRUBBER: grep assert
+; EXPECT: (assert (let ((_let_1 (* x y))) (= _let_1 _let_1 _let_0)))
+; EXPECT: (assert (let ((_let_1 (and a b))) (= _let_1 _let_1 (forall ((_let_0 Int)) (= 0 _let_0) ))))
+; EXPECT: (assert (let ((_let_1 (and a b))) (= _let_1 _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0))) ) ))))
+(set-logic NIA)
+(declare-const _let_0 Int)
+(declare-const x Int)
+(declare-const y Int)
+(declare-const a Bool)
+(declare-const b Bool)
+(assert (= (* x y) (* x y) _let_0))
+(assert (= (and a b) (and a b) (forall ((_let_0 Int)) (= 0 _let_0))))
+(assert (= (and a b) (and a b) (forall ((x Int)) (forall ((y Int)) (and (and a b) (and b a) (and b a) (= 0 _let_0))))))
+(check-sat)