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