/*! \file dagification_visitor.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Paul Meng, Andrew Reynolds
+ ** Morgan Deters, Andres Noetzli, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
#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);
}
}
bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
+ Kind ck = current.getKind();
+ if (current.isClosure())
+ {
+ // 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
// for all subexpressions, so it isn't useful to traverse and
// increment again (they'll be dagified anyway).
- return current.isVar() ||
- current.getMetaKind() == kind::metakind::CONSTANT ||
- current.getNumChildren()==0 ||
- ( ( current.getKind() == kind::NOT ||
- current.getKind() == kind::UMINUS ) &&
- ( current[0].isVar() ||
- current[0].getMetaKind() == kind::metakind::CONSTANT ) ) ||
- current.getKind() == kind::SORT_TYPE ||
- d_nodeCount[current] > d_threshold;
+ return current.isVar() || current.getMetaKind() == kind::metakind::CONSTANT
+ || current.getNumChildren() == 0
+ || ((ck == kind::NOT || ck == kind::UMINUS)
+ && (current[0].isVar()
+ || current[0].getMetaKind() == kind::metakind::CONSTANT))
+ || ck == kind::SORT_TYPE || d_nodeCount[current] > d_threshold;
}
void DagificationVisitor::visit(TNode current, TNode parent) {
TNode& uniqueParent = d_uniqueParent[current];
- if(!uniqueParent.isNull() && uniqueParent != parent) {
+ // We restrict this optimization to nodes with arity 1 since otherwise we
+ // may run into issues with tree traverals. Without this restriction
+ // dumping regress3/pp-regfile increases the file size by a factor of 5000.
+ if (!uniqueParent.isNull()
+ && (uniqueParent != parent || parent.getNumChildren() > 1))
+ {
// there is not a unique parent for this expr, mark it
uniqueParent = TNode::null();
}
}
void DagificationVisitor::start(TNode node) {
- AlwaysAssert(!d_done, "DagificationVisitor cannot be re-used");
+ AlwaysAssert(!d_done) << "DagificationVisitor cannot be re-used";
d_top = 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
Node n = d_substitutions->apply(*i);
- Assert(! d_substitutions->hasSubstitution(n));
+ Assert(!d_substitutions->hasSubstitution(n));
d_substitutions->addSubstitution(n, letvar);
}
}
const theory::SubstitutionMap& DagificationVisitor::getLets() {
- AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
+ AlwaysAssert(d_done)
+ << "DagificationVisitor must be used as a visitor before "
+ "getting the dagified version out!";
return *d_substitutions;
}
Node DagificationVisitor::getDagifiedBody() {
- AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
+ AlwaysAssert(d_done)
+ << "DagificationVisitor must be used as a visitor before "
+ "getting the dagified version out!";
#ifdef CVC4_TRACING
# ifdef CVC4_DEBUG
projects / cvc5.git / blobdiff