From c48548ea68b6241bee2cb9393ef2710c5803fb06 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 1 Feb 2021 14:55:19 -0600 Subject: [PATCH] Eliminate PREPROCESS lemma property (#5827) This is now possible since we always preprocess lemmas. Note that the LemmaProperty on inferences may be redundant throughout the non-linear solver now. --- src/theory/arith/arith_preprocess.cpp | 2 +- src/theory/arith/inference_manager.cpp | 15 +------------- src/theory/arith/inference_manager.h | 4 ---- src/theory/arith/nl/iand_solver.cpp | 20 ++++++++----------- .../nl/transcendental/exponential_solver.cpp | 3 +-- .../arith/nl/transcendental/sine_solver.cpp | 3 +-- src/theory/ext_theory.cpp | 2 +- src/theory/fp/theory_fp.cpp | 5 +++-- src/theory/output_channel.cpp | 8 -------- src/theory/output_channel.h | 8 ++------ .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 +- .../quantifiers/fmf/bounded_integers.cpp | 2 +- src/theory/quantifiers_engine.cpp | 6 ++---- 13 files changed, 22 insertions(+), 58 deletions(-) diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index 142f02eab..ecab1b92c 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -49,7 +49,7 @@ bool ArithPreprocess::reduceAssertion(TNode atom) // tn is of kind REWRITE, turn this into a LEMMA here TrustNode tlem = TrustNode::mkTrustLemma(tn.getProven(), tn.getGenerator()); // must preprocess - d_im.trustedLemma(tlem, LemmaProperty::PREPROCESS); + d_im.trustedLemma(tlem); // mark the atom as reduced d_reduced[atom] = true; return true; diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index e79c12155..6a1f898d3 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -25,7 +25,7 @@ namespace arith { InferenceManager::InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm) - : InferenceManagerBuffered(ta, astate, pnm), d_lemmasPp(ta.getUserContext()) + : InferenceManagerBuffered(ta, astate, pnm) { } @@ -110,25 +110,12 @@ std::size_t InferenceManager::numWaitingLemmas() const bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p) { Node rewritten = Rewriter::rewrite(lem); - if (isLemmaPropertyPreprocess(p)) - { - return d_lemmasPp.find(rewritten) != d_lemmasPp.end(); - } return TheoryInferenceManager::hasCachedLemma(rewritten, p); } bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p) { Node rewritten = Rewriter::rewrite(lem); - if (isLemmaPropertyPreprocess(p)) - { - if (d_lemmasPp.find(rewritten) != d_lemmasPp.end()) - { - return false; - } - d_lemmasPp.insert(rewritten); - return true; - } return TheoryInferenceManager::cacheLemma(rewritten, p); } diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index 0f2614fd7..6de65d677 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -116,10 +116,6 @@ class InferenceManager : public InferenceManagerBuffered /** The waiting lemmas. */ std::vector> d_waitingLem; - - /** cache of all preprocessed lemmas sent on the output channel - * (user-context-dependent) */ - NodeSet d_lemmasPp; }; } // namespace arith diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index f908145fe..5415e6a86 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -150,24 +150,20 @@ void IAndSolver::checkFullRefine() Node lem = sumBasedLemma(i); // add lemmas based on sum mode Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl; - // lemma can contain div/mod so need to tag it with the PREPROCESS lemma property - d_im.addPendingArithLemma(lem, - InferenceId::NL_IAND_SUM_REFINE, - nullptr, - true, - LemmaProperty::PREPROCESS); + // note that lemma can contain div/mod, and will be preprocessed in the + // prop engine + d_im.addPendingArithLemma( + lem, InferenceId::NL_IAND_SUM_REFINE, nullptr, true); } else if (options::iandMode() == options::IandMode::BITWISE) { Node lem = bitwiseLemma(i); // check for violated bitwise axioms Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; BITWISE_REFINE" << std::endl; - // lemma can contain div/mod so need to tag it with the PREPROCESS lemma property - d_im.addPendingArithLemma(lem, - InferenceId::NL_IAND_BITWISE_REFINE, - nullptr, - true, - LemmaProperty::PREPROCESS); + // note that lemma can contain div/mod, and will be preprocessed in the + // prop engine + d_im.addPendingArithLemma( + lem, InferenceId::NL_IAND_BITWISE_REFINE, nullptr, true); } else { diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index cbed48a2a..b0254d2c5 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -45,8 +45,7 @@ void ExponentialSolver::doPurification(TNode a, TNode new_a, TNode y) // note we must do preprocess on this lemma Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; - NlLemma nlem( - lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG); + NlLemma nlem(lem, LemmaProperty::NONE, nullptr, InferenceId::NL_T_PURIFY_ARG); d_data->d_im.addPendingArithLemma(nlem); } diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 40137095c..a88dd7faf 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -79,8 +79,7 @@ void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y) // note we must do preprocess on this lemma Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; - NlLemma nlem( - lem, LemmaProperty::PREPROCESS, proof, InferenceId::NL_T_PURIFY_ARG); + NlLemma nlem(lem, LemmaProperty::NONE, proof, InferenceId::NL_T_PURIFY_ARG); d_data->d_im.addPendingArithLemma(nlem); } diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index ac08b1553..7a6d5c9ab 100644 --- a/src/theory/ext_theory.cpp +++ b/src/theory/ext_theory.cpp @@ -371,7 +371,7 @@ bool ExtTheory::sendLemma(Node lem, bool preprocess) if (d_pp_lemmas.find(lem) == d_pp_lemmas.end()) { d_pp_lemmas.insert(lem); - d_out.lemma(lem, LemmaProperty::PREPROCESS); + d_out.lemma(lem); return true; } } diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index a71a2d0eb..6df991ef9 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -916,8 +916,9 @@ void TheoryFp::preRegisterTerm(TNode node) 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); + // will be preprocessed when sent, which is important because it contains + // embedded ITEs + d_out->lemma(node); } bool TheoryFp::propagateLit(TNode node) diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp index e63b78486..e0bae8fae 100644 --- a/src/theory/output_channel.cpp +++ b/src/theory/output_channel.cpp @@ -41,10 +41,6 @@ bool isLemmaPropertyRemovable(LemmaProperty p) { return (p & LemmaProperty::REMOVABLE) != LemmaProperty::NONE; } -bool isLemmaPropertyPreprocess(LemmaProperty p) -{ - return (p & LemmaProperty::PREPROCESS) != LemmaProperty::NONE; -} bool isLemmaPropertySendAtoms(LemmaProperty p) { return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE; @@ -67,10 +63,6 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p) { out << " REMOVABLE"; } - if (isLemmaPropertyPreprocess(p)) - { - out << " PREPROCESS"; - } if (isLemmaPropertySendAtoms(p)) { out << " SEND_ATOMS"; diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index c3d4b6a42..313fe24cf 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -37,12 +37,10 @@ enum class LemmaProperty : uint32_t NONE = 0, // whether the lemma is removable REMOVABLE = 1, - // whether the lemma needs preprocessing - PREPROCESS = 2, // whether the processing of the lemma should send atoms to the caller - SEND_ATOMS = 4, + SEND_ATOMS = 2, // whether the lemma is part of the justification for answering "sat" - NEEDS_JUSTIFY = 8 + NEEDS_JUSTIFY = 4 }; /** Define operator lhs | rhs */ LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs); @@ -54,8 +52,6 @@ LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs); LemmaProperty& operator&=(LemmaProperty& lhs, LemmaProperty rhs); /** is the removable bit set on p? */ bool isLemmaPropertyRemovable(LemmaProperty p); -/** is the preprocess bit set on p? */ -bool isLemmaPropertyPreprocess(LemmaProperty p); /** is the send atoms bit set on p? */ bool isLemmaPropertySendAtoms(LemmaProperty p); /** is the needs justify bit set on p? */ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 8a8678749..cb31e80d3 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -374,7 +374,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) ce_vars.push_back(tutil->getInstantiationConstant(q, i)); } // send the lemma - d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); + d_quantEngine->getOutputChannel().lemma(lem); // get the preprocessed form of the lemma we just sent std::vector skolems; std::vector skAsserts; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 0f17bb04a..9144bca2a 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -725,7 +725,7 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] ); Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); + d_quantEngine->getOutputChannel().lemma(lem); } return false; }else{ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2cc904ed1..6338c30b3 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -781,8 +781,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } - getOutputChannel().trustedLemma( - lem, LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY); + getOutputChannel().trustedLemma(lem, LemmaProperty::NEEDS_JUSTIFY); } return; } @@ -947,8 +946,7 @@ void QuantifiersEngine::flushLemmas(){ const Node& lemw = d_lemmas_waiting[i]; Trace("qe-lemma") << "Lemma : " << lemw << std::endl; itp = d_lemmasWaitingPg.find(lemw); - LemmaProperty p = - LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY; + LemmaProperty p = LemmaProperty::NEEDS_JUSTIFY; if (itp != d_lemmasWaitingPg.end()) { TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second); -- 2.30.2