Merge branch 'master' into fixWinBuildfixWinBuild

4 files changed, 31 insertions, 12 deletions

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index c472bad3f..3005829e0 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -404,10 +404,20 @@ name   = "Arithmetic theory"
 [[option]]
   name       = "nlExt"
   category   = "regular"
-  long       = "nl-ext"
-  type       = "bool"
-  default    = "true"
+  long       = "nl-ext=MODE"
+  type       = "NlExtMode"
+  default    = "FULL"
   help       = "incremental linearization approach to non-linear"
+  help_mode  = "Modes for the non-linear linearization"
+[[option.mode.NONE]]
+  name = "none"
+  help = "Disable linearization approach"
+[[option.mode.LIGHT]]
+  name = "light"
+  help = "Only use a few light-weight lemma schemes"
+[[option.mode.FULL]]
+  name = "full"
+  help = "Use all lemma schemes"
 
 [[option]]
   name       = "nlExtResBound"
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index ed5d986be..b97c99eae 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1514,7 +1514,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.set(options::nlCad, true);
       if (!opts.wasSetByUser(options::nlExt))
       {
-        opts.set(options::nlExt, false);
+        opts.set(options::nlExt, options::NlExtMode::LIGHT);
       }
       if (!opts.wasSetByUser(options::nlRlvMode))
       {
@@ -1537,7 +1537,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       Notice() << "Cannot use --" << options::nlCad.name
                << " without configuring with --poly." << std::endl;
       opts.set(options::nlCad, false);
-      opts.set(options::nlExt, true);
+      opts.set(options::nlExt, options::NlExtMode::FULL);
     }
   }
 #endif
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 8221e18d5..7f97c4122 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -218,7 +218,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions)
   // relevance here, since we may have discarded literals that are relevant
   // that are entailed based on the techniques in getAssertions.
   std::vector<Node> passertions = assertions;
-  if (options::nlExt())
+  if (options::nlExt() == options::NlExtMode::FULL)
   {
     // preprocess the assertions with the trancendental solver
     if (!d_trSlv.preprocessAssertionsCheckModel(passertions))
@@ -474,8 +474,8 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termS
       }
 
       // we are incomplete
-      if (options::nlExt() && options::nlExtIncPrecision()
-          && d_model.usedApproximate())
+      if (options::nlExt() == options::NlExtMode::FULL
+          && options::nlExtIncPrecision() && d_model.usedApproximate())
       {
         d_trSlv.incrementTaylorDegree();
         needsRecheck = true;
diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp
index 01e319d37..ffe925830 100644
--- a/src/theory/arith/nl/strategy.cpp
+++ b/src/theory/arith/nl/strategy.cpp
@@ -109,9 +109,14 @@ void Strategy::initializeStrategy()
   {
     one << InferStep::ICP << InferStep::BREAK;
   }
-  if (options::nlExt())
+  if (options::nlExt() == options::NlExtMode::FULL
+      || options::nlExt() == options::NlExtMode::LIGHT)
   {
-    one << InferStep::NL_INIT << InferStep::TRANS_INIT << InferStep::BREAK;
+    one << InferStep::NL_INIT << InferStep::BREAK;
+  }
+  if (options::nlExt() == options::NlExtMode::FULL)
+  {
+    one << InferStep::TRANS_INIT << InferStep::BREAK;
     if (options::nlExtSplitZero())
     {
       one << InferStep::NL_SPLIT_ZERO << InferStep::BREAK;
@@ -120,11 +125,15 @@ void Strategy::initializeStrategy()
   }
   one << InferStep::IAND_INIT;
   one << InferStep::IAND_INITIAL << InferStep::BREAK;
-  if (options::nlExt())
+  if (options::nlExt() == options::NlExtMode::FULL
+      || options::nlExt() == options::NlExtMode::LIGHT)
   {
     one << InferStep::NL_MONOMIAL_SIGN << InferStep::BREAK;
-    one << InferStep::TRANS_MONOTONIC << InferStep::BREAK;
     one << InferStep::NL_MONOMIAL_MAGNITUDE0 << InferStep::BREAK;
+  }
+  if (options::nlExt() == options::NlExtMode::FULL)
+  {
+    one << InferStep::TRANS_MONOTONIC << InferStep::BREAK;
     one << InferStep::NL_MONOMIAL_MAGNITUDE1 << InferStep::BREAK;
     one << InferStep::NL_MONOMIAL_MAGNITUDE2 << InferStep::BREAK;
     one << InferStep::NL_MONOMIAL_INFER_BOUNDS;