final ar

[master.git] / ar / assignment1 / src / a4.py

diff --git a/ar/assignment1/src/a4.py b/ar/assignment1/src/a4.py
deleted file mode 100644 (file)
index 8883695..0000000
--- a/ar/assignment1/src/a4.py
+++ /dev/null
@@ -1,53 +0,0 @@
-#!/usr/bin/env python3
-import sys
-if len(sys.argv) != 2:
-    print("usage: {} maxiterations".format(sys.argv[0]))
-    exit()
-
-iterations = int(sys.argv[1]) if len(sys.argv) > 1 else 11
-numa = 7
-
-# Print variables and preamble
-print("(benchmark a4.smt")
-print(":logic QF_UFLIA")
-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(")")
-
-# Print preconditions
-print(":formula")
-print("(and")
-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")
-        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(")")
-
-#  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("))")