-
Notifications
You must be signed in to change notification settings - Fork 0
/
generator_smtlib.py
67 lines (59 loc) · 1.56 KB
/
generator_smtlib.py
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
# Ali Yunus Emre Özköse
# BBM405 HW-2
# n-queen input file is generated as below
# dynamic params:
# n: number of queen
#
# IT IS NOT Z3 WRAPPER. IT IS JUST PREPARING TEXTUAL INPUT FOR Z3 BUILD
# ################## % ################## #
n = 8
print("(and")
print("; at least 1 true in row")
print("(and")
for i in range(1, n + 1):
temp = "(or"
for j in range(1, n+1):
temp += " (p {} {})".format(i, j)
temp += ")"
print("\t"+temp)
print(")")
print()
print("; at most 1 true in row")
print("(and")
for i in range(1, n + 1):
for j in range(1, n+1):
for k in range(1, n+1):
if j < k:
print("\t(or (not (p {} {})) (not (p {} {})))".format(i, j, i, k))
print(")")
print()
print("; at least 1 true in col")
print("(and")
for j in range(1, n + 1):
temp = "(or"
for i in range(1, n+1):
temp += " (p {} {})".format(i, j)
temp += ")"
print("\t"+temp)
print(")")
print()
print("; at most 1 true in col")
print("(and")
for j in range(1, n + 1):
for i in range(1, n+1):
for k in range(1, n+1):
if j < k:
print("\t(or (not (p {} {})) (not (p {} {})))".format(i, j, i, k))
print(")")
print()
print("; at most 1 queen at diagonals")
print("(and")
for i in range(1, n + 1):
for i_ in range(1, n + 1):
if i < i_:
for j in range(1, n+1):
for j_ in range(1, n+1):
if i+j == i_+j_ or i-j == i_-j_:
print("\t(or (not (p {} {})) (not (p {} {})))".format(i, j, i_, j_))
print(")")
print(")")