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/regress/regress1/sygus | |
| parent | 91f9355868d01999fd729544ea50ccd745e84d35 (diff) | |
Rewrite selectors correctly applied to constructors (#2875)
Diffstat (limited to 'test/regress/regress1/sygus')
| -rw-r--r-- | test/regress/regress1/sygus/double.sy | 26 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/extract.sy | 19 |
2 files changed, 45 insertions, 0 deletions
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)
|