From 72a250c01ac3f2623b266b9f85e52a84a4f0ea33 Mon Sep 17 00:00:00 2001 From: "ThanhVu (Vu) Nguyen" Date: Thu, 6 Dec 2012 13:54:57 -0500 Subject: [PATCH] =?UTF-8?q?moving=20my=20common=20z3=20stuff=20to=20z3util?= =?UTF-8?q?.py=20=20=20=E2=80=A6=20=20note=20the=20vset()=20call=20essenti?= =?UTF-8?q?ally=20returns=20a=20list=20with=20no=20duplicate=20elements,?= =?UTF-8?q?=20=20it's=20like=20set=20but=20allows=20the=20user=20to=20add?= =?UTF-8?q?=20in=20a=20function=20to=20compute=20the=20representation=20of?= =?UTF-8?q?=20the=20list=20elements.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/api/python/z3util.py | 410 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 410 insertions(+) diff --git a/src/api/python/z3util.py b/src/api/python/z3util.py index 6d309d9e9..6cdd4de32 100644 --- a/src/api/python/z3util.py +++ b/src/api/python/z3util.py @@ -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 +