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