diff options
| -rw-r--r-- | src/expr/proof_generator.cpp | 8 | ||||
| -rw-r--r-- | src/expr/proof_generator.h | 4 | ||||
| -rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 12 |
3 files changed, 18 insertions, 6 deletions
diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp index 2d114acd6..93f291e9a 100644 --- a/src/expr/proof_generator.cpp +++ b/src/expr/proof_generator.cpp @@ -43,7 +43,10 @@ std::shared_ptr<ProofNode> ProofGenerator::getProofFor(Node f) return nullptr; } -bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy) +bool ProofGenerator::addProofTo(Node f, + CDProof* pf, + CDPOverwrite opolicy, + bool doCopy) { Trace("pfgen") << "ProofGenerator::addProofTo: " << f << "..." << std::endl; Assert(pf != nullptr); @@ -52,8 +55,7 @@ bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy) if (apf != nullptr) { Trace("pfgen") << "...got proof " << *apf.get() << std::endl; - // Add the proof, without deep copying. - if (pf->addProof(apf, opolicy, false)) + if (pf->addProof(apf, opolicy, doCopy)) { Trace("pfgen") << "...success!" << std::endl; return true; diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index c53b7ff23..f2ce6c74b 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -82,11 +82,13 @@ class ProofGenerator * @param f The fact to get the proof for. * @param pf The CDProof object to add the proof to. * @param opolicy The overwrite policy for adding to pf. + * @param doCopy Whether to do a deep copy of the proof steps into pf. * @return True if this call was sucessful. */ virtual bool addProofTo(Node f, CDProof* pf, - CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY); + CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY, + bool doCopy = false); /** * Can we give the proof for formula f? This is used for debugging. This * returns false if the generator cannot provide a proof of formula f. diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 66c36ed95..323f8c6a2 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -376,8 +376,16 @@ TrustNode ProofEqEngine::assertLemma(Node conc, { curr = &tmpProof; } - // Register the proof step. - if (!pg->addProofTo(conc, curr)) + // 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. Notice this is very rarely more than a single step, but + // may be multiple steps if e.g. a theory inference corresponds to a + // sequence of more than one PfRule steps. + if (!pg->addProofTo(conc, curr, CDPOverwrite::ASSUME_ONLY, true)) { // a step went wrong, e.g. during checking Assert(false) << "pfee::assertConflict: register proof step"; |