diff options
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 65 |
1 files changed, 5 insertions, 60 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 36ddecee9..4d29f1955 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -106,63 +106,6 @@ void NonlinearExtension::computeRelevantAssertions( << " assertions" << std::endl; } -unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out) -{ - Trace("nl-ext-lemma-debug") - << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_node << std::endl; - lem.d_node = Rewriter::rewrite(lem.d_node); - - if (d_im.hasCachedLemma(lem.d_node, lem.d_property)) - { - Trace("nl-ext-lemma-debug") - << "NonlinearExtension::Lemma duplicate : " << lem.d_node << std::endl; - return 0; - } - out.emplace_back(lem); - return 1; -} - -unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas, - std::vector<NlLemma>& out) -{ - if (options::nlExtEntailConflicts()) - { - // check if any are entailed to be false - for (const NlLemma& lem : lemmas) - { - Node ch_lemma = lem.d_node.negate(); - ch_lemma = Rewriter::rewrite(ch_lemma); - Trace("nl-ext-et-debug") - << "Check entailment of " << ch_lemma << "..." << std::endl; - std::pair<bool, Node> et = d_containing.getValuation().entailmentCheck( - options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma); - Trace("nl-ext-et-debug") << "entailment test result : " << et.first << " " - << et.second << std::endl; - if (et.first) - { - Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " - << lem.d_node << std::endl; - // return just this lemma - if (filterLemma(lem, out) > 0) - { - lemmas.clear(); - return 1; - } - } - } - } - - unsigned sum = 0; - for (const NlLemma& lem : lemmas) - { - sum += filterLemma(lem, out); - d_containing.getOutputChannel().spendResource( - ResourceManager::Resource::ArithNlLemmaStep); - } - lemmas.clear(); - return sum; -} - void NonlinearExtension::getAssertions(std::vector<Node>& assertions) { Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl; @@ -293,7 +236,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions) bool ret = d_model.checkModel(passertions, tdegree, lemmas); for (const auto& al: lemmas) { - d_im.addPendingArithLemma(al); + d_im.addPendingLemma(al); } return ret; } @@ -500,8 +443,10 @@ bool NonlinearExtension::modelBasedRefinement() d_containing.getOutputChannel().requirePhase(literal, true); Trace("nl-ext-debug") << "Split on : " << literal << std::endl; Node split = literal.orNode(literal.negate()); - NlLemma nsplit(split, InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT); - d_im.addPendingArithLemma(nsplit, true); + d_im.addPendingLemma(split, + InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT, + nullptr, + true); } if (d_im.hasWaitingLemma()) { |