pnm, nullptr, c, "TrustSubstitutionMap::applyPg")
: nullptr),
d_helperPf(pnm, c),
- d_currentSubs(c),
d_name(name),
d_trustId(trustId),
- d_ids(ids)
+ d_ids(ids),
+ d_eqtIndex(c)
{
}
{
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, d_trustId);
}
// 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;
+ Node eq = n.eqNode(ns);
+ // remember the index
+ d_eqtIndex[eq] = d_tsubs.size();
+ // this class will provide a proof if asked
+ return TrustNode::mkTrustRewrite(n, ns, this);
+}
+
+std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
+{
+ Assert(eq.getKind() == kind::EQUAL);
+ Node n = eq[0];
+ Node ns = eq[1];
// 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,
// ---------- 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());
+ return d_subsPg->getProofFor(eq);
}
+ NodeUIntMap::iterator it = d_eqtIndex.find(eq);
+ Assert(it != d_eqtIndex.end());
+ Trace("trust-subs-pf") << "TrustSubstitutionMap::getProofFor, # assumptions= "
+ << it->second << std::endl;
+ Node cs = getSubstitution(it->second);
Assert(eq != cs);
std::vector<Node> pfChildren;
if (!cs.isConst())
d_applyPg->addLazyStep(cs, d_subsPg.get());
}
}
+ Trace("trust-subs-pf") << "...apply eq intro" << std::endl;
if (!d_tspb->applyEqIntro(n, ns, pfChildren, d_ids))
{
// if we fail for any reason, we must use a trusted step instead
d_tspb->addStep(PfRule::TRUST_SUBS_MAP, pfChildren, {eq}, eq);
}
+ Trace("trust-subs-pf") << "...made steps" << std::endl;
// ------- ------- from external proof generators
// x1 = t1 ... xn = tn
// ----------------------- AND_INTRO
// notice this proof is reused.
d_applyPg->addSteps(*d_tspb.get());
d_tspb->clear();
- return TrustNode::mkTrustRewrite(n, ns, d_applyPg.get());
+ Trace("trust-subs-pf") << "...finish, make proof" << std::endl;
+ return d_applyPg->getProofFor(eq);
}
+std::string TrustSubstitutionMap::identify() const { return d_name; }
+
SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; }
bool TrustSubstitutionMap::isProofEnabled() const
return d_subsPg != nullptr;
}
-Node TrustSubstitutionMap::getCurrentSubstitution()
+Node TrustSubstitutionMap::getSubstitution(size_t index)
{
- Assert(isProofEnabled());
- if (!d_currentSubs.get().isNull())
- {
- return d_currentSubs;
- }
+ Assert(index <= d_tsubs.size());
std::vector<Node> csubsChildren;
- for (const TrustNode& tns : d_tsubs)
+ for (size_t i = 0; i < index; i++)
{
- csubsChildren.push_back(tns.getProven());
+ csubsChildren.push_back(d_tsubs[i].getProven());
}
- std::reverse(csubsChildren.begin(),csubsChildren.end());
- d_currentSubs = NodeManager::currentNM()->mkAnd(csubsChildren);
- if (d_currentSubs.get().getKind() == kind::AND)
+ std::reverse(csubsChildren.begin(), csubsChildren.end());
+ Node cs = NodeManager::currentNM()->mkAnd(csubsChildren);
+ if (cs.getKind() == kind::AND)
{
- d_subsPg->addStep(d_currentSubs, PfRule::AND_INTRO, csubsChildren, {});
+ d_subsPg->addStep(cs, PfRule::AND_INTRO, csubsChildren, {});
}
- return d_currentSubs;
+ return cs;
}
} // namespace theory
#ifndef CVC5__THEORY__TRUST_SUBSTITUTIONS_H
#define CVC5__THEORY__TRUST_SUBSTITUTIONS_H
+#include "context/cdhashmap.h"
#include "context/cdlist.h"
#include "context/context.h"
#include "expr/lazy_proof.h"
/**
* A layer on top of SubstitutionMap that tracks proofs.
*/
-class TrustSubstitutionMap
+class TrustSubstitutionMap : public ProofGenerator
{
+ using NodeUIntMap = context::CDHashMap<Node, size_t, NodeHashFunction>;
+
public:
TrustSubstitutionMap(context::Context* c,
ProofNodeManager* pnm,
*/
TrustNode apply(Node n, bool doRewrite = true);
+ /** Get the proof for formula f */
+ std::shared_ptr<ProofNode> getProofFor(Node f) override;
+ /** Identify */
+ std::string identify() const override;
+
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.
+ * Get the substitution up to index
*/
- Node getCurrentSubstitution();
+ Node getSubstitution(size_t index);
/** The context used here */
context::Context* d_ctx;
/** The substitution map */
* A context-dependent list of LazyCDProof, allocated for internal steps.
*/
CDProofSet<LazyCDProof> 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;
/**
PfRule d_trustId;
/** The method id for which form of substitution to apply */
MethodId d_ids;
+ /**
+ * Map from solved equalities to the size of d_tsubs at the time they
+ * were concluded. Notice this is required so that we can reconstruct
+ * proofs for substitutions after they have become invalidated by later
+ * calls to addSubstitution. For example, if we call:
+ * addSubstitution x -> y
+ * addSubstitution z -> w
+ * apply f(x), returns f(y)
+ * addSubstitution y -> w
+ * We map (= (f x) (f y)) to index 2, since we only should apply the first
+ * two substitutions but not the third when asked to prove this equality.
+ */
+ NodeUIntMap d_eqtIndex;
};
} // namespace theory
projects / cvc5.git / commitdiff