1############################################ 2# Copyright (c) 2012 Microsoft Corporation 3# 4# Z3 Python interface 5# 6# Authors: Leonardo de Moura (leonardo) 7# ThanhVu (Vu) Nguyen <tnguyen@cs.unm.edu> 8############################################ 9""" 10Usage: 11import common_z3 as CM_Z3 12""" 13 14from .z3 import * 15 16def vset(seq, idfun=None, as_list=True): 17 # This functions preserves the order of arguments while removing duplicates. 18 # This function is from https://code.google.com/p/common-python-vu/source/browse/vu_common.py 19 # (Thanhu's personal code). It has been copied here to avoid a dependency on vu_common.py. 20 """ 21 order preserving 22 23 >>> vset([[11,2],1, [10,['9',1]],2, 1, [11,2],[3,3],[10,99],1,[10,['9',1]]],idfun=repr) 24 [[11, 2], 1, [10, ['9', 1]], 2, [3, 3], [10, 99]] 25 """ 26 27 def _uniq_normal(seq): 28 d_ = {} 29 for s in seq: 30 if s not in d_: 31 d_[s] = None 32 yield s 33 34 def _uniq_idfun(seq,idfun): 35 d_ = {} 36 for s in seq: 37 h_ = idfun(s) 38 if h_ not in d_: 39 d_[h_] = None 40 yield s 41 42 if idfun is None: 43 res = _uniq_normal(seq) 44 else: 45 res = _uniq_idfun(seq,idfun) 46 47 return list(res) if as_list else res 48 49 50def get_z3_version(as_str=False): 51 major = ctypes.c_uint(0) 52 minor = ctypes.c_uint(0) 53 build = ctypes.c_uint(0) 54 rev = ctypes.c_uint(0) 55 Z3_get_version(major,minor,build,rev) 56 rs = map(int,(major.value,minor.value,build.value,rev.value)) 57 if as_str: 58 return "{}.{}.{}.{}".format(*rs) 59 else: 60 return rs 61 62 63def ehash(v): 64 """ 65 Returns a 'stronger' hash value than the default hash() method. 66 The result from hash() is not enough to distinguish between 2 67 z3 expressions in some cases. 68 69 Note: the following doctests will fail with Python 2.x as the 70 default formatting doesn't match that of 3.x. 71 >>> x1 = Bool('x'); x2 = Bool('x'); x3 = Int('x') 72 >>> print(x1.hash(),x2.hash(),x3.hash()) #BAD: all same hash values 73 783810685 783810685 783810685 74 >>> print(ehash(x1), ehash(x2), ehash(x3)) 75 x_783810685_1 x_783810685_1 x_783810685_2 76 77 """ 78 if z3_debug(): 79 assert is_expr(v) 80 81 return "{}_{}_{}".format(str(v),v.hash(),v.sort_kind()) 82 83 84""" 85In Z3, variables are called *uninterpreted* consts and 86variables are *interpreted* consts. 87""" 88 89def is_expr_var(v): 90 """ 91 EXAMPLES: 92 93 >>> is_expr_var(Int('7')) 94 True 95 >>> is_expr_var(IntVal('7')) 96 False 97 >>> is_expr_var(Bool('y')) 98 True 99 >>> is_expr_var(Int('x') + 7 == Int('y')) 100 False 101 >>> LOnOff, (On,Off) = EnumSort("LOnOff",['On','Off']) 102 >>> Block,Reset,SafetyInjection=Consts("Block Reset SafetyInjection",LOnOff) 103 >>> is_expr_var(LOnOff) 104 False 105 >>> is_expr_var(On) 106 False 107 >>> is_expr_var(Block) 108 True 109 >>> is_expr_var(SafetyInjection) 110 True 111 """ 112 113 return is_const(v) and v.decl().kind()==Z3_OP_UNINTERPRETED 114 115def is_expr_val(v): 116 """ 117 EXAMPLES: 118 119 >>> is_expr_val(Int('7')) 120 False 121 >>> is_expr_val(IntVal('7')) 122 True 123 >>> is_expr_val(Bool('y')) 124 False 125 >>> is_expr_val(Int('x') + 7 == Int('y')) 126 False 127 >>> LOnOff, (On,Off) = EnumSort("LOnOff",['On','Off']) 128 >>> Block,Reset,SafetyInjection=Consts("Block Reset SafetyInjection",LOnOff) 129 >>> is_expr_val(LOnOff) 130 False 131 >>> is_expr_val(On) 132 True 133 >>> is_expr_val(Block) 134 False 135 >>> is_expr_val(SafetyInjection) 136 False 137 """ 138 return is_const(v) and v.decl().kind()!=Z3_OP_UNINTERPRETED 139 140 141 142 143def get_vars(f,rs=[]): 144 """ 145 >>> x,y = Ints('x y') 146 >>> a,b = Bools('a b') 147 >>> get_vars(Implies(And(x+y==0,x*2==10),Or(a,Implies(a,b==False)))) 148 [x, y, a, b] 149 150 """ 151 if z3_debug(): 152 assert is_expr(f) 153 154 if is_const(f): 155 if is_expr_val(f): 156 return rs 157 else: #variable 158 return vset(rs + [f],str) 159 160 else: 161 for f_ in f.children(): 162 rs = get_vars(f_,rs) 163 164 return vset(rs,str) 165 166 167 168def mk_var(name,vsort): 169 if vsort.kind() == Z3_INT_SORT: 170 v = Int(name) 171 elif vsort.kind() == Z3_REAL_SORT: 172 v = Real(name) 173 elif vsort.kind() == Z3_BOOL_SORT: 174 v = Bool(name) 175 elif vsort.kind() == Z3_DATATYPE_SORT: 176 v = Const(name,vsort) 177 178 else: 179 assert False, 'Cannot handle this sort (s: %sid: %d)'\ 180 %(vsort,vsort.kind()) 181 182 return v 183 184 185 186def prove(claim,assume=None,verbose=0): 187 """ 188 >>> r,m = prove(BoolVal(True),verbose=0); r,model_str(m,as_str=False) 189 (True, None) 190 191 #infinite counter example when proving contradiction 192 >>> r,m = prove(BoolVal(False)); r,model_str(m,as_str=False) 193 (False, []) 194 195 >>> x,y,z=Bools('x y z') 196 >>> r,m = prove(And(x,Not(x))); r,model_str(m,as_str=True) 197 (False, '[]') 198 199 >>> r,m = prove(True,assume=And(x,Not(x)),verbose=0) 200 Traceback (most recent call last): 201 ... 202 AssertionError: Assumption is always False! 203 204 >>> r,m = prove(Implies(x,x),assume=y,verbose=2); r,model_str(m,as_str=False) 205 assume: 206 y 207 claim: 208 Implies(x, x) 209 to_prove: 210 Implies(y, Implies(x, x)) 211 (True, None) 212 213 >>> r,m = prove(And(x,True),assume=y,verbose=0); r,model_str(m,as_str=False) 214 (False, [(x, False), (y, True)]) 215 216 >>> r,m = prove(And(x,y),assume=y,verbose=0) 217 >>> print(r) 218 False 219 >>> print(model_str(m,as_str=True)) 220 x = False 221 y = True 222 223 >>> a,b = Ints('a b') 224 >>> r,m = prove(a**b == b**a,assume=None,verbose=0) 225 E: cannot solve ! 226 >>> r is None and m is None 227 True 228 229 """ 230 231 if z3_debug(): 232 assert not assume or is_expr(assume) 233 234 235 to_prove = claim 236 if assume: 237 if z3_debug(): 238 is_proved,_ = prove(Not(assume)) 239 240 def _f(): 241 emsg = "Assumption is always False!" 242 if verbose >= 2: 243 emsg = "{}\n{}".format(assume,emsg) 244 return emsg 245 246 assert is_proved==False, _f() 247 248 to_prove = Implies(assume,to_prove) 249 250 251 252 if verbose >= 2: 253 print('assume: ') 254 print(assume) 255 print('claim: ') 256 print(claim) 257 print('to_prove: ') 258 print(to_prove) 259 260 f = Not(to_prove) 261 262 models = get_models(f,k=1) 263 if models is None: #unknown 264 print('E: cannot solve !') 265 return None, None 266 elif models == False: #unsat 267 return True,None 268 else: #sat 269 if z3_debug(): 270 assert isinstance(models,list) 271 272 if models: 273 return False, models[0] #the first counterexample 274 else: 275 return False, [] #infinite counterexample,models 276 277 278def get_models(f,k): 279 """ 280 Returns the first k models satisfiying f. 281 If f is not satisfiable, returns False. 282 If f cannot be solved, returns None 283 If f is satisfiable, returns the first k models 284 Note that if f is a tautology, e.g.\ True, then the result is [] 285 286 Based on http://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation 287 288 EXAMPLES: 289 >>> x, y = Ints('x y') 290 >>> len(get_models(And(0<=x,x <= 4),k=11)) 291 5 292 >>> get_models(And(0<=x**y,x <= 1),k=2) is None 293 True 294 >>> get_models(And(0<=x,x <= -1),k=2) 295 False 296 >>> len(get_models(x+y==7,5)) 297 5 298 >>> len(get_models(And(x<=5,x>=1),7)) 299 5 300 >>> get_models(And(x<=0,x>=5),7) 301 False 302 303 >>> x = Bool('x') 304 >>> get_models(And(x,Not(x)),k=1) 305 False 306 >>> get_models(Implies(x,x),k=1) 307 [] 308 >>> get_models(BoolVal(True),k=1) 309 [] 310 311 312 313 """ 314 315 if z3_debug(): 316 assert is_expr(f) 317 assert k>=1 318 319 320 321 s = Solver() 322 s.add(f) 323 324 models = [] 325 i = 0 326 while s.check() == sat and i < k: 327 i = i + 1 328 329 m = s.model() 330 331 if not m: #if m == [] 332 break 333 334 models.append(m) 335 336 337 #create new constraint to block the current model 338 block = Not(And([v() == m[v] for v in m])) 339 s.add(block) 340 341 342 if s.check() == unknown: 343 return None 344 elif s.check() == unsat and i==0: 345 return False 346 else: 347 return models 348 349def is_tautology(claim,verbose=0): 350 """ 351 >>> is_tautology(Implies(Bool('x'),Bool('x'))) 352 True 353 354 >>> is_tautology(Implies(Bool('x'),Bool('y'))) 355 False 356 357 >>> is_tautology(BoolVal(True)) 358 True 359 360 >>> is_tautology(BoolVal(False)) 361 False 362 363 """ 364 return prove(claim=claim,assume=None,verbose=verbose)[0] 365 366 367def is_contradiction(claim,verbose=0): 368 """ 369 >>> x,y=Bools('x y') 370 >>> is_contradiction(BoolVal(False)) 371 True 372 373 >>> is_contradiction(BoolVal(True)) 374 False 375 376 >>> is_contradiction(x) 377 False 378 379 >>> is_contradiction(Implies(x,y)) 380 False 381 382 >>> is_contradiction(Implies(x,x)) 383 False 384 385 >>> is_contradiction(And(x,Not(x))) 386 True 387 """ 388 389 return prove(claim=Not(claim),assume=None,verbose=verbose)[0] 390 391 392def exact_one_model(f): 393 """ 394 return True if f has exactly 1 model, False otherwise. 395 396 EXAMPLES: 397 398 >>> x, y = Ints('x y') 399 >>> exact_one_model(And(0<=x**y,x <= 0)) 400 False 401 402 >>> exact_one_model(And(0<=x,x <= 0)) 403 True 404 405 >>> exact_one_model(And(0<=x,x <= 1)) 406 False 407 408 >>> exact_one_model(And(0<=x,x <= -1)) 409 False 410 """ 411 412 models = get_models(f,k=2) 413 if isinstance(models,list): 414 return len(models)==1 415 else: 416 return False 417 418 419 420def myBinOp(op,*L): 421 """ 422 >>> myAnd(*[Bool('x'),Bool('y')]) 423 And(x, y) 424 425 >>> myAnd(*[Bool('x'),None]) 426 x 427 428 >>> myAnd(*[Bool('x')]) 429 x 430 431 >>> myAnd(*[]) 432 433 >>> myAnd(Bool('x'),Bool('y')) 434 And(x, y) 435 436 >>> myAnd(*[Bool('x'),Bool('y')]) 437 And(x, y) 438 439 >>> myAnd([Bool('x'),Bool('y')]) 440 And(x, y) 441 442 >>> myAnd((Bool('x'),Bool('y'))) 443 And(x, y) 444 445 >>> myAnd(*[Bool('x'),Bool('y'),True]) 446 Traceback (most recent call last): 447 ... 448 AssertionError 449 """ 450 451 if z3_debug(): 452 assert op == Z3_OP_OR or op == Z3_OP_AND or op == Z3_OP_IMPLIES 453 454 if len(L)==1 and (isinstance(L[0],list) or isinstance(L[0],tuple)): 455 L = L[0] 456 457 if z3_debug(): 458 assert all(not isinstance(l,bool) for l in L) 459 460 L = [l for l in L if is_expr(l)] 461 if L: 462 if len(L)==1: 463 return L[0] 464 else: 465 if op == Z3_OP_OR: 466 return Or(L) 467 elif op == Z3_OP_AND: 468 return And(L) 469 else: #IMPLIES 470 return Implies(L[0],L[1]) 471 else: 472 return None 473 474 475def myAnd(*L): return myBinOp(Z3_OP_AND,*L) 476def myOr(*L): return myBinOp(Z3_OP_OR,*L) 477def myImplies(a,b):return myBinOp(Z3_OP_IMPLIES,[a,b]) 478 479 480 481Iff = lambda f: And(Implies(f[0],f[1]),Implies(f[1],f[0])) 482 483 484 485def model_str(m,as_str=True): 486 """ 487 Returned a 'sorted' model (so that it's easier to see) 488 The model is sorted by its key, 489 e.g. if the model is y = 3 , x = 10, then the result is 490 x = 10, y = 3 491 492 EXAMPLES: 493 see doctest exampels from function prove() 494 495 """ 496 if z3_debug(): 497 assert m is None or m == [] or isinstance(m,ModelRef) 498 499 if m : 500 vs = [(v,m[v]) for v in m] 501 vs = sorted(vs,key=lambda a,_: str(a)) 502 if as_str: 503 return '\n'.join(['{} = {}'.format(k,v) for (k,v) in vs]) 504 else: 505 return vs 506 else: 507 return str(m) if as_str else m 508 509