diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-08 18:06:16 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-08 16:06:16 -0700 |
commit | 1b6784fe52f4fb745262842e0406d6dd34053cb2 (patch) | |
tree | 6c64a7485612f8af60631fde4dd827222d17215d /test | |
parent | 16b54708ff83a1bf6393203b79da6dc059fd2025 (diff) |
Limit cases of sygus inference based on type (#3370)
This makes `--sygus-inference` a no-op for inputs where there is a free function whose sort cannot be handled in a sygus grammar.
It also fixes an issue where skolem variables were not being treated as functions-to-synthesize.
Fixes #3250 and fixes #3356.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 | 14 |
3 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 94f9496f3..7951a9c41 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -905,6 +905,7 @@ set(regress_0_tests regress0/sygus/dt-sel-parse1.sy regress0/sygus/hd-05-d1-prog-nogrammar.sy regress0/sygus/inv-different-var-order.sy + regress0/sygus/issue3356-syg-inf-usort.smt2 regress0/sygus/let-ringer.sy regress0/sygus/let-simp.sy regress0/sygus/no-syntax-test-bool.sy @@ -1383,6 +1384,7 @@ set(regress_1_tests regress1/quantifiers/is-even.smt2 regress1/quantifiers/isaplanner-goal20.smt2 regress1/quantifiers/issue2970-string-var-elim.smt2 + regress1/quantifiers/issue3250-syg-inf-q.smt2 regress1/quantifiers/issue3317.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 diff --git a/test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 b/test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 new file mode 100644 index 000000000..b35b7253c --- /dev/null +++ b/test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --sygus-inference +; EXPECT: sat +(set-logic ALL) +(declare-sort S 1) +(define-sort SB () (S Bool)) +(declare-fun A () (S Bool)) +(declare-fun B () SB) +(assert (= A B)) +; do not do sygus inference due to uninterpreted sorts +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 b/test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 new file mode 100644 index 000000000..bb6a63490 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () Real) +(assert + (and + (and + (exists ((?b Real)) (forall ((?c Real)) (exists ((?d Real)) + (or (and (and (and (and (< (+ (+ (+ 0 (* 68.0 ?c)) 0) (* 33.0 a)) 0.0) (<= 0 2.0)) + (or (<= 0 (+ (* (+ (* 55.0 ?d) 0) (* 49.0 ?b)) 0)))))))))) + ) + ) +) + +(check-sat) |