ar/assignment1/src/a4.py

   1 #!/usr/bin/env python3
   2 import sys
   3 if len(sys.argv) != 2:
   4     print("usage: {} maxiterations".format(sys.argv[0]))
   5     exit()
   6
   7 iterations = int(sys.argv[1]) if len(sys.argv) > 1 else 11
   8 numa = 7
   9
  10 # Print preamble
  11 print("(benchmark a4.smt")
  12 print(":logic QF_UFLIA")
  13
  14 # Print variables
  15 print(":extrafuns (")
  16 print("(a{} Int)".format(1))
  17 print("(a{} Int)".format(numa))
  18 for i in range(iterations):
  19     for v in range(2, numa):
  20         print("(i{}a{} Int) ".format(i, v))
  21 print(")")
  22
  23 # Print preconditions
  24 print(":formula")
  25 print("(and")
  26 print("(= a1 1)")
  27 print("(= a{0} {0})".format(numa, numa))
  28 for i in range(2, numa):
  29     print("(= i0a{0} {0})".format(i))
  30
  31 # Print iterations
  32 for i in range(1, iterations):
  33     print("(or")
  34     for v in range(2, numa):
  35         print("(and")
  36         for ov in [k for k in range(2, numa) if k != v]:
  37             print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
  38         im1 = 'a1' if v == 2 else 'i{}a{}'.format(i, v-1)
  39         ip1 = 'a{}'.format(numa) if v == numa-1 else 'i{}a{}'.format(i-1, v+1)
  40         print("(= i{}a{} (+ {} {}))".format(i, v, im1, ip1))
  41         print(")")
  42     print(")")
  43
  44 #  Post conditions
  45 print("(or")
  46 for v in range(2, numa):
  47     print("(and (>= i{}a{} 50)".format(iterations-1, v))
  48     print("(or")
  49     for ov in [k for k in range(2, numa) if k != v]:
  50         print("(= i{0}a{1} i{0}a{2})".format(iterations-1, v, ov))
  51     print("))")
  52 print(")")
  53
  54 #  Close the and,benchmark parenthesis
  55 print("))")