added burglars ex1

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