blob: 861b8180f5f4cf62536311f108461bc1df3953fd (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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)
|
