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