Z3
z3py.py
Go to the documentation of this file.
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
18
19 Small example:
20
21 >>> x = Int('x')
22 >>> y = Int('y')
23 >>> s = Solver()
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()
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
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)
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))
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
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():
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():
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
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
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
2778  """Return `True` if `a` is an expression of the form b + c.
2779
2780  >>> x, y = Ints('x y')
2782  True
2784  False
2785  """
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
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
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())
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
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
4952  """ Add element e to set s
4953  >>> a = Const('a', SetSort(IntSort()))
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
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):
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):
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
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()
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()
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
5815  >>> g.as_expr()
5816  x > 1
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