blob: 4b08a937dff5f8dcd8280baa7cfae45cf055eaf1 (
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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(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 betweenInt ((x Int) (r IntRange)) Bool
(and (< (lower r) x) (< x (upper r)))
)
(define-fun betweenLoc ((l Loc) (lr LocRange)) Bool
(and (betweenInt (x l) (xD lr)) (betweenInt (y l) (yD lr)))
)
(define-fun subsetInt ((r1 IntRange) (r2 IntRange)) Bool
(and (>= (lower r1) (lower r2)) (<= (upper r1) (upper r2)))
)
(define-fun betweenShip ((s Ship) (sr ShipRange)) Bool
(and (betweenInt (shipCapacity s) (shipCapacityD sr)) (betweenLoc (shipLoc s) (shipLocD sr)))
)
(define-fun atLeast ((s Ship)) Bool
(> (shipCapacity s) 50)
)
(define-fun subsetLoc ((s1 LocRange) (s2 LocRange)) Bool
(and (subsetInt (xD s1) (xD s2)) (subsetInt (yD s1) (yD s2)))
)
(define-fun subsetShip ((s1 ShipRange) (s2 ShipRange)) Bool
(and (subsetInt (shipCapacityD s1) (shipCapacityD s2)) (subsetLoc (shipLocD s1) (shipLocD s2)))
)
(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)
)
(synth-fun f ((secret Ship) (prior ShipRange) (response Bool)) ShipRange
)
(declare-var secret Ship)
(declare-var prior ShipRange)
(declare-var response Bool)
(constraint (=> (betweenShip secret prior)
(=> (betweenShip secret (f secret prior response))
(= response
(and (atLeast secret)
(subsetShip (f secret prior response) prior))))
))
(check-synth)
|
