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<Node>& 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<Node> 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<Node> 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
#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 {
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();
/**
* 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<Node>& 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
* 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
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<TrustNode> d_tsubs;
+ /** Theory proof step buffer */
+ std::unique_ptr<TheoryProofStepBuffer> d_tspb;
+ /** A lazy proof for substitution steps */
+ std::unique_ptr<LazyCDProof> d_subsPg;
+ /** A lazy proof for apply steps */
+ std::unique_ptr<LazyCDProof> 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<Node> 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
projects / cvc5.git / commitdiff