#include "theory/uf/proof_equality_engine.h"
+#include "expr/lazy_proof_chain.h"
#include "theory/rewriter.h"
#include "theory/uf/proof_checker.h"
return assertLemma(d_false, id, exp, {}, args);
}
-TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
- ProofStepBuffer& psb)
-{
- Trace("pfee") << "pfee::assertConflict " << exp << " via buffer with "
- << psb.getNumSteps() << " steps" << std::endl;
- return assertLemma(d_false, exp, {}, psb);
-}
-
TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
ProofGenerator* pg)
{
Assert(conc != d_true);
LazyCDProof tmpProof(d_pnm, &d_proof);
LazyCDProof* curr;
+ TrustNodeKind tnk;
+ // same policy as above: for conflicts, use existing lazy proof
if (conc == d_false)
{
- // optimization: we can use the main lazy proof directly, because we
- // know we will backtrack immediately after this call.
curr = &d_proof;
+ tnk = TrustNodeKind::CONFLICT;
}
else
{
- // use a lazy proof that always links to d_proof
curr = &tmpProof;
+ tnk = TrustNodeKind::LEMMA;
}
- // Register the proof step.
- if (!curr->addStep(conc, id, exp, args))
+ // explain each literal in the vector
+ std::vector<TNode> assumps;
+ explainVecWithProof(tnk, assumps, exp, noExplain, curr);
+ // Register the proof step. We use a separate lazy CDProof which will make
+ // calls to curr above for the proofs of the literals in exp.
+ LazyCDProof outer(d_pnm, curr);
+ if (!outer.addStep(conc, id, exp, args))
{
// a step went wrong, e.g. during checking
Assert(false) << "pfee::assertConflict: register proof step";
return TrustNode::null();
}
- // We've now decided which lazy proof to use (curr), now get the proof
- // for conc.
- return assertLemmaInternal(conc, exp, noExplain, curr);
-}
-
-TrustNode ProofEqEngine::assertLemma(Node conc,
- const std::vector<Node>& exp,
- const std::vector<Node>& noExplain,
- ProofStepBuffer& psb)
-{
- Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
- << ", noExplain = " << noExplain << " via buffer with "
- << psb.getNumSteps() << " steps" << std::endl;
- LazyCDProof tmpProof(d_pnm, &d_proof);
- LazyCDProof* curr;
- // same policy as above: for conflicts, use existing lazy proof
- if (conc == d_false)
- {
- curr = &d_proof;
- }
- else
- {
- curr = &tmpProof;
- }
- // add all steps to the proof
- const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
- for (const std::pair<Node, ProofStep>& ps : steps)
- {
- if (!curr->addStep(ps.first, ps.second))
- {
- return TrustNode::null();
- }
- }
- return assertLemmaInternal(conc, exp, noExplain, curr);
+ // Now get the proof for conc.
+ return ensureProofForFact(conc, assumps, tnk, &outer);
}
TrustNode ProofEqEngine::assertLemma(Node conc,
<< std::endl;
LazyCDProof tmpProof(d_pnm, &d_proof);
LazyCDProof* curr;
+ TrustNodeKind tnk;
// same policy as above: for conflicts, use existing lazy proof
if (conc == d_false)
{
curr = &d_proof;
+ tnk = TrustNodeKind::CONFLICT;
}
else
{
curr = &tmpProof;
+ tnk = TrustNodeKind::LEMMA;
}
- // Register the proof. Notice we do a deep copy here because the CDProof
- // curr should take ownership of the proof steps that pg provided for conc.
- // In other words, this sets up the "skeleton" of proof that is the base
- // of the proof we are constructing. The call to assertLemmaInternal below
- // will expand the leaves of this proof. If we used a shallow copy, then
- // the connection to these leaves would be lost since they would not be
- // owned by curr.
- if (!pg->addProofTo(conc, curr, CDPOverwrite::ASSUME_ONLY, true))
- {
- // a step went wrong, e.g. during checking
- Assert(false) << "pfee::assertConflict: register proof step";
- return TrustNode::null();
- }
- return assertLemmaInternal(conc, exp, noExplain, curr);
+ // explain each literal in the vector
+ std::vector<TNode> assumps;
+ explainVecWithProof(tnk, assumps, exp, noExplain, curr);
+ // We use a lazy proof chain here. The provided proof generator sets up the
+ // "skeleton" that is the base of the proof we are constructing. The call to
+ // LazyCDProofChain::getProofFor will expand the leaves of this proof via
+ // calls to curr.
+ LazyCDProofChain outer(d_pnm, true, nullptr, curr, false);
+ outer.addLazyStep(conc, pg);
+ return ensureProofForFact(conc, assumps, tnk, &outer);
}
TrustNode ProofEqEngine::explain(Node conc)
return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, &tmpProof);
}
-TrustNode ProofEqEngine::assertLemmaInternal(Node conc,
- const std::vector<Node>& exp,
- const std::vector<Node>& noExplain,
- LazyCDProof* curr)
+void ProofEqEngine::explainVecWithProof(TrustNodeKind& tnk,
+ std::vector<TNode>& assumps,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ LazyCDProof* curr)
{
- // We are a conflict if the conclusion is false and all literals are
- // explained.
- TrustNodeKind tnk =
- conc == d_false ? TrustNodeKind::CONFLICT : TrustNodeKind::LEMMA;
-
- // get the explanation, with proofs
- std::vector<TNode> assumps;
std::vector<Node> expn;
for (const Node& e : exp)
{
tnk = TrustNodeKind::LEMMA;
}
}
- return ensureProofForFact(conc, assumps, tnk, curr);
}
TrustNode ProofEqEngine::ensureProofForFact(Node conc,
const std::vector<TNode>& assumps,
TrustNodeKind tnk,
- LazyCDProof* curr)
+ ProofGenerator* curr)
{
Trace("pfee-proof") << std::endl;
Trace("pfee-proof") << "pfee::ensureProofForFact: input " << conc << " via "
TrustNode assertConflict(PfRule id,
const std::vector<Node>& exp,
const std::vector<Node>& args);
- /** Multi-step version */
- TrustNode assertConflict(const std::vector<Node>& exp, ProofStepBuffer& psb);
/** Generator version, where pg has a proof of false from assumptions exp */
TrustNode assertConflict(const std::vector<Node>& exp, ProofGenerator* pg);
//-------------------------- assert lemma
const std::vector<Node>& exp,
const std::vector<Node>& noExplain,
const std::vector<Node>& args);
- /** Multi-step version */
- TrustNode assertLemma(Node conc,
- const std::vector<Node>& exp,
- const std::vector<Node>& noExplain,
- ProofStepBuffer& psb);
/** Generator version, where pg has a proof of conc */
TrustNode assertLemma(Node conc,
const std::vector<Node>& exp,
bool assertFactInternal(TNode pred, bool polarity, TNode reason);
/** holds */
bool holds(TNode pred, bool polarity);
- /**
- * Assert lemma internal. This method is called for ensuring the proof of
- * conc exists in curr, where exp / noExplain are the its explanation (see
- * assertLemma). This method is used for conflicts as well, where noExplain
- * must be empty and conc = d_false.
- *
- * If curr is null, no proof is constructed.
- *
- * This method returns the trust node of the lemma or conflict with this
- * class as the proof generator.
- */
- TrustNode assertLemmaInternal(Node conc,
- const std::vector<Node>& exp,
- const std::vector<Node>& noExplain,
- LazyCDProof* curr);
/**
* Ensure proof for fact. This is called by the above method after we have
* determined the final set of assumptions used for showing conc. This
TrustNode ensureProofForFact(Node conc,
const std::vector<TNode>& assumps,
TrustNodeKind tnk,
- LazyCDProof* curr);
+ ProofGenerator* curr);
+ /**
+ * This ensures the proof of the literals that are in exp but not in
+ * noExplain have been added to curr. This additionally adds the
+ * explanation of exp to assumps. It updates tnk to LEMMA if there
+ * are any literals in exp that are not in noExplain.
+ */
+ void explainVecWithProof(TrustNodeKind& tnk,
+ std::vector<TNode>& assumps,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ LazyCDProof* curr);
+ /** Explain
+ *
+ * This adds to assumps the set of facts that were asserted to this
+ * class in the current SAT context that are required for showing lit.
+ *
+ * This additionally registers the equality proof steps required to
+ * regress the explanation of lit in curr.
+ */
+ void explainWithProof(Node lit,
+ std::vector<TNode>& assumps,
+ LazyCDProof* curr);
/** Reference to the equality engine */
eq::EqualityEngine& d_ee;
/** The default proof generator (for simple facts) */
* SAT-context-dependent.
*/
NodeSet d_keep;
- /** Explain
- *
- * This adds to assumps the set of facts that were asserted to this
- * class in the current SAT context by calls to assertAssume that are
- * required for showing lit.
- *
- * This additionally registers the equality proof steps required to
- * regress the explanation of lit.
- */
- void explainWithProof(Node lit,
- std::vector<TNode>& assumps,
- LazyCDProof* curr);
};
} // namespace eq
projects / cvc5.git / commitdiff