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.ctxctx = Z3_mk_context_rc(conf)
207  self.ownerowner = True
208  self.eheh = Z3_set_error_handler(self.ctxctx, z3_error_handler)
209  Z3_set_ast_print_mode(self.ctxctx, Z3_PRINT_SMTLIB2_COMPLIANT)
210  Z3_del_config(conf)
211 
212  def __del__(self):
213  if Z3_del_context is not None and self.ownerowner:
214  Z3_del_context(self.ctxctx)
215  self.ctxctx = None
216  self.eheh = None
217 
218  def ref(self):
219  """Return a reference to the actual C pointer to the Z3 context."""
220  return self.ctxctx
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.refref())
229 
230  def param_descrs(self):
231  """Return the global parameter description set."""
232  return ParamDescrsRef(Z3_get_global_param_descrs(self.refref()), 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.astast = ast
347  self.ctxctx = _get_ctx(ctx)
348  Z3_inc_ref(self.ctxctx.ref(), self.as_astas_ast())
349 
350  def __del__(self):
351  if self.ctxctx.ref() is not None and self.astast is not None and Z3_dec_ref is not None:
352  Z3_dec_ref(self.ctxctx.ref(), self.as_astas_ast())
353  self.astast = None
354 
355  def __deepcopy__(self, memo={}):
356  return _to_ast_ref(self.astast, self.ctxctx)
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.eqeq(other)
366 
367  def __hash__(self):
368  return self.hashhash()
369 
370  def __nonzero__(self):
371  return self.__bool____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_refctx_ref(), self.as_astas_ast())
391 
392  def as_ast(self):
393  """Return a pointer to the corresponding C Z3_ast object."""
394  return self.astast
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_refctx_ref(), self.as_astas_ast())
399 
400  def ctx_ref(self):
401  """Return a reference to the C context where this AST node is stored."""
402  return self.ctxctx.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_refctx_ref(), self.as_astas_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.ctxctx.ref(), self.as_astas_ast(), target.ref()), target)
436 
437  def __copy__(self):
438  return self.translatetranslate(self.ctxctx)
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_refctx_ref(), self.as_astas_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_refctx_ref(), self.astast)
564 
565  def get_id(self):
566  return Z3_get_ast_id(self.ctx_refctx_ref(), self.as_astas_astas_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.ctxctx, self.astast)
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.eqeq(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.ctxctx, Z3_get_sort_name(self.ctx_refctx_ref(), self.astast))
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_refctx_ref(), self.astast, 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_refctx_ref(), self.astast, 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_refctx_ref(), self.astast)
728 
729  def get_id(self):
730  return Z3_get_ast_id(self.ctx_refctx_ref(), self.as_astas_astas_ast())
731 
732  def as_func_decl(self):
733  return self.astast
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.ctxctx, Z3_get_decl_name(self.ctx_refctx_ref(), self.astast))
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_refctx_ref(), self.astast))
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.arityarity(), "Index out of bounds")
768  return _to_sort_ref(Z3_get_domain(self.ctx_refctx_ref(), self.astast, i), self.ctxctx)
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_refctx_ref(), self.astast), self.ctxctx)
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_refctx_ref(), self.astast)
792 
793  def params(self):
794  ctx = self.ctxctx
795  n = Z3_get_decl_num_parameters(self.ctx_refctx_ref(), self.astast)
796  result = [None for i in range(n)]
797  for i in range(n):
798  k = Z3_get_decl_parameter_kind(self.ctx_refctx_ref(), self.astast, i)
799  if k == Z3_PARAMETER_INT:
800  result[i] = Z3_get_decl_int_parameter(self.ctx_refctx_ref(), self.astast, i)
801  elif k == Z3_PARAMETER_DOUBLE:
802  result[i] = Z3_get_decl_double_parameter(self.ctx_refctx_ref(), self.astast, i)
803  elif k == Z3_PARAMETER_RATIONAL:
804  result[i] = Z3_get_decl_rational_parameter(self.ctx_refctx_ref(), self.astast, i)
805  elif k == Z3_PARAMETER_SYMBOL:
806  result[i] = Z3_get_decl_symbol_parameter(self.ctx_refctx_ref(), self.astast, i)
807  elif k == Z3_PARAMETER_SORT:
808  result[i] = SortRef(Z3_get_decl_sort_parameter(self.ctx_refctx_ref(), self.astast, i), ctx)
809  elif k == Z3_PARAMETER_AST:
810  result[i] = ExprRef(Z3_get_decl_ast_parameter(self.ctx_refctx_ref(), self.astast, i), ctx)
811  elif k == Z3_PARAMETER_FUNC_DECL:
812  result[i] = FuncDeclRef(Z3_get_decl_func_decl_parameter(self.ctx_refctx_ref(), self.astast, 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.arityarity(), "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.domaindomain(i).cast(args[i])
845  saved.append(tmp)
846  _args[i] = tmp.as_ast()
847  return _to_expr_ref(Z3_mk_app(self.ctx_refctx_ref(), self.astast, len(args), _args), self.ctxctx)
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.astast
974 
975  def get_id(self):
976  return Z3_get_ast_id(self.ctx_refctx_ref(), self.as_astas_astas_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.ctxctx, self.as_astas_astas_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.sortsort().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_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
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_refctx_ref(), 2, _args), self.ctxctx)
1039 
1040  def params(self):
1041  return self.decldecl().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_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
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_refctx_ref(), self.as_astas_astas_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_argsnum_args(), "Invalid argument index")
1093  return _to_expr_ref(Z3_get_app_arg(self.ctx_refctx_ref(), self.as_astas_astas_ast(), idx), self.ctxctx)
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.argarg(i) for i in range(self.num_argsnum_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  if isinstance(a, float) and isinstance(b, ArithRef):
1211  a = RealVal(a, b.ctx)
1212  if isinstance(b, float) and isinstance(a, ArithRef):
1213  b = RealVal(b, a.ctx)
1214 
1215  s = None
1216  s = _coerce_expr_merge(s, a)
1217  s = _coerce_expr_merge(s, b)
1218  a = s.cast(a)
1219  b = s.cast(b)
1220  return (a, b)
1221 
1222 
1223 def _reduce(func, sequence, initial):
1224  result = initial
1225  for element in sequence:
1226  result = func(result, element)
1227  return result
1228 
1229 
1230 def _coerce_expr_list(alist, ctx=None):
1231  has_expr = False
1232  for a in alist:
1233  if is_expr(a):
1234  has_expr = True
1235  break
1236  if not has_expr:
1237  alist = [_py2expr(a, ctx) for a in alist]
1238  s = _reduce(_coerce_expr_merge, alist, None)
1239  return [s.cast(a) for a in alist]
1240 
1241 
1242 def is_expr(a):
1243  """Return `True` if `a` is a Z3 expression.
1244 
1245  >>> a = Int('a')
1246  >>> is_expr(a)
1247  True
1248  >>> is_expr(a + 1)
1249  True
1250  >>> is_expr(IntSort())
1251  False
1252  >>> is_expr(1)
1253  False
1254  >>> is_expr(IntVal(1))
1255  True
1256  >>> x = Int('x')
1257  >>> is_expr(ForAll(x, x >= 0))
1258  True
1259  >>> is_expr(FPVal(1.0))
1260  True
1261  """
1262  return isinstance(a, ExprRef)
1263 
1264 
1265 def is_app(a):
1266  """Return `True` if `a` is a Z3 function application.
1267 
1268  Note that, constants are function applications with 0 arguments.
1269 
1270  >>> a = Int('a')
1271  >>> is_app(a)
1272  True
1273  >>> is_app(a + 1)
1274  True
1275  >>> is_app(IntSort())
1276  False
1277  >>> is_app(1)
1278  False
1279  >>> is_app(IntVal(1))
1280  True
1281  >>> x = Int('x')
1282  >>> is_app(ForAll(x, x >= 0))
1283  False
1284  """
1285  if not isinstance(a, ExprRef):
1286  return False
1287  k = _ast_kind(a.ctx, a)
1288  return k == Z3_NUMERAL_AST or k == Z3_APP_AST
1289 
1290 
1291 def is_const(a):
1292  """Return `True` if `a` is Z3 constant/variable expression.
1293 
1294  >>> a = Int('a')
1295  >>> is_const(a)
1296  True
1297  >>> is_const(a + 1)
1298  False
1299  >>> is_const(1)
1300  False
1301  >>> is_const(IntVal(1))
1302  True
1303  >>> x = Int('x')
1304  >>> is_const(ForAll(x, x >= 0))
1305  False
1306  """
1307  return is_app(a) and a.num_args() == 0
1308 
1309 
1310 def is_var(a):
1311  """Return `True` if `a` is variable.
1312 
1313  Z3 uses de-Bruijn indices for representing bound variables in
1314  quantifiers.
1315 
1316  >>> x = Int('x')
1317  >>> is_var(x)
1318  False
1319  >>> is_const(x)
1320  True
1321  >>> f = Function('f', IntSort(), IntSort())
1322  >>> # Z3 replaces x with bound variables when ForAll is executed.
1323  >>> q = ForAll(x, f(x) == x)
1324  >>> b = q.body()
1325  >>> b
1326  f(Var(0)) == Var(0)
1327  >>> b.arg(1)
1328  Var(0)
1329  >>> is_var(b.arg(1))
1330  True
1331  """
1332  return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
1333 
1334 
1336  """Return the de-Bruijn index of the Z3 bounded variable `a`.
1337 
1338  >>> x = Int('x')
1339  >>> y = Int('y')
1340  >>> is_var(x)
1341  False
1342  >>> is_const(x)
1343  True
1344  >>> f = Function('f', IntSort(), IntSort(), IntSort())
1345  >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1346  >>> q = ForAll([x, y], f(x, y) == x + y)
1347  >>> q.body()
1348  f(Var(1), Var(0)) == Var(1) + Var(0)
1349  >>> b = q.body()
1350  >>> b.arg(0)
1351  f(Var(1), Var(0))
1352  >>> v1 = b.arg(0).arg(0)
1353  >>> v2 = b.arg(0).arg(1)
1354  >>> v1
1355  Var(1)
1356  >>> v2
1357  Var(0)
1358  >>> get_var_index(v1)
1359  1
1360  >>> get_var_index(v2)
1361  0
1362  """
1363  if z3_debug():
1364  _z3_assert(is_var(a), "Z3 bound variable expected")
1365  return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
1366 
1367 
1368 def is_app_of(a, k):
1369  """Return `True` if `a` is an application of the given kind `k`.
1370 
1371  >>> x = Int('x')
1372  >>> n = x + 1
1373  >>> is_app_of(n, Z3_OP_ADD)
1374  True
1375  >>> is_app_of(n, Z3_OP_MUL)
1376  False
1377  """
1378  return is_app(a) and a.decl().kind() == k
1379 
1380 
1381 def If(a, b, c, ctx=None):
1382  """Create a Z3 if-then-else expression.
1383 
1384  >>> x = Int('x')
1385  >>> y = Int('y')
1386  >>> max = If(x > y, x, y)
1387  >>> max
1388  If(x > y, x, y)
1389  >>> simplify(max)
1390  If(x <= y, y, x)
1391  """
1392  if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
1393  return Cond(a, b, c, ctx)
1394  else:
1395  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1396  s = BoolSort(ctx)
1397  a = s.cast(a)
1398  b, c = _coerce_exprs(b, c, ctx)
1399  if z3_debug():
1400  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1401  return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1402 
1403 
1404 def Distinct(*args):
1405  """Create a Z3 distinct expression.
1406 
1407  >>> x = Int('x')
1408  >>> y = Int('y')
1409  >>> Distinct(x, y)
1410  x != y
1411  >>> z = Int('z')
1412  >>> Distinct(x, y, z)
1413  Distinct(x, y, z)
1414  >>> simplify(Distinct(x, y, z))
1415  Distinct(x, y, z)
1416  >>> simplify(Distinct(x, y, z), blast_distinct=True)
1417  And(Not(x == y), Not(x == z), Not(y == z))
1418  """
1419  args = _get_args(args)
1420  ctx = _ctx_from_ast_arg_list(args)
1421  if z3_debug():
1422  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
1423  args = _coerce_expr_list(args, ctx)
1424  _args, sz = _to_ast_array(args)
1425  return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
1426 
1427 
1428 def _mk_bin(f, a, b):
1429  args = (Ast * 2)()
1430  if z3_debug():
1431  _z3_assert(a.ctx == b.ctx, "Context mismatch")
1432  args[0] = a.as_ast()
1433  args[1] = b.as_ast()
1434  return f(a.ctx.ref(), 2, args)
1435 
1436 
1437 def Const(name, sort):
1438  """Create a constant of the given sort.
1439 
1440  >>> Const('x', IntSort())
1441  x
1442  """
1443  if z3_debug():
1444  _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
1445  ctx = sort.ctx
1446  return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
1447 
1448 
1449 def Consts(names, sort):
1450  """Create several constants of the given sort.
1451 
1452  `names` is a string containing the names of all constants to be created.
1453  Blank spaces separate the names of different constants.
1454 
1455  >>> x, y, z = Consts('x y z', IntSort())
1456  >>> x + y + z
1457  x + y + z
1458  """
1459  if isinstance(names, str):
1460  names = names.split(" ")
1461  return [Const(name, sort) for name in names]
1462 
1463 
1464 def FreshConst(sort, prefix="c"):
1465  """Create a fresh constant of a specified sort"""
1466  ctx = _get_ctx(sort.ctx)
1467  return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
1468 
1469 
1470 def Var(idx, s):
1471  """Create a Z3 free variable. Free variables are used to create quantified formulas.
1472  A free variable with index n is bound when it occurs within the scope of n+1 quantified
1473  declarations.
1474 
1475  >>> Var(0, IntSort())
1476  Var(0)
1477  >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1478  False
1479  """
1480  if z3_debug():
1481  _z3_assert(is_sort(s), "Z3 sort expected")
1482  return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1483 
1484 
1485 def RealVar(idx, ctx=None):
1486  """
1487  Create a real free variable. Free variables are used to create quantified formulas.
1488  They are also used to create polynomials.
1489 
1490  >>> RealVar(0)
1491  Var(0)
1492  """
1493  return Var(idx, RealSort(ctx))
1494 
1495 
1496 def RealVarVector(n, ctx=None):
1497  """
1498  Create a list of Real free variables.
1499  The variables have ids: 0, 1, ..., n-1
1500 
1501  >>> x0, x1, x2, x3 = RealVarVector(4)
1502  >>> x2
1503  Var(2)
1504  """
1505  return [RealVar(i, ctx) for i in range(n)]
1506 
1507 
1512 
1513 
1515  """Boolean sort."""
1516 
1517  def cast(self, val):
1518  """Try to cast `val` as a Boolean.
1519 
1520  >>> x = BoolSort().cast(True)
1521  >>> x
1522  True
1523  >>> is_expr(x)
1524  True
1525  >>> is_expr(True)
1526  False
1527  >>> x.sort()
1528  Bool
1529  """
1530  if isinstance(val, bool):
1531  return BoolVal(val, self.ctxctx)
1532  if z3_debug():
1533  if not is_expr(val):
1534  msg = "True, False or Z3 Boolean expression expected. Received %s of type %s"
1535  _z3_assert(is_expr(val), msg % (val, type(val)))
1536  if not self.eqeq(val.sort()):
1537  _z3_assert(self.eqeq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
1538  return val
1539 
1540  def subsort(self, other):
1541  return isinstance(other, ArithSortRef)
1542 
1543  def is_int(self):
1544  return True
1545 
1546  def is_bool(self):
1547  return True
1548 
1549 
1551  """All Boolean expressions are instances of this class."""
1552 
1553  def sort(self):
1554  return BoolSortRef(Z3_get_sort(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
1555 
1556  def __rmul__(self, other):
1557  return self * other
1558 
1559  def __mul__(self, other):
1560  """Create the Z3 expression `self * other`.
1561  """
1562  if isinstance(other, int) and other == 1:
1563  return If(self, 1, 0)
1564  if isinstance(other, int) and other == 0:
1565  return IntVal(0, self.ctxctx)
1566  if isinstance(other, BoolRef):
1567  other = If(other, 1, 0)
1568  return If(self, other, 0)
1569 
1570 
1571 def is_bool(a):
1572  """Return `True` if `a` is a Z3 Boolean expression.
1573 
1574  >>> p = Bool('p')
1575  >>> is_bool(p)
1576  True
1577  >>> q = Bool('q')
1578  >>> is_bool(And(p, q))
1579  True
1580  >>> x = Real('x')
1581  >>> is_bool(x)
1582  False
1583  >>> is_bool(x == 0)
1584  True
1585  """
1586  return isinstance(a, BoolRef)
1587 
1588 
1589 def is_true(a):
1590  """Return `True` if `a` is the Z3 true expression.
1591 
1592  >>> p = Bool('p')
1593  >>> is_true(p)
1594  False
1595  >>> is_true(simplify(p == p))
1596  True
1597  >>> x = Real('x')
1598  >>> is_true(x == 0)
1599  False
1600  >>> # True is a Python Boolean expression
1601  >>> is_true(True)
1602  False
1603  """
1604  return is_app_of(a, Z3_OP_TRUE)
1605 
1606 
1607 def is_false(a):
1608  """Return `True` if `a` is the Z3 false expression.
1609 
1610  >>> p = Bool('p')
1611  >>> is_false(p)
1612  False
1613  >>> is_false(False)
1614  False
1615  >>> is_false(BoolVal(False))
1616  True
1617  """
1618  return is_app_of(a, Z3_OP_FALSE)
1619 
1620 
1621 def is_and(a):
1622  """Return `True` if `a` is a Z3 and expression.
1623 
1624  >>> p, q = Bools('p q')
1625  >>> is_and(And(p, q))
1626  True
1627  >>> is_and(Or(p, q))
1628  False
1629  """
1630  return is_app_of(a, Z3_OP_AND)
1631 
1632 
1633 def is_or(a):
1634  """Return `True` if `a` is a Z3 or expression.
1635 
1636  >>> p, q = Bools('p q')
1637  >>> is_or(Or(p, q))
1638  True
1639  >>> is_or(And(p, q))
1640  False
1641  """
1642  return is_app_of(a, Z3_OP_OR)
1643 
1644 
1645 def is_implies(a):
1646  """Return `True` if `a` is a Z3 implication expression.
1647 
1648  >>> p, q = Bools('p q')
1649  >>> is_implies(Implies(p, q))
1650  True
1651  >>> is_implies(And(p, q))
1652  False
1653  """
1654  return is_app_of(a, Z3_OP_IMPLIES)
1655 
1656 
1657 def is_not(a):
1658  """Return `True` if `a` is a Z3 not expression.
1659 
1660  >>> p = Bool('p')
1661  >>> is_not(p)
1662  False
1663  >>> is_not(Not(p))
1664  True
1665  """
1666  return is_app_of(a, Z3_OP_NOT)
1667 
1668 
1669 def is_eq(a):
1670  """Return `True` if `a` is a Z3 equality expression.
1671 
1672  >>> x, y = Ints('x y')
1673  >>> is_eq(x == y)
1674  True
1675  """
1676  return is_app_of(a, Z3_OP_EQ)
1677 
1678 
1680  """Return `True` if `a` is a Z3 distinct expression.
1681 
1682  >>> x, y, z = Ints('x y z')
1683  >>> is_distinct(x == y)
1684  False
1685  >>> is_distinct(Distinct(x, y, z))
1686  True
1687  """
1688  return is_app_of(a, Z3_OP_DISTINCT)
1689 
1690 
1691 def BoolSort(ctx=None):
1692  """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1693 
1694  >>> BoolSort()
1695  Bool
1696  >>> p = Const('p', BoolSort())
1697  >>> is_bool(p)
1698  True
1699  >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1700  >>> r(0, 1)
1701  r(0, 1)
1702  >>> is_bool(r(0, 1))
1703  True
1704  """
1705  ctx = _get_ctx(ctx)
1706  return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1707 
1708 
1709 def BoolVal(val, ctx=None):
1710  """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1711 
1712  >>> BoolVal(True)
1713  True
1714  >>> is_true(BoolVal(True))
1715  True
1716  >>> is_true(True)
1717  False
1718  >>> is_false(BoolVal(False))
1719  True
1720  """
1721  ctx = _get_ctx(ctx)
1722  if val:
1723  return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1724  else:
1725  return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1726 
1727 
1728 def Bool(name, ctx=None):
1729  """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1730 
1731  >>> p = Bool('p')
1732  >>> q = Bool('q')
1733  >>> And(p, q)
1734  And(p, q)
1735  """
1736  ctx = _get_ctx(ctx)
1737  return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1738 
1739 
1740 def Bools(names, ctx=None):
1741  """Return a tuple of Boolean constants.
1742 
1743  `names` is a single string containing all names separated by blank spaces.
1744  If `ctx=None`, then the global context is used.
1745 
1746  >>> p, q, r = Bools('p q r')
1747  >>> And(p, Or(q, r))
1748  And(p, Or(q, r))
1749  """
1750  ctx = _get_ctx(ctx)
1751  if isinstance(names, str):
1752  names = names.split(" ")
1753  return [Bool(name, ctx) for name in names]
1754 
1755 
1756 def BoolVector(prefix, sz, ctx=None):
1757  """Return a list of Boolean constants of size `sz`.
1758 
1759  The constants are named using the given prefix.
1760  If `ctx=None`, then the global context is used.
1761 
1762  >>> P = BoolVector('p', 3)
1763  >>> P
1764  [p__0, p__1, p__2]
1765  >>> And(P)
1766  And(p__0, p__1, p__2)
1767  """
1768  return [Bool("%s__%s" % (prefix, i)) for i in range(sz)]
1769 
1770 
1771 def FreshBool(prefix="b", ctx=None):
1772  """Return a fresh Boolean constant in the given context using the given prefix.
1773 
1774  If `ctx=None`, then the global context is used.
1775 
1776  >>> b1 = FreshBool()
1777  >>> b2 = FreshBool()
1778  >>> eq(b1, b2)
1779  False
1780  """
1781  ctx = _get_ctx(ctx)
1782  return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1783 
1784 
1785 def Implies(a, b, ctx=None):
1786  """Create a Z3 implies expression.
1787 
1788  >>> p, q = Bools('p q')
1789  >>> Implies(p, q)
1790  Implies(p, q)
1791  """
1792  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1793  s = BoolSort(ctx)
1794  a = s.cast(a)
1795  b = s.cast(b)
1796  return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1797 
1798 
1799 def Xor(a, b, ctx=None):
1800  """Create a Z3 Xor expression.
1801 
1802  >>> p, q = Bools('p q')
1803  >>> Xor(p, q)
1804  Xor(p, q)
1805  >>> simplify(Xor(p, q))
1806  Not(p == q)
1807  """
1808  ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1809  s = BoolSort(ctx)
1810  a = s.cast(a)
1811  b = s.cast(b)
1812  return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1813 
1814 
1815 def Not(a, ctx=None):
1816  """Create a Z3 not expression or probe.
1817 
1818  >>> p = Bool('p')
1819  >>> Not(Not(p))
1820  Not(Not(p))
1821  >>> simplify(Not(Not(p)))
1822  p
1823  """
1824  ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1825  if is_probe(a):
1826  # Not is also used to build probes
1827  return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
1828  else:
1829  s = BoolSort(ctx)
1830  a = s.cast(a)
1831  return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
1832 
1833 
1834 def mk_not(a):
1835  if is_not(a):
1836  return a.arg(0)
1837  else:
1838  return Not(a)
1839 
1840 
1841 def _has_probe(args):
1842  """Return `True` if one of the elements of the given collection is a Z3 probe."""
1843  for arg in args:
1844  if is_probe(arg):
1845  return True
1846  return False
1847 
1848 
1849 def And(*args):
1850  """Create a Z3 and-expression or and-probe.
1851 
1852  >>> p, q, r = Bools('p q r')
1853  >>> And(p, q, r)
1854  And(p, q, r)
1855  >>> P = BoolVector('p', 5)
1856  >>> And(P)
1857  And(p__0, p__1, p__2, p__3, p__4)
1858  """
1859  last_arg = None
1860  if len(args) > 0:
1861  last_arg = args[len(args) - 1]
1862  if isinstance(last_arg, Context):
1863  ctx = args[len(args) - 1]
1864  args = args[:len(args) - 1]
1865  elif len(args) == 1 and isinstance(args[0], AstVector):
1866  ctx = args[0].ctx
1867  args = [a for a in args[0]]
1868  else:
1869  ctx = None
1870  args = _get_args(args)
1871  ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1872  if z3_debug():
1873  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1874  if _has_probe(args):
1875  return _probe_and(args, ctx)
1876  else:
1877  args = _coerce_expr_list(args, ctx)
1878  _args, sz = _to_ast_array(args)
1879  return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1880 
1881 
1882 def Or(*args):
1883  """Create a Z3 or-expression or or-probe.
1884 
1885  >>> p, q, r = Bools('p q r')
1886  >>> Or(p, q, r)
1887  Or(p, q, r)
1888  >>> P = BoolVector('p', 5)
1889  >>> Or(P)
1890  Or(p__0, p__1, p__2, p__3, p__4)
1891  """
1892  last_arg = None
1893  if len(args) > 0:
1894  last_arg = args[len(args) - 1]
1895  if isinstance(last_arg, Context):
1896  ctx = args[len(args) - 1]
1897  args = args[:len(args) - 1]
1898  elif len(args) == 1 and isinstance(args[0], AstVector):
1899  ctx = args[0].ctx
1900  args = [a for a in args[0]]
1901  else:
1902  ctx = None
1903  args = _get_args(args)
1904  ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1905  if z3_debug():
1906  _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1907  if _has_probe(args):
1908  return _probe_or(args, ctx)
1909  else:
1910  args = _coerce_expr_list(args, ctx)
1911  _args, sz = _to_ast_array(args)
1912  return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
1913 
1914 
1919 
1920 
1922  """Patterns are hints for quantifier instantiation.
1923 
1924  """
1925 
1926  def as_ast(self):
1927  return Z3_pattern_to_ast(self.ctx_refctx_ref(), self.astast)
1928 
1929  def get_id(self):
1930  return Z3_get_ast_id(self.ctx_refctx_ref(), self.as_astas_astas_astas_ast())
1931 
1932 
1933 def is_pattern(a):
1934  """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1935 
1936  >>> f = Function('f', IntSort(), IntSort())
1937  >>> x = Int('x')
1938  >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1939  >>> q
1940  ForAll(x, f(x) == 0)
1941  >>> q.num_patterns()
1942  1
1943  >>> is_pattern(q.pattern(0))
1944  True
1945  >>> q.pattern(0)
1946  f(Var(0))
1947  """
1948  return isinstance(a, PatternRef)
1949 
1950 
1951 def MultiPattern(*args):
1952  """Create a Z3 multi-pattern using the given expressions `*args`
1953 
1954  >>> f = Function('f', IntSort(), IntSort())
1955  >>> g = Function('g', IntSort(), IntSort())
1956  >>> x = Int('x')
1957  >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1958  >>> q
1959  ForAll(x, f(x) != g(x))
1960  >>> q.num_patterns()
1961  1
1962  >>> is_pattern(q.pattern(0))
1963  True
1964  >>> q.pattern(0)
1965  MultiPattern(f(Var(0)), g(Var(0)))
1966  """
1967  if z3_debug():
1968  _z3_assert(len(args) > 0, "At least one argument expected")
1969  _z3_assert(all([is_expr(a) for a in args]), "Z3 expressions expected")
1970  ctx = args[0].ctx
1971  args, sz = _to_ast_array(args)
1972  return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
1973 
1974 
1975 def _to_pattern(arg):
1976  if is_pattern(arg):
1977  return arg
1978  else:
1979  return MultiPattern(arg)
1980 
1981 
1986 
1987 
1989  """Universally and Existentially quantified formulas."""
1990 
1991  def as_ast(self):
1992  return self.astast
1993 
1994  def get_id(self):
1995  return Z3_get_ast_id(self.ctx_refctx_ref(), self.as_astas_astas_astas_ast())
1996 
1997  def sort(self):
1998  """Return the Boolean sort or sort of Lambda."""
1999  if self.is_lambdais_lambda():
2000  return _sort(self.ctxctx, self.as_astas_astas_astas_ast())
2001  return BoolSort(self.ctxctx)
2002 
2003  def is_forall(self):
2004  """Return `True` if `self` is a universal quantifier.
2005 
2006  >>> f = Function('f', IntSort(), IntSort())
2007  >>> x = Int('x')
2008  >>> q = ForAll(x, f(x) == 0)
2009  >>> q.is_forall()
2010  True
2011  >>> q = Exists(x, f(x) != 0)
2012  >>> q.is_forall()
2013  False
2014  """
2015  return Z3_is_quantifier_forall(self.ctx_refctx_ref(), self.astast)
2016 
2017  def is_exists(self):
2018  """Return `True` if `self` is an existential quantifier.
2019 
2020  >>> f = Function('f', IntSort(), IntSort())
2021  >>> x = Int('x')
2022  >>> q = ForAll(x, f(x) == 0)
2023  >>> q.is_exists()
2024  False
2025  >>> q = Exists(x, f(x) != 0)
2026  >>> q.is_exists()
2027  True
2028  """
2029  return Z3_is_quantifier_exists(self.ctx_refctx_ref(), self.astast)
2030 
2031  def is_lambda(self):
2032  """Return `True` if `self` is a lambda expression.
2033 
2034  >>> f = Function('f', IntSort(), IntSort())
2035  >>> x = Int('x')
2036  >>> q = Lambda(x, f(x))
2037  >>> q.is_lambda()
2038  True
2039  >>> q = Exists(x, f(x) != 0)
2040  >>> q.is_lambda()
2041  False
2042  """
2043  return Z3_is_lambda(self.ctx_refctx_ref(), self.astast)
2044 
2045  def __getitem__(self, arg):
2046  """Return the Z3 expression `self[arg]`.
2047  """
2048  if z3_debug():
2049  _z3_assert(self.is_lambdais_lambda(), "quantifier should be a lambda expression")
2050  return _array_select(self, arg)
2051 
2052  def weight(self):
2053  """Return the weight annotation of `self`.
2054 
2055  >>> f = Function('f', IntSort(), IntSort())
2056  >>> x = Int('x')
2057  >>> q = ForAll(x, f(x) == 0)
2058  >>> q.weight()
2059  1
2060  >>> q = ForAll(x, f(x) == 0, weight=10)
2061  >>> q.weight()
2062  10
2063  """
2064  return int(Z3_get_quantifier_weight(self.ctx_refctx_ref(), self.astast))
2065 
2066  def num_patterns(self):
2067  """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
2068 
2069  >>> f = Function('f', IntSort(), IntSort())
2070  >>> g = Function('g', IntSort(), IntSort())
2071  >>> x = Int('x')
2072  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2073  >>> q.num_patterns()
2074  2
2075  """
2076  return int(Z3_get_quantifier_num_patterns(self.ctx_refctx_ref(), self.astast))
2077 
2078  def pattern(self, idx):
2079  """Return a pattern (i.e., quantifier instantiation hints) in `self`.
2080 
2081  >>> f = Function('f', IntSort(), IntSort())
2082  >>> g = Function('g', IntSort(), IntSort())
2083  >>> x = Int('x')
2084  >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2085  >>> q.num_patterns()
2086  2
2087  >>> q.pattern(0)
2088  f(Var(0))
2089  >>> q.pattern(1)
2090  g(Var(0))
2091  """
2092  if z3_debug():
2093  _z3_assert(idx < self.num_patternsnum_patterns(), "Invalid pattern idx")
2094  return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_refctx_ref(), self.astast, idx), self.ctxctx)
2095 
2096  def num_no_patterns(self):
2097  """Return the number of no-patterns."""
2098  return Z3_get_quantifier_num_no_patterns(self.ctx_refctx_ref(), self.astast)
2099 
2100  def no_pattern(self, idx):
2101  """Return a no-pattern."""
2102  if z3_debug():
2103  _z3_assert(idx < self.num_no_patternsnum_no_patterns(), "Invalid no-pattern idx")
2104  return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_refctx_ref(), self.astast, idx), self.ctxctx)
2105 
2106  def body(self):
2107  """Return the expression being quantified.
2108 
2109  >>> f = Function('f', IntSort(), IntSort())
2110  >>> x = Int('x')
2111  >>> q = ForAll(x, f(x) == 0)
2112  >>> q.body()
2113  f(Var(0)) == 0
2114  """
2115  return _to_expr_ref(Z3_get_quantifier_body(self.ctx_refctx_ref(), self.astast), self.ctxctx)
2116 
2117  def num_vars(self):
2118  """Return the number of variables bounded by this quantifier.
2119 
2120  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2121  >>> x = Int('x')
2122  >>> y = Int('y')
2123  >>> q = ForAll([x, y], f(x, y) >= x)
2124  >>> q.num_vars()
2125  2
2126  """
2127  return int(Z3_get_quantifier_num_bound(self.ctx_refctx_ref(), self.astast))
2128 
2129  def var_name(self, idx):
2130  """Return a string representing a name used when displaying the quantifier.
2131 
2132  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2133  >>> x = Int('x')
2134  >>> y = Int('y')
2135  >>> q = ForAll([x, y], f(x, y) >= x)
2136  >>> q.var_name(0)
2137  'x'
2138  >>> q.var_name(1)
2139  'y'
2140  """
2141  if z3_debug():
2142  _z3_assert(idx < self.num_varsnum_vars(), "Invalid variable idx")
2143  return _symbol2py(self.ctxctx, Z3_get_quantifier_bound_name(self.ctx_refctx_ref(), self.astast, idx))
2144 
2145  def var_sort(self, idx):
2146  """Return the sort of a bound variable.
2147 
2148  >>> f = Function('f', IntSort(), RealSort(), IntSort())
2149  >>> x = Int('x')
2150  >>> y = Real('y')
2151  >>> q = ForAll([x, y], f(x, y) >= x)
2152  >>> q.var_sort(0)
2153  Int
2154  >>> q.var_sort(1)
2155  Real
2156  """
2157  if z3_debug():
2158  _z3_assert(idx < self.num_varsnum_vars(), "Invalid variable idx")
2159  return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_refctx_ref(), self.astast, idx), self.ctxctx)
2160 
2161  def children(self):
2162  """Return a list containing a single element self.body()
2163 
2164  >>> f = Function('f', IntSort(), IntSort())
2165  >>> x = Int('x')
2166  >>> q = ForAll(x, f(x) == 0)
2167  >>> q.children()
2168  [f(Var(0)) == 0]
2169  """
2170  return [self.bodybody()]
2171 
2172 
2174  """Return `True` if `a` is a Z3 quantifier.
2175 
2176  >>> f = Function('f', IntSort(), IntSort())
2177  >>> x = Int('x')
2178  >>> q = ForAll(x, f(x) == 0)
2179  >>> is_quantifier(q)
2180  True
2181  >>> is_quantifier(f(x))
2182  False
2183  """
2184  return isinstance(a, QuantifierRef)
2185 
2186 
2187 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2188  if z3_debug():
2189  _z3_assert(is_bool(body) or is_app(vs) or (len(vs) > 0 and is_app(vs[0])), "Z3 expression expected")
2190  _z3_assert(is_const(vs) or (len(vs) > 0 and all([is_const(v) for v in vs])), "Invalid bounded variable(s)")
2191  _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected")
2192  _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions")
2193  if is_app(vs):
2194  ctx = vs.ctx
2195  vs = [vs]
2196  else:
2197  ctx = vs[0].ctx
2198  if not is_expr(body):
2199  body = BoolVal(body, ctx)
2200  num_vars = len(vs)
2201  if num_vars == 0:
2202  return body
2203  _vs = (Ast * num_vars)()
2204  for i in range(num_vars):
2205  # TODO: Check if is constant
2206  _vs[i] = vs[i].as_ast()
2207  patterns = [_to_pattern(p) for p in patterns]
2208  num_pats = len(patterns)
2209  _pats = (Pattern * num_pats)()
2210  for i in range(num_pats):
2211  _pats[i] = patterns[i].ast
2212  _no_pats, num_no_pats = _to_ast_array(no_patterns)
2213  qid = to_symbol(qid, ctx)
2214  skid = to_symbol(skid, ctx)
2215  return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid,
2216  num_vars, _vs,
2217  num_pats, _pats,
2218  num_no_pats, _no_pats,
2219  body.as_ast()), ctx)
2220 
2221 
2222 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2223  """Create a Z3 forall formula.
2224 
2225  The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2226 
2227  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2228  >>> x = Int('x')
2229  >>> y = Int('y')
2230  >>> ForAll([x, y], f(x, y) >= x)
2231  ForAll([x, y], f(x, y) >= x)
2232  >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2233  ForAll([x, y], f(x, y) >= x)
2234  >>> ForAll([x, y], f(x, y) >= x, weight=10)
2235  ForAll([x, y], f(x, y) >= x)
2236  """
2237  return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
2238 
2239 
2240 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2241  """Create a Z3 exists formula.
2242 
2243  The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2244 
2245 
2246  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2247  >>> x = Int('x')
2248  >>> y = Int('y')
2249  >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2250  >>> q
2251  Exists([x, y], f(x, y) >= x)
2252  >>> is_quantifier(q)
2253  True
2254  >>> r = Tactic('nnf')(q).as_expr()
2255  >>> is_quantifier(r)
2256  False
2257  """
2258  return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
2259 
2260 
2261 def Lambda(vs, body):
2262  """Create a Z3 lambda expression.
2263 
2264  >>> f = Function('f', IntSort(), IntSort(), IntSort())
2265  >>> mem0 = Array('mem0', IntSort(), IntSort())
2266  >>> lo, hi, e, i = Ints('lo hi e i')
2267  >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
2268  >>> mem1
2269  Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
2270  """
2271  ctx = body.ctx
2272  if is_app(vs):
2273  vs = [vs]
2274  num_vars = len(vs)
2275  _vs = (Ast * num_vars)()
2276  for i in range(num_vars):
2277  # TODO: Check if is constant
2278  _vs[i] = vs[i].as_ast()
2279  return QuantifierRef(Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx)
2280 
2281 
2286 
2287 
2289  """Real and Integer sorts."""
2290 
2291  def is_real(self):
2292  """Return `True` if `self` is of the sort Real.
2293 
2294  >>> x = Real('x')
2295  >>> x.is_real()
2296  True
2297  >>> (x + 1).is_real()
2298  True
2299  >>> x = Int('x')
2300  >>> x.is_real()
2301  False
2302  """
2303  return self.kindkind() == Z3_REAL_SORT
2304 
2305  def is_int(self):
2306  """Return `True` if `self` is of the sort Integer.
2307 
2308  >>> x = Int('x')
2309  >>> x.is_int()
2310  True
2311  >>> (x + 1).is_int()
2312  True
2313  >>> x = Real('x')
2314  >>> x.is_int()
2315  False
2316  """
2317  return self.kindkind() == Z3_INT_SORT
2318 
2319  def is_bool(self):
2320  return False
2321 
2322  def subsort(self, other):
2323  """Return `True` if `self` is a subsort of `other`."""
2324  return self.is_intis_int() and is_arith_sort(other) and other.is_real()
2325 
2326  def cast(self, val):
2327  """Try to cast `val` as an Integer or Real.
2328 
2329  >>> IntSort().cast(10)
2330  10
2331  >>> is_int(IntSort().cast(10))
2332  True
2333  >>> is_int(10)
2334  False
2335  >>> RealSort().cast(10)
2336  10
2337  >>> is_real(RealSort().cast(10))
2338  True
2339  """
2340  if is_expr(val):
2341  if z3_debug():
2342  _z3_assert(self.ctxctxctx == val.ctx, "Context mismatch")
2343  val_s = val.sort()
2344  if self.eqeq(val_s):
2345  return val
2346  if val_s.is_int() and self.is_realis_real():
2347  return ToReal(val)
2348  if val_s.is_bool() and self.is_intis_int():
2349  return If(val, 1, 0)
2350  if val_s.is_bool() and self.is_realis_real():
2351  return ToReal(If(val, 1, 0))
2352  if z3_debug():
2353  _z3_assert(False, "Z3 Integer/Real expression expected")
2354  else:
2355  if self.is_intis_int():
2356  return IntVal(val, self.ctxctxctx)
2357  if self.is_realis_real():
2358  return RealVal(val, self.ctxctxctx)
2359  if z3_debug():
2360  msg = "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s"
2361  _z3_assert(False, msg % self)
2362 
2363 
2365  """Return `True` if s is an arithmetical sort (type).
2366 
2367  >>> is_arith_sort(IntSort())
2368  True
2369  >>> is_arith_sort(RealSort())
2370  True
2371  >>> is_arith_sort(BoolSort())
2372  False
2373  >>> n = Int('x') + 1
2374  >>> is_arith_sort(n.sort())
2375  True
2376  """
2377  return isinstance(s, ArithSortRef)
2378 
2379 
2381  """Integer and Real expressions."""
2382 
2383  def sort(self):
2384  """Return the sort (type) of the arithmetical expression `self`.
2385 
2386  >>> Int('x').sort()
2387  Int
2388  >>> (Real('x') + 1).sort()
2389  Real
2390  """
2391  return ArithSortRef(Z3_get_sort(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
2392 
2393  def is_int(self):
2394  """Return `True` if `self` is an integer expression.
2395 
2396  >>> x = Int('x')
2397  >>> x.is_int()
2398  True
2399  >>> (x + 1).is_int()
2400  True
2401  >>> y = Real('y')
2402  >>> (x + y).is_int()
2403  False
2404  """
2405  return self.sortsortsort().is_int()
2406 
2407  def is_real(self):
2408  """Return `True` if `self` is an real expression.
2409 
2410  >>> x = Real('x')
2411  >>> x.is_real()
2412  True
2413  >>> (x + 1).is_real()
2414  True
2415  """
2416  return self.sortsortsort().is_real()
2417 
2418  def __add__(self, other):
2419  """Create the Z3 expression `self + other`.
2420 
2421  >>> x = Int('x')
2422  >>> y = Int('y')
2423  >>> x + y
2424  x + y
2425  >>> (x + y).sort()
2426  Int
2427  """
2428  a, b = _coerce_exprs(self, other)
2429  return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctxctx)
2430 
2431  def __radd__(self, other):
2432  """Create the Z3 expression `other + self`.
2433 
2434  >>> x = Int('x')
2435  >>> 10 + x
2436  10 + x
2437  """
2438  a, b = _coerce_exprs(self, other)
2439  return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctxctx)
2440 
2441  def __mul__(self, other):
2442  """Create the Z3 expression `self * other`.
2443 
2444  >>> x = Real('x')
2445  >>> y = Real('y')
2446  >>> x * y
2447  x*y
2448  >>> (x * y).sort()
2449  Real
2450  """
2451  if isinstance(other, BoolRef):
2452  return If(other, self, 0)
2453  a, b = _coerce_exprs(self, other)
2454  return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctxctx)
2455 
2456  def __rmul__(self, other):
2457  """Create the Z3 expression `other * self`.
2458 
2459  >>> x = Real('x')
2460  >>> 10 * x
2461  10*x
2462  """
2463  a, b = _coerce_exprs(self, other)
2464  return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctxctx)
2465 
2466  def __sub__(self, other):
2467  """Create the Z3 expression `self - other`.
2468 
2469  >>> x = Int('x')
2470  >>> y = Int('y')
2471  >>> x - y
2472  x - y
2473  >>> (x - y).sort()
2474  Int
2475  """
2476  a, b = _coerce_exprs(self, other)
2477  return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctxctx)
2478 
2479  def __rsub__(self, other):
2480  """Create the Z3 expression `other - self`.
2481 
2482  >>> x = Int('x')
2483  >>> 10 - x
2484  10 - x
2485  """
2486  a, b = _coerce_exprs(self, other)
2487  return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctxctx)
2488 
2489  def __pow__(self, other):
2490  """Create the Z3 expression `self**other` (** is the power operator).
2491 
2492  >>> x = Real('x')
2493  >>> x**3
2494  x**3
2495  >>> (x**3).sort()
2496  Real
2497  >>> simplify(IntVal(2)**8)
2498  256
2499  """
2500  a, b = _coerce_exprs(self, other)
2501  return ArithRef(Z3_mk_power(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
2502 
2503  def __rpow__(self, other):
2504  """Create the Z3 expression `other**self` (** is the power operator).
2505 
2506  >>> x = Real('x')
2507  >>> 2**x
2508  2**x
2509  >>> (2**x).sort()
2510  Real
2511  >>> simplify(2**IntVal(8))
2512  256
2513  """
2514  a, b = _coerce_exprs(self, other)
2515  return ArithRef(Z3_mk_power(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
2516 
2517  def __div__(self, other):
2518  """Create the Z3 expression `other/self`.
2519 
2520  >>> x = Int('x')
2521  >>> y = Int('y')
2522  >>> x/y
2523  x/y
2524  >>> (x/y).sort()
2525  Int
2526  >>> (x/y).sexpr()
2527  '(div x y)'
2528  >>> x = Real('x')
2529  >>> y = Real('y')
2530  >>> x/y
2531  x/y
2532  >>> (x/y).sort()
2533  Real
2534  >>> (x/y).sexpr()
2535  '(/ x y)'
2536  """
2537  a, b = _coerce_exprs(self, other)
2538  return ArithRef(Z3_mk_div(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
2539 
2540  def __truediv__(self, other):
2541  """Create the Z3 expression `other/self`."""
2542  return self.__div____div__(other)
2543 
2544  def __rdiv__(self, other):
2545  """Create the Z3 expression `other/self`.
2546 
2547  >>> x = Int('x')
2548  >>> 10/x
2549  10/x
2550  >>> (10/x).sexpr()
2551  '(div 10 x)'
2552  >>> x = Real('x')
2553  >>> 10/x
2554  10/x
2555  >>> (10/x).sexpr()
2556  '(/ 10.0 x)'
2557  """
2558  a, b = _coerce_exprs(self, other)
2559  return ArithRef(Z3_mk_div(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
2560 
2561  def __rtruediv__(self, other):
2562  """Create the Z3 expression `other/self`."""
2563  return self.__rdiv____rdiv__(other)
2564 
2565  def __mod__(self, other):
2566  """Create the Z3 expression `other%self`.
2567 
2568  >>> x = Int('x')
2569  >>> y = Int('y')
2570  >>> x % y
2571  x%y
2572  >>> simplify(IntVal(10) % IntVal(3))
2573  1
2574  """
2575  a, b = _coerce_exprs(self, other)
2576  if z3_debug():
2577  _z3_assert(a.is_int(), "Z3 integer expression expected")
2578  return ArithRef(Z3_mk_mod(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
2579 
2580  def __rmod__(self, other):
2581  """Create the Z3 expression `other%self`.
2582 
2583  >>> x = Int('x')
2584  >>> 10 % x
2585  10%x
2586  """
2587  a, b = _coerce_exprs(self, other)
2588  if z3_debug():
2589  _z3_assert(a.is_int(), "Z3 integer expression expected")
2590  return ArithRef(Z3_mk_mod(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
2591 
2592  def __neg__(self):
2593  """Return an expression representing `-self`.
2594 
2595  >>> x = Int('x')
2596  >>> -x
2597  -x
2598  >>> simplify(-(-x))
2599  x
2600  """
2601  return ArithRef(Z3_mk_unary_minus(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
2602 
2603  def __pos__(self):
2604  """Return `self`.
2605 
2606  >>> x = Int('x')
2607  >>> +x
2608  x
2609  """
2610  return self
2611 
2612  def __le__(self, other):
2613  """Create the Z3 expression `other <= self`.
2614 
2615  >>> x, y = Ints('x y')
2616  >>> x <= y
2617  x <= y
2618  >>> y = Real('y')
2619  >>> x <= y
2620  ToReal(x) <= y
2621  """
2622  a, b = _coerce_exprs(self, other)
2623  return BoolRef(Z3_mk_le(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
2624 
2625  def __lt__(self, other):
2626  """Create the Z3 expression `other < self`.
2627 
2628  >>> x, y = Ints('x y')
2629  >>> x < y
2630  x < y
2631  >>> y = Real('y')
2632  >>> x < y
2633  ToReal(x) < y
2634  """
2635  a, b = _coerce_exprs(self, other)
2636  return BoolRef(Z3_mk_lt(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
2637 
2638  def __gt__(self, other):
2639  """Create the Z3 expression `other > self`.
2640 
2641  >>> x, y = Ints('x y')
2642  >>> x > y
2643  x > y
2644  >>> y = Real('y')
2645  >>> x > y
2646  ToReal(x) > y
2647  """
2648  a, b = _coerce_exprs(self, other)
2649  return BoolRef(Z3_mk_gt(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
2650 
2651  def __ge__(self, other):
2652  """Create the Z3 expression `other >= self`.
2653 
2654  >>> x, y = Ints('x y')
2655  >>> x >= y
2656  x >= y
2657  >>> y = Real('y')
2658  >>> x >= y
2659  ToReal(x) >= y
2660  """
2661  a, b = _coerce_exprs(self, other)
2662  return BoolRef(Z3_mk_ge(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
2663 
2664 
2665 def is_arith(a):
2666  """Return `True` if `a` is an arithmetical expression.
2667 
2668  >>> x = Int('x')
2669  >>> is_arith(x)
2670  True
2671  >>> is_arith(x + 1)
2672  True
2673  >>> is_arith(1)
2674  False
2675  >>> is_arith(IntVal(1))
2676  True
2677  >>> y = Real('y')
2678  >>> is_arith(y)
2679  True
2680  >>> is_arith(y + 1)
2681  True
2682  """
2683  return isinstance(a, ArithRef)
2684 
2685 
2686 def is_int(a):
2687  """Return `True` if `a` is an integer expression.
2688 
2689  >>> x = Int('x')
2690  >>> is_int(x + 1)
2691  True
2692  >>> is_int(1)
2693  False
2694  >>> is_int(IntVal(1))
2695  True
2696  >>> y = Real('y')
2697  >>> is_int(y)
2698  False
2699  >>> is_int(y + 1)
2700  False
2701  """
2702  return is_arith(a) and a.is_int()
2703 
2704 
2705 def is_real(a):
2706  """Return `True` if `a` is a real expression.
2707 
2708  >>> x = Int('x')
2709  >>> is_real(x + 1)
2710  False
2711  >>> y = Real('y')
2712  >>> is_real(y)
2713  True
2714  >>> is_real(y + 1)
2715  True
2716  >>> is_real(1)
2717  False
2718  >>> is_real(RealVal(1))
2719  True
2720  """
2721  return is_arith(a) and a.is_real()
2722 
2723 
2724 def _is_numeral(ctx, a):
2725  return Z3_is_numeral_ast(ctx.ref(), a)
2726 
2727 
2728 def _is_algebraic(ctx, a):
2729  return Z3_is_algebraic_number(ctx.ref(), a)
2730 
2731 
2733  """Return `True` if `a` is an integer value of sort Int.
2734 
2735  >>> is_int_value(IntVal(1))
2736  True
2737  >>> is_int_value(1)
2738  False
2739  >>> is_int_value(Int('x'))
2740  False
2741  >>> n = Int('x') + 1
2742  >>> n
2743  x + 1
2744  >>> n.arg(1)
2745  1
2746  >>> is_int_value(n.arg(1))
2747  True
2748  >>> is_int_value(RealVal("1/3"))
2749  False
2750  >>> is_int_value(RealVal(1))
2751  False
2752  """
2753  return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2754 
2755 
2757  """Return `True` if `a` is rational value of sort Real.
2758 
2759  >>> is_rational_value(RealVal(1))
2760  True
2761  >>> is_rational_value(RealVal("3/5"))
2762  True
2763  >>> is_rational_value(IntVal(1))
2764  False
2765  >>> is_rational_value(1)
2766  False
2767  >>> n = Real('x') + 1
2768  >>> n.arg(1)
2769  1
2770  >>> is_rational_value(n.arg(1))
2771  True
2772  >>> is_rational_value(Real('x'))
2773  False
2774  """
2775  return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2776 
2777 
2779  """Return `True` if `a` is an algebraic value of sort Real.
2780 
2781  >>> is_algebraic_value(RealVal("3/5"))
2782  False
2783  >>> n = simplify(Sqrt(2))
2784  >>> n
2785  1.4142135623?
2786  >>> is_algebraic_value(n)
2787  True
2788  """
2789  return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2790 
2791 
2792 def is_add(a):
2793  """Return `True` if `a` is an expression of the form b + c.
2794 
2795  >>> x, y = Ints('x y')
2796  >>> is_add(x + y)
2797  True
2798  >>> is_add(x - y)
2799  False
2800  """
2801  return is_app_of(a, Z3_OP_ADD)
2802 
2803 
2804 def is_mul(a):
2805  """Return `True` if `a` is an expression of the form b * c.
2806 
2807  >>> x, y = Ints('x y')
2808  >>> is_mul(x * y)
2809  True
2810  >>> is_mul(x - y)
2811  False
2812  """
2813  return is_app_of(a, Z3_OP_MUL)
2814 
2815 
2816 def is_sub(a):
2817  """Return `True` if `a` is an expression of the form b - c.
2818 
2819  >>> x, y = Ints('x y')
2820  >>> is_sub(x - y)
2821  True
2822  >>> is_sub(x + y)
2823  False
2824  """
2825  return is_app_of(a, Z3_OP_SUB)
2826 
2827 
2828 def is_div(a):
2829  """Return `True` if `a` is an expression of the form b / c.
2830 
2831  >>> x, y = Reals('x y')
2832  >>> is_div(x / y)
2833  True
2834  >>> is_div(x + y)
2835  False
2836  >>> x, y = Ints('x y')
2837  >>> is_div(x / y)
2838  False
2839  >>> is_idiv(x / y)
2840  True
2841  """
2842  return is_app_of(a, Z3_OP_DIV)
2843 
2844 
2845 def is_idiv(a):
2846  """Return `True` if `a` is an expression of the form b div c.
2847 
2848  >>> x, y = Ints('x y')
2849  >>> is_idiv(x / y)
2850  True
2851  >>> is_idiv(x + y)
2852  False
2853  """
2854  return is_app_of(a, Z3_OP_IDIV)
2855 
2856 
2857 def is_mod(a):
2858  """Return `True` if `a` is an expression of the form b % c.
2859 
2860  >>> x, y = Ints('x y')
2861  >>> is_mod(x % y)
2862  True
2863  >>> is_mod(x + y)
2864  False
2865  """
2866  return is_app_of(a, Z3_OP_MOD)
2867 
2868 
2869 def is_le(a):
2870  """Return `True` if `a` is an expression of the form b <= c.
2871 
2872  >>> x, y = Ints('x y')
2873  >>> is_le(x <= y)
2874  True
2875  >>> is_le(x < y)
2876  False
2877  """
2878  return is_app_of(a, Z3_OP_LE)
2879 
2880 
2881 def is_lt(a):
2882  """Return `True` if `a` is an expression of the form b < c.
2883 
2884  >>> x, y = Ints('x y')
2885  >>> is_lt(x < y)
2886  True
2887  >>> is_lt(x == y)
2888  False
2889  """
2890  return is_app_of(a, Z3_OP_LT)
2891 
2892 
2893 def is_ge(a):
2894  """Return `True` if `a` is an expression of the form b >= c.
2895 
2896  >>> x, y = Ints('x y')
2897  >>> is_ge(x >= y)
2898  True
2899  >>> is_ge(x == y)
2900  False
2901  """
2902  return is_app_of(a, Z3_OP_GE)
2903 
2904 
2905 def is_gt(a):
2906  """Return `True` if `a` is an expression of the form b > c.
2907 
2908  >>> x, y = Ints('x y')
2909  >>> is_gt(x > y)
2910  True
2911  >>> is_gt(x == y)
2912  False
2913  """
2914  return is_app_of(a, Z3_OP_GT)
2915 
2916 
2917 def is_is_int(a):
2918  """Return `True` if `a` is an expression of the form IsInt(b).
2919 
2920  >>> x = Real('x')
2921  >>> is_is_int(IsInt(x))
2922  True
2923  >>> is_is_int(x)
2924  False
2925  """
2926  return is_app_of(a, Z3_OP_IS_INT)
2927 
2928 
2929 def is_to_real(a):
2930  """Return `True` if `a` is an expression of the form ToReal(b).
2931 
2932  >>> x = Int('x')
2933  >>> n = ToReal(x)
2934  >>> n
2935  ToReal(x)
2936  >>> is_to_real(n)
2937  True
2938  >>> is_to_real(x)
2939  False
2940  """
2941  return is_app_of(a, Z3_OP_TO_REAL)
2942 
2943 
2944 def is_to_int(a):
2945  """Return `True` if `a` is an expression of the form ToInt(b).
2946 
2947  >>> x = Real('x')
2948  >>> n = ToInt(x)
2949  >>> n
2950  ToInt(x)
2951  >>> is_to_int(n)
2952  True
2953  >>> is_to_int(x)
2954  False
2955  """
2956  return is_app_of(a, Z3_OP_TO_INT)
2957 
2958 
2960  """Integer values."""
2961 
2962  def as_long(self):
2963  """Return a Z3 integer numeral as a Python long (bignum) numeral.
2964 
2965  >>> v = IntVal(1)
2966  >>> v + 1
2967  1 + 1
2968  >>> v.as_long() + 1
2969  2
2970  """
2971  if z3_debug():
2972  _z3_assert(self.is_intis_int(), "Integer value expected")
2973  return int(self.as_stringas_string())
2974 
2975  def as_string(self):
2976  """Return a Z3 integer numeral as a Python string.
2977  >>> v = IntVal(100)
2978  >>> v.as_string()
2979  '100'
2980  """
2981  return Z3_get_numeral_string(self.ctx_refctx_ref(), self.as_astas_astas_ast())
2982 
2983  def as_binary_string(self):
2984  """Return a Z3 integer numeral as a Python binary string.
2985  >>> v = IntVal(10)
2986  >>> v.as_binary_string()
2987  '1010'
2988  """
2989  return Z3_get_numeral_binary_string(self.ctx_refctx_ref(), self.as_astas_astas_ast())
2990 
2991 
2993  """Rational values."""
2994 
2995  def numerator(self):
2996  """ Return the numerator of a Z3 rational numeral.
2997 
2998  >>> is_rational_value(RealVal("3/5"))
2999  True
3000  >>> n = RealVal("3/5")
3001  >>> n.numerator()
3002  3
3003  >>> is_rational_value(Q(3,5))
3004  True
3005  >>> Q(3,5).numerator()
3006  3
3007  """
3008  return IntNumRef(Z3_get_numerator(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
3009 
3010  def denominator(self):
3011  """ Return the denominator of a Z3 rational numeral.
3012 
3013  >>> is_rational_value(Q(3,5))
3014  True
3015  >>> n = Q(3,5)
3016  >>> n.denominator()
3017  5
3018  """
3019  return IntNumRef(Z3_get_denominator(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
3020 
3022  """ Return the numerator as a Python long.
3023 
3024  >>> v = RealVal(10000000000)
3025  >>> v
3026  10000000000
3027  >>> v + 1
3028  10000000000 + 1
3029  >>> v.numerator_as_long() + 1 == 10000000001
3030  True
3031  """
3032  return self.numeratornumerator().as_long()
3033 
3035  """ Return the denominator as a Python long.
3036 
3037  >>> v = RealVal("1/3")
3038  >>> v
3039  1/3
3040  >>> v.denominator_as_long()
3041  3
3042  """
3043  return self.denominatordenominator().as_long()
3044 
3045  def is_int(self):
3046  return False
3047 
3048  def is_real(self):
3049  return True
3050 
3051  def is_int_value(self):
3052  return self.denominatordenominator().is_int() and self.denominator_as_longdenominator_as_long() == 1
3053 
3054  def as_long(self):
3055  _z3_assert(self.is_int_valueis_int_value(), "Expected integer fraction")
3056  return self.numerator_as_longnumerator_as_long()
3057 
3058  def as_decimal(self, prec):
3059  """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
3060 
3061  >>> v = RealVal("1/5")
3062  >>> v.as_decimal(3)
3063  '0.2'
3064  >>> v = RealVal("1/3")
3065  >>> v.as_decimal(3)
3066  '0.333?'
3067  """
3068  return Z3_get_numeral_decimal_string(self.ctx_refctx_ref(), self.as_astas_astas_ast(), prec)
3069 
3070  def as_string(self):
3071  """Return a Z3 rational numeral as a Python string.
3072 
3073  >>> v = Q(3,6)
3074  >>> v.as_string()
3075  '1/2'
3076  """
3077  return Z3_get_numeral_string(self.ctx_refctx_ref(), self.as_astas_astas_ast())
3078 
3079  def as_fraction(self):
3080  """Return a Z3 rational as a Python Fraction object.
3081 
3082  >>> v = RealVal("1/5")
3083  >>> v.as_fraction()
3084  Fraction(1, 5)
3085  """
3086  return Fraction(self.numerator_as_longnumerator_as_long(), self.denominator_as_longdenominator_as_long())
3087 
3088 
3090  """Algebraic irrational values."""
3091 
3092  def approx(self, precision=10):
3093  """Return a Z3 rational number that approximates the algebraic number `self`.
3094  The result `r` is such that |r - self| <= 1/10^precision
3095 
3096  >>> x = simplify(Sqrt(2))
3097  >>> x.approx(20)
3098  6838717160008073720548335/4835703278458516698824704
3099  >>> x.approx(5)
3100  2965821/2097152
3101  """
3102  return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_refctx_ref(), self.as_astas_astas_ast(), precision), self.ctxctx)
3103 
3104  def as_decimal(self, prec):
3105  """Return a string representation of the algebraic number `self` in decimal notation
3106  using `prec` decimal places.
3107 
3108  >>> x = simplify(Sqrt(2))
3109  >>> x.as_decimal(10)
3110  '1.4142135623?'
3111  >>> x.as_decimal(20)
3112  '1.41421356237309504880?'
3113  """
3114  return Z3_get_numeral_decimal_string(self.ctx_refctx_ref(), self.as_astas_astas_ast(), prec)
3115 
3116  def poly(self):
3117  return AstVector(Z3_algebraic_get_poly(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
3118 
3119  def index(self):
3120  return Z3_algebraic_get_i(self.ctx_refctx_ref(), self.as_astas_astas_ast())
3121 
3122 
3123 def _py2expr(a, ctx=None):
3124  if isinstance(a, bool):
3125  return BoolVal(a, ctx)
3126  if _is_int(a):
3127  return IntVal(a, ctx)
3128  if isinstance(a, float):
3129  return RealVal(a, ctx)
3130  if isinstance(a, str):
3131  return StringVal(a, ctx)
3132  if is_expr(a):
3133  return a
3134  if z3_debug():
3135  _z3_assert(False, "Python bool, int, long or float expected")
3136 
3137 
3138 def IntSort(ctx=None):
3139  """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
3140 
3141  >>> IntSort()
3142  Int
3143  >>> x = Const('x', IntSort())
3144  >>> is_int(x)
3145  True
3146  >>> x.sort() == IntSort()
3147  True
3148  >>> x.sort() == BoolSort()
3149  False
3150  """
3151  ctx = _get_ctx(ctx)
3152  return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
3153 
3154 
3155 def RealSort(ctx=None):
3156  """Return the real sort in the given context. If `ctx=None`, then the global context is used.
3157 
3158  >>> RealSort()
3159  Real
3160  >>> x = Const('x', RealSort())
3161  >>> is_real(x)
3162  True
3163  >>> is_int(x)
3164  False
3165  >>> x.sort() == RealSort()
3166  True
3167  """
3168  ctx = _get_ctx(ctx)
3169  return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)
3170 
3171 
3172 def _to_int_str(val):
3173  if isinstance(val, float):
3174  return str(int(val))
3175  elif isinstance(val, bool):
3176  if val:
3177  return "1"
3178  else:
3179  return "0"
3180  elif _is_int(val):
3181  return str(val)
3182  elif isinstance(val, str):
3183  return val
3184  if z3_debug():
3185  _z3_assert(False, "Python value cannot be used as a Z3 integer")
3186 
3187 
3188 def IntVal(val, ctx=None):
3189  """Return a Z3 integer value. If `ctx=None`, then the global context is used.
3190 
3191  >>> IntVal(1)
3192  1
3193  >>> IntVal("100")
3194  100
3195  """
3196  ctx = _get_ctx(ctx)
3197  return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
3198 
3199 
3200 def RealVal(val, ctx=None):
3201  """Return a Z3 real value.
3202 
3203  `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
3204  If `ctx=None`, then the global context is used.
3205 
3206  >>> RealVal(1)
3207  1
3208  >>> RealVal(1).sort()
3209  Real
3210  >>> RealVal("3/5")
3211  3/5
3212  >>> RealVal("1.5")
3213  3/2
3214  """
3215  ctx = _get_ctx(ctx)
3216  return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
3217 
3218 
3219 def RatVal(a, b, ctx=None):
3220  """Return a Z3 rational a/b.
3221 
3222  If `ctx=None`, then the global context is used.
3223 
3224  >>> RatVal(3,5)
3225  3/5
3226  >>> RatVal(3,5).sort()
3227  Real
3228  """
3229  if z3_debug():
3230  _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
3231  _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
3232  return simplify(RealVal(a, ctx) / RealVal(b, ctx))
3233 
3234 
3235 def Q(a, b, ctx=None):
3236  """Return a Z3 rational a/b.
3237 
3238  If `ctx=None`, then the global context is used.
3239 
3240  >>> Q(3,5)
3241  3/5
3242  >>> Q(3,5).sort()
3243  Real
3244  """
3245  return simplify(RatVal(a, b, ctx=ctx))
3246 
3247 
3248 def Int(name, ctx=None):
3249  """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
3250 
3251  >>> x = Int('x')
3252  >>> is_int(x)
3253  True
3254  >>> is_int(x + 1)
3255  True
3256  """
3257  ctx = _get_ctx(ctx)
3258  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
3259 
3260 
3261 def Ints(names, ctx=None):
3262  """Return a tuple of Integer constants.
3263 
3264  >>> x, y, z = Ints('x y z')
3265  >>> Sum(x, y, z)
3266  x + y + z
3267  """
3268  ctx = _get_ctx(ctx)
3269  if isinstance(names, str):
3270  names = names.split(" ")
3271  return [Int(name, ctx) for name in names]
3272 
3273 
3274 def IntVector(prefix, sz, ctx=None):
3275  """Return a list of integer constants of size `sz`.
3276 
3277  >>> X = IntVector('x', 3)
3278  >>> X
3279  [x__0, x__1, x__2]
3280  >>> Sum(X)
3281  x__0 + x__1 + x__2
3282  """
3283  ctx = _get_ctx(ctx)
3284  return [Int("%s__%s" % (prefix, i), ctx) for i in range(sz)]
3285 
3286 
3287 def FreshInt(prefix="x", ctx=None):
3288  """Return a fresh integer constant in the given context using the given prefix.
3289 
3290  >>> x = FreshInt()
3291  >>> y = FreshInt()
3292  >>> eq(x, y)
3293  False
3294  >>> x.sort()
3295  Int
3296  """
3297  ctx = _get_ctx(ctx)
3298  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
3299 
3300 
3301 def Real(name, ctx=None):
3302  """Return a real constant named `name`. If `ctx=None`, then the global context is used.
3303 
3304  >>> x = Real('x')
3305  >>> is_real(x)
3306  True
3307  >>> is_real(x + 1)
3308  True
3309  """
3310  ctx = _get_ctx(ctx)
3311  return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)
3312 
3313 
3314 def Reals(names, ctx=None):
3315  """Return a tuple of real constants.
3316 
3317  >>> x, y, z = Reals('x y z')
3318  >>> Sum(x, y, z)
3319  x + y + z
3320  >>> Sum(x, y, z).sort()
3321  Real
3322  """
3323  ctx = _get_ctx(ctx)
3324  if isinstance(names, str):
3325  names = names.split(" ")
3326  return [Real(name, ctx) for name in names]
3327 
3328 
3329 def RealVector(prefix, sz, ctx=None):
3330  """Return a list of real constants of size `sz`.
3331 
3332  >>> X = RealVector('x', 3)
3333  >>> X
3334  [x__0, x__1, x__2]
3335  >>> Sum(X)
3336  x__0 + x__1 + x__2
3337  >>> Sum(X).sort()
3338  Real
3339  """
3340  ctx = _get_ctx(ctx)
3341  return [Real("%s__%s" % (prefix, i), ctx) for i in range(sz)]
3342 
3343 
3344 def FreshReal(prefix="b", ctx=None):
3345  """Return a fresh real constant in the given context using the given prefix.
3346 
3347  >>> x = FreshReal()
3348  >>> y = FreshReal()
3349  >>> eq(x, y)
3350  False
3351  >>> x.sort()
3352  Real
3353  """
3354  ctx = _get_ctx(ctx)
3355  return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
3356 
3357 
3358 def ToReal(a):
3359  """ Return the Z3 expression ToReal(a).
3360 
3361  >>> x = Int('x')
3362  >>> x.sort()
3363  Int
3364  >>> n = ToReal(x)
3365  >>> n
3366  ToReal(x)
3367  >>> n.sort()
3368  Real
3369  """
3370  if z3_debug():
3371  _z3_assert(a.is_int(), "Z3 integer expression expected.")
3372  ctx = a.ctx
3373  return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
3374 
3375 
3376 def ToInt(a):
3377  """ Return the Z3 expression ToInt(a).
3378 
3379  >>> x = Real('x')
3380  >>> x.sort()
3381  Real
3382  >>> n = ToInt(x)
3383  >>> n
3384  ToInt(x)
3385  >>> n.sort()
3386  Int
3387  """
3388  if z3_debug():
3389  _z3_assert(a.is_real(), "Z3 real expression expected.")
3390  ctx = a.ctx
3391  return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)
3392 
3393 
3394 def IsInt(a):
3395  """ Return the Z3 predicate IsInt(a).
3396 
3397  >>> x = Real('x')
3398  >>> IsInt(x + "1/2")
3399  IsInt(x + 1/2)
3400  >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
3401  [x = 1/2]
3402  >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
3403  no solution
3404  """
3405  if z3_debug():
3406  _z3_assert(a.is_real(), "Z3 real expression expected.")
3407  ctx = a.ctx
3408  return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
3409 
3410 
3411 def Sqrt(a, ctx=None):
3412  """ Return a Z3 expression which represents the square root of a.
3413 
3414  >>> x = Real('x')
3415  >>> Sqrt(x)
3416  x**(1/2)
3417  """
3418  if not is_expr(a):
3419  ctx = _get_ctx(ctx)
3420  a = RealVal(a, ctx)
3421  return a ** "1/2"
3422 
3423 
3424 def Cbrt(a, ctx=None):
3425  """ Return a Z3 expression which represents the cubic root of a.
3426 
3427  >>> x = Real('x')
3428  >>> Cbrt(x)
3429  x**(1/3)
3430  """
3431  if not is_expr(a):
3432  ctx = _get_ctx(ctx)
3433  a = RealVal(a, ctx)
3434  return a ** "1/3"
3435 
3436 
3441 
3442 
3444  """Bit-vector sort."""
3445 
3446  def size(self):
3447  """Return the size (number of bits) of the bit-vector sort `self`.
3448 
3449  >>> b = BitVecSort(32)
3450  >>> b.size()
3451  32
3452  """
3453  return int(Z3_get_bv_sort_size(self.ctx_refctx_ref(), self.astast))
3454 
3455  def subsort(self, other):
3456  return is_bv_sort(other) and self.sizesize() < other.size()
3457 
3458  def cast(self, val):
3459  """Try to cast `val` as a Bit-Vector.
3460 
3461  >>> b = BitVecSort(32)
3462  >>> b.cast(10)
3463  10
3464  >>> b.cast(10).sexpr()
3465  '#x0000000a'
3466  """
3467  if is_expr(val):
3468  if z3_debug():
3469  _z3_assert(self.ctxctxctx == val.ctx, "Context mismatch")
3470  # Idea: use sign_extend if sort of val is a bitvector of smaller size
3471  return val
3472  else:
3473  return BitVecVal(val, self)
3474 
3475 
3476 def is_bv_sort(s):
3477  """Return True if `s` is a Z3 bit-vector sort.
3478 
3479  >>> is_bv_sort(BitVecSort(32))
3480  True
3481  >>> is_bv_sort(IntSort())
3482  False
3483  """
3484  return isinstance(s, BitVecSortRef)
3485 
3486 
3488  """Bit-vector expressions."""
3489 
3490  def sort(self):
3491  """Return the sort of the bit-vector expression `self`.
3492 
3493  >>> x = BitVec('x', 32)
3494  >>> x.sort()
3495  BitVec(32)
3496  >>> x.sort() == BitVecSort(32)
3497  True
3498  """
3499  return BitVecSortRef(Z3_get_sort(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
3500 
3501  def size(self):
3502  """Return the number of bits of the bit-vector expression `self`.
3503 
3504  >>> x = BitVec('x', 32)
3505  >>> (x + 1).size()
3506  32
3507  >>> Concat(x, x).size()
3508  64
3509  """
3510  return self.sortsortsort().size()
3511 
3512  def __add__(self, other):
3513  """Create the Z3 expression `self + other`.
3514 
3515  >>> x = BitVec('x', 32)
3516  >>> y = BitVec('y', 32)
3517  >>> x + y
3518  x + y
3519  >>> (x + y).sort()
3520  BitVec(32)
3521  """
3522  a, b = _coerce_exprs(self, other)
3523  return BitVecRef(Z3_mk_bvadd(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3524 
3525  def __radd__(self, other):
3526  """Create the Z3 expression `other + self`.
3527 
3528  >>> x = BitVec('x', 32)
3529  >>> 10 + x
3530  10 + x
3531  """
3532  a, b = _coerce_exprs(self, other)
3533  return BitVecRef(Z3_mk_bvadd(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
3534 
3535  def __mul__(self, other):
3536  """Create the Z3 expression `self * other`.
3537 
3538  >>> x = BitVec('x', 32)
3539  >>> y = BitVec('y', 32)
3540  >>> x * y
3541  x*y
3542  >>> (x * y).sort()
3543  BitVec(32)
3544  """
3545  a, b = _coerce_exprs(self, other)
3546  return BitVecRef(Z3_mk_bvmul(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3547 
3548  def __rmul__(self, other):
3549  """Create the Z3 expression `other * self`.
3550 
3551  >>> x = BitVec('x', 32)
3552  >>> 10 * x
3553  10*x
3554  """
3555  a, b = _coerce_exprs(self, other)
3556  return BitVecRef(Z3_mk_bvmul(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
3557 
3558  def __sub__(self, other):
3559  """Create the Z3 expression `self - other`.
3560 
3561  >>> x = BitVec('x', 32)
3562  >>> y = BitVec('y', 32)
3563  >>> x - y
3564  x - y
3565  >>> (x - y).sort()
3566  BitVec(32)
3567  """
3568  a, b = _coerce_exprs(self, other)
3569  return BitVecRef(Z3_mk_bvsub(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3570 
3571  def __rsub__(self, other):
3572  """Create the Z3 expression `other - self`.
3573 
3574  >>> x = BitVec('x', 32)
3575  >>> 10 - x
3576  10 - x
3577  """
3578  a, b = _coerce_exprs(self, other)
3579  return BitVecRef(Z3_mk_bvsub(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
3580 
3581  def __or__(self, other):
3582  """Create the Z3 expression bitwise-or `self | other`.
3583 
3584  >>> x = BitVec('x', 32)
3585  >>> y = BitVec('y', 32)
3586  >>> x | y
3587  x | y
3588  >>> (x | y).sort()
3589  BitVec(32)
3590  """
3591  a, b = _coerce_exprs(self, other)
3592  return BitVecRef(Z3_mk_bvor(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3593 
3594  def __ror__(self, other):
3595  """Create the Z3 expression bitwise-or `other | self`.
3596 
3597  >>> x = BitVec('x', 32)
3598  >>> 10 | x
3599  10 | x
3600  """
3601  a, b = _coerce_exprs(self, other)
3602  return BitVecRef(Z3_mk_bvor(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
3603 
3604  def __and__(self, other):
3605  """Create the Z3 expression bitwise-and `self & other`.
3606 
3607  >>> x = BitVec('x', 32)
3608  >>> y = BitVec('y', 32)
3609  >>> x & y
3610  x & y
3611  >>> (x & y).sort()
3612  BitVec(32)
3613  """
3614  a, b = _coerce_exprs(self, other)
3615  return BitVecRef(Z3_mk_bvand(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3616 
3617  def __rand__(self, other):
3618  """Create the Z3 expression bitwise-or `other & self`.
3619 
3620  >>> x = BitVec('x', 32)
3621  >>> 10 & x
3622  10 & x
3623  """
3624  a, b = _coerce_exprs(self, other)
3625  return BitVecRef(Z3_mk_bvand(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
3626 
3627  def __xor__(self, other):
3628  """Create the Z3 expression bitwise-xor `self ^ other`.
3629 
3630  >>> x = BitVec('x', 32)
3631  >>> y = BitVec('y', 32)
3632  >>> x ^ y
3633  x ^ y
3634  >>> (x ^ y).sort()
3635  BitVec(32)
3636  """
3637  a, b = _coerce_exprs(self, other)
3638  return BitVecRef(Z3_mk_bvxor(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3639 
3640  def __rxor__(self, other):
3641  """Create the Z3 expression bitwise-xor `other ^ self`.
3642 
3643  >>> x = BitVec('x', 32)
3644  >>> 10 ^ x
3645  10 ^ x
3646  """
3647  a, b = _coerce_exprs(self, other)
3648  return BitVecRef(Z3_mk_bvxor(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
3649 
3650  def __pos__(self):
3651  """Return `self`.
3652 
3653  >>> x = BitVec('x', 32)
3654  >>> +x
3655  x
3656  """
3657  return self
3658 
3659  def __neg__(self):
3660  """Return an expression representing `-self`.
3661 
3662  >>> x = BitVec('x', 32)
3663  >>> -x
3664  -x
3665  >>> simplify(-(-x))
3666  x
3667  """
3668  return BitVecRef(Z3_mk_bvneg(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
3669 
3670  def __invert__(self):
3671  """Create the Z3 expression bitwise-not `~self`.
3672 
3673  >>> x = BitVec('x', 32)
3674  >>> ~x
3675  ~x
3676  >>> simplify(~(~x))
3677  x
3678  """
3679  return BitVecRef(Z3_mk_bvnot(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
3680 
3681  def __div__(self, other):
3682  """Create the Z3 expression (signed) division `self / other`.
3683 
3684  Use the function UDiv() for unsigned division.
3685 
3686  >>> x = BitVec('x', 32)
3687  >>> y = BitVec('y', 32)
3688  >>> x / y
3689  x/y
3690  >>> (x / y).sort()
3691  BitVec(32)
3692  >>> (x / y).sexpr()
3693  '(bvsdiv x y)'
3694  >>> UDiv(x, y).sexpr()
3695  '(bvudiv x y)'
3696  """
3697  a, b = _coerce_exprs(self, other)
3698  return BitVecRef(Z3_mk_bvsdiv(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3699 
3700  def __truediv__(self, other):
3701  """Create the Z3 expression (signed) division `self / other`."""
3702  return self.__div____div__(other)
3703 
3704  def __rdiv__(self, other):
3705  """Create the Z3 expression (signed) division `other / self`.
3706 
3707  Use the function UDiv() for unsigned division.
3708 
3709  >>> x = BitVec('x', 32)
3710  >>> 10 / x
3711  10/x
3712  >>> (10 / x).sexpr()
3713  '(bvsdiv #x0000000a x)'
3714  >>> UDiv(10, x).sexpr()
3715  '(bvudiv #x0000000a x)'
3716  """
3717  a, b = _coerce_exprs(self, other)
3718  return BitVecRef(Z3_mk_bvsdiv(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
3719 
3720  def __rtruediv__(self, other):
3721  """Create the Z3 expression (signed) division `other / self`."""
3722  return self.__rdiv____rdiv__(other)
3723 
3724  def __mod__(self, other):
3725  """Create the Z3 expression (signed) mod `self % other`.
3726 
3727  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3728 
3729  >>> x = BitVec('x', 32)
3730  >>> y = BitVec('y', 32)
3731  >>> x % y
3732  x%y
3733  >>> (x % y).sort()
3734  BitVec(32)
3735  >>> (x % y).sexpr()
3736  '(bvsmod x y)'
3737  >>> URem(x, y).sexpr()
3738  '(bvurem x y)'
3739  >>> SRem(x, y).sexpr()
3740  '(bvsrem x y)'
3741  """
3742  a, b = _coerce_exprs(self, other)
3743  return BitVecRef(Z3_mk_bvsmod(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3744 
3745  def __rmod__(self, other):
3746  """Create the Z3 expression (signed) mod `other % self`.
3747 
3748  Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3749 
3750  >>> x = BitVec('x', 32)
3751  >>> 10 % x
3752  10%x
3753  >>> (10 % x).sexpr()
3754  '(bvsmod #x0000000a x)'
3755  >>> URem(10, x).sexpr()
3756  '(bvurem #x0000000a x)'
3757  >>> SRem(10, x).sexpr()
3758  '(bvsrem #x0000000a x)'
3759  """
3760  a, b = _coerce_exprs(self, other)
3761  return BitVecRef(Z3_mk_bvsmod(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
3762 
3763  def __le__(self, other):
3764  """Create the Z3 expression (signed) `other <= self`.
3765 
3766  Use the function ULE() for unsigned less than or equal to.
3767 
3768  >>> x, y = BitVecs('x y', 32)
3769  >>> x <= y
3770  x <= y
3771  >>> (x <= y).sexpr()
3772  '(bvsle x y)'
3773  >>> ULE(x, y).sexpr()
3774  '(bvule x y)'
3775  """
3776  a, b = _coerce_exprs(self, other)
3777  return BoolRef(Z3_mk_bvsle(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3778 
3779  def __lt__(self, other):
3780  """Create the Z3 expression (signed) `other < self`.
3781 
3782  Use the function ULT() for unsigned less than.
3783 
3784  >>> x, y = BitVecs('x y', 32)
3785  >>> x < y
3786  x < y
3787  >>> (x < y).sexpr()
3788  '(bvslt x y)'
3789  >>> ULT(x, y).sexpr()
3790  '(bvult x y)'
3791  """
3792  a, b = _coerce_exprs(self, other)
3793  return BoolRef(Z3_mk_bvslt(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3794 
3795  def __gt__(self, other):
3796  """Create the Z3 expression (signed) `other > self`.
3797 
3798  Use the function UGT() for unsigned greater than.
3799 
3800  >>> x, y = BitVecs('x y', 32)
3801  >>> x > y
3802  x > y
3803  >>> (x > y).sexpr()
3804  '(bvsgt x y)'
3805  >>> UGT(x, y).sexpr()
3806  '(bvugt x y)'
3807  """
3808  a, b = _coerce_exprs(self, other)
3809  return BoolRef(Z3_mk_bvsgt(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3810 
3811  def __ge__(self, other):
3812  """Create the Z3 expression (signed) `other >= self`.
3813 
3814  Use the function UGE() for unsigned greater than or equal to.
3815 
3816  >>> x, y = BitVecs('x y', 32)
3817  >>> x >= y
3818  x >= y
3819  >>> (x >= y).sexpr()
3820  '(bvsge x y)'
3821  >>> UGE(x, y).sexpr()
3822  '(bvuge x y)'
3823  """
3824  a, b = _coerce_exprs(self, other)
3825  return BoolRef(Z3_mk_bvsge(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3826 
3827  def __rshift__(self, other):
3828  """Create the Z3 expression (arithmetical) right shift `self >> other`
3829 
3830  Use the function LShR() for the right logical shift
3831 
3832  >>> x, y = BitVecs('x y', 32)
3833  >>> x >> y
3834  x >> y
3835  >>> (x >> y).sexpr()
3836  '(bvashr x y)'
3837  >>> LShR(x, y).sexpr()
3838  '(bvlshr x y)'
3839  >>> BitVecVal(4, 3)
3840  4
3841  >>> BitVecVal(4, 3).as_signed_long()
3842  -4
3843  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3844  -2
3845  >>> simplify(BitVecVal(4, 3) >> 1)
3846  6
3847  >>> simplify(LShR(BitVecVal(4, 3), 1))
3848  2
3849  >>> simplify(BitVecVal(2, 3) >> 1)
3850  1
3851  >>> simplify(LShR(BitVecVal(2, 3), 1))
3852  1
3853  """
3854  a, b = _coerce_exprs(self, other)
3855  return BitVecRef(Z3_mk_bvashr(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3856 
3857  def __lshift__(self, other):
3858  """Create the Z3 expression left shift `self << other`
3859 
3860  >>> x, y = BitVecs('x y', 32)
3861  >>> x << y
3862  x << y
3863  >>> (x << y).sexpr()
3864  '(bvshl x y)'
3865  >>> simplify(BitVecVal(2, 3) << 1)
3866  4
3867  """
3868  a, b = _coerce_exprs(self, other)
3869  return BitVecRef(Z3_mk_bvshl(self.ctx_refctx_ref(), a.as_ast(), b.as_ast()), self.ctxctx)
3870 
3871  def __rrshift__(self, other):
3872  """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3873 
3874  Use the function LShR() for the right logical shift
3875 
3876  >>> x = BitVec('x', 32)
3877  >>> 10 >> x
3878  10 >> x
3879  >>> (10 >> x).sexpr()
3880  '(bvashr #x0000000a x)'
3881  """
3882  a, b = _coerce_exprs(self, other)
3883  return BitVecRef(Z3_mk_bvashr(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
3884 
3885  def __rlshift__(self, other):
3886  """Create the Z3 expression left shift `other << self`.
3887 
3888  Use the function LShR() for the right logical shift
3889 
3890  >>> x = BitVec('x', 32)
3891  >>> 10 << x
3892  10 << x
3893  >>> (10 << x).sexpr()
3894  '(bvshl #x0000000a x)'
3895  """
3896  a, b = _coerce_exprs(self, other)
3897  return BitVecRef(Z3_mk_bvshl(self.ctx_refctx_ref(), b.as_ast(), a.as_ast()), self.ctxctx)
3898 
3899 
3901  """Bit-vector values."""
3902 
3903  def as_long(self):
3904  """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
3905 
3906  >>> v = BitVecVal(0xbadc0de, 32)
3907  >>> v
3908  195936478
3909  >>> print("0x%.8x" % v.as_long())
3910  0x0badc0de
3911  """
3912  return int(self.as_stringas_string())
3913 
3914  def as_signed_long(self):
3915  """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
3916  The most significant bit is assumed to be the sign.
3917 
3918  >>> BitVecVal(4, 3).as_signed_long()
3919  -4
3920  >>> BitVecVal(7, 3).as_signed_long()
3921  -1
3922  >>> BitVecVal(3, 3).as_signed_long()
3923  3
3924  >>> BitVecVal(2**32 - 1, 32).as_signed_long()
3925  -1
3926  >>> BitVecVal(2**64 - 1, 64).as_signed_long()
3927  -1
3928  """
3929  sz = self.sizesize()
3930  val = self.as_longas_long()
3931  if val >= 2**(sz - 1):
3932  val = val - 2**sz
3933  if val < -2**(sz - 1):
3934  val = val + 2**sz
3935  return int(val)
3936 
3937  def as_string(self):
3938  return Z3_get_numeral_string(self.ctx_refctx_ref(), self.as_astas_astas_ast())
3939 
3940  def as_binary_string(self):
3941  return Z3_get_numeral_binary_string(self.ctx_refctx_ref(), self.as_astas_astas_ast())
3942 
3943 
3944 def is_bv(a):
3945  """Return `True` if `a` is a Z3 bit-vector expression.
3946 
3947  >>> b = BitVec('b', 32)
3948  >>> is_bv(b)
3949  True
3950  >>> is_bv(b + 10)
3951  True
3952  >>> is_bv(Int('x'))
3953  False
3954  """
3955  return isinstance(a, BitVecRef)
3956 
3957 
3959  """Return `True` if `a` is a Z3 bit-vector numeral value.
3960 
3961  >>> b = BitVec('b', 32)
3962  >>> is_bv_value(b)
3963  False
3964  >>> b = BitVecVal(10, 32)
3965  >>> b
3966  10
3967  >>> is_bv_value(b)
3968  True
3969  """
3970  return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3971 
3972 
3973 def BV2Int(a, is_signed=False):
3974  """Return the Z3 expression BV2Int(a).
3975 
3976  >>> b = BitVec('b', 3)
3977  >>> BV2Int(b).sort()
3978  Int
3979  >>> x = Int('x')
3980  >>> x > BV2Int(b)
3981  x > BV2Int(b)
3982  >>> x > BV2Int(b, is_signed=False)
3983  x > BV2Int(b)
3984  >>> x > BV2Int(b, is_signed=True)
3985  x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3986  >>> solve(x > BV2Int(b), b == 1, x < 3)
3987  [x = 2, b = 1]
3988  """
3989  if z3_debug():
3990  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
3991  ctx = a.ctx
3992  # investigate problem with bv2int
3993  return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
3994 
3995 
3996 def Int2BV(a, num_bits):
3997  """Return the z3 expression Int2BV(a, num_bits).
3998  It is a bit-vector of width num_bits and represents the
3999  modulo of a by 2^num_bits
4000  """
4001  ctx = a.ctx
4002  return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
4003 
4004 
4005 def BitVecSort(sz, ctx=None):
4006  """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
4007 
4008  >>> Byte = BitVecSort(8)
4009  >>> Word = BitVecSort(16)
4010  >>> Byte
4011  BitVec(8)
4012  >>> x = Const('x', Byte)
4013  >>> eq(x, BitVec('x', 8))
4014  True
4015  """
4016  ctx = _get_ctx(ctx)
4017  return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
4018 
4019 
4020 def BitVecVal(val, bv, ctx=None):
4021  """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
4022 
4023  >>> v = BitVecVal(10, 32)
4024  >>> v
4025  10
4026  >>> print("0x%.8x" % v.as_long())
4027  0x0000000a
4028  """
4029  if is_bv_sort(bv):
4030  ctx = bv.ctx
4031  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
4032  else:
4033  ctx = _get_ctx(ctx)
4034  return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
4035 
4036 
4037 def BitVec(name, bv, ctx=None):
4038  """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
4039  If `ctx=None`, then the global context is used.
4040 
4041  >>> x = BitVec('x', 16)
4042  >>> is_bv(x)
4043  True
4044  >>> x.size()
4045  16
4046  >>> x.sort()
4047  BitVec(16)
4048  >>> word = BitVecSort(16)
4049  >>> x2 = BitVec('x', word)
4050  >>> eq(x, x2)
4051  True
4052  """
4053  if isinstance(bv, BitVecSortRef):
4054  ctx = bv.ctx
4055  else:
4056  ctx = _get_ctx(ctx)
4057  bv = BitVecSort(bv, ctx)
4058  return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
4059 
4060 
4061 def BitVecs(names, bv, ctx=None):
4062  """Return a tuple of bit-vector constants of size bv.
4063 
4064  >>> x, y, z = BitVecs('x y z', 16)
4065  >>> x.size()
4066  16
4067  >>> x.sort()
4068  BitVec(16)
4069  >>> Sum(x, y, z)
4070  0 + x + y + z
4071  >>> Product(x, y, z)
4072  1*x*y*z
4073  >>> simplify(Product(x, y, z))
4074  x*y*z
4075  """
4076  ctx = _get_ctx(ctx)
4077  if isinstance(names, str):
4078  names = names.split(" ")
4079  return [BitVec(name, bv, ctx) for name in names]
4080 
4081 
4082 def Concat(*args):
4083  """Create a Z3 bit-vector concatenation expression.
4084 
4085  >>> v = BitVecVal(1, 4)
4086  >>> Concat(v, v+1, v)
4087  Concat(Concat(1, 1 + 1), 1)
4088  >>> simplify(Concat(v, v+1, v))
4089  289
4090  >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
4091  121
4092  """
4093  args = _get_args(args)
4094  sz = len(args)
4095  if z3_debug():
4096  _z3_assert(sz >= 2, "At least two arguments expected.")
4097 
4098  ctx = None
4099  for a in args:
4100  if is_expr(a):
4101  ctx = a.ctx
4102  break
4103  if is_seq(args[0]) or isinstance(args[0], str):
4104  args = [_coerce_seq(s, ctx) for s in args]
4105  if z3_debug():
4106  _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
4107  v = (Ast * sz)()
4108  for i in range(sz):
4109  v[i] = args[i].as_ast()
4110  return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
4111 
4112  if is_re(args[0]):
4113  if z3_debug():
4114  _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
4115  v = (Ast * sz)()
4116  for i in range(sz):
4117  v[i] = args[i].as_ast()
4118  return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
4119 
4120  if z3_debug():
4121  _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
4122  r = args[0]
4123  for i in range(sz - 1):
4124  r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i + 1].as_ast()), ctx)
4125  return r
4126 
4127 
4128 def Extract(high, low, a):
4129  """Create a Z3 bit-vector extraction expression.
4130  Extract is overloaded to also work on sequence extraction.
4131  The functions SubString and SubSeq are redirected to Extract.
4132  For this case, the arguments are reinterpreted as:
4133  high - is a sequence (string)
4134  low - is an offset
4135  a - is the length to be extracted
4136 
4137  >>> x = BitVec('x', 8)
4138  >>> Extract(6, 2, x)
4139  Extract(6, 2, x)
4140  >>> Extract(6, 2, x).sort()
4141  BitVec(5)
4142  >>> simplify(Extract(StringVal("abcd"),2,1))
4143  "c"
4144  """
4145  if isinstance(high, str):
4146  high = StringVal(high)
4147  if is_seq(high):
4148  s = high
4149  offset, length = _coerce_exprs(low, a, s.ctx)
4150  return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
4151  if z3_debug():
4152  _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
4153  _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0,
4154  "First and second arguments must be non negative integers")
4155  _z3_assert(is_bv(a), "Third argument must be a Z3 bit-vector expression")
4156  return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
4157 
4158 
4159 def _check_bv_args(a, b):
4160  if z3_debug():
4161  _z3_assert(is_bv(a) or is_bv(b), "First or second argument must be a Z3 bit-vector expression")
4162 
4163 
4164 def ULE(a, b):
4165  """Create the Z3 expression (unsigned) `other <= self`.
4166 
4167  Use the operator <= for signed less than or equal to.
4168 
4169  >>> x, y = BitVecs('x y', 32)
4170  >>> ULE(x, y)
4171  ULE(x, y)
4172  >>> (x <= y).sexpr()
4173  '(bvsle x y)'
4174  >>> ULE(x, y).sexpr()
4175  '(bvule x y)'
4176  """
4177  _check_bv_args(a, b)
4178  a, b = _coerce_exprs(a, b)
4179  return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4180 
4181 
4182 def ULT(a, b):
4183  """Create the Z3 expression (unsigned) `other < self`.
4184 
4185  Use the operator < for signed less than.
4186 
4187  >>> x, y = BitVecs('x y', 32)
4188  >>> ULT(x, y)
4189  ULT(x, y)
4190  >>> (x < y).sexpr()
4191  '(bvslt x y)'
4192  >>> ULT(x, y).sexpr()
4193  '(bvult x y)'
4194  """
4195  _check_bv_args(a, b)
4196  a, b = _coerce_exprs(a, b)
4197  return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4198 
4199 
4200 def UGE(a, b):
4201  """Create the Z3 expression (unsigned) `other >= self`.
4202 
4203  Use the operator >= for signed greater than or equal to.
4204 
4205  >>> x, y = BitVecs('x y', 32)
4206  >>> UGE(x, y)
4207  UGE(x, y)
4208  >>> (x >= y).sexpr()
4209  '(bvsge x y)'
4210  >>> UGE(x, y).sexpr()
4211  '(bvuge x y)'
4212  """
4213  _check_bv_args(a, b)
4214  a, b = _coerce_exprs(a, b)
4215  return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4216 
4217 
4218 def UGT(a, b):
4219  """Create the Z3 expression (unsigned) `other > self`.
4220 
4221  Use the operator > for signed greater than.
4222 
4223  >>> x, y = BitVecs('x y', 32)
4224  >>> UGT(x, y)
4225  UGT(x, y)
4226  >>> (x > y).sexpr()
4227  '(bvsgt x y)'
4228  >>> UGT(x, y).sexpr()
4229  '(bvugt x y)'
4230  """
4231  _check_bv_args(a, b)
4232  a, b = _coerce_exprs(a, b)
4233  return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4234 
4235 
4236 def UDiv(a, b):
4237  """Create the Z3 expression (unsigned) division `self / other`.
4238 
4239  Use the operator / for signed division.
4240 
4241  >>> x = BitVec('x', 32)
4242  >>> y = BitVec('y', 32)
4243  >>> UDiv(x, y)
4244  UDiv(x, y)
4245  >>> UDiv(x, y).sort()
4246  BitVec(32)
4247  >>> (x / y).sexpr()
4248  '(bvsdiv x y)'
4249  >>> UDiv(x, y).sexpr()
4250  '(bvudiv x y)'
4251  """
4252  _check_bv_args(a, b)
4253  a, b = _coerce_exprs(a, b)
4254  return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4255 
4256 
4257 def URem(a, b):
4258  """Create the Z3 expression (unsigned) remainder `self % other`.
4259 
4260  Use the operator % for signed modulus, and SRem() for signed remainder.
4261 
4262  >>> x = BitVec('x', 32)
4263  >>> y = BitVec('y', 32)
4264  >>> URem(x, y)
4265  URem(x, y)
4266  >>> URem(x, y).sort()
4267  BitVec(32)
4268  >>> (x % y).sexpr()
4269  '(bvsmod x y)'
4270  >>> URem(x, y).sexpr()
4271  '(bvurem x y)'
4272  """
4273  _check_bv_args(a, b)
4274  a, b = _coerce_exprs(a, b)
4275  return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4276 
4277 
4278 def SRem(a, b):
4279  """Create the Z3 expression signed remainder.
4280 
4281  Use the operator % for signed modulus, and URem() for unsigned remainder.
4282 
4283  >>> x = BitVec('x', 32)
4284  >>> y = BitVec('y', 32)
4285  >>> SRem(x, y)
4286  SRem(x, y)
4287  >>> SRem(x, y).sort()
4288  BitVec(32)
4289  >>> (x % y).sexpr()
4290  '(bvsmod x y)'
4291  >>> SRem(x, y).sexpr()
4292  '(bvsrem x y)'
4293  """
4294  _check_bv_args(a, b)
4295  a, b = _coerce_exprs(a, b)
4296  return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4297 
4298 
4299 def LShR(a, b):
4300  """Create the Z3 expression logical right shift.
4301 
4302  Use the operator >> for the arithmetical right shift.
4303 
4304  >>> x, y = BitVecs('x y', 32)
4305  >>> LShR(x, y)
4306  LShR(x, y)
4307  >>> (x >> y).sexpr()
4308  '(bvashr x y)'
4309  >>> LShR(x, y).sexpr()
4310  '(bvlshr x y)'
4311  >>> BitVecVal(4, 3)
4312  4
4313  >>> BitVecVal(4, 3).as_signed_long()
4314  -4
4315  >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
4316  -2
4317  >>> simplify(BitVecVal(4, 3) >> 1)
4318  6
4319  >>> simplify(LShR(BitVecVal(4, 3), 1))
4320  2
4321  >>> simplify(BitVecVal(2, 3) >> 1)
4322  1
4323  >>> simplify(LShR(BitVecVal(2, 3), 1))
4324  1
4325  """
4326  _check_bv_args(a, b)
4327  a, b = _coerce_exprs(a, b)
4328  return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4329 
4330 
4331 def RotateLeft(a, b):
4332  """Return an expression representing `a` rotated to the left `b` times.
4333 
4334  >>> a, b = BitVecs('a b', 16)
4335  >>> RotateLeft(a, b)
4336  RotateLeft(a, b)
4337  >>> simplify(RotateLeft(a, 0))
4338  a
4339  >>> simplify(RotateLeft(a, 16))
4340  a
4341  """
4342  _check_bv_args(a, b)
4343  a, b = _coerce_exprs(a, b)
4344  return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4345 
4346 
4347 def RotateRight(a, b):
4348  """Return an expression representing `a` rotated to the right `b` times.
4349 
4350  >>> a, b = BitVecs('a b', 16)
4351  >>> RotateRight(a, b)
4352  RotateRight(a, b)
4353  >>> simplify(RotateRight(a, 0))
4354  a
4355  >>> simplify(RotateRight(a, 16))
4356  a
4357  """
4358  _check_bv_args(a, b)
4359  a, b = _coerce_exprs(a, b)
4360  return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4361 
4362 
4363 def SignExt(n, a):
4364  """Return a bit-vector expression with `n` extra sign-bits.
4365 
4366  >>> x = BitVec('x', 16)
4367  >>> n = SignExt(8, x)
4368  >>> n.size()
4369  24
4370  >>> n
4371  SignExt(8, x)
4372  >>> n.sort()
4373  BitVec(24)
4374  >>> v0 = BitVecVal(2, 2)
4375  >>> v0
4376  2
4377  >>> v0.size()
4378  2
4379  >>> v = simplify(SignExt(6, v0))
4380  >>> v
4381  254
4382  >>> v.size()
4383  8
4384  >>> print("%.x" % v.as_long())
4385  fe
4386  """
4387  if z3_debug():
4388  _z3_assert(_is_int(n), "First argument must be an integer")
4389  _z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
4390  return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
4391 
4392 
4393 def ZeroExt(n, a):
4394  """Return a bit-vector expression with `n` extra zero-bits.
4395 
4396  >>> x = BitVec('x', 16)
4397  >>> n = ZeroExt(8, x)
4398  >>> n.size()
4399  24
4400  >>> n
4401  ZeroExt(8, x)
4402  >>> n.sort()
4403  BitVec(24)
4404  >>> v0 = BitVecVal(2, 2)
4405  >>> v0
4406  2
4407  >>> v0.size()
4408  2
4409  >>> v = simplify(ZeroExt(6, v0))
4410  >>> v
4411  2
4412  >>> v.size()
4413  8
4414  """
4415  if z3_debug():
4416  _z3_assert(_is_int(n), "First argument must be an integer")
4417  _z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
4418  return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
4419 
4420 
4421 def RepeatBitVec(n, a):
4422  """Return an expression representing `n` copies of `a`.
4423 
4424  >>> x = BitVec('x', 8)
4425  >>> n = RepeatBitVec(4, x)
4426  >>> n
4427  RepeatBitVec(4, x)
4428  >>> n.size()
4429  32
4430  >>> v0 = BitVecVal(10, 4)
4431  >>> print("%.x" % v0.as_long())
4432  a
4433  >>> v = simplify(RepeatBitVec(4, v0))
4434  >>> v.size()
4435  16
4436  >>> print("%.x" % v.as_long())
4437  aaaa
4438  """
4439  if z3_debug():
4440  _z3_assert(_is_int(n), "First argument must be an integer")
4441  _z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
4442  return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
4443 
4444 
4445 def BVRedAnd(a):
4446  """Return the reduction-and expression of `a`."""
4447  if z3_debug():
4448  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4449  return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
4450 
4451 
4452 def BVRedOr(a):
4453  """Return the reduction-or expression of `a`."""
4454  if z3_debug():
4455  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4456  return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
4457 
4458 
4459 def BVAddNoOverflow(a, b, signed):
4460  """A predicate the determines that bit-vector addition does not overflow"""
4461  _check_bv_args(a, b)
4462  a, b = _coerce_exprs(a, b)
4463  return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4464 
4465 
4467  """A predicate the determines that signed bit-vector addition does not underflow"""
4468  _check_bv_args(a, b)
4469  a, b = _coerce_exprs(a, b)
4470  return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4471 
4472 
4474  """A predicate the determines that bit-vector subtraction does not overflow"""
4475  _check_bv_args(a, b)
4476  a, b = _coerce_exprs(a, b)
4477  return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4478 
4479 
4480 def BVSubNoUnderflow(a, b, signed):
4481  """A predicate the determines that bit-vector subtraction does not underflow"""
4482  _check_bv_args(a, b)
4483  a, b = _coerce_exprs(a, b)
4484  return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4485 
4486 
4488  """A predicate the determines that bit-vector signed division does not overflow"""
4489  _check_bv_args(a, b)
4490  a, b = _coerce_exprs(a, b)
4491  return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4492 
4493 
4495  """A predicate the determines that bit-vector unary negation does not overflow"""
4496  if z3_debug():
4497  _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4498  return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
4499 
4500 
4501 def BVMulNoOverflow(a, b, signed):
4502  """A predicate the determines that bit-vector multiplication does not overflow"""
4503  _check_bv_args(a, b)
4504  a, b = _coerce_exprs(a, b)
4505  return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4506 
4507 
4509  """A predicate the determines that bit-vector signed multiplication does not underflow"""
4510  _check_bv_args(a, b)
4511  a, b = _coerce_exprs(a, b)
4512  return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4513 
4514 
4515 
4520 
4522  """Array sorts."""
4523 
4524  def domain(self):
4525  """Return the domain of the array sort `self`.
4526 
4527  >>> A = ArraySort(IntSort(), BoolSort())
4528  >>> A.domain()
4529  Int
4530  """
4531  return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_refctx_ref(), self.astast), self.ctxctx)
4532 
4533  def domain_n(self, i):
4534  """Return the domain of the array sort `self`.
4535  """
4536  return _to_sort_ref(Z3_get_array_sort_domain_n(self.ctx_refctx_ref(), self.astast, i), self.ctxctx)
4537 
4538  def range(self):
4539  """Return the range of the array sort `self`.
4540 
4541  >>> A = ArraySort(IntSort(), BoolSort())
4542  >>> A.range()
4543  Bool
4544  """
4545  return _to_sort_ref(Z3_get_array_sort_range(self.ctx_refctx_ref(), self.astast), self.ctxctx)
4546 
4547 
4549  """Array expressions. """
4550 
4551  def sort(self):
4552  """Return the array sort of the array expression `self`.
4553 
4554  >>> a = Array('a', IntSort(), BoolSort())
4555  >>> a.sort()
4556  Array(Int, Bool)
4557  """
4558  return ArraySortRef(Z3_get_sort(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
4559 
4560  def domain(self):
4561  """Shorthand for `self.sort().domain()`.
4562 
4563  >>> a = Array('a', IntSort(), BoolSort())
4564  >>> a.domain()
4565  Int
4566  """
4567  return self.sortsortsort().domain()
4568 
4569  def domain_n(self, i):
4570  """Shorthand for self.sort().domain_n(i)`."""
4571  return self.sortsortsort().domain_n(i)
4572 
4573  def range(self):
4574  """Shorthand for `self.sort().range()`.
4575 
4576  >>> a = Array('a', IntSort(), BoolSort())
4577  >>> a.range()
4578  Bool
4579  """
4580  return self.sortsortsort().range()
4581 
4582  def __getitem__(self, arg):
4583  """Return the Z3 expression `self[arg]`.
4584 
4585  >>> a = Array('a', IntSort(), BoolSort())
4586  >>> i = Int('i')
4587  >>> a[i]
4588  a[i]
4589  >>> a[i].sexpr()
4590  '(select a i)'
4591  """
4592  return _array_select(self, arg)
4593 
4594  def default(self):
4595  return _to_expr_ref(Z3_mk_array_default(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
4596 
4597 
4598 def _array_select(ar, arg):
4599  if isinstance(arg, tuple):
4600  args = [ar.sort().domain_n(i).cast(arg[i]) for i in range(len(arg))]
4601  _args, sz = _to_ast_array(args)
4602  return _to_expr_ref(Z3_mk_select_n(ar.ctx_ref(), ar.as_ast(), sz, _args), ar.ctx)
4603  arg = ar.sort().domain().cast(arg)
4604  return _to_expr_ref(Z3_mk_select(ar.ctx_ref(), ar.as_ast(), arg.as_ast()), ar.ctx)
4605 
4606 
4608  return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
4609 
4610 
4611 def is_array(a):
4612  """Return `True` if `a` is a Z3 array expression.
4613 
4614  >>> a = Array('a', IntSort(), IntSort())
4615  >>> is_array(a)
4616  True
4617  >>> is_array(Store(a, 0, 1))
4618  True
4619  >>> is_array(a[0])
4620  False
4621  """
4622  return isinstance(a, ArrayRef)
4623 
4624 
4626  """Return `True` if `a` is a Z3 constant array.
4627 
4628  >>> a = K(IntSort(), 10)
4629  >>> is_const_array(a)
4630  True
4631  >>> a = Array('a', IntSort(), IntSort())
4632  >>> is_const_array(a)
4633  False
4634  """
4635  return is_app_of(a, Z3_OP_CONST_ARRAY)
4636 
4637 
4638 def is_K(a):
4639  """Return `True` if `a` is a Z3 constant array.
4640 
4641  >>> a = K(IntSort(), 10)
4642  >>> is_K(a)
4643  True
4644  >>> a = Array('a', IntSort(), IntSort())
4645  >>> is_K(a)
4646  False
4647  """
4648  return is_app_of(a, Z3_OP_CONST_ARRAY)
4649 
4650 
4651 def is_map(a):
4652  """Return `True` if `a` is a Z3 map array expression.
4653 
4654  >>> f = Function('f', IntSort(), IntSort())
4655  >>> b = Array('b', IntSort(), IntSort())
4656  >>> a = Map(f, b)
4657  >>> a
4658  Map(f, b)
4659  >>> is_map(a)
4660  True
4661  >>> is_map(b)
4662  False
4663  """
4664  return is_app_of(a, Z3_OP_ARRAY_MAP)
4665 
4666 
4667 def is_default(a):
4668  """Return `True` if `a` is a Z3 default array expression.
4669  >>> d = Default(K(IntSort(), 10))
4670  >>> is_default(d)
4671  True
4672  """
4673  return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4674 
4675 
4677  """Return the function declaration associated with a Z3 map array expression.
4678 
4679  >>> f = Function('f', IntSort(), IntSort())
4680  >>> b = Array('b', IntSort(), IntSort())
4681  >>> a = Map(f, b)
4682  >>> eq(f, get_map_func(a))
4683  True
4684  >>> get_map_func(a)
4685  f
4686  >>> get_map_func(a)(0)
4687  f(0)
4688  """
4689  if z3_debug():
4690  _z3_assert(is_map(a), "Z3 array map expression expected.")
4691  return FuncDeclRef(
4693  a.ctx_ref(),
4694  Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0),
4695  ),
4696  ctx=a.ctx,
4697  )
4698 
4699 
4700 def ArraySort(*sig):
4701  """Return the Z3 array sort with the given domain and range sorts.
4702 
4703  >>> A = ArraySort(IntSort(), BoolSort())
4704  >>> A
4705  Array(Int, Bool)
4706  >>> A.domain()
4707  Int
4708  >>> A.range()
4709  Bool
4710  >>> AA = ArraySort(IntSort(), A)
4711  >>> AA
4712  Array(Int, Array(Int, Bool))
4713  """
4714  sig = _get_args(sig)
4715  if z3_debug():
4716  _z3_assert(len(sig) > 1, "At least two arguments expected")
4717  arity = len(sig) - 1
4718  r = sig[arity]
4719  d = sig[0]
4720  if z3_debug():
4721  for s in sig:
4722  _z3_assert(is_sort(s), "Z3 sort expected")
4723  _z3_assert(s.ctx == r.ctx, "Context mismatch")
4724  ctx = d.ctx
4725  if len(sig) == 2:
4726  return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
4727  dom = (Sort * arity)()
4728  for i in range(arity):
4729  dom[i] = sig[i].ast
4730  return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)
4731 
4732 
4733 def Array(name, *sorts):
4734  """Return an array constant named `name` with the given domain and range sorts.
4735 
4736  >>> a = Array('a', IntSort(), IntSort())
4737  >>> a.sort()
4738  Array(Int, Int)
4739  >>> a[0]
4740  a[0]
4741  """
4742  s = ArraySort(sorts)
4743  ctx = s.ctx
4744  return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
4745 
4746 
4747 def Update(a, *args):
4748  """Return a Z3 store array expression.
4749 
4750  >>> a = Array('a', IntSort(), IntSort())
4751  >>> i, v = Ints('i v')
4752  >>> s = Update(a, i, v)
4753  >>> s.sort()
4754  Array(Int, Int)
4755  >>> prove(s[i] == v)
4756  proved
4757  >>> j = Int('j')
4758  >>> prove(Implies(i != j, s[j] == a[j]))
4759  proved
4760  """
4761  if z3_debug():
4762  _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4763  args = _get_args(args)
4764  ctx = a.ctx
4765  if len(args) <= 1:
4766  raise Z3Exception("array update requires index and value arguments")
4767  if len(args) == 2:
4768  i = args[0]
4769  v = args[1]
4770  i = a.sort().domain().cast(i)
4771  v = a.sort().range().cast(v)
4772  return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
4773  v = a.sort().range().cast(args[-1])
4774  idxs = [a.sort().domain_n(i).cast(args[i]) for i in range(len(args)-1)]
4775  _args, sz = _to_ast_array(idxs)
4776  return _to_expr_ref(Z3_mk_store_n(ctx.ref(), a.as_ast(), sz, _args, v.as_ast()), ctx)
4777 
4778 
4779 def Default(a):
4780  """ Return a default value for array expression.
4781  >>> b = K(IntSort(), 1)
4782  >>> prove(Default(b) == 1)
4783  proved
4784  """
4785  if z3_debug():
4786  _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4787  return a.default()
4788 
4789 
4790 def Store(a, *args):
4791  """Return a Z3 store array expression.
4792 
4793  >>> a = Array('a', IntSort(), IntSort())
4794  >>> i, v = Ints('i v')
4795  >>> s = Store(a, i, v)
4796  >>> s.sort()
4797  Array(Int, Int)
4798  >>> prove(s[i] == v)
4799  proved
4800  >>> j = Int('j')
4801  >>> prove(Implies(i != j, s[j] == a[j]))
4802  proved
4803  """
4804  return Update(a, args)
4805 
4806 
4807 def Select(a, *args):
4808  """Return a Z3 select array expression.
4809 
4810  >>> a = Array('a', IntSort(), IntSort())
4811  >>> i = Int('i')
4812  >>> Select(a, i)
4813  a[i]
4814  >>> eq(Select(a, i), a[i])
4815  True
4816  """
4817  args = _get_args(args)
4818  if z3_debug():
4819  _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4820  return a[args]
4821 
4822 
4823 def Map(f, *args):
4824  """Return a Z3 map array expression.
4825 
4826  >>> f = Function('f', IntSort(), IntSort(), IntSort())
4827  >>> a1 = Array('a1', IntSort(), IntSort())
4828  >>> a2 = Array('a2', IntSort(), IntSort())
4829  >>> b = Map(f, a1, a2)
4830  >>> b
4831  Map(f, a1, a2)
4832  >>> prove(b[0] == f(a1[0], a2[0]))
4833  proved
4834  """
4835  args = _get_args(args)
4836  if z3_debug():
4837  _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
4838  _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
4839  _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
4840  _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
4841  _args, sz = _to_ast_array(args)
4842  ctx = f.ctx
4843  return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
4844 
4845 
4846 def K(dom, v):
4847  """Return a Z3 constant array expression.
4848 
4849  >>> a = K(IntSort(), 10)
4850  >>> a
4851  K(Int, 10)
4852  >>> a.sort()
4853  Array(Int, Int)
4854  >>> i = Int('i')
4855  >>> a[i]
4856  K(Int, 10)[i]
4857  >>> simplify(a[i])
4858  10
4859  """
4860  if z3_debug():
4861  _z3_assert(is_sort(dom), "Z3 sort expected")
4862  ctx = dom.ctx
4863  if not is_expr(v):
4864  v = _py2expr(v, ctx)
4865  return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
4866 
4867 
4868 def Ext(a, b):
4869  """Return extensionality index for one-dimensional arrays.
4870  >> a, b = Consts('a b', SetSort(IntSort()))
4871  >> Ext(a, b)
4872  Ext(a, b)
4873  """
4874  ctx = a.ctx
4875  if z3_debug():
4876  _z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays")
4877  return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4878 
4879 
4880 def SetHasSize(a, k):
4881  ctx = a.ctx
4882  k = _py2expr(k, ctx)
4883  return _to_expr_ref(Z3_mk_set_has_size(ctx.ref(), a.as_ast(), k.as_ast()), ctx)
4884 
4885 
4886 def is_select(a):
4887  """Return `True` if `a` is a Z3 array select application.
4888 
4889  >>> a = Array('a', IntSort(), IntSort())
4890  >>> is_select(a)
4891  False
4892  >>> i = Int('i')
4893  >>> is_select(a[i])
4894  True
4895  """
4896  return is_app_of(a, Z3_OP_SELECT)
4897 
4898 
4899 def is_store(a):
4900  """Return `True` if `a` is a Z3 array store application.
4901 
4902  >>> a = Array('a', IntSort(), IntSort())
4903  >>> is_store(a)
4904  False
4905  >>> is_store(Store(a, 0, 1))
4906  True
4907  """
4908  return is_app_of(a, Z3_OP_STORE)
4909 
4910 
4915 
4916 
4917 def SetSort(s):
4918  """ Create a set sort over element sort s"""
4919  return ArraySort(s, BoolSort())
4920 
4921 
4922 def EmptySet(s):
4923  """Create the empty set
4924  >>> EmptySet(IntSort())
4925  K(Int, False)
4926  """
4927  ctx = s.ctx
4928  return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
4929 
4930 
4931 def FullSet(s):
4932  """Create the full set
4933  >>> FullSet(IntSort())
4934  K(Int, True)
4935  """
4936  ctx = s.ctx
4937  return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
4938 
4939 
4940 def SetUnion(*args):
4941  """ Take the union of sets
4942  >>> a = Const('a', SetSort(IntSort()))
4943  >>> b = Const('b', SetSort(IntSort()))
4944  >>> SetUnion(a, b)
4945  union(a, b)
4946  """
4947  args = _get_args(args)
4948  ctx = _ctx_from_ast_arg_list(args)
4949  _args, sz = _to_ast_array(args)
4950  return ArrayRef(Z3_mk_set_union(ctx.ref(), sz, _args), ctx)
4951 
4952 
4953 def SetIntersect(*args):
4954  """ Take the union of sets
4955  >>> a = Const('a', SetSort(IntSort()))
4956  >>> b = Const('b', SetSort(IntSort()))
4957  >>> SetIntersect(a, b)
4958  intersection(a, b)
4959  """
4960  args = _get_args(args)
4961  ctx = _ctx_from_ast_arg_list(args)
4962  _args, sz = _to_ast_array(args)
4963  return ArrayRef(Z3_mk_set_intersect(ctx.ref(), sz, _args), ctx)
4964 
4965 
4966 def SetAdd(s, e):
4967  """ Add element e to set s
4968  >>> a = Const('a', SetSort(IntSort()))
4969  >>> SetAdd(a, 1)
4970  Store(a, 1, True)
4971  """
4972  ctx = _ctx_from_ast_arg_list([s, e])
4973  e = _py2expr(e, ctx)
4974  return ArrayRef(Z3_mk_set_add(ctx.ref(), s.as_ast(), e.as_ast()), ctx)
4975 
4976 
4977 def SetDel(s, e):
4978  """ Remove element e to set s
4979  >>> a = Const('a', SetSort(IntSort()))
4980  >>> SetDel(a, 1)
4981  Store(a, 1, False)
4982  """
4983  ctx = _ctx_from_ast_arg_list([s, e])
4984  e = _py2expr(e, ctx)
4985  return ArrayRef(Z3_mk_set_del(ctx.ref(), s.as_ast(), e.as_ast()), ctx)
4986 
4987 
4989  """ The complement of set s
4990  >>> a = Const('a', SetSort(IntSort()))
4991  >>> SetComplement(a)
4992  complement(a)
4993  """
4994  ctx = s.ctx
4995  return ArrayRef(Z3_mk_set_complement(ctx.ref(), s.as_ast()), ctx)
4996 
4997 
4998 def SetDifference(a, b):
4999  """ The set difference of a and b
5000  >>> a = Const('a', SetSort(IntSort()))
5001  >>> b = Const('b', SetSort(IntSort()))
5002  >>> SetDifference(a, b)
5003  setminus(a, b)
5004  """
5005  ctx = _ctx_from_ast_arg_list([a, b])
5006  return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
5007 
5008 
5009 def IsMember(e, s):
5010  """ Check if e is a member of set s
5011  >>> a = Const('a', SetSort(IntSort()))
5012  >>> IsMember(1, a)
5013  a[1]
5014  """
5015  ctx = _ctx_from_ast_arg_list([s, e])
5016  e = _py2expr(e, ctx)
5017  return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx)
5018 
5019 
5020 def IsSubset(a, b):
5021  """ Check if a is a subset of b
5022  >>> a = Const('a', SetSort(IntSort()))
5023  >>> b = Const('b', SetSort(IntSort()))
5024  >>> IsSubset(a, b)
5025  subset(a, b)
5026  """
5027  ctx = _ctx_from_ast_arg_list([a, b])
5028  return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
5029 
5030 
5031 
5036 
5037 def _valid_accessor(acc):
5038  """Return `True` if acc is pair of the form (String, Datatype or Sort). """
5039  if not isinstance(acc, tuple):
5040  return False
5041  if len(acc) != 2:
5042  return False
5043  return isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1]))
5044 
5045 
5046 class Datatype:
5047  """Helper class for declaring Z3 datatypes.
5048 
5049  >>> List = Datatype('List')
5050  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5051  >>> List.declare('nil')
5052  >>> List = List.create()
5053  >>> # List is now a Z3 declaration
5054  >>> List.nil
5055  nil
5056  >>> List.cons(10, List.nil)
5057  cons(10, nil)
5058  >>> List.cons(10, List.nil).sort()
5059  List
5060  >>> cons = List.cons
5061  >>> nil = List.nil
5062  >>> car = List.car
5063  >>> cdr = List.cdr
5064  >>> n = cons(1, cons(0, nil))
5065  >>> n
5066  cons(1, cons(0, nil))
5067  >>> simplify(cdr(n))
5068  cons(0, nil)
5069  >>> simplify(car(n))
5070  1
5071  """
5072 
5073  def __init__(self, name, ctx=None):
5074  self.ctxctx = _get_ctx(ctx)
5075  self.namename = name
5076  self.constructorsconstructors = []
5077 
5078  def __deepcopy__(self, memo={}):
5079  r = Datatype(self.namename, self.ctxctx)
5080  r.constructors = copy.deepcopy(self.constructorsconstructors)
5081  return r
5082 
5083  def declare_core(self, name, rec_name, *args):
5084  if z3_debug():
5085  _z3_assert(isinstance(name, str), "String expected")
5086  _z3_assert(isinstance(rec_name, str), "String expected")
5087  _z3_assert(
5088  all([_valid_accessor(a) for a in args]),
5089  "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)",
5090  )
5091  self.constructorsconstructors.append((name, rec_name, args))
5092 
5093  def declare(self, name, *args):
5094  """Declare constructor named `name` with the given accessors `args`.
5095  Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort
5096  or a reference to the datatypes being declared.
5097 
5098  In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
5099  declares the constructor named `cons` that builds a new List using an integer and a List.
5100  It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer
5101  of a `cons` cell, and `cdr` the list of a `cons` cell. After all constructors were declared,
5102  we use the method create() to create the actual datatype in Z3.
5103 
5104  >>> List = Datatype('List')
5105  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5106  >>> List.declare('nil')
5107  >>> List = List.create()
5108  """
5109  if z3_debug():
5110  _z3_assert(isinstance(name, str), "String expected")
5111  _z3_assert(name != "", "Constructor name cannot be empty")
5112  return self.declare_coredeclare_core(name, "is-" + name, *args)
5113 
5114  def __repr__(self):
5115  return "Datatype(%s, %s)" % (self.namename, self.constructorsconstructors)
5116 
5117  def create(self):
5118  """Create a Z3 datatype based on the constructors declared using the method `declare()`.
5119 
5120  The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
5121 
5122  >>> List = Datatype('List')
5123  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5124  >>> List.declare('nil')
5125  >>> List = List.create()
5126  >>> List.nil
5127  nil
5128  >>> List.cons(10, List.nil)
5129  cons(10, nil)
5130  """
5131  return CreateDatatypes([self])[0]
5132 
5133 
5135  """Auxiliary object used to create Z3 datatypes."""
5136 
5137  def __init__(self, c, ctx):
5138  self.cc = c
5139  self.ctxctx = ctx
5140 
5141  def __del__(self):
5142  if self.ctxctx.ref() is not None and Z3_del_constructor is not None:
5143  Z3_del_constructor(self.ctxctx.ref(), self.cc)
5144 
5145 
5147  """Auxiliary object used to create Z3 datatypes."""
5148 
5149  def __init__(self, c, ctx):
5150  self.cc = c
5151  self.ctxctx = ctx
5152 
5153  def __del__(self):
5154  if self.ctxctx.ref() is not None and Z3_del_constructor_list is not None:
5155  Z3_del_constructor_list(self.ctxctx.ref(), self.cc)
5156 
5157 
5159  """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
5160 
5161  In the following example we define a Tree-List using two mutually recursive datatypes.
5162 
5163  >>> TreeList = Datatype('TreeList')
5164  >>> Tree = Datatype('Tree')
5165  >>> # Tree has two constructors: leaf and node
5166  >>> Tree.declare('leaf', ('val', IntSort()))
5167  >>> # a node contains a list of trees
5168  >>> Tree.declare('node', ('children', TreeList))
5169  >>> TreeList.declare('nil')
5170  >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
5171  >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
5172  >>> Tree.val(Tree.leaf(10))
5173  val(leaf(10))
5174  >>> simplify(Tree.val(Tree.leaf(10)))
5175  10
5176  >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
5177  >>> n1
5178  node(cons(leaf(10), cons(leaf(20), nil)))
5179  >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
5180  >>> simplify(n2 == n1)
5181  False
5182  >>> simplify(TreeList.car(Tree.children(n2)) == n1)
5183  True
5184  """
5185  ds = _get_args(ds)
5186  if z3_debug():
5187  _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
5188  _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
5189  _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
5190  _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
5191  ctx = ds[0].ctx
5192  num = len(ds)
5193  names = (Symbol * num)()
5194  out = (Sort * num)()
5195  clists = (ConstructorList * num)()
5196  to_delete = []
5197  for i in range(num):
5198  d = ds[i]
5199  names[i] = to_symbol(d.name, ctx)
5200  num_cs = len(d.constructors)
5201  cs = (Constructor * num_cs)()
5202  for j in range(num_cs):
5203  c = d.constructors[j]
5204  cname = to_symbol(c[0], ctx)
5205  rname = to_symbol(c[1], ctx)
5206  fs = c[2]
5207  num_fs = len(fs)
5208  fnames = (Symbol * num_fs)()
5209  sorts = (Sort * num_fs)()
5210  refs = (ctypes.c_uint * num_fs)()
5211  for k in range(num_fs):
5212  fname = fs[k][0]
5213  ftype = fs[k][1]
5214  fnames[k] = to_symbol(fname, ctx)
5215  if isinstance(ftype, Datatype):
5216  if z3_debug():
5217  _z3_assert(
5218  ds.count(ftype) == 1,
5219  "One and only one occurrence of each datatype is expected",
5220  )
5221  sorts[k] = None
5222  refs[k] = ds.index(ftype)
5223  else:
5224  if z3_debug():
5225  _z3_assert(is_sort(ftype), "Z3 sort expected")
5226  sorts[k] = ftype.ast
5227  refs[k] = 0
5228  cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
5229  to_delete.append(ScopedConstructor(cs[j], ctx))
5230  clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
5231  to_delete.append(ScopedConstructorList(clists[i], ctx))
5232  Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
5233  result = []
5234  # Create a field for every constructor, recognizer and accessor
5235  for i in range(num):
5236  dref = DatatypeSortRef(out[i], ctx)
5237  num_cs = dref.num_constructors()
5238  for j in range(num_cs):
5239  cref = dref.constructor(j)
5240  cref_name = cref.name()
5241  cref_arity = cref.arity()
5242  if cref.arity() == 0:
5243  cref = cref()
5244  setattr(dref, cref_name, cref)
5245  rref = dref.recognizer(j)
5246  setattr(dref, "is_" + cref_name, rref)
5247  for k in range(cref_arity):
5248  aref = dref.accessor(j, k)
5249  setattr(dref, aref.name(), aref)
5250  result.append(dref)
5251  return tuple(result)
5252 
5253 
5255  """Datatype sorts."""
5256 
5257  def num_constructors(self):
5258  """Return the number of constructors in the given Z3 datatype.
5259 
5260  >>> List = Datatype('List')
5261  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5262  >>> List.declare('nil')
5263  >>> List = List.create()
5264  >>> # List is now a Z3 declaration
5265  >>> List.num_constructors()
5266  2
5267  """
5268  return int(Z3_get_datatype_sort_num_constructors(self.ctx_refctx_ref(), self.astast))
5269 
5270  def constructor(self, idx):
5271  """Return a constructor of the datatype `self`.
5272 
5273  >>> List = Datatype('List')
5274  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5275  >>> List.declare('nil')
5276  >>> List = List.create()
5277  >>> # List is now a Z3 declaration
5278  >>> List.num_constructors()
5279  2
5280  >>> List.constructor(0)
5281  cons
5282  >>> List.constructor(1)
5283  nil
5284  """
5285  if z3_debug():
5286  _z3_assert(idx < self.num_constructorsnum_constructors(), "Invalid constructor index")
5287  return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_refctx_ref(), self.astast, idx), self.ctxctx)
5288 
5289  def recognizer(self, idx):
5290  """In Z3, each constructor has an associated recognizer predicate.
5291 
5292  If the constructor is named `name`, then the recognizer `is_name`.
5293 
5294  >>> List = Datatype('List')
5295  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5296  >>> List.declare('nil')
5297  >>> List = List.create()
5298  >>> # List is now a Z3 declaration
5299  >>> List.num_constructors()
5300  2
5301  >>> List.recognizer(0)
5302  is(cons)
5303  >>> List.recognizer(1)
5304  is(nil)
5305  >>> simplify(List.is_nil(List.cons(10, List.nil)))
5306  False
5307  >>> simplify(List.is_cons(List.cons(10, List.nil)))
5308  True
5309  >>> l = Const('l', List)
5310  >>> simplify(List.is_cons(l))
5311  is(cons, l)
5312  """
5313  if z3_debug():
5314  _z3_assert(idx < self.num_constructorsnum_constructors(), "Invalid recognizer index")
5315  return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_refctx_ref(), self.astast, idx), self.ctxctx)
5316 
5317  def accessor(self, i, j):
5318  """In Z3, each constructor has 0 or more accessor.
5319  The number of accessors is equal to the arity of the constructor.
5320 
5321  >>> List = Datatype('List')
5322  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5323  >>> List.declare('nil')
5324  >>> List = List.create()
5325  >>> List.num_constructors()
5326  2
5327  >>> List.constructor(0)
5328  cons
5329  >>> num_accs = List.constructor(0).arity()
5330  >>> num_accs
5331  2
5332  >>> List.accessor(0, 0)
5333  car
5334  >>> List.accessor(0, 1)
5335  cdr
5336  >>> List.constructor(1)
5337  nil
5338  >>> num_accs = List.constructor(1).arity()
5339  >>> num_accs
5340  0
5341  """
5342  if z3_debug():
5343  _z3_assert(i < self.num_constructorsnum_constructors(), "Invalid constructor index")
5344  _z3_assert(j < self.constructorconstructor(i).arity(), "Invalid accessor index")
5345  return FuncDeclRef(
5346  Z3_get_datatype_sort_constructor_accessor(self.ctx_refctx_ref(), self.astast, i, j),
5347  ctx=self.ctxctx,
5348  )
5349 
5350 
5352  """Datatype expressions."""
5353 
5354  def sort(self):
5355  """Return the datatype sort of the datatype expression `self`."""
5356  return DatatypeSortRef(Z3_get_sort(self.ctx_refctx_ref(), self.as_astas_astas_ast()), self.ctxctx)
5357 
5358 def DatatypeSort(name, ctx = None):
5359  """Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""
5360  ctx = _get_ctx(ctx)
5361  return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
5362 
5363 def TupleSort(name, sorts, ctx=None):
5364  """Create a named tuple sort base on a set of underlying sorts
5365  Example:
5366  >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])
5367  """
5368  tuple = Datatype(name, ctx)
5369  projects = [("project%d" % i, sorts[i]) for i in range(len(sorts))]
5370  tuple.declare(name, *projects)
5371  tuple = tuple.create()
5372  return tuple, tuple.constructor(0), [tuple.accessor(0, i) for i in range(len(sorts))]
5373 
5374 
5375 def DisjointSum(name, sorts, ctx=None):
5376  """Create a named tagged union sort base on a set of underlying sorts
5377  Example:
5378  >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
5379  """
5380  sum = Datatype(name, ctx)
5381  for i in range(len(sorts)):
5382  sum.declare("inject%d" % i, ("project%d" % i, sorts[i]))
5383  sum = sum.create()
5384  return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]
5385 
5386 
5387 def EnumSort(name, values, ctx=None):
5388  """Return a new enumeration sort named `name` containing the given values.
5389 
5390  The result is a pair (sort, list of constants).
5391  Example:
5392  >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5393  """
5394  if z3_debug():
5395  _z3_assert(isinstance(name, str), "Name must be a string")
5396  _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
5397  _z3_assert(len(values) > 0, "At least one value expected")
5398  ctx = _get_ctx(ctx)
5399  num = len(values)
5400  _val_names = (Symbol * num)()
5401  for i in range(num):
5402  _val_names[i] = to_symbol(values[i])
5403  _values = (FuncDecl * num)()
5404  _testers = (FuncDecl * num)()
5405  name = to_symbol(name)
5406  S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
5407  V = []
5408  for i in range(num):
5409  V.append(FuncDeclRef(_values[i], ctx))
5410  V = [a() for a in V]
5411  return S, V
5412 
5413 
5418 
5419 
5421  """Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3.
5422 
5423  Consider using the function `args2params` to create instances of this object.
5424  """
5425 
5426  def __init__(self, ctx=None, params=None):
5427  self.ctxctx = _get_ctx(ctx)
5428  if params is None:
5429  self.paramsparams = Z3_mk_params(self.ctxctx.ref())
5430  else:
5431  self.paramsparams = params
5432  Z3_params_inc_ref(self.ctxctx.ref(), self.paramsparams)
5433 
5434  def __deepcopy__(self, memo={}):
5435  return ParamsRef(self.ctxctx, self.paramsparams)
5436 
5437  def __del__(self):
5438  if self.ctxctx.ref() is not None and Z3_params_dec_ref is not None:
5439  Z3_params_dec_ref(self.ctxctx.ref(), self.paramsparams)
5440 
5441  def set(self, name, val):
5442  """Set parameter name with value val."""
5443  if z3_debug():
5444  _z3_assert(isinstance(name, str), "parameter name must be a string")
5445  name_sym = to_symbol(name, self.ctxctx)
5446  if isinstance(val, bool):
5447  Z3_params_set_bool(self.ctxctx.ref(), self.paramsparams, name_sym, val)
5448  elif _is_int(val):
5449  Z3_params_set_uint(self.ctxctx.ref(), self.paramsparams, name_sym, val)
5450  elif isinstance(val, float):
5451  Z3_params_set_double(self.ctxctx.ref(), self.paramsparams, name_sym, val)
5452  elif isinstance(val, str):
5453  Z3_params_set_symbol(self.ctxctx.ref(), self.paramsparams, name_sym, to_symbol(val, self.ctxctx))
5454  else:
5455  if z3_debug():
5456  _z3_assert(False, "invalid parameter value")
5457 
5458  def __repr__(self):
5459  return Z3_params_to_string(self.ctxctx.ref(), self.paramsparams)
5460 
5461  def validate(self, ds):
5462  _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected")
5463  Z3_params_validate(self.ctxctx.ref(), self.paramsparams, ds.descr)
5464 
5465 
5466 def args2params(arguments, keywords, ctx=None):
5467  """Convert python arguments into a Z3_params object.
5468  A ':' is added to the keywords, and '_' is replaced with '-'
5469 
5470  >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5471  (params model true relevancy 2 elim_and true)
5472  """
5473  if z3_debug():
5474  _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
5475  prev = None
5476  r = ParamsRef(ctx)
5477  for a in arguments:
5478  if prev is None:
5479  prev = a
5480  else:
5481  r.set(prev, a)
5482  prev = None
5483  for k in keywords:
5484  v = keywords[k]
5485  r.set(k, v)
5486  return r
5487 
5488 
5490  """Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3.
5491  """
5492 
5493  def __init__(self, descr, ctx=None):
5494  _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected")
5495  self.ctxctx = _get_ctx(ctx)
5496  self.descrdescr = descr
5497  Z3_param_descrs_inc_ref(self.ctxctx.ref(), self.descrdescr)
5498 
5499  def __deepcopy__(self, memo={}):
5500  return ParamsDescrsRef(self.descrdescr, self.ctxctx)
5501 
5502  def __del__(self):
5503  if self.ctxctx.ref() is not None and Z3_param_descrs_dec_ref is not None:
5504  Z3_param_descrs_dec_ref(self.ctxctx.ref(), self.descrdescr)
5505 
5506  def size(self):
5507  """Return the size of in the parameter description `self`.
5508  """
5509  return int(Z3_param_descrs_size(self.ctxctx.ref(), self.descrdescr))
5510 
5511  def __len__(self):
5512  """Return the size of in the parameter description `self`.
5513  """
5514  return self.sizesize()
5515 
5516  def get_name(self, i):
5517  """Return the i-th parameter name in the parameter description `self`.
5518  """
5519  return _symbol2py(self.ctxctx, Z3_param_descrs_get_name(self.ctxctx.ref(), self.descrdescr, i))
5520 
5521  def get_kind(self, n):
5522  """Return the kind of the parameter named `n`.
5523  """
5524  return Z3_param_descrs_get_kind(self.ctxctx.ref(), self.descrdescr, to_symbol(n, self.ctxctx))
5525 
5526  def get_documentation(self, n):
5527  """Return the documentation string of the parameter named `n`.
5528  """
5529  return Z3_param_descrs_get_documentation(self.ctxctx.ref(), self.descrdescr, to_symbol(n, self.ctxctx))
5530 
5531  def __getitem__(self, arg):
5532  if _is_int(arg):
5533  return self.get_nameget_name(arg)
5534  else:
5535  return self.get_kindget_kind(arg)
5536 
5537  def __repr__(self):
5538  return Z3_param_descrs_to_string(self.ctxctx.ref(), self.descrdescr)
5539 
5540 
5545 
5546 
5548  """Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible).
5549 
5550  Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
5551  A goal has a solution if one of its subgoals has a solution.
5552  A goal is unsatisfiable if all subgoals are unsatisfiable.
5553  """
5554 
5555  def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
5556  if z3_debug():
5557  _z3_assert(goal is None or ctx is not None,
5558  "If goal is different from None, then ctx must be also different from None")
5559  self.ctxctx = _get_ctx(ctx)
5560  self.goalgoal = goal
5561  if self.goalgoal is None:
5562  self.goalgoal = Z3_mk_goal(self.ctxctx.ref(), models, unsat_cores, proofs)
5563  Z3_goal_inc_ref(self.ctxctx.ref(), self.goalgoal)
5564 
5565  def __del__(self):
5566  if self.goalgoal is not None and self.ctxctx.ref() is not None and Z3_goal_dec_ref is not None:
5567  Z3_goal_dec_ref(self.ctxctx.ref(), self.goalgoal)
5568 
5569  def depth(self):
5570  """Return the depth of the goal `self`.
5571  The depth corresponds to the number of tactics applied to `self`.
5572 
5573  >>> x, y = Ints('x y')
5574  >>> g = Goal()
5575  >>> g.add(x == 0, y >= x + 1)
5576  >>> g.depth()
5577  0
5578  >>> r = Then('simplify', 'solve-eqs')(g)
5579  >>> # r has 1 subgoal
5580  >>> len(r)
5581  1
5582  >>> r[0].depth()
5583  2
5584  """
5585  return int(Z3_goal_depth(self.ctxctx.ref(), self.goalgoal))
5586 
5587  def inconsistent(self):
5588  """Return `True` if `self` contains the `False` constraints.
5589 
5590  >>> x, y = Ints('x y')
5591  >>> g = Goal()
5592  >>> g.inconsistent()
5593  False
5594  >>> g.add(x == 0, x == 1)
5595  >>> g
5596  [x == 0, x == 1]
5597  >>> g.inconsistent()
5598  False
5599  >>> g2 = Tactic('propagate-values')(g)[0]
5600  >>> g2.inconsistent()
5601  True
5602  """
5603  return Z3_goal_inconsistent(self.ctxctx.ref(), self.goalgoal)
5604 
5605  def prec(self):
5606  """Return the precision (under-approximation, over-approximation, or precise) of the goal `self`.
5607 
5608  >>> g = Goal()
5609  >>> g.prec() == Z3_GOAL_PRECISE
5610  True
5611  >>> x, y = Ints('x y')
5612  >>> g.add(x == y + 1)
5613  >>> g.prec() == Z3_GOAL_PRECISE
5614  True
5615  >>> t = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10)
5616  >>> g2 = t(g)[0]
5617  >>> g2
5618  [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
5619  >>> g2.prec() == Z3_GOAL_PRECISE
5620  False
5621  >>> g2.prec() == Z3_GOAL_UNDER
5622  True
5623  """
5624  return Z3_goal_precision(self.ctxctx.ref(), self.goalgoal)
5625 
5626  def precision(self):
5627  """Alias for `prec()`.
5628 
5629  >>> g = Goal()
5630  >>> g.precision() == Z3_GOAL_PRECISE
5631  True
5632  """
5633  return self.precprec()
5634 
5635  def size(self):
5636  """Return the number of constraints in the goal `self`.
5637 
5638  >>> g = Goal()
5639  >>> g.size()
5640  0
5641  >>> x, y = Ints('x y')
5642  >>> g.add(x == 0, y > x)
5643  >>> g.size()
5644  2
5645  """
5646  return int(Z3_goal_size(self.ctxctx.ref(), self.goalgoal))
5647 
5648  def __len__(self):
5649  """Return the number of constraints in the goal `self`.
5650 
5651  >>> g = Goal()
5652  >>> len(g)
5653  0
5654  >>> x, y = Ints('x y')
5655  >>> g.add(x == 0, y > x)
5656  >>> len(g)
5657  2
5658  """
5659  return self.sizesize()
5660 
5661  def get(self, i):
5662  """Return a constraint in the goal `self`.
5663 
5664  >>> g = Goal()
5665  >>> x, y = Ints('x y')
5666  >>> g.add(x == 0, y > x)
5667  >>> g.get(0)
5668  x == 0
5669  >>> g.get(1)
5670  y > x
5671  """
5672  return _to_expr_ref(Z3_goal_formula(self.ctxctx.ref(), self.goalgoal, i), self.ctxctx)
5673 
5674  def __getitem__(self, arg):
5675  """Return a constraint in the goal `self`.
5676 
5677  >>> g = Goal()
5678  >>> x, y = Ints('x y')
5679  >>> g.add(x == 0, y > x)
5680  >>> g[0]
5681  x == 0
5682  >>> g[1]
5683  y > x
5684  """
5685  if arg >= len(self):
5686  raise IndexError
5687  return self.getget(arg)
5688 
5689  def assert_exprs(self, *args):
5690  """Assert constraints into the goal.
5691 
5692  >>> x = Int('x')
5693  >>> g = Goal()
5694  >>> g.assert_exprs(x > 0, x < 2)
5695  >>> g
5696  [x > 0, x < 2]
5697  """
5698  args = _get_args(args)
5699  s = BoolSort(self.ctxctx)
5700  for arg in args:
5701  arg = s.cast(arg)
5702  Z3_goal_assert(self.ctxctx.ref(), self.goalgoal, arg.as_ast())
5703 
5704  def append(self, *args):
5705  """Add constraints.
5706 
5707  >>> x = Int('x')
5708  >>> g = Goal()
5709  >>> g.append(x > 0, x < 2)
5710  >>> g
5711  [x > 0, x < 2]
5712  """
5713  self.assert_exprsassert_exprs(*args)
5714 
5715  def insert(self, *args):
5716  """Add constraints.
5717 
5718  >>> x = Int('x')
5719  >>> g = Goal()
5720  >>> g.insert(x > 0, x < 2)
5721  >>> g
5722  [x > 0, x < 2]
5723  """
5724  self.assert_exprsassert_exprs(*args)
5725 
5726  def add(self, *args):
5727  """Add constraints.
5728 
5729  >>> x = Int('x')
5730  >>> g = Goal()
5731  >>> g.add(x > 0, x < 2)
5732  >>> g
5733  [x > 0, x < 2]
5734  """
5735  self.assert_exprsassert_exprs(*args)
5736 
5737  def convert_model(self, model):
5738  """Retrieve model from a satisfiable goal
5739  >>> a, b = Ints('a b')
5740  >>> g = Goal()
5741  >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
5742  >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs'))
5743  >>> r = t(g)
5744  >>> r[0]
5745  [Or(b == 0, b == 1), Not(0 <= b)]
5746  >>> r[1]
5747  [Or(b == 0, b == 1), Not(1 <= b)]
5748  >>> # Remark: the subgoal r[0] is unsatisfiable
5749  >>> # Creating a solver for solving the second subgoal
5750  >>> s = Solver()
5751  >>> s.add(r[1])
5752  >>> s.check()
5753  sat
5754  >>> s.model()
5755  [b = 0]
5756  >>> # Model s.model() does not assign a value to `a`
5757  >>> # It is a model for subgoal `r[1]`, but not for goal `g`
5758  >>> # The method convert_model creates a model for `g` from a model for `r[1]`.
5759  >>> r[1].convert_model(s.model())
5760  [b = 0, a = 1]
5761  """
5762  if z3_debug():
5763  _z3_assert(isinstance(model, ModelRef), "Z3 Model expected")
5764  return ModelRef(Z3_goal_convert_model(self.ctxctx.ref(), self.goalgoal, model.model), self.ctxctx)
5765 
5766  def __repr__(self):
5767  return obj_to_string(self)
5768 
5769  def sexpr(self):
5770  """Return a textual representation of the s-expression representing the goal."""
5771  return Z3_goal_to_string(self.ctxctx.ref(), self.goalgoal)
5772 
5773  def dimacs(self, include_names=True):
5774  """Return a textual representation of the goal in DIMACS format."""
5775  return Z3_goal_to_dimacs_string(self.ctxctx.ref(), self.goalgoal, include_names)
5776 
5777  def translate(self, target):
5778  """Copy goal `self` to context `target`.
5779 
5780  >>> x = Int('x')
5781  >>> g = Goal()
5782  >>> g.add(x > 10)
5783  >>> g
5784  [x > 10]
5785  >>> c2 = Context()
5786  >>> g2 = g.translate(c2)
5787  >>> g2
5788  [x > 10]
5789  >>> g.ctx == main_ctx()
5790  True
5791  >>> g2.ctx == c2
5792  True
5793  >>> g2.ctx == main_ctx()
5794  False
5795  """
5796  if z3_debug():
5797  _z3_assert(isinstance(target, Context), "target must be a context")
5798  return Goal(goal=Z3_goal_translate(self.ctxctx.ref(), self.goalgoal, target.ref()), ctx=target)
5799 
5800  def __copy__(self):
5801  return self.translatetranslate(self.ctxctx)
5802 
5803  def __deepcopy__(self, memo={}):
5804  return self.translatetranslate(self.ctxctx)
5805 
5806  def simplify(self, *arguments, **keywords):
5807  """Return a new simplified goal.
5808 
5809  This method is essentially invoking the simplify tactic.
5810 
5811  >>> g = Goal()
5812  >>> x = Int('x')
5813  >>> g.add(x + 1 >= 2)
5814  >>> g
5815  [x + 1 >= 2]
5816  >>> g2 = g.simplify()
5817  >>> g2
5818  [x >= 1]
5819  >>> # g was not modified
5820  >>> g
5821  [x + 1 >= 2]
5822  """
5823  t = Tactic("simplify")
5824  return t.apply(self, *arguments, **keywords)[0]
5825 
5826  def as_expr(self):
5827  """Return goal `self` as a single Z3 expression.
5828 
5829  >>> x = Int('x')
5830  >>> g = Goal()
5831  >>> g.as_expr()
5832  True
5833  >>> g.add(x > 1)
5834  >>> g.as_expr()
5835  x > 1
5836  >>> g.add(x < 10)
5837  >>> g.as_expr()
5838  And(x > 1, x < 10)
5839  """
5840  sz = len(self)
5841  if sz == 0:
5842  return BoolVal(True, self.ctxctx)
5843  elif sz == 1:
5844  return self.getget(0)
5845  else:
5846  return And([self.getget(i) for i in range(len(self))], self.ctxctx)
5847 
5848 
5853 
5854 
5856  """A collection (vector) of ASTs."""
5857 
5858  def __init__(self, v=None, ctx=None):
5859  self.vectorvector = None
5860  if v is None:
5861  self.ctxctx = _get_ctx(ctx)
5862  self.vectorvector = Z3_mk_ast_vector(self.ctxctx.ref())
5863  else:
5864  self.vectorvector = v
5865  assert ctx is not None
5866  self.ctxctx = ctx
5867  Z3_ast_vector_inc_ref(self.ctxctx.ref(), self.vectorvector)
5868 
5869  def __del__(self):
5870  if self.vectorvector is not None and self.ctxctx.ref() is not None and Z3_ast_vector_dec_ref is not None:
5871  Z3_ast_vector_dec_ref(self.ctxctx.ref(), self.vectorvector)
5872 
5873  def __len__(self):
5874  """Return the size of the vector `self`.
5875 
5876  >>> A = AstVector()
5877  >>> len(A)
5878  0
5879  >>> A.push(Int('x'))
5880  >>> A.push(Int('x'))
5881  >>> len(A)
5882  2
5883  """
5884  return int(Z3_ast_vector_size(self.ctxctx.ref(), self.vectorvector))
5885 
5886  def __getitem__(self, i):
5887  """Return the AST at position `i`.
5888 
5889  >>> A = AstVector()
5890  >>> A.push(Int('x') + 1)
5891  >>> A.push(Int('y'))
5892  >>> A[0]
5893  x + 1
5894  >>> A[1]
5895  y
5896  """
5897 
5898  if isinstance(i, int):
5899  if i < 0:
5900  i += self.__len____len__()
5901 
5902  if i >= self.__len____len__():
5903  raise IndexError
5904  return _to_ast_ref(Z3_ast_vector_get(self.ctxctx.ref(), self.vectorvector, i), self.ctxctx)
5905 
5906  elif isinstance(i, slice):
5907  result = []
5908  for ii in range(*i.indices(self.__len____len__())):
5909  result.append(_to_ast_ref(
5910  Z3_ast_vector_get(self.ctxctx.ref(), self.vectorvector, ii),
5911  self.ctxctx,
5912  ))
5913  return result
5914 
5915  def __setitem__(self, i, v):
5916  """Update AST at position `i`.
5917 
5918  >>> A = AstVector()
5919  >>> A.push(Int('x') + 1)
5920  >>> A.push(Int('y'))
5921  >>> A[0]
5922  x + 1
5923  >>> A[0] = Int('x')
5924  >>> A[0]
5925  x
5926  """
5927  if i >= self.__len____len__():
5928  raise IndexError
5929  Z3_ast_vector_set(self.ctxctx.ref(), self.vectorvector, i, v.as_ast())
5930 
5931  def push(self, v):
5932  """Add `v` in the end of the vector.
5933 
5934  >>> A = AstVector()
5935  >>> len(A)
5936  0
5937  >>> A.push(Int('x'))
5938  >>> len(A)
5939  1
5940  """
5941  Z3_ast_vector_push(self.ctxctx.ref(), self.vectorvector, v.as_ast())
5942 
5943  def resize(self, sz):
5944  """Resize the vector to `sz` elements.
5945 
5946  >>> A = AstVector()
5947  >>> A.resize(10)
5948  >>> len(A)
5949  10
5950  >>> for i in range(10): A[i] = Int('x')
5951  >>> A[5]
5952  x
5953  """
5954