ar/assignments/as11.py

   1 niter = range(10)
   2 nvar = range(7)
   3
   4 for a in niter:
   5     for b in nvar:
   6         print '(define a_{}_{}::int)'.format(a, b)
   7
   8 for a in nvar:
   9     print '(assert (= a_0_{} {}))'.format(a, a+1)
  10
  11 for a in niter[1:]:
  12     for b in nvar[1:-1]:
  13         print '(assert (= a_{0}_{1} (+ a_{2}_{3} a_{2}_{4})))'.format(
  14                 a, b, a-1, b-1, b+1)
  15
  16 for a in niter[1:]:
  17     print '(assert (= a_{}_0 a_{}_0))'.format(a-1, a)
  18     print '(assert (= a_{}_6 a_{}_6))'.format(a-1, a)
  19
  20
  21 print '(assert (or',
  22 for a in niter:
  23     for b1 in nvar:
  24         for b2 in nvar:
  25             if b1 != b2:
  26                 print '(and (>= a_{0}_{1} 50) (= a_{0}_{2} a_{0}_{1}))'.format(
  27                         a, b1, b2),
  28 print '))'
  29
  30 print '(check)'
  31 print '(show-model)'