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