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