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

remove special characters

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-09-14 10:32:17 -07:00
parent 01eafdf68e
commit e7f36a2d35
1 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
examples/python/socrates.py
View file

@ -1,9 +1,9 @@
############################################ ############################################
# Copyright (c) Microsoft Corporation. All Rights Reserved. # Copyright (c) Microsoft Corporation. All Rights Reserved.
#  #
# all humans are mortal # all humans are mortal
# Socrates is a human # Socrates is a human
# so Socrates mortal # so Socrates mortal
############################################ ############################################
from z3 import * from z3 import *
@ -15,10 +15,10 @@ Object = DeclareSort('Object')
Human = Function('Human', Object, BoolSort()) Human = Function('Human', Object, BoolSort())
Mortal = Function('Mortal', Object, BoolSort()) Mortal = Function('Mortal', Object, BoolSort())
# a well known philosopher # a well known philosopher
socrates = Const('socrates', Object) socrates = Const('socrates', Object)
# free variables used in forall must be declared Const in python # free variables used in forall must be declared Const in python
x = Const('x', Object) x = Const('x', Object)
axioms = [ForAll([x], Implies(Human(x), Mortal(x))), axioms = [ForAll([x], Implies(Human(x), Mortal(x))),
@ -27,7 +27,9 @@ axioms = [ForAll([x], Implies(Human(x), Mortal(x))),
s = Solver() s = Solver()
s.add(axioms) s.add(axioms)
# classical refutation # classical refutation
s.add(Mortal(socrates) == False) s.add(Mortal(socrates) == False)
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.