diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/trust_node.cpp | 6 | ||||
| -rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 10 |
2 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp index 35fc5e348..d447cbf60 100644 --- a/src/theory/trust_node.cpp +++ b/src/theory/trust_node.cpp @@ -14,6 +14,8 @@ #include "theory/trust_node.h" +#include "theory/proof_engine_output_channel.h" + namespace CVC4 { namespace theory { @@ -36,14 +38,14 @@ std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk) TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g) { // if a generator is provided, should confirm that it can prove it - Assert(g == nullptr || g->hasProofFor(conf)); + Assert(g == nullptr || g->hasProofFor(ProofEngineOutputChannel::getConflictKeyValue(conf))); return TrustNode(TrustNodeKind::CONFLICT, conf, g); } TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g) { // if a generator is provided, should confirm that it can prove it - Assert(g == nullptr || g->hasProofFor(lem)); + Assert(g == nullptr || g->hasProofFor(ProofEngineOutputChannel::getLemmaKeyValue(lem))); return TrustNode(TrustNodeKind::LEMMA, lem, g); } diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 5dd62daee..c98e51adb 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -371,11 +371,13 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, // ensured by the fact that the core mechanism for generating proofs // from the equality engine is syncronized with its getExplanation // method. + std::stringstream ss; + pfConc->printDebug(ss); Trace("pfee-proof") << "Could not find free assumption for " << a << " in " << freeAssumps << std::endl; - Assert(false) << "pfee::ensureProofForFact: explained assumption " << a - << " does not match a free assumption from " << freeAssumps - << " in the corresponding proof"; + Notice() << "pfee::ensureProofForFact: explained assumption " << a + << " does not match a free assumption from " << freeAssumps << std::endl; + // Assert(false); } } else @@ -398,13 +400,13 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, } Trace("pfee-proof") << "pfee::ensureProofForFact: formula is " << formula << std::endl; + Node concFormula = isConflict ? formula.negate() : formula; // if proofs are enabled, scope the proof constructed above, and connect the // formula with the proof if (d_pfEnabled) { // Notice that we have an expected conclusion (formula) which we pass to // mkNode, which can check it if it wants. This is negated for conflicts. - Node concFormula = isConflict ? formula.negate() : formula; std::shared_ptr<ProofNode> pf = d_pnm->mkNode(PfRule::SCOPE, pfConc, scopeAssumps, concFormula); if (Trace.isOn("pfee-proof") || Trace.isOn("pfee-proof-final")) |