update ar
authorMart Lubbers <mart@martlubbers.net>
Thu, 1 Oct 2015 17:14:14 +0000 (19:14 +0200)
committerMart Lubbers <mart@martlubbers.net>
Thu, 1 Oct 2015 17:14:14 +0000 (19:14 +0200)
ar/assignments/4.py [new file with mode: 0644]
ar/assignments/a11.smt [new file with mode: 0644]

diff --git a/ar/assignments/4.py b/ar/assignments/4.py
new file mode 100644 (file)
index 0000000..ae1fb4b
--- /dev/null
@@ -0,0 +1,23 @@
+
+if __name__ == '__main__':
+    frontier = [(0, [], range(1, 8))]
+    oldlen = 0
+    iterations = 0
+
+    while frontier:
+        it, moves, a = frontier.pop(0)
+        iterations += 1
+
+        if len(moves) > oldlen:
+            oldlen = len(moves)
+            print oldlen
+        h50 = [x for x in a if x > 50 and a.count(x) > 1]
+        if h50:
+            break
+        for i in range(1, len(a)-1):
+            aa = a[:]
+            aa[i] = a[i-1]+a[i+1]
+            moves2 = moves[:]
+            frontier.append((it+1, moves2 + [i], aa))
+
+    print it, iterations, moves, a
diff --git a/ar/assignments/a11.smt b/ar/assignments/a11.smt
new file mode 100644 (file)
index 0000000..a208034
--- /dev/null
@@ -0,0 +1,15 @@
+(benchmark a11.smt
+:logic QF_UFLIA
+:extrafuns (
+       (Nuzzles Int)
+       (Prittles Int)
+       (Skipples Int)
+       (Crottles Int)
+       (Duples Int))
+:formula (and
+(= Nuzzles 700)
+(= Prittles 800)
+(= Skipples 1000)
+(= Crottles 1500)
+(= Duples 100)
+))