diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-02 09:40:36 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-02 09:40:36 -0500 |
commit | 613bf2cc56a80af66f2cad9e55374136c5a346f8 (patch) | |
tree | 1378a3c216635f578fd4c2105d90e9dc28318a60 /test/regress | |
parent | 71d0ce95f1e5ab74f3b0074494d4e8a4137fd079 (diff) |
Fix solution filtering for streaming abducts (#3143)
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus-abduct-ex1-grammar.smt2 | 28 |
2 files changed, 29 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2c65c7e14..99b464d09 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1630,6 +1630,7 @@ set(regress_1_tests regress1/strings/type002.smt2 regress1/strings/type003.smt2 regress1/strings/username_checker_min.smt2 + regress1/sygus-abduct-ex1-grammar.smt2 regress1/sygus-abduct-test.smt2 regress1/sygus-abduct-test-user.smt2 regress1/sygus/VC22_a.sy diff --git a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 new file mode 100644 index 000000000..17971f184 --- /dev/null +++ b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 @@ -0,0 +1,28 @@ +; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=3 +; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.") +; SCRUBBER: sed -e 's/.*(>= j (+ 1 1))/SPURIOUS/; s/(define-fun.*//; /^$/d' +; EXIT: 1 + +(set-logic QF_LIA) +(set-option :produce-abducts true) + +(declare-fun n () Int) +(declare-fun m () Int) +(declare-fun i () Int) +(declare-fun j () Int) + +(assert (and (>= n 0) (>= m 0))) +(assert (< n i)) +(assert (< (+ i j) m)) + +; This test ensures that (>= j (+ 1 1)) is not printed as a solution, +; since it is spurious: (>= j 0) is a stronger solution and will be enumerated +; first. +(get-abduct A + (not (<= n m)) + ((GA Bool) (GI Int)) + ( + (GA Bool ((>= GI GI))) + (GI Int ((+ GI GI) (- GI) i j 0 1)) + ) +) |