+++ /dev/null
-niter = range(500)
-nvar = range(7)
-
-for a in niter:
- for b in nvar:
- print '(define a_{}_{}::int)'.format(a, b)
-
-for a in nvar:
- print '(assert (= a_0_{} {}))'.format(a, a+1)
-
-for a in niter[1:]:
- for b in nvar[1:-1]:
- print '(assert (= a_{0}_{1} (+ a_{2}_{3} a_{2}_{4})))'.format(
- a, b, a-1, b-1, b+1)
-
-for a in niter[1:]:
- print '(assert (= a_{}_0 a_{}_0))'.format(a-1, a)
- print '(assert (= a_{}_6 a_{}_6))'.format(a-1, a)
-
-
-print '(assert (or',
-for a in niter:
- for b1 in nvar:
- for b2 in nvar:
- if b1 != b2:
- print '(and (>= a_{0}_{1} 50) (= a_{0}_{2} a_{0}_{1}))'.format(
- a, b1, b2),
-print '))'
-
-print '(check)'
-print '(show-model)'