From: Andrew Reynolds Date: Wed, 2 Dec 2020 22:09:28 +0000 (-0600) Subject: Remove dagification visitor (#5574) X-Git-Tag: cvc5-1.0.0~2518 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=768157d3bf78337a603004a2a47026ecf1b70612;p=cvc5.git Remove dagification visitor (#5574) This has fully been replaced by the new let binding. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e56379f0c..4b5c37d9e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -122,8 +122,6 @@ libcvc4_add_sources( printer/ast/ast_printer.h printer/cvc/cvc_printer.cpp printer/cvc/cvc_printer.h - printer/dagification_visitor.cpp - printer/dagification_visitor.h printer/let_binding.cpp printer/let_binding.h printer/printer.cpp diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp deleted file mode 100644 index 89fbe786d..000000000 --- a/src/printer/dagification_visitor.cpp +++ /dev/null @@ -1,208 +0,0 @@ -/********************* */ -/*! \file dagification_visitor.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Mathias Preiner - ** This file is part of the CVC4 project. - ** 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 - ** - ** \brief Implementation of a dagifier for CVC4 expressions - ** - ** Implementation of a dagifier for CVC4 expressions. - **/ - -#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 - -namespace CVC4 { -namespace printer { - -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); -} - -DagificationVisitor::~DagificationVisitor() { - delete d_substitutions; - delete d_context; -} - -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 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 - || ((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) { - -#ifdef CVC4_TRACING -# ifdef CVC4_DEBUG - // turn off dagification for Debug stream while we're doing this work - Node::dag::Scope scopeDebug(Debug.getStream(), false); -# endif /* CVC4_DEBUG */ - // turn off dagification for Trace stream while we're doing this work - Node::dag::Scope scopeTrace(Trace.getStream(), false); -#endif /* CVC4_TRACING */ - - if(d_uniqueParent.find(current) != d_uniqueParent.end()) { - // we've seen this expr before - - TNode& uniqueParent = d_uniqueParent[current]; - - // 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(); - } - - // increase the count - const unsigned count = ++d_nodeCount[current]; - - if(count > d_threshold) { - // candidate for a let binder - d_substNodes.push_back(current); - } - } else { - // we haven't seen this expr before - Assert(d_nodeCount[current] == 0); - d_nodeCount[current] = 1; - d_uniqueParent[current] = parent; - } -} - -void DagificationVisitor::start(TNode node) { - AlwaysAssert(!d_done) << "DagificationVisitor cannot be re-used"; - d_top = node; -} - -void DagificationVisitor::done(TNode node) { - AlwaysAssert(!d_done); - - d_done = true; - -#ifdef CVC4_TRACING -# ifdef CVC4_DEBUG - // turn off dagification for Debug stream while we're doing this work - Node::dag::Scope scopeDebug(Debug.getStream(), false); -# endif /* CVC4_DEBUG */ - // turn off dagification for Trace stream while we're doing this work - Node::dag::Scope scopeTrace(Trace.getStream(), false); -#endif /* CVC4_TRACING */ - - // letify subexprs before parents (cascading LETs) - std::sort(d_substNodes.begin(), d_substNodes.end()); - - for(std::vector::iterator i = d_substNodes.begin(); - i != d_substNodes.end(); - ++i) { - Assert(d_nodeCount[*i] > d_threshold); - TNode parent = d_uniqueParent[*i]; - if(!parent.isNull() && d_nodeCount[parent] > d_threshold) { - // no need to letify this expr, because it only occurs in - // a single super-expression, and that one will be letified - continue; - } - - // construct the let binder - std::stringstream ss; - 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)); - 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!"; - return *d_substitutions; -} - -Node DagificationVisitor::getDagifiedBody() { - AlwaysAssert(d_done) - << "DagificationVisitor must be used as a visitor before " - "getting the dagified version out!"; - -#ifdef CVC4_TRACING -# ifdef CVC4_DEBUG - // turn off dagification for Debug stream while we're doing this work - Node::dag::Scope scopeDebug(Debug.getStream(), false); -# endif /* CVC4_DEBUG */ - // turn off dagification for Trace stream while we're doing this work - Node::dag::Scope scopeTrace(Trace.getStream(), false); -#endif /* CVC4_TRACING */ - - return d_substitutions->apply(d_top); -} - -}/* CVC4::printer namespace */ -}/* CVC4 namespace */ diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h deleted file mode 100644 index 7c6f57af8..000000000 --- a/src/printer/dagification_visitor.h +++ /dev/null @@ -1,185 +0,0 @@ -/********************* */ -/*! \file dagification_visitor.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Mathias Preiner - ** This file is part of the CVC4 project. - ** 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 - ** - ** \brief A dagifier for CVC4 expressions - ** - ** A dagifier for CVC4 expressions. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__PRINTER__DAGIFICATION_VISITOR_H -#define CVC4__PRINTER__DAGIFICATION_VISITOR_H - -#include -#include -#include -#include - -#include "expr/node.h" -#include "util/hash.h" - -namespace CVC4 { - -namespace context { - class Context; -}/* CVC4::context namespace */ - -namespace theory { - class SubstitutionMap; -}/* CVC4::theory namespace */ - -namespace printer { - -/** - * This is a visitor class (intended to be used with CVC4's NodeVisitor) - * that visits an expression looking for common subexpressions that appear - * more than N times, where N is a configurable threshold. Afterward, - * let bindings can be extracted from this visitor and applied to the - * expression. - * - * This dagifier never introduces let bindings for variables, constants, - * unary-minus exprs over variables or constants, or NOT exprs over - * variables or constants. This dagifier never introduces let bindings - * for types. - */ -class DagificationVisitor { - - /** - * The threshold for dagification. Subexprs occurring more than this - * number of times are dagified. - */ - const unsigned d_threshold; - - /** - * The prefix for introduced let bindings. - */ - const std::string d_letVarPrefix; - - /** - * A map of subexprs to their occurrence count. - */ - std::unordered_map d_nodeCount; - - /** - * The set of variable names with the let prefix that appear in the - * expression. - */ - std::unordered_set d_reservedLetNames; - - /** - * The top-most node we are visiting. - */ - TNode d_top; - - /** - * This class doesn't operate in a context-dependent fashion, but - * SubstitutionMap does, so we need a context. - */ - context::Context* d_context; - - /** - * A map of subexprs to their newly-introduced let bindings. - */ - theory::SubstitutionMap* d_substitutions; - - /** - * The current count of let bindings. Used to build unique names - * for the bindings. - */ - unsigned d_letVar; - - /** - * Keep track of whether we are done yet (for assertions---this visitor - * can only be used one time). - */ - bool d_done; - - /** - * If a subexpr occurs uniquely in one parent expr, this map points to - * it. An expr not occurring as a key in this map means we haven't - * seen it yet (and its occurrence count should be zero). If an expr - * points to the null expr in this map, it means we've seen more than - * one parent, so the subexpr doesn't have a unique parent. - * - * This information is kept because if a subexpr occurs more than the - * threshold, it is normally subject to dagification. But if it occurs - * only in one unique parent expression, and the parent meets the - * threshold too, then the parent will be dagified and there's no point - * in independently dagifying the child. (If it is beyond the threshold - * and occurs in more than one parent, we'll independently dagify.) - */ - std::unordered_map d_uniqueParent; - - /** - * A list of all nodes that meet the occurrence threshold and therefore - * *may* be subject to dagification, except for the unique-parent rule - * mentioned above. - */ - std::vector d_substNodes; - -public: - - /** Our visitor doesn't return anything. */ - typedef void return_type; - - /** - * Construct a dagification visitor with the given threshold and let - * binding prefix. - * - * @param threshold the threshold to apply for dagification (must be > 0) - * @param letVarPrefix prefix for let bindings (by default, "_let_") - */ - DagificationVisitor(unsigned threshold, std::string letVarPrefix = "_let_"); - - /** - * Simple destructor, clean up memory. - */ - ~DagificationVisitor(); - - /** - * Returns true if "current" has already been visited a sufficient - * number of times to make it a candidate for dagification, or if - * it cannot ever be subject to dagification. - */ - bool alreadyVisited(TNode current, TNode parent); - - /** - * Visit the expr "current", it might be a candidate for a let binder. - */ - void visit(TNode current, TNode parent); - - /** - * Marks the node as the starting literal. - */ - void start(TNode node); - - /** - * Called when we're done with all visitation. Does postprocessing. - */ - void done(TNode node); - - /** - * Get the let substitutions. - */ - const theory::SubstitutionMap& getLets(); - - /** - * Return the let-substituted expression. - */ - Node getDagifiedBody(); - -};/* class DagificationVisitor */ - -}/* CVC4::printer namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__PRINTER__DAGIFICATION_VISITOR_H */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index d3e9b48e4..6f03553ae 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -30,7 +30,6 @@ #include "options/language.h" #include "options/printer_options.h" #include "options/smt_options.h" -#include "printer/dagification_visitor.h" #include "printer/let_binding.h" #include "proof/unsat_core.h" #include "smt/command.h"