diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-30 14:12:56 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-30 19:12:56 +0000 |
commit | 327a24508ed1d02a3fa233e680ffd0b30aa685a9 (patch) | |
tree | d130a4b5afcf34383b6bdf38c433d77c5911709d /src/smt/expand_definitions.cpp | |
parent | 38a45651953d3bcfe67cb80b4f2ba2d1b278f7ba (diff) |
Use substitutions for implementing defined functions (#6437)
This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions.
In other words, the effect of:
(define-fun f X t)
is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when
(= f (lambda X t)) was an equality solved by non-clausal simplification
The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula.
In this PR:
define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline.
Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit.
The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions.
The proof manager does not require a special case of using the define-function maps.
Define-function maps are eliminated from SmtEngine.
Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.
Diffstat (limited to 'src/smt/expand_definitions.cpp')
-rw-r--r-- | src/smt/expand_definitions.cpp | 192 |
1 files changed, 6 insertions, 186 deletions
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index d331e8e78..14182a46d 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -20,7 +20,7 @@ #include "expr/node_manager_attributes.h" #include "preprocessing/assertion_pipeline.h" -#include "smt/defined_function.h" +#include "smt/env.h" #include "smt/smt_engine.h" #include "smt/smt_engine_stats.h" #include "theory/theory_engine.h" @@ -32,10 +32,8 @@ using namespace cvc5::kind; namespace cvc5 { namespace smt { -ExpandDefs::ExpandDefs(SmtEngine& smt, - ResourceManager& rm, - SmtEngineStatistics& stats) - : d_smt(smt), d_resourceManager(rm), d_smtStats(stats), d_tpg(nullptr) +ExpandDefs::ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats) + : d_smt(smt), d_env(env), d_smtStats(stats), d_tpg(nullptr) { } @@ -57,7 +55,6 @@ TrustNode ExpandDefs::expandDefinitions( TConvProofGenerator* tpg) { const TNode orig = n; - 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)); @@ -67,7 +64,7 @@ TrustNode ExpandDefs::expandDefinitions( do { - d_resourceManager.spendResource(Resource::PreprocessStep); + d_env.getResourceManager()->spendResource(Resource::PreprocessStep); // n is the input / original // node is the output / result @@ -79,38 +76,9 @@ TrustNode ExpandDefs::expandDefinitions( // 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(); - const std::vector<Node>& formals = (*i).second.getFormals(); - // replacement must be closed - if (!formals.empty()) - { - f = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, formals), f); - } - // are we are producing proofs for this call? - if (tpg != nullptr) - { - // if this is a variable, we can simply assume it - // ------- ASSUME - // n = f - Node conc = n.eqNode(f); - tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc}, true); - } - // must recursively expand its definition - TrustNode tfe = expandDefinitions(f, cache, expandOnly, tpg); - Node fe = tfe.isNull() ? f : tfe.getNode(); - // don't bother putting in the cache - result.push(fe); - continue; - } // don't bother putting in the cache result.push(n); continue; @@ -125,132 +93,7 @@ TrustNode ExpandDefs::expandDefinitions( 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()); - } - } - // the premise of the proof of expansion (if we are expanding a definition - // and proofs are enabled) - std::vector<Node> pfExpChildren; - 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 TypeCheckingExceptionPrivate( - n, - 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(); - // are we producing proofs for this call? - if (tpg != nullptr) - { - Node pfRhs = fm; - if (!formals.empty()) - { - Node bvl = nm->mkNode(BOUND_VAR_LIST, formals); - pfRhs = nm->mkNode(LAMBDA, bvl, pfRhs); - } - Assert(func.getType().isComparableTo(pfRhs.getType())); - pfExpChildren.push_back(func.eqNode(pfRhs)); - } - } - - Node instance = fm.substitute(formals.begin(), - formals.end(), - n.begin(), - n.begin() + formals.size()); - Debug("expand") << "made : " << instance << std::endl; - // are we producing proofs for this call? - if (tpg != nullptr) - { - if (n != instance) - { - // This code is run both when we are doing expand definitions and - // simple beta reduction. - // - // f = (lambda ((x T)) t) [if we are expanding a definition] - // ---------------------- MACRO_SR_PRED_INTRO - // n = instance - Node conc = n.eqNode(instance); - tpg->addRewriteStep(n, - instance, - PfRule::MACRO_SR_PRED_INTRO, - pfExpChildren, - {conc}, - true); - } - } - // now, call expand definitions again on the result - TrustNode texp = expandDefinitions(instance, cache, expandOnly, tpg); - Node expanded = texp.isNull() ? instance : texp.getNode(); - cache[n] = n == expanded ? Node::null() : expanded; - result.push(expanded); - continue; - } - else if (!expandOnly) + if (!expandOnly) { // do not do any theory stuff if expandOnly is true @@ -331,35 +174,12 @@ TrustNode ExpandDefs::expandDefinitions( return TrustNode::mkTrustRewrite(orig, res, tpg); } -void ExpandDefs::expandAssertions(AssertionPipeline& assertions, - bool expandOnly) -{ - Chat() << "expanding definitions in assertions..." << std::endl; - Trace("exp-defs") << "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]; - // notice we call this method with only one value of expandOnly currently, - // hence we maintain only a single set of proof steps in d_tpg. - TrustNode expd = expandDefinitions(assert, cache, expandOnly, d_tpg.get()); - if (!expd.isNull()) - { - Trace("exp-defs") << "ExpandDefs::expandAssertions: " << assert << " -> " - << expd.getNode() << std::endl; - assertions.replaceTrusted(i, expd); - } - } -} - void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm) { if (d_tpg == nullptr) { d_tpg.reset(new TConvProofGenerator(pnm, - d_smt.getUserContext(), + d_env.getUserContext(), TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, "ExpandDefs::TConvProofGenerator", |