From 63281fbfe093b1d5e375a378bb59761f77256d08 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 17 May 2021 17:18:57 +0200 Subject: [PATCH] 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. --- src/options/arith_options.toml | 16 +++++++++++++--- src/smt/set_defaults.cpp | 4 ++-- src/theory/arith/nl/nonlinear_extension.cpp | 6 +++--- src/theory/arith/nl/strategy.cpp | 17 +++++++++++++---- .../arith/issue5219-conflict-rewrite.smt2 | 2 +- test/regress/regress0/nl/coeff-sat.smt2 | 1 - test/regress/regress0/nl/issue3003.smt2 | 2 +- .../regress0/nl/issue5726-downpolys.smt2 | 2 +- .../regress/regress0/nl/issue5726-sqfactor.smt2 | 2 +- .../regress0/nl/magnitude-wrong-1020-m.smt2 | 2 +- test/regress/regress0/nl/mult-po.smt2 | 2 +- test/regress/regress0/nl/nia-wrong-tl.smt2 | 2 +- test/regress/regress0/nl/nta/cos-sig-value.smt2 | 2 +- test/regress/regress0/nl/nta/real-pi.smt2 | 2 +- test/regress/regress0/nl/nta/sin-sym.smt2 | 2 +- test/regress/regress0/nl/nta/tan-rewrite.smt2 | 2 +- test/regress/regress0/nl/real-div-ufnra.smt2 | 2 +- .../regress0/nl/subs0-unsat-confirm.smt2 | 2 +- test/regress/regress0/nl/very-easy-sat.smt2 | 2 +- test/regress/regress0/nl/very-simple-unsat.smt2 | 2 +- .../quantifiers/cegqi-needs-justify.smt2 | 2 +- test/regress/regress1/nl/arrowsmith-050317.smt2 | 2 +- test/regress/regress1/nl/bad-050217.smt2 | 2 +- test/regress/regress1/nl/bug698.smt2 | 2 +- test/regress/regress1/nl/coeff-unsat-base.smt2 | 2 +- test/regress/regress1/nl/coeff-unsat.smt2 | 2 +- test/regress/regress1/nl/combine.smt2 | 2 +- test/regress/regress1/nl/cos-bound.smt2 | 2 +- test/regress/regress1/nl/cos1-tc.smt2 | 2 +- test/regress/regress1/nl/disj-eval.smt2 | 2 +- test/regress/regress1/nl/dist-big.smt2 | 2 +- test/regress/regress1/nl/div-mod-partial.smt2 | 2 +- .../regress1/nl/exp-soundness-bound.smt2 | 2 +- test/regress/regress1/nl/exp_monotone.smt2 | 2 +- test/regress/regress1/nl/metitarski-1025.smt2 | 2 +- test/regress/regress1/nl/metitarski-3-4.smt2 | 2 +- test/regress/regress1/nl/metitarski_3_4_2e.smt2 | 2 +- test/regress/regress1/nl/mirko-050417.smt2 | 2 +- .../regress1/nl/nl-help-unsat-quant.smt2 | 2 +- test/regress/regress1/nl/nl-unk-quant.smt2 | 2 +- test/regress/regress1/nl/ones.smt2 | 2 +- test/regress/regress1/nl/poly-1025.smt2 | 2 +- test/regress/regress1/nl/quant-nl.smt2 | 2 +- test/regress/regress1/nl/red-exp.smt2 | 2 +- test/regress/regress1/nl/rewriting-sums.smt2 | 2 +- test/regress/regress1/nl/shifting.smt2 | 2 +- test/regress/regress1/nl/shifting2.smt2 | 2 +- test/regress/regress1/nl/simple-mono-unsat.smt2 | 2 +- test/regress/regress1/nl/simple-mono.smt2 | 2 +- .../regress1/nl/sin-compare-across-phase.smt2 | 2 +- test/regress/regress1/nl/sin-compare.smt2 | 2 +- test/regress/regress1/nl/sin-init-tangents.smt2 | 2 +- test/regress/regress1/nl/sin-sign.smt2 | 2 +- test/regress/regress1/nl/sin-sym2.smt2 | 2 +- test/regress/regress1/nl/tan-rewrite2.smt2 | 2 +- test/regress/regress1/nl/zero-subset.smt2 | 2 +- test/regress/regress2/nl/nt-lemmas-bad.smt2 | 2 +- test/regress/regress4/siegel-nl-bases.smt2 | 2 +- 58 files changed, 84 insertions(+), 66 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& assertions) // relevance here, since we may have discarded literals that are relevant // that are entailed based on the techniques in getAssertions. std::vector 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& 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; diff --git a/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 index 3c8a949ad..76898e07d 100644 --- 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 84502bb63..f8bac932f 100644 --- 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 99f975e41..f28a1fd77 100644 --- 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 75e6d8cc9..b9b204198 100644 --- 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 4608746f6..bfe8d31a6 100644 --- 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 6575385d5..7fc50f07a 100644 --- 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 65498338a..9e4032647 100644 --- 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 40ac92b43..6345e033d 100644 --- 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 7bd65b72b..55904572a 100644 --- 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 4163e09f9..e7446a8c0 100644 --- 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 292f091ac..7ea92284d 100644 --- 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 353ed74eb..bf1c26b8c 100644 --- 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 e7a031fa8..aa99ed0b6 100644 --- 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 a1df91b17..73ec87527 100644 --- 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 0a0405a8e..86b34467e 100644 --- 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 839fbb88b..5a1c87999 100644 --- 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 9b7f7a847..62853011b 100644 --- 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 e24df9d23..762d617ad 100644 --- 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 69a033001..4f3cf8951 100644 --- 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 f24d05372..221a5613d 100644 --- 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 d56421bf9..97c8fa375 100644 --- 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 f86d08fe7..2e32906f2 100644 --- 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 9f7e7a548..94bdc8027 100644 --- 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 d5052f675..1371a33c7 100644 --- 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 4b911e576..bedc0209b 100644 --- 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 ac8cfc937..e8287ab0f 100644 --- 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 53c9c3f1d..e73a5bc68 100644 --- 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 c94acf770..0f0d60fa9 100644 --- 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 5bcae30b0..8074fb2f2 100644 --- 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 0d754dada..74f646534 100644 --- 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 3fbf9cb77..200d5903e 100644 --- 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 f26640f49..9ed273be6 100644 --- 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 07efc3d32..7771dcaad 100644 --- 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 0b341ac6a..9598c8477 100644 --- 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 d0acca99d..f32cd1927 100644 --- 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 64cc419d7..253811bcb 100644 --- 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 be06912d0..79ecebb57 100644 --- 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 2fb918e3c..6459f29bf 100644 --- 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 f47023e99..f2f3f83d2 100644 --- 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 5dc5258e2..95e6efb80 100644 --- 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 ca2edf024..74c38c841 100644 --- 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 320c92d58..e460532ae 100644 --- 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 c5e805c50..9122701f6 100644 --- 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 b82b7ad7c..5e5446382 100644 --- 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 3d4adad28..092d9e90e 100644 --- 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 c4c28f527..9c700b891 100644 --- 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 d22cec0b9..a65220744 100644 --- 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 fa29cd911..bf8cf9134 100644 --- 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 df2a56b32..7da92ae53 100644 --- 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 45d86dcac..eb47f113d 100644 --- 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 601021a7f..4e3b1f7e8 100644 --- 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 a8ce65b02..1df45f2d2 100644 --- 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 43a5f3d88..68a365533 100644 --- 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 cf6e3ab5e..fbede19e0 100644 --- 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) -- 2.30.2