mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 13:58:45 +00:00
Merge branch 'contrib' of https://git01.codeplex.com/forks/nguyenthanhvuh/vuz3 into vu
This commit is contained in:
Leonardo de Moura
commit
bca0c0bb5f
|
|
@ -1,5 +1,46 @@
|
|||
"""
|
||||
Usage:
|
||||
import common_z3 as CM_Z3
|
||||
"""
|
||||
|
||||
import common as CM
|
||||
from z3 import *
|
||||
|
||||
def get_z3_version(as_str=False):
|
||||
major = ctypes.c_uint(0)
|
||||
minor = ctypes.c_uint(0)
|
||||
build = ctypes.c_uint(0)
|
||||
rev = ctypes.c_uint(0)
|
||||
Z3_get_version(major,minor,build,rev)
|
||||
rs = map(int,(major.value,minor.value,build.value,rev.value))
|
||||
if as_str:
|
||||
return "{}.{}.{}.{}".format(*rs)
|
||||
else:
|
||||
return rs
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
def ehash(v):
|
||||
"""
|
||||
Returns a 'stronger' hash value than the default hash() method.
|
||||
The result from hash() is not enough to distinguish between 2
|
||||
z3 expressions in some cases.
|
||||
|
||||
>>> x1 = Bool('x'); x2 = Bool('x'); x3 = Int('x')
|
||||
>>> print x1.hash(),x2.hash(),x3.hash() #BAD: all same hash values
|
||||
783810685 783810685 783810685
|
||||
>>> print ehash(x1), ehash(x2), ehash(x3)
|
||||
x_783810685_1 x_783810685_1 x_783810685_2
|
||||
|
||||
"""
|
||||
if __debug__:
|
||||
assert is_expr(v)
|
||||
|
||||
return "{}_{}_{}".format(str(v),v.hash(),v.sort_kind())
|
||||
|
||||
|
||||
"""
|
||||
In Z3, variables are caleld *uninterpreted* consts and
|
||||
variables are *interpreted* consts.
|
||||
|
|
@ -56,3 +97,372 @@ def is_expr_val(v):
|
|||
"""
|
||||
return is_const(v) and v.decl().kind()!=Z3_OP_UNINTERPRETED
|
||||
|
||||
|
||||
|
||||
|
||||
def get_vars(f,rs=[]):
|
||||
"""
|
||||
>>> x,y = Ints('x y')
|
||||
>>> a,b = Bools('a b')
|
||||
>>> get_vars(Implies(And(x+y==0,x*2==10),Or(a,Implies(a,b==False))))
|
||||
[x, y, a, b]
|
||||
|
||||
"""
|
||||
if __debug__:
|
||||
assert is_expr(f)
|
||||
|
||||
if is_const(f):
|
||||
if is_expr_val(f):
|
||||
return rs
|
||||
else: #variable
|
||||
return CM.vset(rs + [f],str)
|
||||
|
||||
else:
|
||||
for f_ in f.children():
|
||||
rs = get_vars(f_,rs)
|
||||
|
||||
return CM.vset(rs,str)
|
||||
|
||||
|
||||
|
||||
def mk_var(name,vsort):
|
||||
if vsort.kind() == Z3_INT_SORT:
|
||||
v = Int(name)
|
||||
elif vsort.kind() == Z3_REAL_SORT:
|
||||
v = Real(name)
|
||||
elif vsort.kind() == Z3_BOOL_SORT:
|
||||
v = Bool(name)
|
||||
elif vsort.kind() == Z3_DATATYPE_SORT:
|
||||
v = Const(name,vsort)
|
||||
|
||||
else:
|
||||
assert False, 'Cannot handle this sort (s: %sid: %d)'\
|
||||
%(vsort,vsort.kind())
|
||||
|
||||
return v
|
||||
|
||||
|
||||
|
||||
def prove(claim,assume=None,verbose=0):
|
||||
"""
|
||||
>>> r,m = prove(BoolVal(True),verbose=0); r,model_str(m,as_str=False)
|
||||
(True, None)
|
||||
|
||||
#infinite counter example when proving contradiction
|
||||
>>> r,m = prove(BoolVal(False)); r,model_str(m,as_str=False)
|
||||
(False, [])
|
||||
|
||||
>>> x,y,z=Bools('x y z')
|
||||
>>> r,m = prove(And(x,Not(x))); r,model_str(m,as_str=True)
|
||||
(False, '[]')
|
||||
|
||||
>>> r,m = prove(True,assume=And(x,Not(x)),verbose=0)
|
||||
Traceback (most recent call last):
|
||||
...
|
||||
AssertionError: Assumption is alway False!
|
||||
|
||||
>>> r,m = prove(Implies(x,x),assume=y,verbose=2); r,model_str(m,as_str=False)
|
||||
assume:
|
||||
y
|
||||
claim:
|
||||
Implies(x, x)
|
||||
to_prove:
|
||||
Implies(y, Implies(x, x))
|
||||
(True, None)
|
||||
|
||||
>>> r,m = prove(And(x,True),assume=y,verbose=0); r,model_str(m,as_str=False)
|
||||
(False, [(x, False), (y, True)])
|
||||
|
||||
>>> r,m = prove(And(x,y),assume=y,verbose=0)
|
||||
>>> print r
|
||||
False
|
||||
>>> print model_str(m,as_str=True)
|
||||
x = False
|
||||
y = True
|
||||
|
||||
>>> a,b = Ints('a b')
|
||||
>>> r,m = prove(a**b == b**a,assume=None,verbose=0)
|
||||
E: cannot solve !
|
||||
>>> r is None and m is None
|
||||
True
|
||||
|
||||
"""
|
||||
|
||||
if __debug__:
|
||||
assert not assume or is_expr(assume)
|
||||
|
||||
|
||||
to_prove = claim
|
||||
if assume:
|
||||
if __debug__:
|
||||
is_proved,_ = prove(Not(assume))
|
||||
|
||||
def _f():
|
||||
emsg = "Assumption is alway False!"
|
||||
if verbose >= 2:
|
||||
emsg = "{}\n{}".format(assume,emsg)
|
||||
return emsg
|
||||
|
||||
assert is_proved==False, _f()
|
||||
|
||||
to_prove = Implies(assume,to_prove)
|
||||
|
||||
|
||||
|
||||
if verbose >= 2:
|
||||
print 'assume: '
|
||||
print assume
|
||||
print 'claim: '
|
||||
print claim
|
||||
print 'to_prove: '
|
||||
print to_prove
|
||||
|
||||
f = Not(to_prove)
|
||||
|
||||
models = get_models(f,k=1)
|
||||
if models is None: #unknown
|
||||
print 'E: cannot solve !'
|
||||
return None, None
|
||||
elif models == False: #unsat
|
||||
return True,None
|
||||
else: #sat
|
||||
if __debug__:
|
||||
assert isinstance(models,list)
|
||||
|
||||
if models:
|
||||
return False, models[0] #the first counterexample
|
||||
else:
|
||||
return False, [] #infinite counterexample,models
|
||||
|
||||
|
||||
def get_models(f,k):
|
||||
"""
|
||||
Returns the first k models satisfiying f.
|
||||
If f is not satisfiable, returns False.
|
||||
If f cannot be solved, returns None
|
||||
If f is satisfiable, returns the first k models
|
||||
Note that if f is a tautology, e.g.\ True, then the result is []
|
||||
|
||||
Based on http://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation
|
||||
|
||||
EXAMPLES:
|
||||
>>> x, y = Ints('x y')
|
||||
>>> len(get_models(And(0<=x,x <= 4),k=11))
|
||||
5
|
||||
>>> get_models(And(0<=x**y,x <= 1),k=2) is None
|
||||
True
|
||||
>>> get_models(And(0<=x,x <= -1),k=2)
|
||||
False
|
||||
>>> len(get_models(x+y==7,5))
|
||||
5
|
||||
>>> len(get_models(And(x<=5,x>=1),7))
|
||||
5
|
||||
>>> get_models(And(x<=0,x>=5),7)
|
||||
False
|
||||
|
||||
>>> x = Bool('x')
|
||||
>>> get_models(And(x,Not(x)),k=1)
|
||||
False
|
||||
>>> get_models(Implies(x,x),k=1)
|
||||
[]
|
||||
>>> get_models(BoolVal(True),k=1)
|
||||
[]
|
||||
|
||||
|
||||
|
||||
"""
|
||||
|
||||
if __debug__:
|
||||
assert is_expr(f)
|
||||
assert k>=1
|
||||
|
||||
|
||||
|
||||
s = Solver()
|
||||
s.add(f)
|
||||
|
||||
models = []
|
||||
i = 0
|
||||
while s.check() == sat and i < k:
|
||||
i = i + 1
|
||||
|
||||
m = s.model()
|
||||
|
||||
if not m: #if m == []
|
||||
break
|
||||
|
||||
models.append(m)
|
||||
|
||||
|
||||
#create new constraint to block the current model
|
||||
block = Not(And([v() == m[v] for v in m]))
|
||||
s.add(block)
|
||||
|
||||
|
||||
if s.check() == unknown:
|
||||
return None
|
||||
elif s.check() == unsat and i==0:
|
||||
return False
|
||||
else:
|
||||
return models
|
||||
|
||||
def is_tautology(claim,verbose=0):
|
||||
"""
|
||||
>>> is_tautology(Implies(Bool('x'),Bool('x')))
|
||||
True
|
||||
|
||||
>>> is_tautology(Implies(Bool('x'),Bool('y')))
|
||||
False
|
||||
|
||||
>>> is_tautology(BoolVal(True))
|
||||
True
|
||||
|
||||
>>> is_tautology(BoolVal(False))
|
||||
False
|
||||
|
||||
"""
|
||||
return prove(claim=claim,assume=None,verbose=verbose)[0]
|
||||
|
||||
|
||||
def is_contradiction(claim,verbose=0):
|
||||
"""
|
||||
>>> x,y=Bools('x y')
|
||||
>>> is_contradiction(BoolVal(False))
|
||||
True
|
||||
|
||||
>>> is_contradiction(BoolVal(True))
|
||||
False
|
||||
|
||||
>>> is_contradiction(x)
|
||||
False
|
||||
|
||||
>>> is_contradiction(Implies(x,y))
|
||||
False
|
||||
|
||||
>>> is_contradiction(Implies(x,x))
|
||||
False
|
||||
|
||||
>>> is_contradiction(And(x,Not(x)))
|
||||
True
|
||||
"""
|
||||
|
||||
return prove(claim=Not(claim),assume=None,verbose=verbose)[0]
|
||||
|
||||
|
||||
def exact_one_model(f):
|
||||
"""
|
||||
return True if f has exactly 1 model, False otherwise.
|
||||
|
||||
EXAMPLES:
|
||||
|
||||
>>> x, y = Ints('x y')
|
||||
>>> exact_one_model(And(0<=x**y,x <= 0))
|
||||
False
|
||||
|
||||
>>> exact_one_model(And(0<=x,x <= 0))
|
||||
True
|
||||
|
||||
>>> exact_one_model(And(0<=x,x <= 1))
|
||||
False
|
||||
|
||||
>>> exact_one_model(And(0<=x,x <= -1))
|
||||
False
|
||||
"""
|
||||
|
||||
models = get_models(f,k=2)
|
||||
if isinstance(models,list):
|
||||
return len(models)==1
|
||||
else:
|
||||
return False
|
||||
|
||||
|
||||
|
||||
def myBinOp(op,*L):
|
||||
"""
|
||||
>>> myAnd(*[Bool('x'),Bool('y')])
|
||||
And(x, y)
|
||||
|
||||
>>> myAnd(*[Bool('x'),None])
|
||||
x
|
||||
|
||||
>>> myAnd(*[Bool('x')])
|
||||
x
|
||||
|
||||
>>> myAnd(*[])
|
||||
|
||||
>>> myAnd(Bool('x'),Bool('y'))
|
||||
And(x, y)
|
||||
|
||||
>>> myAnd(*[Bool('x'),Bool('y')])
|
||||
And(x, y)
|
||||
|
||||
>>> myAnd([Bool('x'),Bool('y')])
|
||||
And(x, y)
|
||||
|
||||
>>> myAnd((Bool('x'),Bool('y')))
|
||||
And(x, y)
|
||||
|
||||
>>> myAnd(*[Bool('x'),Bool('y'),True])
|
||||
Traceback (most recent call last):
|
||||
...
|
||||
AssertionError
|
||||
"""
|
||||
|
||||
if __debug__:
|
||||
assert op == Z3_OP_OR or op == Z3_OP_AND or op == Z3_OP_IMPLIES
|
||||
|
||||
if len(L)==1 and (isinstance(L[0],list) or isinstance(L[0],tuple)):
|
||||
L = L[0]
|
||||
|
||||
if __debug__:
|
||||
assert all(not isinstance(l,bool) for l in L)
|
||||
|
||||
L = [l for l in L if is_expr(l)]
|
||||
if L:
|
||||
if len(L)==1:
|
||||
return L[0]
|
||||
else:
|
||||
if op == Z3_OP_OR:
|
||||
return Or(L)
|
||||
elif op == Z3_OP_AND:
|
||||
return And(L)
|
||||
else: #IMPLIES
|
||||
return Implies(L[0],L[1])
|
||||
else:
|
||||
return None
|
||||
|
||||
|
||||
def myAnd(*L): return myBinOp(Z3_OP_AND,*L)
|
||||
def myOr(*L): return myBinOp(Z3_OP_OR,*L)
|
||||
def myImplies(a,b):return myBinOp(Z3_OP_IMPLIES,[a,b])
|
||||
|
||||
|
||||
|
||||
Iff = lambda f,g: And(Implies(f,g),Implies(g,f))
|
||||
|
||||
|
||||
|
||||
def model_str(m,as_str=True):
|
||||
"""
|
||||
Returned a 'sorted' model (so that it's easier to see)
|
||||
The model is sorted by its key,
|
||||
e.g. if the model is y = 3 , x = 10, then the result is
|
||||
x = 10, y = 3
|
||||
|
||||
EXAMPLES:
|
||||
see doctest exampels from function prove()
|
||||
|
||||
"""
|
||||
if __debug__:
|
||||
assert m is None or m == [] or isinstance(m,ModelRef)
|
||||
|
||||
if m :
|
||||
vs = [(v,m[v]) for v in m]
|
||||
vs = sorted(vs,key=lambda (a,_): str(a))
|
||||
if as_str:
|
||||
return '\n'.join(['{} = {}'.format(k,v) for (k,v) in vs])
|
||||
else:
|
||||
return vs
|
||||
else:
|
||||
return str(m) if as_str else m
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue