This PR makes it so that theory-preprocessing is always called on lemmas. It simplifies the proof production in the theory preprocessor accordingly.
Additionally, it ensures that our theory-preprocessor is run on lemmas that are generated from term formula removal. Previously, this was not the case and in fact certain lemmas (e.g. literals within witness terms that are not in preprocessed form) would escape and be asserted to TheoryEngine. This was uncovered by a unit test failure, the corresponding regression is added in this PR.
It adds a new interface removeItes to PropEngine which is required for the (deprecated) preprocessing pass removeItes.
This PR now makes the lemma propery PREPROCESS obsolete. Further simplification is possible after this PR in non-linear arithmetic and quantifiers, where it is not necessary to distinguish 2 caches for preprocessed vs. non-preprocessed lemmas.
Node assertion = (*assertions)[i];
std::vector<theory::TrustNode> newAsserts;
std::vector<Node> newSkolems;
- TrustNode trn = pe->preprocess(assertion, newAsserts, newSkolems, false);
+ TrustNode trn = pe->removeItes(assertion, newAsserts, newSkolems);
if (!trn.isNull())
{
// process
assertions->replaceTrusted(i, trn);
- // rewritten assertion has a dependence on the node (old pf architecture)
- if (options::unsatCores() && !options::proofNew())
- {
- ProofManager::currentPM()->addDependence(trn.getNode(), assertion);
- }
}
Assert(newSkolems.size() == newAsserts.size());
for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
Node assertion = (*assertions)[i];
std::vector<theory::TrustNode> newAsserts;
std::vector<Node> newSkolems;
- TrustNode trn =
- propEngine->preprocess(assertion, newAsserts, newSkolems, true);
+ TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems);
if (!trn.isNull())
{
// process
assertions->replaceTrusted(i, trn);
- // rewritten assertion has a dependence on the node (old pf architecture)
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(trn.getNode(), assertion);
- }
}
Assert(newSkolems.size() == newAsserts.size());
for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
theory::TrustNode PropEngine::preprocess(
TNode node,
std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems,
- bool doTheoryPreprocess)
+ std::vector<Node>& newSkolems)
{
- return d_theoryProxy->preprocess(
- node, newLemmas, newSkolems, doTheoryPreprocess);
+ return d_theoryProxy->preprocess(node, newLemmas, newSkolems);
+}
+
+theory::TrustNode PropEngine::removeItes(
+ TNode node,
+ std::vector<theory::TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems)
+{
+ return d_theoryProxy->removeItes(node, newLemmas, newSkolems);
}
void PropEngine::notifyPreprocessedAssertions(
Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
{
bool removable = isLemmaPropertyRemovable(p);
- bool preprocess = isLemmaPropertyPreprocess(p);
// call preprocessor
std::vector<theory::TrustNode> ppLemmas;
std::vector<Node> ppSkolems;
theory::TrustNode tplemma =
- d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems, preprocess);
+ d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems);
Assert(ppSkolems.size() == ppLemmas.size());
// must preprocess
std::vector<theory::TrustNode> newLemmas;
std::vector<Node> newSkolems;
- theory::TrustNode tpn =
- d_theoryProxy->preprocess(n, newLemmas, newSkolems, true);
+ theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
// send lemmas corresponding to the skolems introduced by preprocessing n
for (const theory::TrustNode& tnl : newLemmas)
{
* @param node The assertion to preprocess,
* @param ppLemmas The lemmas to add to the set of assertions,
* @param ppSkolems The skolems that newLemmas correspond to,
- * @param doTheoryPreprocess whether to run theory-specific preprocessing.
* @return The (REWRITE) trust node corresponding to rewritten node via
* preprocessing.
*/
theory::TrustNode preprocess(TNode node,
std::vector<theory::TrustNode>& ppLemmas,
- std::vector<Node>& ppSkolems,
- bool doTheoryPreprocess);
-
+ std::vector<Node>& ppSkolems);
+ /**
+ * Remove term ITEs (and more generally, term formulas) from the given node.
+ * Return the REWRITE trust node corresponding to rewriting node. New lemmas
+ * and skolems are added to ppLemmas and ppSkolems respectively. This can
+ * be seen a subset of the above preprocess method, which also does theory
+ * preprocessing and rewriting.
+ *
+ * @param node The assertion to preprocess,
+ * @param ppLemmas The lemmas to add to the set of assertions,
+ * @param ppSkolems The skolems that newLemmas correspond to,
+ * @return The (REWRITE) trust node corresponding to rewritten node via
+ * preprocessing.
+ */
+ theory::TrustNode removeItes(TNode node,
+ std::vector<theory::TrustNode>& ppLemmas,
+ std::vector<Node>& ppSkolems);
/**
* Notify preprocessed assertions. This method is called just before the
* assertions are asserted to this prop engine. This method notifies the
theory::TrustNode TheoryProxy::preprocessLemma(
theory::TrustNode trn,
std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems,
- bool doTheoryPreprocess)
+ std::vector<Node>& newSkolems)
{
- return d_tpp.preprocessLemma(
- trn, newLemmas, newSkolems, doTheoryPreprocess, true);
+ return d_tpp.preprocessLemma(trn, newLemmas, newSkolems);
}
theory::TrustNode TheoryProxy::preprocess(
TNode node,
std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems,
- bool doTheoryPreprocess)
+ std::vector<Node>& newSkolems)
{
- theory::TrustNode pnode =
- d_tpp.preprocess(node, newLemmas, newSkolems, doTheoryPreprocess, true);
- return pnode;
+ return d_tpp.preprocess(node, newLemmas, newSkolems);
+}
+
+theory::TrustNode TheoryProxy::removeItes(
+ TNode node,
+ std::vector<theory::TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems)
+{
+ RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
+ return rtf.run(node, newLemmas, newSkolems, true);
}
void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
*/
theory::TrustNode preprocessLemma(theory::TrustNode trn,
std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems,
- bool doTheoryPreprocess);
+ std::vector<Node>& newSkolems);
/**
* Call the preprocessor on node, return trust node corresponding to the
* rewrite.
*/
theory::TrustNode preprocess(TNode node,
std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems,
- bool doTheoryPreprocess);
+ std::vector<Node>& newSkolems);
+ /**
+ * Remove ITEs from the node.
+ */
+ theory::TrustNode removeItes(TNode node,
+ std::vector<theory::TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems);
/** Preregister term */
void preRegister(Node n) override;
&d_iqtc)
: nullptr),
d_tspg(nullptr),
- d_tpgRew(pnm ? new TConvProofGenerator(pnm,
- userContext,
- TConvPolicy::FIXPOINT,
- TConvCachePolicy::NEVER,
- "TheoryPreprocessor::rewrite")
- : nullptr),
- d_tspgNoPp(nullptr),
d_lp(pnm ? new LazyCDProof(pnm,
nullptr,
userContext,
ts.push_back(d_tpg.get());
d_tspg.reset(new TConvSeqProofGenerator(
pnm, ts, userContext, "TheoryPreprocessor::sequence"));
- // Make the "no preprocess" term conversion sequence generator, which
- // applies only steps (2) and (3), where notice (3) must use the
- // "pure rewrite" term conversion (d_tpgRew).
- std::vector<ProofGenerator*> tsNoPp;
- tsNoPp.push_back(d_tfr.getTConvProofGenerator());
- tsNoPp.push_back(d_tpgRew.get());
- d_tspgNoPp.reset(new TConvSeqProofGenerator(
- pnm, tsNoPp, userContext, "TheoryPreprocessor::sequence_no_pp"));
}
}
TrustNode TheoryPreprocessor::preprocess(TNode node,
std::vector<TrustNode>& newLemmas,
- std::vector<Node>& newSkolems,
- bool doTheoryPreprocess,
- bool fixedPoint)
+ std::vector<Node>& newSkolems)
+{
+ return preprocessInternal(node, newLemmas, newSkolems, true);
+}
+
+TrustNode TheoryPreprocessor::preprocessInternal(
+ TNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems,
+ bool procLemmas)
{
// In this method, all rewriting steps of node are stored in d_tpg.
Trace("tpp-debug") << "TheoryPreprocessor::preprocess: start " << node
- << ", doTheoryPreprocess=" << doTheoryPreprocess
<< std::endl;
- // Run theory preprocessing, maybe
- Node ppNode = node;
- if (doTheoryPreprocess)
- {
- // run theory preprocessing
- TrustNode tpp = theoryPreprocess(node);
- ppNode = tpp.getNode();
- }
+ // run theory preprocessing
+ TrustNode tpp = theoryPreprocess(node);
+ Node ppNode = tpp.getNode();
// Remove the ITEs, fixed point
- TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, fixedPoint);
+ TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, true);
Node rtfNode = ttfr.isNull() ? ppNode : ttfr.getNode();
if (Debug.isOn("lemma-ites"))
Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
<< std::endl;
// no change
- Assert(newLemmas.empty());
return TrustNode::null();
}
{
std::vector<Node> cterms;
cterms.push_back(node);
- if (doTheoryPreprocess)
- {
- cterms.push_back(ppNode);
- }
+ cterms.push_back(ppNode);
cterms.push_back(rtfNode);
cterms.push_back(retNode);
// We have that:
- // node -> ppNode via preprocessing + rewriting (if doTheoryPreprocess)
+ // node -> ppNode via preprocessing + rewriting
// ppNode -> rtfNode via term formula removal
// rtfNode -> retNode via rewriting
- if (!doTheoryPreprocess)
- {
- // If preprocessing is not performed, we cannot use the main sequence
- // generator, instead we use d_tspgNoPp.
- // We register the top-level rewrite in the pure rewrite term converter.
- d_tpgRew->addRewriteStep(
- rtfNode, retNode, PfRule::REWRITE, {}, {rtfNode});
- // Now get the trust node from the sequence generator
- tret = d_tspgNoPp->mkTrustRewriteSequence(cterms);
- }
- else
- {
- // we wil use the sequence generator
- tret = d_tspg->mkTrustRewriteSequence(cterms);
- }
+ tret = d_tspg->mkTrustRewriteSequence(cterms);
tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
}
else
}
Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
<< tret.getNode() << std::endl;
+ if (procLemmas)
+ {
+ // Also must preprocess the new lemmas. This is especially important for
+ // formulas containing witness terms whose bodies are not in preprocessed
+ // form, as term formula removal introduces new lemmas for these that
+ // require theory-preprocessing.
+ size_t i = 0;
+ while (i < newLemmas.size())
+ {
+ TrustNode cur = newLemmas[i];
+ newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, false);
+ i++;
+ }
+ }
return tret;
}
-TrustNode TheoryPreprocessor::preprocess(TNode node, bool doTheoryPreprocess)
+TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems)
{
- // ignore lemmas, no fixed point
- std::vector<TrustNode> newLemmas;
- std::vector<Node> newSkolems;
- return preprocess(node, newLemmas, newSkolems, doTheoryPreprocess, false);
+ return preprocessLemmaInternal(node, newLemmas, newSkolems, true);
}
-TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
- std::vector<TrustNode>& newLemmas,
- std::vector<Node>& newSkolems,
- bool doTheoryPreprocess,
- bool fixedPoint)
+TrustNode TheoryPreprocessor::preprocessLemmaInternal(
+ TrustNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems,
+ bool procLemmas)
{
// what was originally proven
Node lemma = node.getProven();
TrustNode tplemma =
- preprocess(lemma, newLemmas, newSkolems, doTheoryPreprocess, fixedPoint);
+ preprocessInternal(lemma, newLemmas, newSkolems, procLemmas);
if (tplemma.isNull())
{
// no change needed
return TrustNode::mkTrustLemma(lemmap, d_lp.get());
}
-TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
- bool doTheoryPreprocess)
-{
- // ignore lemmas, no fixed point
- std::vector<TrustNode> newLemmas;
- std::vector<Node> newSkolems;
- return preprocessLemma(
- node, newLemmas, newSkolems, doTheoryPreprocess, false);
-}
-
RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas()
{
return d_tfr;
}
// Mark the substitution and continue
Node result = builder;
- if (result != current)
- {
- result = rewriteWithProof(result);
- }
+ // always rewrite here, since current may not be in rewritten form
+ result = rewriteWithProof(result);
Trace("theory::preprocess-debug")
<< "TheoryPreprocessor::theoryPreprocess(" << assertion
<< "): setting " << current << " -> " << result << endl;
* additional lemmas in newLemmas, which are trust nodes of kind
* TrustNodeKind::LEMMA. These correspond to e.g. lemmas corresponding to ITE
* removal. For each lemma in newLemmas, we add the corresponding skolem that
- * the lemma defines. The flag doTheoryPreprocess is whether we should run
- * theory-specific preprocessing.
+ * the lemma defines.
*
* @param node The assertion to preprocess,
* @param newLemmas The lemmas to add to the set of assertions,
* @param newSkolems The skolems that newLemmas correspond to,
- * @param doTheoryPreprocess whether to run theory-specific preprocessing.
* @return The (REWRITE) trust node corresponding to rewritten node via
* preprocessing.
*/
TrustNode preprocess(TNode node,
std::vector<TrustNode>& newLemmas,
- std::vector<Node>& newSkolems,
- bool doTheoryPreprocess,
- bool fixedPoint);
- /**
- * Same as above, without lemma tracking or fixed point. Lemmas for skolems
- * can be extracted from the RemoveTermFormulas utility.
- */
- TrustNode preprocess(TNode node, bool doTheoryPreprocess);
+ std::vector<Node>& newSkolems);
/**
* Same as above, but transforms the proof of node into a proof of the
* preprocessed node and returns the LEMMA trust node.
* @param node The assertion to preprocess,
* @param newLemmas The lemmas to add to the set of assertions,
* @param newSkolems The skolems that newLemmas correspond to,
- * @param doTheoryPreprocess whether to run theory-specific preprocessing.
* @return The (LEMMA) trust node corresponding to the proof of the rewritten
* form of the proven field of node.
*/
TrustNode preprocessLemma(TrustNode node,
std::vector<TrustNode>& newLemmas,
- std::vector<Node>& newSkolems,
- bool doTheoryPreprocess,
- bool fixedPoint);
- /**
- * Same as above, without lemma tracking or fixed point. Lemmas for skolems
- * can be extracted from the RemoveTermFormulas utility.
- */
- TrustNode preprocessLemma(TrustNode node, bool doTheoryPreprocess);
+ std::vector<Node>& newSkolems);
/** Get the term formula removal utility */
RemoveTermFormulas& getRemoveTermFormulas();
* parts of the node.
*/
TrustNode theoryPreprocess(TNode node);
+ /**
+ * Internal helper for preprocess, which also optionally preprocesses the
+ * new lemmas generated until a fixed point is reached based on argument
+ * procLemmas.
+ */
+ TrustNode preprocessInternal(TNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems,
+ bool procLemmas);
+ /**
+ * Internal helper for preprocessLemma, which also optionally preprocesses the
+ * new lemmas generated until a fixed point is reached based on argument
+ * procLemmas.
+ */
+ TrustNode preprocessLemmaInternal(TrustNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems,
+ bool procLemmas);
/** Reference to owning theory engine */
TheoryEngine& d_engine;
/** Logic info of theory engine */
* from d_tpg, which interleaves both preprocessing and rewriting.
*/
std::unique_ptr<TConvProofGenerator> d_tpgRew;
- /**
- * A term conversion sequence generator, which applies term formula removal
- * and rewriting in sequence. This is used for reconstruct proofs of
- * calls to preprocess where doTheoryPreprocess is false.
- */
- std::unique_ptr<TConvSeqProofGenerator> d_tspgNoPp;
/** A lazy proof, for additional lemmas. */
std::unique_ptr<LazyCDProof> d_lp;
/** Helper for theoryPreprocess */
regress1/quantifiers/smtlibf957ea.smt2
regress1/quantifiers/sygus-infer-nested.smt2
regress1/quantifiers/symmetric_unsat_7.smt2
+ regress1/quantifiers/tpp-unit-fail-qbv.smt2
regress1/quantifiers/var-eq-trigger.smt2
regress1/quantifiers/var-eq-trigger-simple.smt2
regress1/quantifiers/z3.620661-no-fv-trigger.smt2
--- /dev/null
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun t () (_ BitVec 4))
+(declare-fun s () (_ BitVec 4))
+(assert
+(distinct (bvult t (bvnot (bvneg s))) (exists ((BOUND_VARIABLE_273 (_ BitVec 4))) (bvugt (bvurem BOUND_VARIABLE_273 s) t)))
+)
+(check-sat)
projects / cvc5.git / commitdiff