From ec5d4f111970ca74bacba12243f681e4a52660d5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 23 Oct 2016 20:35:20 -0700
Subject: [PATCH] add example to exercise at-most-1 constraints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/python/all_interval_series.py | 69 ++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)
 create mode 100644 examples/python/all_interval_series.py

diff --git a/examples/python/all_interval_series.py b/examples/python/all_interval_series.py
new file mode 100644
index 000000000..485363f02
--- /dev/null
+++ b/examples/python/all_interval_series.py
@@ -0,0 +1,69 @@
+from z3 import *
+import time
+
+def diff_at_j_is_i(xs, j, i):
+    assert(0 <= j and j + 1 < len(xs))
+    assert(1 <= i and i < len(xs))
+    return Or([ And(xs[j][k], xs[j+1][k-i]) for k in range(i,len(xs))] + 
+              [ And(xs[j][k], xs[j+1][k+i]) for k in range(0,len(xs)-i)])
+    
+
+def ais(n):
+    xij = [ [ Bool("x_%d_%d" % (i,j)) for j in range(n)] for i in range(n) ]
+    s = SolverFor("QF_FD")
+# Optionally replace by (slower) default solver if using
+# more then just finite domains (Booleans, Bit-vectors, enumeration types
+# and bounded integers)
+#   s = Solver() 
+    for i in range(n):
+        s.add(AtMost(xij[i] + [1]))
+        s.add(Or(xij[i]))
+    for j in range(n):
+        xi = [ xij[i][j] for i in range(n) ]
+        s.add(AtMost(xi + [1]))
+        s.add(Or(xi))
+    dji = [ [ diff_at_j_is_i(xij, j, i + 1) for i in range(n-1)] for j in range(n-1) ]
+    for j in range(n-1):
+        s.add(AtMost(dji[j] + [1]))
+        s.add(Or(dji[j]))
+    for i in range(n-1):
+        dj = [dji[j][i] for j in range(n-1)]
+        s.add(AtMost(dj + [1]))
+        s.add(Or(dj))
+    return s, xij
+
+def process_model(s, xij, n):
+    # x_ij integer i is at position j
+    # d_ij difference between integer at position j, j+1 is i
+    # sum_j d_ij = 1 i = 1,...,n-1
+    # sum_j x_ij = 1
+    # sum_i x_ij = 1
+    m = s.model()
+    block = []
+    values = []
+    for i in range(n):
+        k = -1
+        for j in range(n):
+            if is_true(m.eval(xij[i][j])):
+               assert(k == -1)
+               block += [xij[i][j]]
+               k = j
+        values += [k]
+    print values
+    sys.stdout.flush()
+    return block
+
+def all_models(n):
+    count = 0
+    s, xij = ais(n)
+    start = time.clock()
+    while sat == s.check():
+        block = process_model(s, xij, n)
+        s.add(Not(And(block)))
+        count += 1
+    print s.statistics()
+    print time.clock() - start
+    print count
+
+set_option(verbose=1)  
+all_models(12)