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