lub2022-practical/farm_animals/final.py

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

# No need to parse anything for this example

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

# todo
# Create Z3 variables which hold the number of animals and the price respectively
amount_of_animals = Int("amount_of_animals")
total_price = Int("total_price")
target_price = 10000
target_amount = 100

# todo
# Create Z3 variables which hold the amount of the different animals our farmes is going to buy
cows = Int("cows")
mice = Int("mice")
chicken = Int("chicken")

# todo
# Add constraints which model our real life requirements
solver.add(cows + chicken + mice == amount_of_animals)
solver.add(cows * 1000 + chicken * 300 + mice * 25 == total_price)
solver.add(total_price == target_price)
solver.add(amount_of_animals == target_amount)
# Done?

solver.add(cows > 1)
solver.add(chicken > 1)
solver.add(mice > 1)

print(solver.sexpr())

# 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
result =  str(m[cows]) + " cows and "
result += str(m[chicken]) + " chicken and "
result += str(m[mice]) + " mice -> "
print(result)
print(m[cows].as_long() * 10 + m[chicken].as_long() * 3 + m[mice].as_long() * 0.25)
solver.add(mice != m[mice])
res = solver.check()
if res != sat:
    print("unsat")
    sys.exit(1)

################################################################################