diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-23 12:29:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-23 12:29:58 -0500 |
commit | 5f384849d20c915374c7b189a232c5d811c186ef (patch) | |
tree | 26c830da54c5536cd28462ce4fd274e394b32314 /test/regress/regress0/sygus | |
parent | 2a96d7de381aa565a6eacf724848c0e7839c7cf6 (diff) |
Fix sygus datatype parsing in sygus v1 format (#3113)
Diffstat (limited to 'test/regress/regress0/sygus')
-rw-r--r-- | test/regress/regress0/sygus/dt-sel-parse1.sy | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/dt-sel-parse1.sy b/test/regress/regress0/sygus/dt-sel-parse1.sy new file mode 100644 index 000000000..52edb3278 --- /dev/null +++ b/test/regress/regress0/sygus/dt-sel-parse1.sy @@ -0,0 +1,48 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat +(set-logic ALL_SUPPORTED) + +(declare-datatypes ((IntRange 0)) + (((IntRange (lower Int) (upper Int))))) + +(declare-datatypes ((Loc 0)) + (((Loc (x Int) (y Int))))) + +(declare-datatypes ((LocRange 0)) + (((LocRange (xD IntRange) (yD IntRange))))) + +(declare-datatypes ((Ship 0)) + (((Ship (shipCapacity Int) (shipLoc Loc))))) + +(declare-datatypes ((ShipRange 0)) + (((ShipRange (shipCapacityD IntRange) (shipLocD LocRange))))) + +(define-fun max ((x Int) (y Int)) Int + (ite (>= x y) x y) +) + +(define-fun min ((x Int) (y Int)) Int + (ite (<= x y) x y) +) + +; provide synthesis template +(synth-fun f ((secret Ship) (prior ShipRange) (response Bool)) ShipRange +( + (Start ShipRange ((ite B SR SR))) + (B Bool (response)) + (SR ShipRange ((ShipRange IR LR) prior)) + (IR IntRange ((IntRange I I) (shipCapacityD SR))) + (LR LocRange ((LocRange IR IR) (shipLocD SR))) + (I Int ((lower IR) (upper IR) + (max I (lower (shipCapacityD SR))) + (min I I) 50 51)) + ) +) + +(declare-var secret Ship) +(declare-var prior ShipRange) +(declare-var response Bool) + +(constraint true) + +(check-synth) |