ar/assignments/src/4.py

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