From: Andrew Reynolds Date: Thu, 28 Jan 2021 20:01:26 +0000 (-0600) Subject: Simplify lemma interface (#5819) X-Git-Tag: cvc5-1.0.0~2343 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e234ff58f561ac97642df15c698962faa9d1e5e4;p=cvc5.git Simplify lemma interface (#5819) This makes it so that TheoryEngine::lemma returns void not LemmaStatus. Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions. It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems. --- diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index fb43ebe73..28159c229 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -36,6 +36,7 @@ #include "prop/theory_proxy.h" #include "smt/smt_statistics_registry.h" #include "theory/output_channel.h" +#include "theory/rewriter.h" #include "theory/theory_engine.h" #include "util/resource_manager.h" #include "util/result.h" @@ -206,7 +207,7 @@ void PropEngine::assertFormula(TNode node) { } } -Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) +void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) { bool removable = isLemmaPropertyRemovable(p); @@ -261,20 +262,6 @@ Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) } d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems); } - - // make the return lemma, which the theory engine will use - Node retLemma = tplemma.getProven(); - if (!ppLemmas.empty()) - { - std::vector lemmas{retLemma}; - for (const theory::TrustNode& tnl : ppLemmas) - { - lemmas.push_back(tnl.getProven()); - } - // the returned lemma is the conjunction of all additional lemmas. - retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas); - } - return retLemma; } void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable) @@ -441,6 +428,7 @@ Node PropEngine::ensureLiteral(TNode n) Node PropEngine::getPreprocessedTerm(TNode n) { + Node rewritten = theory::Rewriter::rewrite(n); // must preprocess std::vector newLemmas; std::vector newSkolems; @@ -453,6 +441,39 @@ Node PropEngine::getPreprocessedTerm(TNode n) return tpn.isNull() ? Node(n) : tpn.getNode(); } +Node PropEngine::getPreprocessedTerm(TNode n, + std::vector& skAsserts, + std::vector& sks) +{ + // get the preprocessed form of the term + Node pn = getPreprocessedTerm(n); + // initialize the set of skolems and assertions to process + std::vector toProcessAsserts; + std::vector toProcess; + d_theoryProxy->getSkolems(pn, toProcessAsserts, toProcess); + size_t index = 0; + // until fixed point is reached + while (index < toProcess.size()) + { + theory::TrustNode ka = toProcessAsserts[index]; + Node k = toProcess[index]; + index++; + if (std::find(sks.begin(), sks.end(), k) != sks.end()) + { + // already added the skolem to the list + continue; + } + // must preprocess lemmas as well + Node kap = getPreprocessedTerm(ka.getProven()); + skAsserts.push_back(kap); + sks.push_back(k); + // get the skolems in the preprocessed form of the lemma ka + d_theoryProxy->getSkolems(kap, toProcessAsserts, toProcess); + } + // return the preprocessed term + return pn; +} + void PropEngine::push() { Assert(!d_inCheckSat) << "Sat solver in solve()!"; diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 493dbfe01..f7561d945 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -145,9 +145,8 @@ class PropEngine * * @param trn the trust node storing the formula to assert * @param p the properties of the lemma - * @return the (preprocessed) lemma */ - Node assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p); + void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p); /** * If ever n is decided upon, it must be in the given phase. This @@ -209,6 +208,20 @@ class PropEngine * if preprocessing n involves introducing new skolems. */ Node getPreprocessedTerm(TNode n); + /** + * Same as above, but also compute the skolems in n and in the lemmas + * corresponding to their definition. + * + * Note this will include skolems that occur in the definition lemma + * for all skolems in sks. This is run until a fixed point is reached. + * For example, if k1 has definition (ite A (= k1 k2) (= k1 x)) where k2 is + * another skolem introduced by term formula removal, then calling this + * method on (P k1) will include both k1 and k2 in sks, and their definitions + * in skAsserts. + */ + Node getPreprocessedTerm(TNode n, + std::vector& skAsserts, + std::vector& sks); /** * Push the context level. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index c604c47f7..a6d570bc2 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -194,6 +194,20 @@ theory::TrustNode TheoryProxy::removeItes( return rtf.run(node, newLemmas, newSkolems, true); } +void TheoryProxy::getSkolems(TNode node, + std::vector& skAsserts, + std::vector& sks) +{ + RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas(); + std::unordered_set skolems; + rtf.getSkolems(node, skolems); + for (const Node& k : skolems) + { + sks.push_back(k); + skAsserts.push_back(rtf.getLemmaForSkolem(k)); + } +} + void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); } }/* CVC4::prop namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 57115d660..ac79cf967 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -118,6 +118,17 @@ class TheoryProxy : public Registrar theory::TrustNode removeItes(TNode node, std::vector& newLemmas, std::vector& newSkolems); + /** + * Get the skolems within node and their corresponding definitions, store + * them in sks and skAsserts respectively. Note that this method does not + * necessary include all of the skolems in skAsserts. In other words, it + * collects from node only. To compute all skolems that node depends on + * requires calling this method again on each lemma in skAsserts until a + * fixed point is reached. + */ + void getSkolems(TNode node, + std::vector& skAsserts, + std::vector& sks); /** Preregister term */ void preRegister(Node n) override; diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index f77ae7b49..9a856fc14 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -517,21 +517,9 @@ Node RemoveTermFormulas::getSkolemForNode(Node k) const return Node::null(); } -bool RemoveTermFormulas::getSkolems( +void RemoveTermFormulas::getSkolems( TNode n, std::unordered_set& skolems) const { - // if n was unchanged by term formula removal, just return immediately - std::pair initial(n, d_rtfc.initialValue()); - TermFormulaCache::const_iterator itc = d_tfCache.find(initial); - if (itc != d_tfCache.end()) - { - if (itc->second == n) - { - return false; - } - } - // otherwise, traverse it - bool ret = false; std::unordered_set visited; std::unordered_set::iterator it; std::vector visit; @@ -549,16 +537,15 @@ bool RemoveTermFormulas::getSkolems( { if (d_lemmaCache.find(cur) != d_lemmaCache.end()) { - // technically could already be in skolems if skolems was non-empty, - // regardless set return value to true. skolems.insert(cur); - ret = true; } } - visit.insert(visit.end(), cur.begin(), cur.end()); + else + { + visit.insert(visit.end(), cur.begin(), cur.end()); + } } } while (!visit.empty()); - return ret; } Node RemoveTermFormulas::getAxiomFor(Node n) diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index ac2644182..0c026a5fe 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -130,12 +130,10 @@ class RemoveTermFormulas { * Get the set of skolems introduced by this class that occur in node n, * add them to skolems. * - * This method uses an optimization that returns false immediately if n - * was unchanged by term formula removal, based on the initial context. - * - * Return true if any nodes were added to skolems. + * @param n The node to traverse + * @param skolems The set where the skolems are added */ - bool getSkolems(TNode n, + void getSkolems(TNode n, std::unordered_set& skolems) const; /** diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp index 45a709d19..402eeeb26 100644 --- a/src/theory/combination_care_graph.cpp +++ b/src/theory/combination_care_graph.cpp @@ -85,7 +85,7 @@ void CombinationCareGraph::combineTheories() // This is supposed to force preference to follow what the theory models // already have but it doesn't seem to make a big difference - need to // explore more -Clark - Node e = d_te.ensureLiteral(equality); + Node e = d_valuation.ensureLiteral(equality); propEngine->requirePhase(e, true); } } diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 71eac49a0..21450df04 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -28,6 +28,7 @@ CombinationEngine::CombinationEngine(TheoryEngine& te, const std::vector& paraTheories, ProofNodeManager* pnm) : d_te(te), + d_valuation(&te), d_pnm(pnm), d_logicInfo(te.getLogicInfo()), d_paraTheories(paraTheories), diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index 765a49d68..5bc9d7bdd 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -24,6 +24,7 @@ #include "theory/ee_manager.h" #include "theory/model_manager.h" #include "theory/shared_solver.h" +#include "theory/valuation.h" namespace CVC4 { @@ -104,6 +105,8 @@ class CombinationEngine void sendLemma(TrustNode trn, TheoryId atomsTo); /** Reference to the theory engine */ TheoryEngine& d_te; + /** Valuation for the engine */ + Valuation d_valuation; /** The proof node manager */ ProofNodeManager* d_pnm; /** Logic info of theory engine (cached) */ diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index 0aa56a381..1105b918b 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -67,7 +67,7 @@ void EngineOutputChannel::safePoint(ResourceManager::Resource r) } } -theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p) +void EngineOutputChannel::lemma(TNode lemma, LemmaProperty p) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" @@ -76,15 +76,13 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p) d_engine->d_outputChannelUsed = true; TrustNode tlem = TrustNode::mkTrustLemma(lemma); - theory::LemmaStatus result = d_engine->lemma( - tlem, - p, - isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST, - d_theory); - return result; + d_engine->lemma(tlem, + p, + isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST, + d_theory); } -theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) +void EngineOutputChannel::splitLemma(TNode lemma, bool removable) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; @@ -95,8 +93,7 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) << std::endl; TrustNode tlem = TrustNode::mkTrustLemma(lemma); LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE; - theory::LemmaStatus result = d_engine->lemma(tlem, p, d_theory); - return result; + d_engine->lemma(tlem, p, d_theory); } bool EngineOutputChannel::propagate(TNode literal) @@ -172,7 +169,7 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf) d_engine->conflict(pconf, d_theory); } -LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p) +void EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::trustedLemma(" << plem << ")" << std::endl; @@ -184,11 +181,10 @@ LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p) ++d_statistics.lemmas; d_engine->d_outputChannelUsed = true; // now, call the normal interface for lemma - return d_engine->lemma( - plem, - p, - isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST, - d_theory); + d_engine->lemma(plem, + p, + isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST, + d_theory); } } // namespace theory diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index 7a59dbf2a..c53feabc5 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -48,10 +48,9 @@ class EngineOutputChannel : public theory::OutputChannel void conflict(TNode conflictNode) override; bool propagate(TNode literal) override; - theory::LemmaStatus lemma(TNode lemma, - LemmaProperty p = LemmaProperty::NONE) override; + void lemma(TNode lemma, LemmaProperty p = LemmaProperty::NONE) override; - theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) override; + void splitLemma(TNode lemma, bool removable = false) override; void demandRestart() override; @@ -76,8 +75,8 @@ class EngineOutputChannel : public theory::OutputChannel * by the generator pfg. Apart from pfg, the interface for this method is * the same as calling OutputChannel::lemma on lem. */ - LemmaStatus trustedLemma(TrustNode plem, - LemmaProperty p = LemmaProperty::NONE) override; + void trustedLemma(TrustNode plem, + LemmaProperty p = LemmaProperty::NONE) override; protected: /** diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 0a8c4ee0e..a71a2d0eb 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -918,9 +918,6 @@ void TheoryFp::handleLemma(Node node) { Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl; // Preprocess has to be true because it contains embedded ITEs d_out->lemma(node, LemmaProperty::PREPROCESS); - // Ignore the LemmaStatus structure for now... - - return; } bool TheoryFp::propagateLit(TNode node) diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp index 91f30514c..e63b78486 100644 --- a/src/theory/output_channel.cpp +++ b/src/theory/output_channel.cpp @@ -84,19 +84,7 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p) return out; } -LemmaStatus::LemmaStatus(TNode rewrittenLemma, unsigned level) - : d_rewrittenLemma(rewrittenLemma), d_level(level) -{ -} - -TNode LemmaStatus::getRewrittenLemma() const { return d_rewrittenLemma; } - -unsigned LemmaStatus::getLevel() const { return d_level; } - -LemmaStatus OutputChannel::split(TNode n) -{ - return splitLemma(n.orNode(n.notNode())); -} +void OutputChannel::split(TNode n) { splitLemma(n.orNode(n.notNode())); } void OutputChannel::trustedConflict(TrustNode pconf) { @@ -104,7 +92,7 @@ void OutputChannel::trustedConflict(TrustNode pconf) << std::endl; } -LemmaStatus OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p) +void OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p) { Unreachable() << "OutputChannel::trustedLemma: no implementation" << std::endl; diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 197e42a99..c3d4b6a42 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -72,29 +72,6 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p); class Theory; -/** - * A LemmaStatus, returned from OutputChannel::lemma(), provides information - * about the lemma added. In particular, it contains the T-rewritten lemma - * for inspection and the user-level at which the lemma will reside. - */ -class LemmaStatus { - public: - LemmaStatus(TNode rewrittenLemma, unsigned level); - - /** Get the T-rewritten form of the lemma. */ - TNode getRewrittenLemma() const; - /** - * Get the user-level at which the lemma resides. After this user level - * is popped, the lemma is un-asserted from the SAT layer. This level - * will be 0 if the lemma didn't reach the SAT layer at all. - */ - unsigned getLevel() const; - - private: - Node d_rewrittenLemma; - unsigned d_level; -}; /* class LemmaStatus */ - /** * Generic "theory output channel" interface. * @@ -150,10 +127,8 @@ class OutputChannel { * * @param n - a theory lemma valid at decision level 0 * @param p The properties of the lemma - * @return the "status" of the lemma, including user level at which - * the lemma resides; the lemma will be removed when this user level pops */ - virtual LemmaStatus lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) = 0; + virtual void lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) = 0; /** * Request a split on a new theory atom. This is equivalent to @@ -161,9 +136,9 @@ class OutputChannel { * * @param n - a theory atom; must be of Boolean type */ - LemmaStatus split(TNode n); + void split(TNode n); - virtual LemmaStatus splitLemma(TNode n, bool removable = false) = 0; + virtual void splitLemma(TNode n, bool removable = false) = 0; /** * If a decision is made on n, it must be in the phase specified. @@ -227,8 +202,8 @@ class OutputChannel { * by the generator pfg. Apart from pfg, the interface for this method is * the same as OutputChannel. */ - virtual LemmaStatus trustedLemma(TrustNode lem, - LemmaProperty p = LemmaProperty::NONE); + virtual void trustedLemma(TrustNode lem, + LemmaProperty p = LemmaProperty::NONE); //---------------------------- end new proof }; /* class OutputChannel */ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 118e7023c..8a8678749 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -373,13 +373,20 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) { ce_vars.push_back(tutil->getInstantiationConstant(q, i)); } - CegInstantiator* cinst = getInstantiator(q); - LemmaStatus status = - d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); - Node ppLem = status.getRewrittenLemma(); + // send the lemma + d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); + // get the preprocessed form of the lemma we just sent + std::vector skolems; + std::vector skAsserts; + Node ppLem = d_quantEngine->getValuation().getPreprocessedTerm( + lem, skAsserts, skolems); + std::vector lemp{ppLem}; + lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end()); + ppLem = NodeManager::currentNM()->mkAnd(lemp); Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem << std::endl; std::vector auxLems; + CegInstantiator* cinst = getInstantiator(q); cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems); for (unsigned i = 0, size = auxLems.size(); i < size; i++) { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 18d9bb572..3492f97a9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1161,19 +1161,6 @@ Node TheoryEngine::getModelValue(TNode var) { return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } - -Node TheoryEngine::ensureLiteral(TNode n) { - Trace("ensureLiteral") << "ensureLiteral rewriting: " << n << std::endl; - Node rewritten = Rewriter::rewrite(n); - return d_propEngine->ensureLiteral(rewritten); -} - -Node TheoryEngine::getPreprocessedTerm(TNode n) -{ - Node rewritten = Rewriter::rewrite(n); - return d_propEngine->getPreprocessedTerm(rewritten); -} - void TheoryEngine::printSynthSolution( std::ostream& out ) { if( d_quantEngine ){ d_quantEngine->printSynthSolution( out ); @@ -1340,10 +1327,10 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector& atoms, theory::The } } -theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, - theory::LemmaProperty p, - theory::TheoryId atomsTo, - theory::TheoryId from) +void TheoryEngine::lemma(theory::TrustNode tlemma, + theory::LemmaProperty p, + theory::TheoryId atomsTo, + theory::TheoryId from) { // For resource-limiting (also does a time check). // spendResource(); @@ -1393,20 +1380,24 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, printer.toStreamCmdCheckSat(out, n); } - Node retLemma = d_propEngine->assertLemma(tlemma, p); + // assert the lemma + d_propEngine->assertLemma(tlemma, p); // If specified, we must add this lemma to the set of those that need to be - // justified, where note we pass all auxiliary lemmas in lemmas, since these - // by extension must be justified as well. + // justified, where note we pass all auxiliary lemmas in skAsserts as well, + // since these by extension must be justified as well. if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p)) { + std::vector skAsserts; + std::vector sks; + Node retLemma = + d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks); d_relManager->notifyPreprocessedAssertion(retLemma); + d_relManager->notifyPreprocessedAssertions(skAsserts); } // Mark that we added some lemmas d_lemmasAdded = true; - - return theory::LemmaStatus(retLemma, d_userContext->getLevel()); } void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId) diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 747c1ccc9..46498e71a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -274,13 +274,11 @@ class TheoryEngine { * @param p the properties of the lemma. * @param atomsTo the theory that atoms of the lemma should be sent to * @param from the theory that sent the lemma - * @return a lemma status, containing the lemma and context information - * about when it was sent. */ - theory::LemmaStatus lemma(theory::TrustNode node, - theory::LemmaProperty p, - theory::TheoryId atomsTo = theory::THEORY_LAST, - theory::TheoryId from = theory::THEORY_LAST); + void lemma(theory::TrustNode node, + theory::LemmaProperty p, + theory::TheoryId atomsTo = theory::THEORY_LAST, + theory::TheoryId from = theory::THEORY_LAST); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); @@ -648,20 +646,6 @@ class TheoryEngine { * has (or null if none); */ Node getModelValue(TNode var); - - /** - * Takes a literal and returns an equivalent literal that is guaranteed to be - * a SAT literal. This rewrites and preprocesses n, which notice may involve - * adding clauses to the SAT solver if preprocessing n involves introducing - * new skolems. - */ - Node ensureLiteral(TNode n); - /** - * This returns the theory-preprocessed form of term n. This rewrites and - * preprocesses n, which notice may involve adding clauses to the SAT solver - * if preprocessing n involves introducing new skolems. - */ - Node getPreprocessedTerm(TNode n); /** * Print solution for synthesis conjectures found by ce_guided_instantiation module */ diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 003e439ae..f37e4c942 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -77,26 +77,18 @@ public: return true; } - LemmaStatus lemma(TNode n, LemmaProperty p) override - { - push(LEMMA, n); - return LemmaStatus(Node::null(), 0); - } + void lemma(TNode n, LemmaProperty p) override { push(LEMMA, n); } - LemmaStatus trustedLemma(TrustNode n, LemmaProperty p) override + void trustedLemma(TrustNode n, LemmaProperty p) override { push(LEMMA, n.getNode()); - return LemmaStatus(Node::null(), 0); } void requirePhase(TNode, bool) override {} void setIncomplete() override {} void handleUserAttribute(const char* attr, theory::Theory* t) override {} - LemmaStatus splitLemma(TNode n, bool removable = false) override { - push(LEMMA, n); - return LemmaStatus(Node::null(), 0); - } + void splitLemma(TNode n, bool removable = false) override { push(LEMMA, n); } void clear() { d_callHistory.clear(); } diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index b8ee5d41c..6fae8421d 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -156,13 +156,21 @@ void Valuation::setIrrelevantKind(Kind k) Node Valuation::ensureLiteral(TNode n) { Assert(d_engine != nullptr); - return d_engine->ensureLiteral(n); + return d_engine->getPropEngine()->ensureLiteral(n); } Node Valuation::getPreprocessedTerm(TNode n) { Assert(d_engine != nullptr); - return d_engine->getPreprocessedTerm(n); + return d_engine->getPropEngine()->getPreprocessedTerm(n); +} + +Node Valuation::getPreprocessedTerm(TNode n, + std::vector& skAsserts, + std::vector& sks) +{ + Assert(d_engine != nullptr); + return d_engine->getPropEngine()->getPreprocessedTerm(n, skAsserts, sks); } bool Valuation::isDecision(Node lit) const { diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 065556872..9759309fa 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -159,6 +159,13 @@ public: * @return The preprocessed form of n */ Node getPreprocessedTerm(TNode n); + /** + * Same as above, but also tracks the skolems and their corresponding + * definitions in sks and skAsserts respectively. + */ + Node getPreprocessedTerm(TNode n, + std::vector& skAsserts, + std::vector& sks); /** * Returns whether the given lit (which must be a SAT literal) is a decision diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 97da7eb8b..04bc79b3a 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -56,8 +56,7 @@ using namespace std; class FakeOutputChannel : public OutputChannel { void conflict(TNode n) override { Unimplemented(); } bool propagate(TNode n) override { Unimplemented(); } - LemmaStatus lemma(TNode n, - LemmaProperty p = LemmaProperty::NONE) override + void lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) override { Unimplemented(); } @@ -66,7 +65,7 @@ class FakeOutputChannel : public OutputChannel { void handleUserAttribute(const char* attr, Theory* t) override { Unimplemented(); } - LemmaStatus splitLemma(TNode n, bool removable) override { Unimplemented(); } + void splitLemma(TNode n, bool removable) override { Unimplemented(); } }; /* class FakeOutputChannel */ template diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 9f23dbad6..4b6c1a064 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -54,17 +54,12 @@ class TestOutputChannel : public OutputChannel { return true; } - LemmaStatus lemma(TNode n, - LemmaProperty p = LemmaProperty::NONE) override + void lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) override { push(LEMMA, n); - return LemmaStatus(Node::null(), 0); } - LemmaStatus splitLemma(TNode n, bool removable) override { - push(LEMMA, n); - return LemmaStatus(Node::null(), 0); - } + void splitLemma(TNode n, bool removable) override { push(LEMMA, n); } void requirePhase(TNode, bool) override { Unreachable(); } void setIncomplete() override { Unreachable(); }