diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-25 07:15:06 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-25 07:15:06 -0500 |
| commit | 1af865f3429c0dd5910b5a8d1e12d690c3623dfa (patch) | |
| tree | ac996a942c79ebb083900226a7b7c0348ef9be3a /src/theory/arith/nl/nl_model.cpp | |
| parent | e8482734bb0cd0af285464a4c50b631234ea36ee (diff) | |
Update option --nl-ext to enable/disable incremental linearization solver only (#4649)
Previously, this option disabled/enabled the entire non-linear solver. This is in preparation for new CAD techniques.
I am intentionally not renaming "--nl-ext" to e.g. "--nl-inc-lin" for the sake of not breaking user configurations.
It makes some minor changes to clean the interface in a few places and to not enable the non-linear solver in linear logics.
Diffstat (limited to 'src/theory/arith/nl/nl_model.cpp')
| -rw-r--r-- | src/theory/arith/nl/nl_model.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index bf27ecbb3..d471bf0f6 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -211,13 +211,12 @@ int NlModel::compareValue(Node i, Node j, bool isAbsolute) const } bool NlModel::checkModel(const std::vector<Node>& assertions, - const std::vector<Node>& false_asserts, unsigned d, std::vector<NlLemma>& lemmas, std::vector<Node>& gs) { Trace("nl-ext-cm-debug") << " solve for equalities..." << std::endl; - for (const Node& atom : false_asserts) + for (const Node& atom : assertions) { // see if it corresponds to a univariate polynomial equation of degree two if (atom.getKind() == EQUAL) @@ -489,6 +488,7 @@ bool NlModel::solveEqualitySimple(Node eq, { if (seq.getConst<bool>()) { + // already true d_check_model_solved[eq] = Node::null(); return true; } |