forked from Lainports/opnsense-ports
18 lines
573 B
Python
18 lines
573 B
Python
# 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)
|
|
|