diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 23 | ||||
-rw-r--r-- | src/theory/uf/proof_equality_engine.h | 2 |
2 files changed, 13 insertions, 12 deletions
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 021a737c0..66c36ed95 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -260,9 +260,8 @@ TrustNode ProofEqEngine::assertConflict(PfRule id, { 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, @@ -270,15 +269,15 @@ 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, diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 314353131..e1105623a 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -180,6 +180,8 @@ class ProofEqEngine : public EagerProofGenerator 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 |