3 iterations
= int(sys
.argv
[1]) if len(sys
.argv
) > 1 else 11
4 numa
= int(sys
.argv
[2]) if len(sys
.argv
) > 2 else 7
7 print("(benchmark a4.smt")
8 print(":logic QF_UFLIA")
12 print("(a{} Int)".format(1))
13 print("(a{} Int)".format(numa
))
14 for i
in range(iterations
):
15 for v
in range(2,numa
):
16 print("(i{}a{} Int) ".format(i
,v
))
17 print("(c{} Int)".format(i
))
25 print("(= a{0} {0})".format(numa
, numa
))
26 for i
in range(2,numa
):
27 print("(= i0a{0} {0})".format(i
))
30 for i
in range(1, iterations
):
32 for v
in range(2, numa
):
34 print("(= c{} {})".format(i
, v
))
35 for ov
in [k
for k
in range(2, numa
) if k
!= v
]:
36 print("(= i{0}a{1} i{2}a{1})".format(i
, ov
, i
-1))
37 im1
= 'a1' if v
== 2 else 'i{}a{}'.format(i
, v
-1)
38 ip1
= 'a{}'.format(numa
) if v
== numa
-1 else 'i{}a{}'.format(i
-1, v
+1)
39 print("(= i{}a{} (+ {} {}))".format(i
, v
, im1
, ip1
))
42 print("(= c{} 0)".format(i
))
43 for ov
in range(2, numa
):
44 print("(= i{0}a{1} i{2}a{1})".format(i
, ov
, i
-1))
51 for v
in range(2, numa
):
52 print("(and (>= i{}a{} 50)".format(iterations
-1, v
))
54 for ov
in [k
for k
in range(2, numa
) if k
!= v
]:
55 print("(= i{0}a{1} i{0}a{2})".format(iterations
-1, v
, ov
))
59 ## Close the and,benchmark parenthesis