From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 23 Sep 2015 18:02:01 +0000 (+0200)
Subject: started with ar
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=08ebf143cfef8cf3f3746a4e02d3fecc787cdfb7;p=master.git

started with ar
---

diff --git a/ar/assignments/as11.py b/ar/assignments/as11.py
deleted file mode 100644
index 4df0a0c..0000000
--- a/ar/assignments/as11.py
+++ /dev/null
@@ -1,31 +0,0 @@
-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)'
diff --git a/ar/assignments/prnijm.pdf b/ar/assignments/prnijm.pdf
new file mode 100644
index 0000000..a65fb82
Binary files /dev/null and b/ar/assignments/prnijm.pdf differ
diff --git a/ar/tests/test1.smt b/ar/tests/test1.smt
new file mode 100644
index 0000000..82c943c
--- /dev/null
+++ b/ar/tests/test1.smt
@@ -0,0 +1,9 @@
+(benchmark test1.smt
+:logic QF_UFLIA
+:extrafuns ((A Int) (B Int) (C Int) (D Int))
+:formula (and
+(> (* 2 A) (+ B C))
+(> (* 2 B) (+ C D))
+(> (* 2 C) (* 3 D))
+(> (* 3 D) (+ A C))
+))