summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/nl')
-rw-r--r--src/theory/arith/nl/cad_solver.cpp2
-rw-r--r--src/theory/arith/nl/nl_lemma_utils.cpp12
-rw-r--r--src/theory/arith/nl/nl_lemma_utils.h30
-rw-r--r--src/theory/arith/nl/nl_model.cpp3
-rw-r--r--src/theory/arith/nl/nl_solver.cpp2
-rw-r--r--src/theory/arith/nl/nonlinear_extension.cpp23
-rw-r--r--src/theory/arith/nl/nonlinear_extension.h5
-rw-r--r--src/theory/arith/nl/transcendental_solver.cpp4
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback