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).
void LazyCDProof::addLazyStep(Node expected,
ProofGenerator* pg,
+ PfRule idNull,
bool isClosed,
const char* ctx,
- bool forceOverwrite,
- PfRule idNull)
+ bool forceOverwrite)
{
if (pg == nullptr)
{
*
* @param expected The fact that can be proven.
* @param pg The generator that can proof expected.
+ * @param trustId If a null proof generator is provided, we add a step to
+ * the proof that has trustId as the rule and expected as the sole argument.
+ * We do this only if trustId is not PfRule::ASSUME. This is primarily used
+ * for identifying the kind of hole when a proof generator is not given.
* @param isClosed Whether to expect that pg can provide a closed proof for
* this fact.
* @param ctx The context we are in (for debugging).
* @param forceOverwrite If this flag is true, then this call overwrites
* an existing proof generator provided for expected, if one was provided
* via a previous call to addLazyStep in the current context.
- * @param trustId If a null proof generator is provided, we add a step to
- * the proof that has trustId as the rule and expected as the sole argument.
- * We do this only if trustId is not PfRule::ASSUME. This is primarily used
- * for identifying the kind of hole when a proof generator is not given.
*/
void addLazyStep(Node expected,
ProofGenerator* pg,
- bool isClosed = true,
+ PfRule trustId = PfRule::ASSUME,
+ bool isClosed = false,
const char* ctx = "LazyCDProof::addLazyStep",
- bool forceOverwrite = false,
- PfRule trustId = PfRule::ASSUME);
+ bool forceOverwrite = false);
/**
* Does this have any proof generators? This method always returns true
* if the default is non-null.
TConvProofGenerator::~TConvProofGenerator() {}
-void TConvProofGenerator::addRewriteStep(
- Node t, Node s, ProofGenerator* pg, bool isClosed, uint32_t tctx)
+void TConvProofGenerator::addRewriteStep(Node t,
+ Node s,
+ ProofGenerator* pg,
+ PfRule trustId,
+ bool isClosed,
+ uint32_t tctx)
{
Node eq = registerRewriteStep(t, s, tctx);
if (!eq.isNull())
{
- d_proof.addLazyStep(eq, pg, isClosed);
+ d_proof.addLazyStep(eq, pg, trustId, isClosed);
}
}
/**
* Add rewrite step t --> s based on proof generator.
*
+ * @param trustId If a null proof generator is provided, we add a step to
+ * the proof that has trustId as the rule and expected as the sole argument.
* @param isClosed whether to expect that pg can provide a closed proof for
* this fact.
* @param tctx The term context identifier for the rewrite step. This
void addRewriteStep(Node t,
Node s,
ProofGenerator* pg,
- bool isClosed = true,
+ PfRule trustId = PfRule::ASSUME,
+ bool isClosed = false,
uint32_t tctx = 0);
/** Same as above, for a single step */
void addRewriteStep(Node t, Node s, ProofStep ps, uint32_t tctx = 0);
// rewrite( d_nodes[i] ^ n )
// allocate a fresh proof which will act as the proof generator
LazyCDProof* lcp = d_pppg->allocateHelperProof();
- lcp->addLazyStep(n, pg, false);
+ lcp->addLazyStep(n, pg, PfRule::PREPROCESS);
if (d_nodes[i].isConst() && d_nodes[i].getConst<bool>())
{
// skip the AND_INTRO if the previous d_nodes[i] was true
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
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();
// 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);
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);
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();
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();
}
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
{
// add the transformation proof, or THEORY_PREPROCESS if none provided
pfTmp->addLazyStep(proven,
tpBody.getGenerator(),
+ PfRule::THEORY_PREPROCESS,
true,
- "Instantiate::getInstantiation:qpreprocess",
- false,
- PfRule::THEORY_PREPROCESS);
+ "Instantiate::getInstantiation:qpreprocess");
pfTmp->addStep(body, PfRule::EQ_RESOLVE, {orig_body, proven}, {});
}
}
Node proven = trn.getProven();
pf->addLazyStep(proven,
trn.getGenerator(),
+ PfRule::THEORY_PREPROCESS,
true,
- "Instantiate::getInstantiation:rewrite_inst",
- false,
- PfRule::THEORY_PREPROCESS);
+ "Instantiate::getInstantiation:rewrite_inst");
pf->addStep(newBody, PfRule::EQ_RESOLVE, {body, proven}, {});
}
body = newBody;
{
d_lazyProof->addLazyStep(tplemma.getProven(),
tplemma.getGenerator(),
+ PfRule::PREPROCESS_LEMMA,
true,
- "TheoryEngine::lemma_pp",
- false,
- PfRule::PREPROCESS_LEMMA);
+ "TheoryEngine::lemma_pp");
// ---------- from d_lazyProof -------------- from theory preprocess
// lemma lemma = lemmap
// ------------------------------------------ EQ_RESOLVE
// store in the lazy proof
d_lp->addLazyStep(assertion,
trn.getGenerator(),
+ PfRule::THEORY_PREPROCESS_LEMMA,
true,
- "TheoryPreprocessor::rewrite_lemma_new",
- false,
- PfRule::THEORY_PREPROCESS_LEMMA);
+ "TheoryPreprocessor::rewrite_lemma_new");
d_lp->addStep(rewritten,
PfRule::MACRO_SR_PRED_TRANSFORM,
{assertion},
trn.debugCheckClosed("tpp-proof-debug",
"TheoryPreprocessor::preprocessWithProof");
// always use term context hash 0 (default)
- d_tpg->addRewriteStep(term, termr, trn.getGenerator());
+ d_tpg->addRewriteStep(
+ term, termr, trn.getGenerator(), PfRule::ASSUME, true);
}
else
{
// current substitution node is no longer valid.
d_currentSubs = Node::null();
// add to lazy proof
- d_subsPg->addLazyStep(tnl.getProven(),
- pg,
- false,
- "TrustSubstitutionMap::addSubstitution",
- false,
- d_trustId);
+ d_subsPg->addLazyStep(tnl.getProven(), pg, d_trustId);
}
}
addSubstitution(x, t, stepPg);
}
-void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
+ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x,
+ TNode t,
+ TrustNode tn)
{
Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add "
<< x << " -> " << t << " from " << tn.getProven()
// no generator or not proof enabled, nothing to do
addSubstitution(x, t, nullptr);
Trace("trust-subs") << "...no proof" << std::endl;
- return;
+ return nullptr;
}
Node eq = x.eqNode(t);
Node proven = tn.getProven();
// no rewrite required, just use the generator
addSubstitution(x, t, tn.getGenerator());
Trace("trust-subs") << "...use generator directly" << std::endl;
- return;
+ return tn.getGenerator();
}
LazyCDProof* solvePg = d_helperPf.allocateProof();
// Try to transform tn.getProven() to (= x t) here, if necessary
// failed to rewrite
addSubstitution(x, t, nullptr);
Trace("trust-subs") << "...failed to rewrite" << std::endl;
- return;
+ return nullptr;
}
Trace("trust-subs") << "...successful rewrite" << std::endl;
solvePg->addSteps(*d_tspb.get());
// link the given generator
solvePg->addLazyStep(proven, tn.getGenerator());
addSubstitution(x, t, solvePg);
+ return solvePg;
}
void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
* based on transforming the tn.getProven() to (= x t) if tn has a
* non-null proof generator; otherwise if tn has no proof generator
* we simply add the substitution.
+ *
+ * @return The proof generator that can prove (= x t).
*/
- void addSubstitutionSolved(TNode x, TNode t, TrustNode tn);
+ ProofGenerator* addSubstitutionSolved(TNode x, TNode t, TrustNode tn);
/**
* Add substitutions from trust substitution map t. This adds all
* substitutions from the map t and carries over its information about proofs.
ps.d_args = args;
d_factPg.addStep(lit, ps);
// add lazy step to proof
- d_proof.addLazyStep(lit, &d_factPg, false);
+ d_proof.addLazyStep(lit, &d_factPg);
// second, assert it to the equality engine
Node reason = NodeManager::currentNM()->mkAnd(exp);
return assertFactInternal(atom, polarity, reason);
ps.d_args = args;
d_factPg.addStep(lit, ps);
// add lazy step to proof
- d_proof.addLazyStep(lit, &d_factPg, false);
+ d_proof.addLazyStep(lit, &d_factPg);
// second, assert it to the equality engine
return assertFactInternal(atom, polarity, exp);
}
d_factPg.addStep(step.first, step.second);
}
// add lazy step to proof
- d_proof.addLazyStep(lit, &d_factPg, false);
+ d_proof.addLazyStep(lit, &d_factPg);
// second, assert it to the equality engine
return assertFactInternal(atom, polarity, exp);
}
return false;
}
// note the proof generator is responsible for remembering the explanation
- d_proof.addLazyStep(lit, pg, false);
+ d_proof.addLazyStep(lit, pg);
// second, assert it to the equality engine
return assertFactInternal(atom, polarity, exp);
}
projects / cvc5.git / commitdiff