diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-21 13:41:46 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-21 13:41:46 -0500 |
| commit | 6c8a2652605b031182b3c2c25d237719470f5620 (patch) | |
| tree | 0061019093bb4a892625acab3b2996381dc0127b /test | |
| parent | 91f9355868d01999fd729544ea50ccd745e84d35 (diff) | |
Rewrite selectors correctly applied to constructors (#2875)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/double.sy | 26 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/extract.sy | 19 |
3 files changed, 47 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 21e08f2bf..083f8df75 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1605,8 +1605,10 @@ set(regress_1_tests regress1/sygus/crcy-si-rcons.sy regress1/sygus/crcy-si.sy regress1/sygus/cube-nia.sy + regress1/sygus/double.sy regress1/sygus/dt-test-ns.sy regress1/sygus/dup-op.sy + regress1/sygus/extract.sy regress1/sygus/fg_polynomial3.sy regress1/sygus/find_sc_bvult_bvnot.sy regress1/sygus/hd-01-d1-prog.sy diff --git a/test/regress/regress1/sygus/double.sy b/test/regress/regress1/sygus/double.sy new file mode 100644 index 000000000..f3fea3122 --- /dev/null +++ b/test/regress/regress1/sygus/double.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic SLIA)
+(declare-datatype Ex ((Ex2 (ex Int))))
+
+(synth-fun double ((x1 Ex)) Int
+ (
+ (Start Int (ntInt))
+ (ntInt Int
+ (
+ (ex ntEx)
+ (+ ntInt ntInt)
+ )
+ )
+ (ntEx Ex
+ (
+ x1
+ (Ex2 ntInt)
+ )
+ )
+ )
+)
+(constraint (= (double (Ex2 1)) 2))
+(constraint (= (double (Ex2 4)) 8))
+(check-synth)
diff --git a/test/regress/regress1/sygus/extract.sy b/test/regress/regress1/sygus/extract.sy new file mode 100644 index 000000000..d1541fa87 --- /dev/null +++ b/test/regress/regress1/sygus/extract.sy @@ -0,0 +1,19 @@ +; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic ALL_SUPPORTED)
+(declare-datatype Ex ((Ex2 (ex Int))))
+
+(synth-fun ident ((x1 Ex)) Int
+ (
+ (Start Int (ntInt))
+ (ntInt Int
+ (
+ (ex ntEx)
+ )
+ )
+ (ntEx Ex ( x1 ) )
+ )
+)
+(constraint (= (ident (Ex2 1)) 1))
+(check-synth)
|