blob: 05ba6b85eb74d020a6ee1769b63fd46df52c8839 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
; EXPECT: unsat
(set-logic ALL)
(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) (B Bool) (SR ShipRange) (IR IntRange) (LR LocRange) (I Int))
(
(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)
|
