math/py-z3-solver: update 4.8.17 → 4.13.2

This fixes the problem from bug#280689.

PR:		280689

1 files changed, 22 insertions, 0 deletions

diff --git a/math/py-z3-solver/files/example-eight-queens.py b/math/py-z3-solver/files/example-eight-queens.py
new file mode 100644
index 000000000000..06eb2955fd02
--- /dev/null
+++ b/math/py-z3-solver/files/example-eight-queens.py
@@ -0,0 +1,22 @@
+# example from https://ericpony.github.io/z3py-tutorial/guide-examples.htm
+
+from z3 import Int, And, Distinct, If, solve, print_matrix
+
+
+# We know each queen must be in a different row.
+# So, we represent each queen by a single integer: the column position
+Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]
+
+# Each queen is in a column {1, ... 8 }
+val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]
+
+# At most one queen per column
+col_c = [ Distinct(Q) ]
+
+# Diagonal constraint
+diag_c = [ If(i == j,
+              True,
+              And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
+           for i in range(8) for j in range(i) ]
+
+solve(val_c + col_c + diag_c)