This gives theories a finer grained control over explained lemmas and conflicts.
A theory may now use an inference manager to construct "explained" lemmas/conflicts e.g. via mkLemmaExp, subsequently do any theory-specific debugging or modification to that lemma before sending it via trustedLemma.
This is required for the new strings inference manager on proof-new.
This also adds a missing variant of conflicts for the proof equality engine. It also does a minor simplification of a previous variant for constructing conflicts from proof equality engine based on a proof step buffer.
}
}
+bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; }
+
void TheoryInferenceManager::reset()
{
d_numCurrentLemmas = 0;
{
if (!d_theoryState.isInConflict())
{
- if (d_pfee != nullptr)
- {
- // use proof equality engine to construct the trust node
- TrustNode tconf = d_pfee->assertConflict(id, exp, args);
- d_out.trustedConflict(tconf);
- }
- else
- {
- // version without proofs
- Node conf = mkExplainPartial(exp, {});
- conflict(conf);
- }
+ // make the trust node
+ TrustNode tconf = mkConflictExp(id, exp, args);
+ // send it on the output channel
+ trustedConflict(tconf);
}
}
+TrustNode TheoryInferenceManager::mkConflictExp(PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args)
+{
+ if (d_pfee != nullptr)
+ {
+ // use proof equality engine to construct the trust node
+ return d_pfee->assertConflict(id, exp, args);
+ }
+ // version without proofs
+ Node conf = mkExplainPartial(exp, {});
+ return TrustNode::mkTrustConflict(conf, nullptr);
+}
+
+void TheoryInferenceManager::conflictExp(const std::vector<Node>& exp,
+ ProofGenerator* pg)
+{
+ if (!d_theoryState.isInConflict())
+ {
+ // make the trust node
+ TrustNode tconf = mkConflictExp(exp, pg);
+ // send it on the output channel
+ trustedConflict(tconf);
+ }
+}
+
+TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp,
+ ProofGenerator* pg)
+{
+ if (d_pfee != nullptr)
+ {
+ // use proof equality engine to construct the trust node
+ return d_pfee->assertConflict(exp, pg);
+ }
+ // version without proofs
+ Node conf = mkExplainPartial(exp, {});
+ return TrustNode::mkTrustConflict(conf, nullptr);
+}
+
bool TheoryInferenceManager::propagateLit(TNode lit)
{
// If already in conflict, no more propagation
const std::vector<Node>& args,
LemmaProperty p,
bool doCache)
+{
+ // make the trust node
+ TrustNode trn = mkLemmaExp(conc, id, exp, noExplain, args);
+ // send it on the output channel
+ return trustedLemma(trn, p, doCache);
+}
+
+TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ const std::vector<Node>& args)
{
if (d_pfee != nullptr)
{
// make the trust node from the proof equality engine
- TrustNode trn = d_pfee->assertLemma(conc, id, exp, noExplain, args);
- return trustedLemma(trn, p, doCache);
+ return d_pfee->assertLemma(conc, id, exp, noExplain, args);
}
- // otherwise, not using proofs, explain and send lemma
+ // otherwise, not using proofs, explain and make trust node
Node ant = mkExplainPartial(exp, noExplain);
Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
- return lemma(lem, p, doCache);
+ return TrustNode::mkTrustLemma(lem, nullptr);
}
bool TheoryInferenceManager::lemmaExp(Node conc,
ProofGenerator* pg,
LemmaProperty p,
bool doCache)
+{
+ // make the trust node
+ TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg);
+ // send it on the output channel
+ return trustedLemma(trn, p, doCache);
+}
+
+TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ ProofGenerator* pg)
{
if (d_pfee != nullptr)
{
// make the trust node from the proof equality engine
- TrustNode trn = d_pfee->assertLemma(conc, exp, noExplain, pg);
- return trustedLemma(trn, p, doCache);
+ return d_pfee->assertLemma(conc, exp, noExplain, pg);
}
- // otherwise, not using proofs, explain and send lemma
+ // otherwise, not using proofs, explain and make trust node
Node ant = mkExplainPartial(exp, noExplain);
Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
- return lemma(lem, p, doCache);
+ return TrustNode::mkTrustLemma(lem, nullptr);
}
bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
* of theory.
*/
void setEqualityEngine(eq::EqualityEngine* ee);
+ /**
+ * Are proofs enabled in this inference manager? Returns true if the proof
+ * node manager pnm provided to the constructor of this class was non-null.
+ */
+ bool isProofEnabled() const;
/**
* Reset, which resets counters regarding the number of added lemmas and
* internal facts. This method should be manually called by the theory at
void conflict(TNode conf);
/**
* Raise trusted conflict tconf (of any form) where a proof generator has
- * been provided in a custom way.
+ * been provided (as part of the trust node) in a custom way.
*/
void trustedConflict(TrustNode tconf);
/**
void conflictExp(PfRule id,
const std::vector<Node>& exp,
const std::vector<Node>& args);
+ /**
+ * Make the trust node corresponding to the conflict of the above form. It is
+ * the responsibility of the caller to subsequently call trustedConflict with
+ * the returned trust node.
+ */
+ TrustNode mkConflictExp(PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args);
+ /**
+ * Explain and send conflict from contradictory facts. This method is called
+ * when proof generator pg has a proof of false from free assumptions exp.
+ * This method sends a trusted conflict corresponding to the official
+ * equality engine's explanation of literals in exp, with the proof equality
+ * engine as the proof generator (if it exists), where pg provides the
+ * final step(s) of this proof during this call.
+ */
+ void conflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
+ /**
+ * Make the trust node corresponding to the conflict of the above form. It is
+ * the responsibility of the caller to subsequently call trustedConflict with
+ * the returned trust node.
+ */
+ TrustNode mkConflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
//--------------------------------------- lemmas
/**
* Send (trusted) lemma lem with property p on the output channel.
const std::vector<Node>& args,
LemmaProperty p = LemmaProperty::NONE,
bool doCache = true);
+ /**
+ * Make the trust node for the above method. It is responsibility of the
+ * caller to subsequently call trustedLemma with the returned trust node.
+ */
+ TrustNode mkLemmaExp(Node conc,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ const std::vector<Node>& args);
/**
* Same as above, but where pg can provide a proof of conc from free
- * assumptions in exp. It is required to do so in the remainder of the user
- * context when this method returns true.
+ * assumptions in exp. This sends a trusted lemma on the output channel where
+ * the proof equality engine is the proof generator. The generator pg
+ * is asked to provide the final step(s) of this proof during this call.
*
* @param conc The conclusion of the lemma
* @param exp The set of (all) literals that imply conc
ProofGenerator* pg = nullptr,
LemmaProperty p = LemmaProperty::NONE,
bool doCache = true);
+ /**
+ * Make the trust node for the above method. It is responsibility of the
+ * caller to subsequently call trustedLemma with the returned trust node.
+ */
+ TrustNode mkLemmaExp(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ ProofGenerator* pg = nullptr);
/**
* Has this inference manager cached and sent the given lemma (in this user
* context)? This method can be overridden by the particular manager. If not,
{
Trace("pfee") << "pfee::assertConflict " << id << ", exp = " << exp
<< ", args = " << args << std::endl;
- // conflict is same as proof of false
- std::vector<Node> empVec;
- return assertLemma(d_false, id, exp, empVec, args);
+ // conflict is same as lemma concluding false
+ return assertLemma(d_false, id, exp, {}, args);
}
TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
{
Trace("pfee") << "pfee::assertConflict " << exp << " via buffer with "
<< psb.getNumSteps() << " steps" << std::endl;
- if (d_pfEnabled)
- {
- if (!d_proof.addSteps(psb))
- {
- return TrustNode::null();
- }
- }
- std::vector<Node> empVec;
- return assertLemmaInternal(d_false, exp, empVec, &d_proof);
+ return assertLemma(d_false, exp, {}, psb);
+}
+
+TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
+ ProofGenerator* pg)
+{
+ Trace("pfee") << "pfee::assertConflict " << exp << " via generator"
+ << std::endl;
+ return assertLemma(d_false, exp, {}, pg);
}
TrustNode ProofEqEngine::assertLemma(Node conc,
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
/**
* Called when we have concluded conc, typically via theory specific
projects / cvc5.git / commitdiff