summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/lazy_proof.cpp4
-rw-r--r--src/expr/lazy_proof.h14
-rw-r--r--src/expr/term_conversion_proof_generator.cpp10
-rw-r--r--src/expr/term_conversion_proof_generator.h5
-rw-r--r--src/preprocessing/assertion_pipeline.cpp2
-rw-r--r--src/prop/proof_cnf_stream.cpp14
-rw-r--r--src/smt/proof_post_processor.cpp8
-rw-r--r--src/smt/term_formula_removal.cpp5
-rw-r--r--src/smt/witness_form.cpp7
-rw-r--r--src/theory/quantifiers/instantiate.cpp10
-rw-r--r--src/theory/theory_engine.cpp5
-rw-r--r--src/theory/theory_preprocessor.cpp8
-rw-r--r--src/theory/trust_substitutions.cpp18
-rw-r--r--src/theory/trust_substitutions.h4
-rw-r--r--src/theory/uf/proof_equality_engine.cpp8
15 files changed, 64 insertions, 58 deletions
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index a96e30fde..267da2607 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -133,10 +133,10 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
void LazyCDProof::addLazyStep(Node expected,
ProofGenerator* pg,
+ PfRule idNull,
bool isClosed,
const char* ctx,
- bool forceOverwrite,
- PfRule idNull)
+ bool forceOverwrite)
{
if (pg == nullptr)
{
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index 691902945..e2bba3015 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -67,23 +67,23 @@ class LazyCDProof : public CDProof
*
* @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.
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index 11e8eb054..02613345f 100644
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -62,13 +62,17 @@ TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
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);
}
}
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index 184f24e13..0a1f4e70a 100644
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -144,6 +144,8 @@ class TConvProofGenerator : public ProofGenerator
/**
* 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
@@ -154,7 +156,8 @@ class TConvProofGenerator : public ProofGenerator
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);
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 78c459cb7..cd7aadf9a 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -177,7 +177,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
// 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
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();
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
{
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index f88c2e7a0..8549b1eae 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -268,10 +268,9 @@ bool Instantiate::addInstantiation(
// 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}, {});
}
}
@@ -477,10 +476,9 @@ Node Instantiate::getInstantiation(Node q,
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;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index aaa010148..924d045da 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1462,10 +1462,9 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
{
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
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index e7cdb8f2c..b37a45967 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -213,10 +213,9 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
// 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},
@@ -433,7 +432,8 @@ Node TheoryPreprocessor::preprocessWithProof(Node term)
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
{
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index 482c487eb..27159f964 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -54,12 +54,7 @@ void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
// 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);
}
}
@@ -79,7 +74,9 @@ void TrustSubstitutionMap::addSubstitution(TNode x,
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()
@@ -89,7 +86,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
// 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();
@@ -100,7 +97,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
// 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
@@ -109,7 +106,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
// 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());
@@ -117,6 +114,7 @@ void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
// link the given generator
solvePg->addLazyStep(proven, tn.getGenerator());
addSubstitution(x, t, solvePg);
+ return solvePg;
}
void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index 91555ee56..d7f48d054 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -68,8 +68,10 @@ class TrustSubstitutionMap
* 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.
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 77ee1effd..184584aa9 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -68,7 +68,7 @@ bool ProofEqEngine::assertFact(Node lit,
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);
@@ -116,7 +116,7 @@ bool ProofEqEngine::assertFact(Node lit,
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);
}
@@ -140,7 +140,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
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);
}
@@ -157,7 +157,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg)
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback