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