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