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