We are changing our policy on how expand definitions is handled during preprocessing.
This will require some additions to expand definitions handling. This PR makes a standalone module for expanding definitions.
smt/dump.h
smt/dump_manager.cpp
smt/dump_manager.h
+ smt/expand_definitions.cpp
+ smt/expand_definitions.h
smt/listeners.cpp
smt/listeners.h
smt/logic_exception.h
--- /dev/null
+/********************* */
+/*! \file expand_definitions.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Tim King, Haniel Barbosa
+ ** 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 expand definitions for an SMT engine.
+ **/
+
+#include "smt/expand_definitions.h"
+
+#include <stack>
+#include <utility>
+
+#include "expr/node_manager_attributes.h"
+#include "smt/defined_function.h"
+#include "smt/smt_engine.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4::preprocessing;
+using namespace CVC4::theory;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace smt {
+
+ExpandDefs::ExpandDefs(SmtEngine& smt,
+ ResourceManager& rm,
+ SmtEngineStatistics& stats)
+ : d_smt(smt), d_resourceManager(rm), d_smtStats(stats)
+{
+}
+
+ExpandDefs::~ExpandDefs() {}
+
+Node ExpandDefs::expandDefinitions(
+ TNode n,
+ std::unordered_map<Node, Node, NodeHashFunction>& cache,
+ bool expandOnly)
+{
+ NodeManager* nm = d_smt.getNodeManager();
+ std::stack<std::tuple<Node, Node, bool>> worklist;
+ std::stack<Node> result;
+ worklist.push(std::make_tuple(Node(n), Node(n), false));
+ // The worklist is made of triples, each is input / original node then the
+ // output / rewritten node and finally a flag tracking whether the children
+ // have been explored (i.e. if this is a downward or upward pass).
+
+ do
+ {
+ d_resourceManager.spendResource(ResourceManager::Resource::PreprocessStep);
+
+ // n is the input / original
+ // node is the output / result
+ Node node;
+ bool childrenPushed;
+ std::tie(n, node, childrenPushed) = worklist.top();
+ worklist.pop();
+
+ // Working downwards
+ if (!childrenPushed)
+ {
+ Kind k = n.getKind();
+
+ // we can short circuit (variable) leaves
+ if (n.isVar())
+ {
+ SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
+ SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n);
+ if (i != dfuns->end())
+ {
+ Node f = (*i).second.getFormula();
+ // must expand its definition
+ Node fe = expandDefinitions(f, cache, expandOnly);
+ // replacement must be closed
+ if ((*i).second.getFormals().size() > 0)
+ {
+ result.push(
+ nm->mkNode(LAMBDA,
+ nm->mkNode(BOUND_VAR_LIST, (*i).second.getFormals()),
+ fe));
+ continue;
+ }
+ // don't bother putting in the cache
+ result.push(fe);
+ continue;
+ }
+ // don't bother putting in the cache
+ result.push(n);
+ continue;
+ }
+
+ // maybe it's in the cache
+ std::unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit =
+ cache.find(n);
+ if (cacheHit != cache.end())
+ {
+ TNode ret = (*cacheHit).second;
+ result.push(ret.isNull() ? n : ret);
+ continue;
+ }
+
+ // otherwise expand it
+ bool doExpand = false;
+ if (k == APPLY_UF)
+ {
+ // Always do beta-reduction here. The reason is that there may be
+ // operators such as INTS_MODULUS in the body of the lambda that would
+ // otherwise be introduced by beta-reduction via the rewriter, but are
+ // not expanded here since the traversal in this function does not
+ // traverse the operators of nodes. Hence, we beta-reduce here to
+ // ensure terms in the body of the lambda are expanded during this
+ // call.
+ if (n.getOperator().getKind() == LAMBDA)
+ {
+ doExpand = true;
+ }
+ else
+ {
+ // We always check if this operator corresponds to a defined function.
+ doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr());
+ }
+ }
+ if (doExpand)
+ {
+ std::vector<Node> formals;
+ TNode fm;
+ if (n.getOperator().getKind() == LAMBDA)
+ {
+ TNode op = n.getOperator();
+ // lambda
+ for (unsigned i = 0; i < op[0].getNumChildren(); i++)
+ {
+ formals.push_back(op[0][i]);
+ }
+ fm = op[1];
+ }
+ else
+ {
+ // application of a user-defined symbol
+ TNode func = n.getOperator();
+ SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
+ SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func);
+ if (i == dfuns->end())
+ {
+ throw TypeCheckingException(
+ n.toExpr(),
+ std::string("Undefined function: `") + func.toString() + "'");
+ }
+ DefinedFunction def = (*i).second;
+ formals = def.getFormals();
+
+ if (Debug.isOn("expand"))
+ {
+ Debug("expand") << "found: " << n << std::endl;
+ Debug("expand") << " func: " << func << std::endl;
+ std::string name = func.getAttribute(expr::VarNameAttr());
+ Debug("expand") << " : \"" << name << "\"" << std::endl;
+ }
+ if (Debug.isOn("expand"))
+ {
+ Debug("expand") << " defn: " << def.getFunction() << std::endl
+ << " [";
+ if (formals.size() > 0)
+ {
+ copy(formals.begin(),
+ formals.end() - 1,
+ std::ostream_iterator<Node>(Debug("expand"), ", "));
+ Debug("expand") << formals.back();
+ }
+ Debug("expand")
+ << "]" << std::endl
+ << " " << def.getFunction().getType() << std::endl
+ << " " << def.getFormula() << std::endl;
+ }
+
+ fm = def.getFormula();
+ }
+
+ Node instance = fm.substitute(formals.begin(),
+ formals.end(),
+ n.begin(),
+ n.begin() + formals.size());
+ Debug("expand") << "made : " << instance << std::endl;
+
+ Node expanded = expandDefinitions(instance, cache, expandOnly);
+ cache[n] = (n == expanded ? Node::null() : expanded);
+ result.push(expanded);
+ continue;
+ }
+ else if (!expandOnly)
+ {
+ // do not do any theory stuff if expandOnly is true
+
+ theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node);
+
+ Assert(t != NULL);
+ TrustNode trn = t->expandDefinition(n);
+ node = trn.isNull() ? Node(n) : trn.getNode();
+ }
+
+ // the partial functions can fall through, in which case we still
+ // consider their children
+ worklist.push(std::make_tuple(
+ Node(n), node, true)); // Original and rewritten result
+
+ for (size_t i = 0; i < node.getNumChildren(); ++i)
+ {
+ worklist.push(
+ std::make_tuple(node[i],
+ node[i],
+ false)); // Rewrite the children of the result only
+ }
+ }
+ else
+ {
+ // Working upwards
+ // Reconstruct the node from it's (now rewritten) children on the stack
+
+ Debug("expand") << "cons : " << node << std::endl;
+ if (node.getNumChildren() > 0)
+ {
+ // cout << "cons : " << node << std::endl;
+ NodeBuilder<> nb(node.getKind());
+ if (node.getMetaKind() == metakind::PARAMETERIZED)
+ {
+ Debug("expand") << "op : " << node.getOperator() << std::endl;
+ // cout << "op : " << node.getOperator() << std::endl;
+ nb << node.getOperator();
+ }
+ for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; ++i)
+ {
+ Assert(!result.empty());
+ Node expanded = result.top();
+ result.pop();
+ // cout << "exchld : " << expanded << std::endl;
+ Debug("expand") << "exchld : " << expanded << std::endl;
+ nb << expanded;
+ }
+ node = nb;
+ }
+ // Only cache once all subterms are expanded
+ cache[n] = n == node ? Node::null() : node;
+ result.push(node);
+ }
+ } while (!worklist.empty());
+
+ AlwaysAssert(result.size() == 1);
+
+ return result.top();
+}
+
+void ExpandDefs::expandAssertions(AssertionPipeline& assertions,
+ bool expandOnly)
+{
+ Chat() << "expanding definitions in assertions..." << std::endl;
+ Trace("simplify") << "ExpandDefs::simplify(): expanding definitions"
+ << std::endl;
+ TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime);
+ std::unordered_map<Node, Node, NodeHashFunction> cache;
+ for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
+ {
+ Node assert = assertions[i];
+ Node expd = expandDefinitions(assert, cache, expandOnly);
+ if (expd != assert)
+ {
+ assertions.replace(i, expd);
+ }
+ }
+}
+
+} // namespace smt
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file process_assertions.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Tim King, Morgan Deters
+ ** 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 The module for processing assertions for an SMT engine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__EXPAND_DEFINITIONS_H
+#define CVC4__SMT__EXPAND_DEFINITIONS_H
+
+#include <unordered_map>
+
+#include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "smt/smt_engine_stats.h"
+#include "util/resource_manager.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+/**
+ * Module in charge of expanding definitions for an SMT engine.
+ *
+ * Its main features is expandDefinitions(TNode, ...), which returns the
+ * expanded formula of a term.
+ */
+class ExpandDefs
+{
+ public:
+ ExpandDefs(SmtEngine& smt, ResourceManager& rm, SmtEngineStatistics& stats);
+ ~ExpandDefs();
+ /**
+ * Expand definitions in term n. Return the expanded form of n.
+ *
+ * @param n The node to expand
+ * @param cache Cache of previous results
+ * @param expandOnly if true, then the expandDefinitions function of
+ * TheoryEngine is not called on subterms of n.
+ * @return The expanded term.
+ */
+ Node expandDefinitions(
+ TNode n,
+ std::unordered_map<Node, Node, NodeHashFunction>& cache,
+ bool expandOnly = false);
+ /**
+ * Expand defintitions in assertions. This applies this above method to each
+ * assertion in the given pipeline.
+ */
+ void expandAssertions(preprocessing::AssertionPipeline& assertions,
+ bool expandOnly = false);
+
+ private:
+ /** Reference to the SMT engine */
+ SmtEngine& d_smt;
+ /** Reference to resource manager */
+ ResourceManager& d_resourceManager;
+ /** Reference to the SMT stats */
+ SmtEngineStatistics& d_smtStats;
+};
+
+} // namespace smt
+} // namespace CVC4
+
+#endif
d_absValues(abs),
d_propagator(true, true),
d_assertionsProcessed(u, false),
- d_processor(smt, *smt.getResourceManager(), stats),
+ d_exDefs(smt, *smt.getResourceManager(), stats),
+ d_processor(smt, d_exDefs, *smt.getResourceManager(), stats),
d_rtf(u),
d_pnm(nullptr)
{
Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly)
{
std::unordered_map<Node, Node, NodeHashFunction> cache;
- return expandDefinitions(n, cache, expandOnly);
+ return d_exDefs.expandDefinitions(n, cache, expandOnly);
}
Node Preprocessor::expandDefinitions(
n.getType(true);
}
// expand only = true
- return d_processor.expandDefinitions(n, cache, expandOnly);
+ return d_exDefs.expandDefinitions(n, cache, expandOnly);
}
Node Preprocessor::simplify(const Node& node, bool removeItes)
nas.getType(true);
}
std::unordered_map<Node, Node, NodeHashFunction> cache;
- Node n = d_processor.expandDefinitions(nas, cache);
+ Node n = d_exDefs.expandDefinitions(nas, cache);
TrustNode ts = d_ppContext->getTopLevelSubstitutions().apply(n);
Node ns = ts.isNull() ? n : ts.getNode();
if (removeItes)
#include <vector>
#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/expand_definitions.h"
#include "smt/process_assertions.h"
#include "smt/term_formula_removal.h"
#include "theory/booleans/circuit_propagator.h"
context::CDO<bool> d_assertionsProcessed;
/** The preprocessing pass context */
std::unique_ptr<preprocessing::PreprocessingPassContext> d_ppContext;
+ /** Expand definitions module, responsible for expanding definitions */
+ ExpandDefs d_exDefs;
/**
* Process assertions module, responsible for implementing the preprocessing
* passes.
};
ProcessAssertions::ProcessAssertions(SmtEngine& smt,
+ ExpandDefs& exDefs,
ResourceManager& rm,
SmtEngineStatistics& stats)
: d_smt(smt),
+ d_exDefs(exDefs),
d_resourceManager(rm),
d_smtStats(stats),
d_preprocessingPassContext(nullptr)
<< "ProcessAssertions::processAssertions() : pre-definition-expansion"
<< endl;
dumpAssertions("pre-definition-expansion", assertions);
- {
- Chat() << "expanding definitions..." << endl;
- Trace("simplify") << "ProcessAssertions::simplify(): expanding definitions"
- << endl;
- TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime);
- unordered_map<Node, Node, NodeHashFunction> cache;
- for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
- {
- Node expd = expandDefinitions(assertions[i], cache);
- if (expd != assertions[i])
- {
- assertions.replace(i, expd);
- }
- }
- }
+ d_exDefs.expandAssertions(assertions, false);
Trace("smt-proc")
<< "ProcessAssertions::processAssertions() : post-definition-expansion"
<< endl;
}
}
-Node ProcessAssertions::expandDefinitions(
- TNode n,
- unordered_map<Node, Node, NodeHashFunction>& cache,
- bool expandOnly)
-{
- NodeManager* nm = d_smt.getNodeManager();
- std::stack<std::tuple<Node, Node, bool>> worklist;
- std::stack<Node> result;
- worklist.push(std::make_tuple(Node(n), Node(n), false));
- // The worklist is made of triples, each is input / original node then the
- // output / rewritten node and finally a flag tracking whether the children
- // have been explored (i.e. if this is a downward or upward pass).
-
- do
- {
- spendResource(ResourceManager::Resource::PreprocessStep);
-
- // n is the input / original
- // node is the output / result
- Node node;
- bool childrenPushed;
- std::tie(n, node, childrenPushed) = worklist.top();
- worklist.pop();
-
- // Working downwards
- if (!childrenPushed)
- {
- Kind k = n.getKind();
-
- // we can short circuit (variable) leaves
- if (n.isVar())
- {
- SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
- SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n);
- if (i != dfuns->end())
- {
- Node f = (*i).second.getFormula();
- // must expand its definition
- Node fe = expandDefinitions(f, cache, expandOnly);
- // replacement must be closed
- if ((*i).second.getFormals().size() > 0)
- {
- result.push(
- nm->mkNode(LAMBDA,
- nm->mkNode(BOUND_VAR_LIST, (*i).second.getFormals()),
- fe));
- continue;
- }
- // don't bother putting in the cache
- result.push(fe);
- continue;
- }
- // don't bother putting in the cache
- result.push(n);
- continue;
- }
-
- // maybe it's in the cache
- unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit =
- cache.find(n);
- if (cacheHit != cache.end())
- {
- TNode ret = (*cacheHit).second;
- result.push(ret.isNull() ? n : ret);
- continue;
- }
-
- // otherwise expand it
- bool doExpand = false;
- if (k == APPLY_UF)
- {
- // Always do beta-reduction here. The reason is that there may be
- // operators such as INTS_MODULUS in the body of the lambda that would
- // otherwise be introduced by beta-reduction via the rewriter, but are
- // not expanded here since the traversal in this function does not
- // traverse the operators of nodes. Hence, we beta-reduce here to
- // ensure terms in the body of the lambda are expanded during this
- // call.
- if (n.getOperator().getKind() == LAMBDA)
- {
- doExpand = true;
- }
- else
- {
- // We always check if this operator corresponds to a defined function.
- doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr());
- }
- }
- if (doExpand)
- {
- vector<Node> formals;
- TNode fm;
- if (n.getOperator().getKind() == LAMBDA)
- {
- TNode op = n.getOperator();
- // lambda
- for (unsigned i = 0; i < op[0].getNumChildren(); i++)
- {
- formals.push_back(op[0][i]);
- }
- fm = op[1];
- }
- else
- {
- // application of a user-defined symbol
- TNode func = n.getOperator();
- SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
- SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func);
- if (i == dfuns->end())
- {
- throw TypeCheckingException(
- n.toExpr(),
- string("Undefined function: `") + func.toString() + "'");
- }
- DefinedFunction def = (*i).second;
- formals = def.getFormals();
-
- if (Debug.isOn("expand"))
- {
- Debug("expand") << "found: " << n << endl;
- Debug("expand") << " func: " << func << endl;
- string name = func.getAttribute(expr::VarNameAttr());
- Debug("expand") << " : \"" << name << "\"" << endl;
- }
- if (Debug.isOn("expand"))
- {
- Debug("expand") << " defn: " << def.getFunction() << endl
- << " [";
- if (formals.size() > 0)
- {
- copy(formals.begin(),
- formals.end() - 1,
- ostream_iterator<Node>(Debug("expand"), ", "));
- Debug("expand") << formals.back();
- }
- Debug("expand") << "]" << endl
- << " " << def.getFunction().getType() << endl
- << " " << def.getFormula() << endl;
- }
-
- fm = def.getFormula();
- }
-
- Node instance = fm.substitute(formals.begin(),
- formals.end(),
- n.begin(),
- n.begin() + formals.size());
- Debug("expand") << "made : " << instance << endl;
-
- Node expanded = expandDefinitions(instance, cache, expandOnly);
- cache[n] = (n == expanded ? Node::null() : expanded);
- result.push(expanded);
- continue;
- }
- else if (!expandOnly)
- {
- // do not do any theory stuff if expandOnly is true
-
- theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node);
-
- Assert(t != NULL);
- TrustNode trn = t->expandDefinition(n);
- node = trn.isNull() ? Node(n) : trn.getNode();
- }
-
- // the partial functions can fall through, in which case we still
- // consider their children
- worklist.push(std::make_tuple(
- Node(n), node, true)); // Original and rewritten result
-
- for (size_t i = 0; i < node.getNumChildren(); ++i)
- {
- worklist.push(
- std::make_tuple(node[i],
- node[i],
- false)); // Rewrite the children of the result only
- }
- }
- else
- {
- // Working upwards
- // Reconstruct the node from it's (now rewritten) children on the stack
-
- Debug("expand") << "cons : " << node << endl;
- if (node.getNumChildren() > 0)
- {
- // cout << "cons : " << node << endl;
- NodeBuilder<> nb(node.getKind());
- if (node.getMetaKind() == metakind::PARAMETERIZED)
- {
- Debug("expand") << "op : " << node.getOperator() << endl;
- // cout << "op : " << node.getOperator() << endl;
- nb << node.getOperator();
- }
- for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; ++i)
- {
- Assert(!result.empty());
- Node expanded = result.top();
- result.pop();
- // cout << "exchld : " << expanded << endl;
- Debug("expand") << "exchld : " << expanded << endl;
- nb << expanded;
- }
- node = nb;
- }
- // Only cache once all subterms are expanded
- cache[n] = n == node ? Node::null() : node;
- result.push(node);
- }
- } while (!worklist.empty());
-
- AlwaysAssert(result.size() == 1);
-
- return result.top();
-}
-
void ProcessAssertions::collectSkolems(
IteSkolemMap& iskMap,
TNode n,
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "smt/assertions.h"
+#include "smt/expand_definitions.h"
#include "smt/smt_engine_stats.h"
#include "util/resource_manager.h"
{
/** The types for the recursive function definitions */
typedef context::CDList<Node> NodeList;
- typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
public:
ProcessAssertions(SmtEngine& smt,
+ ExpandDefs& exDefs,
ResourceManager& rm,
SmtEngineStatistics& stats);
~ProcessAssertions();
* processing the assertions.
*/
bool apply(Assertions& as);
- /**
- * Expand definitions in term n. Return the expanded form of n.
- *
- * @param n The node to expand
- * @param cache Cache of previous results
- * @param expandOnly if true, then the expandDefinitions function of
- * TheoryEngine is not called on subterms of n.
- * @return The expanded term.
- */
- Node expandDefinitions(TNode n,
- NodeToNodeHashMap& cache,
- bool expandOnly = false);
private:
/** Reference to the SMT engine */
SmtEngine& d_smt;
+ /** Reference to expand definitions module */
+ ExpandDefs& d_exDefs;
/** Reference to resource manager */
ResourceManager& d_resourceManager;
/** Reference to the SMT stats */
projects / cvc5.git / commitdiff