diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-12 11:41:26 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-12 09:41:26 -0700 |
commit | 9d1ce085de6df543d9d9a2fa9b8fa9001feb4b6b (patch) | |
tree | 023474f131ee9f21e829fc623e31de808b9235d5 /src/expr/lazy_proof.cpp | |
parent | 3f77b4ac0d4ff8ab69e2f2932e9ced088bd339ed (diff) |
(proof-new) Witness form proof generator (#4782)
This class is responsible for the connection between terms and their witness form in the final proof.
Diffstat (limited to 'src/expr/lazy_proof.cpp')
-rw-r--r-- | src/expr/lazy_proof.cpp | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index 3980a3cb3..df0258af7 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -109,9 +109,24 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact) void LazyCDProof::addLazyStep(Node expected, ProofGenerator* pg, - bool forceOverwrite) + bool forceOverwrite, + PfRule idNull) { - Assert(pg != nullptr); + if (pg == nullptr) + { + // null generator, should have given a proof rule + if (idNull == PfRule::ASSUME) + { + Assert(false); + return; + } + Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected + << " set (trusted) step " << idNull << "\n"; + addStep(expected, idNull, {}, {expected}); + return; + } + Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected + << " set to generator " << pg->identify() << "\n"; if (!forceOverwrite) { NodeProofGeneratorMap::const_iterator it = d_gens.find(expected); |