diff options
Diffstat (limited to 'src/theory/arith/nl')
-rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/nl_lemma_utils.cpp | 12 | ||||
-rw-r--r-- | src/theory/arith/nl/nl_lemma_utils.h | 30 | ||||
-rw-r--r-- | src/theory/arith/nl/nl_model.cpp | 3 | ||||
-rw-r--r-- | src/theory/arith/nl/nl_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 23 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 5 | ||||
-rw-r--r-- | src/theory/arith/nl/transcendental_solver.cpp | 4 |
8 files changed, 49 insertions, 32 deletions
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index b1f0894fb..ac939c341 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -95,7 +95,7 @@ std::vector<NlLemma> CadSolver::checkFull() { lems.emplace_back(nm->mkNode(Kind::OR, mis), Inference::CAD_CONFLICT); } - Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_lemma << std::endl; + Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_node << std::endl; } return lems; #else diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index 49eec186e..58a552815 100644 --- a/src/theory/arith/nl/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -15,20 +15,26 @@ #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/nonlinear_extension.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { -LemmaProperty NlLemma::getLemmaProperty() const +bool NlLemma::process(TheoryInferenceManager* im) { - return d_preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE; + bool res = ArithLemma::process(im); + if (d_nlext != nullptr) + { + d_nlext->processSideEffect(*this); + } + return res; } std::ostream& operator<<(std::ostream& out, NlLemma& n) { - out << n.d_lemma; + out << n.d_node; return out; } diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index f40857fda..c6c22c3c6 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -17,7 +17,9 @@ #include <tuple> #include <vector> + #include "expr/node.h" +#include "theory/arith/arith_lemma.h" #include "theory/arith/nl/inference.h" #include "theory/output_channel.h" @@ -27,6 +29,7 @@ namespace arith { namespace nl { class NlModel; +class NonlinearExtension; /** * The data structure for a single lemma to process by the non-linear solver, @@ -39,19 +42,24 @@ class NlModel; * - A set of secant points to record (for transcendental secant plane * inferences). */ -struct NlLemma +class NlLemma : public ArithLemma { - NlLemma(Node lem, Inference id = Inference::UNKNOWN) - : d_id(id), d_lemma(lem), d_preprocess(false) + public: + NlLemma(Node n, + LemmaProperty p, + ProofGenerator* pg, + nl::Inference inf = nl::Inference::UNKNOWN) + : ArithLemma(n, p, pg, inf) + { + } + NlLemma(Node n, nl::Inference inf = nl::Inference::UNKNOWN) + : ArithLemma(n, LemmaProperty::NONE, nullptr, inf) { } ~NlLemma() {} - /** The inference id for the lemma */ - Inference d_id; - /** The lemma */ - Node d_lemma; - /** Whether to preprocess the lemma */ - bool d_preprocess; + + bool process(TheoryInferenceManager* im) override; + /** secant points to add * * A member (tf, d, c) in this vector indicates that point c should be added @@ -62,8 +70,8 @@ struct NlLemma * Cimatti et al., CADE 2017. */ std::vector<std::tuple<Node, unsigned, Node> > d_secantPoint; - /** get lemma property (preprocess or none) */ - LemmaProperty getLemmaProperty() const; + + NonlinearExtension* d_nlext; }; /** * Writes a non-linear lemma to a stream. diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index cc10d6659..fbc38fbc2 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -16,6 +16,7 @@ #include "expr/node_algorithm.h" #include "options/arith_options.h" +#include "options/smt_options.h" #include "options/theory_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" @@ -325,7 +326,7 @@ bool NlModel::checkModel(const std::vector<Node>& assertions, Node v = cb.first; Node pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); pred = nm->mkNode(OR, mg.negate(), pred); - lemmas.push_back(pred); + lemmas.emplace_back(pred); } } return true; diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp index 521539674..6c20eec76 100644 --- a/src/theory/arith/nl/nl_solver.cpp +++ b/src/theory/arith/nl/nl_solver.cpp @@ -843,7 +843,7 @@ std::vector<NlLemma> NlSolver::checkMonomialMagnitude(unsigned c) std::vector<NlLemma> nr_lemmas; for (unsigned i = 0; i < lemmas.size(); i++) { - if (r_lemmas.find(lemmas[i].d_lemma) == r_lemmas.end()) + if (r_lemmas.find(lemmas[i].d_node) == r_lemmas.end()) { nr_lemmas.push_back(lemmas[i]); } diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 8535396e7..ada6aa11a 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -166,9 +166,9 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out) { for (const NlLemma& nlem : out) { - Node lem = nlem.d_lemma; - LemmaProperty p = nlem.getLemmaProperty(); - Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_id + Node lem = nlem.d_node; + LemmaProperty p = nlem.d_property; + Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_inference << " : " << lem << std::endl; d_containing.getOutputChannel().lemma(lem, p); // process the side effect @@ -182,7 +182,7 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out) { d_lemmas.insert(lem); } - d_stats.d_inferences << nlem.d_id; + d_stats.d_inferences << nlem.d_inference; } } @@ -210,14 +210,15 @@ void NonlinearExtension::computeRelevantAssertions( unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out) { Trace("nl-ext-lemma-debug") - << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_lemma << std::endl; - lem.d_lemma = Rewriter::rewrite(lem.d_lemma); + << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_node << std::endl; + lem.d_node = Rewriter::rewrite(lem.d_node); // get the proper cache - NodeSet& lcache = lem.d_preprocess ? d_lemmasPp : d_lemmas; - if (lcache.find(lem.d_lemma) != lcache.end()) + NodeSet& lcache = + isLemmaPropertyPreprocess(lem.d_property) ? d_lemmasPp : d_lemmas; + if (lcache.find(lem.d_node) != lcache.end()) { Trace("nl-ext-lemma-debug") - << "NonlinearExtension::Lemma duplicate : " << lem.d_lemma << std::endl; + << "NonlinearExtension::Lemma duplicate : " << lem.d_node << std::endl; return 0; } out.emplace_back(lem); @@ -232,7 +233,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas, // check if any are entailed to be false for (const NlLemma& lem : lemmas) { - Node ch_lemma = lem.d_lemma.negate(); + 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; @@ -243,7 +244,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas, if (et.first) { Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " - << lem.d_lemma << std::endl; + << lem.d_node << std::endl; // return just this lemma if (filterLemma(lem, out) > 0) { diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index ee58a9e2e..d035b1056 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -172,6 +172,9 @@ class NonlinearExtension */ void presolve(); + /** Process side effect se */ + void processSideEffect(const NlLemma& se); + private: /** Model-based refinement * @@ -274,8 +277,6 @@ class NonlinearExtension * Send lemmas in out on the output channel of theory of arithmetic. */ void sendLemmas(const std::vector<NlLemma>& out); - /** Process side effect se */ - void processSideEffect(const NlLemma& se); /** cache of all lemmas sent on the output channel (user-context-dependent) */ NodeSet d_lemmas; diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp index 321818b94..b2ef16459 100644 --- a/src/theory/arith/nl/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental_solver.cpp @@ -212,8 +212,8 @@ void TranscendentalSolver::initLastCall(const std::vector<Node>& assertions, // note we must do preprocess on this lemma Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; - NlLemma nlem(lem, Inference::T_PURIFY_ARG); - nlem.d_preprocess = true; + NlLemma nlem( + lem, LemmaProperty::PREPROCESS, nullptr, Inference::T_PURIFY_ARG); lems.emplace_back(nlem); } |