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