From bf7f7d6960f6e03e90880dd3da9ff1bf00943cf3 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 31 Jul 2015 10:32:34 +0200
Subject: Sygus support for inductive datatypes.

---
 test/regress/regress0/sygus/Makefile.am |  3 ++-
 test/regress/regress0/sygus/sygus-dt.sy | 16 ++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100755 test/regress/regress0/sygus/sygus-dt.sy

(limited to 'test/regress/regress0/sygus')

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 9d7155f78..82ff67d41 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -43,7 +43,8 @@ TESTS = commutative.sy \
         enum-test.sy \
         no-syntax-test-bool.sy \
         inv-example.sy \
-        uminus_one.sy
+        uminus_one.sy \
+        sygus-dt.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy
new file mode 100755
index 000000000..e842477e8
--- /dev/null
+++ b/test/regress/regress0/sygus/sygus-dt.sy
@@ -0,0 +1,16 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi --no-dump-synth
+
+(set-logic LIA)
+
+(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
+(define-fun g ((x Int)) List (cons (+ x 1) nil))
+(define-fun i () List (cons 3 nil))
+
+(synth-fun f ((x Int)) List ((Start List ((g StartInt) i (cons StartInt Start) (nil) (tail Start)))
+                             (StartInt Int (x 0 1 (+ StartInt StartInt)))))
+
+(declare-var x Int)
+
+(constraint (= (f x) (cons x nil)))
+(check-synth)
\ No newline at end of file
-- 
cgit v1.2.3