ar/assignments/src/a4.py

   1 #!/usr/bin/env python3
   2 import sys
   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
   5
   6 ##Print preamble
   7 print("(benchmark a4.smt")
   8 print(":logic QF_UFLIA")
   9
  10 ##Print variables
  11 print(":extrafuns (")
  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))
  18 print(")")
  19
  20 ##Print preconditions
  21 print(":formula")
  22 print("(and")
  23 print("(= c0 0)")
  24 print("(= a1 1)")
  25 print("(= a{0} {0})".format(numa, numa))
  26 for i in range(2,numa):
  27     print("(= i0a{0} {0})".format(i))
  28
  29 ##Print iterations
  30 for i in range(1, iterations):
  31     print("(or")
  32     for v in range(2, numa):
  33         print("(and")
  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))
  40         print(")")
  41     print("(and")
  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))
  45     print(")")
  46     print(")")
  47
  48
  49 ## Post conditions
  50 print("(or")
  51 for v in range(2, numa):
  52     print("(and (>= i{}a{} 50)".format(iterations-1, v))
  53     print("(or")
  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))
  56     print("))")
  57 print(")")
  58
  59 ## Close the and,benchmark parenthesis
  60 print("))")