diff options
-rw-r--r-- | src/smt/term_formula_removal.cpp | 118 | ||||
-rw-r--r-- | src/smt/term_formula_removal.h | 29 | ||||
-rw-r--r-- | src/theory/theory_preprocessor.cpp | 9 | ||||
-rw-r--r-- | test/regress/regress1/nl/nl_uf_lalt.smt2 | 2 |
4 files changed, 104 insertions, 54 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) diff --git a/test/regress/regress1/nl/nl_uf_lalt.smt2 b/test/regress/regress1/nl/nl_uf_lalt.smt2 index c5ccd322f..fc224d59a 100644 --- a/test/regress/regress1/nl/nl_uf_lalt.smt2 +++ b/test/regress/regress1/nl/nl_uf_lalt.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-unsat-cores +; COMMAND-LINE: --no-check-unsat-cores --decision=justification (set-logic QF_UFNIA) (set-info :status unsat) (declare-fun c (Int) Int) |