started with the report

[master.git] / ar / assignments / src / 4.py

diff --git a/ar/assignments/src/4.py b/ar/assignments/src/4.py
new file mode 100644 (file)
index 0000000..e260264
--- /dev/null
+++ b/ar/assignments/src/4.py
@@ -0,0 +1,59 @@
+iterations = 11
+numa = 8
+
+##Print preamble
+print("(benchmark a4.smt")
+print(":logic QF_UFLIA")
+
+##Print variables
+print(":extrafuns (")
+print("(a{} Int)".format(1))
+print("(a{} Int)".format(numa))
+for i in range(iterations):
+    for v in range(2,numa):
+        print("(i{}a{} Int) ".format(i,v))
+    print("(c{} Int)".format(i))
+print(")")
+
+##Print preconditions
+print(":formula")
+print("(and")
+print("(= c0 0)")
+print("(= a1 1)")
+print("(= a{0} {0})".format(numa, numa))
+for i in range(2,numa):
+    print("(= i0a{0} {0})".format(i))
+
+##Print iterations
+for i in range(1, iterations):
+    print("(or")
+    for v in range(2, numa):
+        print("(and")
+        print("(= c{} {})".format(i, v))
+        for ov in [k for k in range(2, numa) if k != v]:
+            print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
+        im1 = 'a1' if v == 2 else 'i{}a{}'.format(i, v-1)
+        ip1 = 'a{}'.format(numa) if v == numa-1 else 'i{}a{}'.format(i-1, v+1)
+        print("(= i{}a{} (+ {} {}))".format(i, v, im1, ip1))
+        print(")")
+    print("(and")
+    print("(= c{} 0)".format(i))
+    for ov in range(2, numa):
+        print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
+    print(")")
+    print(")")
+
+
+## Post conditions
+print("(or")
+for v in range(2, numa):
+    print("(and (>= i{}a{} 50)".format(iterations-1, v))
+    print("(or")
+    for ov in [k for k in range(2, numa) if k != v]:
+        print("(= i{0}a{1} i{0}a{2})".format(iterations-1, v, ov))
+    print("))")
+
+
+print(")")
+## Close the and,benchmark parenthesis
+print("))")