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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
from z3 import *
class Car():
def __init__(self, is_vertical, base_pos, length, start, color):
self.is_vertical = is_vertical
self.base = base_pos
self.length = length
self.start = start
self.color = color
def __eq__(self, other):
return self.color == other.color
def __ne__(self, other):
return self.color != other.color
dimension = 6
red_car = Car(False, 2, 2, 3, "red")
cars = [
Car(True, 0, 3, 0, 'yellow'),
Car(False, 3, 3, 0, 'blue'),
Car(False, 5, 2, 0, "brown"),
Car(False, 0, 2, 1, "lgreen"),
Car(True, 1, 2, 1, "light blue"),
Car(True, 2, 2, 1, "pink"),
Car(True, 2, 2, 4, "dark green"),
red_car,
Car(True, 3, 2, 3, "purple"),
Car(False, 5, 2, 3, "light yellow"),
Car(True, 4, 2, 0, "orange"),
Car(False, 4, 2, 4, "black"),
Car(True, 5, 3, 1, "light purple")
]
num_cars = len(cars)
B = BoolSort()
bv3 = BitVecSort(3)
state = Function('state', [ bv3 for c in cars] + [B])
def num(i):
return BitVecVal(i,bv3)
def bound(i):
return Const(cars[i].color, bv3)
fp = Fixedpoint()
fp.set("fp.engine","datalog")
fp.set("datalog.generate_explanations",True)
fp.declare_var([bound(i) for i in range(num_cars)])
fp.register_relation(state)
def mk_state(car, value):
return state([ (num(value) if (cars[i] == car) else bound(i)) for i in range(num_cars)])
def mk_transition(row, col, i0, j, car0):
body = [mk_state(car0, i0)]
for index in range(num_cars):
car = cars[index]
if car0 != car:
if car.is_vertical and car.base == col:
for i in range(dimension):
if i <= row and row < i + car.length and i + car.length <= dimension:
body += [bound(index) != num(i)]
if car.base == row and not car.is_vertical:
for i in range(dimension):
if i <= col and col < i + car.length and i + car.length <= dimension:
body += [bound(index) != num(i)]
s = "%s %d->%d" % (car0.color, i0, j)
fp.rule(mk_state(car0, j), body, s)
def move_down(i, car):
free_row = i + car.length
if free_row < dimension:
mk_transition(free_row, car.base, i, i + 1, car)
def move_up(i, car):
free_row = i - 1
if 0 <= free_row and i + car.length <= dimension:
mk_transition(free_row, car.base, i, i - 1, car)
def move_left(i, car):
free_col = i - 1;
if 0 <= free_col and i + car.length <= dimension:
mk_transition(car.base, free_col, i, i - 1, car)
def move_right(i, car):
free_col = car.length + i
if free_col < dimension:
mk_transition(car.base, free_col, i, i + 1, car)
# Initial state:
fp.fact(state([num(cars[i].start) for i in range(num_cars)]))
# Transitions:
for car in cars:
for i in range(dimension):
if car.is_vertical:
move_down(i, car)
move_up(i, car)
else:
move_left(i, car)
move_right(i, car)
def get_instructions(ans):
lastAnd = ans.arg(0).children()[-1]
trace = lastAnd.children()[1]
while trace.num_args() > 0:
print(trace.decl())
trace = trace.children()[-1]
goal = state([ (num(4) if cars[i] == red_car else bound(i)) for i in range(num_cars)])
fp.query(goal)
get_instructions(fp.get_answer())
del goal
del state
del fp
|
