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