diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 8 | ||||
| -rw-r--r-- | src/smt/term_formula_removal.cpp | 5 | ||||
| -rw-r--r-- | src/smt/witness_form.cpp | 7 |
3 files changed, 8 insertions, 12 deletions
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 0c2f8ccf8..a7723d265 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -460,8 +460,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // add previous rewrite steps for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { - // not necessarily closed, so we pass false to addRewriteStep. - tcg.addRewriteStep(vvec[j], svec[j], pgs[j], false); + tcg.addRewriteStep(vvec[j], svec[j], pgs[j]); } // get the proof for the update to the current substitution Node seqss = subs.eqNode(ss); @@ -506,8 +505,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, true); for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { - // not necessarily closed, so we pass false to addRewriteStep. - tcpg.addRewriteStep(vvec[j], svec[j], pgs[j], false); + tcpg.addRewriteStep(vvec[j], svec[j], pgs[j]); } // add the proof constructed by the term conversion utility std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(eq); @@ -545,10 +543,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, Node eq = args[0].eqNode(ret); if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT) { - // rewrites from theory::Rewriter // automatically expand THEORY_REWRITE as well here if set bool elimTR = (d_elimRules.find(PfRule::THEORY_REWRITE) != d_elimRules.end()); + // rewrites from theory::Rewriter bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT); // use rewrite with proof interface Rewriter* rr = d_smte->getRewriter(); diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index cf7c00e2b..46135f12a 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -334,10 +334,9 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr, ProofGenerator* expg = sm->getProofGenerator(existsAssertion); d_lp->addLazyStep(existsAssertion, expg, + PfRule::WITNESS_AXIOM, true, - "RemoveTermFormulas::run:skolem_pf", - false, - PfRule::WITNESS_AXIOM); + "RemoveTermFormulas::run:skolem_pf"); d_lp->addStep(newAssertion, PfRule::SKOLEMIZE, {existsAssertion}, {}); newAssertionPg = d_lp.get(); } diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index e4f0a56dc..9c2c035a8 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -114,12 +114,11 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) d_wintroPf.addLazyStep( exists, pg, + PfRule::WITNESS_AXIOM, true, - "WitnessFormGenerator::convertToWitnessForm:witness_axiom", - false, - PfRule::WITNESS_AXIOM); + "WitnessFormGenerator::convertToWitnessForm:witness_axiom"); d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {}); - d_tcpg.addRewriteStep(cur, curw, &d_wintroPf); + d_tcpg.addRewriteStep(cur, curw, &d_wintroPf, PfRule::ASSUME, true); } else { |