From a7e3a9df5a35a88e6ee11ee5ee2b85ee436a0f0e Mon Sep 17 00:00:00 2001
From: Mathieu Roger <rogma.boami@free.fr>
Date: Wed, 14 Sep 2016 19:10:49 +0200
Subject: [PATCH] Create socrates.py

Classical syllogism in Z3.
Many samples talks about integer, reals. Not much sample available on non integer things.
---
 examples/python/socrates.py | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 examples/python/socrates.py

diff --git a/examples/python/socrates.py b/examples/python/socrates.py
new file mode 100644
index 000000000..79a1b57f1
--- /dev/null
+++ b/examples/python/socrates.py
@@ -0,0 +1,33 @@
+############################################
+# Copyright (c) Microsoft Corporation. All Rights Reserved.
+# 
+# all humans are mortal
+# Socrates is a human
+# so Socrates mortal 
+############################################
+
+from z3 import *
+
+set_param(proof=True)
+
+Object = DeclareSort('Object')
+
+Human = Function('Human', Object, BoolSort())
+Mortal = Function('Mortal', Object, BoolSort())
+
+# a well known philosopher 
+socrates = Const('socrates', Object)
+
+# free variables used in forall must be declared Const in python
+x = Const('x', Object)
+
+axioms = [ForAll([x], Implies(Human(x), Mortal(x))), 
+          Human(socrates) == True]
+
+
+s = Solver()
+s.add(axioms)
+# classical refutation
+s.add(Mortal(socrates) == False)
+
+print(s.check()) # prints unsat so socrates is Mortal