Z3
z3py.py
Go to the documentation of this file.
1 ############################################
2 # Copyright (c) 2012 Microsoft Corporation
3 #
4 # Z3 Python interface
5 #
6 # Author: Leonardo de Moura (leonardo)
7 ############################################
8
9 """Z3 is a high performance theorem prover developed at Microsoft Research. Z3 is used in many applications such as: software/hardware verification and testing, constraint solving, analysis of hybrid systems, security, biology (in silico analysis), and geometrical problems.
10
11 Several online tutorials for Z3Py are available at:
12 http://rise4fun.com/Z3Py/tutorial/guide
13
15
16 Small example:
17
18 >>> x = Int('x')
19 >>> y = Int('y')
20 >>> s = Solver()
23 >>> s.add(y == x + 1)
24 >>> s.check()
25 sat
26 >>> s.model()
27 [y = 2, x = 1]
28
29 Z3 exceptions:
30
31 >>> try:
32 ... x = Int('x')
33 ... y = Bool('y')
34 ... # the expression x + y is type incorrect
35 ... n = x + y
36 ... except Z3Exception as ex:
37 ... print "failed:", ex
38 failed: 'sort mismatch'
39 """
40 from z3core import *
41 from z3types import *
42 from z3consts import *
43 from z3printer import *
44 import io
45
46 def enable_trace(msg):
47  Z3_enable_trace(msg)
48
49 def disable_trace(msg):
50  Z3_disable_trace(msg)
51
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  return "%s.%s.%s" % (major.value, minor.value, build.value)
59
61  major = ctypes.c_uint(0)
62  minor = ctypes.c_uint(0)
63  build = ctypes.c_uint(0)
64  rev = ctypes.c_uint(0)
65  Z3_get_version(major, minor, build, rev)
66  return (major.value, minor.value, build.value, rev.value)
67
68 # We use _z3_assert instead of the assert command because we want to
69 # produce nice error messages in Z3Py at rise4fun.com
70 def _z3_assert(cond, msg):
71  if not cond:
72  raise Z3Exception(msg)
73
74 def open_log(fname):
75  """Log interaction to a file. This function must be invoked immediately after init(). """
76  Z3_open_log(fname)
77
78 def append_log(s):
79  """Append user-defined string to interaction log. """
80  Z3_append_log(s)
81
82 def to_symbol(s, ctx=None):
83  """Convert an integer or string into a Z3 symbol."""
84  if isinstance(s, int):
85  return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
86  else:
87  return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
88
89 def _symbol2py(ctx, s):
90  """Convert a Z3 symbol back into a Python object. """
91  if Z3_get_symbol_kind(ctx.ref(), s) == Z3_INT_SYMBOL:
92  return "k!%s" % Z3_get_symbol_int(ctx.ref(), s)
93  else:
94  return Z3_get_symbol_string(ctx.ref(), s)
95
96 _error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
97
98 # Hack for having nary functions that can receive one argument that is the
99 # list of arguments.
100 def _get_args(args):
101  try:
102  if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
103  return args[0]
104  else:
105  return args
106  except: # len is not necessarily defined when args is not a sequence (use reflection?)
107  return args
108
109 def _Z3python_error_handler_core(c, e):
110  # Do nothing error handler, just avoid exit(0)
111  # The wrappers in z3core.py will raise a Z3Exception if an error is detected
112  return
113
114 _Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)
115
116 def _to_param_value(val):
117  if isinstance(val, bool):
118  if val == True:
119  return "true"
120  else:
121  return "false"
122  else:
123  return str(val)
124
125 class Context:
126  """A Context manages all other Z3 objects, global configuration options, etc.
127
128  Z3Py uses a default global context. For most applications this is sufficient.
129  An application may use multiple Z3 contexts. Objects created in one context
130  cannot be used in another one. However, several objects may be "translated" from
131  one context to another. It is not safe to access Z3 objects from multiple threads.
132  The only exception is the method `interrupt()` that can be used to interrupt() a long
133  computation.
134  The initialization method receives global configuration options for the new context.
135  """
136  def __init__(self, *args, **kws):
137  if __debug__:
138  _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
139  conf = Z3_mk_config()
140  for key, value in kws.iteritems():
141  Z3_set_param_value(conf, str(key).upper(), _to_param_value(value))
142  prev = None
143  for a in args:
144  if prev == None:
145  prev = a
146  else:
147  Z3_set_param_value(conf, str(prev), _to_param_value(a))
148  prev = None
149  self.lib = lib()
150  self.ctx = Z3_mk_context_rc(conf)
151  Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
152  lib().Z3_set_error_handler.restype = None
153  lib().Z3_set_error_handler.argtypes = [ContextObj, _error_handler_fptr]
154  lib().Z3_set_error_handler(self.ctx, _Z3Python_error_handler)
155  Z3_del_config(conf)
156
157  def __del__(self):
158  self.lib.Z3_del_context(self.ctx)
159
160  def ref(self):
161  """Return a reference to the actual C pointer to the Z3 context."""
162  return self.ctx
163
164  def interrupt(self):
165  """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
166
167  This method can be invoked from a thread different from the one executing the
168  interruptable procedure.
169  """
170  Z3_interrupt(self.ref())
171
172  def set(self, *args, **kws):
173  """Set global configuration options.
174
175  Z3 command line options can be set using this method.
176  The option names can be specified in different ways:
177
178  >>> ctx = Context()
179  >>> ctx.set('WELL_SORTED_CHECK', True)
180  >>> ctx.set(':well-sorted-check', True)
181  >>> ctx.set(well_sorted_check=True)
182  """
183  if __debug__:
184  _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
185  for key, value in kws.iteritems():
186  Z3_update_param_value(self.ctx, str(key).upper(), _to_param_value(value))
187  prev = None
188  for a in args:
189  if prev == None:
190  prev = a
191  else:
192  Z3_update_param_value(self.ctx, str(prev), _to_param_value(a))
193  prev = None
194
195 # Global Z3 context
196 _main_ctx = None
197 def main_ctx():
198  """Return a reference to the global Z3 context.
199
200  >>> x = Real('x')
201  >>> x.ctx == main_ctx()
202  True
203  >>> c = Context()
204  >>> c == main_ctx()
205  False
206  >>> x2 = Real('x', c)
207  >>> x2.ctx == c
208  True
209  >>> eq(x, x2)
210  False
211  """
212  global _main_ctx
213  if _main_ctx == None:
214  _main_ctx = Context()
215  return _main_ctx
216
217 def _get_ctx(ctx):
218  if ctx == None:
219  return main_ctx()
220  else:
221  return ctx
222
223 def set_option(*args, **kws):
224  """Update parameters of the global context `main_ctx()`, and global configuration options of Z3Py. See `Context.set()`.
225
226  >>> set_option(precision=10)
227  """
228  new_kws = {}
229  for k, v in kws.iteritems():
230  if not set_pp_option(k, v):
231  new_kws[k] = v
232  main_ctx().set(*args, **new_kws)
233
234 #########################################
235 #
236 # ASTs base class
237 #
238 #########################################
239
240 # Mark objects that use pretty printer
242  """Superclass for all Z3 objects that have support for pretty printing."""
243  def use_pp(self):
244  return True
245
247  """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions."""
248  def __init__(self, ast, ctx=None):
249  self.ast = ast
250  self.ctx = _get_ctx(ctx)
251  Z3_inc_ref(self.ctx.ref(), self.as_ast())
252
253  def __del__(self):
254  Z3_dec_ref(self.ctx.ref(), self.as_ast())
255
256  def __str__(self):
257  return obj_to_string(self)
258
259  def __repr__(self):
260  return obj_to_string(self)
261
262  def sexpr(self):
263  """Return an string representing the AST node in s-expression notation.
264
265  >>> x = Int('x')
266  >>> ((x + 1)*x).sexpr()
267  '(* (+ x 1) x)'
268  """
269  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
270
271  def as_ast(self):
272  """Return a pointer to the corresponding C Z3_ast object."""
273  return self.ast
274
275  def ctx_ref(self):
276  """Return a reference to the C context where this AST node is stored."""
277  return self.ctx.ref()
278
279  def eq(self, other):
280  """Return `True` if `self` and `other` are structurally identical.
281
282  >>> x = Int('x')
283  >>> n1 = x + 1
284  >>> n2 = 1 + x
285  >>> n1.eq(n2)
286  False
287  >>> n1 = simplify(n1)
288  >>> n2 = simplify(n2)
289  >>> n1.eq(n2)
290  True
291  """
292  if __debug__:
293  _z3_assert(is_ast(other), "Z3 AST expected")
294  return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
295
296  def translate(self, target):
297  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
298
299  >>> c1 = Context()
300  >>> c2 = Context()
301  >>> x = Int('x', c1)
302  >>> y = Int('y', c2)
303  >>> # Nodes in different contexts can't be mixed.
304  >>> # However, we can translate nodes from one context to another.
305  >>> x.translate(c2) + y
306  x + y
307  """
308  if __debug__:
309  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
310  return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
311
312  def hash(self):
313  """Return a hashcode for the `self`.
314
315  >>> n1 = simplify(Int('x') + 1)
316  >>> n2 = simplify(2 + Int('x') - 1)
317  >>> n1.hash() == n2.hash()
318  True
319  """
320  return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
321
322 def is_ast(a):
323  """Return `True` if `a` is an AST node.
324
325  >>> is_ast(10)
326  False
327  >>> is_ast(IntVal(10))
328  True
329  >>> is_ast(Int('x'))
330  True
331  >>> is_ast(BoolSort())
332  True
333  >>> is_ast(Function('f', IntSort(), IntSort()))
334  True
335  >>> is_ast("x")
336  False
337  >>> is_ast(Solver())
338  False
339  """
340  return isinstance(a, AstRef)
341
342 def eq(a, b):
343  """Return `True` if `a` and `b` are structurally identical AST nodes.
344
345  >>> x = Int('x')
346  >>> y = Int('y')
347  >>> eq(x, y)
348  False
349  >>> eq(x + 1, x + 1)
350  True
351  >>> eq(x + 1, 1 + x)
352  False
353  >>> eq(simplify(x + 1), simplify(1 + x))
354  True
355  """
356  if __debug__:
357  _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
358  return a.eq(b)
359
360 def _ast_kind(ctx, a):
361  if is_ast(a):
362  a = a.as_ast()
363  return Z3_get_ast_kind(ctx.ref(), a)
364
365 def _ctx_from_ast_arg_list(args, default_ctx=None):
366  ctx = None
367  for a in args:
368  if is_ast(a) or is_probe(a):
369  if ctx == None:
370  ctx = a.ctx
371  else:
372  if __debug__:
373  _z3_assert(ctx == a.ctx, "Context mismatch")
374  if ctx == None:
375  ctx = default_ctx
376  return ctx
377
378 def _ctx_from_ast_args(*args):
379  return _ctx_from_ast_arg_list(args)
380
381 def _to_func_decl_array(args):
382  sz = len(args)
383  _args = (FuncDecl * sz)()
384  for i in range(sz):
385  _args[i] = args[i].as_func_decl()
386  return _args, sz
387
388 def _to_ast_array(args):
389  sz = len(args)
390  _args = (Ast * sz)()
391  for i in range(sz):
392  _args[i] = args[i].as_ast()
393  return _args, sz
394
395 def _to_ref_array(ref, args):
396  sz = len(args)
397  _args = (ref * sz)()
398  for i in range(sz):
399  _args[i] = args[i].as_ast()
400  return _args, sz
401
402 def _to_ast_ref(a, ctx):
403  k = _ast_kind(ctx, a)
404  if k == Z3_SORT_AST:
405  return _to_sort_ref(a, ctx)
406  elif k == Z3_FUNC_DECL_AST:
407  return _to_func_decl_ref(a, ctx)
408  else:
409  return _to_expr_ref(a, ctx)
410
411 #########################################
412 #
413 # Sorts
414 #
415 #########################################
416
417 def _sort_kind(ctx, s):
418  return Z3_get_sort_kind(ctx.ref(), s)
419
421  """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node."""
422  def as_ast(self):
423  return Z3_sort_to_ast(self.ctx_ref(), self.ast)
424
425  def kind(self):
426  """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
427
428  >>> b = BoolSort()
429  >>> b.kind() == Z3_BOOL_SORT
430  True
431  >>> b.kind() == Z3_INT_SORT
432  False
433  >>> A = ArraySort(IntSort(), IntSort())
434  >>> A.kind() == Z3_ARRAY_SORT
435  True
436  >>> A.kind() == Z3_INT_SORT
437  False
438  """
439  return _sort_kind(self.ctx, self.ast)
440
441  def subsort(self, other):
442  """Return `True` if `self` is a subsort of `other`.
443
444  >>> IntSort().subsort(RealSort())
445  True
446  """
447  return False
448
449  def cast(self, val):
450  """Try to cast `val` as an element of sort `self`.
451
452  This method is used in Z3Py to convert Python objects such as integers,
453  floats, longs and strings into Z3 expressions.
454
455  >>> x = Int('x')
456  >>> RealSort().cast(x)
457  ToReal(x)
458  """
459  if __debug__:
460  _z3_assert(is_expr(val), "Z3 expression expected")
461  _z3_assert(self.eq(val.sort()), "Sort mismatch")
462  return val
463
464  def name(self):
465  """Return the name (string) of sort `self`.
466
467  >>> BoolSort().name()
468  'Bool'
469  >>> ArraySort(IntSort(), IntSort()).name()
470  'Array'
471  """
472  return _symbol2py(self.ctx, Z3_get_sort_name(self.ctx_ref(), self.ast))
473
474  def __eq__(self, other):
475  """Return `True` if `self` and `other` are the same Z3 sort.
476
477  >>> p = Bool('p')
478  >>> p.sort() == BoolSort()
479  True
480  >>> p.sort() == IntSort()
481  False
482  """
483  if other == None:
484  return False
485  return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
486
487  def __ne__(self, other):
488  """Return `True` if `self` and `other` are not the same Z3 sort.
489
490  >>> p = Bool('p')
491  >>> p.sort() != BoolSort()
492  False
493  >>> p.sort() != IntSort()
494  True
495  """
496  return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
497
498 def is_sort(s):
499  """Return `True` if `s` is a Z3 sort.
500
501  >>> is_sort(IntSort())
502  True
503  >>> is_sort(Int('x'))
504  False
505  >>> is_expr(Int('x'))
506  True
507  """
508  return isinstance(s, SortRef)
509
510 def _to_sort_ref(s, ctx):
511  if __debug__:
512  _z3_assert(isinstance(s, Sort), "Z3 Sort expected")
513  k = _sort_kind(ctx, s)
514  if k == Z3_BOOL_SORT:
515  return BoolSortRef(s, ctx)
516  elif k == Z3_INT_SORT or k == Z3_REAL_SORT:
517  return ArithSortRef(s, ctx)
518  elif k == Z3_BV_SORT:
519  return BitVecSortRef(s, ctx)
520  elif k == Z3_ARRAY_SORT:
521  return ArraySortRef(s, ctx)
522  elif k == Z3_DATATYPE_SORT:
523  return DatatypeSortRef(s, ctx)
524  return SortRef(s, ctx)
525
526 def _sort(ctx, a):
527  return _to_sort_ref(Z3_get_sort(ctx.ref(), a), ctx)
528
529 def DeclareSort(name, ctx=None):
530  """Create a new uninterpred sort named `name`.
531
532  If `ctx=None`, then the new sort is declared in the global Z3Py context.
533
534  >>> A = DeclareSort('A')
535  >>> a = Const('a', A)
536  >>> b = Const('b', A)
537  >>> a.sort() == A
538  True
539  >>> b.sort() == A
540  True
541  >>> a == b
542  a == b
543  """
544  ctx = _get_ctx(ctx)
545  return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
546
547 #########################################
548 #
549 # Function Declarations
550 #
551 #########################################
552
554  """Function declaration. Every constant and function have an associated declaration.
555
556  The declaration assigns a name, a sort (i.e., type), and for function
557  the sort (i.e., type) of each of its arguments. Note that, in Z3,
558  a constant is a function with 0 arguments.
559  """
560  def as_ast(self):
561  return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
562
563  def name(self):
564  """Return the name of the function declaration `self`.
565
566  >>> f = Function('f', IntSort(), IntSort())
567  >>> f.name()
568  'f'
569  >>> isinstance(f.name(), str)
570  True
571  """
572  return _symbol2py(self.ctx, Z3_get_decl_name(self.ctx_ref(), self.ast))
573
574  def arity(self):
575  """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0.
576
577  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
578  >>> f.arity()
579  2
580  """
581  return int(Z3_get_arity(self.ctx_ref(), self.ast))
582
583  def domain(self, i):
584  """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`.
585
586  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
587  >>> f.domain(0)
588  Int
589  >>> f.domain(1)
590  Real
591  """
592  if __debug__:
593  _z3_assert(i < self.arity(), "Index out of bounds")
594  return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
595
596  def range(self):
597  """Return the sort of the range of a function declaration. For constants, this is the sort of the constant.
598
599  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
600  >>> f.range()
601  Bool
602  """
603  return _to_sort_ref(Z3_get_range(self.ctx_ref(), self.ast), self.ctx)
604
605  def kind(self):
606  """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
607
608  >>> x = Int('x')
609  >>> d = (x + 1).decl()
611  True
612  >>> d.kind() == Z3_OP_MUL
613  False
614  """
615  return Z3_get_decl_kind(self.ctx_ref(), self.ast)
616
617  def __call__(self, *args):
618  """Create a Z3 application expression using the function `self`, and the given arguments.
619
620  The arguments must be Z3 expressions. This method assumes that
621  the sorts of the elements in `args` match the sorts of the
622  domain. Limited coersion is supported. For example, if
623  args[0] is a Python integer, and the function expects a Z3
624  integer, then the argument is automatically converted into a
625  Z3 integer.
626
627  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
628  >>> x = Int('x')
629  >>> y = Real('y')
630  >>> f(x, y)
631  f(x, y)
632  >>> f(x, x)
633  f(x, ToReal(x))
634  """
635  args = _get_args(args)
636  num = len(args)
637  if __debug__:
638  _z3_assert(num == self.arity(), "Incorrect number of arguments")
639  _args = (Ast * num)()
640  saved = []
641  for i in range(num):
642  # self.domain(i).cast(args[i]) may create a new Z3 expression,
643  # then we must save in 'saved' to prevent it from being garbage collected.
644  tmp = self.domain(i).cast(args[i])
645  saved.append(tmp)
646  _args[i] = tmp.as_ast()
647  return _to_expr_ref(Z3_mk_app(self.ctx_ref(), self.ast, len(args), _args), self.ctx)
648
650  """Return `True` if `a` is a Z3 function declaration.
651
652  >>> f = Function('f', IntSort(), IntSort())
653  >>> is_func_decl(f)
654  True
655  >>> x = Real('x')
656  >>> is_func_decl(x)
657  False
658  """
659  return isinstance(a, FuncDeclRef)
660
661 def Function(name, *sig):
662  """Create a new Z3 uninterpreted function with the given sorts.
663
664  >>> f = Function('f', IntSort(), IntSort())
665  >>> f(f(0))
666  f(f(0))
667  """
668  sig = _get_args(sig)
669  if __debug__:
670  _z3_assert(len(sig) > 0, "At least two arguments expected")
671  arity = len(sig) - 1
672  rng = sig[arity]
673  if __debug__:
674  _z3_assert(is_sort(rng), "Z3 sort expected")
675  dom = (Sort * arity)()
676  for i in range(arity):
677  if __debug__:
678  _z3_assert(is_sort(sig[i]), "Z3 sort expected")
679  dom[i] = sig[i].ast
680  ctx = rng.ctx
681  return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
682
683 def _to_func_decl_ref(a, ctx):
684  return FuncDeclRef(a, ctx)
685
686 #########################################
687 #
688 # Expressions
689 #
690 #########################################
691
693  """Constraints, formulas and terms are expressions in Z3.
694
695  Expressions are ASTs. Every expression has a sort.
696  There are three main kinds of expressions:
697  function applications, quantifiers and bounded variables.
698  A constant is a function application with 0 arguments.
699  For quantifier free problems, all expressions are
700  function applications.
701  """
702  def as_ast(self):
703  return self.ast
704
705  def sort(self):
706  """Return the sort of expression `self`.
707
708  >>> x = Int('x')
709  >>> (x + 1).sort()
710  Int
711  >>> y = Real('y')
712  >>> (x + y).sort()
713  Real
714  """
715  return _sort(self.ctx, self.as_ast())
716
717  def sort_kind(self):
718  """Shorthand for `self.sort().kind()`.
719
720  >>> a = Array('a', IntSort(), IntSort())
721  >>> a.sort_kind() == Z3_ARRAY_SORT
722  True
723  >>> a.sort_kind() == Z3_INT_SORT
724  False
725  """
726  return self.sort().kind()
727
728  def __eq__(self, other):
729  """Return a Z3 expression that represents the constraint `self == other`.
730
731  If `other` is `None`, then this method simply returns `False`.
732
733  >>> a = Int('a')
734  >>> b = Int('b')
735  >>> a == b
736  a == b
737  >>> a == None
738  False
739  """
740  if other == None:
741  return False
742  a, b = _coerce_exprs(self, other)
743  return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
744
745  def __ne__(self, other):
746  """Return a Z3 expression that represents the constraint `self != other`.
747
748  If `other` is `None`, then this method simply returns `True`.
749
750  >>> a = Int('a')
751  >>> b = Int('b')
752  >>> a != b
753  a != b
754  >>> a != None
755  True
756  """
757  if other == None:
758  return True
759  a, b = _coerce_exprs(self, other)
760  _args, sz = _to_ast_array((a, b))
761  return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
762
763  def decl(self):
764  """Return the Z3 function declaration associated with a Z3 application.
765
766  >>> f = Function('f', IntSort(), IntSort())
767  >>> a = Int('a')
768  >>> t = f(a)
769  >>> eq(t.decl(), f)
770  True
771  >>> (a + 1).decl()
772  +
773  """
774  if __debug__:
775  _z3_assert(is_app(self), "Z3 application expected")
776  return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
777
778  def num_args(self):
779  """Return the number of arguments of a Z3 application.
780
781  >>> a = Int('a')
782  >>> b = Int('b')
783  >>> (a + b).num_args()
784  2
785  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
786  >>> t = f(a, b, 0)
787  >>> t.num_args()
788  3
789  """
790  if __debug__:
791  _z3_assert(is_app(self), "Z3 application expected")
792  return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
793
794  def arg(self, idx):
795  """Return argument `idx` of the application `self`.
796
797  This method assumes that `self` is a function application with at least `idx+1` arguments.
798
799  >>> a = Int('a')
800  >>> b = Int('b')
801  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
802  >>> t = f(a, b, 0)
803  >>> t.arg(0)
804  a
805  >>> t.arg(1)
806  b
807  >>> t.arg(2)
808  0
809  """
810  if __debug__:
811  _z3_assert(is_app(self), "Z3 application expected")
812  _z3_assert(idx < self.num_args(), "Invalid argument index")
813  return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
814
815  def children(self):
816  """Return a list containing the children of the given expression
817
818  >>> a = Int('a')
819  >>> b = Int('b')
820  >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
821  >>> t = f(a, b, 0)
822  >>> t.children()
823  [a, b, 0]
824  """
825  if is_app(self):
826  return [self.arg(i) for i in range(self.num_args())]
827  else:
828  return []
829
830 def _to_expr_ref(a, ctx):
831  if isinstance(a, Pattern):
832  return PatternRef(a, ctx)
833  ctx_ref = ctx.ref()
834  k = Z3_get_ast_kind(ctx_ref, a)
835  if k == Z3_QUANTIFIER_AST:
836  return QuantifierRef(a, ctx)
837  sk = Z3_get_sort_kind(ctx_ref, Z3_get_sort(ctx_ref, a))
838  if sk == Z3_BOOL_SORT:
839  return BoolRef(a, ctx)
840  if sk == Z3_INT_SORT:
841  if k == Z3_NUMERAL_AST:
842  return IntNumRef(a, ctx)
843  return ArithRef(a, ctx)
844  if sk == Z3_REAL_SORT:
845  if k == Z3_NUMERAL_AST:
846  return RatNumRef(a, ctx)
847  if _is_algebraic(ctx, a):
848  return AlgebraicNumRef(a, ctx)
849  return ArithRef(a, ctx)
850  if sk == Z3_BV_SORT:
851  if k == Z3_NUMERAL_AST:
852  return BitVecNumRef(a, ctx)
853  else:
854  return BitVecRef(a, ctx)
855  if sk == Z3_ARRAY_SORT:
856  return ArrayRef(a, ctx)
857  if sk == Z3_DATATYPE_SORT:
858  return DatatypeRef(a, ctx)
859  return ExprRef(a, ctx)
860
861 def _coerce_expr_merge(s, a):
862  if is_expr(a):
863  s1 = a.sort()
864  if s == None:
865  return s1
866  if s1.eq(s):
867  return s
868  elif s.subsort(s1):
869  return s1
870  elif s1.subsort(s):
871  return s
872  else:
873  if __debug__:
874  _z3_assert(False, "sort mismatch")
875  else:
876  return s
877
878 def _coerce_exprs(a, b, ctx=None):
879  if not is_expr(a) and not is_expr(b):
880  a = _py2expr(a, ctx)
881  b = _py2expr(b, ctx)
882  s = None
883  s = _coerce_expr_merge(s, a)
884  s = _coerce_expr_merge(s, b)
885  a = s.cast(a)
886  b = s.cast(b)
887  return (a, b)
888
889 def _coerce_expr_list(alist, ctx=None):
890  if filter(is_expr, alist) == []:
891  alist = map(lambda a: _py2expr(a, ctx), alist)
892  s = reduce(_coerce_expr_merge, alist, None)
893  return map(lambda a: s.cast(a), alist)
894
895 def is_expr(a):
896  """Return `True` if `a` is a Z3 expression.
897
898  >>> a = Int('a')
899  >>> is_expr(a)
900  True
901  >>> is_expr(a + 1)
902  True
903  >>> is_expr(IntSort())
904  False
905  >>> is_expr(1)
906  False
907  >>> is_expr(IntVal(1))
908  True
909  >>> x = Int('x')
910  >>> is_expr(ForAll(x, x >= 0))
911  True
912  """
913  return isinstance(a, ExprRef)
914
915 def is_app(a):
916  """Return `True` if `a` is a Z3 function application.
917
918  Note that, constants are function applications with 0 arguments.
919
920  >>> a = Int('a')
921  >>> is_app(a)
922  True
923  >>> is_app(a + 1)
924  True
925  >>> is_app(IntSort())
926  False
927  >>> is_app(1)
928  False
929  >>> is_app(IntVal(1))
930  True
931  >>> x = Int('x')
932  >>> is_app(ForAll(x, x >= 0))
933  False
934  """
935  if not isinstance(a, ExprRef):
936  return False
937  k = _ast_kind(a.ctx, a)
938  return k == Z3_NUMERAL_AST or k == Z3_APP_AST
939
940 def is_const(a):
941  """Return `True` if `a` is Z3 constant/variable expression.
942
943  >>> a = Int('a')
944  >>> is_const(a)
945  True
946  >>> is_const(a + 1)
947  False
948  >>> is_const(1)
949  False
950  >>> is_const(IntVal(1))
951  True
952  >>> x = Int('x')
953  >>> is_const(ForAll(x, x >= 0))
954  False
955  """
956  return is_app(a) and a.num_args() == 0
957
958 def is_var(a):
959  """Return `True` if `a` is variable.
960
961  Z3 uses de-Bruijn indices for representing bound variables in
962  quantifiers.
963
964  >>> x = Int('x')
965  >>> is_var(x)
966  False
967  >>> is_const(x)
968  True
969  >>> f = Function('f', IntSort(), IntSort())
970  >>> # Z3 replaces x with bound variables when ForAll is executed.
971  >>> q = ForAll(x, f(x) == x)
972  >>> b = q.body()
973  >>> b
974  f(Var(0)) == Var(0)
975  >>> b.arg(1)
976  Var(0)
977  >>> is_var(b.arg(1))
978  True
979  """
980  return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
981
983  """Return the de-Bruijn index of the Z3 bounded variable `a`.
984
985  >>> x = Int('x')
986  >>> y = Int('y')
987  >>> is_var(x)
988  False
989  >>> is_const(x)
990  True
991  >>> f = Function('f', IntSort(), IntSort(), IntSort())
992  >>> # Z3 replaces x and y with bound variables when ForAll is executed.
993  >>> q = ForAll([x, y], f(x, y) == x + y)
994  >>> q.body()
995  f(Var(1), Var(0)) == Var(1) + Var(0)
996  >>> b = q.body()
997  >>> b.arg(0)
998  f(Var(1), Var(0))
999  >>> v1 = b.arg(0).arg(0)
1000  >>> v2 = b.arg(0).arg(1)
1001  >>> v1
1002  Var(1)
1003  >>> v2
1004  Var(0)
1005  >>> get_var_index(v1)
1006  1
1007  >>> get_var_index(v2)
1008  0
1009  """
1010  if __debug__:
1011  _z3_assert(is_var(a), "Z3 bound variable expected")
1012  return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
1013
1014 def is_app_of(a, k):
1015  """Return `True` if `a` is an application of the given kind `k`.
1016
1017  >>> x = Int('x')
1018  >>> n = x + 1
1020  True
1021  >>> is_app_of(n, Z3_OP_MUL)
1022  False
1023  """
1024  return is_app(a) and a.decl().kind() == k
1025
1026 def If(a, b, c, ctx=None):
1027  """Create a Z3 if-then-else expression.
1028
1029  >>> x = Int('x')
1030  >>> y = Int('y')
1031  >>> max = If(x > y, x, y)
1032  >>> max
1033  If(x > y, x, y)
1034  >>> simplify(max)
1035  If(x <= y, y, x)
1036  """
1037  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1038  return Cond(a, b, c, ctx)
1039  else:
1040  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1041  s = BoolSort(ctx)
1042  a = s.cast(a)
1043  b, c = _coerce_exprs(b, c, ctx)
1044  if __debug__:
1045  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1046  return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1047
1048 def Distinct(*args):
1049  """Create a Z3 distinct expression.
1050
1051  >>> x = Int('x')
1052  >>> y = Int('y')
1053  >>> Distinct(x, y)
1054  x != y
1055  >>> z = Int('z')
1056  >>> Distinct(x, y, z)
1057  Distinct(x, y, z)
1058  >>> simplify(Distinct(x, y, z))
1059  Distinct(x, y, z)
1060  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1061  And(Not(x == y), Not(x == z), Not(y == z))
1062  """
1063  args = _get_args(args)
1064  ctx = _ctx_from_ast_arg_list(args)
1065  if __debug__:
1066  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
1067  args = _coerce_expr_list(args, ctx)
1068  _args, sz = _to_ast_array(args)
1069  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
1070
1071 def _mk_bin(f, a, b):
1072  args = (Ast * 2)()
1073  if __debug__:
1074  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1075  args[0] = a.as_ast()
1076  args[1] = b.as_ast()
1077  return f(a.ctx.ref(), 2, args)
1078
1079 def Const(name, sort):
1080  """Create a constant of the given sort.
1081
1082  >>> Const('x', IntSort())
1083  x
1084  """
1085  if __debug__:
1086  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1087  ctx = sort.ctx
1088  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1089
1090 def Consts(names, sort):
1091  """Create a several constants of the given sort.
1092
1093  `names` is a string containing the names of all constants to be created.
1094  Blank spaces separate the names of different constants.
1095
1096  >>> x, y, z = Consts('x y z', IntSort())
1097  >>> x + y + z
1098  x + y + z
1099  """
1100  if isinstance(names, str):
1101  names = names.split(" ")
1102  return [Const(name, sort) for name in names]
1103
1104 def Var(idx, s):
1105  """Create a Z3 free variable. Free variables are used to create quantified formulas.
1106
1107  >>> Var(0, IntSort())
1108  Var(0)
1109  >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1110  False
1111  """
1112  if __debug__:
1113  _z3_assert(is_sort(s), "Z3 sort expected")
1114  return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1115
1116 #########################################
1117 #
1118 # Booleans
1119 #
1120 #########################################
1121
1123  """Boolean sort."""
1124  def cast(self, val):
1125  """Try to cast `val` as a Boolean.
1126
1127  >>> x = BoolSort().cast(True)
1128  >>> x
1129  True
1130  >>> is_expr(x)
1131  True
1132  >>> is_expr(True)
1133  False
1134  >>> x.sort()
1135  Bool
1136  """
1137  if isinstance(val, bool):
1138  return BoolVal(val, self.ctx)
1139  if __debug__:
1140  _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected")
1141  _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
1142  return val
1143
1145  """All Boolean expressions are instances of this class."""
1146  def sort(self):
1147  return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
1148
1149 def is_bool(a):
1150  """Return `True` if `a` is a Z3 Boolean expression.
1151
1152  >>> p = Bool('p')
1153  >>> is_bool(p)
1154  True
1155  >>> q = Bool('q')
1156  >>> is_bool(And(p, q))
1157  True
1158  >>> x = Real('x')
1159  >>> is_bool(x)
1160  False
1161  >>> is_bool(x == 0)
1162  True
1163  """
1164  return isinstance(a, BoolRef)
1165
1166 def is_true(a):
1167  """Return `True` if `a` is the Z3 true expression.
1168
1169  >>> p = Bool('p')
1170  >>> is_true(p)
1171  False
1172  >>> is_true(simplify(p == p))
1173  True
1174  >>> x = Real('x')
1175  >>> is_true(x == 0)
1176  False
1177  >>> # True is a Python Boolean expression
1178  >>> is_true(True)
1179  False
1180  """
1181  return is_app_of(a, Z3_OP_TRUE)
1182
1183 def is_false(a):
1184  """Return `True` if `a` is the Z3 false expression.
1185
1186  >>> p = Bool('p')
1187  >>> is_false(p)
1188  False
1189  >>> is_false(False)
1190  False
1191  >>> is_false(BoolVal(False))
1192  True
1193  """
1194  return is_app_of(a, Z3_OP_FALSE)
1195
1196 def is_and(a):
1197  """Return `True` if `a` is a Z3 and expression.
1198
1199  >>> p, q = Bools('p q')
1200  >>> is_and(And(p, q))
1201  True
1202  >>> is_and(Or(p, q))
1203  False
1204  """
1205  return is_app_of(a, Z3_OP_AND)
1206
1207 def is_or(a):
1208  """Return `True` if `a` is a Z3 or expression.
1209
1210  >>> p, q = Bools('p q')
1211  >>> is_or(Or(p, q))
1212  True
1213  >>> is_or(And(p, q))
1214  False
1215  """
1216  return is_app_of(a, Z3_OP_OR)
1217
1218 def is_not(a):
1219  """Return `True` if `a` is a Z3 not expression.
1220
1221  >>> p = Bool('p')
1222  >>> is_not(p)
1223  False
1224  >>> is_not(Not(p))
1225  True
1226  """
1227  return is_app_of(a, Z3_OP_NOT)
1228
1229 def is_eq(a):
1230  """Return `True` if `a` is a Z3 equality expression.
1231
1232  >>> x, y = Ints('x y')
1233  >>> is_eq(x == y)
1234  True
1235  """
1236  return is_app_of(a, Z3_OP_EQ)
1237
1239  """Return `True` if `a` is a Z3 distinct expression.
1240
1241  >>> x, y, z = Ints('x y z')
1242  >>> is_distinct(x == y)
1243  False
1244  >>> is_distinct(Distinct(x, y, z))
1245  True
1246  """
1247  return is_app_of(a, Z3_OP_DISTINCT)
1248
1249 def BoolSort(ctx=None):
1250  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1251
1252  >>> BoolSort()
1253  Bool
1254  >>> p = Const('p', BoolSort())
1255  >>> is_bool(p)
1256  True
1257  >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1258  >>> r(0, 1)
1259  r(0, 1)
1260  >>> is_bool(r(0, 1))
1261  True
1262  """
1263  ctx = _get_ctx(ctx)
1264  return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1265
1266 def BoolVal(val, ctx=None):
1267  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1268
1269  >>> BoolVal(True)
1270  True
1271  >>> is_true(BoolVal(True))
1272  True
1273  >>> is_true(True)
1274  False
1275  >>> is_false(BoolVal(False))
1276  True
1277  """
1278  ctx = _get_ctx(ctx)
1279  if val == False:
1280  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1281  else:
1282  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1283
1284 def Bool(name, ctx=None):
1285  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1286
1287  >>> p = Bool('p')
1288  >>> q = Bool('q')
1289  >>> And(p, q)
1290  And(p, q)
1291  """
1292  ctx = _get_ctx(ctx)
1293  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1294
1295 def Bools(names, ctx=None):
1296  """Return a tuple of Boolean constants.
1297
1298  `names` is a single string containing all names separated by blank spaces.
1299  If `ctx=None`, then the global context is used.
1300
1301  >>> p, q, r = Bools('p q r')
1302  >>> And(p, Or(q, r))
1303  And(p, Or(q, r))
1304  """
1305  ctx = _get_ctx(ctx)
1306  if isinstance(names, str):
1307  names = names.split(" ")
1308  return [Bool(name, ctx) for name in names]
1309
1310 def BoolVector(prefix, sz, ctx=None):
1311  """Return a list of Boolean constants of size `sz`.
1312
1313  The constants are named using the given prefix.
1314  If `ctx=None`, then the global context is used.
1315
1316  >>> P = BoolVector('p', 3)
1317  >>> P
1318  [p__0, p__1, p__2]
1319  >>> And(P)
1320  And(p__0, p__1, p__2)
1321  """
1322  return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
1323
1324 def FreshBool(prefix='b', ctx=None):
1325  """Return a fresh Bolean constant in the given context using the given prefix.
1326
1327  If `ctx=None`, then the global context is used.
1328
1329  >>> b1 = FreshBool()
1330  >>> b2 = FreshBool()
1331  >>> eq(b1, b2)
1332  False
1333  """
1334  ctx = _get_ctx(ctx)
1335  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1336
1337 def Implies(a, b, ctx=None):
1338  """Create a Z3 implies expression.
1339
1340  >>> p, q = Bools('p q')
1341  >>> Implies(p, q)
1342  Implies(p, q)
1343  >>> simplify(Implies(p, q))
1344  Or(Not(p), q)
1345  """
1346  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1347  s = BoolSort(ctx)
1348  a = s.cast(a)
1349  b = s.cast(b)
1350  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1351
1352 def Xor(a, b, ctx=None):
1353  """Create a Z3 Xor expression.
1354
1355  >>> p, q = Bools('p q')
1356  >>> Xor(p, q)
1357  Xor(p, q)
1358  >>> simplify(Xor(p, q))
1359  Not(p) == q
1360  """
1361  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1362  s = BoolSort(ctx)
1363  a = s.cast(a)
1364  b = s.cast(b)
1365  return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1366
1367 def Not(a, ctx=None):
1368  """Create a Z3 not expression or probe.
1369
1370  >>> p = Bool('p')
1371  >>> Not(Not(p))
1372  Not(Not(p))
1373  >>> simplify(Not(Not(p)))
1374  p
1375  """
1376  ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1377  if is_probe(a):
1378  # Not is also used to build probes
1379  return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
1380  else:
1381  s = BoolSort(ctx)
1382  a = s.cast(a)
1383  return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
1384
1385 def _has_probe(args):
1386  """Return `True` if one of the elements of the given collection is a Z3 probe."""
1387  for arg in args:
1388  if is_probe(arg):
1389  return True
1390  return False
1391
1392 def And(*args):
1393  """Create a Z3 and-expression or and-probe.
1394
1395  >>> p, q, r = Bools('p q r')
1396  >>> And(p, q, r)
1397  And(p, q, r)
1398  >>> P = BoolVector('p', 5)
1399  >>> And(P)
1400  And(p__0, p__1, p__2, p__3, p__4)
1401  """
1402  args = _get_args(args)
1403  ctx = _ctx_from_ast_arg_list(args)
1404  if __debug__:
1405  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
1406  if _has_probe(args):
1407  return _probe_and(args, ctx)
1408  else:
1409  args = _coerce_expr_list(args, ctx)
1410  _args, sz = _to_ast_array(args)
1411  return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1412
1413 def Or(*args):
1414  """Create a Z3 or-expression or or-probe.
1415
1416  >>> p, q, r = Bools('p q r')
1417  >>> Or(p, q, r)
1418  Or(p, q, r)
1419  >>> P = BoolVector('p', 5)
1420  >>> Or(P)
1421  Or(p__0, p__1, p__2, p__3, p__4)
1422  """
1423  args = _get_args(args)
1424  ctx = _ctx_from_ast_arg_list(args)
1425  if __debug__:
1426  _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
1427  if _has_probe(args):
1428  return _probe_or(args, ctx)
1429  else:
1430  args = _coerce_expr_list(args, ctx)
1431  _args, sz = _to_ast_array(args)
1432  return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
1433
1434 #########################################
1435 #
1436 # Patterns
1437 #
1438 #########################################
1439
1440 class PatternRef(ExprRef):
1441  """Patterns are hints for quantifier instantiation.
1442
1443  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1444  """
1445  def as_ast(self):
1446  return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
1447
1448 def is_pattern(a):
1449  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1450
1451  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1452
1453  >>> f = Function('f', IntSort(), IntSort())
1454  >>> x = Int('x')
1455  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1456  >>> q
1457  ForAll(x, f(x) == 0)
1458  >>> q.num_patterns()
1459  1
1460  >>> is_pattern(q.pattern(0))
1461  True
1462  >>> q.pattern(0)
1463  f(Var(0))
1464  """
1465  return isinstance(a, PatternRef)
1466
1467 def MultiPattern(*args):
1468  """Create a Z3 multi-pattern using the given expressions `*args`
1469
1470  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1471
1472  >>> f = Function('f', IntSort(), IntSort())
1473  >>> g = Function('g', IntSort(), IntSort())
1474  >>> x = Int('x')
1475  >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1476  >>> q
1477  ForAll(x, f(x) != g(x))
1478  >>> q.num_patterns()
1479  1
1480  >>> is_pattern(q.pattern(0))
1481  True
1482  >>> q.pattern(0)
1483  MultiPattern(f(Var(0)), g(Var(0)))
1484  """
1485  if __debug__:
1486  _z3_assert(len(args) > 0, "At least one argument expected")
1487  _z3_assert(all(map(is_expr, args)), "Z3 expressions expected")
1488  ctx = args[0].ctx
1489  args, sz = _to_ast_array(args)
1490  return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
1491
1492 def _to_pattern(arg):
1493  if is_pattern(arg):
1494  return arg
1495  else:
1496  return MultiPattern(arg)
1497
1498 #########################################
1499 #
1500 # Quantifiers
1501 #
1502 #########################################
1503
1504 class QuantifierRef(BoolRef):
1505  """Universally and Existentially quantified formulas."""
1506
1507  def as_ast(self):
1508  return self.ast
1509
1510  def sort(self):
1511  """Return the Boolean sort."""
1512  return BoolSort(self.ctx)
1513
1514  def is_forall(self):
1515  """Return `True` if `self` is a universal quantifier.
1516
1517  >>> f = Function('f', IntSort(), IntSort())
1518  >>> x = Int('x')
1519  >>> q = ForAll(x, f(x) == 0)
1520  >>> q.is_forall()
1521  True
1522  >>> q = Exists(x, f(x) != 0)
1523  >>> q.is_forall()
1524  False
1525  """
1526  return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
1527
1528  def weight(self):
1529  """Return the weight annotation of `self`.
1530
1531  >>> f = Function('f', IntSort(), IntSort())
1532  >>> x = Int('x')
1533  >>> q = ForAll(x, f(x) == 0)
1534  >>> q.weight()
1535  1
1536  >>> q = ForAll(x, f(x) == 0, weight=10)
1537  >>> q.weight()
1538  10
1539  """
1540  return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
1541
1542  def num_patterns(self):
1543  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
1544
1545  >>> f = Function('f', IntSort(), IntSort())
1546  >>> g = Function('g', IntSort(), IntSort())
1547  >>> x = Int('x')
1548  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1549  >>> q.num_patterns()
1550  2
1551  """
1552  return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
1553
1554  def pattern(self, idx):
1555  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
1556
1557  >>> f = Function('f', IntSort(), IntSort())
1558  >>> g = Function('g', IntSort(), IntSort())
1559  >>> x = Int('x')
1560  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1561  >>> q.num_patterns()
1562  2
1563  >>> q.pattern(0)
1564  f(Var(0))
1565  >>> q.pattern(1)
1566  g(Var(0))
1567  """
1568  if __debug__:
1569  _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1570  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1571
1572  def num_no_patterns(self):
1573  """Return the number of no-patterns."""
1574  return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
1575
1576  def no_pattern(self, idx):
1577  """Return a no-pattern."""
1578  if __debug__:
1579  _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1580  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1581
1582  def body(self):
1583  """Return the expression being quantified.
1584
1585  >>> f = Function('f', IntSort(), IntSort())
1586  >>> x = Int('x')
1587  >>> q = ForAll(x, f(x) == 0)
1588  >>> q.body()
1589  f(Var(0)) == 0
1590  """
1591  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
1592
1593  def num_vars(self):
1594  """Return the number of variables bounded by this quantifier.
1595
1596  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1597  >>> x = Int('x')
1598  >>> y = Int('y')
1599  >>> q = ForAll([x, y], f(x, y) >= x)
1600  >>> q.num_vars()
1601  2
1602  """
1603  return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
1604
1605  def var_name(self, idx):
1606  """Return a string representing a name used when displaying the quantifier.
1607
1608  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1609  >>> x = Int('x')
1610  >>> y = Int('y')
1611  >>> q = ForAll([x, y], f(x, y) >= x)
1612  >>> q.var_name(0)
1613  'x'
1614  >>> q.var_name(1)
1615  'y'
1616  """
1617  if __debug__:
1618  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1619  return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
1620
1621  def var_sort(self, idx):
1622  """Return the sort of a bound variable.
1623
1624  >>> f = Function('f', IntSort(), RealSort(), IntSort())
1625  >>> x = Int('x')
1626  >>> y = Real('y')
1627  >>> q = ForAll([x, y], f(x, y) >= x)
1628  >>> q.var_sort(0)
1629  Int
1630  >>> q.var_sort(1)
1631  Real
1632  """
1633  if __debug__:
1634  _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1635  return SortRef(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
1636
1637  def children(self):
1638  """Return a list containing a single element self.body()
1639
1640  >>> f = Function('f', IntSort(), IntSort())
1641  >>> x = Int('x')
1642  >>> q = ForAll(x, f(x) == 0)
1643  >>> q.children()
1644  [f(Var(0)) == 0]
1645  """
1646  return [ self.body() ]
1647
1648 def is_quantifier(a):
1649  """Return `True` if `a` is a Z3 quantifier.
1650
1651  >>> f = Function('f', IntSort(), IntSort())
1652  >>> x = Int('x')
1653  >>> q = ForAll(x, f(x) == 0)
1654  >>> is_quantifier(q)
1655  True
1656  >>> is_quantifier(f(x))
1657  False
1658  """
1659  return isinstance(a, QuantifierRef)
1660
1661 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1662  if __debug__:
1663  _z3_assert(is_bool(body), "Z3 expression expected")
1664  _z3_assert(is_const(vs) or (len(vs) > 0 and all(map(is_const, vs))), "Invalid bounded variable(s)")
1665  _z3_assert(all(map(lambda a: is_pattern(a) or is_expr(a), patterns)), "Z3 patterns expected")
1666  _z3_assert(all(map(is_expr, no_patterns)), "no patterns are Z3 expressions")
1667  ctx = body.ctx
1668  if is_app(vs):
1669  vs = [vs]
1670  num_vars = len(vs)
1671  _vs = (Ast * num_vars)()
1672  for i in range(num_vars):
1673  ## TODO: Check if is constant
1674  _vs[i] = vs[i].as_ast()
1675  patterns = map(_to_pattern, patterns)
1676  num_pats = len(patterns)
1677  _pats = (Pattern * num_pats)()
1678  for i in range(num_pats):
1679  _pats[i] = patterns[i].ast
1680  _no_pats, num_no_pats = _to_ast_array(no_patterns)
1681  qid = to_symbol(qid, ctx)
1682  skid = to_symbol(skid, ctx)
1683  return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid,
1684  num_vars, _vs,
1685  num_pats, _pats,
1686  num_no_pats, _no_pats,
1687  body.as_ast()), ctx)
1688
1689 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1690  """Create a Z3 forall formula.
1691
1692  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
1693
1694  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1695
1696  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1697  >>> x = Int('x')
1698  >>> y = Int('y')
1699  >>> ForAll([x, y], f(x, y) >= x)
1700  ForAll([x, y], f(x, y) >= x)
1701  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
1702  ForAll([x, y], f(x, y) >= x)
1703  >>> ForAll([x, y], f(x, y) >= x, weight=10)
1704  ForAll([x, y], f(x, y) >= x)
1705  """
1706  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
1707
1708 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1709  """Create a Z3 exists formula.
1710
1711  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
1712
1713  See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
1714
1715  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1716  >>> x = Int('x')
1717  >>> y = Int('y')
1718  >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
1719  >>> q
1720  Exists([x, y], f(x, y) >= x)
1721  >>> Tactic('nnf')(q)
1722  [[f(x!foo!1, y!foo!0) >= x!foo!1]]
1723  >>> Tactic('nnf')(q).as_expr()
1724  f(x!foo!3, y!foo!2) >= x!foo!3
1725  """
1726  return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
1727
1728 #########################################
1729 #
1730 # Arithmetic
1731 #
1732 #########################################
1733
1734 class ArithSortRef(SortRef):
1735  """Real and Integer sorts."""
1736
1737  def is_real(self):
1738  """Return `True` if `self` is the integer sort.
1739
1740  >>> x = Real('x')
1741  >>> x.is_real()
1742  True
1743  >>> (x + 1).is_real()
1744  True
1745  >>> x = Int('x')
1746  >>> x.is_real()
1747  False
1748  """
1749  return self.kind() == Z3_REAL_SORT
1750
1751  def is_int(self):
1752  """Return `True` if `self` is the real sort.
1753
1754  >>> x = Int('x')
1755  >>> x.is_int()
1756  True
1757  >>> (x + 1).is_int()
1758  True
1759  >>> x = Real('x')
1760  >>> x.is_int()
1761  False
1762  """
1763  return self.kind() == Z3_INT_SORT
1764
1765  def subsort(self, other):
1766  """Return `True` if `self` is a subsort of `other`."""
1767  return self.is_int() and is_arith_sort(other) and other.is_real()
1768
1769  def cast(self, val):
1770  """Try to cast `val` as an Integer or Real.
1771
1772  >>> IntSort().cast(10)
1773  10
1774  >>> is_int(IntSort().cast(10))
1775  True
1776  >>> is_int(10)
1777  False
1778  >>> RealSort().cast(10)
1779  10
1780  >>> is_real(RealSort().cast(10))
1781  True
1782  """
1783  if is_expr(val):
1784  if __debug__:
1785  _z3_assert(self.ctx == val.ctx, "Context mismatch")
1786  val_s = val.sort()
1787  if self.eq(val_s):
1788  return val
1789  if val_s.is_int() and self.is_real():
1791  if __debug__:
1792  _z3_assert(False, "Z3 Integer/Real expression expected" )
1793  else:
1794  if self.is_int():
1795  return IntVal(val, self.ctx)
1796  if self.is_real():
1797  return RealVal(val, self.ctx)
1798  if __debug__:
1799  _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
1800
1801 def is_arith_sort(s):
1802  """Return `True` if s is an arithmetical sort (type).
1803
1804  >>> is_arith_sort(IntSort())
1805  True
1806  >>> is_arith_sort(RealSort())
1807  True
1808  >>> is_arith_sort(BoolSort())
1809  False
1810  >>> n = Int('x') + 1
1811  >>> is_arith_sort(n.sort())
1812  True
1813  """
1814  return isinstance(s, ArithSortRef)
1815
1816 class ArithRef(ExprRef):
1817  """Integer and Real expressions."""
1818
1819  def sort(self):
1820  """Return the sort (type) of the arithmetical expression `self`.
1821
1822  >>> Int('x').sort()
1823  Int
1824  >>> (Real('x') + 1).sort()
1825  Real
1826  """
1827  return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
1828
1829  def is_int(self):
1830  """Return `True` if `self` is an integer expression.
1831
1832  >>> x = Int('x')
1833  >>> x.is_int()
1834  True
1835  >>> (x + 1).is_int()
1836  True
1837  >>> y = Real('y')
1838  >>> (x + y).is_int()
1839  False
1840  """
1841  return self.sort().is_int()
1842
1843  def is_real(self):
1844  """Return `True` if `self` is an real expression.
1845
1846  >>> x = Real('x')
1847  >>> x.is_real()
1848  True
1849  >>> (x + 1).is_real()
1850  True
1851  """
1852  return self.sort().is_real()
1853
1855  """Create the Z3 expression `self + other`.
1856
1857  >>> x = Int('x')
1858  >>> y = Int('y')
1859  >>> x + y
1860  x + y
1861  >>> (x + y).sort()
1862  Int
1863  """
1864  a, b = _coerce_exprs(self, other)
1865  return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
1866
1868  """Create the Z3 expression `other + self`.
1869
1870  >>> x = Int('x')
1871  >>> 10 + x
1872  10 + x
1873  """
1874  a, b = _coerce_exprs(self, other)
1875  return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
1876
1877  def __mul__(self, other):
1878  """Create the Z3 expression `self * other`.
1879
1880  >>> x = Real('x')
1881  >>> y = Real('y')
1882  >>> x * y
1883  x*y
1884  >>> (x * y).sort()
1885  Real
1886  """
1887  a, b = _coerce_exprs(self, other)
1888  return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
1889
1890  def __rmul__(self, other):
1891  """Create the Z3 expression `other * self`.
1892
1893  >>> x = Real('x')
1894  >>> 10 * x
1895  10*x
1896  """
1897  a, b = _coerce_exprs(self, other)
1898  return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
1899
1900  def __sub__(self, other):
1901  """Create the Z3 expression `self - other`.
1902
1903  >>> x = Int('x')
1904  >>> y = Int('y')
1905  >>> x - y
1906  x - y
1907  >>> (x - y).sort()
1908  Int
1909  """
1910  a, b = _coerce_exprs(self, other)
1911  return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
1912
1913  def __rsub__(self, other):
1914  """Create the Z3 expression `other - self`.
1915
1916  >>> x = Int('x')
1917  >>> 10 - x
1918  10 - x
1919  """
1920  a, b = _coerce_exprs(self, other)
1921  return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
1922
1923  def __pow__(self, other):
1924  """Create the Z3 expression `self**other` (** is the power operator).
1925
1926  >>> x = Real('x')
1927  >>> x**3
1928  x**3
1929  >>> (x**3).sort()
1930  Real
1931  >>> simplify(IntVal(2)**8)
1932  256
1933  """
1934  a, b = _coerce_exprs(self, other)
1935  return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
1936
1937  def __rpow__(self, other):
1938  """Create the Z3 expression `other**self` (** is the power operator).
1939
1940  >>> x = Real('x')
1941  >>> 2**x
1942  2**x
1943  >>> (2**x).sort()
1944  Real
1945  >>> simplify(2**IntVal(8))
1946  256
1947  """
1948  a, b = _coerce_exprs(self, other)
1949  return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
1950
1951  def __div__(self, other):
1952  """Create the Z3 expression `other/self`.
1953
1954  >>> x = Int('x')
1955  >>> y = Int('y')
1956  >>> x/y
1957  x/y
1958  >>> (x/y).sort()
1959  Int
1960  >>> (x/y).sexpr()
1961  '(div x y)'
1962  >>> x = Real('x')
1963  >>> y = Real('y')
1964  >>> x/y
1965  x/y
1966  >>> (x/y).sort()
1967  Real
1968  >>> (x/y).sexpr()
1969  '(/ x y)'
1970  """
1971  a, b = _coerce_exprs(self, other)
1972  return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
1973
1974  def __truediv__(self, other):
1975  """Create the Z3 expression `other/self`."""
1976  self.__div__(other)
1977
1978  def __rdiv__(self, other):
1979  """Create the Z3 expression `other/self`.
1980
1981  >>> x = Int('x')
1982  >>> 10/x
1983  10/x
1984  >>> (10/x).sexpr()
1985  '(div 10 x)'
1986  >>> x = Real('x')
1987  >>> 10/x
1988  10/x
1989  >>> (10/x).sexpr()
1990  '(/ 10.0 x)'
1991  """
1992  a, b = _coerce_exprs(self, other)
1993  return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
1994
1995  def __rtruediv__(self, other):
1996  """Create the Z3 expression `other/self`."""
1997  self.__rdiv__(other)
1998
1999  def __mod__(self, other):
2000  """Create the Z3 expression `other%self`.
2001
2002  >>> x = Int('x')
2003  >>> y = Int('y')
2004  >>> x % y
2005  x%y
2006  >>> simplify(IntVal(10) % IntVal(3))
2007  1
2008  """
2009  a, b = _coerce_exprs(self, other)
2010  if __debug__:
2011  _z3_assert(a.is_int(), "Z3 integer expression expected")
2012  return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2013
2014  def __rmod__(self, other):
2015  """Create the Z3 expression `other%self`.
2016
2017  >>> x = Int('x')
2018  >>> 10 % x
2019  10%x
2020  """
2021  a, b = _coerce_exprs(self, other)
2022  if __debug__:
2023  _z3_assert(a.is_int(), "Z3 integer expression expected")
2024  return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2025
2026  def __neg__(self):
2027  """Return an expression representing `-self`.
2028
2029  >>> x = Int('x')
2030  >>> -x
2031  -x
2032  >>> simplify(-(-x))
2033  x
2034  """
2035  return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
2036
2037  def __pos__(self):
2038  """Return `self`.
2039
2040  >>> x = Int('x')
2041  >>> +x
2042  x
2043  """
2044  return self
2045
2046  def __le__(self, other):
2047  """Create the Z3 expression `other <= self`.
2048
2049  >>> x, y = Ints('x y')
2050  >>> x <= y
2051  x <= y
2052  >>> y = Real('y')
2053  >>> x <= y
2054  ToReal(x) <= y
2055  """
2056  a, b = _coerce_exprs(self, other)
2057  return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2058
2059  def __lt__(self, other):
2060  """Create the Z3 expression `other < self`.
2061
2062  >>> x, y = Ints('x y')
2063  >>> x < y
2064  x < y
2065  >>> y = Real('y')
2066  >>> x < y
2067  ToReal(x) < y
2068  """
2069  a, b = _coerce_exprs(self, other)
2070  return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2071
2072  def __gt__(self, other):
2073  """Create the Z3 expression `other > self`.
2074
2075  >>> x, y = Ints('x y')
2076  >>> x > y
2077  x > y
2078  >>> y = Real('y')
2079  >>> x > y
2080  ToReal(x) > y
2081  """
2082  a, b = _coerce_exprs(self, other)
2083  return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2084
2085  def __ge__(self, other):
2086  """Create the Z3 expression `other >= self`.
2087
2088  >>> x, y = Ints('x y')
2089  >>> x >= y
2090  x >= y
2091  >>> y = Real('y')
2092  >>> x >= y
2093  ToReal(x) >= y
2094  """
2095  a, b = _coerce_exprs(self, other)
2096  return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2097
2098 def is_arith(a):
2099  """Return `True` if `a` is an arithmetical expression.
2100
2101  >>> x = Int('x')
2102  >>> is_arith(x)
2103  True
2104  >>> is_arith(x + 1)
2105  True
2106  >>> is_arith(1)
2107  False
2108  >>> is_arith(IntVal(1))
2109  True
2110  >>> y = Real('y')
2111  >>> is_arith(y)
2112  True
2113  >>> is_arith(y + 1)
2114  True
2115  """
2116  return isinstance(a, ArithRef)
2117
2118 def is_int(a):
2119  """Return `True` if `a` is an integer expression.
2120
2121  >>> x = Int('x')
2122  >>> is_int(x + 1)
2123  True
2124  >>> is_int(1)
2125  False
2126  >>> is_int(IntVal(1))
2127  True
2128  >>> y = Real('y')
2129  >>> is_int(y)
2130  False
2131  >>> is_int(y + 1)
2132  False
2133  """
2134  return is_arith(a) and a.is_int()
2135
2136 def is_real(a):
2137  """Return `True` if `a` is a real expression.
2138
2139  >>> x = Int('x')
2140  >>> is_real(x + 1)
2141  False
2142  >>> y = Real('y')
2143  >>> is_real(y)
2144  True
2145  >>> is_real(y + 1)
2146  True
2147  >>> is_real(1)
2148  False
2149  >>> is_real(RealVal(1))
2150  True
2151  """
2152  return is_arith(a) and a.is_real()
2153
2154 def _is_numeral(ctx, a):
2155  return Z3_is_numeral_ast(ctx.ref(), a)
2156
2157 def _is_algebraic(ctx, a):
2158  return Z3_is_algebraic_number(ctx.ref(), a)
2159
2160 def is_int_value(a):
2161  """Return `True` if `a` is an integer value of sort Int.
2162
2163  >>> is_int_value(IntVal(1))
2164  True
2165  >>> is_int_value(1)
2166  False
2167  >>> is_int_value(Int('x'))
2168  False
2169  >>> n = Int('x') + 1
2170  >>> n
2171  x + 1
2172  >>> n.arg(1)
2173  1
2174  >>> is_int_value(n.arg(1))
2175  True
2176  >>> is_int_value(RealVal("1/3"))
2177  False
2178  >>> is_int_value(RealVal(1))
2179  False
2180  """
2181  return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2182
2183 def is_rational_value(a):
2184  """Return `True` if `a` is rational value of sort Real.
2185
2186  >>> is_rational_value(RealVal(1))
2187  True
2188  >>> is_rational_value(RealVal("3/5"))
2189  True
2190  >>> is_rational_value(IntVal(1))
2191  False
2192  >>> is_rational_value(1)
2193  False
2194  >>> n = Real('x') + 1
2195  >>> n.arg(1)
2196  1
2197  >>> is_rational_value(n.arg(1))
2198  True
2199  >>> is_rational_value(Real('x'))
2200  False
2201  """
2202  return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2203
2204 def is_algebraic_value(a):
2205  """Return `True` if `a` is an algerbraic value of sort Real.
2206
2207  >>> is_algebraic_value(RealVal("3/5"))
2208  False
2209  >>> n = simplify(Sqrt(2))
2210  >>> n
2211  1.4142135623?
2212  >>> is_algebraic_value(n)
2213  True
2214  """
2215  return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2216
2218  """Return `True` if `a` is an expression of the form b + c.
2219
2220  >>> x, y = Ints('x y')
2222  True
2224  False
2225  """
2227
2228 def is_mul(a):
2229  """Return `True` if `a` is an expression of the form b * c.
2230
2231  >>> x, y = Ints('x y')
2232  >>> is_mul(x * y)
2233  True
2234  >>> is_mul(x - y)
2235  False
2236  """
2237  return is_app_of(a, Z3_OP_MUL)
2238
2239 def is_sub(a):
2240  """Return `True` if `a` is an expression of the form b - c.
2241
2242  >>> x, y = Ints('x y')
2243  >>> is_sub(x - y)
2244  True
2245  >>> is_sub(x + y)
2246  False
2247  """
2248  return is_app_of(a, Z3_OP_SUB)
2249
2250 def is_div(a):
2251  """Return `True` if `a` is an expression of the form b / c.
2252
2253  >>> x, y = Reals('x y')
2254  >>> is_div(x / y)
2255  True
2256  >>> is_div(x + y)
2257  False
2258  >>> x, y = Ints('x y')
2259  >>> is_div(x / y)
2260  False
2261  >>> is_idiv(x / y)
2262  True
2263  """
2264  return is_app_of(a, Z3_OP_DIV)
2265
2266 def is_idiv(a):
2267  """Return `True` if `a` is an expression of the form b div c.
2268
2269  >>> x, y = Ints('x y')
2270  >>> is_idiv(x / y)
2271  True
2272  >>> is_idiv(x + y)
2273  False
2274  """
2275  return is_app_of(a, Z3_OP_IDIV)
2276
2277 def is_mod(a):
2278  """Return `True` if `a` is an expression of the form b % c.
2279
2280  >>> x, y = Ints('x y')
2281  >>> is_mod(x % y)
2282  True
2283  >>> is_mod(x + y)
2284  False
2285  """
2286  return is_app_of(a, Z3_OP_MOD)
2287
2288 def is_le(a):
2289  """Return `True` if `a` is an expression of the form b <= c.
2290
2291  >>> x, y = Ints('x y')
2292  >>> is_le(x <= y)
2293  True
2294  >>> is_le(x < y)
2295  False
2296  """
2297  return is_app_of(a, Z3_OP_LE)
2298
2299 def is_lt(a):
2300  """Return `True` if `a` is an expression of the form b < c.
2301
2302  >>> x, y = Ints('x y')
2303  >>> is_lt(x < y)
2304  True
2305  >>> is_lt(x == y)
2306  False
2307  """
2308  return is_app_of(a, Z3_OP_LT)
2309
2310 def is_ge(a):
2311  """Return `True` if `a` is an expression of the form b >= c.
2312
2313  >>> x, y = Ints('x y')
2314  >>> is_ge(x >= y)
2315  True
2316  >>> is_ge(x == y)
2317  False
2318  """
2319  return is_app_of(a, Z3_OP_GE)
2320
2321 def is_gt(a):
2322  """Return `True` if `a` is an expression of the form b > c.
2323
2324  >>> x, y = Ints('x y')
2325  >>> is_gt(x > y)
2326  True
2327  >>> is_gt(x == y)
2328  False
2329  """
2330  return is_app_of(a, Z3_OP_GT)
2331
2332 def is_is_int(a):
2333  """Return `True` if `a` is an expression of the form IsInt(b).
2334
2335  >>> x = Real('x')
2336  >>> is_is_int(IsInt(x))
2337  True
2338  >>> is_is_int(x)
2339  False
2340  """
2341  return is_app_of(a, Z3_OP_IS_INT)
2342
2343 def is_to_real(a):
2344  """Return `True` if `a` is an expression of the form ToReal(b).
2345
2346  >>> x = Int('x')
2347  >>> n = ToReal(x)
2348  >>> n
2349  ToReal(x)
2350  >>> is_to_real(n)
2351  True
2352  >>> is_to_real(x)
2353  False
2354  """
2355  return is_app_of(a, Z3_OP_TO_REAL)
2356
2357 def is_to_int(a):
2358  """Return `True` if `a` is an expression of the form ToInt(b).
2359
2360  >>> x = Real('x')
2361  >>> n = ToInt(x)
2362  >>> n
2363  ToInt(x)
2364  >>> is_to_int(n)
2365  True
2366  >>> is_to_int(x)
2367  False
2368  """
2369  return is_app_of(a, Z3_OP_TO_INT)
2370
2371 class IntNumRef(ArithRef):
2372  """Integer values."""
2373
2374  def as_long(self):
2375  """Return a Z3 integer numeral as a Python long (bignum) numeral.
2376
2377  >>> v = IntVal(1)
2378  >>> v + 1
2379  1 + 1
2380  >>> v.as_long() + 1
2381  2L
2382  """
2383  if __debug__:
2384  _z3_assert(self.is_int(), "Integer value expected")
2385  return long(self.as_string())
2386
2387  def as_string(self):
2388  """Return a Z3 integer numeral as a Python string.
2389  >>> v = IntVal(100)
2390  >>> v.as_string()
2391  '100'
2392  """
2393  return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
2394
2395 class RatNumRef(ArithRef):
2396  """Rational values."""
2397
2398  def numerator(self):
2399  """ Return the numerator of a Z3 rational numeral.
2400
2401  >>> is_rational_value(RealVal("3/5"))
2402  True
2403  >>> n = RealVal("3/5")
2404  >>> n.numerator()
2405  3
2406  >>> is_rational_value(Q(3,5))
2407  True
2408  >>> Q(3,5).numerator()
2409  3
2410  """
2411  return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
2412
2413  def denominator(self):
2414  """ Return the denominator of a Z3 rational numeral.
2415
2416  >>> is_rational_value(Q(3,5))
2417  True
2418  >>> n = Q(3,5)
2419  >>> n.denominator()
2420  5
2421  """
2422  return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
2423
2424  def numerator_as_long(self):
2425  """ Return the numerator as a Python long.
2426
2427  >>> v = RealVal(10000000000)
2428  >>> v
2429  10000000000
2430  >>> v + 1
2431  10000000000 + 1
2432  >>> v.numerator_as_long() + 1
2433  10000000001L
2434  """
2435  return self.numerator().as_long()
2436
2437  def denominator_as_long(self):
2438  """ Return the denominator as a Python long.
2439
2440  >>> v = RealVal("1/3")
2441  >>> v
2442  1/3
2443  >>> v.denominator_as_long()
2444  3L
2445  """
2446  return self.denominator().as_long()
2447
2448  def as_decimal(self, prec):
2449  """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
2450
2451  >>> v = RealVal("1/5")
2452  >>> v.as_decimal(3)
2453  '0.2'
2454  >>> v = RealVal("1/3")
2455  >>> v.as_decimal(3)
2456  '0.333?'
2457  """
2458  return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
2459
2460  def as_string(self):
2461  """Return a Z3 rational numeral as a Python string.
2462
2463  >>> v = Q(3,6)
2464  >>> v.as_string()
2465  '1/2'
2466  """
2467  return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
2468
2469 class AlgebraicNumRef(ArithRef):
2470  """Algebraic irrational values."""
2471
2472  def approx(self, precision=10):
2473  """Return a Z3 rational number that approximates the algebraic number `self`.
2474  The result `r` is such that |r - self| <= 1/10^precision
2475
2476  >>> x = simplify(Sqrt(2))
2477  >>> x.approx(20)
2478  6838717160008073720548335/4835703278458516698824704
2479  >>> x.approx(5)
2480  2965821/2097152
2481  """
2482  return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
2483  def as_decimal(self, prec):
2484  """Return a string representation of the algebraic number `self` in decimal notation using `prec` decimal places
2485
2486  >>> x = simplify(Sqrt(2))
2487  >>> x.as_decimal(10)
2488  '1.4142135623?'
2489  >>> x.as_decimal(20)
2490  '1.41421356237309504880?'
2491  """
2492  return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
2493
2494 def _py2expr(a, ctx=None):
2495  if isinstance(a, bool):
2496  return BoolVal(a, ctx)
2497  if isinstance(a, int) or isinstance(a, long):
2498  return IntVal(a, ctx)
2499  if isinstance(a, float):
2500  return RealVal(a, ctx)
2501  if __debug__:
2502  _z3_assert(False, "Python bool, int, long or float expected")
2503
2504 def IntSort(ctx=None):
2505  """Return the interger sort in the given context. If `ctx=None`, then the global context is used.
2506
2507  >>> IntSort()
2508  Int
2509  >>> x = Const('x', IntSort())
2510  >>> is_int(x)
2511  True
2512  >>> x.sort() == IntSort()
2513  True
2514  >>> x.sort() == BoolSort()
2515  False
2516  """
2517  ctx = _get_ctx(ctx)
2518  return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
2519
2520 def RealSort(ctx=None):
2521  """Return the real sort in the given context. If `ctx=None`, then the global context is used.
2522
2523  >>> RealSort()
2524  Real
2525  >>> x = Const('x', RealSort())
2526  >>> is_real(x)
2527  True
2528  >>> is_int(x)
2529  False
2530  >>> x.sort() == RealSort()
2531  True
2532  """
2533  ctx = _get_ctx(ctx)
2534  return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)
2535
2536 def _to_int_str(val):
2537  if isinstance(val, float):
2538  return str(int(val))
2539  elif isinstance(val, bool):
2540  if val:
2541  return "1"
2542  else:
2543  return "0"
2544  elif isinstance(val, int):
2545  return str(val)
2546  elif isinstance(val, long):
2547  return str(val)
2548  elif isinstance(val, str):
2549  return val
2550  if __debug__:
2551  _z3_assert(False, "Python value cannot be used as a Z3 integer")
2552
2553 def IntVal(val, ctx=None):
2554  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
2555
2556  >>> IntVal(1)
2557  1
2558  >>> IntVal("100")
2559  100
2560  """
2561  ctx = _get_ctx(ctx)
2562  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
2563
2564 def RealVal(val, ctx=None):
2565  """Return a Z3 real value.
2566
2567  `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
2568  If `ctx=None`, then the global context is used.
2569
2570  >>> RealVal(1)
2571  1
2572  >>> RealVal(1).sort()
2573  Real
2574  >>> RealVal("3/5")
2575  3/5
2576  >>> RealVal("1.5")
2577  3/2
2578  """
2579  ctx = _get_ctx(ctx)
2580  return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
2581
2582 def RatVal(a, b, ctx=None):
2583  """Return a Z3 rational a/b.
2584
2585  If `ctx=None`, then the global context is used.
2586
2587  >>> RatVal(3,5)
2588  3/5
2589  >>> RatVal(3,5).sort()
2590  Real
2591  """
2592  if __debug__:
2593  _z3_assert(isinstance(a, int) or isinstance(a, str) or isinstance(a, long), "First argument cannot be converted into an integer")
2594  _z3_assert(isinstance(b, int) or isinstance(b, str) or isinstance(a, long), "Second argument cannot be converted into an integer")
2595  return simplify(RealVal(a, ctx)/RealVal(b, ctx))
2596
2597 def Q(a, b, ctx=None):
2598  """Return a Z3 rational a/b.
2599
2600  If `ctx=None`, then the global context is used.
2601
2602  >>> Q(3,5)
2603  3/5
2604  >>> Q(3,5).sort()
2605  Real
2606  """
2607  return simplify(RatVal(a, b))
2608
2609 def Int(name, ctx=None):
2610  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
2611
2612  >>> x = Int('x')
2613  >>> is_int(x)
2614  True
2615  >>> is_int(x + 1)
2616  True
2617  """
2618  ctx = _get_ctx(ctx)
2619  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
2620
2621 def Ints(names, ctx=None):
2622  """Return a tuple of Integer constants.
2623
2624  >>> x, y, z = Ints('x y z')
2625  >>> Sum(x, y, z)
2626  x + y + z
2627  """
2628  ctx = _get_ctx(ctx)
2629  if isinstance(names, str):
2630  names = names.split(" ")
2631  return [Int(name, ctx) for name in names]
2632
2633 def IntVector(prefix, sz, ctx=None):
2634  """Return a list of integer constants of size `sz`.
2635
2636  >>> X = IntVector('x', 3)
2637  >>> X
2638  [x__0, x__1, x__2]
2639  >>> Sum(X)
2640  x__0 + x__1 + x__2
2641  """
2642  return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ]
2643
2644 def FreshInt(prefix='x', ctx=None):
2645  """Return a fresh integer constant in the given context using the given prefix.
2646
2647  >>> x = FreshInt()
2648  >>> y = FreshInt()
2649  >>> eq(x, y)
2650  False
2651  >>> x.sort()
2652  Int
2653  """
2654  ctx = _get_ctx(ctx)
2655  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
2656
2657 def Real(name, ctx=None):
2658  """Return a real constant named `name`. If `ctx=None`, then the global context is used.
2659
2660  >>> x = Real('x')
2661  >>> is_real(x)
2662  True
2663  >>> is_real(x + 1)
2664  True
2665  """
2666  ctx = _get_ctx(ctx)
2667  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)
2668
2669 def Reals(names, ctx=None):
2670  """Return a tuple of real constants.
2671
2672  >>> x, y, z = Reals('x y z')
2673  >>> Sum(x, y, z)
2674  x + y + z
2675  >>> Sum(x, y, z).sort()
2676  Real
2677  """
2678  ctx = _get_ctx(ctx)
2679  if isinstance(names, str):
2680  names = names.split(" ")
2681  return [Real(name, ctx) for name in names]
2682
2683 def RealVector(prefix, sz, ctx=None):
2684  """Return a list of real constants of size `sz`.
2685
2686  >>> X = RealVector('x', 3)
2687  >>> X
2688  [x__0, x__1, x__2]
2689  >>> Sum(X)
2690  x__0 + x__1 + x__2
2691  >>> Sum(X).sort()
2692  Real
2693  """
2694  return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ]
2695
2696 def FreshReal(prefix='b', ctx=None):
2697  """Return a fresh real constant in the given context using the given prefix.
2698
2699  >>> x = FreshReal()
2700  >>> y = FreshReal()
2701  >>> eq(x, y)
2702  False
2703  >>> x.sort()
2704  Real
2705  """
2706  ctx = _get_ctx(ctx)
2707  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
2708
2709 def ToReal(a):
2710  """ Return the Z3 expression ToReal(a).
2711
2712  >>> x = Int('x')
2713  >>> x.sort()
2714  Int
2715  >>> n = ToReal(x)
2716  >>> n
2717  ToReal(x)
2718  >>> n.sort()
2719  Real
2720  """
2721  if __debug__:
2722  _z3_assert(a.is_int(), "Z3 integer expression expected.")
2723  ctx = a.ctx
2724  return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
2725
2726 def ToInt(a):
2727  """ Return the Z3 expression ToInt(a).
2728
2729  >>> x = Real('x')
2730  >>> x.sort()
2731  Real
2732  >>> n = ToInt(x)
2733  >>> n
2734  ToInt(x)
2735  >>> n.sort()
2736  Int
2737  """
2738  if __debug__:
2739  _z3_assert(a.is_real(), "Z3 real expression expected.")
2740  ctx = a.ctx
2741  return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)
2742
2743 def IsInt(a):
2744  """ Return the Z3 predicate IsInt(a).
2745
2746  >>> x = Real('x')
2747  >>> IsInt(x + "1/2")
2748  IsInt(x + 1/2)
2749  >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
2750  [x = 1/2]
2751  >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
2752  no solution
2753  """
2754  if __debug__:
2755  _z3_assert(a.is_real(), "Z3 real expression expected.")
2756  ctx = a.ctx
2757  return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
2758
2759 def Sqrt(a, ctx=None):
2760  """ Return a Z3 expression which represents the square root of a.
2761
2762  >>> x = Real('x')
2763  >>> Sqrt(x)
2764  x**(1/2)
2765  """
2766  if not is_expr(a):
2767  ctx = _get_ctx(ctx)
2768  a = RealVal(a, ctx)
2769  return a ** "1/2"
2770
2771 def Cbrt(a, ctx=None):
2772  """ Return a Z3 expression which represents the cubic root of a.
2773
2774  >>> x = Real('x')
2775  >>> Cbrt(x)
2776  x**(1/3)
2777  """
2778  if not is_expr(a):
2779  ctx = _get_ctx(ctx)
2780  a = RealVal(a, ctx)
2781  return a ** "1/3"
2782
2783 #########################################
2784 #
2785 # Bit-Vectors
2786 #
2787 #########################################
2788
2789 class BitVecSortRef(SortRef):
2790  """Bit-vector sort."""
2791
2792  def size(self):
2793  """Return the size (number of bits) of the bit-vector sort `self`.
2794
2795  >>> b = BitVecSort(32)
2796  >>> b.size()
2797  32
2798  """
2799  return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast))
2800
2801  def subsort(self, other):
2802  return is_bv_sort(other) and self.size() < other.size()
2803
2804  def cast(self, val):
2805  """Try to cast `val` as a Bit-Vector.
2806
2807  >>> b = BitVecSort(32)
2808  >>> b.cast(10)
2809  10
2810  >>> b.cast(10).sexpr()
2811  '#x0000000a'
2812  """
2813  if is_expr(val):
2814  if __debug__:
2815  _z3_assert(self.ctx == val.ctx, "Context mismatch")
2816  # Idea: use sign_extend if sort of val is a bitvector of smaller size
2817  return val
2818  else:
2819  return BitVecVal(val, self)
2820
2821 def is_bv_sort(s):
2822  """Return True if `s` is a Z3 bit-vector sort.
2823
2824  >>> is_bv_sort(BitVecSort(32))
2825  True
2826  >>> is_bv_sort(IntSort())
2827  False
2828  """
2829  return isinstance(s, BitVecSortRef)
2830
2831 class BitVecRef(ExprRef):
2832  """Bit-vector expressions."""
2833
2834  def sort(self):
2835  """Return the sort of the bit-vector expression `self`.
2836
2837  >>> x = BitVec('x', 32)
2838  >>> x.sort()
2839  BitVec(32)
2840  >>> x.sort() == BitVecSort(32)
2841  True
2842  """
2843  return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
2844
2845  def size(self):
2846  """Return the number of bits of the bit-vector expression `self`.
2847
2848  >>> x = BitVec('x', 32)
2849  >>> (x + 1).size()
2850  32
2851  >>> Concat(x, x).size()
2852  64
2853  """
2854  return self.sort().size()
2855
2857  """Create the Z3 expression `self + other`.
2858
2859  >>> x = BitVec('x', 32)
2860  >>> y = BitVec('y', 32)
2861  >>> x + y
2862  x + y
2863  >>> (x + y).sort()
2864  BitVec(32)
2865  """
2866  a, b = _coerce_exprs(self, other)
2867  return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2868
2870  """Create the Z3 expression `other + self`.
2871
2872  >>> x = BitVec('x', 32)
2873  >>> 10 + x
2874  10 + x
2875  """
2876  a, b = _coerce_exprs(self, other)
2877  return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2878
2879  def __mul__(self, other):
2880  """Create the Z3 expression `self * other`.
2881
2882  >>> x = BitVec('x', 32)
2883  >>> y = BitVec('y', 32)
2884  >>> x * y
2885  x*y
2886  >>> (x * y).sort()
2887  BitVec(32)
2888  """
2889  a, b = _coerce_exprs(self, other)
2890  return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2891
2892  def __rmul__(self, other):
2893  """Create the Z3 expression `other * self`.
2894
2895  >>> x = BitVec('x', 32)
2896  >>> 10 * x
2897  10*x
2898  """
2899  a, b = _coerce_exprs(self, other)
2900  return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2901
2902  def __sub__(self, other):
2903  """Create the Z3 expression `self - other`.
2904
2905  >>> x = BitVec('x', 32)
2906  >>> y = BitVec('y', 32)
2907  >>> x - y
2908  x - y
2909  >>> (x - y).sort()
2910  BitVec(32)
2911  """
2912  a, b = _coerce_exprs(self, other)
2913  return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2914
2915  def __rsub__(self, other):
2916  """Create the Z3 expression `other - self`.
2917
2918  >>> x = BitVec('x', 32)
2919  >>> 10 - x
2920  10 - x
2921  """
2922  a, b = _coerce_exprs(self, other)
2923  return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2924
2925  def __or__(self, other):
2926  """Create the Z3 expression bitwise-or `self | other`.
2927
2928  >>> x = BitVec('x', 32)
2929  >>> y = BitVec('y', 32)
2930  >>> x | y
2931  x | y
2932  >>> (x | y).sort()
2933  BitVec(32)
2934  """
2935  a, b = _coerce_exprs(self, other)
2936  return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2937
2938  def __ror__(self, other):
2939  """Create the Z3 expression bitwise-or `other | self`.
2940
2941  >>> x = BitVec('x', 32)
2942  >>> 10 | x
2943  10 | x
2944  """
2945  a, b = _coerce_exprs(self, other)
2946  return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2947
2948  def __and__(self, other):
2949  """Create the Z3 expression bitwise-and `self & other`.
2950
2951  >>> x = BitVec('x', 32)
2952  >>> y = BitVec('y', 32)
2953  >>> x & y
2954  x & y
2955  >>> (x & y).sort()
2956  BitVec(32)
2957  """
2958  a, b = _coerce_exprs(self, other)
2959  return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2960
2961  def __rand__(self, other):
2962  """Create the Z3 expression bitwise-or `other & self`.
2963
2964  >>> x = BitVec('x', 32)
2965  >>> 10 & x
2966  10 & x
2967  """
2968  a, b = _coerce_exprs(self, other)
2969  return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2970
2971  def __xor__(self, other):
2972  """Create the Z3 expression bitwise-xor `self ^ other`.
2973
2974  >>> x = BitVec('x', 32)
2975  >>> y = BitVec('y', 32)
2976  >>> x ^ y
2977  x ^ y
2978  >>> (x ^ y).sort()
2979  BitVec(32)
2980  """
2981  a, b = _coerce_exprs(self, other)
2982  return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2983
2984  def __rxor__(self, other):
2985  """Create the Z3 expression bitwise-xor `other ^ self`.
2986
2987  >>> x = BitVec('x', 32)
2988  >>> 10 ^ x
2989  10 ^ x
2990  """
2991  a, b = _coerce_exprs(self, other)
2992  return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2993
2994  def __pos__(self):
2995  """Return `self`.
2996
2997  >>> x = BitVec('x', 32)
2998  >>> +x
2999  x
3000  """
3001  return self
3002
3003  def __neg__(self):
3004  """Return an expression representing `-self`.
3005
3006  >>> x = BitVec('x', 32)
3007  >>> -x
3008  -x
3009  >>> simplify(-(-x))
3010  x
3011  """
3012  return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx)
3013
3014  def __invert__(self):
3015  """Create the Z3 expression bitwise-not `~self`.
3016
3017  >>> x = BitVec('x', 32)
3018  >>> ~x
3019  ~x
3020  >>> simplify(~(~x))
3021  x
3022  """
3023  return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx)
3024
3025  def __div__(self, other):
3026  """Create the Z3 expression (signed) division `self / other`.
3027
3028  Use the function UDiv() for unsigned division.
3029
3030  >>> x = BitVec('x', 32)
3031  >>> y = BitVec('y', 32)
3032  >>> x / y
3033  x/y
3034  >>> (x / y).sort()
3035  BitVec(32)
3036  >>> (x / y).sexpr()
3037  '(bvsdiv x y)'
3038  >>> UDiv(x, y).sexpr()
3039  '(bvudiv x y)'
3040  """
3041  a, b = _coerce_exprs(self, other)
3042  return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3043
3044  def __truediv__(self, other):
3045  """Create the Z3 expression (signed) division `self / other`."""
3046  self.__div__(other)
3047
3048  def __rdiv__(self, other):
3049  """Create the Z3 expression (signed) division `other / self`.
3050
3051  Use the function UDiv() for unsigned division.
3052
3053  >>> x = BitVec('x', 32)
3054  >>> 10 / x
3055  10/x
3056  >>> (10 / x).sexpr()
3057  '(bvsdiv #x0000000a x)'
3058  >>> UDiv(10, x).sexpr()
3059  '(bvudiv #x0000000a x)'
3060  """
3061  a, b = _coerce_exprs(self, other)
3062  return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3063
3064  def __rtruediv__(self, other):
3065  """Create the Z3 expression (signed) division `other / self`."""
3066  self.__rdiv__(other)
3067
3068  def __mod__(self, other):
3069  """Create the Z3 expression (signed) mod `self % other`.
3070
3071  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3072
3073  >>> x = BitVec('x', 32)
3074  >>> y = BitVec('y', 32)
3075  >>> x % y
3076  x%y
3077  >>> (x % y).sort()
3078  BitVec(32)
3079  >>> (x % y).sexpr()
3080  '(bvsmod x y)'
3081  >>> URem(x, y).sexpr()
3082  '(bvurem x y)'
3083  >>> SRem(x, y).sexpr()
3084  '(bvsrem x y)'
3085  """
3086  a, b = _coerce_exprs(self, other)
3087  return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3088
3089  def __rmod__(self, other):
3090  """Create the Z3 expression (signed) mod `other % self`.
3091
3092  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3093
3094  >>> x = BitVec('x', 32)
3095  >>> 10 % x
3096  10%x
3097  >>> (10 % x).sexpr()
3098  '(bvsmod #x0000000a x)'
3099  >>> URem(10, x).sexpr()
3100  '(bvurem #x0000000a x)'
3101  >>> SRem(10, x).sexpr()
3102  '(bvsrem #x0000000a x)'
3103  """
3104  a, b = _coerce_exprs(self, other)
3105  return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3106
3107  def __le__(self, other):
3108  """Create the Z3 expression (signed) `other <= self`.
3109
3110  Use the function ULE() for unsigned less than or equal to.
3111
3112  >>> x, y = BitVecs('x y', 32)
3113  >>> x <= y
3114  x <= y
3115  >>> (x <= y).sexpr()
3116  '(bvsle x y)'
3117  >>> ULE(x, y).sexpr()
3118  '(bvule x y)'
3119  """
3120  a, b = _coerce_exprs(self, other)
3121  return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3122
3123  def __lt__(self, other):
3124  """Create the Z3 expression (signed) `other < self`.
3125
3126  Use the function ULT() for unsigned less than.
3127
3128  >>> x, y = BitVecs('x y', 32)
3129  >>> x < y
3130  x < y
3131  >>> (x < y).sexpr()
3132  '(bvslt x y)'
3133  >>> ULT(x, y).sexpr()
3134  '(bvult x y)'
3135  """
3136  a, b = _coerce_exprs(self, other)
3137  return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3138
3139  def __gt__(self, other):
3140  """Create the Z3 expression (signed) `other > self`.
3141
3142  Use the function UGT() for unsigned greater than.
3143
3144  >>> x, y = BitVecs('x y', 32)
3145  >>> x > y
3146  x > y
3147  >>> (x > y).sexpr()
3148  '(bvsgt x y)'
3149  >>> UGT(x, y).sexpr()
3150  '(bvugt x y)'
3151  """
3152  a, b = _coerce_exprs(self, other)
3153  return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3154
3155  def __ge__(self, other):
3156  """Create the Z3 expression (signed) `other >= self`.
3157
3158  Use the function UGE() for unsigned greater than or equal to.
3159
3160  >>> x, y = BitVecs('x y', 32)
3161  >>> x >= y
3162  x >= y
3163  >>> (x >= y).sexpr()
3164  '(bvsge x y)'
3165  >>> UGE(x, y).sexpr()
3166  '(bvuge x y)'
3167  """
3168  a, b = _coerce_exprs(self, other)
3169  return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3170
3171  def __rshift__(self, other):
3172  """Create the Z3 expression (arithmetical) right shift `self >> other`
3173
3174  Use the function LShR() for the right logical shift
3175
3176  >>> x, y = BitVecs('x y', 32)
3177  >>> x >> y
3178  x >> y
3179  >>> (x >> y).sexpr()
3180  '(bvashr x y)'
3181  >>> LShR(x, y).sexpr()
3182  '(bvlshr x y)'
3183  >>> BitVecVal(4, 3)
3184  4
3185  >>> BitVecVal(4, 3).as_signed_long()
3186  -4L
3187  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3188  -2L
3189  >>> simplify(BitVecVal(4, 3) >> 1)
3190  6
3191  >>> simplify(LShR(BitVecVal(4, 3), 1))
3192  2
3193  >>> simplify(BitVecVal(2, 3) >> 1)
3194  1
3195  >>> simplify(LShR(BitVecVal(2, 3), 1))
3196  1
3197  """
3198  a, b = _coerce_exprs(self, other)
3199  return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3200
3201  def __lshift__(self, other):
3202  """Create the Z3 expression left shift `self << other`
3203
3204  >>> x, y = BitVecs('x y', 32)
3205  >>> x << y
3206  x << y
3207  >>> (x << y).sexpr()
3208  '(bvshl x y)'
3209  >>> simplify(BitVecVal(2, 3) << 1)
3210  4
3211  """
3212  a, b = _coerce_exprs(self, other)
3213  return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3214
3215  def __rrshift__(self, other):
3216  """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3217
3218  Use the function LShR() for the right logical shift
3219
3220  >>> x = BitVec('x', 32)
3221  >>> 10 >> x
3222  10 >> x
3223  >>> (10 >> x).sexpr()
3224  '(bvashr #x0000000a x)'
3225  """
3226  a, b = _coerce_exprs(self, other)
3227  return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3228
3229  def __rlshift__(self, other):
3230  """Create the Z3 expression left shift `other << self`.
3231
3232  Use the function LShR() for the right logical shift
3233
3234  >>> x = BitVec('x', 32)
3235  >>> 10 << x
3236  10 << x
3237  >>> (10 << x).sexpr()
3238  '(bvshl #x0000000a x)'
3239  """
3240  a, b = _coerce_exprs(self, other)
3241  return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3242
3243 class BitVecNumRef(BitVecRef):
3244  """Bit-vector values."""
3245
3246  def as_long(self):
3247  """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
3248
3249  >>> v = BitVecVal(0xbadc0de, 32)
3250  >>> v
3251  195936478
3252  >>> print "0x%.8x" % v.as_long()
3254  """
3255  return long(self.as_string())
3256
3257  def as_signed_long(self):
3258  """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign.
3259
3260  >>> BitVecVal(4, 3).as_signed_long()
3261  -4L
3262  >>> BitVecVal(7, 3).as_signed_long()
3263  -1L
3264  >>> BitVecVal(3, 3).as_signed_long()
3265  3L
3266  >>> BitVecVal(2L**32 - 1, 32).as_signed_long()
3267  -1L
3268  >>> BitVecVal(2L**64 - 1, 64).as_signed_long()
3269  -1L
3270  """
3271  sz = long(self.size())
3272  val = self.as_long()
3273  if val >= 2L**(sz - 1):
3274  val = val - 2L**sz
3275  if val < -2L**(sz - 1):
3276  val = val + 2L**sz
3277  return val
3278
3279  def as_string(self):
3280  return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
3281
3282 def is_bv(a):
3283  """Return `True` if `a` is a Z3 bit-vector expression.
3284
3285  >>> b = BitVec('b', 32)
3286  >>> is_bv(b)
3287  True
3288  >>> is_bv(b + 10)
3289  True
3290  >>> is_bv(Int('x'))
3291  False
3292  """
3293  return isinstance(a, BitVecRef)
3294
3295 def is_bv_value(a):
3296  """Return `True` if `a` is a Z3 bit-vector numeral value.
3297
3298  >>> b = BitVec('b', 32)
3299  >>> is_bv_value(b)
3300  False
3301  >>> b = BitVecVal(10, 32)
3302  >>> b
3303  10
3304  >>> is_bv_value(b)
3305  True
3306  """
3307  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3308
3309 def BV2Int(a):
3310  """Return the Z3 expression BV2Int(a).
3311
3312  >>> b = BitVec('b', 3)
3313  >>> BV2Int(b).sort()
3314  Int
3315  >>> x = Int('x')
3316  >>> x > BV2Int(b)
3317  x > BV2Int(b)
3318  >>> solve(x > BV2Int(b), b == 1, x < 3)
3319  [b = 1, x = 2]
3320  """
3321  if __debug__:
3322  _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
3323  ctx = a.ctx
3324  ## investigate problem with bv2int
3325  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)
3326
3327 def BitVecSort(sz, ctx=None):
3328  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3329
3330  >>> Byte = BitVecSort(8)
3331  >>> Word = BitVecSort(16)
3332  >>> Byte
3333  BitVec(8)
3334  >>> x = Const('x', Byte)
3335  >>> eq(x, BitVec('x', 8))
3336  True
3337  """
3338  ctx = _get_ctx(ctx)
3339  return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
3340
3341 def BitVecVal(val, bv, ctx=None):
3342  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3343
3344  >>> v = BitVecVal(10, 32)
3345  >>> v
3346  10
3347  >>> print "0x%.8x" % v.as_long()
3348  0x0000000a
3349  """
3350  if is_bv_sort(bv):
3351  ctx = bv.ctx
3352  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3353  else:
3354  ctx = _get_ctx(ctx)
3355  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
3356
3357 def BitVec(name, bv, ctx=None):
3358  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3359  If `ctx=None`, then the global context is used.
3360
3361  >>> x = BitVec('x', 16)
3362  >>> is_bv(x)
3363  True
3364  >>> x.size()
3365  16
3366  >>> x.sort()
3367  BitVec(16)
3368  >>> word = BitVecSort(16)
3369  >>> x2 = BitVec('x', word)
3370  >>> eq(x, x2)
3371  True
3372  """
3373  if isinstance(bv, BitVecSortRef):
3374  ctx = bv.ctx
3375  else:
3376  ctx = _get_ctx(ctx)
3377  bv = BitVecSort(bv, ctx)
3378  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
3379
3380 def BitVecs(names, bv, ctx=None):
3381  """Return a tuple of bit-vector constants of size bv.
3382
3383  >>> x, y, z = BitVecs('x y z', 16)
3384  >>> x.size()
3385  16
3386  >>> x.sort()
3387  BitVec(16)
3388  >>> Sum(x, y, z)
3389  0 + x + y + z
3390  >>> Product(x, y, z)
3391  1*x*y*z
3392  >>> simplify(Product(x, y, z))
3393  x*y*z
3394  """
3395  ctx = _get_ctx(ctx)
3396  if isinstance(names, str):
3397  names = names.split(" ")
3398  return [BitVec(name, bv, ctx) for name in names]
3399
3400 def Concat(*args):
3401  """Create a Z3 bit-vector concatenation expression.
3402
3403  >>> v = BitVecVal(1, 4)
3404  >>> Concat(v, v+1, v)
3405  Concat(Concat(1, 1 + 1), 1)
3406  >>> simplify(Concat(v, v+1, v))
3407  289
3408  >>> print "%.3x" % simplify(Concat(v, v+1, v)).as_long()
3409  121
3410  """
3411  args = _get_args(args)
3412  if __debug__:
3413  _z3_assert(all(map(is_bv, args)), "All arguments must be Z3 bit-vector expressions.")
3414  _z3_assert(len(args) >= 2, "At least two arguments expected.")
3415  ctx = args[0].ctx
3416  r = args[0]
3417  for i in range(len(args) - 1):
3418  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
3419  return r
3420
3421 def Extract(high, low, a):
3422  """Create a Z3 bit-vector extraction expression.
3423
3424  >>> x = BitVec('x', 8)
3425  >>> Extract(6, 2, x)
3426  Extract(6, 2, x)
3427  >>> Extract(6, 2, x).sort()
3428  BitVec(5)
3429  """
3430  if __debug__:
3431  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
3432  _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
3433  _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
3434  return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
3435
3436 def _check_bv_args(a, b):
3437  if __debug__:
3438  _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression")
3439
3440 def ULE(a, b):
3441  """Create the Z3 expression (unsigned) `other <= self`.
3442
3443  Use the operator <= for signed less than or equal to.
3444
3445  >>> x, y = BitVecs('x y', 32)
3446  >>> ULE(x, y)
3447  ULE(x, y)
3448  >>> (x <= y).sexpr()
3449  '(bvsle x y)'
3450  >>> ULE(x, y).sexpr()
3451  '(bvule x y)'
3452  """
3453  _check_bv_args(a, b)
3454  a, b = _coerce_exprs(a, b)
3455  return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3456
3457 def ULT(a, b):
3458  """Create the Z3 expression (unsigned) `other < self`.
3459
3460  Use the operator < for signed less than.
3461
3462  >>> x, y = BitVecs('x y', 32)
3463  >>> ULT(x, y)
3464  ULT(x, y)
3465  >>> (x < y).sexpr()
3466  '(bvslt x y)'
3467  >>> ULT(x, y).sexpr()
3468  '(bvult x y)'
3469  """
3470  _check_bv_args(a, b)
3471  a, b = _coerce_exprs(a, b)
3472  return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3473
3474 def UGE(a, b):
3475  """Create the Z3 expression (unsigned) `other >= self`.
3476
3477  Use the operator >= for signed greater than or equal to.
3478
3479  >>> x, y = BitVecs('x y', 32)
3480  >>> UGE(x, y)
3481  UGE(x, y)
3482  >>> (x >= y).sexpr()
3483  '(bvsge x y)'
3484  >>> UGE(x, y).sexpr()
3485  '(bvuge x y)'
3486  """
3487  _check_bv_args(a, b)
3488  a, b = _coerce_exprs(a, b)
3489  return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3490
3491 def UGT(a, b):
3492  """Create the Z3 expression (unsigned) `other > self`.
3493
3494  Use the operator > for signed greater than.
3495
3496  >>> x, y = BitVecs('x y', 32)
3497  >>> UGT(x, y)
3498  UGT(x, y)
3499  >>> (x > y).sexpr()
3500  '(bvsgt x y)'
3501  >>> UGT(x, y).sexpr()
3502  '(bvugt x y)'
3503  """
3504  _check_bv_args(a, b)
3505  a, b = _coerce_exprs(a, b)
3506  return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3507
3508 def UDiv(a, b):
3509  """Create the Z3 expression (unsigned) division `self / other`.
3510
3511  Use the operator / for signed division.
3512
3513  >>> x = BitVec('x', 32)
3514  >>> y = BitVec('y', 32)
3515  >>> UDiv(x, y)
3516  UDiv(x, y)
3517  >>> UDiv(x, y).sort()
3518  BitVec(32)
3519  >>> (x / y).sexpr()
3520  '(bvsdiv x y)'
3521  >>> UDiv(x, y).sexpr()
3522  '(bvudiv x y)'
3523  """
3524  _check_bv_args(a, b)
3525  a, b = _coerce_exprs(a, b)
3526  return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3527
3528 def URem(a, b):
3529  """Create the Z3 expression (unsigned) remainder `self % other`.
3530
3531  Use the operator % for signed modulus, and SRem() for signed remainder.
3532
3533  >>> x = BitVec('x', 32)
3534  >>> y = BitVec('y', 32)
3535  >>> URem(x, y)
3536  URem(x, y)
3537  >>> URem(x, y).sort()
3538  BitVec(32)
3539  >>> (x % y).sexpr()
3540  '(bvsmod x y)'
3541  >>> URem(x, y).sexpr()
3542  '(bvurem x y)'
3543  """
3544  _check_bv_args(a, b)
3545  a, b = _coerce_exprs(a, b)
3546  return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3547
3548 def SRem(a, b):
3549  """Create the Z3 expression signed remainder.
3550
3551  Use the operator % for signed modulus, and URem() for unsigned remainder.
3552
3553  >>> x = BitVec('x', 32)
3554  >>> y = BitVec('y', 32)
3555  >>> SRem(x, y)
3556  SRem(x, y)
3557  >>> SRem(x, y).sort()
3558  BitVec(32)
3559  >>> (x % y).sexpr()
3560  '(bvsmod x y)'
3561  >>> SRem(x, y).sexpr()
3562  '(bvsrem x y)'
3563  """
3564  _check_bv_args(a, b)
3565  a, b = _coerce_exprs(a, b)
3566  return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3567
3568 def LShR(a, b):
3569  """Create the Z3 expression logical right shift.
3570
3571  Use the operator >> for the arithmetical right shift.
3572
3573  >>> x, y = BitVecs('x y', 32)
3574  >>> LShR(x, y)
3575  LShR(x, y)
3576  >>> (x >> y).sexpr()
3577  '(bvashr x y)'
3578  >>> LShR(x, y).sexpr()
3579  '(bvlshr x y)'
3580  >>> BitVecVal(4, 3)
3581  4
3582  >>> BitVecVal(4, 3).as_signed_long()
3583  -4L
3584  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3585  -2L
3586  >>> simplify(BitVecVal(4, 3) >> 1)
3587  6
3588  >>> simplify(LShR(BitVecVal(4, 3), 1))
3589  2
3590  >>> simplify(BitVecVal(2, 3) >> 1)
3591  1
3592  >>> simplify(LShR(BitVecVal(2, 3), 1))
3593  1
3594  """
3595  _check_bv_args(a, b)
3596  a, b = _coerce_exprs(a, b)
3597  return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3598
3599 def RotateLeft(a, b):
3600  """Return an expression representing `a` rotated to the left `b` times.
3601
3602  >>> a, b = BitVecs('a b', 16)
3603  >>> RotateLeft(a, b)
3604  RotateLeft(a, b)
3605  >>> simplify(RotateLeft(a, 0))
3606  a
3607  >>> simplify(RotateLeft(a, 16))
3608  a
3609  """
3610  _check_bv_args(a, b)
3611  a, b = _coerce_exprs(a, b)
3612  return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3613
3614 def RotateRight(a, b):
3615  """Return an expression representing `a` rotated to the right `b` times.
3616
3617  >>> a, b = BitVecs('a b', 16)
3618  >>> RotateRight(a, b)
3619  RotateRight(a, b)
3620  >>> simplify(RotateRight(a, 0))
3621  a
3622  >>> simplify(RotateRight(a, 16))
3623  a
3624  """
3625  _check_bv_args(a, b)
3626  a, b = _coerce_exprs(a, b)
3627  return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3628
3629 def SignExt(n, a):
3630  """Return a bit-vector expression with `n` extra sign-bits.
3631
3632  >>> x = BitVec('x', 16)
3633  >>> n = SignExt(8, x)
3634  >>> n.size()
3635  24
3636  >>> n
3637  SignExt(8, x)
3638  >>> n.sort()
3639  BitVec(24)
3640  >>> v0 = BitVecVal(2, 2)
3641  >>> v0
3642  2
3643  >>> v0.size()
3644  2
3645  >>> v = simplify(SignExt(6, v0))
3646  >>> v
3647  254
3648  >>> v.size()
3649  8
3650  >>> print "%.x" % v.as_long()
3651  fe
3652  """
3653  if __debug__:
3654  _z3_assert(isinstance(n, int), "First argument must be an integer")
3655  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3656  return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
3657
3658 def ZeroExt(n, a):
3659  """Return a bit-vector expression with `n` extra zero-bits.
3660
3661  >>> x = BitVec('x', 16)
3662  >>> n = ZeroExt(8, x)
3663  >>> n.size()
3664  24
3665  >>> n
3666  ZeroExt(8, x)
3667  >>> n.sort()
3668  BitVec(24)
3669  >>> v0 = BitVecVal(2, 2)
3670  >>> v0
3671  2
3672  >>> v0.size()
3673  2
3674  >>> v = simplify(ZeroExt(6, v0))
3675  >>> v
3676  2
3677  >>> v.size()
3678  8
3679  """
3680  if __debug__:
3681  _z3_assert(isinstance(n, int), "First argument must be an integer")
3682  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3683  return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
3684
3685 def RepeatBitVec(n, a):
3686  """Return an expression representing `n` copies of `a`.
3687
3688  >>> x = BitVec('x', 8)
3689  >>> n = RepeatBitVec(4, x)
3690  >>> n
3691  RepeatBitVec(4, x)
3692  >>> n.size()
3693  32
3694  >>> v0 = BitVecVal(10, 4)
3695  >>> print "%.x" % v0.as_long()
3696  a
3697  >>> v = simplify(RepeatBitVec(4, v0))
3698  >>> v.size()
3699  16
3700  >>> print "%.x" % v.as_long()
3701  aaaa
3702  """
3703  if __debug__:
3704  _z3_assert(isinstance(n, int), "First argument must be an integer")
3705  _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3706  return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
3707
3708 #########################################
3709 #
3710 # Arrays
3711 #
3712 #########################################
3713
3714 class ArraySortRef(SortRef):
3715  """Array sorts."""
3716
3717  def domain(self):
3718  """Return the domain of the array sort `self`.
3719
3720  >>> A = ArraySort(IntSort(), BoolSort())
3721  >>> A.domain()
3722  Int
3723  """
3724  return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx)
3725
3726  def range(self):
3727  """Return the range of the array sort `self`.
3728
3729  >>> A = ArraySort(IntSort(), BoolSort())
3730  >>> A.range()
3731  Bool
3732  """
3733  return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)
3734
3735 class ArrayRef(ExprRef):
3736  """Array expressions. """
3737
3738  def sort(self):
3739  """Return the array sort of the array expression `self`.
3740
3741  >>> a = Array('a', IntSort(), BoolSort())
3742  >>> a.sort()
3743  Array(Int, Bool)
3744  """
3745  return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
3746
3747  def domain(self):
3748  """Shorthand for `self.sort().domain()`.
3749
3750  >>> a = Array('a', IntSort(), BoolSort())
3751  >>> a.domain()
3752  Int
3753  """
3754  return self.sort().domain()
3755
3756  def range(self):
3757  """Shorthand for `self.sort().range()`.
3758
3759  >>> a = Array('a', IntSort(), BoolSort())
3760  >>> a.range()
3761  Bool
3762  """
3763  return self.sort().range()
3764
3765  def __getitem__(self, arg):
3766  """Return the Z3 expression `self[arg]`.
3767
3768  >>> a = Array('a', IntSort(), BoolSort())
3769  >>> i = Int('i')
3770  >>> a[i]
3771  a[i]
3772  >>> a[i].sexpr()
3773  '(select a i)'
3774  """
3775  arg = self.domain().cast(arg)
3776  return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
3777
3778 def is_array(a):
3779  """Return `True` if `a` is a Z3 array expression.
3780
3781  >>> a = Array('a', IntSort(), IntSort())
3782  >>> is_array(a)
3783  True
3784  >>> is_array(Store(a, 0, 1))
3785  True
3786  >>> is_array(a[0])
3787  False
3788  """
3789  return isinstance(a, ArrayRef)
3790
3791 def is_select(a):
3792  """Return `True` if `a` is a Z3 array select.
3793
3794  >>> a = Array('a', IntSort(), IntSort())
3795  >>> is_select(a)
3796  False
3797  >>> i = Int('i')
3798  >>> is_select(a[i])
3799  True
3800  """
3801  return is_app_of(a, Z3_OP_SELECT)
3802
3803 def is_store(a):
3804  """Return `True` if `a` is a Z3 array store.
3805
3806  >>> a = Array('a', IntSort(), IntSort())
3807  >>> is_store(a)
3808  False
3809  >>> i = Int('i')
3810  >>> is_store(a[i])
3811  False
3812  >>> is_store(Store(a, i, i + 1))
3813  True
3814  """
3815  return is_app_of(a, Z3_OP_STORE)
3816
3817 def is_const_array(a):
3818  """Return `True` if `a` is a Z3 constant array.
3819
3820  >>> a = K(IntSort(), 10)
3821  >>> is_const_array(a)
3822  True
3823  >>> a = Array('a', IntSort(), IntSort())
3824  >>> is_const_array(a)
3825  False
3826  """
3827  return is_app_of(a, Z3_OP_CONST_ARRAY)
3828
3829 def is_K(a):
3830  """Return `True` if `a` is a Z3 constant array.
3831
3832  >>> a = K(IntSort(), 10)
3833  >>> is_K(a)
3834  True
3835  >>> a = Array('a', IntSort(), IntSort())
3836  >>> is_K(a)
3837  False
3838  """
3839  return is_app_of(a, Z3_OP_CONST_ARRAY)
3840
3841 def is_map(a):
3842  """Return `True` if `a` is a Z3 map array expression.
3843
3844  >>> f = Function('f', IntSort(), IntSort())
3845  >>> b = Array('b', IntSort(), IntSort())
3846  >>> a = Map(f, b)
3847  >>> a
3848  Map(f, b)
3849  >>> is_map(a)
3850  True
3851  >>> is_map(b)
3852  False
3853  """
3854  return is_app_of(a, Z3_OP_ARRAY_MAP)
3855
3856 def get_map_func(a):
3857  """Return the function declaration associated with a Z3 map array expression.
3858
3859  >>> f = Function('f', IntSort(), IntSort())
3860  >>> b = Array('b', IntSort(), IntSort())
3861  >>> a = Map(f, b)
3862  >>> eq(f, get_map_func(a))
3863  True
3864  >>> get_map_func(a)
3865  f
3866  >>> get_map_func(a)(0)
3867  f(0)
3868  """
3869  if __debug__:
3870  _z3_assert(is_map(a), "Z3 array map expression expected.")
3871  return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
3872
3873 def ArraySort(d, r):
3874  """Return the Z3 array sort with the given domain and range sorts.
3875
3876  >>> A = ArraySort(IntSort(), BoolSort())
3877  >>> A
3878  Array(Int, Bool)
3879  >>> A.domain()
3880  Int
3881  >>> A.range()
3882  Bool
3883  >>> AA = ArraySort(IntSort(), A)
3884  >>> AA
3885  Array(Int, Array(Int, Bool))
3886  """
3887  if __debug__:
3888  _z3_assert(is_sort(d), "Z3 sort expected")
3889  _z3_assert(is_sort(r), "Z3 sort expected")
3890  _z3_assert(d.ctx == r.ctx, "Context mismatch")
3891  ctx = d.ctx
3892  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
3893
3894 def Array(name, dom, rng):
3895  """Return an array constant named `name` with the given domain and range sorts.
3896
3897  >>> a = Array('a', IntSort(), IntSort())
3898  >>> a.sort()
3899  Array(Int, Int)
3900  >>> a[0]
3901  a[0]
3902  """
3903  s = ArraySort(dom, rng)
3904  ctx = s.ctx
3905  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
3906
3907 def Update(a, i, v):
3908  """Return a Z3 store array expression.
3909
3910  >>> a = Array('a', IntSort(), IntSort())
3911  >>> i, v = Ints('i v')
3912  >>> s = Update(a, i, v)
3913  >>> s.sort()
3914  Array(Int, Int)
3915  >>> prove(s[i] == v)
3916  proved
3917  >>> j = Int('j')
3918  >>> prove(Implies(i != j, s[j] == a[j]))
3919  proved
3920  """
3921  if __debug__:
3922  _z3_assert(is_array(a), "First argument must be a Z3 array expression")
3923  i = a.domain().cast(i)
3924  v = a.range().cast(v)
3925  ctx = a.ctx
3926  return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
3927
3928 def Store(a, i, v):
3929  """Return a Z3 store array expression.
3930
3931  >>> a = Array('a', IntSort(), IntSort())
3932  >>> i, v = Ints('i v')
3933  >>> s = Store(a, i, v)
3934  >>> s.sort()
3935  Array(Int, Int)
3936  >>> prove(s[i] == v)
3937  proved
3938  >>> j = Int('j')
3939  >>> prove(Implies(i != j, s[j] == a[j]))
3940  proved
3941  """
3942  return Update(a, i, v)
3943
3944 def Select(a, i):
3945  """Return a Z3 select array expression.
3946
3947  >>> a = Array('a', IntSort(), IntSort())
3948  >>> i = Int('i')
3949  >>> Select(a, i)
3950  a[i]
3951  >>> eq(Select(a, i), a[i])
3952  True
3953  """
3954  if __debug__:
3955  _z3_assert(is_array(a), "First argument must be a Z3 array expression")
3956  return a[i]
3957
3958 def Map(f, *args):
3959  """Return a Z3 map array expression.
3960
3961  >>> f = Function('f', IntSort(), IntSort(), IntSort())
3962  >>> a1 = Array('a1', IntSort(), IntSort())
3963  >>> a2 = Array('a2', IntSort(), IntSort())
3964  >>> b = Map(f, a1, a2)
3965  >>> b
3966  Map(f, a1, a2)
3967  >>> prove(b[0] == f(a1[0], a2[0]))
3968  proved
3969  """
3970  args = _get_args(args)
3971  if __debug__:
3972  _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
3973  _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
3974  _z3_assert(all(map(is_array, args)), "Z3 array expected expected")
3975  _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
3976  _args, sz = _to_ast_array(args)
3977  ctx = f.ctx
3978  return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
3979
3980 def K(dom, v):
3981  """Return a Z3 constant array expression.
3982
3983  >>> a = K(IntSort(), 10)
3984  >>> a
3985  K(Int, 10)
3986  >>> a.sort()
3987  Array(Int, Int)
3988  >>> i = Int('i')
3989  >>> a[i]
3990  K(Int, 10)[i]
3991  >>> simplify(a[i])
3992  10
3993  """
3994  if __debug__:
3995  _z3_assert(is_sort(dom), "Z3 sort expected")
3996  ctx = dom.ctx
3997  if not is_expr(v):
3998  v = _py2expr(v, ctx)
3999  return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
4000
4001 def is_select(a):
4002  """Return `True` if `a` is a Z3 array select application.
4003
4004  >>> a = Array('a', IntSort(), IntSort())
4005  >>> is_select(a)
4006  False
4007  >>> is_select(a[0])
4008  True
4009  """
4010  return is_app_of(a, Z3_OP_SELECT)
4011
4012 def is_store(a):
4013  """Return `True` if `a` is a Z3 array store application.
4014
4015  >>> a = Array('a', IntSort(), IntSort())
4016  >>> is_store(a)
4017  False
4018  >>> is_store(Store(a, 0, 1))
4019  True
4020  """
4021  return is_app_of(a, Z3_OP_STORE)
4022
4023 #########################################
4024 #
4025 # Datatypes
4026 #
4027 #########################################
4028
4029 def _valid_accessor(acc):
4030  """Return `True` if acc is pair of the form (String, Datatype or Sort). """
4031  return isinstance(acc, tuple) and len(acc) == 2 and isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1]))
4032
4033 class Datatype:
4034  """Helper class for declaring Z3 datatypes.
4035
4036  >>> List = Datatype('List')
4037  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4038  >>> List.declare('nil')
4039  >>> List = List.create()
4040  >>> # List is now a Z3 declaration
4041  >>> List.nil
4042  nil
4043  >>> List.cons(10, List.nil)
4044  cons(10, nil)
4045  >>> List.cons(10, List.nil).sort()
4046  List
4047  >>> cons = List.cons
4048  >>> nil = List.nil
4049  >>> car = List.car
4050  >>> cdr = List.cdr
4051  >>> n = cons(1, cons(0, nil))
4052  >>> n
4053  cons(1, cons(0, nil))
4054  >>> simplify(cdr(n))
4055  cons(0, nil)
4056  >>> simplify(car(n))
4057  1
4058  """
4059  def __init__(self, name, ctx=None):
4060  self.ctx = _get_ctx(ctx)
4061  self.name = name
4062  self.constructors = []
4063
4064  def declare_core(self, name, rec_name, *args):
4065  if __debug__:
4066  _z3_assert(isinstance(name, str), "String expected")
4067  _z3_assert(isinstance(rec_name, str), "String expected")
4068  _z3_assert(all(map(_valid_accessor, args)), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)")
4069  self.constructors.append((name, rec_name, args))
4070
4071  def declare(self, name, *args):
4072  """Declare constructor named `name` with the given accessors `args`.
4073  Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared.
4074
4075  In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
4076  declares the constructor named `cons` that builds a new List using an integer and a List.
4077  It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
4078  and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create
4079  the actual datatype in Z3.
4080
4081  >>> List = Datatype('List')
4082  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4083  >>> List.declare('nil')
4084  >>> List = List.create()
4085  """
4086  if __debug__:
4087  _z3_assert(isinstance(name, str), "String expected")
4088  return self.declare_core(name, "is_" + name, *args)
4089
4090  def __repr__(self):
4091  return "Datatype(%s, %s)" % (self.name, self.constructors)
4092
4093  def create(self):
4094  """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`.
4095
4096  The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
4097
4098  >>> List = Datatype('List')
4099  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4100  >>> List.declare('nil')
4101  >>> List = List.create()
4102  >>> List.nil
4103  nil
4104  >>> List.cons(10, List.nil)
4105  cons(10, nil)
4106  """
4107  return CreateDatatypes([self])[0]
4108
4109 class ScopedConstructor:
4110  """Auxiliary object used to create Z3 datatypes."""
4111  def __init__(self, c, ctx):
4112  self.c = c
4113  self.ctx = ctx
4114  def __del__(self):
4115  Z3_del_constructor(self.ctx.ref(), self.c)
4116
4117 class ScopedConstructorList:
4118  """Auxiliary object used to create Z3 datatypes."""
4119  def __init__(self, c, ctx):
4120  self.c = c
4121  self.ctx = ctx
4122  def __del__(self):
4123  Z3_del_constructor_list(self.ctx.ref(), self.c)
4124
4125 def CreateDatatypes(*ds):
4126  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
4127
4128  In the following example we define a Tree-List using two mutually recursive datatypes.
4129
4130  >>> TreeList = Datatype('TreeList')
4131  >>> Tree = Datatype('Tree')
4132  >>> # Tree has two constructors: leaf and node
4133  >>> Tree.declare('leaf', ('val', IntSort()))
4134  >>> # a node contains a list of trees
4135  >>> Tree.declare('node', ('children', TreeList))
4136  >>> TreeList.declare('nil')
4137  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
4138  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
4139  >>> Tree.val(Tree.leaf(10))
4140  val(leaf(10))
4141  >>> simplify(Tree.val(Tree.leaf(10)))
4142  10
4143  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4144  >>> n1
4145  node(cons(leaf(10), cons(leaf(20), nil)))
4146  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4147  >>> simplify(n2 == n1)
4148  False
4149  >>> simplify(TreeList.car(Tree.children(n2)) == n1)
4150  True
4151  """
4152  ds = _get_args(ds)
4153  if __debug__:
4154  _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
4155  _z3_assert(all(map(lambda d: isinstance(d, Datatype), ds)), "Arguments must be Datatypes")
4156  _z3_assert(all(map(lambda d: d.ctx == ds[0].ctx, ds)), "Context mismatch")
4157  _z3_assert(all(map(lambda d: d.constructors != [], ds)), "Non-empty Datatypes expected")
4158  ctx = ds[0].ctx
4159  num = len(ds)
4160  names = (Symbol * num)()
4161  out = (Sort * num)()
4162  clists = (ConstructorList * num)()
4163  to_delete = []
4164  for i in range(num):
4165  d = ds[i]
4166  names[i] = to_symbol(d.name, ctx)
4167  num_cs = len(d.constructors)
4168  cs = (Constructor * num_cs)()
4169  for j in range(num_cs):
4170  c = d.constructors[j]
4171  cname = to_symbol(c[0], ctx)
4172  rname = to_symbol(c[1], ctx)
4173  fs = c[2]
4174  num_fs = len(fs)
4175  fnames = (Symbol * num_fs)()
4176  sorts = (Sort * num_fs)()
4177  refs = (ctypes.c_uint * num_fs)()
4178  for k in range(num_fs):
4179  fname = fs[k][0]
4180  ftype = fs[k][1]
4181  fnames[k] = to_symbol(fname, ctx)
4182  if isinstance(ftype, Datatype):
4183  if __debug__:
4184  _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
4185  sorts[k] = None
4186  refs[k] = ds.index(ftype)
4187  else:
4188  if __debug__:
4189  _z3_assert(is_sort(ftype), "Z3 sort expected")
4190  sorts[k] = ftype.ast
4191  refs[k] = 0
4192  cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
4193  to_delete.append(ScopedConstructor(cs[j], ctx))
4194  clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
4195  to_delete.append(ScopedConstructorList(clists[i], ctx))
4196  Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
4197  result = []
4198  ## Create a field for every constructor, recognizer and accessor
4199  for i in range(num):
4200  dref = DatatypeSortRef(out[i], ctx)
4201  num_cs = dref.num_constructors()
4202  for j in range(num_cs):
4203  cref = dref.constructor(j)
4204  cref_name = cref.name()
4205  cref_arity = cref.arity()
4206  if cref.arity() == 0:
4207  cref = cref()
4208  setattr(dref, cref_name, cref)
4209  rref = dref.recognizer(j)
4210  setattr(dref, rref.name(), rref)
4211  for k in range(cref_arity):
4212  aref = dref.accessor(j, k)
4213  setattr(dref, aref.name(), aref)
4214  result.append(dref)
4215  return tuple(result)
4216
4217 class DatatypeSortRef(SortRef):
4218  """Datatype sorts."""
4219  def num_constructors(self):
4220  """Return the number of constructors in the given Z3 datatype.
4221
4222  >>> List = Datatype('List')
4223  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4224  >>> List.declare('nil')
4225  >>> List = List.create()
4226  >>> # List is now a Z3 declaration
4227  >>> List.num_constructors()
4228  2
4229  """
4230  return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
4231
4232  def constructor(self, idx):
4233  """Return a constructor of the datatype `self`.
4234
4235  >>> List = Datatype('List')
4236  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4237  >>> List.declare('nil')
4238  >>> List = List.create()
4239  >>> # List is now a Z3 declaration
4240  >>> List.num_constructors()
4241  2
4242  >>> List.constructor(0)
4243  cons
4244  >>> List.constructor(1)
4245  nil
4246  """
4247  if __debug__:
4248  _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
4249  return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
4250
4251  def recognizer(self, idx):
4252  """In Z3, each constructor has an associated recognizer predicate.
4253
4254  If the constructor is named `name`, then the recognizer `is_name`.
4255
4256  >>> List = Datatype('List')
4257  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4258  >>> List.declare('nil')
4259  >>> List = List.create()
4260  >>> # List is now a Z3 declaration
4261  >>> List.num_constructors()
4262  2
4263  >>> List.recognizer(0)
4264  is_cons
4265  >>> List.recognizer(1)
4266  is_nil
4267  >>> simplify(List.is_nil(List.cons(10, List.nil)))
4268  False
4269  >>> simplify(List.is_cons(List.cons(10, List.nil)))
4270  True
4271  >>> l = Const('l', List)
4272  >>> simplify(List.is_cons(l))
4273  is_cons(l)
4274  """
4275  if __debug__:
4276  _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
4277  return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
4278
4279  def accessor(self, i, j):
4280  """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
4281
4282  >>> List = Datatype('List')
4283  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4284  >>> List.declare('nil')
4285  >>> List = List.create()
4286  >>> List.num_constructors()
4287  2
4288  >>> List.constructor(0)
4289  cons
4290  >>> num_accs = List.constructor(0).arity()
4291  >>> num_accs
4292  2
4293  >>> List.accessor(0, 0)
4294  car
4295  >>> List.accessor(0, 1)
4296  cdr
4297  >>> List.constructor(1)
4298  nil
4299  >>> num_accs = List.constructor(1).arity()
4300  >>> num_accs
4301  0
4302  """
4303  if __debug__:
4304  _z3_assert(i < self.num_constructors(), "Invalid constructor index")
4305  _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
4306  return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
4307
4308 class DatatypeRef(ExprRef):
4309  """Datatype expressions."""
4310  def sort(self):
4311  """Return the datatype sort of the datatype expression `self`."""
4312  return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
4313
4314 def EnumSort(name, values, ctx=None):
4315  """Return a new enumeration sort named `name` containing the given values.
4316
4317  The result is a pair (sort, list of constants).
4318  Example:
4319  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
4320  """
4321  if __debug__:
4322  _z3_assert(isinstance(name, str), "Name must be a string")
4323  _z3_assert(all(map(lambda v: isinstance(v, str), values)), "Eumeration sort values must be strings")
4324  _z3_assert(len(values) > 0, "At least one value expected")
4325  ctx = _get_ctx(ctx)
4326  num = len(values)
4327  _val_names = (Symbol * num)()
4328  for i in range(num):
4329  _val_names[i] = to_symbol(values[i])
4330  _values = (FuncDecl * num)()
4331  _testers = (FuncDecl * num)()
4332  name = to_symbol(name)
4333  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
4334  V = []
4335  for i in range(num):
4336  V.append(FuncDeclRef(_values[i], ctx))
4337  V = map(lambda a: a(), V)
4338  return S, V
4339
4340 #########################################
4341 #
4342 # Parameter Sets
4343 #
4344 #########################################
4345
4346 class ParamsRef:
4347  """Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3.
4348
4349  Consider using the function `args2params` to create instances of this object.
4350  """
4351  def __init__(self, ctx=None):
4352  self.ctx = _get_ctx(ctx)
4353  self.params = Z3_mk_params(self.ctx.ref())
4354  Z3_params_inc_ref(self.ctx.ref(), self.params)
4355
4356  def __del__(self):
4357  Z3_params_dec_ref(self.ctx.ref(), self.params)
4358
4359  def set(self, name, val):
4360  """Set parameter name with value val."""
4361  if __debug__:
4362  _z3_assert(isinstance(name, str), "parameter name must be a string")
4363  name_sym = to_symbol(name, self.ctx)
4364  if isinstance(val, bool):
4365  Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val)
4366  elif isinstance(val, int):
4367  Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val)
4368  elif isinstance(val, float):
4369  Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val)
4370  elif isinstance(val, str):
4371  Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx))
4372  else:
4373  if __debug__:
4374  _z3_assert(False, "invalid parameter value")
4375
4376  def __repr__(self):
4377  return Z3_params_to_string(self.ctx.ref(), self.params)
4378
4379  def validate(self, ds):
4380  _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected")
4381  Z3_params_validate(self.ctx.ref(), self.params, ds.descr)
4382
4383 def args2params(arguments, keywords, ctx=None):
4384  """Convert python arguments into a Z3_params object.
4385  A ':' is added to the keywords, and '_' is replaced with '-'
4386
4387  >>> args2params([':model', True, ':relevancy', 2], {'elim_and' : True})
4388  (params :model 1 :relevancy 2 :elim-and 1)
4389  """
4390  if __debug__:
4391  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
4392  prev = None
4393  r = ParamsRef(ctx)
4394  for a in arguments:
4395  if prev == None:
4396  prev = a
4397  else:
4398  r.set(prev, a)
4399  prev = None
4400  for k, v in keywords.iteritems():
4401  k = ':' + k.replace('_', '-')
4402  r.set(k, v)
4403  return r
4404
4405 class ParamDescrsRef:
4406  """Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3.
4407  """
4408  def __init__(self, descr, ctx=None):
4409  _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected")
4410  self.ctx = _get_ctx(ctx)
4411  self.descr = descr
4412  Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr)
4413
4414  def __del__(self):
4415  Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
4416
4417  def size(self):
4418  """Return the size of in the parameter description `self`.
4419  """
4420  return int(Z3_param_descrs_size(self.ctx.ref(), self.descr))
4421
4422  def __len__(self):
4423  """Return the size of in the parameter description `self`.
4424  """
4425  return self.size()
4426
4427  def get_name(self, i):
4428  """Return the i-th parameter name in the parameter description `self`.
4429  """
4430  return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i))
4431
4432  def get_kind(self, n):
4433  """Return the kind of the parameter named `n`.
4434  """
4435  return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
4436
4437  def __getitem__(self, arg):
4438  if isinstance(arg, int) or isinstance(arg, long):
4439  return self.get_name(arg)
4440  else:
4441  return self.get_kind(arg)
4442
4443  def __repr__(self):
4444  return Z3_param_descrs_to_string(self.ctx.ref(), self.descr)
4445
4446 #########################################
4447 #
4448 # Goals
4449 #
4450 #########################################
4451
4452 class Goal(Z3PPObject):
4453  """Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible).
4454
4455  Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
4456  A goal has a solution if one of its subgoals has a solution.
4457  A goal is unsatisfiable if all subgoals are unsatisfiable.
4458  """
4459
4460  def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
4461  if __debug__:
4462  _z3_assert(goal == None or ctx != None, "If goal is different from None, then ctx must be also different from None")
4463  self.ctx = _get_ctx(ctx)
4464  self.goal = goal
4465  if self.goal == None:
4466  self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
4467  Z3_goal_inc_ref(self.ctx.ref(), self.goal)
4468
4469  def __del__(self):
4470  if self.goal != None:
4471  Z3_goal_dec_ref(self.ctx.ref(), self.goal)
4472
4473  def depth(self):
4474  """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
4475
4476  >>> x, y = Ints('x y')
4477  >>> g = Goal()
4478  >>> g.add(x == 0, y >= x + 1)
4479  >>> g.depth()
4480  0
4481  >>> r = Then('simplify', 'solve-eqs')(g)
4482  >>> # r has 1 subgoal
4483  >>> len(r)
4484  1
4485  >>> r[0].depth()
4486  2
4487  """
4488  return int(Z3_goal_depth(self.ctx.ref(), self.goal))
4489
4490  def inconsistent(self):
4491  """Return `True` if `self` contains the `False` constraints.
4492
4493  >>> x, y = Ints('x y')
4494  >>> g = Goal()
4495  >>> g.inconsistent()
4496  False
4497  >>> g.add(x == 0, x == 1)
4498  >>> g
4499  [x == 0, x == 1]
4500  >>> g.inconsistent()
4501  False
4502  >>> g2 = Tactic('propagate-values')(g)[0]
4503  >>> g2.inconsistent()
4504  True
4505  """
4506  return Z3_goal_inconsistent(self.ctx.ref(), self.goal)
4507
4508  def prec(self):
4509  """Return the precision (under-approximation, over-approximation, or precise) of the goal `self`.
4510
4511  >>> g = Goal()
4512  >>> g.prec() == Z3_GOAL_PRECISE
4513  True
4514  >>> x, y = Ints('x y')
4515  >>> g.add(x == y + 1)
4516  >>> g.prec() == Z3_GOAL_PRECISE
4517  True
4519  >>> g2 = t(g)[0]
4520  >>> g2
4521  [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
4522  >>> g2.prec() == Z3_GOAL_PRECISE
4523  False
4524  >>> g2.prec() == Z3_GOAL_UNDER
4525  True
4526  """
4527  return Z3_goal_precision(self.ctx.ref(), self.goal)
4528
4529  def precision(self):
4530  """Alias for `prec()`.
4531
4532  >>> g = Goal()
4533  >>> g.precision() == Z3_GOAL_PRECISE
4534  True
4535  """
4536  return self.prec()
4537
4538  def size(self):
4539  """Return the number of constraints in the goal `self`.
4540
4541  >>> g = Goal()
4542  >>> g.size()
4543  0
4544  >>> x, y = Ints('x y')
4545  >>> g.add(x == 0, y > x)
4546  >>> g.size()
4547  2
4548  """
4549  return int(Z3_goal_size(self.ctx.ref(), self.goal))
4550
4551  def __len__(self):
4552  """Return the number of constraints in the goal `self`.
4553
4554  >>> g = Goal()
4555  >>> len(g)
4556  0
4557  >>> x, y = Ints('x y')
4558  >>> g.add(x == 0, y > x)
4559  >>> len(g)
4560  2
4561  """
4562  return self.size()
4563
4564  def get(self, i):
4565  """Return a constraint in the goal `self`.
4566
4567  >>> g = Goal()
4568  >>> x, y = Ints('x y')
4569  >>> g.add(x == 0, y > x)
4570  >>> g.get(0)
4571  x == 0
4572  >>> g.get(1)
4573  y > x
4574  """
4575  return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx)
4576
4577  def __getitem__(self, arg):
4578  """Return a constraint in the goal `self`.
4579
4580  >>> g = Goal()
4581  >>> x, y = Ints('x y')
4582  >>> g.add(x == 0, y > x)
4583  >>> g[0]
4584  x == 0
4585  >>> g[1]
4586  y > x
4587  """
4588  if arg >= len(self):
4589  raise IndexError
4590  return self.get(arg)
4591
4592  def assert_exprs(self, *args):
4593  """Assert constraints into the goal.
4594
4595  >>> x = Int('x')
4596  >>> g = Goal()
4597  >>> g.assert_exprs(x > 0, x < 2)
4598  >>> g
4599  [x > 0, x < 2]
4600  """
4601  args = _get_args(args)
4602  s = BoolSort(self.ctx)
4603  for arg in args:
4604  arg = s.cast(arg)
4605  Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast())
4606
4607  def append(self, *args):
4609
4610  >>> x = Int('x')
4611  >>> g = Goal()
4612  >>> g.append(x > 0, x < 2)
4613  >>> g
4614  [x > 0, x < 2]
4615  """
4616  self.assert_exprs(*args)
4617
4618  def insert(self, *args):
4620
4621  >>> x = Int('x')
4622  >>> g = Goal()
4623  >>> g.insert(x > 0, x < 2)
4624  >>> g
4625  [x > 0, x < 2]
4626  """
4627  self.assert_exprs(*args)
4628
4631
4632  >>> x = Int('x')
4633  >>> g = Goal()
4634  >>> g.add(x > 0, x < 2)
4635  >>> g
4636  [x > 0, x < 2]
4637  """
4638  self.assert_exprs(*args)
4639
4640  def __repr__(self):
4641  return obj_to_string(self)
4642
4643  def sexpr(self):
4644  """Return a textual representation of the s-expression representing the goal."""
4645  return Z3_goal_to_string(self.ctx.ref(), self.goal)
4646
4647  def translate(self, target):
4648  """Copy goal `self` to context `target`.
4649
4650  >>> x = Int('x')
4651  >>> g = Goal()
4653  >>> g
4654  [x > 10]
4655  >>> c2 = Context()
4656  >>> g2 = g.translate(c2)
4657  >>> g2
4658  [x > 10]
4659  >>> g.ctx == main_ctx()
4660  True
4661  >>> g2.ctx == c2
4662  True
4663  >>> g2.ctx == main_ctx()
4664  False
4665  """
4666  if __debug__:
4667  _z3_assert(isinstance(target, Context), "target must be a context")
4668  return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target)
4669
4670  def simplify(self, *arguments, **keywords):
4671  """Return a new simplified goal.
4672
4673  This method is essentially invoking the simplify tactic.
4674
4675  >>> g = Goal()
4676  >>> x = Int('x')
4677  >>> g.add(x + 1 >= 2)
4678  >>> g
4679  [x + 1 >= 2]
4680  >>> g2 = g.simplify()
4681  >>> g2
4682  [x >= 1]
4683  >>> # g was not modified
4684  >>> g
4685  [x + 1 >= 2]
4686  """
4687  t = Tactic('simplify')
4688  return t.apply(self, *arguments, **keywords)[0]
4689
4690  def as_expr(self):
4691  """Return goal `self` as a single Z3 expression.
4692
4693  >>> x = Int('x')
4694  >>> g = Goal()
4695  >>> g.as_expr()
4696  True
4698  >>> g.as_expr()
4699  x > 1
4701  >>> g.as_expr()
4702  And(x > 1, x < 10)
4703  """
4704  sz = len(self)
4705  if sz == 0:
4706  return BoolVal(True, self.ctx)
4707  elif sz == 1:
4708  return self.get(0)
4709  else:
4710  return And([ self.get(i) for i in range(len(self)) ])
4711
4712 #########################################
4713 #
4714 # AST Vector
4715 #
4716 #########################################
4717 class AstVector(Z3PPObject):
4718  """A collection (vector) of ASTs."""
4719
4720  def __init__(self, v=None, ctx=None):
4721  self.vector = None
4722  if v == None:
4723  self.ctx = _get_ctx(ctx)
4724  self.vector = Z3_mk_ast_vector(self.ctx.ref())
4725  else:
4726  self.vector = v
4727  assert ctx != None
4728  self.ctx = ctx
4729  Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
4730
4731  def __del__(self):
4732  if self.vector != None:
4733  Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
4734
4735  def __len__(self):
4736  """Return the size of the vector `self`.
4737
4738  >>> A = AstVector()
4739  >>> len(A)
4740  0
4741  >>> A.push(Int('x'))
4742  >>> A.push(Int('x'))
4743  >>> len(A)
4744  2
4745  """
4746  return int(Z3_ast_vector_size(self.ctx.ref(), self.vector))
4747
4748  def __getitem__(self, i):
4749  """Return the AST at position `i`.
4750
4751  >>> A = AstVector()
4752  >>> A.push(Int('x') + 1)
4753  >>> A.push(Int('y'))
4754  >>> A[0]
4755  x + 1
4756  >>> A[1]
4757  y
4758  """
4759  if i >= self.__len__():
4760  raise IndexError
4761  return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
4762
4763  def __setitem__(self, i, v):
4764  """Update AST at position `i`.
4765
4766  >>> A = AstVector()
4767  >>> A.push(Int('x') + 1)
4768  >>> A.push(Int('y'))
4769  >>> A[0]
4770  x + 1
4771  >>> A[0] = Int('x')
4772  >>> A[0]
4773  x
4774  """
4775  if i >= self.__len__():
4776  raise IndexError
4777  Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast())
4778
4779  def push(self, v):
4780  """Add `v` in the end of the vector.
4781
4782  >>> A = AstVector()
4783  >>> len(A)
4784  0
4785  >>> A.push(Int('x'))
4786  >>> len(A)
4787  1
4788  """
4789  Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast())
4790
4791  def resize(self, sz):
4792  """Resize the vector to `sz` elements.
4793
4794  >>> A = AstVector()
4795  >>> A.resize(10)
4796  >>> len(A)
4797  10
4798  >>> for i in range(10): A[i] = Int('x')
4799  >>> A[5]
4800  x
4801  """
4802  Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz)
4803
4804  def __contains__(self, item):
4805  """Return `True` if the vector contains `item`.
4806
4807  >>> x = Int('x')
4808  >>> A = AstVector()
4809  >>> x in A
4810  False
4811  >>> A.push(x)
4812  >>> x in A
4813  True
4814  >>> (x+1) in A
4815  False
4816  >>> A.push(x+1)
4817  >>> (x+1) in A
4818  True
4819  >>> A
4820  [x, x + 1]
4821  """
4822  for elem in self:
4823  if elem.eq(item):
4824  return True
4825  return False
4826
4827  def translate(self, other_ctx):
4828  """Copy vector `self` to context `other_ctx`.
4829
4830  >>> x = Int('x')
4831  >>> A = AstVector()
4832  >>> A.push(x)
4833  >>> c2 = Context()
4834  >>> B = A.translate(c2)
4835  >>> B
4836  [x]
4837  """
4838  return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx)
4839
4840  def __repr__(self):
4841  return obj_to_string(self)
4842
4843  def sexpr(self):
4844  """Return a textual representation of the s-expression representing the vector."""
4845  return Z3_ast_vector_to_string(self.ctx.ref(), self.vector)
4846
4847 #########################################
4848 #
4849 # AST Map
4850 #
4851 #########################################
4852 class AstMap:
4853  """A mapping from ASTs to ASTs."""
4854
4855  def __init__(self, m=None, ctx=None):
4856  self.map = None
4857  if m == None:
4858  self.ctx = _get_ctx(ctx)
4859  self.map = Z3_mk_ast_map(self.ctx.ref())
4860  else:
4861  self.map = m
4862  assert ctx != None
4863  self.ctx = ctx
4864  Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
4865
4866  def __del__(self):
4867  if self.map != None:
4868  Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
4869
4870  def __len__(self):
4871  """Return the size of the map.
4872
4873  >>> M = AstMap()
4874  >>> len(M)
4875  0
4876  >>> x = Int('x')
4877  >>> M[x] = IntVal(1)
4878  >>> len(M)
4879  1
4880  """
4881  return int(Z3_ast_map_size(self.ctx.ref(), self.map))
4882
4883  def __contains__(self, key):
4884  """Return `True` if the map contains key `key`.
4885
4886  >>> M = AstMap()
4887  >>> x = Int('x')
4888  >>> M[x] = x + 1
4889  >>> x in M
4890  True
4891  >>> x+1 in M
4892  False
4893  """
4894  return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast())
4895
4896  def __getitem__(self, key):
4897  """Retrieve the value associated with key `key`.
4898
4899  >>> M = AstMap()
4900  >>> x = Int('x')
4901  >>> M[x] = x + 1
4902  >>> M[x]
4903  x + 1
4904  """
4905  return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx)
4906
4907  def __setitem__(self, k, v):
4908  """Add/Update key `k` with value `v`.
4909
4910  >>> M = AstMap()
4911  >>> x = Int('x')
4912  >>> M[x] = x + 1
4913  >>> len(M)
4914  1
4915  >>> M[x]
4916  x + 1
4917  >>> M[x] = IntVal(1)
4918  >>> M[x]
4919  1
4920  """
4921  Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast())
4922
4923  def __repr__(self):
4924  return Z3_ast_map_to_string(self.ctx.ref(), self.map)
4925
4926  def erase(self, k):
4927  """Remove the entry associated with key `k`.
4928
4929  >>> M = AstMap()
4930  >>> x = Int('x')
4931  >>> M[x] = x + 1
4932  >>> len(M)
4933  1
4934  >>> M.erase(x)
4935  >>> len(M)
4936  0
4937  """
4938  Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast())
4939
4940  def reset(self):
4941  """Remove all entries from the map.
4942
4943  >>> M = AstMap()
4944  >>> x = Int('x')
4945  >>> M[x] = x + 1
4946  >>> M[x+x] = IntVal(1)
4947  >>> len(M)
4948  2
4949  >>> M.reset()
4950  >>> len(M)
4951  0
4952  """
4953  Z3_ast_map_reset(self.ctx.ref(), self.map)
4954
4955  def keys(self):
4956  """Return an AstVector containing all keys in the map.
4957
4958  >>> M = AstMap()
4959  >>> x = Int('x')
4960  >>> M[x] = x + 1
4961  >>> M[x+x] = IntVal(1)
4962  >>> M.keys()
4963  [x, x + x]
4964  """
4965  return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx)
4966
4967 #########################################
4968 #
4969 # Model
4970 #
4971 #########################################
4972
4973 class FuncEntry:
4974  """Store the value of the interpretation of a function in a particular point."""
4975
4976  def __init__(self, entry, ctx):
4977  self.entry = entry
4978  self.ctx = ctx
4979  Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
4980
4981  def __del__(self):
4982  Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
4983
4984  def num_args(self):
4985  """Return the number of arguments in the given entry.
4986
4987  >>> f = Function('f', IntSort(), IntSort(), IntSort())
4988  >>> s = Solver()
4989  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
4990  >>> s.check()
4991  sat
4992  >>> m = s.model()
4993  >>> f_i = m[f]
4994  >>> f_i.num_entries()
4995  3
4996  >>> e = f_i.entry(0)
4997  >>> e.num_args()
4998  2
4999  """
5000  return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
5001
5002  def arg_value(self, idx):
5003  """Return the value of argument `idx`.
5004
5005  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5006  >>> s = Solver()
5007  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5008  >>> s.check()
5009  sat
5010  >>> m = s.model()
5011  >>> f_i = m[f]
5012  >>> f_i.num_entries()
5013  3
5014  >>> e = f_i.entry(0)
5015  >>> e
5016  [0, 1, 10]
5017  >>> e.num_args()
5018  2
5019  >>> e.arg_value(0)
5020  0
5021  >>> e.arg_value(1)
5022  1
5023  >>> try:
5024  ... e.arg_value(2)
5025  ... except IndexError:
5026  ... print "index error"
5027  index error
5028  """
5029  if idx >= self.num_args():
5030  raise IndexError
5031  return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
5032
5033  def value(self):
5034  """Return the value of the function at point `self`.
5035
5036  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5037  >>> s = Solver()
5038  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5039  >>> s.check()
5040  sat
5041  >>> m = s.model()
5042  >>> f_i = m[f]
5043  >>> f_i.num_entries()
5044  3
5045  >>> e = f_i.entry(0)
5046  >>> e
5047  [0, 1, 10]
5048  >>> e.num_args()
5049  2
5050  >>> e.value()
5051  10
5052  """
5053  return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
5054
5055  def as_list(self):
5056  """Return entry `self` as a Python list.
5057  >>> f = Function('f', IntSort(), IntSort(), IntSort())
5058  >>> s = Solver()
5059  >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5060  >>> s.check()
5061  sat
5062  >>> m = s.model()
5063  >>> f_i = m[f]
5064  >>> f_i.num_entries()
5065  3
5066  >>> e = f_i.entry(0)
5067  >>> e.as_list()
5068  [0, 1, 10]
5069  """
5070  args = [ self.arg_value(i) for i in range(self.num_args())]
5071  args.append(self.value())
5072  return args
5073
5074  def __repr__(self):
5075  return repr(self.as_list())
5076
5077 class FuncInterp(Z3PPObject):
5078  """Stores the interpretation of a function in a Z3 model."""
5079
5080  def __init__(self, f, ctx):
5081  self.f = f
5082  self.ctx = ctx
5083  if self.f != None:
5084  Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
5085
5086  def __del__(self):
5087  if self.f != None:
5088  Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
5089
5090  def else_value(self):
5091  """Return the `else` value for a function interpretation.
5092
5093  >>> f = Function('f', IntSort(), IntSort())
5094  >>> s = Solver()
5095  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5096  >>> s.check()
5097  sat
5098  >>> m = s.model()
5099  >>> m[f]
5100  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5101  >>> m[f].else_value()
5102  1
5103  """
5104  return _to_expr_ref(Z3_func_interp_get_else(self.ctx.ref(), self.f), self.ctx)
5105
5106  def num_entries(self):
5107  """Return the number of entries/points in the function interpretation `self`.
5108
5109  >>> f = Function('f', IntSort(), IntSort())
5110  >>> s = Solver()
5111  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5112  >>> s.check()
5113  sat
5114  >>> m = s.model()
5115  >>> m[f]
5116  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5117  >>> m[f].num_entries()
5118  3
5119  """
5120  return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
5121
5122  def arity(self):
5123  """Return the number of arguments for each entry in the function interpretation `self`.
5124
5125  >>> f = Function('f', IntSort(), IntSort())
5126  >>> s = Solver()
5127  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5128  >>> s.check()
5129  sat
5130  >>> m = s.model()
5131  >>> m[f].arity()
5132  1
5133  """
5134  return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
5135
5136  def entry(self, idx):
5137  """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
5138
5139  >>> f = Function('f', IntSort(), IntSort())
5140  >>> s = Solver()
5141  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5142  >>> s.check()
5143  sat
5144  >>> m = s.model()
5145  >>> m[f]
5146  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5147  >>> m[f].num_entries()
5148  3
5149  >>> m[f].entry(0)
5150  [0, 1]
5151  >>> m[f].entry(1)
5152  [1, 1]
5153  >>> m[f].entry(2)
5154  [2, 0]
5155  """
5156  if idx >= self.num_entries():
5157  raise IndexError
5158  return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
5159
5160  def as_list(self):
5161  """Return the function interpretation as a Python list.
5162  >>> f = Function('f', IntSort(), IntSort())
5163  >>> s = Solver()
5164  >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
5165  >>> s.check()
5166  sat
5167  >>> m = s.model()
5168  >>> m[f]
5169  [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
5170  >>> m[f].as_list()
5171  [[0, 1], [1, 1], [2, 0], 1]
5172  """
5173  r = [ self.entry(i).as_list() for i in range(self.num_entries())]
5174  r.append(self.else_value())
5175  return r
5176
5177  def __repr__(self):
5178  return obj_to_string(self)
5179
5180 class ModelRef(Z3PPObject):
5181  """Model/Solution of a satisfiability problem (aka system of constraints)."""
5182
5183  def __init__(self, m, ctx):
5184  assert ctx != None
5185  self.model = m
5186  self.ctx = ctx
5187  Z3_model_inc_ref(self.ctx.ref(), self.model)
5188
5189  def __del__(self):
5190  Z3_model_dec_ref(self.ctx.ref(), self.model)
5191
5192  def __repr__(self):
5193  return obj_to_string(self)
5194
5195  def sexpr(self):
5196  """Return a textual representation of the s-expression representing the model."""
5197  return Z3_model_to_string(self.ctx.ref(), self.model)
5198
5199  def eval(self, t, model_completion=False):
5200  """Evaluate the expression `t` in the model `self`. If `model_completion` is enabled, then a default interpretation is automatically added for symbols that do not have an interpretation in the model `self`.
5201
5202  >>> x = Int('x')
5203  >>> s = Solver()
5204  >>> s.add(x > 0, x < 2)
5205  >>> s.check()
5206  sat
5207  >>> m = s.model()
5208  >>> m.eval(x + 1)
5209  2
5210  >>> m.eval(x == 1)
5211  True
5212  >>> y = Int('y')
5213  >>> m.eval(y + x)
5214  1 + y
5215  >>> m.eval(y)
5216  y
5217  >>> m.eval(y, model_completion=True)
5218  0
5219  >>> # Now, m contains an interpretation for y
5220  >>> m.eval(y + x)
5221  1
5222  """
5223  r = (Ast * 1)()
5224  if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
5225  return _to_expr_ref(r[0], self.ctx)
5226  raise Z3Exception("failed to evaluate expression in the model")
5227
5228  def evaluate(self, t, model_completion=False):
5229  """Alias for `eval`.
5230
5231  >>> x = Int('x')
5232  >>> s = Solver()
5233  >>> s.add(x > 0, x < 2)
5234  >>> s.check()
5235  sat
5236  >>> m = s.model()
5237  >>> m.evaluate(x + 1)
5238  2
5239  >>> m.evaluate(x == 1)
5240  True
5241  >>> y = Int('y')
5242  >>> m.evaluate(y + x)
5243  1 + y
5244  >>> m.evaluate(y)
5245  y
5246  >>> m.evaluate(y, model_completion=True)
5247  0
5248  >>> # Now, m contains an interpretation for y
5249  >>> m.evaluate(y + x)
5250  1
5251  """
5252  return self.eval(t, model_completion)
5253
5254  def __len__(self):
5255  """Return the number of constant and function declarations in the model `self`.
5256
5257  >>> f = Function('f', IntSort(), IntSort())
5258  >>> x = Int('x')
5259  >>> s = Solver()
5260  >>> s.add(x > 0, f(x) != x)
5261  >>> s.check()
5262  sat
5263  >>> m = s.model()
5264  >>> len(m)
5265  2
5266  """
5267  return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model))
5268
5269  def get_interp(self, decl):
5270  """Return the interpretation for a given declaration or constant.
5271
5272  >>> f = Function('f', IntSort(), IntSort())
5273  >>> x = Int('x')
5274  >>> s = Solver()
5275  >>> s.add(x > 0, x < 2, f(x) == 0)
5276  >>> s.check()
5277  sat
5278  >>> m = s.model()
5279  >>> m[x]
5280  1
5281  >>> m[f]
5282  [1 -> 0, else -> 0]
5283  """
5284  if __debug__:
5285  _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected")
5286  if is_const(decl):
5287  decl = decl.decl()
5288  try:
5289  if decl.arity() == 0:
5290  r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
5291  if is_as_array(r):
5292  return self.get_interp(get_as_array_func(r))
5293  else:
5294  return r
5295  else:
5296  return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
5297  except Z3Exception:
5298  return None
5299
5300  def num_sorts(self):
5301  """Return the number of unintepreted sorts that contain an interpretation in the model `self`.
5302
5303  >>> A = DeclareSort('A')
5304  >>> a, b = Consts('a b', A)
5305  >>> s = Solver()
5307  >>> s.check()
5308  sat
5309  >>> m = s.model()
5310  >>> m.num_sorts()
5311  1
5312  """
5313  return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model))
5314
5315  def get_sort(self, idx):
5316  """Return the unintepreted sort at position `idx` < self.num_sorts().
5317
5318  >>> A = DeclareSort('A')
5319  >>> B = DeclareSort('B')
5320  >>> a1, a2 = Consts('a1 a2', A)
5321  >>> b1, b2 = Consts('b1 b2', B)
5322  >>> s = Solver()
5323  >>> s.add(a1 != a2, b1 != b2)
5324  >>> s.check()
5325  sat
5326  >>> m = s.model()
5327  >>> m.num_sorts()
5328  2
5329  >>> m.get_sort(0)
5330  A
5331  >>> m.get_sort(1)
5332  B
5333  """
5334  if idx >= self.num_sorts():
5335  raise IndexError
5336  return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx)
5337
5338  def sorts(self):
5339  """Return all uninterpreted sorts that have an interpretation in the model `self`.
5340
5341  >>> A = DeclareSort('A')
5342  >>> B = DeclareSort('B')
5343  >>> a1, a2 = Consts('a1 a2', A)
5344  >>> b1, b2 = Consts('b1 b2', B)
5345  >>> s = Solver()
5346  >>> s.add(a1 != a2, b1 != b2)
5347  >>> s.check()
5348  sat
5349  >>> m = s.model()
5350  >>> m.sorts()
5351  [A, B]
5352  """
5353  return [ self.get_sort(i) for i in range(self.num_sorts()) ]
5354
5355  def get_universe(self, s):
5356  """Return the intepretation for the uninterpreted sort `s` in the model `self`.
5357
5358  >>> A = DeclareSort('A')
5359  >>> a, b = Consts('a b', A)
5360  >>> s = Solver()
5362  >>> s.check()
5363  sat
5364  >>> m = s.model()
5365  >>> m.get_universe(A)
5366  [A!val!0, A!val!1]
5367  """
5368  if __debug__:
5369  _z3_assert(isinstance(s, SortRef), "Z3 sort expected")
5370  try:
5371  return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx)
5372  except Z3Exception:
5373  return None
5374
5375  def __getitem__(self, idx):
5376  """If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpreation is returned.
5377
5378  The elements can be retrieved using position or the actual declaration.
5379
5380  >>> f = Function('f', IntSort(), IntSort())
5381  >>> x = Int('x')
5382  >>> s = Solver()
5383  >>> s.add(x > 0, x < 2, f(x) == 0)
5384  >>> s.check()
5385  sat
5386  >>> m = s.model()
5387  >>> len(m)
5388  2
5389  >>> m[0]
5390  x
5391  >>> m[1]
5392  f
5393  >>> m[x]
5394  1
5395  >>> m[f]
5396  [1 -> 0, else -> 0]
5397  >>> for d in m: print "%s -> %s" % (d, m[d])
5398  x -> 1
5399  f -> [1 -> 0, else -> 0]
5400  """
5401  if isinstance(idx, int):
5402  if idx >= len(self):
5403  raise IndexError
5404  num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
5405  if (idx < num_consts):
5406  return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx)
5407  else:
5408  return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx)
5409  if isinstance(idx, FuncDeclRef):
5410  return self.get_interp(idx)
5411  if is_const(idx):
5412  return self.get_interp(idx.decl())
5413  if isinstance(idx, SortRef):
5414  return self.get_universe(idx)
5415  if __debug__:
5416  _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected")
5417  return None
5418
5419  def decls(self):
5420  """Return a list with all symbols that have an interpreation in the model `self`.
5421  >>> f = Function('f', IntSort(), IntSort())
5422  >>> x = Int('x')
5423  >>> s = Solver()
5424  >>> s.add(x > 0, x < 2, f(x) == 0)
5425  >>> s.check()
5426  sat
5427  >>> m = s.model()
5428  >>> m.decls()
5429  [x, f]
5430  """
5431  r = []
5432  for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)):
5433  r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx))
5434  for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)):
5435  r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
5436  return r
5437
5438 def is_as_array(n):
5439  """Return true if n is a Z3 expression of the form (_ as-array f)."""
5440  return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
5441
5442 def get_as_array_func(n):
5443  """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
5444  if __debug__:
5445  _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
5446  return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
5447
5448 #########################################
5449 #
5450 # Statistics
5451 #
5452 #########################################
5453 class Statistics:
5454  """Statistics for `Solver.check()`."""
5455
5456  def __init__(self, stats, ctx):
5457  self.stats = stats
5458  self.ctx = ctx
5459  Z3_stats_inc_ref(self.ctx.ref(), self.stats)
5460
5461  def __del__(self):
5462  Z3_stats_dec_ref(self.ctx.ref(), self.stats)
5463
5464  def __repr__(self):
5465  if in_html_mode():
5466  out = io.StringIO()
5467  even = True
5469  for k, v in self:
5470  if even:
5471  out.write(u'<tr style="background-color:#CFCFCF">')
5472  even = False
5473  else:
5474  out.write(u'<tr>')
5475  even = True
5476  out.write(u'<td>%s</td><td>%s</td></tr>' % (k, v))
5477  out.write(u'</table>')
5478  return out.getvalue()
5479  else:
5480  return Z3_stats_to_string(self.ctx.ref(), self.stats)
5481
5482  def __len__(self):
5483  """Return the number of statistical counters.
5484
5485  >>> x = Int('x')
5486  >>> s = Then('simplify', 'nlsat').solver()
5488  >>> s.check()
5489  sat
5490  >>> st = s.statistics()
5491  >>> len(st)
5492  2
5493  """
5494  return int(Z3_stats_size(self.ctx.ref(), self.stats))
5495
5496  def __getitem__(self, idx):
5497  """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
5498
5499  >>> x = Int('x')
5500  >>> s = Then('simplify', 'nlsat').solver()
5502  >>> s.check()
5503  sat
5504  >>> st = s.statistics()
5505  >>> len(st)
5506  2
5507  >>> st[0]
5508  ('nlsat propagations', 2)
5509  >>> st[1]
5510  ('nlsat stages', 2)
5511  """
5512  if idx >= len(self):
5513  raise IndexError
5514  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5515  val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5516  else:
5517  val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5518  return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
5519
5520  def keys(self):
5521  """Return the list of statistical counters.
5522
5523  >>> x = Int('x')
5524  >>> s = Then('simplify', 'nlsat').solver()
5526  >>> s.check()
5527  sat
5528  >>> st = s.statistics()
5529  >>> st.keys()
5530  ['nlsat propagations', 'nlsat stages']
5531  """
5532  return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
5533
5534  def get_key_value(self, key):
5535  """Return the value of a particular statistical counter.
5536
5537  >>> x = Int('x')
5538  >>> s = Then('simplify', 'nlsat').solver()
5540  >>> s.check()
5541  sat
5542  >>> st = s.statistics()
5543  >>> st.get_key_value('nlsat propagations')
5544  2
5545  """
5546  for idx in range(len(self)):
5547  if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
5548  if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5549  return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5550  else:
5551  return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5552  raise Z3Exception("unknown key")
5553
5554  def __getattr__(self, name):
5555  """Access the value of statistical using attributes.
5556
5557  Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
5558  we should use '_' (e.g., 'nlsat_propagations').
5559
5560  >>> x = Int('x')
5561  >>> s = Then('simplify', 'nlsat').solver()
5563  >>> s.check()
5564  sat
5565  >>> st = s.statistics()
5566  >>> st.keys()
5567  ['nlsat propagations', 'nlsat stages']
5568  >>> st.nlsat_propagations
5569  2
5570  >>> st.nlsat_stages
5571  2
5572  """
5573  key = name.replace('_', ' ')
5574  try:
5575  return self.get_key_value(key)
5576  except Z3Exception:
5577  raise AttributeError
5578
5579 #########################################
5580 #
5581 # Solver
5582 #
5583 #########################################
5584 class CheckSatResult:
5585  """Represents the result of a satisfiability check: sat, unsat, unknown.
5586
5587  >>> s = Solver()
5588  >>> s.check()
5589  sat
5590  >>> r = s.check()
5591  >>> isinstance(r, CheckSatResult)
5592  True
5593  """
5594
5595  def __init__(self, r):
5596  self.r = r
5597
5598  def __eq__(self, other):
5599  return isinstance(other, CheckSatResult) and self.r == other.r
5600
5601  def __ne__(self, other):
5602  return not self.__eq__(other)
5603
5604  def __repr__(self):
5605  if in_html_mode():
5606  if self.r == Z3_L_TRUE:
5607  return "<b>sat</b>"
5608  elif self.r == Z3_L_FALSE:
5609  return "<b>unsat</b>"
5610  else:
5611  return "<b>unknown</b>"
5612  else:
5613  if self.r == Z3_L_TRUE:
5614  return "sat"
5615  elif self.r == Z3_L_FALSE:
5616  return "unsat"
5617  else:
5618  return "unknown"
5619
5620 sat = CheckSatResult(Z3_L_TRUE)
5621 unsat = CheckSatResult(Z3_L_FALSE)
5622 unknown = CheckSatResult(Z3_L_UNDEF)
5623
5624 class Solver(Z3PPObject):
5625  """Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc."""
5626
5627  def __init__(self, solver=None, ctx=None):
5628  assert solver == None or ctx != None
5629  self.ctx = _get_ctx(ctx)
5630  self.solver = None
5631  if solver == None:
5632  self.solver = Z3_mk_solver(self.ctx.ref())
5633  else:
5634  self.solver = solver
5635  Z3_solver_inc_ref(self.ctx.ref(), self.solver)
5636
5637  def __del__(self):
5638  if self.solver != None:
5639  Z3_solver_dec_ref(self.ctx.ref(), self.solver)
5640
5641  def set(self, *args, **keys):
5642  """Set a configuration option. The method `help()` return a string containing all available options.
5643
5644  >>> s = Solver()
5645  >>> # The option MBQI can be set using three different approaches.
5646  >>> s.set(mbqi=True)
5647  >>> s.set('MBQI', True)
5648  >>> s.set(':mbqi', True)
5649  """
5650  p = args2params(args, keys, self.ctx)
5651  Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
5652
5653  def push(self):
5654  """Create a backtracking point.
5655
5656  >>> x = Int('x')
5657  >>> s = Solver()
5659  >>> s
5660  [x > 0]
5661  >>> s.push()
5663  >>> s
5664  [x > 0, x < 1]
5665  >>> s.check()
5666  unsat
5667  >>> s.pop()
5668  >>> s.check()
5669  sat
5670  >>> s
5671  [x > 0]
5672  """
5673  Z3_solver_push(self.ctx.ref(), self.solver)
5674
5675  def pop(self, num=1):
5676  """Backtrack \c num backtracking points.
5677
5678  >>> x = Int('x')
5679  >>> s = Solver()
5681  >>> s
5682  [x > 0]
5683  >>> s.push()
5685  >>> s
5686  [x > 0, x < 1]
5687  >>> s.check()
5688  unsat
5689  >>> s.pop()
5690  >>> s.check()
5691  sat
5692  >>> s
5693  [x > 0]
5694  """
5695  Z3_solver_pop(self.ctx.ref(), self.solver, num)
5696
5697  def reset(self):
5698  """Remove all asserted constraints and backtracking points created using `push()`.
5699
5700  >>> x = Int('x')
5701  >>> s = Solver()
5703  >>> s
5704  [x > 0]
5705  >>> s.reset()
5706  >>> s
5707  []
5708  """
5709  Z3_solver_reset(self.ctx.ref(), self.solver)
5710
5711  def assert_exprs(self, *args):
5712  """Assert constraints into the solver.
5713
5714  >>> x = Int('x')
5715  >>> s = Solver()
5716  >>> s.assert_exprs(x > 0, x < 2)
5717  >>> s
5718  [x > 0, x < 2]
5719  """
5720  args = _get_args(args)
5721  s = BoolSort(self.ctx)
5722  for arg in args:
5723  if isinstance(arg, Goal) or isinstance(arg, AstVector):
5724  for f in arg:
5725  Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
5726  else:
5727  arg = s.cast(arg)
5728  Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
5729
5731  """Assert constraints into the solver.
5732
5733  >>> x = Int('x')
5734  >>> s = Solver()
5735  >>> s.add(x > 0, x < 2)
5736  >>> s
5737  [x > 0, x < 2]
5738  """
5739  self.assert_exprs(*args)
5740
5741  def append(self, *args):
5742  """Assert constraints into the solver.
5743
5744  >>> x = Int('x')
5745  >>> s = Solver()
5746  >>> s.append(x > 0, x < 2)
5747  >>> s
5748  [x > 0, x < 2]
5749  """
5750  self.assert_exprs(*args)
5751
5752  def insert(self, *args):
5753  """Assert constraints into the solver.
5754
5755  >>> x = Int('x')
5756  >>> s = Solver()
5757  >>> s.insert(x > 0, x < 2)
5758  >>> s
5759  [x > 0, x < 2]
5760  """
5761  self.assert_exprs(*args)
5762
5763  def assert_and_track(self, a, p):
5764  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
5765
5766  If `p` is a string, it will be automatically converted into a Boolean constant.
5767
5768  >>> x = Int('x')
5769  >>> p3 = Bool('p3')
5770  >>> s = Solver()
5771  >>> s.set(unsat_core=True)
5772  >>> s.assert_and_track(x > 0, 'p1')
5773  >>> s.assert_and_track(x != 1, 'p2')
5774  >>> s.assert_and_track(x < 0, p3)
5775  >>> print s.check()
5776  unsat
5777  >>> print s.unsat_core()
5778  [p3, p1]
5779  """
5780  if isinstance(p, str):
5781  p = Bool(p, self.ctx)
5782  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
5783  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
5784  Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
5785
5786  def check(self, *assumptions):
5787  """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
5788
5789  >>> x = Int('x')
5790  >>> s = Solver()
5791  >>> s.check()
5792  sat
5793  >>> s.add(x > 0, x < 2)
5794  >>> s.check()
5795  sat
5796  >>> s.model()
5797  [x = 1]
5799  >>> s.check()
5800  unsat
5801  >>> s.reset()
5803  >>> s.check()
5804  unknown
5805  """
5806  assumptions = _get_args(assumptions)
5807  num = len(assumptions)
5808  _assumptions = (Ast * num)()
5809  for i in range(num):
5810  _assumptions[i] = assumptions[i].as_ast()
5811  r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
5812  return CheckSatResult(r)
5813
5814  def model(self):
5815  """Return a model for the last `check()`.
5816
5817  This function raises an exception if
5818  a model is not available (e.g., last `check()` returned unsat).
5819
5820  >>> s = Solver()
5821  >>> a = Int('a')
5822  >>> s.add(a + 2 == 0)
5823  >>> s.check()
5824  sat
5825  >>> s.model()
5826  [a = -2]
5827  """
5828  try:
5829  return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
5830  except Z3Exception:
5831  raise Z3Exception("model is not available")
5832
5833  def unsat_core(self):
5834  """Return a subset (as an AST vector) of the assumptions provided to the last check().
5835
5836  These are the assumptions Z3 used in the unsatisfiability proof.
5837  Assumptions are available in Z3. They are used to extract unsatisfiable cores.
5838  They may be also used to "retract" assumptions. Note that, assumptions are not really
5839  "soft constraints", but they can be used to implement them.
5840
5841  >>> p1, p2, p3 = Bools('p1 p2 p3')
5842  >>> x, y = Ints('x y')
5843  >>> s = Solver()
5844  >>> s.add(Implies(p1, x > 0))
5845  >>> s.add(Implies(p2, y > x))
5846  >>> s.add(Implies(p2, y < 1))
5847  >>> s.add(Implies(p3, y > -3))
5848  >>> s.check(p1, p2, p3)
5849  unsat
5850  >>> core = s.unsat_core()
5851  >>> len(core)
5852  2
5853  >>> p1 in core
5854  True
5855  >>> p2 in core
5856  True
5857  >>> p3 in core
5858  False
5859  >>> # "Retracting" p2
5860  >>> s.check(p1, p3)
5861  sat
5862  """
5863  return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
5864
5865  def proof(self):
5866  """Return a proof for the last `check()`. Proof construction must be enabled."""
5867  return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
5868
5869  def assertions(self):
5870  """Return an AST vector containing all added constraints.
5871
5872  >>> s = Solver()
5873  >>> s.assertions()
5874  []
5875  >>> a = Int('a')
5878  >>> s.assertions()
5879  [a > 0, a < 10]
5880  """
5881  return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
5882
5883  def statistics(self):
5884  """Return statistics for the last `check()`.
5885
5886  >>> s = SimpleSolver()
5887  >>> x = Int('x')
5889  >>> s.check()
5890  sat
5891  >>> st = s.statistics()
5892  >>> st.get_key_value('final checks')
5893  1
5894  >>> len(st) > 0
5895  True
5896  >>> st[0] != 0
5897  True
5898  """
5899  return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
5900
5901  def reason_unknown(self):
5902  """Return a string describing why the last `check()` returned `unknown`.
5903
5904  >>> x = Int('x')
5905  >>> s = SimpleSolver()
5907  >>> s.check()
5908  unknown
5909  >>> s.reason_unknown()
5910  '(incomplete (theory arithmetic))'
5911  """
5912  return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
5913
5914  def help(self):
5915  """Display a string describing all available options."""
5916  print Z3_solver_get_help(self.ctx.ref(), self.solver)
5917
5918  def param_descrs(self):
5919  """Return the parameter description set."""
5920  return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
5921
5922  def __repr__(self):
5923  """Return a formatted string with all added constraints."""
5924  return obj_to_string(self)
5925
5926  def sexpr(self):
5927  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
5928
5929  >>> x = Int('x')
5930  >>> s = Solver()