cleaned up old directory

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

diff --git a/ar/assignments/src/a4.py b/ar/assignments/src/a4.py
deleted file mode 100644 (file)
index 51d5347..0000000
--- a/ar/assignments/src/a4.py
+++ /dev/null
@@ -1,60 +0,0 @@
-#!/usr/bin/env python3
-import sys
-iterations = int(sys.argv[1]) if len(sys.argv) > 1 else 11
-numa = int(sys.argv[2]) if len(sys.argv) > 2 else 7
-
-##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("))")