1 files changed, 18 insertions, 0 deletions
diff --git a/math/py-z3-solver/files/example-dog-cat-mouse.py b/math/py-z3-solver/files/example-dog-cat-mouse.py
new file mode 100644
index 000000000000..861b8180f5f4
--- /dev/null
+++ b/math/py-z3-solver/files/example-dog-cat-mouse.py
@@ -0,0 +1,18 @@
+# example from https://ericpony.github.io/z3py-tutorial/guide-examples.htm
+
+from z3 import Ints, solve
+
+
+# Create 3 integer variables
+dog, cat, mouse = Ints('dog cat mouse')
+solve(dog >= 1,   # at least one dog
+      cat >= 1,   # at least one cat
+      mouse >= 1, # at least one mouse
+      # we want to buy 100 animals
+      dog + cat + mouse == 100,
+      # We have 100 dollars (10000 cents):
+      #   dogs cost 15 dollars (1500 cents), 
+      #   cats cost 1 dollar (100 cents), and 
+      #   mice cost 25 cents 
+      1500 * dog + 100 * cat + 25 * mouse == 10000)
+