From 738676c39badd9a03db0feaa00bb4bd467f0600a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 18 Oct 2020 18:01:24 -0500 Subject: [PATCH] (proof-new) Implementation of trust substitution (#5276) Trust substitution is a data structure that is used throughout preprocessing for proofs. This adds its implementation. --- src/expr/proof_rule.cpp | 1 + src/expr/proof_rule.h | 7 +- src/theory/builtin/proof_checker.cpp | 4 +- src/theory/trust_substitutions.cpp | 214 +++++++++++++++++++++++++-- src/theory/trust_substitutions.h | 64 +++++++- 5 files changed, 276 insertions(+), 14 deletions(-) diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index e4719ff30..9448e1939 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -43,6 +43,7 @@ const char* toString(PfRule id) case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; case PfRule::TRUST_REWRITE: return "TRUST_REWRITE"; case PfRule::TRUST_SUBS: return "TRUST_SUBS"; + case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP"; //================================================= Boolean rules case PfRule::RESOLUTION: return "RESOLUTION"; case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 340b636ae..4000d4df7 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -234,11 +234,14 @@ enum class PfRule : uint32_t // a witness term (witness ((x T)) (P x)). WITNESS_AXIOM, // where F is an equality (= t t') that holds by a form of rewriting that - // could not be replayed. + // could not be replayed during proof postprocessing. TRUST_REWRITE, // where F is an equality (= t t') that holds by a form of substitution that - // could not be replayed. + // could not be replayed during proof postprocessing. TRUST_SUBS, + // where F is an equality (= t t') that holds by a form of substitution that + // could not be determined by the TrustSubstitutionMap. + TRUST_SUBS_MAP, //================================================= Boolean rules // ======== Resolution diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 6fc4671ee..e59f48fff 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -76,6 +76,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3); pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1); + pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( @@ -397,7 +398,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, else if (id == PfRule::PREPROCESS || id == PfRule::THEORY_PREPROCESS || id == PfRule::WITNESS_AXIOM || id == PfRule::THEORY_LEMMA || id == PfRule::PREPROCESS_LEMMA || id == PfRule::THEORY_REWRITE - || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS) + || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS + || id == PfRule::TRUST_SUBS_MAP) { // "trusted" rules Assert(children.empty()); diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index de8fc2ceb..482c487eb 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -20,41 +20,235 @@ namespace CVC4 { namespace theory { TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, - ProofNodeManager* pnm) - : d_subs(c) + ProofNodeManager* pnm, + std::string name, + PfRule trustId, + MethodId ids) + : 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_currentSubs(c), + d_name(name), + d_trustId(trustId), + d_ids(ids) { } void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg) { + Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: add " << x + << " -> " << t << std::endl; d_subs.addSubstitution(x, t); + if (isProofEnabled()) + { + TrustNode tnl = TrustNode::mkTrustRewrite(x, t, pg); + d_tsubs.push_back(tnl); + // current substitution node is no longer valid. + d_currentSubs = Node::null(); + // add to lazy proof + d_subsPg->addLazyStep(tnl.getProven(), + pg, + false, + "TrustSubstitutionMap::addSubstitution", + false, + d_trustId); + } } -TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite) +void TrustSubstitutionMap::addSubstitution(TNode x, + TNode t, + PfRule id, + const std::vector& args) { - Node ns = d_subs.apply(n); - if (doRewrite) + if (!isProofEnabled()) { - ns = Rewriter::rewrite(ns); + addSubstitution(x, t, nullptr); + return; } - return TrustNode::mkTrustRewrite(n, ns, nullptr); + LazyCDProof* stepPg = d_helperPf.allocateProof(); + Node eq = x.eqNode(t); + stepPg->addStep(eq, id, {}, args); + addSubstitution(x, t, stepPg); } void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn) { + Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add " + << x << " -> " << t << " from " << tn.getProven() + << std::endl; if (!isProofEnabled() || tn.getGenerator() == nullptr) { // no generator or not proof enabled, nothing to do addSubstitution(x, t, nullptr); + Trace("trust-subs") << "...no proof" << std::endl; + return; + } + Node eq = x.eqNode(t); + Node proven = tn.getProven(); + // notice that this checks syntactic equality, not CDProof::isSame since + // tn.getGenerator() is not necessarily robust to symmetry. + if (eq == proven) + { + // no rewrite required, just use the generator + addSubstitution(x, t, tn.getGenerator()); + Trace("trust-subs") << "...use generator directly" << std::endl; return; } - // NOTE: can try to transform tn.getProven() to (= x t) here - addSubstitution(x, t, nullptr); + LazyCDProof* solvePg = d_helperPf.allocateProof(); + // Try to transform tn.getProven() to (= x t) here, if necessary + if (!d_tspb->applyPredTransform(proven, eq, {})) + { + // failed to rewrite + addSubstitution(x, t, nullptr); + Trace("trust-subs") << "...failed to rewrite" << std::endl; + return; + } + Trace("trust-subs") << "...successful rewrite" << std::endl; + solvePg->addSteps(*d_tspb.get()); + d_tspb->clear(); + // link the given generator + solvePg->addLazyStep(proven, tn.getGenerator()); + addSubstitution(x, t, solvePg); +} + +void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t) +{ + if (!isProofEnabled()) + { + // just use the basic utility + d_subs.addSubstitutions(t.get()); + return; + } + // call addSubstitution above in sequence + for (const TrustNode& tns : t.d_tsubs) + { + Node proven = tns.getProven(); + addSubstitution(proven[0], proven[1], tns.getGenerator()); + } +} + +TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite) +{ + Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n + << std::endl; + Node ns = d_subs.apply(n); + Trace("trust-subs") << "...subs " << ns << std::endl; + // rewrite if indicated + if (doRewrite) + { + ns = Rewriter::rewrite(ns); + Trace("trust-subs") << "...rewrite " << ns << std::endl; + } + if (n == ns) + { + // no change + return TrustNode::null(); + } + if (!isProofEnabled()) + { + // no proofs, use null generator + return TrustNode::mkTrustRewrite(n, ns, nullptr); + } + Node cs = getCurrentSubstitution(); + Trace("trust-subs") + << "TrustSubstitutionMap::addSubstitution: current substitution is " << cs + << std::endl; + // Easy case: if n is in the domain of the substitution, maybe it is already + // a proof in the substitution proof generator. This is moreover required + // to avoid cyclic proofs below. For example, if { x -> 5 } is a substitution, + // and we are asked to transform x, resulting in 5, we hence must provide + // a proof of (= x 5) based on the substitution. However, it must be the + // case that (= x 5) is a proven fact of the substitution generator. Hence + // we avoid a proof that looks like: + // ---------- from d_subsPg + // (= x 5) + // ---------- MACRO_SR_EQ_INTRO{x} + // (= x 5) + // by taking the premise proof directly. + Node eq = n.eqNode(ns); + if (d_subsPg->hasStep(eq) || d_subsPg->hasGenerator(eq)) + { + return TrustNode::mkTrustRewrite(n, ns, d_subsPg.get()); + } + Assert(eq != cs); + std::vector pfChildren; + if (!cs.isConst()) + { + // note we will get more proof reuse if we do not special case AND here. + if (cs.getKind() == kind::AND) + { + for (const Node& csc : cs) + { + pfChildren.push_back(csc); + // connect substitution generator into apply generator + d_applyPg->addLazyStep(csc, d_subsPg.get()); + } + } + else + { + pfChildren.push_back(cs); + // connect substitution generator into apply generator + d_applyPg->addLazyStep(cs, d_subsPg.get()); + } + } + if (!d_tspb->applyEqIntro(n, ns, pfChildren, d_ids)) + { + return TrustNode::mkTrustRewrite(n, ns, nullptr); + } + // ------- ------- from external proof generators + // x1 = t1 ... xn = tn + // ----------------------- AND_INTRO + // ... + // --------- MACRO_SR_EQ_INTRO + // n == ns + // add it to the apply proof generator. + // + // Notice that we use a single child to MACRO_SR_EQ_INTRO here. This is an + // optimization motivated by the fact that n may be large and reused many + // time. For instance, if this class is being used to track substitutions + // derived during non-clausal simplification during preprocessing, it is + // a fixed (possibly) large substitution applied to many terms. Having + // a single child saves us from creating many proofs with n children, where + // notice this proof is reused. + d_applyPg->addSteps(*d_tspb.get()); + d_tspb->clear(); + return TrustNode::mkTrustRewrite(n, ns, d_applyPg.get()); } SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; } -bool TrustSubstitutionMap::isProofEnabled() const { return false; } +bool TrustSubstitutionMap::isProofEnabled() const +{ + return d_subsPg != nullptr; +} + +Node TrustSubstitutionMap::getCurrentSubstitution() +{ + Assert(isProofEnabled()); + if (!d_currentSubs.get().isNull()) + { + return d_currentSubs; + } + std::vector csubsChildren; + for (const TrustNode& tns : d_tsubs) + { + csubsChildren.push_back(tns.getProven()); + } + d_currentSubs = NodeManager::currentNM()->mkAnd(csubsChildren); + if (d_currentSubs.get().getKind() == kind::AND) + { + d_subsPg->addStep(d_currentSubs, PfRule::AND_INTRO, csubsChildren, {}); + } + return d_currentSubs; +} } // namespace theory } // namespace CVC4 diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index 0eacc50f5..91555ee56 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -17,9 +17,15 @@ #ifndef CVC4__THEORY__TRUST_SUBSTITUTIONS_H #define CVC4__THEORY__TRUST_SUBSTITUTIONS_H +#include "context/cdlist.h" #include "context/context.h" +#include "expr/lazy_proof.h" +#include "expr/lazy_proof_set.h" #include "expr/proof_node_manager.h" +#include "expr/term_conversion_proof_generator.h" +#include "theory/eager_proof_generator.h" #include "theory/substitutions.h" +#include "theory/theory_proof_step_buffer.h" #include "theory/trust_node.h" namespace CVC4 { @@ -31,7 +37,11 @@ namespace theory { class TrustSubstitutionMap { public: - TrustSubstitutionMap(context::Context* c, ProofNodeManager* pnm); + TrustSubstitutionMap(context::Context* c, + ProofNodeManager* pnm, + std::string name = "TrustSubstitutionMap", + PfRule trustId = PfRule::TRUST_SUBS_MAP, + MethodId ids = MethodId::SB_DEFAULT); /** Gets a reference to the underlying substitution map */ SubstitutionMap& get(); /** @@ -39,6 +49,14 @@ class TrustSubstitutionMap * in the remainder of this user context. */ void addSubstitution(TNode x, TNode t, ProofGenerator* pg = nullptr); + /** + * Add substitution x -> t from a single proof step with rule id, no children + * and arguments args. + */ + void addSubstitution(TNode x, + TNode t, + PfRule id, + const std::vector& args); /** * Add substitution x -> t, which was derived from the proven field of * trust node tn. In other words, (= x t) is the solved form of @@ -52,6 +70,11 @@ class TrustSubstitutionMap * we simply add the substitution. */ void addSubstitutionSolved(TNode x, TNode t, TrustNode tn); + /** + * Add substitutions from trust substitution map t. This adds all + * substitutions from the map t and carries over its information about proofs. + */ + void addSubstitutions(TrustSubstitutionMap& t); /** * Apply substitutions in this class to node n. Returns a trust node * proving n = n*sigma, where the proof generator is provided by this class @@ -62,8 +85,47 @@ class TrustSubstitutionMap private: /** Are proofs enabled? */ bool isProofEnabled() const; + /** + * Get current substitution. This returns a node of the form: + * (and (= x1 t1) ... (= xn tn)) + * where (x1, t1) ... (xn, tn) have been registered via addSubstitution above. + * Moreover, it ensures that d_subsPg has a proof of the returned value. + */ + Node getCurrentSubstitution(); /** The substitution map */ SubstitutionMap d_subs; + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** A context-dependent list of trust nodes */ + context::CDList d_tsubs; + /** Theory proof step buffer */ + std::unique_ptr d_tspb; + /** A lazy proof for substitution steps */ + std::unique_ptr d_subsPg; + /** A lazy proof for apply steps */ + std::unique_ptr d_applyPg; + /** + * A context-dependent list of LazyCDProof, allocated for internal steps. + */ + LazyCDProofSet d_helperPf; + /** + * The formula corresponding to the current substitution. This is of the form + * (and (= x1 t1) ... (= xn tn)) + * when the substitution map contains { x1 -> t1, ... xn -> tn }. This field + * is updated on demand. When this class applies a substitution to a node, + * this formula is computed and recorded as the premise of a + * MACRO_SR_EQ_INTRO step. + */ + context::CDO d_currentSubs; + /** Name for debugging */ + std::string d_name; + /** + * The placeholder trusted PfRule identifier for calls to addSubstitution + * that are not given proof generators. + */ + PfRule d_trustId; + /** The method id for which form of substitution to apply */ + MethodId d_ids; }; } // namespace theory -- 2.30.2