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/theory_arith.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/theory_arith.cpp')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c25090f38..30b8ed01d 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -40,7 +40,9 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, , d_proofRecorder(nullptr) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); - if (options::nlExt()) { + // if logic is non-linear + if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) + { setupExtTheory(); getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT); getExtTheory()->addFunctionKind(kind::EXPONENTIAL); |