summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-10-08 18:06:16 -0500
committerAndres Noetzli <andres.noetzli@gmail.com>2019-10-08 16:06:16 -0700
commit1b6784fe52f4fb745262842e0406d6dd34053cb2 (patch)
tree6c64a7485612f8af60631fde4dd827222d17215d /test
parent16b54708ff83a1bf6393203b79da6dc059fd2025 (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.txt2
-rw-r--r--test/regress/regress0/sygus/issue3356-syg-inf-usort.smt211
-rw-r--r--test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt214
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback