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 variables and preamble
  11 print("(benchmark a4.smt")
  12 print(":logic QF_UFLIA")
  13 print(":extrafuns (")
  14 print("(a{} Int)".format(1))
  15 print("(a{} Int)".format(numa))
  16 for i in range(iterations):
  17     for v in range(2, numa):
  18         print("(i{}a{} Int) ".format(i, v))
  19 print(")")
  20
  21 # Print preconditions
  22 print(":formula")
  23 print("(and")
  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         for ov in [k for k in range(2, numa) if k != v]:
  35             print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
  36         im1 = 'a1' if v == 2 else 'i{}a{}'.format(i, v-1)
  37         ip1 = 'a{}'.format(numa) if v == numa-1 else 'i{}a{}'.format(i-1, v+1)
  38         print("(= i{}a{} (+ {} {}))".format(i, v, im1, ip1))
  39         print(")")
  40     print(")")
  41
  42 #  Post conditions
  43 print("(or")
  44 for v in range(2, numa):
  45     print("(and (>= i{}a{} 50)".format(iterations-1, v))
  46     print("(or")
  47     for ov in [k for k in range(2, numa) if k != v]:
  48         print("(= i{0}a{1} i{0}a{2})".format(iterations-1, v, ov))
  49     print("))")
  50 print(")")
  51
  52 #  Close the and,benchmark parenthesis
  53 print("))")