diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-22 09:01:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-22 09:01:13 -0500 |
| commit | d5ad777c539f5a49e1cdf4e483c2d5d689738b12 (patch) | |
| tree | d69e66580008f800d5e283c54887448640d1e3f0 /test/regress/regress1 | |
| parent | f7336df0c8ace6c0d73fefc2d2e54966599ee40b (diff) | |
More fixes for PBE with datatypes (#2882)
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/sygus/tester.sy | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy new file mode 100644 index 000000000..261666dd4 --- /dev/null +++ b/test/regress/regress1/sygus/tester.sy @@ -0,0 +1,37 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic SLIA) +(declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool)))) + +(define-fun isA ((i DT)) Bool ((_ is A) i) ) +(define-fun isB ((i DT)) Bool ((_ is B) i) ) + +(synth-fun add ((x1 DT)) DT + ( + (Start DT (ntDT)) + (ntDT DT + ( x1 x2 + (JSBool ntBool) + (A ntInt) + (ite ntBool ntDT ntDT) + ) + ) + (ntBool Bool + ( + (isA ntDT) + (isB ntDT) + (jsBool ntDT) + ) + ) + (ntInt Int + (1 + (a ntDT) + (+ ntInt ntInt) + ) + ) + ) +) +(constraint (= (add (A 6)) (A 7))) +(constraint (= (add (B "j")) (B "j"))) +(check-synth) |