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/theory | |
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/theory')
-rw-r--r-- | src/theory/trust_substitutions.cpp | 33 | ||||
-rw-r--r-- | src/theory/trust_substitutions.h | 8 |
2 files changed, 26 insertions, 15 deletions
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index 4088deb94..47507bfe0 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -27,21 +27,32 @@ TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, MethodId ids) : d_ctx(c), d_subs(c), - d_pnm(pnm), d_tsubs(c), - d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr), - d_subsPg( - pnm ? new LazyCDProof(pnm, nullptr, c, "TrustSubstitutionMap::subsPg") - : nullptr), - d_applyPg(pnm ? new LazyCDProof( - pnm, nullptr, c, "TrustSubstitutionMap::applyPg") - : nullptr), - d_helperPf(pnm, c), + d_tspb(nullptr), + d_subsPg(nullptr), + d_applyPg(nullptr), + d_helperPf(nullptr), d_name(name), d_trustId(trustId), d_ids(ids), d_eqtIndex(c) { + setProofNodeManager(pnm); +} + +void TrustSubstitutionMap::setProofNodeManager(ProofNodeManager* pnm) +{ + if (pnm != nullptr) + { + // should not set the proof node manager more than once + Assert(d_tspb == nullptr); + d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker())), + d_subsPg.reset(new LazyCDProof( + pnm, nullptr, d_ctx, "TrustSubstitutionMap::subsPg")); + d_applyPg.reset( + new LazyCDProof(pnm, nullptr, d_ctx, "TrustSubstitutionMap::applyPg")); + d_helperPf.reset(new CDProofSet<LazyCDProof>(pnm, d_ctx)); + } } void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg) @@ -69,7 +80,7 @@ void TrustSubstitutionMap::addSubstitution(TNode x, addSubstitution(x, t, nullptr); return; } - LazyCDProof* stepPg = d_helperPf.allocateProof(nullptr, d_ctx); + LazyCDProof* stepPg = d_helperPf->allocateProof(nullptr, d_ctx); Node eq = x.eqNode(t); stepPg->addStep(eq, id, children, args); addSubstitution(x, t, stepPg); @@ -100,7 +111,7 @@ ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x, Trace("trust-subs") << "...use generator directly" << std::endl; return tn.getGenerator(); } - LazyCDProof* solvePg = d_helperPf.allocateProof(nullptr, d_ctx); + LazyCDProof* solvePg = d_helperPf->allocateProof(nullptr, d_ctx); // Try to transform tn.getProven() to (= x t) here, if necessary if (!d_tspb->applyPredTransform(proven, eq, {})) { diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index e8b627249..ec5b2ffb5 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -42,10 +42,12 @@ class TrustSubstitutionMap : public ProofGenerator public: TrustSubstitutionMap(context::Context* c, - ProofNodeManager* pnm, + ProofNodeManager* pnm = nullptr, std::string name = "TrustSubstitutionMap", PfRule trustId = PfRule::PREPROCESS_LEMMA, MethodId ids = MethodId::SB_DEFAULT); + /** Set proof node manager */ + void setProofNodeManager(ProofNodeManager* pnm); /** Gets a reference to the underlying substitution map */ SubstitutionMap& get(); /** @@ -105,8 +107,6 @@ class TrustSubstitutionMap : public ProofGenerator context::Context* d_ctx; /** The substitution map */ SubstitutionMap d_subs; - /** The proof node manager */ - ProofNodeManager* d_pnm; /** A context-dependent list of trust nodes */ context::CDList<TrustNode> d_tsubs; /** Theory proof step buffer */ @@ -118,7 +118,7 @@ class TrustSubstitutionMap : public ProofGenerator /** * A context-dependent list of LazyCDProof, allocated for internal steps. */ - CDProofSet<LazyCDProof> d_helperPf; + std::unique_ptr<CDProofSet<LazyCDProof>> d_helperPf; /** Name for debugging */ std::string d_name; /** |