summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/smt/term_formula_removal.cpp118
-rw-r--r--src/smt/term_formula_removal.h29
-rw-r--r--src/theory/theory_preprocessor.cpp9
3 files changed, 103 insertions, 53 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 4b519f06a..ae3039ffa 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -50,14 +50,77 @@ RemoveTermFormulas::~RemoveTermFormulas() {}
theory::TrustNode RemoveTermFormulas::run(
Node assertion,
std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems)
+ std::vector<Node>& newSkolems,
+ bool fixedPoint)
{
Node itesRemoved = runInternal(assertion, newAsserts, newSkolems);
+ Assert(newAsserts.size() == newSkolems.size());
+ if (itesRemoved == assertion)
+ {
+ return theory::TrustNode::null();
+ }
+ // if running to fixed point, we run each new assertion through the
+ // run lemma method
+ if (fixedPoint)
+ {
+ size_t i = 0;
+ std::unordered_set<Node, NodeHashFunction> processed;
+ while (i < newAsserts.size())
+ {
+ theory::TrustNode trn = newAsserts[i];
+ AlwaysAssert(processed.find(trn.getProven()) == processed.end());
+ processed.insert(trn.getProven());
+ // do not run to fixed point on subcall, since we are processing all
+ // lemmas in this loop
+ newAsserts[i] = runLemma(trn, newAsserts, newSkolems, false);
+ i++;
+ }
+ }
// The rewriting of assertion can be justified by the term conversion proof
// generator d_tpg.
return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
}
+theory::TrustNode RemoveTermFormulas::runLemma(
+ theory::TrustNode lem,
+ std::vector<theory::TrustNode>& newAsserts,
+ std::vector<Node>& newSkolems,
+ bool fixedPoint)
+{
+ theory::TrustNode trn =
+ run(lem.getProven(), newAsserts, newSkolems, fixedPoint);
+ if (trn.isNull())
+ {
+ // no change
+ return lem;
+ }
+ Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
+ Node newAssertion = trn.getNode();
+ if (!isProofEnabled())
+ {
+ // proofs not enabled, just take result
+ return theory::TrustNode::mkTrustLemma(newAssertion, nullptr);
+ }
+ Trace("rtf-proof-debug")
+ << "RemoveTermFormulas::run: setup proof for processed new lemma"
+ << std::endl;
+ Node assertionPre = lem.getProven();
+ Node naEq = trn.getProven();
+ // this method is applying this method to TrustNode whose generator is
+ // already d_lp (from the run method above), in which case this link is
+ // not necessary.
+ if (trn.getGenerator() != d_lp.get())
+ {
+ d_lp->addLazyStep(naEq, trn.getGenerator());
+ }
+ // ---------------- from input ------------------------------- from trn
+ // assertionPre assertionPre = newAssertion
+ // ------------------------------------------------------- EQ_RESOLVE
+ // newAssertion
+ d_lp->addStep(newAssertion, PfRule::EQ_RESOLVE, {assertionPre, naEq}, {});
+ return theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
+}
+
Node RemoveTermFormulas::runInternal(Node assertion,
std::vector<theory::TrustNode>& output,
std::vector<Node>& newSkolems)
@@ -91,10 +154,18 @@ Node RemoveTermFormulas::runInternal(Node assertion,
if (!processedChildren.back())
{
// check if we should replace the current node
- Node currt = runCurrent(curr, output, newSkolems);
- // if null, we need to recurse
+ theory::TrustNode newLem;
+ Node currt = runCurrent(curr, newLem);
+ // if we replaced by a skolem, we do not recurse
if (!currt.isNull())
{
+ // if this is the first time we've seen this term, we have a new lemma
+ // which we add to our vectors
+ if (!newLem.isNull())
+ {
+ output.push_back(newLem);
+ newSkolems.push_back(currt);
+ }
Trace("rtf-debug") << "...replace by skolem" << std::endl;
d_tfCache.insert(curr, currt);
ctx.pop();
@@ -165,14 +236,9 @@ Node RemoveTermFormulas::runInternal(Node assertion,
}
Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
- std::vector<theory::TrustNode>& output,
- std::vector<Node>& newSkolems)
+ theory::TrustNode& newLem)
{
TNode node = curr.first;
- if (node.getKind() == kind::INST_PATTERN_LIST)
- {
- return Node(node);
- }
uint32_t cval = curr.second;
bool inQuant, inTerm;
RtfTermContext::getFlags(curr.second, inQuant, inTerm);
@@ -413,39 +479,11 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
Trace("rtf-debug") << "*** term formula removal introduced " << skolem
<< " for " << node << std::endl;
- // Remove ITEs from the new assertion, rewrite it and push it to the
- // output
- Node newAssertionPre = newAssertion;
- newAssertion = runInternal(newAssertion, output, newSkolems);
-
- if (isProofEnabled())
- {
- if (newAssertionPre != newAssertion)
- {
- Trace("rtf-proof-debug")
- << "RemoveTermFormulas::run: setup proof for processed new lemma"
- << std::endl;
- // for new assertions that rewrite recursively
- Node naEq = newAssertionPre.eqNode(newAssertion);
- d_lp->addLazyStep(naEq, d_tpg.get());
- // ---------------- from lp ------------------------------- from tpg
- // newAssertionPre newAssertionPre = newAssertion
- // ------------------------------------------------------- EQ_RESOLVE
- // newAssertion
- d_lp->addStep(
- newAssertion, PfRule::EQ_RESOLVE, {newAssertionPre, naEq}, {});
- }
- }
-
- theory::TrustNode trna =
- theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
+ newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
- trna.debugCheckClosed("rtf-proof-debug",
- "RemoveTermFormulas::run:new_assert");
-
- output.push_back(trna);
- newSkolems.push_back(skolem);
+ newLem.debugCheckClosed("rtf-proof-debug",
+ "RemoveTermFormulas::run:new_assert");
}
// The representation is now the skolem
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 4a5d4648e..e5453254c 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -83,13 +83,26 @@ class RemoveTermFormulas {
* @param newAsserts The new assertions corresponding to axioms for newly
* introduced skolems.
* @param newSkolems The skolems corresponding to each of the newAsserts.
+ * @param fixedPoint Whether to run term formula removal on the lemmas in
+ * newAsserts. This adds new assertions to this vector until a fixed
+ * point is reached. When this option is true, all lemmas in newAsserts
+ * have all term formulas removed.
* @return a trust node of kind TrustNodeKind::REWRITE whose
* right hand side is assertion after removing term formulas, and the proof
* generator (if provided) that can prove the equivalence.
*/
theory::TrustNode run(Node assertion,
std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems);
+ std::vector<Node>& newSkolems,
+ bool fixedPoint = false);
+ /**
+ * Same as above, but transforms a lemma, returning a LEMMA trust node that
+ * proves the same formula as lem with term formulas removed.
+ */
+ theory::TrustNode runLemma(theory::TrustNode lem,
+ std::vector<theory::TrustNode>& newAsserts,
+ std::vector<Node>& newSkolems,
+ bool fixedPoint = false);
/**
* Get proof generator that is responsible for all proofs for removing term
@@ -179,14 +192,14 @@ class RemoveTermFormulas {
/**
* This is called on curr of the form (t, val) where t is a term and val is
* a term context identifier computed by RtfTermContext. If curr should be
- * replaced by a skolem, this method returns this skolem k, adds k to
- * newSkolems and adds the axiom defining that skolem to newAsserts, where
- * runInternal is called on that axiom. Otherwise, this method returns the
- * null node.
+ * replaced by a skolem, this method returns this skolem k. If this was the
+ * first time that t was encountered, we set newLem to the lemma for the
+ * skolem that axiomatizes k.
+ *
+ * Otherwise, if t should not be replaced in the term context, this method
+ * returns the null node.
*/
- Node runCurrent(std::pair<Node, uint32_t>& curr,
- std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems);
+ Node runCurrent(std::pair<Node, uint32_t>& curr, theory::TrustNode& newLem);
/** Whether proofs are enabled */
bool isProofEnabled() const;
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 179ecc130..7c917dff5 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -100,14 +100,13 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
ppNode = tpp.getNode();
}
- // Remove the ITEs
- TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems);
- Node rtfNode = ttfr.getNode();
+ // Remove the ITEs, fixed point
+ TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, true);
+ Node rtfNode = ttfr.isNull() ? ppNode : ttfr.getNode();
if (Debug.isOn("lemma-ites"))
{
- Debug("lemma-ites") << "removed ITEs from lemma: " << ttfr.getNode()
- << endl;
+ Debug("lemma-ites") << "removed ITEs from lemma: " << rtfNode << endl;
Debug("lemma-ites") << " + now have the following " << newLemmas.size()
<< " lemma(s):" << endl;
for (size_t i = 0, lsize = newLemmas.size(); i <= lsize; ++i)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback