updatesssss
authorMart Lubbers <mart@martlubbers.net>
Tue, 15 Sep 2015 19:48:10 +0000 (21:48 +0200)
committerMart Lubbers <mart@martlubbers.net>
Tue, 15 Sep 2015 19:48:10 +0000 (21:48 +0200)
ar/assignments/.gitignore [new file with mode: 0644]
ar/assignments/as11.py [new file with mode: 0644]
ct/syllabus.pdf [moved from complexity_theory/syllabus.pdf with 100% similarity]

diff --git a/ar/assignments/.gitignore b/ar/assignments/.gitignore
new file mode 100644 (file)
index 0000000..9aa6a64
--- /dev/null
@@ -0,0 +1 @@
+output.log
diff --git a/ar/assignments/as11.py b/ar/assignments/as11.py
new file mode 100644 (file)
index 0000000..4df0a0c
--- /dev/null
@@ -0,0 +1,31 @@
+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)'