lub2022-practical/farm_animals/bare.py

# coding: utf-8
import os, sys
from z3 import *

# No need to parse anything for this example

#################################### Farm Animals ####################################
solver = Solver()

# We have 100€ ( == 10000c) and we want to buy **exactly** 100 animals, where
# price(cow) = 10€
# price(chicken) = 3€
# price(mouse) = 25c

# todo
# Create Z3 variables which hold the number of animals and the price respectively

# todo
# Create Z3 variables which hold the amount of the different animals our farmes is going to buy

# todo
# Add constraints which model our real life requirements

# Check for satisfiability
res = solver.check()
if res != sat:
    print("unsat")
    sys.exit(1)

################################################################################
# print the model
#  get the model
m = solver.model()
#  print all Z3 variables which have an assignment in the model
for d in m.decls():
    print("%s = %s" % (d.name(), m[d]))
################################################################################