# 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) ################################################################################