3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00

Merge pull request #737 from MathieuRoger/patch-1

Update socrates.py
This commit is contained in:
Nikolaj Bjorner 2016-09-14 12:42:36 -07:00 committed by GitHub
commit 5290cd1ff5

View file

@ -8,8 +8,6 @@
from z3 import *
set_param(proof=True)
Object = DeclareSort('Object')
Human = Function('Human', Object, BoolSort())
@ -22,14 +20,15 @@ socrates = Const('socrates', Object)
x = Const('x', Object)
axioms = [ForAll([x], Implies(Human(x), Mortal(x))),
Human(socrates) == True]
Human(socrates)]
s = Solver()
s.add(axioms)
print(s.check()) # prints sat so axioms are coherents
# classical refutation
s.add(Mortal(socrates) == False)
s.add(Not(Mortal(socrates)))
print(s.check()) # prints unsat so socrates is Mortal
# print(s.proof()) # prints a low level (not readable) proof object.