Improve integration of CAD with nl-Ext (#6542)

This PR improves the integration of the CAD solver with the nl-ext solver in a simple way: we simply use a few of the simple linearization lemmas in combination with CAD by default, significantly improving the performance on QF_NRA.

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index c472bad3f180914ba5f469e42ee0c67689196815..3005829e05c2056caacae80322a892d14ac9b31d 100644 (file)
--- 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 ed5d986be933c340dac81f24fe4f7681895a46d8..b97c99eaef3192eae3ae85e17a81ba27c5115876 100644 (file)
--- 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 8221e18d5a96670b6065719249e80c00c8ede785..7f97c4122f656a6699fa0439229d57a7089f1e46 100644 (file)
--- 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 01e319d378a483a5c6b200113fefa1337aa4966f..ffe9258303e92d395949e816bbc8aabbefae870b 100644 (file)
--- 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;

diff --git a/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2
index 3c8a949adc9837a94dc8c5ded5d82279718f4073..76898e07d1b2218a24781ba6b86317ea402e8884 100644 (file)
--- a/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2
+++ b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2
@@ -1,5 +1,5 @@
 ; REQUIRES: poly
-; COMMAND-LINE: --theoryof-mode=term --nl-ext --nl-icp
+; COMMAND-LINE: --theoryof-mode=term --nl-icp
 ; EXPECT: unknown
 (set-logic QF_NRA)
 (declare-fun x () Real)

diff --git a/test/regress/regress0/nl/coeff-sat.smt2 b/test/regress/regress0/nl/coeff-sat.smt2
index 84502bb63dc6510a1780eef9536df7b1dd39a380..f8bac932ff498970b0174b5d3da234f3022f062f 100644 (file)
--- a/test/regress/regress0/nl/coeff-sat.smt2
+++ b/test/regress/regress0/nl/coeff-sat.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --nl-ext
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)

diff --git a/test/regress/regress0/nl/issue3003.smt2 b/test/regress/regress0/nl/issue3003.smt2
index 99f975e412dfdfc9a4c9db120969e6916507f7de..f28a1fd7745365b07ab9d24a796337a5d1ad92cc 100644 (file)
--- a/test/regress/regress0/nl/issue3003.smt2
+++ b/test/regress/regress0/nl/issue3003.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: --nl-ext=none
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)

diff --git a/test/regress/regress0/nl/issue5726-downpolys.smt2 b/test/regress/regress0/nl/issue5726-downpolys.smt2
index 75e6d8cc94ac3a8398692ba9e9b935df0e599cfe..b9b204198abd220a3f1ee1bc064c65fa58d3ecf2 100644 (file)
--- a/test/regress/regress0/nl/issue5726-downpolys.smt2
+++ b/test/regress/regress0/nl/issue5726-downpolys.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-nl-ext --nl-cad
+; COMMAND-LINE: --nl-ext=none --nl-cad
 ; REQUIRES: poly
 ; EXPECT: unsat
 (set-logic QF_NRA)

diff --git a/test/regress/regress0/nl/issue5726-sqfactor.smt2 b/test/regress/regress0/nl/issue5726-sqfactor.smt2
index 4608746f6e3190e2c36426f17e72e5c93279a3ff..bfe8d31a688acf22492aaff9fa72191333bc079f 100644 (file)
--- a/test/regress/regress0/nl/issue5726-sqfactor.smt2
+++ b/test/regress/regress0/nl/issue5726-sqfactor.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-nl-ext --nl-cad
+; COMMAND-LINE: --nl-ext=none --nl-cad
 ; REQUIRES: poly
 ; EXPECT: sat
 (set-logic QF_NRA)

diff --git a/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 b/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2
index 6575385d5485780209ba6b06d345348e176d9644..7fc50f07ab9509ccb45abaab08adf1f551aa24c2 100644 (file)
--- a/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2
+++ b/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |

diff --git a/test/regress/regress0/nl/mult-po.smt2 b/test/regress/regress0/nl/mult-po.smt2
index 65498338af45752f4267179089ebe40c53d5bc77..9e4032647a270740833e92afd5d7773174c56fe8 100644 (file)
--- a/test/regress/regress0/nl/mult-po.smt2
+++ b/test/regress/regress0/nl/mult-po.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)

diff --git a/test/regress/regress0/nl/nia-wrong-tl.smt2 b/test/regress/regress0/nl/nia-wrong-tl.smt2
index 40ac92b43df64e24a84fca9e1b766bd978074ab9..6345e033df92e5c13a18ae8bd5819db6d1310e56 100644 (file)
--- a/test/regress/regress0/nl/nia-wrong-tl.smt2
+++ b/test/regress/regress0/nl/nia-wrong-tl.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NIA)
 (set-info :status sat)

diff --git a/test/regress/regress0/nl/nta/cos-sig-value.smt2 b/test/regress/regress0/nl/nta/cos-sig-value.smt2
index 7bd65b72bead644ad423cad98809f47a644cdb6c..55904572a0679ea46d55b7b96ecdda472d147906 100644 (file)
--- a/test/regress/regress0/nl/nta/cos-sig-value.smt2
+++ b/test/regress/regress0/nl/nta/cos-sig-value.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress0/nl/nta/real-pi.smt2 b/test/regress/regress0/nl/nta/real-pi.smt2
index 4163e09f9cce44572a4d07fd82f8f07e8f81144a..e7446a8c070fbdb79a1f5aa18d58e88de1b3e1fa 100644 (file)
--- a/test/regress/regress0/nl/nta/real-pi.smt2
+++ b/test/regress/regress0/nl/nta/real-pi.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --no-check-models
+; COMMAND-LINE: --nl-ext=full --no-check-models
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)

diff --git a/test/regress/regress0/nl/nta/sin-sym.smt2 b/test/regress/regress0/nl/nta/sin-sym.smt2
index 292f091ac247d9c3bac96a4e2559a1764dcd124b..7ea92284d4b13e57ef55ae94386714fb5e618f05 100644 (file)
--- a/test/regress/regress0/nl/nta/sin-sym.smt2
+++ b/test/regress/regress0/nl/nta/sin-sym.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress0/nl/nta/tan-rewrite.smt2 b/test/regress/regress0/nl/nta/tan-rewrite.smt2
index 353ed74eb56e34fcd13c8f4578ed837587ef685b..bf1c26b8c8380fff30573890eaf441954aaeb4b0 100644 (file)
--- a/test/regress/regress0/nl/nta/tan-rewrite.smt2
+++ b/test/regress/regress0/nl/nta/tan-rewrite.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress0/nl/real-div-ufnra.smt2 b/test/regress/regress0/nl/real-div-ufnra.smt2
index e7a031fa88927ae7d39b476f64a2128436af05db..aa99ed0b64ecd24453efdb13665929943ee192e7 100644 (file)
--- a/test/regress/regress0/nl/real-div-ufnra.smt2
+++ b/test/regress/regress0/nl/real-div-ufnra.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --simplification=none
+; COMMAND-LINE: --nl-ext=full --simplification=none
 ; EXPECT: sat
 (set-logic QF_UFNRA)
 (set-info :status sat)

diff --git a/test/regress/regress0/nl/subs0-unsat-confirm.smt2 b/test/regress/regress0/nl/subs0-unsat-confirm.smt2
index a1df91b177b6967448443db39e132e38603e9719..73ec87527f6b462e9e9ab0e740f26b2ea3d7bc1f 100644 (file)
--- a/test/regress/regress0/nl/subs0-unsat-confirm.smt2
+++ b/test/regress/regress0/nl/subs0-unsat-confirm.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)

diff --git a/test/regress/regress0/nl/very-easy-sat.smt2 b/test/regress/regress0/nl/very-easy-sat.smt2
index 0a0405a8eaa1cf1c5f42b4022a2de79c35108001..86b34467e526aee35589bf516842fe0ea52d015e 100644 (file)
--- a/test/regress/regress0/nl/very-easy-sat.smt2
+++ b/test/regress/regress0/nl/very-easy-sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |

diff --git a/test/regress/regress0/nl/very-simple-unsat.smt2 b/test/regress/regress0/nl/very-simple-unsat.smt2
index 839fbb88b9a6dfa6f386eeb16a93f16a832e4952..5a1c879996161823079b4c4f201d3f5b5a4d4aca 100644 (file)
--- a/test/regress/regress0/nl/very-simple-unsat.smt2
+++ b/test/regress/regress0/nl/very-simple-unsat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :source |

diff --git a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
index 9b7f7a84727126aafe89e20aecf44d7933e4e5c6..62853011bff11f4b61eb9d8f442cd28154c6745d 100644 (file)
--- a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
+++ b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
@@ -5,5 +5,5 @@
 (declare-fun c () Real)
 (declare-fun t () Real)
 (assert (forall ((s Real)) (and (> t 0) (= 0 (* t c)) (or (< s c) (> s 1.0)))))
-; previously answered "sat" with --no-nl-ext --nl-rlv=always
+; previously answered "sat" with --nl-ext=none --nl-rlv=always
 (check-sat)

diff --git a/test/regress/regress1/nl/arrowsmith-050317.smt2 b/test/regress/regress1/nl/arrowsmith-050317.smt2
index e24df9d23486e901ab59c3de9d3ff75475cdd30f..762d617ad6d6ec12a63f7421a1bb8e078d914f1c 100644 (file)
--- a/test/regress/regress1/nl/arrowsmith-050317.smt2
+++ b/test/regress/regress1/nl/arrowsmith-050317.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/bad-050217.smt2 b/test/regress/regress1/nl/bad-050217.smt2
index 69a0330017123cf6aa7753029ef1693a93c08c11..4f3cf89515bd7f3ac81eda9c80466555dfe359f6 100644 (file)
--- a/test/regress/regress1/nl/bad-050217.smt2
+++ b/test/regress/regress1/nl/bad-050217.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/bug698.smt2 b/test/regress/regress1/nl/bug698.smt2
index f24d053729b1c949e24491440aa61b4ac1e109bf..221a5613d1494a4f004dc71a4af7870a7bfc4090 100644 (file)
--- a/test/regress/regress1/nl/bug698.smt2
+++ b/test/regress/regress1/nl/bug698.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --nl-ext --fmf-fun-rlv --no-check-models
+; COMMAND-LINE: --incremental --nl-ext=full --fmf-fun-rlv --no-check-models
 (set-logic UFNIA)
 (set-info :smt-lib-version 2.6)
 

diff --git a/test/regress/regress1/nl/coeff-unsat-base.smt2 b/test/regress/regress1/nl/coeff-unsat-base.smt2
index d56421bf99b2cea87ba7c0fcb670616badc11898..97c8fa375b51cac096f320f7722cdf1dc23b5f56 100644 (file)
--- a/test/regress/regress1/nl/coeff-unsat-base.smt2
+++ b/test/regress/regress1/nl/coeff-unsat-base.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/coeff-unsat.smt2 b/test/regress/regress1/nl/coeff-unsat.smt2
index f86d08fe7953a0ac7837169dc5fef7c1953091c9..2e32906f274957abd95dcb9d13efe43ac12141f1 100644 (file)
--- a/test/regress/regress1/nl/coeff-unsat.smt2
+++ b/test/regress/regress1/nl/coeff-unsat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/combine.smt2 b/test/regress/regress1/nl/combine.smt2
index 9f7e7a5480ea3f268cb6b668b5afba655236f92b..94bdc8027abf84c5b8abedf369453274abb334ce 100644 (file)
--- a/test/regress/regress1/nl/combine.smt2
+++ b/test/regress/regress1/nl/combine.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/cos-bound.smt2 b/test/regress/regress1/nl/cos-bound.smt2
index d5052f675b1db59f10e5fbbc698057f860015f35..1371a33c7794792b4358c64878e5347b89e55d11 100644 (file)
--- a/test/regress/regress1/nl/cos-bound.smt2
+++ b/test/regress/regress1/nl/cos-bound.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (declare-fun x () Real)

diff --git a/test/regress/regress1/nl/cos1-tc.smt2 b/test/regress/regress1/nl/cos1-tc.smt2
index 4b911e576dcd1090084835e90e776cc5dcea9644..bedc0209ba1d44eb0d1480ca120225d0e94fe596 100644 (file)
--- a/test/regress/regress1/nl/cos1-tc.smt2
+++ b/test/regress/regress1/nl/cos1-tc.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --no-nl-ext-tf-tplanes --no-nl-ext-inc-prec
+; COMMAND-LINE: --nl-ext=full --no-nl-ext-tf-tplanes --no-nl-ext-inc-prec
 ; EXPECT: unknown
 (set-logic UFNRAT)
 (declare-fun f (Real) Real)

diff --git a/test/regress/regress1/nl/disj-eval.smt2 b/test/regress/regress1/nl/disj-eval.smt2
index ac8cfc937f11817692a77235a2dc6f2cc7babbd5..e8287ab0f0c10bde68dc591b3c31580c500e2746 100644 (file)
--- a/test/regress/regress1/nl/disj-eval.smt2
+++ b/test/regress/regress1/nl/disj-eval.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NIA)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/dist-big.smt2 b/test/regress/regress1/nl/dist-big.smt2
index 53c9c3f1d51397247c9e4f21f97b9edd658fbe41..e73a5bc68f0192c21eb8dab6112e92d62f323f28 100644 (file)
--- a/test/regress/regress1/nl/dist-big.smt2
+++ b/test/regress/regress1/nl/dist-big.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/div-mod-partial.smt2 b/test/regress/regress1/nl/div-mod-partial.smt2
index c94acf77069054aea4713e65b4bb7fdb9ee5587a..0f0d60fa912f153d16bf6a8cf90b340f552c635b 100644 (file)
--- a/test/regress/regress1/nl/div-mod-partial.smt2
+++ b/test/regress/regress1/nl/div-mod-partial.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes -q
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes -q
 ; EXPECT: sat
 (set-logic QF_UFNIA)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/exp-soundness-bound.smt2 b/test/regress/regress1/nl/exp-soundness-bound.smt2
index 5bcae30b031330465235f2a9c2fbb6c464bf8bea..8074fb2f2bb9094bb262292395d26234fca2d4d8 100644 (file)
--- a/test/regress/regress1/nl/exp-soundness-bound.smt2
+++ b/test/regress/regress1/nl/exp-soundness-bound.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --decision=internal --no-check-models
+; COMMAND-LINE: --nl-ext=full --decision=internal --no-check-models
 ; EXPECT: sat
 (set-logic ALL)
 (assert (or (< 60.3 (exp 4.1) 60.4) (< (exp 5.1) 164.1)))

diff --git a/test/regress/regress1/nl/exp_monotone.smt2 b/test/regress/regress1/nl/exp_monotone.smt2
index 0d754dadab8d5c34a02d396ee343d9fb7430e771..74f6465343ae26edeaf535e46b732698137f79ac 100644 (file)
--- a/test/regress/regress1/nl/exp_monotone.smt2
+++ b/test/regress/regress1/nl/exp_monotone.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/metitarski-1025.smt2 b/test/regress/regress1/nl/metitarski-1025.smt2
index 3fbf9cb77b3a2da7de58449c79b4cf90b91e08c2..200d5903eb79773684d2929c6ca23ea4b19e2640 100644 (file)
--- a/test/regress/regress1/nl/metitarski-1025.smt2
+++ b/test/regress/regress1/nl/metitarski-1025.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --no-new-prop
+; COMMAND-LINE: --nl-ext=full --no-new-prop
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |

diff --git a/test/regress/regress1/nl/metitarski-3-4.smt2 b/test/regress/regress1/nl/metitarski-3-4.smt2
index f26640f49f8008d38e7038076616f8c0ae911f0b..9ed273be6f9e478dfba6445984d9d37e98535f6c 100644 (file)
--- a/test/regress/regress1/nl/metitarski-3-4.smt2
+++ b/test/regress/regress1/nl/metitarski-3-4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --no-new-prop
+; COMMAND-LINE: --nl-ext=full --no-new-prop
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |

diff --git a/test/regress/regress1/nl/metitarski_3_4_2e.smt2 b/test/regress/regress1/nl/metitarski_3_4_2e.smt2
index 07efc3d3292da542cc34dcece6b8122717b84d55..7771dcaad0b9691a90537473fc6c4f2bc242b710 100644 (file)
--- a/test/regress/regress1/nl/metitarski_3_4_2e.smt2
+++ b/test/regress/regress1/nl/metitarski_3_4_2e.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/mirko-050417.smt2 b/test/regress/regress1/nl/mirko-050417.smt2
index 0b341ac6a1e763bcd9995aaac07da08087d8b076..9598c8477d6be35d5bfd2df74f7cc6438ce7a84c 100644 (file)
--- a/test/regress/regress1/nl/mirko-050417.smt2
+++ b/test/regress/regress1/nl/mirko-050417.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/nl-help-unsat-quant.smt2 b/test/regress/regress1/nl/nl-help-unsat-quant.smt2
index d0acca99d3c522d370d18ba1b7708744b468070f..f32cd19274c6fcc03483c014a8381c376271fba7 100644 (file)
--- a/test/regress/regress1/nl/nl-help-unsat-quant.smt2
+++ b/test/regress/regress1/nl/nl-help-unsat-quant.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic UFNIA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/nl-unk-quant.smt2 b/test/regress/regress1/nl/nl-unk-quant.smt2
index 64cc419d763214be84b2000632853b8936422f81..253811bcbcc493d125e62d5304574606e84892a1 100644 (file)
--- a/test/regress/regress1/nl/nl-unk-quant.smt2
+++ b/test/regress/regress1/nl/nl-unk-quant.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic UFNIA)
 (set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011.  Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)

diff --git a/test/regress/regress1/nl/ones.smt2 b/test/regress/regress1/nl/ones.smt2
index be06912d0d670ac232c286898ac01fffa2751fc7..79ecebb576802aeb028d56807f78e355785e4cf2 100644 (file)
--- a/test/regress/regress1/nl/ones.smt2
+++ b/test/regress/regress1/nl/ones.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/poly-1025.smt2 b/test/regress/regress1/nl/poly-1025.smt2
index 2fb918e3c5861dcf02c20fed27c94f5905f9a046..6459f29bfaabb26d2c807d198ec2dd19765f3e8a 100644 (file)
--- a/test/regress/regress1/nl/poly-1025.smt2
+++ b/test/regress/regress1/nl/poly-1025.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |

diff --git a/test/regress/regress1/nl/quant-nl.smt2 b/test/regress/regress1/nl/quant-nl.smt2
index f47023e99f8411a8c802ac0f2efe92454ca1d3ae..f2f3f83d27631c9a294845909dbe0b0dec09784b 100644 (file)
--- a/test/regress/regress1/nl/quant-nl.smt2
+++ b/test/regress/regress1/nl/quant-nl.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic UFNIA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/red-exp.smt2 b/test/regress/regress1/nl/red-exp.smt2
index 5dc5258e2f111ccc8d16401197af65b52d3ea816..95e6efb80e52fb4f0317bb518210a953f3048d39 100644 (file)
--- a/test/regress/regress1/nl/red-exp.smt2
+++ b/test/regress/regress1/nl/red-exp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/rewriting-sums.smt2 b/test/regress/regress1/nl/rewriting-sums.smt2
index ca2edf024c09fae601d4d1a8b12e71f5f4f65d88..74c38c84166b469296d692ec5d507633914b2c45 100644 (file)
--- a/test/regress/regress1/nl/rewriting-sums.smt2
+++ b/test/regress/regress1/nl/rewriting-sums.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NIA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/shifting.smt2 b/test/regress/regress1/nl/shifting.smt2
index 320c92d587a801f71d5e3597197b1fe6579a3689..e460532aeb392716fb903ed7d1facd1a047c35a5 100644 (file)
--- a/test/regress/regress1/nl/shifting.smt2
+++ b/test/regress/regress1/nl/shifting.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: sat
 (set-logic QF_NIRA)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/shifting2.smt2 b/test/regress/regress1/nl/shifting2.smt2
index c5e805c502cddaf5b31c0a30816ac2a3f2097fcf..9122701f62e1c59572b05517657fea6e35cb3905 100644 (file)
--- a/test/regress/regress1/nl/shifting2.smt2
+++ b/test/regress/regress1/nl/shifting2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NIRA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/simple-mono-unsat.smt2 b/test/regress/regress1/nl/simple-mono-unsat.smt2
index b82b7ad7c60bca7c206092530bd812b19affc039..5e54463827cb45164c1ae107f560de2b40e19785 100644 (file)
--- a/test/regress/regress1/nl/simple-mono-unsat.smt2
+++ b/test/regress/regress1/nl/simple-mono-unsat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/simple-mono.smt2 b/test/regress/regress1/nl/simple-mono.smt2
index 3d4adad2858f801e64b3ae0c77bbc55dd3bda107..092d9e90e767f8272f92e69f9ed47c071052d47f 100644 (file)
--- a/test/regress/regress1/nl/simple-mono.smt2
+++ b/test/regress/regress1/nl/simple-mono.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/sin-compare-across-phase.smt2 b/test/regress/regress1/nl/sin-compare-across-phase.smt2
index c4c28f527e269dc7caaaf6c674c001b81f28beca..9c700b8919d6d181938a2e8b4c390b3419ed2eca 100644 (file)
--- a/test/regress/regress1/nl/sin-compare-across-phase.smt2
+++ b/test/regress/regress1/nl/sin-compare-across-phase.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/sin-compare.smt2 b/test/regress/regress1/nl/sin-compare.smt2
index d22cec0b9ec204edc6dacf315248609ba26222e8..a6522074458bb4669d0628d549d6a9d0c57ba100 100644 (file)
--- a/test/regress/regress1/nl/sin-compare.smt2
+++ b/test/regress/regress1/nl/sin-compare.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/sin-init-tangents.smt2 b/test/regress/regress1/nl/sin-init-tangents.smt2
index fa29cd911a45d05b4084f8220568ffc312a96174..bf8cf9134f69596517c346e693ab4575e99416af 100644 (file)
--- a/test/regress/regress1/nl/sin-init-tangents.smt2
+++ b/test/regress/regress1/nl/sin-init-tangents.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/sin-sign.smt2 b/test/regress/regress1/nl/sin-sign.smt2
index df2a56b32cbb93851f5f87c16ba036cc5e9002b6..7da92ae53c72ca7b810ee69881815d356ce949ea 100644 (file)
--- a/test/regress/regress1/nl/sin-sign.smt2
+++ b/test/regress/regress1/nl/sin-sign.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/sin-sym2.smt2 b/test/regress/regress1/nl/sin-sym2.smt2
index 45d86dcac91f79ad54402e428dc04dbafa998a7e..eb47f113dba73e392173dd2c57b68a58734dc501 100644 (file)
--- a/test/regress/regress1/nl/sin-sym2.smt2
+++ b/test/regress/regress1/nl/sin-sym2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/tan-rewrite2.smt2 b/test/regress/regress1/nl/tan-rewrite2.smt2
index 601021a7f64292065659df8f125f6a11192af719..4e3b1f7e8a3133ec041366d3805bd12a41da31fa 100644 (file)
--- a/test/regress/regress1/nl/tan-rewrite2.smt2
+++ b/test/regress/regress1/nl/tan-rewrite2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)

diff --git a/test/regress/regress1/nl/zero-subset.smt2 b/test/regress/regress1/nl/zero-subset.smt2
index a8ce65b02b6eea413fd3d678452cb4349bfd51e5..1df45f2d2156dcc2c96f1cb7efe4b861b232ec51 100644 (file)
--- a/test/regress/regress1/nl/zero-subset.smt2
+++ b/test/regress/regress1/nl/zero-subset.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)

diff --git a/test/regress/regress2/nl/nt-lemmas-bad.smt2 b/test/regress/regress2/nl/nt-lemmas-bad.smt2
index 43a5f3d8856735f43a6fd5b356375f0acc946a96..68a36553349ca80acfe846c940f5dc0ad431817c 100644 (file)
--- a/test/regress/regress2/nl/nt-lemmas-bad.smt2
+++ b/test/regress/regress2/nl/nt-lemmas-bad.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :source |

diff --git a/test/regress/regress4/siegel-nl-bases.smt2 b/test/regress/regress4/siegel-nl-bases.smt2
index cf6e3ab5e94e58122dd9c8551c743ffefe4d8ad8..fbede19e091493a48c2310ea45ab4d88fbb3caee 100644 (file)
--- a/test/regress/regress4/siegel-nl-bases.smt2
+++ b/test/regress/regress4/siegel-nl-bases.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NIA)
 (declare-const n Int)