diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-12 19:35:01 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-12 21:35:01 -0500 |
commit | 43cec89207dd1043608273769a20309167ad3c90 (patch) | |
tree | 6a69ac4d89d976ea552e6e6786c4cc8a2cf9291d /test | |
parent | 8597f207187baff3b9f8cc5d8955e5b96d6d57d0 (diff) |
Reset input language for ExprMiner subsolver (#2624)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 4 | ||||
-rw-r--r-- | test/regress/Makefile.tests | 2 | ||||
-rw-r--r-- | test/regress/regress1/rr-verify/fp-arith.sy | 34 | ||||
-rw-r--r-- | test/regress/regress1/rr-verify/fp-bool.sy | 50 |
4 files changed, 89 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 902ddf0f9..aef40d373 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1168,8 +1168,8 @@ set(regress_1_tests regress1/nl/dist-big.smt2 regress1/nl/div-mod-partial.smt2 regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 - regress1/nl/exp-approx.smt2 regress1/nl/exp-4.5-lt.smt2 + regress1/nl/exp-approx.smt2 regress1/nl/exp1-lb.smt2 regress1/nl/exp_monotone.smt2 regress1/nl/factor_agg_s.smt2 @@ -1412,6 +1412,8 @@ set(regress_1_tests regress1/rr-verify/bool-crci.sy regress1/rr-verify/bv-term-32.sy regress1/rr-verify/bv-term.sy + regress1/rr-verify/fp-arith.sy + regress1/rr-verify/fp-bool.sy regress1/rr-verify/regex.sy regress1/rr-verify/string-term.sy regress1/sep/chain-int.smt2 diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 91f33721a..b4e151a17 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1409,6 +1409,8 @@ REG1_TESTS = \ regress1/rr-verify/bool-crci.sy \ regress1/rr-verify/bv-term-32.sy \ regress1/rr-verify/bv-term.sy \ + regress1/rr-verify/fp-arith.sy \ + regress1/rr-verify/fp-bool.sy \ regress1/rr-verify/regex.sy \ regress1/rr-verify/string-term.sy \ regress1/sep/chain-int.smt2 \ diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy new file mode 100644 index 000000000..1b056271c --- /dev/null +++ b/test/regress/regress1/rr-verify/fp-arith.sy @@ -0,0 +1,34 @@ +; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break +; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") +; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' +; EXIT: 1 + +(set-logic FP) + +(define-fun fp_plus_zero () Float16 (_ +zero 5 11)) +(define-fun fp_minus_zero () Float16 (_ -zero 5 11)) +(define-fun fp_plus_inf () Float16 (_ +oo 5 11)) +(define-fun fp_minus_inf () Float16 (_ -oo 5 11)) +(define-fun fp_nan () Float16 (_ NaN 5 11)) + +(synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Float16 +( + (Start Float16 ( + (fp.abs Start) + (fp.neg Start) + (fp.add r Start Start) + (fp.sub r Start Start) + (fp.mul r Start Start) + (fp.div r Start Start) + (fp.sqrt r Start) + (fp.rem Start Start) + x + y + fp_plus_zero + fp_minus_zero + fp_plus_inf + fp_minus_inf + fp_nan + )) +)) +(check-synth) diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy new file mode 100644 index 000000000..e94319401 --- /dev/null +++ b/test/regress/regress1/rr-verify/fp-bool.sy @@ -0,0 +1,50 @@ +; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break +; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") +; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' +; EXIT: 1 + +(set-logic FP) + +(define-fun fp_plus_zero () Float16 (_ +zero 5 11)) +(define-fun fp_minus_zero () Float16 (_ -zero 5 11)) +(define-fun fp_plus_inf () Float16 (_ +oo 5 11)) +(define-fun fp_minus_inf () Float16 (_ -oo 5 11)) +(define-fun fp_nan () Float16 (_ NaN 5 11)) + +(synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Bool +( + (Start Bool ( + (fp.isNaN FpOp) + (fp.isNegative FpOp) + (fp.isPositive FpOp) + (fp.isZero FpOp) + (fp.isSubnormal FpOp) + (fp.isNormal FpOp) + (and Start Start) + (or Start Start) + (not Start Start) + true + false + )) + + (FpOp Float16 ( + (fp.abs FpOp) + (fp.neg FpOp) + (fp.add r FpOp FpOp) + (fp.sub r FpOp FpOp) + (fp.mul r FpOp FpOp) + (fp.div r FpOp FpOp) + (fp.sqrt r FpOp) + (fp.rem FpOp FpOp) + x + y + fp_plus_zero + fp_minus_zero + fp_plus_inf + fp_minus_inf + fp_nan + (ite Start FpOp FpOp) + )) + +)) +(check-synth) |