diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-20 15:20:35 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-20 15:20:35 -0500 |
| commit | 656004c54655ab15289d9e7666bda2e1c7bada1c (patch) | |
| tree | 23d53585f8204a30fe42b35e91824901e6dc4e2c /src/prop | |
| parent | 417299119500eac6a910fcb6b2109f4c129b355c (diff) | |
(proof-new) Update add lazy step interface in LazyCDProof (#5299)
Ensuring closed proofs should not be enabled by default, it is actually not used very often as a whole. Moreover, the "trust id" argument is the most useful argument and hence should come as the 3rd argument. This updates all uses of addLazyStep for the change in interface, also changes term conversion generator which had a similar issue with default arguments.
Notice that some calls to addLazyStep were checking closed but without providing a debug string, these I've left alone (they no longer check closed).
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/proof_cnf_stream.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index b2d33a61d..790e5aeb2 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -81,8 +81,11 @@ void ProofCnfStream::convertAndAssert(TNode node, Trace("cnf") << "ProofCnfStream::convertAndAssert: pg: " << pg->identify() << "\n"; Node toJustify = negated ? node.notNode() : static_cast<Node>(node); - d_proof.addLazyStep( - toJustify, pg, true, "ProofCnfStream::convertAndAssert:cnf"); + d_proof.addLazyStep(toJustify, + pg, + PfRule::ASSUME, + true, + "ProofCnfStream::convertAndAssert:cnf"); } convertAndAssert(node, negated); // process saved steps in buffer @@ -519,8 +522,11 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn) Assert(trn.getGenerator()->getProofFor(proven)->isClosed()); Trace("cnf-steps") << proven << " by explainPropagation " << trn.identifyGenerator() << std::endl; - d_proof.addLazyStep( - proven, trn.getGenerator(), true, "ProofCnfStream::convertPropagation"); + d_proof.addLazyStep(proven, + trn.getGenerator(), + PfRule::ASSUME, + true, + "ProofCnfStream::convertPropagation"); // since the propagation is added directly to the SAT solver via theoryProxy, // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here NodeManager* nm = NodeManager::currentNM(); |