diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-11-20 20:04:37 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-20 13:04:37 -0600 |
| commit | 20007b739555fe27a6600fcb4d156173bcc0eee3 (patch) | |
| tree | ac5b25d48fe713e0ab35839b7480d86a8cb1c2e1 /src/theory/trust_substitutions.cpp | |
| parent | de0d36b8972954c281f1e97b15d37c07a861cbc1 (diff) | |
(proof-new) Replace LazyCDProofSet by generic CDProofSet (#5487)
This PR replaces the LazyCDProofSet, that was hardcoded to use LazyCDProof objects, by a templated CDProofSet.
Diffstat (limited to 'src/theory/trust_substitutions.cpp')
| -rw-r--r-- | src/theory/trust_substitutions.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index 27159f964..aaa3b44f7 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -24,7 +24,8 @@ TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, std::string name, PfRule trustId, MethodId ids) - : d_subs(c), + : d_ctx(c), + d_subs(c), d_pnm(pnm), d_tsubs(c), d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr), @@ -68,7 +69,7 @@ void TrustSubstitutionMap::addSubstitution(TNode x, addSubstitution(x, t, nullptr); return; } - LazyCDProof* stepPg = d_helperPf.allocateProof(); + LazyCDProof* stepPg = d_helperPf.allocateProof(nullptr, d_ctx); Node eq = x.eqNode(t); stepPg->addStep(eq, id, {}, args); addSubstitution(x, t, stepPg); @@ -99,7 +100,7 @@ ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x, Trace("trust-subs") << "...use generator directly" << std::endl; return tn.getGenerator(); } - LazyCDProof* solvePg = d_helperPf.allocateProof(); + LazyCDProof* solvePg = d_helperPf.allocateProof(nullptr, d_ctx); // Try to transform tn.getProven() to (= x t) here, if necessary if (!d_tspb->applyPredTransform(proven, eq, {})) { |