From bb095659fb12e3733a73f1be31769ff5b5eb6055 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 24 Nov 2017 06:44:46 -0600 Subject: Implement tangent and secant planes for transcendental functions (#1401) --- test/regress/regress0/nl/Makefile.am | 15 +++++++++++++- test/regress/regress0/nl/nta/NAVIGATION2.smt2 | 23 ++++++++++++++++++++++ ...ier_llibre_artes_ex_5_13.transcendental.k2.smt2 | 22 +++++++++++++++++++++ test/regress/regress0/nl/nta/exp-4.5-lt.smt2 | 9 +++++++++ test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 | 10 ++++++++++ test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 | 10 ++++++++++ test/regress/regress0/nl/nta/exp1-lb.smt2 | 10 ++++++++++ test/regress/regress0/nl/nta/exp1-ub.smt2 | 11 +++++++++++ test/regress/regress0/nl/nta/sin1-lb.smt2 | 10 ++++++++++ test/regress/regress0/nl/nta/sin1-ub.smt2 | 10 ++++++++++ test/regress/regress0/nl/nta/sin2-lb.smt2 | 10 ++++++++++ test/regress/regress0/nl/nta/sin2-ub.smt2 | 10 ++++++++++ 12 files changed, 149 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/nl/nta/NAVIGATION2.smt2 create mode 100644 test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 create mode 100644 test/regress/regress0/nl/nta/exp-4.5-lt.smt2 create mode 100644 test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 create mode 100644 test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 create mode 100644 test/regress/regress0/nl/nta/exp1-lb.smt2 create mode 100644 test/regress/regress0/nl/nta/exp1-ub.smt2 create mode 100644 test/regress/regress0/nl/nta/sin1-lb.smt2 create mode 100644 test/regress/regress0/nl/nta/sin1-ub.smt2 create mode 100644 test/regress/regress0/nl/nta/sin2-lb.smt2 create mode 100644 test/regress/regress0/nl/nta/sin2-ub.smt2 (limited to 'test/regress/regress0/nl') diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am index d26d53d07..9881b3e72 100644 --- a/test/regress/regress0/nl/Makefile.am +++ b/test/regress/regress0/nl/Makefile.am @@ -66,7 +66,20 @@ TESTS = \ nta/tan-rewrite.smt2 \ nta/arrowsmith-050317.smt2 \ nta/sin-init-tangents.smt2 \ - nta/cos1-tc.smt2 + nta/cos1-tc.smt2 \ + nta/sin1-ub.smt2 \ + nta/sin1-lb.smt2 \ + nta/sin2-ub.smt2 \ + nta/sin2-lb.smt2 \ + nta/exp1-ub.smt2 \ + nta/exp1-lb.smt2 \ + nta/exp-4.5-lt.smt2 \ + nta/exp-n0.5-ub.smt2 \ + nta/exp-n0.5-lb.smt2 \ + nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 \ + nta/NAVIGATION2.smt2 + +# unsolved : garbage_collect.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/nl/nta/NAVIGATION2.smt2 b/test/regress/regress0/nl/nta/NAVIGATION2.smt2 new file mode 100644 index 000000000..445b8a21e --- /dev/null +++ b/test/regress/regress0/nl/nta/NAVIGATION2.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :source |printed by MathSAT|) +(declare-fun X () Real) + +(assert (let ((.def_44 (* (- (/ 11 10)) X))) +(let ((.def_45 (exp .def_44))) +(let ((.def_50 (* 250 .def_45))) +(let ((.def_40 (* (- (/ 13 10)) X))) +(let ((.def_41 (exp .def_40))) +(let ((.def_52 (* 173 .def_41))) +(let ((.def_53 (+ .def_52 .def_50))) +(let ((.def_54 (* 250 X))) +(let ((.def_55 (+ .def_54 .def_53))) +(let ((.def_56 (<= .def_55 (/ 595 2)))) +(let ((.def_57 (not .def_56))) +(let ((.def_31 (<= 0 X))) +(let ((.def_32 (not .def_31))) +(let ((.def_58 (or .def_32 .def_57))) +(let ((.def_59 (not .def_58))) +.def_59)))))))))))))))) +(check-sat) diff --git a/test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 b/test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 new file mode 100644 index 000000000..5dce6ddca --- /dev/null +++ b/test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: sat +(set-logic QF_NRA) +(declare-fun time__AT0@0 () Real) +(declare-fun instance.y__AT0@0 () Real) +(declare-fun instance.x__AT0@0 () Real) +(declare-fun instance.y__AT0@2 () Real) +(declare-fun event_is_timed__AT0@2 () Bool) +(declare-fun instance.EVENT.0__AT0@1 () Bool) +(declare-fun instance.EVENT.1__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@0 () Bool) +(declare-fun instance.EVENT.0__AT0@0 () Bool) +(declare-fun instance.EVENT.1__AT0@0 () Bool) +(declare-fun instance.y__AT0@1 () Real) +(declare-fun instance.x__AT0@1 () Real) +(declare-fun time__AT0@1 () Real) +(declare-fun instance.x__AT0@2 () Real) +(declare-fun time__AT0@2 () Real) +(assert (let ((.def_0 (<= instance.y__AT0@2 2.0))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@1))) (let ((.def_3 (not instance.EVENT.0__AT0@1))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_6 (<= time__AT0@1 time__AT0@2))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@1 time__AT0@2))) (let ((.def_10 (or instance.EVENT.1__AT0@1 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) time__AT0@1))) (let ((.def_13 (+ .def_12 time__AT0@2))) (let ((.def_14 (exp .def_13))) (let ((.def_15 (* instance.y__AT0@1 .def_14))) (let ((.def_16 (= instance.y__AT0@2 .def_15))) (let ((.def_17 (* 970143.0 instance.x__AT0@2))) (let ((.def_18 (* (- 970143.0) instance.x__AT0@1))) (let ((.def_19 (+ .def_18 .def_17))) (let ((.def_20 (* (- 242536.0) instance.y__AT0@1))) (let ((.def_21 (+ .def_20 .def_19))) (let ((.def_22 (* 242536.0 instance.y__AT0@2))) (let ((.def_23 (+ .def_22 .def_21))) (let ((.def_24 (= .def_23 0.0))) (let ((.def_25 (and .def_24 .def_16))) (let ((.def_26 (not .def_9))) (let ((.def_27 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_28 (= instance.y__AT0@2 instance.y__AT0@1))) (let ((.def_29 (and .def_28 .def_27))) (let ((.def_30 (or .def_29 .def_26))) (let ((.def_31 (and .def_30 .def_25))) (let ((.def_32 (and .def_31 .def_6))) (let ((.def_33 (or .def_2 .def_32))) (let ((.def_34 (and .def_33 .def_10))) (let ((.def_35 (and .def_3 .def_2))) (let ((.def_36 (or .def_35 .def_34))) (let ((.def_37 (and .def_36 .def_11))) (let ((.def_38 (not .def_35))) (let ((.def_39 (or .def_38 .def_29))) (let ((.def_40 (and .def_39 .def_37))) (let ((.def_41 (not event_is_timed__AT0@1))) (let ((.def_42 (= event_is_timed__AT0@2 .def_41))) (let ((.def_43 (and .def_42 .def_40))) (let ((.def_44 (and .def_43 .def_4))) (let ((.def_45 (not instance.EVENT.1__AT0@0))) (let ((.def_46 (not instance.EVENT.0__AT0@0))) (let ((.def_47 (or .def_46 .def_45))) (let ((.def_48 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_49 (<= time__AT0@0 time__AT0@1))) (let ((.def_50 (or .def_45 .def_49))) (let ((.def_51 (and .def_50 .def_48))) (let ((.def_52 (= time__AT0@0 time__AT0@1))) (let ((.def_53 (or instance.EVENT.1__AT0@0 .def_52))) (let ((.def_54 (and .def_53 .def_51))) (let ((.def_55 (* (- 1.0) time__AT0@0))) (let ((.def_56 (+ .def_55 time__AT0@1))) (let ((.def_57 (exp .def_56))) (let ((.def_58 (* instance.y__AT0@0 .def_57))) (let ((.def_59 (= instance.y__AT0@1 .def_58))) (let ((.def_60 (+ .def_20 .def_18))) (let ((.def_61 (* 970143.0 instance.x__AT0@0))) (let ((.def_62 (+ .def_61 .def_60))) (let ((.def_63 (* 242536.0 instance.y__AT0@0))) (let ((.def_64 (+ .def_63 .def_62))) (let ((.def_65 (= .def_64 0.0))) (let ((.def_66 (and .def_65 .def_59))) (let ((.def_67 (not .def_52))) (let ((.def_68 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_69 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_70 (and .def_69 .def_68))) (let ((.def_71 (or .def_70 .def_67))) (let ((.def_72 (and .def_71 .def_66))) (let ((.def_73 (and .def_72 .def_49))) (let ((.def_74 (or .def_45 .def_73))) (let ((.def_75 (and .def_74 .def_53))) (let ((.def_76 (and .def_46 .def_45))) (let ((.def_77 (or .def_76 .def_75))) (let ((.def_78 (and .def_77 .def_54))) (let ((.def_79 (not .def_76))) (let ((.def_80 (or .def_79 .def_70))) (let ((.def_81 (and .def_80 .def_78))) (let ((.def_82 (not event_is_timed__AT0@0))) (let ((.def_83 (= event_is_timed__AT0@1 .def_82))) (let ((.def_84 (and .def_83 .def_81))) (let ((.def_85 (and .def_84 .def_47))) (let ((.def_86 (<= instance.x__AT0@0 (- (/ 1 2))))) (let ((.def_87 (not .def_86))) (let ((.def_88 (<= 0.0 instance.x__AT0@0))) (let ((.def_89 (not .def_88))) (let ((.def_90 (and .def_89 .def_87))) (let ((.def_91 (<= 0.0 instance.y__AT0@0))) (let ((.def_92 (not .def_91))) (let ((.def_93 (<= (- (/ 1 2)) instance.y__AT0@0))) (let ((.def_94 (and .def_93 .def_92))) (let ((.def_95 (and .def_94 .def_90))) (let ((.def_96 (= time__AT0@0 0.0))) (let ((.def_97 (and .def_96 .def_95))) (let ((.def_98 (and .def_97 .def_85 .def_44 .def_1))) .def_98)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/nl/nta/exp-4.5-lt.smt2 b/test/regress/regress0/nl/nta/exp-4.5-lt.smt2 new file mode 100644 index 000000000..b0d39ff44 --- /dev/null +++ b/test/regress/regress0/nl/nta/exp-4.5-lt.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(declare-fun x () Real) + +(assert (> (exp x) 2000.0)) +(assert (< x 4.5)) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 b/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 new file mode 100644 index 000000000..33806cf75 --- /dev/null +++ b/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(declare-fun x () Real) + +(assert (> (exp (- (/ 1 2))) 0.65)) +(assert (= x (exp (- (/ 1 2))))) + + +(check-sat) diff --git a/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 b/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 new file mode 100644 index 000000000..b0ea1b39e --- /dev/null +++ b/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(declare-fun x () Real) + +(assert (< (exp (- (/ 1 2))) 0.6)) +(assert (= x (exp (- (/ 1 2))))) + + +(check-sat) diff --git a/test/regress/regress0/nl/nta/exp1-lb.smt2 b/test/regress/regress0/nl/nta/exp1-lb.smt2 new file mode 100644 index 000000000..b0bc3079c --- /dev/null +++ b/test/regress/regress0/nl/nta/exp1-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (exp 1) 2.719)) +(assert (= x (exp 1))) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/exp1-ub.smt2 b/test/regress/regress0/nl/nta/exp1-ub.smt2 new file mode 100644 index 000000000..3b3a14c89 --- /dev/null +++ b/test/regress/regress0/nl/nta/exp1-ub.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (< (exp 1) 2.717)) +(assert (= x (exp 1))) + + +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin1-lb.smt2 b/test/regress/regress0/nl/nta/sin1-lb.smt2 new file mode 100644 index 000000000..f8070cdb8 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin1-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (sin 1) 0.842)) +(assert (= x (sin 1))) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin1-ub.smt2 b/test/regress/regress0/nl/nta/sin1-ub.smt2 new file mode 100644 index 000000000..47d322a77 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin1-ub.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (< (sin 1) 0.8414)) +(assert (= x (sin 1))) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin2-lb.smt2 b/test/regress/regress0/nl/nta/sin2-lb.smt2 new file mode 100644 index 000000000..686708230 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin2-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (sin 2) 0.96)) +(assert (= x (sin 2))) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin2-ub.smt2 b/test/regress/regress0/nl/nta/sin2-ub.smt2 new file mode 100644 index 000000000..51c9eb8a9 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin2-ub.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (< (sin 2) 0.901)) +(assert (= x (sin 2))) + +(check-sat) -- cgit v1.2.3