mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

Update socrates.py

Browse source
This commit is contained in:
Mathieu Roger 2016-09-14 21:36:39 +02:00 committed by GitHub
parent e7f36a2d35
commit 9245e61775
1 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
examples/python/socrates.py
View file

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