From d008b4fbbdd041c8a778369b251c7e631eca14ff Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Sun, 20 Feb 2022 17:58:24 +0100 Subject: [PATCH] added burglars ex1 --- ex1/burglars.py | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 ex1/burglars.py diff --git a/ex1/burglars.py b/ex1/burglars.py new file mode 100644 index 0000000..b49043b --- /dev/null +++ b/ex1/burglars.py @@ -0,0 +1,32 @@ +# coding: utf-8 +from z3 import * + +################################# Burglars ################################## +# create the solver +solver = Solver() + +############################################################################# +# (1) Ed: "Fred did it, and Ted is innocent". +# (2) Fred: "If Ed is guilty , then so is Ted". +# (3) Ted: "Im innocent, but at least one of the others is guilty". +############################################################################# + +# TODO +# Create boolean variables for each of the culprits + +# TODO +# Add constraints to the solver representing the statements from above + + + +res = solver.check() +if res != sat: + print("unsat") + sys.exit(1) + +print(solver) +m = solver.model() +for d in m.decls(): + print("%s -> %s" % (d, m[d])) + +print("\n" + str(m))