From e9cffe98e1ef34cde01e7778fc2be55839044007 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 7 Oct 2021 11:49:41 -0500 Subject: Use skolem lemma in prop layer interfaces (#7320) --- src/preprocessing/passes/ite_removal.cpp | 12 +++--- src/preprocessing/passes/theory_preprocess.cpp | 12 +++--- src/prop/prop_engine.cpp | 56 +++++++++++--------------- src/prop/prop_engine.h | 26 +++++------- src/prop/theory_proxy.cpp | 17 ++++---- src/prop/theory_proxy.h | 11 ++--- src/smt/term_formula_removal.cpp | 33 +++++---------- src/smt/term_formula_removal.h | 17 ++------ src/theory/skolem_lemma.cpp | 2 + src/theory/skolem_lemma.h | 2 + src/theory/theory_preprocessor.cpp | 45 +++++++-------------- src/theory/theory_preprocessor.h | 17 +++----- 12 files changed, 93 insertions(+), 157 deletions(-) (limited to 'src') diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 97e56c58c..c7ec46337 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -47,19 +47,17 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) for (unsigned i = 0, size = assertions->size(); i < size; ++i) { Node assertion = (*assertions)[i]; - std::vector newAsserts; - std::vector newSkolems; - TrustNode trn = pe->removeItes(assertion, newAsserts, newSkolems); + std::vector newAsserts; + TrustNode trn = pe->removeItes(assertion, newAsserts); if (!trn.isNull()) { // process assertions->replaceTrusted(i, trn); } - Assert(newSkolems.size() == newAsserts.size()); - for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) + for (const SkolemLemma& lem : newAsserts) { - imap[assertions->size()] = newSkolems[j]; - assertions->pushBackTrusted(newAsserts[j]); + imap[assertions->size()] = lem.d_skolem; + assertions->pushBackTrusted(lem.d_lemma); } } for (unsigned i = 0, size = assertions->size(); i < size; ++i) diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 641cab162..2f9d12637 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -44,19 +44,17 @@ PreprocessingPassResult TheoryPreprocess::applyInternal( for (unsigned i = 0, size = assertions->size(); i < size; ++i) { Node assertion = (*assertions)[i]; - std::vector newAsserts; - std::vector newSkolems; - TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems); + std::vector newAsserts; + TrustNode trn = propEngine->preprocess(assertion, newAsserts); if (!trn.isNull()) { // process assertions->replaceTrusted(i, trn); } - Assert(newSkolems.size() == newAsserts.size()); - for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) + for (const SkolemLemma& lem : newAsserts) { - imap[assertions->size()] = newSkolems[j]; - assertions->pushBackTrusted(newAsserts[j]); + imap[assertions->size()] = lem.d_skolem; + assertions->pushBackTrusted(lem.d_lemma); } } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 5bd719fe9..6f8bbe997 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -161,17 +161,15 @@ PropEngine::~PropEngine() { } TrustNode PropEngine::preprocess(TNode node, - std::vector& newLemmas, - std::vector& newSkolems) + std::vector& newLemmas) { - return d_theoryProxy->preprocess(node, newLemmas, newSkolems); + return d_theoryProxy->preprocess(node, newLemmas); } TrustNode PropEngine::removeItes(TNode node, - std::vector& newLemmas, - std::vector& newSkolems) + std::vector& newLemmas) { - return d_theoryProxy->removeItes(node, newLemmas, newSkolems); + return d_theoryProxy->removeItes(node, newLemmas); } void PropEngine::assertInputFormulas( @@ -210,12 +208,8 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p) bool removable = isLemmaPropertyRemovable(p); // call preprocessor - std::vector ppLemmas; - std::vector ppSkolems; - TrustNode tplemma = - d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems); - - Assert(ppSkolems.size() == ppLemmas.size()); + std::vector ppLemmas; + TrustNode tplemma = d_theoryProxy->preprocessLemma(tlemma, ppLemmas); // do final checks on the lemmas we are about to send if (isProofEnabled() @@ -224,25 +218,25 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p) Assert(tplemma.getGenerator() != nullptr); // ensure closed, make the proof node eagerly here to debug tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma"); - for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) + for (theory::SkolemLemma& lem : ppLemmas) { - Assert(ppLemmas[i].getGenerator() != nullptr); - ppLemmas[i].debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new"); + Assert(lem.d_lemma.getGenerator() != nullptr); + lem.d_lemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new"); } } if (Trace.isOn("te-lemma")) { Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl; - for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) + for (const theory::SkolemLemma& lem : ppLemmas) { - Trace("te-lemma") << "Lemma, new lemma: " << ppLemmas[i].getProven() - << " (skolem is " << ppSkolems[i] << ")" << std::endl; + Trace("te-lemma") << "Lemma, new lemma: " << lem.d_lemma.getProven() + << " (skolem is " << lem.d_skolem << ")" << std::endl; } } // now, assert the lemmas - assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable); + assertLemmasInternal(tplemma, ppLemmas, removable); } void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable) @@ -296,18 +290,18 @@ void PropEngine::assertInternal( } } -void PropEngine::assertLemmasInternal(TrustNode trn, - const std::vector& ppLemmas, - const std::vector& ppSkolems, - bool removable) +void PropEngine::assertLemmasInternal( + TrustNode trn, + const std::vector& ppLemmas, + bool removable) { if (!trn.isNull()) { assertTrustedLemmaInternal(trn, removable); } - for (const TrustNode& tnl : ppLemmas) + for (const theory::SkolemLemma& lem : ppLemmas) { - assertTrustedLemmaInternal(tnl, removable); + assertTrustedLemmaInternal(lem.d_lemma, removable); } // assert to decision engine if (!removable) @@ -318,10 +312,9 @@ void PropEngine::assertLemmasInternal(TrustNode trn, // notify the theory proxy of the lemma d_theoryProxy->notifyAssertion(trn.getProven()); } - Assert(ppSkolems.size() == ppLemmas.size()); - for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) + for (const theory::SkolemLemma& lem : ppLemmas) { - d_theoryProxy->notifyAssertion(ppLemmas[i].getProven(), ppSkolems[i]); + d_theoryProxy->notifyAssertion(lem.getProven(), lem.d_skolem); } } } @@ -510,12 +503,11 @@ Node PropEngine::ensureLiteral(TNode n) Node PropEngine::getPreprocessedTerm(TNode n) { // must preprocess - std::vector newLemmas; - std::vector newSkolems; - TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems); + std::vector newLemmas; + TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas); // send lemmas corresponding to the skolems introduced by preprocessing n TrustNode trnNull; - assertLemmasInternal(trnNull, newLemmas, newSkolems, false); + assertLemmasInternal(trnNull, newLemmas, false); return tpn.isNull() ? Node(n) : tpn.getNode(); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 3556108d1..2f569ba72 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -25,6 +25,7 @@ #include "proof/trust_node.h" #include "prop/skolem_def_manager.h" #include "theory/output_channel.h" +#include "theory/skolem_lemma.h" #include "util/result.h" namespace cvc5 { @@ -85,14 +86,12 @@ class PropEngine * ppSkolems respectively. * * @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 ppLemmas The lemmas to add to the set of assertions, which tracks + * their corresponding skolems, * @return The (REWRITE) trust node corresponding to rewritten node via * preprocessing. */ - TrustNode preprocess(TNode node, - std::vector& ppLemmas, - std::vector& ppSkolems); + TrustNode preprocess(TNode node, std::vector& ppLemmas); /** * Remove term ITEs (and more generally, term formulas) from the given node. * Return the REWRITE trust node corresponding to rewriting node. New lemmas @@ -101,14 +100,12 @@ class PropEngine * 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, + * @param ppLemmas The lemmas to add to the set of assertions, which tracks + * their corresponding skolems. * @return The (REWRITE) trust node corresponding to rewritten node via * preprocessing. */ - TrustNode removeItes(TNode node, - std::vector& ppLemmas, - std::vector& ppSkolems); + TrustNode removeItes(TNode node, std::vector& ppLemmas); /** * Converts the given formulas to CNF and assert the CNF to the SAT solver. @@ -334,13 +331,12 @@ class PropEngine ProofGenerator* pg = nullptr); /** * Assert lemmas internal, where trn is a trust node corresponding to a - * formula to assert to the CNF stream, ppLemmas and ppSkolems are the - * skolem definitions and skolems obtained from preprocessing it, and - * removable is whether the lemma is removable. + * formula to assert to the CNF stream, ppLemmas are the skolem definitions + * obtained from preprocessing it, and removable is whether the lemma is + * removable. */ void assertLemmasInternal(TrustNode trn, - const std::vector& ppLemmas, - const std::vector& ppSkolems, + const std::vector& ppLemmas, bool removable); /** diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index a4690ff0a..254388a49 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -203,26 +203,23 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; } -TrustNode TheoryProxy::preprocessLemma(TrustNode trn, - std::vector& newLemmas, - std::vector& newSkolems) +TrustNode TheoryProxy::preprocessLemma( + TrustNode trn, std::vector& newLemmas) { - return d_tpp.preprocessLemma(trn, newLemmas, newSkolems); + return d_tpp.preprocessLemma(trn, newLemmas); } TrustNode TheoryProxy::preprocess(TNode node, - std::vector& newLemmas, - std::vector& newSkolems) + std::vector& newLemmas) { - return d_tpp.preprocess(node, newLemmas, newSkolems); + return d_tpp.preprocess(node, newLemmas); } TrustNode TheoryProxy::removeItes(TNode node, - std::vector& newLemmas, - std::vector& newSkolems) + std::vector& newLemmas) { RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas(); - return rtf.run(node, newLemmas, newSkolems, true); + return rtf.run(node, newLemmas, true); } void TheoryProxy::getSkolems(TNode node, diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index a196bd4d4..67d3c0668 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -109,21 +109,16 @@ class TheoryProxy : public Registrar * rewrite. */ TrustNode preprocessLemma(TrustNode trn, - std::vector& newLemmas, - std::vector& newSkolems); + std::vector& newLemmas); /** * Call the preprocessor on node, return trust node corresponding to the * rewrite. */ - TrustNode preprocess(TNode node, - std::vector& newLemmas, - std::vector& newSkolems); + TrustNode preprocess(TNode node, std::vector& newLemmas); /** * Remove ITEs from the node. */ - TrustNode removeItes(TNode node, - std::vector& newLemmas, - std::vector& newSkolems); + TrustNode removeItes(TNode node, std::vector& newLemmas); /** * Get the skolems within node and their corresponding definitions, store * them in sks and skAsserts respectively. Note that this method does not diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 6a2f6fbd4..470c035a9 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -55,12 +55,10 @@ RemoveTermFormulas::RemoveTermFormulas(Env& env) RemoveTermFormulas::~RemoveTermFormulas() {} TrustNode RemoveTermFormulas::run(TNode assertion, - std::vector& newAsserts, - std::vector& newSkolems, + std::vector& newAsserts, bool fixedPoint) { - Node itesRemoved = runInternal(assertion, newAsserts, newSkolems); - Assert(newAsserts.size() == newSkolems.size()); + Node itesRemoved = runInternal(assertion, newAsserts); if (itesRemoved == assertion) { return TrustNode::null(); @@ -72,10 +70,10 @@ TrustNode RemoveTermFormulas::run(TNode assertion, size_t i = 0; while (i < newAsserts.size()) { - TrustNode trn = newAsserts[i]; + TrustNode trn = newAsserts[i].d_lemma; // do not run to fixed point on subcall, since we are processing all // lemmas in this loop - newAsserts[i] = runLemma(trn, newAsserts, newSkolems, false); + newAsserts[i].d_lemma = runLemma(trn, newAsserts, false); i++; } } @@ -84,19 +82,12 @@ TrustNode RemoveTermFormulas::run(TNode assertion, return TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get()); } -TrustNode RemoveTermFormulas::run(TNode assertion) +TrustNode RemoveTermFormulas::runLemma( + TrustNode lem, + std::vector& newAsserts, + bool fixedPoint) { - std::vector newAsserts; - std::vector newSkolems; - return run(assertion, newAsserts, newSkolems, false); -} - -TrustNode RemoveTermFormulas::runLemma(TrustNode lem, - std::vector& newAsserts, - std::vector& newSkolems, - bool fixedPoint) -{ - TrustNode trn = run(lem.getProven(), newAsserts, newSkolems, fixedPoint); + TrustNode trn = run(lem.getProven(), newAsserts, fixedPoint); if (trn.isNull()) { // no change @@ -130,8 +121,7 @@ TrustNode RemoveTermFormulas::runLemma(TrustNode lem, } Node RemoveTermFormulas::runInternal(TNode assertion, - std::vector& output, - std::vector& newSkolems) + std::vector& output) { NodeManager* nm = NodeManager::currentNM(); TCtxStack ctx(&d_rtfc); @@ -171,8 +161,7 @@ Node RemoveTermFormulas::runInternal(TNode assertion, // which we add to our vectors if (!newLem.isNull()) { - output.push_back(newLem); - newSkolems.push_back(currt); + output.push_back(theory::SkolemLemma(newLem, currt)); } Trace("rtf-debug") << "...replace by skolem" << std::endl; d_tfCache.insert(curr, currt); diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index a47bcfbb0..80cbc3b03 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -26,6 +26,7 @@ #include "expr/term_context.h" #include "proof/trust_node.h" #include "smt/env_obj.h" +#include "theory/skolem_lemma.h" #include "util/hash.h" namespace cvc5 { @@ -81,7 +82,6 @@ class RemoveTermFormulas : protected EnvObj * @param assertion The assertion to remove term formulas from * @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 @@ -91,22 +91,14 @@ class RemoveTermFormulas : protected EnvObj * generator (if provided) that can prove the equivalence. */ TrustNode run(TNode assertion, - std::vector& newAsserts, - std::vector& newSkolems, + std::vector& newAsserts, bool fixedPoint = false); - /** - * Same as above, but does not track lemmas, and does not run to fixed point. - * The relevant lemmas can be extracted by the caller later using getSkolems - * and getLemmaForSkolem. - */ - TrustNode run(TNode assertion); /** * Same as above, but transforms a lemma, returning a LEMMA trust node that * proves the same formula as lem with term formulas removed. */ TrustNode runLemma(TrustNode lem, - std::vector& newAsserts, - std::vector& newSkolems, + std::vector& newAsserts, bool fixedPoint = false); /** @@ -190,8 +182,7 @@ class RemoveTermFormulas : protected EnvObj * the version of assertion with all term formulas removed. */ Node runInternal(TNode assertion, - std::vector& newAsserts, - std::vector& newSkolems); + std::vector& newAsserts); /** * 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 diff --git a/src/theory/skolem_lemma.cpp b/src/theory/skolem_lemma.cpp index ff1ffdcf9..af4d09492 100644 --- a/src/theory/skolem_lemma.cpp +++ b/src/theory/skolem_lemma.cpp @@ -31,6 +31,8 @@ SkolemLemma::SkolemLemma(Node k, ProofGenerator* pg) : d_lemma(), d_skolem(k) d_lemma = TrustNode::mkTrustLemma(lem, pg); } +Node SkolemLemma::getProven() const { return d_lemma.getProven(); } + Node SkolemLemma::getSkolemLemmaFor(Node k) { Node w = SkolemManager::getWitnessForm(k); diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h index 277daf88c..4f17ed9d3 100644 --- a/src/theory/skolem_lemma.h +++ b/src/theory/skolem_lemma.h @@ -52,6 +52,8 @@ class SkolemLemma /** The skolem associated with that lemma */ Node d_skolem; + /** Get proven from the lemma */ + Node getProven() const; /** * Get the lemma for skolem k based on its witness form. If k has witness * form (witness ((x T)) (P x)), this is the formula (P k). diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 4b100a12f..043b0b37c 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -80,17 +80,13 @@ TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine) TheoryPreprocessor::~TheoryPreprocessor() {} TrustNode TheoryPreprocessor::preprocess(TNode node, - std::vector& newLemmas, - std::vector& newSkolems) + std::vector& newLemmas) { - return preprocessInternal(node, newLemmas, newSkolems, true); + return preprocessInternal(node, newLemmas, true); } TrustNode TheoryPreprocessor::preprocessInternal( - TNode node, - std::vector& newLemmas, - std::vector& newSkolems, - bool procLemmas) + TNode node, std::vector& newLemmas, bool procLemmas) { // In this method, all rewriting steps of node are stored in d_tpg. @@ -104,7 +100,7 @@ TrustNode TheoryPreprocessor::preprocessInternal( Node irNode = rewriteWithProof(node, d_tpgRew.get(), true); // run theory preprocessing - TrustNode tpp = theoryPreprocess(irNode, newLemmas, newSkolems); + TrustNode tpp = theoryPreprocess(irNode, newLemmas); Node ppNode = tpp.getNode(); if (Trace.isOn("tpp-debug")) @@ -131,8 +127,8 @@ TrustNode TheoryPreprocessor::preprocessInternal( size_t i = 0; while (i < newLemmas.size()) { - TrustNode cur = newLemmas[i]; - newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, false); + TrustNode cur = newLemmas[i].d_lemma; + newLemmas[i].d_lemma = preprocessLemmaInternal(cur, newLemmas, false); Trace("tpp") << "Final lemma : " << newLemmas[i].getProven() << std::endl; i++; } @@ -173,23 +169,18 @@ TrustNode TheoryPreprocessor::preprocessInternal( return tret; } -TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node, - std::vector& newLemmas, - std::vector& newSkolems) +TrustNode TheoryPreprocessor::preprocessLemma( + TrustNode node, std::vector& newLemmas) { - return preprocessLemmaInternal(node, newLemmas, newSkolems, true); + return preprocessLemmaInternal(node, newLemmas, true); } TrustNode TheoryPreprocessor::preprocessLemmaInternal( - TrustNode node, - std::vector& newLemmas, - std::vector& newSkolems, - bool procLemmas) + TrustNode node, std::vector& newLemmas, bool procLemmas) { // what was originally proven Node lemma = node.getProven(); - TrustNode tplemma = - preprocessInternal(lemma, newLemmas, newSkolems, procLemmas); + TrustNode tplemma = preprocessInternal(lemma, newLemmas, procLemmas); if (tplemma.isNull()) { // no change needed @@ -240,9 +231,7 @@ struct preprocess_stack_element }; TrustNode TheoryPreprocessor::theoryPreprocess( - TNode assertion, - std::vector& newLemmas, - std::vector& newSkolems) + TNode assertion, std::vector& newLemmas) { Trace("theory::preprocess") << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl; @@ -284,13 +273,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess( // If this is an atom, we preprocess its terms with the theory ppRewriter if (tid != THEORY_BOOL) { - std::vector lems; - Node ppRewritten = ppTheoryRewrite(current, lems); - for (const SkolemLemma& lem : lems) - { - newLemmas.push_back(lem.d_lemma); - newSkolems.push_back(lem.d_skolem); - } + Node ppRewritten = ppTheoryRewrite(current, newLemmas); Assert(Rewriter::rewrite(ppRewritten) == ppRewritten); if (isProofEnabled() && ppRewritten != current) { @@ -302,7 +285,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess( // Term formula removal without fixed point. We do not need to do fixed // point since newLemmas are theory-preprocessed until fixed point in // preprocessInternal (at top-level, when procLemmas=true). - TrustNode ttfr = d_tfr.run(ppRewritten, newLemmas, newSkolems, false); + TrustNode ttfr = d_tfr.run(ppRewritten, newLemmas, false); Node rtfNode = ppRewritten; if (!ttfr.isNull()) { diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index d34bd5c45..e4bd5955a 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -93,9 +93,7 @@ class TheoryPreprocessor : protected EnvObj * @return The (REWRITE) trust node corresponding to rewritten node via * preprocessing. */ - TrustNode preprocess(TNode node, - std::vector& newLemmas, - std::vector& newSkolems); + TrustNode preprocess(TNode node, std::vector& newLemmas); /** * Same as above, but transforms the proof of node into a proof of the * preprocessed node and returns the LEMMA trust node. @@ -107,8 +105,7 @@ class TheoryPreprocessor : protected EnvObj * form of the proven field of node. */ TrustNode preprocessLemma(TrustNode node, - std::vector& newLemmas, - std::vector& newSkolems); + std::vector& newLemmas); /** Get the term formula removal utility */ RemoveTermFormulas& getRemoveTermFormulas(); @@ -118,17 +115,14 @@ class TheoryPreprocessor : protected EnvObj * Runs theory specific preprocessing (Theory::ppRewrite) on the non-Boolean * parts of the node. */ - TrustNode theoryPreprocess(TNode node, - std::vector& newLemmas, - std::vector& newSkolems); + TrustNode theoryPreprocess(TNode node, std::vector& newLemmas); /** * 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& newLemmas, - std::vector& newSkolems, + std::vector& newLemmas, bool procLemmas); /** * Internal helper for preprocessLemma, which also optionally preprocesses the @@ -136,8 +130,7 @@ class TheoryPreprocessor : protected EnvObj * procLemmas. */ TrustNode preprocessLemmaInternal(TrustNode node, - std::vector& newLemmas, - std::vector& newSkolems, + std::vector& newLemmas, bool procLemmas); /** Reference to owning theory engine */ TheoryEngine& d_engine; -- cgit v1.2.3