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
|
#!/usr/bin/env python
import sys
# i = 1..8
n = 8
steps = int(sys.argv[1])
literals = []
preds = []
def fillin(cases, template_vars):
if type(cases) == str:
return cases.format(**template_vars)
return [template.format(**template_vars) for template in cases]
# a. Repeat a number of steps, check in each step
# if a_3 = a_7 is possible in that step.
# Number a_i in step s is encoded as a_i_s.
# The initial state is a_i_0.
for step in range(steps + 1):
for i in range(1, n + 1):
literals += ["a{i}_{step}".format(**vars())]
# Initial state, a_i_0 = i
for i in range(1, n + 1):
preds += ["(= a{i}_0 {i})".format(i=i)]
# Goal: have a_3 = a_7 in any step:
preds += [
"(or %s)" % " ".join("(= a3_{i} a7_{i})".format(i=i)
for i in range(steps + 1))
]
# In each step, can sum neighbors (leaving others unchanged).
for step in range(1, steps + 1):
# The first and last one cannot be changed. In a step, one can choose to
# change a_i for any i, leaving all other j (i != j) intact.
altpreds = []
for i in range(2, n):
laststep = step - 1
prev = i - 1
next = i + 1
# Require a'_i = a_{i-1} + a_{i+1}
statepreds = fillin([
"(= a{i}_{step} (+ a{prev}_{laststep} a{next}_{laststep}))"
], vars())
# Require a'_j = a_j for i != j
for j in range(1, n + 1):
if i == j:
continue
statepreds += fillin([
"(= a{j}_{step} a{j}_{laststep})"
], vars())
# All assignments must apply for this step.
altpreds += [
"(and %s)" % "\n".join(statepreds)
]
preds += [
"(or",
"%s" % "\n".join(altpreds),
")"
]
# Begin generator
s = """(benchmark test.smt
:logic QF_UFLIA
:extrafuns (
"""
s += "\n".join("(%s Int)" % x for x in literals)
s += """
)
:formula (and
"""
s += "\n".join(preds)
s += """
))
"""
try:
import sys
print(s)
# Hack to avoid printing a ugly error in case stdin of next pipe is closed.
sys.stdout.flush()
sys.stdout.close()
except BrokenPipeError:
pass
|