00001
00002
00003
00004
00005
00006
00007
00008
00009 """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.
00010
00011 Several online tutorials for Z3Py are available at:
00012 http://rise4fun.com/Z3Py/tutorial/guide
00013
00014 Please send feedback, comments and/or corrections to leonardo@microsoft.com. Your comments are very valuable.
00015
00016 Small example:
00017
00018 >>> x = Int('x')
00019 >>> y = Int('y')
00020 >>> s = Solver()
00021 >>> s.add(x > 0)
00022 >>> s.add(x < 2)
00023 >>> s.add(y == x + 1)
00024 >>> s.check()
00025 sat
00026 >>> m = s.model()
00027 >>> m[x]
00028 1
00029 >>> m[y]
00030 2
00031
00032 Z3 exceptions:
00033
00034 >>> try:
00035 ... x = Int('x')
00036 ... y = Bool('y')
00037 ... # the expression x + y is type incorrect
00038 ... n = x + y
00039 ... except Z3Exception as ex:
00040 ... print("failed: %s" % ex)
00041 failed: sort mismatch
00042 """
00043 from z3core import *
00044 from z3types import *
00045 from z3consts import *
00046 from z3printer import *
00047 from fractions import Fraction
00048 import sys
00049 import io
00050
00051 if sys.version < '3':
00052 def _is_int(v):
00053 return isinstance(v, int) or isinstance(v, long)
00054 else:
00055 def _is_int(v):
00056 return isinstance(v, int)
00057
00058 def enable_trace(msg):
00059 Z3_enable_trace(msg)
00060
00061 def disable_trace(msg):
00062 Z3_disable_trace(msg)
00063
00064 def get_version_string():
00065 major = ctypes.c_uint(0)
00066 minor = ctypes.c_uint(0)
00067 build = ctypes.c_uint(0)
00068 rev = ctypes.c_uint(0)
00069 Z3_get_version(major, minor, build, rev)
00070 return "%s.%s.%s" % (major.value, minor.value, build.value)
00071
00072 def get_version():
00073 major = ctypes.c_uint(0)
00074 minor = ctypes.c_uint(0)
00075 build = ctypes.c_uint(0)
00076 rev = ctypes.c_uint(0)
00077 Z3_get_version(major, minor, build, rev)
00078 return (major.value, minor.value, build.value, rev.value)
00079
00080
00081
00082 def _z3_assert(cond, msg):
00083 if not cond:
00084 raise Z3Exception(msg)
00085
00086 def open_log(fname):
00087 """Log interaction to a file. This function must be invoked immediately after init(). """
00088 Z3_open_log(fname)
00089
00090 def append_log(s):
00091 """Append user-defined string to interaction log. """
00092 Z3_append_log(s)
00093
00094 def to_symbol(s, ctx=None):
00095 """Convert an integer or string into a Z3 symbol."""
00096 if isinstance(s, int):
00097 return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
00098 else:
00099 return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
00100
00101 def _symbol2py(ctx, s):
00102 """Convert a Z3 symbol back into a Python object. """
00103 if Z3_get_symbol_kind(ctx.ref(), s) == Z3_INT_SYMBOL:
00104 return "k!%s" % Z3_get_symbol_int(ctx.ref(), s)
00105 else:
00106 return Z3_get_symbol_string(ctx.ref(), s)
00107
00108 _error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
00109
00110
00111
00112 def _get_args(args):
00113 try:
00114 if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
00115 return args[0]
00116 else:
00117 return args
00118 except:
00119 return args
00120
00121 def _Z3python_error_handler_core(c, e):
00122
00123
00124 return
00125
00126 _Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)
00127
00128 def _to_param_value(val):
00129 if isinstance(val, bool):
00130 if val == True:
00131 return "true"
00132 else:
00133 return "false"
00134 else:
00135 return str(val)
00136
00137 class Context:
00138 """A Context manages all other Z3 objects, global configuration options, etc.
00139
00140 Z3Py uses a default global context. For most applications this is sufficient.
00141 An application may use multiple Z3 contexts. Objects created in one context
00142 cannot be used in another one. However, several objects may be "translated" from
00143 one context to another. It is not safe to access Z3 objects from multiple threads.
00144 The only exception is the method `interrupt()` that can be used to interrupt() a long
00145 computation.
00146 The initialization method receives global configuration options for the new context.
00147 """
00148 def __init__(self, *args, **kws):
00149 if __debug__:
00150 _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
00151 conf = Z3_mk_config()
00152 for key in kws:
00153 value = kws[key]
00154 Z3_set_param_value(conf, str(key).upper(), _to_param_value(value))
00155 prev = None
00156 for a in args:
00157 if prev == None:
00158 prev = a
00159 else:
00160 Z3_set_param_value(conf, str(prev), _to_param_value(a))
00161 prev = None
00162 self.lib = lib()
00163 self.ctx = Z3_mk_context_rc(conf)
00164 Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
00165 lib().Z3_set_error_handler.restype = None
00166 lib().Z3_set_error_handler.argtypes = [ContextObj, _error_handler_fptr]
00167 lib().Z3_set_error_handler(self.ctx, _Z3Python_error_handler)
00168 Z3_del_config(conf)
00169
00170 def __del__(self):
00171 self.lib.Z3_del_context(self.ctx)
00172
00173 def ref(self):
00174 """Return a reference to the actual C pointer to the Z3 context."""
00175 return self.ctx
00176
00177 def interrupt(self):
00178 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
00179
00180 This method can be invoked from a thread different from the one executing the
00181 interruptable procedure.
00182 """
00183 Z3_interrupt(self.ref())
00184
00185
00186
00187 _main_ctx = None
00188 def main_ctx():
00189 """Return a reference to the global Z3 context.
00190
00191 >>> x = Real('x')
00192 >>> x.ctx == main_ctx()
00193 True
00194 >>> c = Context()
00195 >>> c == main_ctx()
00196 False
00197 >>> x2 = Real('x', c)
00198 >>> x2.ctx == c
00199 True
00200 >>> eq(x, x2)
00201 False
00202 """
00203 global _main_ctx
00204 if _main_ctx == None:
00205 _main_ctx = Context()
00206 return _main_ctx
00207
00208 def _get_ctx(ctx):
00209 if ctx == None:
00210 return main_ctx()
00211 else:
00212 return ctx
00213
00214 def set_param(*args, **kws):
00215 """Set Z3 global (or module) parameters.
00216
00217 >>> set_param(precision=10)
00218 """
00219 if __debug__:
00220 _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
00221 new_kws = {}
00222 for k in kws:
00223 v = kws[k]
00224 if not set_pp_option(k, v):
00225 new_kws[k] = v
00226 for key in new_kws:
00227 value = new_kws[key]
00228 Z3_global_param_set(str(key).upper(), _to_param_value(value))
00229 prev = None
00230 for a in args:
00231 if prev == None:
00232 prev = a
00233 else:
00234 Z3_global_param_set(str(prev), _to_param_value(a))
00235 prev = None
00236
00237 def reset_params():
00238 """Reset all global (or module) parameters.
00239 """
00240 Z3_global_param_reset_all()
00241
00242 def set_option(*args, **kws):
00243 """Alias for 'set_param' for backward compatibility.
00244 """
00245 return set_param(*args, **kws)
00246
00247 def get_param(name):
00248 """Return the value of a Z3 global (or module) parameter
00249
00250 >>> get_param('nlsat.reorder')
00251 'true'
00252 """
00253 ptr = (ctypes.c_char_p * 1)()
00254 if Z3_global_param_get(str(name), ptr):
00255 r = z3core._to_pystr(ptr[0])
00256 return r
00257 raise Z3Exception("failed to retrieve value for '%s'" % name)
00258
00259
00260
00261
00262
00263
00264
00265
00266 class Z3PPObject:
00267 """Superclass for all Z3 objects that have support for pretty printing."""
00268 def use_pp(self):
00269 return True
00270
00271 class AstRef(Z3PPObject):
00272 """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions."""
00273 def __init__(self, ast, ctx=None):
00274 self.ast = ast
00275 self.ctx = _get_ctx(ctx)
00276 Z3_inc_ref(self.ctx.ref(), self.as_ast())
00277
00278 def __del__(self):
00279 Z3_dec_ref(self.ctx.ref(), self.as_ast())
00280
00281 def __str__(self):
00282 return obj_to_string(self)
00283
00284 def __repr__(self):
00285 return obj_to_string(self)
00286
00287 def sexpr(self):
00288 """Return an string representing the AST node in s-expression notation.
00289
00290 >>> x = Int('x')
00291 >>> ((x + 1)*x).sexpr()
00292 '(* (+ x 1) x)'
00293 """
00294 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
00295
00296 def as_ast(self):
00297 """Return a pointer to the corresponding C Z3_ast object."""
00298 return self.ast
00299
00300 def get_id(self):
00301 """Return unique identifier for object. It can be used for hash-tables and maps."""
00302 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
00303
00304
00305 def ctx_ref(self):
00306 """Return a reference to the C context where this AST node is stored."""
00307 return self.ctx.ref()
00308
00309 def eq(self, other):
00310 """Return `True` if `self` and `other` are structurally identical.
00311
00312 >>> x = Int('x')
00313 >>> n1 = x + 1
00314 >>> n2 = 1 + x
00315 >>> n1.eq(n2)
00316 False
00317 >>> n1 = simplify(n1)
00318 >>> n2 = simplify(n2)
00319 >>> n1.eq(n2)
00320 True
00321 """
00322 if __debug__:
00323 _z3_assert(is_ast(other), "Z3 AST expected")
00324 return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
00325
00326 def translate(self, target):
00327 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
00328
00329 >>> c1 = Context()
00330 >>> c2 = Context()
00331 >>> x = Int('x', c1)
00332 >>> y = Int('y', c2)
00333 >>> # Nodes in different contexts can't be mixed.
00334 >>> # However, we can translate nodes from one context to another.
00335 >>> x.translate(c2) + y
00336 x + y
00337 """
00338 if __debug__:
00339 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
00340 return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
00341
00342 def hash(self):
00343 """Return a hashcode for the `self`.
00344
00345 >>> n1 = simplify(Int('x') + 1)
00346 >>> n2 = simplify(2 + Int('x') - 1)
00347 >>> n1.hash() == n2.hash()
00348 True
00349 """
00350 return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
00351
00352 def is_ast(a):
00353 """Return `True` if `a` is an AST node.
00354
00355 >>> is_ast(10)
00356 False
00357 >>> is_ast(IntVal(10))
00358 True
00359 >>> is_ast(Int('x'))
00360 True
00361 >>> is_ast(BoolSort())
00362 True
00363 >>> is_ast(Function('f', IntSort(), IntSort()))
00364 True
00365 >>> is_ast("x")
00366 False
00367 >>> is_ast(Solver())
00368 False
00369 """
00370 return isinstance(a, AstRef)
00371
00372 def eq(a, b):
00373 """Return `True` if `a` and `b` are structurally identical AST nodes.
00374
00375 >>> x = Int('x')
00376 >>> y = Int('y')
00377 >>> eq(x, y)
00378 False
00379 >>> eq(x + 1, x + 1)
00380 True
00381 >>> eq(x + 1, 1 + x)
00382 False
00383 >>> eq(simplify(x + 1), simplify(1 + x))
00384 True
00385 """
00386 if __debug__:
00387 _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
00388 return a.eq(b)
00389
00390 def _ast_kind(ctx, a):
00391 if is_ast(a):
00392 a = a.as_ast()
00393 return Z3_get_ast_kind(ctx.ref(), a)
00394
00395 def _ctx_from_ast_arg_list(args, default_ctx=None):
00396 ctx = None
00397 for a in args:
00398 if is_ast(a) or is_probe(a):
00399 if ctx == None:
00400 ctx = a.ctx
00401 else:
00402 if __debug__:
00403 _z3_assert(ctx == a.ctx, "Context mismatch")
00404 if ctx == None:
00405 ctx = default_ctx
00406 return ctx
00407
00408 def _ctx_from_ast_args(*args):
00409 return _ctx_from_ast_arg_list(args)
00410
00411 def _to_func_decl_array(args):
00412 sz = len(args)
00413 _args = (FuncDecl * sz)()
00414 for i in range(sz):
00415 _args[i] = args[i].as_func_decl()
00416 return _args, sz
00417
00418 def _to_ast_array(args):
00419 sz = len(args)
00420 _args = (Ast * sz)()
00421 for i in range(sz):
00422 _args[i] = args[i].as_ast()
00423 return _args, sz
00424
00425 def _to_ref_array(ref, args):
00426 sz = len(args)
00427 _args = (ref * sz)()
00428 for i in range(sz):
00429 _args[i] = args[i].as_ast()
00430 return _args, sz
00431
00432 def _to_ast_ref(a, ctx):
00433 k = _ast_kind(ctx, a)
00434 if k == Z3_SORT_AST:
00435 return _to_sort_ref(a, ctx)
00436 elif k == Z3_FUNC_DECL_AST:
00437 return _to_func_decl_ref(a, ctx)
00438 else:
00439 return _to_expr_ref(a, ctx)
00440
00441
00442
00443
00444
00445
00446
00447 def _sort_kind(ctx, s):
00448 return Z3_get_sort_kind(ctx.ref(), s)
00449
00450 class SortRef(AstRef):
00451 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node."""
00452 def as_ast(self):
00453 return Z3_sort_to_ast(self.ctx_ref(), self.ast)
00454
00455 def get_id(self):
00456 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
00457
00458
00459 def kind(self):
00460 """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
00461
00462 >>> b = BoolSort()
00463 >>> b.kind() == Z3_BOOL_SORT
00464 True
00465 >>> b.kind() == Z3_INT_SORT
00466 False
00467 >>> A = ArraySort(IntSort(), IntSort())
00468 >>> A.kind() == Z3_ARRAY_SORT
00469 True
00470 >>> A.kind() == Z3_INT_SORT
00471 False
00472 """
00473 return _sort_kind(self.ctx, self.ast)
00474
00475 def subsort(self, other):
00476 """Return `True` if `self` is a subsort of `other`.
00477
00478 >>> IntSort().subsort(RealSort())
00479 True
00480 """
00481 return False
00482
00483 def cast(self, val):
00484 """Try to cast `val` as an element of sort `self`.
00485
00486 This method is used in Z3Py to convert Python objects such as integers,
00487 floats, longs and strings into Z3 expressions.
00488
00489 >>> x = Int('x')
00490 >>> RealSort().cast(x)
00491 ToReal(x)
00492 """
00493 if __debug__:
00494 _z3_assert(is_expr(val), "Z3 expression expected")
00495 _z3_assert(self.eq(val.sort()), "Sort mismatch")
00496 return val
00497
00498 def name(self):
00499 """Return the name (string) of sort `self`.
00500
00501 >>> BoolSort().name()
00502 'Bool'
00503 >>> ArraySort(IntSort(), IntSort()).name()
00504 'Array'
00505 """
00506 return _symbol2py(self.ctx, Z3_get_sort_name(self.ctx_ref(), self.ast))
00507
00508 def __eq__(self, other):
00509 """Return `True` if `self` and `other` are the same Z3 sort.
00510
00511 >>> p = Bool('p')
00512 >>> p.sort() == BoolSort()
00513 True
00514 >>> p.sort() == IntSort()
00515 False
00516 """
00517 if other == None:
00518 return False
00519 return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
00520
00521 def __ne__(self, other):
00522 """Return `True` if `self` and `other` are not the same Z3 sort.
00523
00524 >>> p = Bool('p')
00525 >>> p.sort() != BoolSort()
00526 False
00527 >>> p.sort() != IntSort()
00528 True
00529 """
00530 return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
00531
00532 def is_sort(s):
00533 """Return `True` if `s` is a Z3 sort.
00534
00535 >>> is_sort(IntSort())
00536 True
00537 >>> is_sort(Int('x'))
00538 False
00539 >>> is_expr(Int('x'))
00540 True
00541 """
00542 return isinstance(s, SortRef)
00543
00544 def _to_sort_ref(s, ctx):
00545 if __debug__:
00546 _z3_assert(isinstance(s, Sort), "Z3 Sort expected")
00547 k = _sort_kind(ctx, s)
00548 if k == Z3_BOOL_SORT:
00549 return BoolSortRef(s, ctx)
00550 elif k == Z3_INT_SORT or k == Z3_REAL_SORT:
00551 return ArithSortRef(s, ctx)
00552 elif k == Z3_BV_SORT:
00553 return BitVecSortRef(s, ctx)
00554 elif k == Z3_ARRAY_SORT:
00555 return ArraySortRef(s, ctx)
00556 elif k == Z3_DATATYPE_SORT:
00557 return DatatypeSortRef(s, ctx)
00558 return SortRef(s, ctx)
00559
00560 def _sort(ctx, a):
00561 return _to_sort_ref(Z3_get_sort(ctx.ref(), a), ctx)
00562
00563 def DeclareSort(name, ctx=None):
00564 """Create a new uninterpred sort named `name`.
00565
00566 If `ctx=None`, then the new sort is declared in the global Z3Py context.
00567
00568 >>> A = DeclareSort('A')
00569 >>> a = Const('a', A)
00570 >>> b = Const('b', A)
00571 >>> a.sort() == A
00572 True
00573 >>> b.sort() == A
00574 True
00575 >>> a == b
00576 a == b
00577 """
00578 ctx = _get_ctx(ctx)
00579 return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
00580
00581
00582
00583
00584
00585
00586
00587 class FuncDeclRef(AstRef):
00588 """Function declaration. Every constant and function have an associated declaration.
00589
00590 The declaration assigns a name, a sort (i.e., type), and for function
00591 the sort (i.e., type) of each of its arguments. Note that, in Z3,
00592 a constant is a function with 0 arguments.
00593 """
00594 def as_ast(self):
00595 return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
00596
00597 def get_id(self):
00598 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
00599
00600 def as_func_decl(self):
00601 return self.ast
00602
00603 def name(self):
00604 """Return the name of the function declaration `self`.
00605
00606 >>> f = Function('f', IntSort(), IntSort())
00607 >>> f.name()
00608 'f'
00609 >>> isinstance(f.name(), str)
00610 True
00611 """
00612 return _symbol2py(self.ctx, Z3_get_decl_name(self.ctx_ref(), self.ast))
00613
00614 def arity(self):
00615 """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0.
00616
00617 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
00618 >>> f.arity()
00619 2
00620 """
00621 return int(Z3_get_arity(self.ctx_ref(), self.ast))
00622
00623 def domain(self, i):
00624 """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`.
00625
00626 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
00627 >>> f.domain(0)
00628 Int
00629 >>> f.domain(1)
00630 Real
00631 """
00632 if __debug__:
00633 _z3_assert(i < self.arity(), "Index out of bounds")
00634 return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
00635
00636 def range(self):
00637 """Return the sort of the range of a function declaration. For constants, this is the sort of the constant.
00638
00639 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
00640 >>> f.range()
00641 Bool
00642 """
00643 return _to_sort_ref(Z3_get_range(self.ctx_ref(), self.ast), self.ctx)
00644
00645 def kind(self):
00646 """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
00647
00648 >>> x = Int('x')
00649 >>> d = (x + 1).decl()
00650 >>> d.kind() == Z3_OP_ADD
00651 True
00652 >>> d.kind() == Z3_OP_MUL
00653 False
00654 """
00655 return Z3_get_decl_kind(self.ctx_ref(), self.ast)
00656
00657 def __call__(self, *args):
00658 """Create a Z3 application expression using the function `self`, and the given arguments.
00659
00660 The arguments must be Z3 expressions. This method assumes that
00661 the sorts of the elements in `args` match the sorts of the
00662 domain. Limited coersion is supported. For example, if
00663 args[0] is a Python integer, and the function expects a Z3
00664 integer, then the argument is automatically converted into a
00665 Z3 integer.
00666
00667 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
00668 >>> x = Int('x')
00669 >>> y = Real('y')
00670 >>> f(x, y)
00671 f(x, y)
00672 >>> f(x, x)
00673 f(x, ToReal(x))
00674 """
00675 args = _get_args(args)
00676 num = len(args)
00677 if __debug__:
00678 _z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self)
00679 _args = (Ast * num)()
00680 saved = []
00681 for i in range(num):
00682
00683
00684 tmp = self.domain(i).cast(args[i])
00685 saved.append(tmp)
00686 _args[i] = tmp.as_ast()
00687 return _to_expr_ref(Z3_mk_app(self.ctx_ref(), self.ast, len(args), _args), self.ctx)
00688
00689 def is_func_decl(a):
00690 """Return `True` if `a` is a Z3 function declaration.
00691
00692 >>> f = Function('f', IntSort(), IntSort())
00693 >>> is_func_decl(f)
00694 True
00695 >>> x = Real('x')
00696 >>> is_func_decl(x)
00697 False
00698 """
00699 return isinstance(a, FuncDeclRef)
00700
00701 def Function(name, *sig):
00702 """Create a new Z3 uninterpreted function with the given sorts.
00703
00704 >>> f = Function('f', IntSort(), IntSort())
00705 >>> f(f(0))
00706 f(f(0))
00707 """
00708 sig = _get_args(sig)
00709 if __debug__:
00710 _z3_assert(len(sig) > 0, "At least two arguments expected")
00711 arity = len(sig) - 1
00712 rng = sig[arity]
00713 if __debug__:
00714 _z3_assert(is_sort(rng), "Z3 sort expected")
00715 dom = (Sort * arity)()
00716 for i in range(arity):
00717 if __debug__:
00718 _z3_assert(is_sort(sig[i]), "Z3 sort expected")
00719 dom[i] = sig[i].ast
00720 ctx = rng.ctx
00721 return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
00722
00723 def _to_func_decl_ref(a, ctx):
00724 return FuncDeclRef(a, ctx)
00725
00726
00727
00728
00729
00730
00731
00732 class ExprRef(AstRef):
00733 """Constraints, formulas and terms are expressions in Z3.
00734
00735 Expressions are ASTs. Every expression has a sort.
00736 There are three main kinds of expressions:
00737 function applications, quantifiers and bounded variables.
00738 A constant is a function application with 0 arguments.
00739 For quantifier free problems, all expressions are
00740 function applications.
00741 """
00742 def as_ast(self):
00743 return self.ast
00744
00745 def get_id(self):
00746 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
00747
00748 def sort(self):
00749 """Return the sort of expression `self`.
00750
00751 >>> x = Int('x')
00752 >>> (x + 1).sort()
00753 Int
00754 >>> y = Real('y')
00755 >>> (x + y).sort()
00756 Real
00757 """
00758 return _sort(self.ctx, self.as_ast())
00759
00760 def sort_kind(self):
00761 """Shorthand for `self.sort().kind()`.
00762
00763 >>> a = Array('a', IntSort(), IntSort())
00764 >>> a.sort_kind() == Z3_ARRAY_SORT
00765 True
00766 >>> a.sort_kind() == Z3_INT_SORT
00767 False
00768 """
00769 return self.sort().kind()
00770
00771 def __eq__(self, other):
00772 """Return a Z3 expression that represents the constraint `self == other`.
00773
00774 If `other` is `None`, then this method simply returns `False`.
00775
00776 >>> a = Int('a')
00777 >>> b = Int('b')
00778 >>> a == b
00779 a == b
00780 >>> a == None
00781 False
00782 """
00783 if other == None:
00784 return False
00785 a, b = _coerce_exprs(self, other)
00786 return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
00787
00788 def __ne__(self, other):
00789 """Return a Z3 expression that represents the constraint `self != other`.
00790
00791 If `other` is `None`, then this method simply returns `True`.
00792
00793 >>> a = Int('a')
00794 >>> b = Int('b')
00795 >>> a != b
00796 a != b
00797 >>> a != None
00798 True
00799 """
00800 if other == None:
00801 return True
00802 a, b = _coerce_exprs(self, other)
00803 _args, sz = _to_ast_array((a, b))
00804 return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
00805
00806 def decl(self):
00807 """Return the Z3 function declaration associated with a Z3 application.
00808
00809 >>> f = Function('f', IntSort(), IntSort())
00810 >>> a = Int('a')
00811 >>> t = f(a)
00812 >>> eq(t.decl(), f)
00813 True
00814 >>> (a + 1).decl()
00815 +
00816 """
00817 if __debug__:
00818 _z3_assert(is_app(self), "Z3 application expected")
00819 return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
00820
00821 def num_args(self):
00822 """Return the number of arguments of a Z3 application.
00823
00824 >>> a = Int('a')
00825 >>> b = Int('b')
00826 >>> (a + b).num_args()
00827 2
00828 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
00829 >>> t = f(a, b, 0)
00830 >>> t.num_args()
00831 3
00832 """
00833 if __debug__:
00834 _z3_assert(is_app(self), "Z3 application expected")
00835 return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))
00836
00837 def arg(self, idx):
00838 """Return argument `idx` of the application `self`.
00839
00840 This method assumes that `self` is a function application with at least `idx+1` arguments.
00841
00842 >>> a = Int('a')
00843 >>> b = Int('b')
00844 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
00845 >>> t = f(a, b, 0)
00846 >>> t.arg(0)
00847 a
00848 >>> t.arg(1)
00849 b
00850 >>> t.arg(2)
00851 0
00852 """
00853 if __debug__:
00854 _z3_assert(is_app(self), "Z3 application expected")
00855 _z3_assert(idx < self.num_args(), "Invalid argument index")
00856 return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
00857
00858 def children(self):
00859 """Return a list containing the children of the given expression
00860
00861 >>> a = Int('a')
00862 >>> b = Int('b')
00863 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
00864 >>> t = f(a, b, 0)
00865 >>> t.children()
00866 [a, b, 0]
00867 """
00868 if is_app(self):
00869 return [self.arg(i) for i in range(self.num_args())]
00870 else:
00871 return []
00872
00873 def _to_expr_ref(a, ctx):
00874 if isinstance(a, Pattern):
00875 return PatternRef(a, ctx)
00876 ctx_ref = ctx.ref()
00877 k = Z3_get_ast_kind(ctx_ref, a)
00878 if k == Z3_QUANTIFIER_AST:
00879 return QuantifierRef(a, ctx)
00880 sk = Z3_get_sort_kind(ctx_ref, Z3_get_sort(ctx_ref, a))
00881 if sk == Z3_BOOL_SORT:
00882 return BoolRef(a, ctx)
00883 if sk == Z3_INT_SORT:
00884 if k == Z3_NUMERAL_AST:
00885 return IntNumRef(a, ctx)
00886 return ArithRef(a, ctx)
00887 if sk == Z3_REAL_SORT:
00888 if k == Z3_NUMERAL_AST:
00889 return RatNumRef(a, ctx)
00890 if _is_algebraic(ctx, a):
00891 return AlgebraicNumRef(a, ctx)
00892 return ArithRef(a, ctx)
00893 if sk == Z3_BV_SORT:
00894 if k == Z3_NUMERAL_AST:
00895 return BitVecNumRef(a, ctx)
00896 else:
00897 return BitVecRef(a, ctx)
00898 if sk == Z3_ARRAY_SORT:
00899 return ArrayRef(a, ctx)
00900 if sk == Z3_DATATYPE_SORT:
00901 return DatatypeRef(a, ctx)
00902 return ExprRef(a, ctx)
00903
00904 def _coerce_expr_merge(s, a):
00905 if is_expr(a):
00906 s1 = a.sort()
00907 if s == None:
00908 return s1
00909 if s1.eq(s):
00910 return s
00911 elif s.subsort(s1):
00912 return s1
00913 elif s1.subsort(s):
00914 return s
00915 else:
00916 if __debug__:
00917 _z3_assert(s1.ctx == s.ctx, "context mismatch")
00918 _z3_assert(False, "sort mismatch")
00919 else:
00920 return s
00921
00922 def _coerce_exprs(a, b, ctx=None):
00923 if not is_expr(a) and not is_expr(b):
00924 a = _py2expr(a, ctx)
00925 b = _py2expr(b, ctx)
00926 s = None
00927 s = _coerce_expr_merge(s, a)
00928 s = _coerce_expr_merge(s, b)
00929 a = s.cast(a)
00930 b = s.cast(b)
00931 return (a, b)
00932
00933 def _reduce(f, l, a):
00934 r = a
00935 for e in l:
00936 r = f(r, e)
00937 return r
00938
00939 def _coerce_expr_list(alist, ctx=None):
00940 has_expr = False
00941 for a in alist:
00942 if is_expr(a):
00943 has_expr = True
00944 break
00945 if not has_expr:
00946 alist = [ _py2expr(a, ctx) for a in alist ]
00947 s = _reduce(_coerce_expr_merge, alist, None)
00948 return [ s.cast(a) for a in alist ]
00949
00950 def is_expr(a):
00951 """Return `True` if `a` is a Z3 expression.
00952
00953 >>> a = Int('a')
00954 >>> is_expr(a)
00955 True
00956 >>> is_expr(a + 1)
00957 True
00958 >>> is_expr(IntSort())
00959 False
00960 >>> is_expr(1)
00961 False
00962 >>> is_expr(IntVal(1))
00963 True
00964 >>> x = Int('x')
00965 >>> is_expr(ForAll(x, x >= 0))
00966 True
00967 """
00968 return isinstance(a, ExprRef)
00969
00970 def is_app(a):
00971 """Return `True` if `a` is a Z3 function application.
00972
00973 Note that, constants are function applications with 0 arguments.
00974
00975 >>> a = Int('a')
00976 >>> is_app(a)
00977 True
00978 >>> is_app(a + 1)
00979 True
00980 >>> is_app(IntSort())
00981 False
00982 >>> is_app(1)
00983 False
00984 >>> is_app(IntVal(1))
00985 True
00986 >>> x = Int('x')
00987 >>> is_app(ForAll(x, x >= 0))
00988 False
00989 """
00990 if not isinstance(a, ExprRef):
00991 return False
00992 k = _ast_kind(a.ctx, a)
00993 return k == Z3_NUMERAL_AST or k == Z3_APP_AST
00994
00995 def is_const(a):
00996 """Return `True` if `a` is Z3 constant/variable expression.
00997
00998 >>> a = Int('a')
00999 >>> is_const(a)
01000 True
01001 >>> is_const(a + 1)
01002 False
01003 >>> is_const(1)
01004 False
01005 >>> is_const(IntVal(1))
01006 True
01007 >>> x = Int('x')
01008 >>> is_const(ForAll(x, x >= 0))
01009 False
01010 """
01011 return is_app(a) and a.num_args() == 0
01012
01013 def is_var(a):
01014 """Return `True` if `a` is variable.
01015
01016 Z3 uses de-Bruijn indices for representing bound variables in
01017 quantifiers.
01018
01019 >>> x = Int('x')
01020 >>> is_var(x)
01021 False
01022 >>> is_const(x)
01023 True
01024 >>> f = Function('f', IntSort(), IntSort())
01025 >>> # Z3 replaces x with bound variables when ForAll is executed.
01026 >>> q = ForAll(x, f(x) == x)
01027 >>> b = q.body()
01028 >>> b
01029 f(Var(0)) == Var(0)
01030 >>> b.arg(1)
01031 Var(0)
01032 >>> is_var(b.arg(1))
01033 True
01034 """
01035 return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
01036
01037 def get_var_index(a):
01038 """Return the de-Bruijn index of the Z3 bounded variable `a`.
01039
01040 >>> x = Int('x')
01041 >>> y = Int('y')
01042 >>> is_var(x)
01043 False
01044 >>> is_const(x)
01045 True
01046 >>> f = Function('f', IntSort(), IntSort(), IntSort())
01047 >>> # Z3 replaces x and y with bound variables when ForAll is executed.
01048 >>> q = ForAll([x, y], f(x, y) == x + y)
01049 >>> q.body()
01050 f(Var(1), Var(0)) == Var(1) + Var(0)
01051 >>> b = q.body()
01052 >>> b.arg(0)
01053 f(Var(1), Var(0))
01054 >>> v1 = b.arg(0).arg(0)
01055 >>> v2 = b.arg(0).arg(1)
01056 >>> v1
01057 Var(1)
01058 >>> v2
01059 Var(0)
01060 >>> get_var_index(v1)
01061 1
01062 >>> get_var_index(v2)
01063 0
01064 """
01065 if __debug__:
01066 _z3_assert(is_var(a), "Z3 bound variable expected")
01067 return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
01068
01069 def is_app_of(a, k):
01070 """Return `True` if `a` is an application of the given kind `k`.
01071
01072 >>> x = Int('x')
01073 >>> n = x + 1
01074 >>> is_app_of(n, Z3_OP_ADD)
01075 True
01076 >>> is_app_of(n, Z3_OP_MUL)
01077 False
01078 """
01079 return is_app(a) and a.decl().kind() == k
01080
01081 def If(a, b, c, ctx=None):
01082 """Create a Z3 if-then-else expression.
01083
01084 >>> x = Int('x')
01085 >>> y = Int('y')
01086 >>> max = If(x > y, x, y)
01087 >>> max
01088 If(x > y, x, y)
01089 >>> simplify(max)
01090 If(x <= y, y, x)
01091 """
01092 if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic):
01093 return Cond(a, b, c, ctx)
01094 else:
01095 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
01096 s = BoolSort(ctx)
01097 a = s.cast(a)
01098 b, c = _coerce_exprs(b, c, ctx)
01099 if __debug__:
01100 _z3_assert(a.ctx == b.ctx, "Context mismatch")
01101 return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
01102
01103 def Distinct(*args):
01104 """Create a Z3 distinct expression.
01105
01106 >>> x = Int('x')
01107 >>> y = Int('y')
01108 >>> Distinct(x, y)
01109 x != y
01110 >>> z = Int('z')
01111 >>> Distinct(x, y, z)
01112 Distinct(x, y, z)
01113 >>> simplify(Distinct(x, y, z))
01114 Distinct(x, y, z)
01115 >>> simplify(Distinct(x, y, z), blast_distinct=True)
01116 And(Not(x == y), Not(x == z), Not(y == z))
01117 """
01118 args = _get_args(args)
01119 ctx = _ctx_from_ast_arg_list(args)
01120 if __debug__:
01121 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
01122 args = _coerce_expr_list(args, ctx)
01123 _args, sz = _to_ast_array(args)
01124 return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
01125
01126 def _mk_bin(f, a, b):
01127 args = (Ast * 2)()
01128 if __debug__:
01129 _z3_assert(a.ctx == b.ctx, "Context mismatch")
01130 args[0] = a.as_ast()
01131 args[1] = b.as_ast()
01132 return f(a.ctx.ref(), 2, args)
01133
01134 def Const(name, sort):
01135 """Create a constant of the given sort.
01136
01137 >>> Const('x', IntSort())
01138 x
01139 """
01140 if __debug__:
01141 _z3_assert(isinstance(sort, SortRef), "Z3 sort expected")
01142 ctx = sort.ctx
01143 return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
01144
01145 def Consts(names, sort):
01146 """Create a several constants of the given sort.
01147
01148 `names` is a string containing the names of all constants to be created.
01149 Blank spaces separate the names of different constants.
01150
01151 >>> x, y, z = Consts('x y z', IntSort())
01152 >>> x + y + z
01153 x + y + z
01154 """
01155 if isinstance(names, str):
01156 names = names.split(" ")
01157 return [Const(name, sort) for name in names]
01158
01159 def Var(idx, s):
01160 """Create a Z3 free variable. Free variables are used to create quantified formulas.
01161
01162 >>> Var(0, IntSort())
01163 Var(0)
01164 >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
01165 False
01166 """
01167 if __debug__:
01168 _z3_assert(is_sort(s), "Z3 sort expected")
01169 return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
01170
01171 def RealVar(idx, ctx=None):
01172 """
01173 Create a real free variable. Free variables are used to create quantified formulas.
01174 They are also used to create polynomials.
01175
01176 >>> RealVar(0)
01177 Var(0)
01178 """
01179 return Var(idx, RealSort(ctx))
01180
01181 def RealVarVector(n, ctx=None):
01182 """
01183 Create a list of Real free variables.
01184 The variables have ids: 0, 1, ..., n-1
01185
01186 >>> x0, x1, x2, x3 = RealVarVector(4)
01187 >>> x2
01188 Var(2)
01189 """
01190 return [ RealVar(i, ctx) for i in range(n) ]
01191
01192
01193
01194
01195
01196
01197
01198 class BoolSortRef(SortRef):
01199 """Boolean sort."""
01200 def cast(self, val):
01201 """Try to cast `val` as a Boolean.
01202
01203 >>> x = BoolSort().cast(True)
01204 >>> x
01205 True
01206 >>> is_expr(x)
01207 True
01208 >>> is_expr(True)
01209 False
01210 >>> x.sort()
01211 Bool
01212 """
01213 if isinstance(val, bool):
01214 return BoolVal(val, self.ctx)
01215 if __debug__:
01216 _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected")
01217 _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
01218 return val
01219
01220 class BoolRef(ExprRef):
01221 """All Boolean expressions are instances of this class."""
01222 def sort(self):
01223 return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
01224
01225 def is_bool(a):
01226 """Return `True` if `a` is a Z3 Boolean expression.
01227
01228 >>> p = Bool('p')
01229 >>> is_bool(p)
01230 True
01231 >>> q = Bool('q')
01232 >>> is_bool(And(p, q))
01233 True
01234 >>> x = Real('x')
01235 >>> is_bool(x)
01236 False
01237 >>> is_bool(x == 0)
01238 True
01239 """
01240 return isinstance(a, BoolRef)
01241
01242 def is_true(a):
01243 """Return `True` if `a` is the Z3 true expression.
01244
01245 >>> p = Bool('p')
01246 >>> is_true(p)
01247 False
01248 >>> is_true(simplify(p == p))
01249 True
01250 >>> x = Real('x')
01251 >>> is_true(x == 0)
01252 False
01253 >>> # True is a Python Boolean expression
01254 >>> is_true(True)
01255 False
01256 """
01257 return is_app_of(a, Z3_OP_TRUE)
01258
01259 def is_false(a):
01260 """Return `True` if `a` is the Z3 false expression.
01261
01262 >>> p = Bool('p')
01263 >>> is_false(p)
01264 False
01265 >>> is_false(False)
01266 False
01267 >>> is_false(BoolVal(False))
01268 True
01269 """
01270 return is_app_of(a, Z3_OP_FALSE)
01271
01272 def is_and(a):
01273 """Return `True` if `a` is a Z3 and expression.
01274
01275 >>> p, q = Bools('p q')
01276 >>> is_and(And(p, q))
01277 True
01278 >>> is_and(Or(p, q))
01279 False
01280 """
01281 return is_app_of(a, Z3_OP_AND)
01282
01283 def is_or(a):
01284 """Return `True` if `a` is a Z3 or expression.
01285
01286 >>> p, q = Bools('p q')
01287 >>> is_or(Or(p, q))
01288 True
01289 >>> is_or(And(p, q))
01290 False
01291 """
01292 return is_app_of(a, Z3_OP_OR)
01293
01294 def is_not(a):
01295 """Return `True` if `a` is a Z3 not expression.
01296
01297 >>> p = Bool('p')
01298 >>> is_not(p)
01299 False
01300 >>> is_not(Not(p))
01301 True
01302 """
01303 return is_app_of(a, Z3_OP_NOT)
01304
01305 def is_eq(a):
01306 """Return `True` if `a` is a Z3 equality expression.
01307
01308 >>> x, y = Ints('x y')
01309 >>> is_eq(x == y)
01310 True
01311 """
01312 return is_app_of(a, Z3_OP_EQ)
01313
01314 def is_distinct(a):
01315 """Return `True` if `a` is a Z3 distinct expression.
01316
01317 >>> x, y, z = Ints('x y z')
01318 >>> is_distinct(x == y)
01319 False
01320 >>> is_distinct(Distinct(x, y, z))
01321 True
01322 """
01323 return is_app_of(a, Z3_OP_DISTINCT)
01324
01325 def BoolSort(ctx=None):
01326 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
01327
01328 >>> BoolSort()
01329 Bool
01330 >>> p = Const('p', BoolSort())
01331 >>> is_bool(p)
01332 True
01333 >>> r = Function('r', IntSort(), IntSort(), BoolSort())
01334 >>> r(0, 1)
01335 r(0, 1)
01336 >>> is_bool(r(0, 1))
01337 True
01338 """
01339 ctx = _get_ctx(ctx)
01340 return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
01341
01342 def BoolVal(val, ctx=None):
01343 """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
01344
01345 >>> BoolVal(True)
01346 True
01347 >>> is_true(BoolVal(True))
01348 True
01349 >>> is_true(True)
01350 False
01351 >>> is_false(BoolVal(False))
01352 True
01353 """
01354 ctx = _get_ctx(ctx)
01355 if val == False:
01356 return BoolRef(Z3_mk_false(ctx.ref()), ctx)
01357 else:
01358 return BoolRef(Z3_mk_true(ctx.ref()), ctx)
01359
01360 def Bool(name, ctx=None):
01361 """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
01362
01363 >>> p = Bool('p')
01364 >>> q = Bool('q')
01365 >>> And(p, q)
01366 And(p, q)
01367 """
01368 ctx = _get_ctx(ctx)
01369 return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
01370
01371 def Bools(names, ctx=None):
01372 """Return a tuple of Boolean constants.
01373
01374 `names` is a single string containing all names separated by blank spaces.
01375 If `ctx=None`, then the global context is used.
01376
01377 >>> p, q, r = Bools('p q r')
01378 >>> And(p, Or(q, r))
01379 And(p, Or(q, r))
01380 """
01381 ctx = _get_ctx(ctx)
01382 if isinstance(names, str):
01383 names = names.split(" ")
01384 return [Bool(name, ctx) for name in names]
01385
01386 def BoolVector(prefix, sz, ctx=None):
01387 """Return a list of Boolean constants of size `sz`.
01388
01389 The constants are named using the given prefix.
01390 If `ctx=None`, then the global context is used.
01391
01392 >>> P = BoolVector('p', 3)
01393 >>> P
01394 [p__0, p__1, p__2]
01395 >>> And(P)
01396 And(p__0, p__1, p__2)
01397 """
01398 return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
01399
01400 def FreshBool(prefix='b', ctx=None):
01401 """Return a fresh Boolean constant in the given context using the given prefix.
01402
01403 If `ctx=None`, then the global context is used.
01404
01405 >>> b1 = FreshBool()
01406 >>> b2 = FreshBool()
01407 >>> eq(b1, b2)
01408 False
01409 """
01410 ctx = _get_ctx(ctx)
01411 return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
01412
01413 def Implies(a, b, ctx=None):
01414 """Create a Z3 implies expression.
01415
01416 >>> p, q = Bools('p q')
01417 >>> Implies(p, q)
01418 Implies(p, q)
01419 >>> simplify(Implies(p, q))
01420 Or(Not(p), q)
01421 """
01422 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
01423 s = BoolSort(ctx)
01424 a = s.cast(a)
01425 b = s.cast(b)
01426 return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
01427
01428 def Xor(a, b, ctx=None):
01429 """Create a Z3 Xor expression.
01430
01431 >>> p, q = Bools('p q')
01432 >>> Xor(p, q)
01433 Xor(p, q)
01434 >>> simplify(Xor(p, q))
01435 Not(p) == q
01436 """
01437 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
01438 s = BoolSort(ctx)
01439 a = s.cast(a)
01440 b = s.cast(b)
01441 return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
01442
01443 def Not(a, ctx=None):
01444 """Create a Z3 not expression or probe.
01445
01446 >>> p = Bool('p')
01447 >>> Not(Not(p))
01448 Not(Not(p))
01449 >>> simplify(Not(Not(p)))
01450 p
01451 """
01452 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
01453 if is_probe(a):
01454 # Not is also used to build probes
01455 return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
01456 else:
01457 s = BoolSort(ctx)
01458 a = s.cast(a)
01459 return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
01460
01461 def _has_probe(args):
01462 """Return `True` if one of the elements of the given collection is a Z3 probe."""
01463 for arg in args:
01464 if is_probe(arg):
01465 return True
01466 return False
01467
01468 def And(*args):
01469 """Create a Z3 and-expression or and-probe.
01470
01471 >>> p, q, r = Bools('p q r')
01472 >>> And(p, q, r)
01473 And(p, q, r)
01474 >>> P = BoolVector('p', 5)
01475 >>> And(P)
01476 And(p__0, p__1, p__2, p__3, p__4)
01477 """
01478 last_arg = None
01479 if len(args) > 0:
01480 last_arg = args[len(args)-1]
01481 if isinstance(last_arg, Context):
01482 ctx = args[len(args)-1]
01483 args = args[:len(args)-1]
01484 else:
01485 ctx = main_ctx()
01486 args = _get_args(args)
01487 ctx_args = _ctx_from_ast_arg_list(args, ctx)
01488 if __debug__:
01489 _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
01490 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
01491 if _has_probe(args):
01492 return _probe_and(args, ctx)
01493 else:
01494 args = _coerce_expr_list(args, ctx)
01495 _args, sz = _to_ast_array(args)
01496 return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
01497
01498 def Or(*args):
01499 """Create a Z3 or-expression or or-probe.
01500
01501 >>> p, q, r = Bools('p q r')
01502 >>> Or(p, q, r)
01503 Or(p, q, r)
01504 >>> P = BoolVector('p', 5)
01505 >>> Or(P)
01506 Or(p__0, p__1, p__2, p__3, p__4)
01507 """
01508 last_arg = None
01509 if len(args) > 0:
01510 last_arg = args[len(args)-1]
01511 if isinstance(last_arg, Context):
01512 ctx = args[len(args)-1]
01513 args = args[:len(args)-1]
01514 else:
01515 ctx = main_ctx()
01516 args = _get_args(args)
01517 ctx_args = _ctx_from_ast_arg_list(args, ctx)
01518 if __debug__:
01519 _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
01520 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
01521 if _has_probe(args):
01522 return _probe_or(args, ctx)
01523 else:
01524 args = _coerce_expr_list(args, ctx)
01525 _args, sz = _to_ast_array(args)
01526 return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
01527
01528 #########################################
01529 #
01530 # Patterns
01531 #
01532 #########################################
01533
01534 class PatternRef(ExprRef):
01535 """Patterns are hints for quantifier instantiation.
01536
01537 See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01538 """
01539 def as_ast(self):
01540 return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
01541
01542 def get_id(self):
01543 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
01544
01545 def is_pattern(a):
01546 """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
01547
01548 See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01549
01550 >>> f = Function('f', IntSort(), IntSort())
01551 >>> x = Int('x')
01552 >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
01553 >>> q
01554 ForAll(x, f(x) == 0)
01555 >>> q.num_patterns()
01556 1
01557 >>> is_pattern(q.pattern(0))
01558 True
01559 >>> q.pattern(0)
01560 f(Var(0))
01561 """
01562 return isinstance(a, PatternRef)
01563
01564 def MultiPattern(*args):
01565 """Create a Z3 multi-pattern using the given expressions `*args`
01566
01567 See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01568
01569 >>> f = Function('f', IntSort(), IntSort())
01570 >>> g = Function('g', IntSort(), IntSort())
01571 >>> x = Int('x')
01572 >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
01573 >>> q
01574 ForAll(x, f(x) != g(x))
01575 >>> q.num_patterns()
01576 1
01577 >>> is_pattern(q.pattern(0))
01578 True
01579 >>> q.pattern(0)
01580 MultiPattern(f(Var(0)), g(Var(0)))
01581 """
01582 if __debug__:
01583 _z3_assert(len(args) > 0, "At least one argument expected")
01584 _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected")
01585 ctx = args[0].ctx
01586 args, sz = _to_ast_array(args)
01587 return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
01588
01589 def _to_pattern(arg):
01590 if is_pattern(arg):
01591 return arg
01592 else:
01593 return MultiPattern(arg)
01594
01595 #########################################
01596 #
01597 # Quantifiers
01598 #
01599 #########################################
01600
01601 class QuantifierRef(BoolRef):
01602 """Universally and Existentially quantified formulas."""
01603
01604 def as_ast(self):
01605 return self.ast
01606
01607 def get_id(self):
01608 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
01609
01610 def sort(self):
01611 """Return the Boolean sort."""
01612 return BoolSort(self.ctx)
01613
01614 def is_forall(self):
01615 """Return `True` if `self` is a universal quantifier.
01616
01617 >>> f = Function('f', IntSort(), IntSort())
01618 >>> x = Int('x')
01619 >>> q = ForAll(x, f(x) == 0)
01620 >>> q.is_forall()
01621 True
01622 >>> q = Exists(x, f(x) != 0)
01623 >>> q.is_forall()
01624 False
01625 """
01626 return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
01627
01628 def weight(self):
01629 """Return the weight annotation of `self`.
01630
01631 >>> f = Function('f', IntSort(), IntSort())
01632 >>> x = Int('x')
01633 >>> q = ForAll(x, f(x) == 0)
01634 >>> q.weight()
01635 1
01636 >>> q = ForAll(x, f(x) == 0, weight=10)
01637 >>> q.weight()
01638 10
01639 """
01640 return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
01641
01642 def num_patterns(self):
01643 """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
01644
01645 >>> f = Function('f', IntSort(), IntSort())
01646 >>> g = Function('g', IntSort(), IntSort())
01647 >>> x = Int('x')
01648 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
01649 >>> q.num_patterns()
01650 2
01651 """
01652 return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
01653
01654 def pattern(self, idx):
01655 """Return a pattern (i.e., quantifier instantiation hints) in `self`.
01656
01657 >>> f = Function('f', IntSort(), IntSort())
01658 >>> g = Function('g', IntSort(), IntSort())
01659 >>> x = Int('x')
01660 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
01661 >>> q.num_patterns()
01662 2
01663 >>> q.pattern(0)
01664 f(Var(0))
01665 >>> q.pattern(1)
01666 g(Var(0))
01667 """
01668 if __debug__:
01669 _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
01670 return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
01671
01672 def num_no_patterns(self):
01673 """Return the number of no-patterns."""
01674 return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
01675
01676 def no_pattern(self, idx):
01677 """Return a no-pattern."""
01678 if __debug__:
01679 _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
01680 return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
01681
01682 def body(self):
01683 """Return the expression being quantified.
01684
01685 >>> f = Function('f', IntSort(), IntSort())
01686 >>> x = Int('x')
01687 >>> q = ForAll(x, f(x) == 0)
01688 >>> q.body()
01689 f(Var(0)) == 0
01690 """
01691 return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
01692
01693 def num_vars(self):
01694 """Return the number of variables bounded by this quantifier.
01695
01696 >>> f = Function('f', IntSort(), IntSort(), IntSort())
01697 >>> x = Int('x')
01698 >>> y = Int('y')
01699 >>> q = ForAll([x, y], f(x, y) >= x)
01700 >>> q.num_vars()
01701 2
01702 """
01703 return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
01704
01705 def var_name(self, idx):
01706 """Return a string representing a name used when displaying the quantifier.
01707
01708 >>> f = Function('f', IntSort(), IntSort(), IntSort())
01709 >>> x = Int('x')
01710 >>> y = Int('y')
01711 >>> q = ForAll([x, y], f(x, y) >= x)
01712 >>> q.var_name(0)
01713 'x'
01714 >>> q.var_name(1)
01715 'y'
01716 """
01717 if __debug__:
01718 _z3_assert(idx < self.num_vars(), "Invalid variable idx")
01719 return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
01720
01721 def var_sort(self, idx):
01722 """Return the sort of a bound variable.
01723
01724 >>> f = Function('f', IntSort(), RealSort(), IntSort())
01725 >>> x = Int('x')
01726 >>> y = Real('y')
01727 >>> q = ForAll([x, y], f(x, y) >= x)
01728 >>> q.var_sort(0)
01729 Int
01730 >>> q.var_sort(1)
01731 Real
01732 """
01733 if __debug__:
01734 _z3_assert(idx < self.num_vars(), "Invalid variable idx")
01735 return SortRef(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
01736
01737 def children(self):
01738 """Return a list containing a single element self.body()
01739
01740 >>> f = Function('f', IntSort(), IntSort())
01741 >>> x = Int('x')
01742 >>> q = ForAll(x, f(x) == 0)
01743 >>> q.children()
01744 [f(Var(0)) == 0]
01745 """
01746 return [ self.body() ]
01747
01748 def is_quantifier(a):
01749 """Return `True` if `a` is a Z3 quantifier.
01750
01751 >>> f = Function('f', IntSort(), IntSort())
01752 >>> x = Int('x')
01753 >>> q = ForAll(x, f(x) == 0)
01754 >>> is_quantifier(q)
01755 True
01756 >>> is_quantifier(f(x))
01757 False
01758 """
01759 return isinstance(a, QuantifierRef)
01760
01761 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
01762 if __debug__:
01763 _z3_assert(is_bool(body), "Z3 expression expected")
01764 _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)")
01765 _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected")
01766 _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions")
01767 ctx = body.ctx
01768 if is_app(vs):
01769 vs = [vs]
01770 num_vars = len(vs)
01771 _vs = (Ast * num_vars)()
01772 for i in range(num_vars):
01773 ## TODO: Check if is constant
01774 _vs[i] = vs[i].as_ast()
01775 patterns = [ _to_pattern(p) for p in patterns ]
01776 num_pats = len(patterns)
01777 _pats = (Pattern * num_pats)()
01778 for i in range(num_pats):
01779 _pats[i] = patterns[i].ast
01780 _no_pats, num_no_pats = _to_ast_array(no_patterns)
01781 qid = to_symbol(qid, ctx)
01782 skid = to_symbol(skid, ctx)
01783 return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid,
01784 num_vars, _vs,
01785 num_pats, _pats,
01786 num_no_pats, _no_pats,
01787 body.as_ast()), ctx)
01788
01789 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
01790 """Create a Z3 forall formula.
01791
01792 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
01793
01794 See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01795
01796 >>> f = Function('f', IntSort(), IntSort(), IntSort())
01797 >>> x = Int('x')
01798 >>> y = Int('y')
01799 >>> ForAll([x, y], f(x, y) >= x)
01800 ForAll([x, y], f(x, y) >= x)
01801 >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
01802 ForAll([x, y], f(x, y) >= x)
01803 >>> ForAll([x, y], f(x, y) >= x, weight=10)
01804 ForAll([x, y], f(x, y) >= x)
01805 """
01806 return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
01807
01808 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
01809 """Create a Z3 exists formula.
01810
01811 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
01812
01813 See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
01814
01815 >>> f = Function('f', IntSort(), IntSort(), IntSort())
01816 >>> x = Int('x')
01817 >>> y = Int('y')
01818 >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
01819 >>> q
01820 Exists([x, y], f(x, y) >= x)
01821 >>> is_quantifier(q)
01822 True
01823 >>> r = Tactic('nnf')(q).as_expr()
01824 >>> is_quantifier(r)
01825 False
01826 """
01827 return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
01828
01829 #########################################
01830 #
01831 # Arithmetic
01832 #
01833 #########################################
01834
01835 class ArithSortRef(SortRef):
01836 """Real and Integer sorts."""
01837
01838 def is_real(self):
01839 """Return `True` if `self` is of the sort Real.
01840
01841 >>> x = Real('x')
01842 >>> x.is_real()
01843 True
01844 >>> (x + 1).is_real()
01845 True
01846 >>> x = Int('x')
01847 >>> x.is_real()
01848 False
01849 """
01850 return self.kind() == Z3_REAL_SORT
01851
01852 def is_int(self):
01853 """Return `True` if `self` is of the sort Integer.
01854
01855 >>> x = Int('x')
01856 >>> x.is_int()
01857 True
01858 >>> (x + 1).is_int()
01859 True
01860 >>> x = Real('x')
01861 >>> x.is_int()
01862 False
01863 """
01864 return self.kind() == Z3_INT_SORT
01865
01866 def subsort(self, other):
01867 """Return `True` if `self` is a subsort of `other`."""
01868 return self.is_int() and is_arith_sort(other) and other.is_real()
01869
01870 def cast(self, val):
01871 """Try to cast `val` as an Integer or Real.
01872
01873 >>> IntSort().cast(10)
01874 10
01875 >>> is_int(IntSort().cast(10))
01876 True
01877 >>> is_int(10)
01878 False
01879 >>> RealSort().cast(10)
01880 10
01881 >>> is_real(RealSort().cast(10))
01882 True
01883 """
01884 if is_expr(val):
01885 if __debug__:
01886 _z3_assert(self.ctx == val.ctx, "Context mismatch")
01887 val_s = val.sort()
01888 if self.eq(val_s):
01889 return val
01890 if val_s.is_int() and self.is_real():
01891 return ToReal(val)
01892 if __debug__:
01893 _z3_assert(False, "Z3 Integer/Real expression expected" )
01894 else:
01895 if self.is_int():
01896 return IntVal(val, self.ctx)
01897 if self.is_real():
01898 return RealVal(val, self.ctx)
01899 if __debug__:
01900 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
01901
01902 def is_arith_sort(s):
01903 """Return `True` if s is an arithmetical sort (type).
01904
01905 >>> is_arith_sort(IntSort())
01906 True
01907 >>> is_arith_sort(RealSort())
01908 True
01909 >>> is_arith_sort(BoolSort())
01910 False
01911 >>> n = Int('x') + 1
01912 >>> is_arith_sort(n.sort())
01913 True
01914 """
01915 return isinstance(s, ArithSortRef)
01916
01917 class ArithRef(ExprRef):
01918 """Integer and Real expressions."""
01919
01920 def sort(self):
01921 """Return the sort (type) of the arithmetical expression `self`.
01922
01923 >>> Int('x').sort()
01924 Int
01925 >>> (Real('x') + 1).sort()
01926 Real
01927 """
01928 return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
01929
01930 def is_int(self):
01931 """Return `True` if `self` is an integer expression.
01932
01933 >>> x = Int('x')
01934 >>> x.is_int()
01935 True
01936 >>> (x + 1).is_int()
01937 True
01938 >>> y = Real('y')
01939 >>> (x + y).is_int()
01940 False
01941 """
01942 return self.sort().is_int()
01943
01944 def is_real(self):
01945 """Return `True` if `self` is an real expression.
01946
01947 >>> x = Real('x')
01948 >>> x.is_real()
01949 True
01950 >>> (x + 1).is_real()
01951 True
01952 """
01953 return self.sort().is_real()
01954
01955 def __add__(self, other):
01956 """Create the Z3 expression `self + other`.
01957
01958 >>> x = Int('x')
01959 >>> y = Int('y')
01960 >>> x + y
01961 x + y
01962 >>> (x + y).sort()
01963 Int
01964 """
01965 a, b = _coerce_exprs(self, other)
01966 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
01967
01968 def __radd__(self, other):
01969 """Create the Z3 expression `other + self`.
01970
01971 >>> x = Int('x')
01972 >>> 10 + x
01973 10 + x
01974 """
01975 a, b = _coerce_exprs(self, other)
01976 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
01977
01978 def __mul__(self, other):
01979 """Create the Z3 expression `self * other`.
01980
01981 >>> x = Real('x')
01982 >>> y = Real('y')
01983 >>> x * y
01984 x*y
01985 >>> (x * y).sort()
01986 Real
01987 """
01988 a, b = _coerce_exprs(self, other)
01989 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
01990
01991 def __rmul__(self, other):
01992 """Create the Z3 expression `other * self`.
01993
01994 >>> x = Real('x')
01995 >>> 10 * x
01996 10*x
01997 """
01998 a, b = _coerce_exprs(self, other)
01999 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
02000
02001 def __sub__(self, other):
02002 """Create the Z3 expression `self - other`.
02003
02004 >>> x = Int('x')
02005 >>> y = Int('y')
02006 >>> x - y
02007 x - y
02008 >>> (x - y).sort()
02009 Int
02010 """
02011 a, b = _coerce_exprs(self, other)
02012 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
02013
02014 def __rsub__(self, other):
02015 """Create the Z3 expression `other - self`.
02016
02017 >>> x = Int('x')
02018 >>> 10 - x
02019 10 - x
02020 """
02021 a, b = _coerce_exprs(self, other)
02022 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
02023
02024 def __pow__(self, other):
02025 """Create the Z3 expression `self**other` (** is the power operator).
02026
02027 >>> x = Real('x')
02028 >>> x**3
02029 x**3
02030 >>> (x**3).sort()
02031 Real
02032 >>> simplify(IntVal(2)**8)
02033 256
02034 """
02035 a, b = _coerce_exprs(self, other)
02036 return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02037
02038 def __rpow__(self, other):
02039 """Create the Z3 expression `other**self` (** is the power operator).
02040
02041 >>> x = Real('x')
02042 >>> 2**x
02043 2**x
02044 >>> (2**x).sort()
02045 Real
02046 >>> simplify(2**IntVal(8))
02047 256
02048 """
02049 a, b = _coerce_exprs(self, other)
02050 return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
02051
02052 def __div__(self, other):
02053 """Create the Z3 expression `other/self`.
02054
02055 >>> x = Int('x')
02056 >>> y = Int('y')
02057 >>> x/y
02058 x/y
02059 >>> (x/y).sort()
02060 Int
02061 >>> (x/y).sexpr()
02062 '(div x y)'
02063 >>> x = Real('x')
02064 >>> y = Real('y')
02065 >>> x/y
02066 x/y
02067 >>> (x/y).sort()
02068 Real
02069 >>> (x/y).sexpr()
02070 '(/ x y)'
02071 """
02072 a, b = _coerce_exprs(self, other)
02073 return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02074
02075 def __truediv__(self, other):
02076 """Create the Z3 expression `other/self`."""
02077 return self.__div__(other)
02078
02079 def __rdiv__(self, other):
02080 """Create the Z3 expression `other/self`.
02081
02082 >>> x = Int('x')
02083 >>> 10/x
02084 10/x
02085 >>> (10/x).sexpr()
02086 '(div 10 x)'
02087 >>> x = Real('x')
02088 >>> 10/x
02089 10/x
02090 >>> (10/x).sexpr()
02091 '(/ 10.0 x)'
02092 """
02093 a, b = _coerce_exprs(self, other)
02094 return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
02095
02096 def __rtruediv__(self, other):
02097 """Create the Z3 expression `other/self`."""
02098 return self.__rdiv__(other)
02099
02100 def __mod__(self, other):
02101 """Create the Z3 expression `other%self`.
02102
02103 >>> x = Int('x')
02104 >>> y = Int('y')
02105 >>> x % y
02106 x%y
02107 >>> simplify(IntVal(10) % IntVal(3))
02108 1
02109 """
02110 a, b = _coerce_exprs(self, other)
02111 if __debug__:
02112 _z3_assert(a.is_int(), "Z3 integer expression expected")
02113 return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02114
02115 def __rmod__(self, other):
02116 """Create the Z3 expression `other%self`.
02117
02118 >>> x = Int('x')
02119 >>> 10 % x
02120 10%x
02121 """
02122 a, b = _coerce_exprs(self, other)
02123 if __debug__:
02124 _z3_assert(a.is_int(), "Z3 integer expression expected")
02125 return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
02126
02127 def __neg__(self):
02128 """Return an expression representing `-self`.
02129
02130 >>> x = Int('x')
02131 >>> -x
02132 -x
02133 >>> simplify(-(-x))
02134 x
02135 """
02136 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
02137
02138 def __pos__(self):
02139 """Return `self`.
02140
02141 >>> x = Int('x')
02142 >>> +x
02143 x
02144 """
02145 return self
02146
02147 def __le__(self, other):
02148 """Create the Z3 expression `other <= self`.
02149
02150 >>> x, y = Ints('x y')
02151 >>> x <= y
02152 x <= y
02153 >>> y = Real('y')
02154 >>> x <= y
02155 ToReal(x) <= y
02156 """
02157 a, b = _coerce_exprs(self, other)
02158 return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02159
02160 def __lt__(self, other):
02161 """Create the Z3 expression `other < self`.
02162
02163 >>> x, y = Ints('x y')
02164 >>> x < y
02165 x < y
02166 >>> y = Real('y')
02167 >>> x < y
02168 ToReal(x) < y
02169 """
02170 a, b = _coerce_exprs(self, other)
02171 return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02172
02173 def __gt__(self, other):
02174 """Create the Z3 expression `other > self`.
02175
02176 >>> x, y = Ints('x y')
02177 >>> x > y
02178 x > y
02179 >>> y = Real('y')
02180 >>> x > y
02181 ToReal(x) > y
02182 """
02183 a, b = _coerce_exprs(self, other)
02184 return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02185
02186 def __ge__(self, other):
02187 """Create the Z3 expression `other >= self`.
02188
02189 >>> x, y = Ints('x y')
02190 >>> x >= y
02191 x >= y
02192 >>> y = Real('y')
02193 >>> x >= y
02194 ToReal(x) >= y
02195 """
02196 a, b = _coerce_exprs(self, other)
02197 return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02198
02199 def is_arith(a):
02200 """Return `True` if `a` is an arithmetical expression.
02201
02202 >>> x = Int('x')
02203 >>> is_arith(x)
02204 True
02205 >>> is_arith(x + 1)
02206 True
02207 >>> is_arith(1)
02208 False
02209 >>> is_arith(IntVal(1))
02210 True
02211 >>> y = Real('y')
02212 >>> is_arith(y)
02213 True
02214 >>> is_arith(y + 1)
02215 True
02216 """
02217 return isinstance(a, ArithRef)
02218
02219 def is_int(a):
02220 """Return `True` if `a` is an integer expression.
02221
02222 >>> x = Int('x')
02223 >>> is_int(x + 1)
02224 True
02225 >>> is_int(1)
02226 False
02227 >>> is_int(IntVal(1))
02228 True
02229 >>> y = Real('y')
02230 >>> is_int(y)
02231 False
02232 >>> is_int(y + 1)
02233 False
02234 """
02235 return is_arith(a) and a.is_int()
02236
02237 def is_real(a):
02238 """Return `True` if `a` is a real expression.
02239
02240 >>> x = Int('x')
02241 >>> is_real(x + 1)
02242 False
02243 >>> y = Real('y')
02244 >>> is_real(y)
02245 True
02246 >>> is_real(y + 1)
02247 True
02248 >>> is_real(1)
02249 False
02250 >>> is_real(RealVal(1))
02251 True
02252 """
02253 return is_arith(a) and a.is_real()
02254
02255 def _is_numeral(ctx, a):
02256 return Z3_is_numeral_ast(ctx.ref(), a)
02257
02258 def _is_algebraic(ctx, a):
02259 return Z3_is_algebraic_number(ctx.ref(), a)
02260
02261 def is_int_value(a):
02262 """Return `True` if `a` is an integer value of sort Int.
02263
02264 >>> is_int_value(IntVal(1))
02265 True
02266 >>> is_int_value(1)
02267 False
02268 >>> is_int_value(Int('x'))
02269 False
02270 >>> n = Int('x') + 1
02271 >>> n
02272 x + 1
02273 >>> n.arg(1)
02274 1
02275 >>> is_int_value(n.arg(1))
02276 True
02277 >>> is_int_value(RealVal("1/3"))
02278 False
02279 >>> is_int_value(RealVal(1))
02280 False
02281 """
02282 return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
02283
02284 def is_rational_value(a):
02285 """Return `True` if `a` is rational value of sort Real.
02286
02287 >>> is_rational_value(RealVal(1))
02288 True
02289 >>> is_rational_value(RealVal("3/5"))
02290 True
02291 >>> is_rational_value(IntVal(1))
02292 False
02293 >>> is_rational_value(1)
02294 False
02295 >>> n = Real('x') + 1
02296 >>> n.arg(1)
02297 1
02298 >>> is_rational_value(n.arg(1))
02299 True
02300 >>> is_rational_value(Real('x'))
02301 False
02302 """
02303 return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
02304
02305 def is_algebraic_value(a):
02306 """Return `True` if `a` is an algerbraic value of sort Real.
02307
02308 >>> is_algebraic_value(RealVal("3/5"))
02309 False
02310 >>> n = simplify(Sqrt(2))
02311 >>> n
02312 1.4142135623?
02313 >>> is_algebraic_value(n)
02314 True
02315 """
02316 return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
02317
02318 def is_add(a):
02319 """Return `True` if `a` is an expression of the form b + c.
02320
02321 >>> x, y = Ints('x y')
02322 >>> is_add(x + y)
02323 True
02324 >>> is_add(x - y)
02325 False
02326 """
02327 return is_app_of(a, Z3_OP_ADD)
02328
02329 def is_mul(a):
02330 """Return `True` if `a` is an expression of the form b * c.
02331
02332 >>> x, y = Ints('x y')
02333 >>> is_mul(x * y)
02334 True
02335 >>> is_mul(x - y)
02336 False
02337 """
02338 return is_app_of(a, Z3_OP_MUL)
02339
02340 def is_sub(a):
02341 """Return `True` if `a` is an expression of the form b - c.
02342
02343 >>> x, y = Ints('x y')
02344 >>> is_sub(x - y)
02345 True
02346 >>> is_sub(x + y)
02347 False
02348 """
02349 return is_app_of(a, Z3_OP_SUB)
02350
02351 def is_div(a):
02352 """Return `True` if `a` is an expression of the form b / c.
02353
02354 >>> x, y = Reals('x y')
02355 >>> is_div(x / y)
02356 True
02357 >>> is_div(x + y)
02358 False
02359 >>> x, y = Ints('x y')
02360 >>> is_div(x / y)
02361 False
02362 >>> is_idiv(x / y)
02363 True
02364 """
02365 return is_app_of(a, Z3_OP_DIV)
02366
02367 def is_idiv(a):
02368 """Return `True` if `a` is an expression of the form b div c.
02369
02370 >>> x, y = Ints('x y')
02371 >>> is_idiv(x / y)
02372 True
02373 >>> is_idiv(x + y)
02374 False
02375 """
02376 return is_app_of(a, Z3_OP_IDIV)
02377
02378 def is_mod(a):
02379 """Return `True` if `a` is an expression of the form b % c.
02380
02381 >>> x, y = Ints('x y')
02382 >>> is_mod(x % y)
02383 True
02384 >>> is_mod(x + y)
02385 False
02386 """
02387 return is_app_of(a, Z3_OP_MOD)
02388
02389 def is_le(a):
02390 """Return `True` if `a` is an expression of the form b <= c.
02391
02392 >>> x, y = Ints('x y')
02393 >>> is_le(x <= y)
02394 True
02395 >>> is_le(x < y)
02396 False
02397 """
02398 return is_app_of(a, Z3_OP_LE)
02399
02400 def is_lt(a):
02401 """Return `True` if `a` is an expression of the form b < c.
02402
02403 >>> x, y = Ints('x y')
02404 >>> is_lt(x < y)
02405 True
02406 >>> is_lt(x == y)
02407 False
02408 """
02409 return is_app_of(a, Z3_OP_LT)
02410
02411 def is_ge(a):
02412 """Return `True` if `a` is an expression of the form b >= c.
02413
02414 >>> x, y = Ints('x y')
02415 >>> is_ge(x >= y)
02416 True
02417 >>> is_ge(x == y)
02418 False
02419 """
02420 return is_app_of(a, Z3_OP_GE)
02421
02422 def is_gt(a):
02423 """Return `True` if `a` is an expression of the form b > c.
02424
02425 >>> x, y = Ints('x y')
02426 >>> is_gt(x > y)
02427 True
02428 >>> is_gt(x == y)
02429 False
02430 """
02431 return is_app_of(a, Z3_OP_GT)
02432
02433 def is_is_int(a):
02434 """Return `True` if `a` is an expression of the form IsInt(b).
02435
02436 >>> x = Real('x')
02437 >>> is_is_int(IsInt(x))
02438 True
02439 >>> is_is_int(x)
02440 False
02441 """
02442 return is_app_of(a, Z3_OP_IS_INT)
02443
02444 def is_to_real(a):
02445 """Return `True` if `a` is an expression of the form ToReal(b).
02446
02447 >>> x = Int('x')
02448 >>> n = ToReal(x)
02449 >>> n
02450 ToReal(x)
02451 >>> is_to_real(n)
02452 True
02453 >>> is_to_real(x)
02454 False
02455 """
02456 return is_app_of(a, Z3_OP_TO_REAL)
02457
02458 def is_to_int(a):
02459 """Return `True` if `a` is an expression of the form ToInt(b).
02460
02461 >>> x = Real('x')
02462 >>> n = ToInt(x)
02463 >>> n
02464 ToInt(x)
02465 >>> is_to_int(n)
02466 True
02467 >>> is_to_int(x)
02468 False
02469 """
02470 return is_app_of(a, Z3_OP_TO_INT)
02471
02472 class IntNumRef(ArithRef):
02473 """Integer values."""
02474
02475 def as_long(self):
02476 """Return a Z3 integer numeral as a Python long (bignum) numeral.
02477
02478 >>> v = IntVal(1)
02479 >>> v + 1
02480 1 + 1
02481 >>> v.as_long() + 1
02482 2
02483 """
02484 if __debug__:
02485 _z3_assert(self.is_int(), "Integer value expected")
02486 return int(self.as_string())
02487
02488 def as_string(self):
02489 """Return a Z3 integer numeral as a Python string.
02490 >>> v = IntVal(100)
02491 >>> v.as_string()
02492 '100'
02493 """
02494 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
02495
02496 class RatNumRef(ArithRef):
02497 """Rational values."""
02498
02499 def numerator(self):
02500 """ Return the numerator of a Z3 rational numeral.
02501
02502 >>> is_rational_value(RealVal("3/5"))
02503 True
02504 >>> n = RealVal("3/5")
02505 >>> n.numerator()
02506 3
02507 >>> is_rational_value(Q(3,5))
02508 True
02509 >>> Q(3,5).numerator()
02510 3
02511 """
02512 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
02513
02514 def denominator(self):
02515 """ Return the denominator of a Z3 rational numeral.
02516
02517 >>> is_rational_value(Q(3,5))
02518 True
02519 >>> n = Q(3,5)
02520 >>> n.denominator()
02521 5
02522 """
02523 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
02524
02525 def numerator_as_long(self):
02526 """ Return the numerator as a Python long.
02527
02528 >>> v = RealVal(10000000000)
02529 >>> v
02530 10000000000
02531 >>> v + 1
02532 10000000000 + 1
02533 >>> v.numerator_as_long() + 1 == 10000000001
02534 True
02535 """
02536 return self.numerator().as_long()
02537
02538 def denominator_as_long(self):
02539 """ Return the denominator as a Python long.
02540
02541 >>> v = RealVal("1/3")
02542 >>> v
02543 1/3
02544 >>> v.denominator_as_long()
02545 3
02546 """
02547 return self.denominator().as_long()
02548
02549 def as_decimal(self, prec):
02550 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
02551
02552 >>> v = RealVal("1/5")
02553 >>> v.as_decimal(3)
02554 '0.2'
02555 >>> v = RealVal("1/3")
02556 >>> v.as_decimal(3)
02557 '0.333?'
02558 """
02559 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
02560
02561 def as_string(self):
02562 """Return a Z3 rational numeral as a Python string.
02563
02564 >>> v = Q(3,6)
02565 >>> v.as_string()
02566 '1/2'
02567 """
02568 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
02569
02570 def as_fraction(self):
02571 """Return a Z3 rational as a Python Fraction object.
02572
02573 >>> v = RealVal("1/5")
02574 >>> v.as_fraction()
02575 Fraction(1, 5)
02576 """
02577 return Fraction(self.numerator_as_long(), self.denominator_as_long())
02578
02579 class AlgebraicNumRef(ArithRef):
02580 """Algebraic irrational values."""
02581
02582 def approx(self, precision=10):
02583 """Return a Z3 rational number that approximates the algebraic number `self`.
02584 The result `r` is such that |r - self| <= 1/10^precision
02585
02586 >>> x = simplify(Sqrt(2))
02587 >>> x.approx(20)
02588 6838717160008073720548335/4835703278458516698824704
02589 >>> x.approx(5)
02590 2965821/2097152
02591 """
02592 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
02593 def as_decimal(self, prec):
02594 """Return a string representation of the algebraic number `self` in decimal notation using `prec` decimal places
02595
02596 >>> x = simplify(Sqrt(2))
02597 >>> x.as_decimal(10)
02598 '1.4142135623?'
02599 >>> x.as_decimal(20)
02600 '1.41421356237309504880?'
02601 """
02602 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
02603
02604 def _py2expr(a, ctx=None):
02605 if isinstance(a, bool):
02606 return BoolVal(a, ctx)
02607 if _is_int(a):
02608 return IntVal(a, ctx)
02609 if isinstance(a, float):
02610 return RealVal(a, ctx)
02611 if __debug__:
02612 _z3_assert(False, "Python bool, int, long or float expected")
02613
02614 def IntSort(ctx=None):
02615 """Return the interger sort in the given context. If `ctx=None`, then the global context is used.
02616
02617 >>> IntSort()
02618 Int
02619 >>> x = Const('x', IntSort())
02620 >>> is_int(x)
02621 True
02622 >>> x.sort() == IntSort()
02623 True
02624 >>> x.sort() == BoolSort()
02625 False
02626 """
02627 ctx = _get_ctx(ctx)
02628 return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
02629
02630 def RealSort(ctx=None):
02631 """Return the real sort in the given context. If `ctx=None`, then the global context is used.
02632
02633 >>> RealSort()
02634 Real
02635 >>> x = Const('x', RealSort())
02636 >>> is_real(x)
02637 True
02638 >>> is_int(x)
02639 False
02640 >>> x.sort() == RealSort()
02641 True
02642 """
02643 ctx = _get_ctx(ctx)
02644 return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)
02645
02646 def _to_int_str(val):
02647 if isinstance(val, float):
02648 return str(int(val))
02649 elif isinstance(val, bool):
02650 if val:
02651 return "1"
02652 else:
02653 return "0"
02654 elif _is_int(val):
02655 return str(val)
02656 elif isinstance(val, str):
02657 return val
02658 if __debug__:
02659 _z3_assert(False, "Python value cannot be used as a Z3 integer")
02660
02661 def IntVal(val, ctx=None):
02662 """Return a Z3 integer value. If `ctx=None`, then the global context is used.
02663
02664 >>> IntVal(1)
02665 1
02666 >>> IntVal("100")
02667 100
02668 """
02669 ctx = _get_ctx(ctx)
02670 return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
02671
02672 def RealVal(val, ctx=None):
02673 """Return a Z3 real value.
02674
02675 `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
02676 If `ctx=None`, then the global context is used.
02677
02678 >>> RealVal(1)
02679 1
02680 >>> RealVal(1).sort()
02681 Real
02682 >>> RealVal("3/5")
02683 3/5
02684 >>> RealVal("1.5")
02685 3/2
02686 """
02687 ctx = _get_ctx(ctx)
02688 return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
02689
02690 def RatVal(a, b, ctx=None):
02691 """Return a Z3 rational a/b.
02692
02693 If `ctx=None`, then the global context is used.
02694
02695 >>> RatVal(3,5)
02696 3/5
02697 >>> RatVal(3,5).sort()
02698 Real
02699 """
02700 if __debug__:
02701 _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
02702 _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
02703 return simplify(RealVal(a, ctx)/RealVal(b, ctx))
02704
02705 def Q(a, b, ctx=None):
02706 """Return a Z3 rational a/b.
02707
02708 If `ctx=None`, then the global context is used.
02709
02710 >>> Q(3,5)
02711 3/5
02712 >>> Q(3,5).sort()
02713 Real
02714 """
02715 return simplify(RatVal(a, b))
02716
02717 def Int(name, ctx=None):
02718 """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
02719
02720 >>> x = Int('x')
02721 >>> is_int(x)
02722 True
02723 >>> is_int(x + 1)
02724 True
02725 """
02726 ctx = _get_ctx(ctx)
02727 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
02728
02729 def Ints(names, ctx=None):
02730 """Return a tuple of Integer constants.
02731
02732 >>> x, y, z = Ints('x y z')
02733 >>> Sum(x, y, z)
02734 x + y + z
02735 """
02736 ctx = _get_ctx(ctx)
02737 if isinstance(names, str):
02738 names = names.split(" ")
02739 return [Int(name, ctx) for name in names]
02740
02741 def IntVector(prefix, sz, ctx=None):
02742 """Return a list of integer constants of size `sz`.
02743
02744 >>> X = IntVector('x', 3)
02745 >>> X
02746 [x__0, x__1, x__2]
02747 >>> Sum(X)
02748 x__0 + x__1 + x__2
02749 """
02750 return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ]
02751
02752 def FreshInt(prefix='x', ctx=None):
02753 """Return a fresh integer constant in the given context using the given prefix.
02754
02755 >>> x = FreshInt()
02756 >>> y = FreshInt()
02757 >>> eq(x, y)
02758 False
02759 >>> x.sort()
02760 Int
02761 """
02762 ctx = _get_ctx(ctx)
02763 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
02764
02765 def Real(name, ctx=None):
02766 """Return a real constant named `name`. If `ctx=None`, then the global context is used.
02767
02768 >>> x = Real('x')
02769 >>> is_real(x)
02770 True
02771 >>> is_real(x + 1)
02772 True
02773 """
02774 ctx = _get_ctx(ctx)
02775 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)
02776
02777 def Reals(names, ctx=None):
02778 """Return a tuple of real constants.
02779
02780 >>> x, y, z = Reals('x y z')
02781 >>> Sum(x, y, z)
02782 x + y + z
02783 >>> Sum(x, y, z).sort()
02784 Real
02785 """
02786 ctx = _get_ctx(ctx)
02787 if isinstance(names, str):
02788 names = names.split(" ")
02789 return [Real(name, ctx) for name in names]
02790
02791 def RealVector(prefix, sz, ctx=None):
02792 """Return a list of real constants of size `sz`.
02793
02794 >>> X = RealVector('x', 3)
02795 >>> X
02796 [x__0, x__1, x__2]
02797 >>> Sum(X)
02798 x__0 + x__1 + x__2
02799 >>> Sum(X).sort()
02800 Real
02801 """
02802 return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ]
02803
02804 def FreshReal(prefix='b', ctx=None):
02805 """Return a fresh real constant in the given context using the given prefix.
02806
02807 >>> x = FreshReal()
02808 >>> y = FreshReal()
02809 >>> eq(x, y)
02810 False
02811 >>> x.sort()
02812 Real
02813 """
02814 ctx = _get_ctx(ctx)
02815 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
02816
02817 def ToReal(a):
02818 """ Return the Z3 expression ToReal(a).
02819
02820 >>> x = Int('x')
02821 >>> x.sort()
02822 Int
02823 >>> n = ToReal(x)
02824 >>> n
02825 ToReal(x)
02826 >>> n.sort()
02827 Real
02828 """
02829 if __debug__:
02830 _z3_assert(a.is_int(), "Z3 integer expression expected.")
02831 ctx = a.ctx
02832 return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
02833
02834 def ToInt(a):
02835 """ Return the Z3 expression ToInt(a).
02836
02837 >>> x = Real('x')
02838 >>> x.sort()
02839 Real
02840 >>> n = ToInt(x)
02841 >>> n
02842 ToInt(x)
02843 >>> n.sort()
02844 Int
02845 """
02846 if __debug__:
02847 _z3_assert(a.is_real(), "Z3 real expression expected.")
02848 ctx = a.ctx
02849 return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)
02850
02851 def IsInt(a):
02852 """ Return the Z3 predicate IsInt(a).
02853
02854 >>> x = Real('x')
02855 >>> IsInt(x + "1/2")
02856 IsInt(x + 1/2)
02857 >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
02858 [x = 1/2]
02859 >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
02860 no solution
02861 """
02862 if __debug__:
02863 _z3_assert(a.is_real(), "Z3 real expression expected.")
02864 ctx = a.ctx
02865 return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
02866
02867 def Sqrt(a, ctx=None):
02868 """ Return a Z3 expression which represents the square root of a.
02869
02870 >>> x = Real('x')
02871 >>> Sqrt(x)
02872 x**(1/2)
02873 """
02874 if not is_expr(a):
02875 ctx = _get_ctx(ctx)
02876 a = RealVal(a, ctx)
02877 return a ** "1/2"
02878
02879 def Cbrt(a, ctx=None):
02880 """ Return a Z3 expression which represents the cubic root of a.
02881
02882 >>> x = Real('x')
02883 >>> Cbrt(x)
02884 x**(1/3)
02885 """
02886 if not is_expr(a):
02887 ctx = _get_ctx(ctx)
02888 a = RealVal(a, ctx)
02889 return a ** "1/3"
02890
02891 #########################################
02892 #
02893 # Bit-Vectors
02894 #
02895 #########################################
02896
02897 class BitVecSortRef(SortRef):
02898 """Bit-vector sort."""
02899
02900 def size(self):
02901 """Return the size (number of bits) of the bit-vector sort `self`.
02902
02903 >>> b = BitVecSort(32)
02904 >>> b.size()
02905 32
02906 """
02907 return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast))
02908
02909 def subsort(self, other):
02910 return is_bv_sort(other) and self.size() < other.size()
02911
02912 def cast(self, val):
02913 """Try to cast `val` as a Bit-Vector.
02914
02915 >>> b = BitVecSort(32)
02916 >>> b.cast(10)
02917 10
02918 >>> b.cast(10).sexpr()
02919 '#x0000000a'
02920 """
02921 if is_expr(val):
02922 if __debug__:
02923 _z3_assert(self.ctx == val.ctx, "Context mismatch")
02924 # Idea: use sign_extend if sort of val is a bitvector of smaller size
02925 return val
02926 else:
02927 return BitVecVal(val, self)
02928
02929 def is_bv_sort(s):
02930 """Return True if `s` is a Z3 bit-vector sort.
02931
02932 >>> is_bv_sort(BitVecSort(32))
02933 True
02934 >>> is_bv_sort(IntSort())
02935 False
02936 """
02937 return isinstance(s, BitVecSortRef)
02938
02939 class BitVecRef(ExprRef):
02940 """Bit-vector expressions."""
02941
02942 def sort(self):
02943 """Return the sort of the bit-vector expression `self`.
02944
02945 >>> x = BitVec('x', 32)
02946 >>> x.sort()
02947 BitVec(32)
02948 >>> x.sort() == BitVecSort(32)
02949 True
02950 """
02951 return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
02952
02953 def size(self):
02954 """Return the number of bits of the bit-vector expression `self`.
02955
02956 >>> x = BitVec('x', 32)
02957 >>> (x + 1).size()
02958 32
02959 >>> Concat(x, x).size()
02960 64
02961 """
02962 return self.sort().size()
02963
02964 def __add__(self, other):
02965 """Create the Z3 expression `self + other`.
02966
02967 >>> x = BitVec('x', 32)
02968 >>> y = BitVec('y', 32)
02969 >>> x + y
02970 x + y
02971 >>> (x + y).sort()
02972 BitVec(32)
02973 """
02974 a, b = _coerce_exprs(self, other)
02975 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02976
02977 def __radd__(self, other):
02978 """Create the Z3 expression `other + self`.
02979
02980 >>> x = BitVec('x', 32)
02981 >>> 10 + x
02982 10 + x
02983 """
02984 a, b = _coerce_exprs(self, other)
02985 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
02986
02987 def __mul__(self, other):
02988 """Create the Z3 expression `self * other`.
02989
02990 >>> x = BitVec('x', 32)
02991 >>> y = BitVec('y', 32)
02992 >>> x * y
02993 x*y
02994 >>> (x * y).sort()
02995 BitVec(32)
02996 """
02997 a, b = _coerce_exprs(self, other)
02998 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
02999
03000 def __rmul__(self, other):
03001 """Create the Z3 expression `other * self`.
03002
03003 >>> x = BitVec('x', 32)
03004 >>> 10 * x
03005 10*x
03006 """
03007 a, b = _coerce_exprs(self, other)
03008 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03009
03010 def __sub__(self, other):
03011 """Create the Z3 expression `self - other`.
03012
03013 >>> x = BitVec('x', 32)
03014 >>> y = BitVec('y', 32)
03015 >>> x - y
03016 x - y
03017 >>> (x - y).sort()
03018 BitVec(32)
03019 """
03020 a, b = _coerce_exprs(self, other)
03021 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03022
03023 def __rsub__(self, other):
03024 """Create the Z3 expression `other - self`.
03025
03026 >>> x = BitVec('x', 32)
03027 >>> 10 - x
03028 10 - x
03029 """
03030 a, b = _coerce_exprs(self, other)
03031 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03032
03033 def __or__(self, other):
03034 """Create the Z3 expression bitwise-or `self | other`.
03035
03036 >>> x = BitVec('x', 32)
03037 >>> y = BitVec('y', 32)
03038 >>> x | y
03039 x | y
03040 >>> (x | y).sort()
03041 BitVec(32)
03042 """
03043 a, b = _coerce_exprs(self, other)
03044 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03045
03046 def __ror__(self, other):
03047 """Create the Z3 expression bitwise-or `other | self`.
03048
03049 >>> x = BitVec('x', 32)
03050 >>> 10 | x
03051 10 | x
03052 """
03053 a, b = _coerce_exprs(self, other)
03054 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03055
03056 def __and__(self, other):
03057 """Create the Z3 expression bitwise-and `self & other`.
03058
03059 >>> x = BitVec('x', 32)
03060 >>> y = BitVec('y', 32)
03061 >>> x & y
03062 x & y
03063 >>> (x & y).sort()
03064 BitVec(32)
03065 """
03066 a, b = _coerce_exprs(self, other)
03067 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03068
03069 def __rand__(self, other):
03070 """Create the Z3 expression bitwise-or `other & self`.
03071
03072 >>> x = BitVec('x', 32)
03073 >>> 10 & x
03074 10 & x
03075 """
03076 a, b = _coerce_exprs(self, other)
03077 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03078
03079 def __xor__(self, other):
03080 """Create the Z3 expression bitwise-xor `self ^ other`.
03081
03082 >>> x = BitVec('x', 32)
03083 >>> y = BitVec('y', 32)
03084 >>> x ^ y
03085 x ^ y
03086 >>> (x ^ y).sort()
03087 BitVec(32)
03088 """
03089 a, b = _coerce_exprs(self, other)
03090 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03091
03092 def __rxor__(self, other):
03093 """Create the Z3 expression bitwise-xor `other ^ self`.
03094
03095 >>> x = BitVec('x', 32)
03096 >>> 10 ^ x
03097 10 ^ x
03098 """
03099 a, b = _coerce_exprs(self, other)
03100 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03101
03102 def __pos__(self):
03103 """Return `self`.
03104
03105 >>> x = BitVec('x', 32)
03106 >>> +x
03107 x
03108 """
03109 return self
03110
03111 def __neg__(self):
03112 """Return an expression representing `-self`.
03113
03114 >>> x = BitVec('x', 32)
03115 >>> -x
03116 -x
03117 >>> simplify(-(-x))
03118 x
03119 """
03120 return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx)
03121
03122 def __invert__(self):
03123 """Create the Z3 expression bitwise-not `~self`.
03124
03125 >>> x = BitVec('x', 32)
03126 >>> ~x
03127 ~x
03128 >>> simplify(~(~x))
03129 x
03130 """
03131 return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx)
03132
03133 def __div__(self, other):
03134 """Create the Z3 expression (signed) division `self / other`.
03135
03136 Use the function UDiv() for unsigned division.
03137
03138 >>> x = BitVec('x', 32)
03139 >>> y = BitVec('y', 32)
03140 >>> x / y
03141 x/y
03142 >>> (x / y).sort()
03143 BitVec(32)
03144 >>> (x / y).sexpr()
03145 '(bvsdiv x y)'
03146 >>> UDiv(x, y).sexpr()
03147 '(bvudiv x y)'
03148 """
03149 a, b = _coerce_exprs(self, other)
03150 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03151
03152 def __truediv__(self, other):
03153 """Create the Z3 expression (signed) division `self / other`."""
03154 return self.__div__(other)
03155
03156 def __rdiv__(self, other):
03157 """Create the Z3 expression (signed) division `other / self`.
03158
03159 Use the function UDiv() for unsigned division.
03160
03161 >>> x = BitVec('x', 32)
03162 >>> 10 / x
03163 10/x
03164 >>> (10 / x).sexpr()
03165 '(bvsdiv #x0000000a x)'
03166 >>> UDiv(10, x).sexpr()
03167 '(bvudiv #x0000000a x)'
03168 """
03169 a, b = _coerce_exprs(self, other)
03170 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03171
03172 def __rtruediv__(self, other):
03173 """Create the Z3 expression (signed) division `other / self`."""
03174 return self.__rdiv__(other)
03175
03176 def __mod__(self, other):
03177 """Create the Z3 expression (signed) mod `self % other`.
03178
03179 Use the function URem() for unsigned remainder, and SRem() for signed remainder.
03180
03181 >>> x = BitVec('x', 32)
03182 >>> y = BitVec('y', 32)
03183 >>> x % y
03184 x%y
03185 >>> (x % y).sort()
03186 BitVec(32)
03187 >>> (x % y).sexpr()
03188 '(bvsmod x y)'
03189 >>> URem(x, y).sexpr()
03190 '(bvurem x y)'
03191 >>> SRem(x, y).sexpr()
03192 '(bvsrem x y)'
03193 """
03194 a, b = _coerce_exprs(self, other)
03195 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03196
03197 def __rmod__(self, other):
03198 """Create the Z3 expression (signed) mod `other % self`.
03199
03200 Use the function URem() for unsigned remainder, and SRem() for signed remainder.
03201
03202 >>> x = BitVec('x', 32)
03203 >>> 10 % x
03204 10%x
03205 >>> (10 % x).sexpr()
03206 '(bvsmod #x0000000a x)'
03207 >>> URem(10, x).sexpr()
03208 '(bvurem #x0000000a x)'
03209 >>> SRem(10, x).sexpr()
03210 '(bvsrem #x0000000a x)'
03211 """
03212 a, b = _coerce_exprs(self, other)
03213 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03214
03215 def __le__(self, other):
03216 """Create the Z3 expression (signed) `other <= self`.
03217
03218 Use the function ULE() for unsigned less than or equal to.
03219
03220 >>> x, y = BitVecs('x y', 32)
03221 >>> x <= y
03222 x <= y
03223 >>> (x <= y).sexpr()
03224 '(bvsle x y)'
03225 >>> ULE(x, y).sexpr()
03226 '(bvule x y)'
03227 """
03228 a, b = _coerce_exprs(self, other)
03229 return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03230
03231 def __lt__(self, other):
03232 """Create the Z3 expression (signed) `other < self`.
03233
03234 Use the function ULT() for unsigned less than.
03235
03236 >>> x, y = BitVecs('x y', 32)
03237 >>> x < y
03238 x < y
03239 >>> (x < y).sexpr()
03240 '(bvslt x y)'
03241 >>> ULT(x, y).sexpr()
03242 '(bvult x y)'
03243 """
03244 a, b = _coerce_exprs(self, other)
03245 return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03246
03247 def __gt__(self, other):
03248 """Create the Z3 expression (signed) `other > self`.
03249
03250 Use the function UGT() for unsigned greater than.
03251
03252 >>> x, y = BitVecs('x y', 32)
03253 >>> x > y
03254 x > y
03255 >>> (x > y).sexpr()
03256 '(bvsgt x y)'
03257 >>> UGT(x, y).sexpr()
03258 '(bvugt x y)'
03259 """
03260 a, b = _coerce_exprs(self, other)
03261 return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03262
03263 def __ge__(self, other):
03264 """Create the Z3 expression (signed) `other >= self`.
03265
03266 Use the function UGE() for unsigned greater than or equal to.
03267
03268 >>> x, y = BitVecs('x y', 32)
03269 >>> x >= y
03270 x >= y
03271 >>> (x >= y).sexpr()
03272 '(bvsge x y)'
03273 >>> UGE(x, y).sexpr()
03274 '(bvuge x y)'
03275 """
03276 a, b = _coerce_exprs(self, other)
03277 return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03278
03279 def __rshift__(self, other):
03280 """Create the Z3 expression (arithmetical) right shift `self >> other`
03281
03282 Use the function LShR() for the right logical shift
03283
03284 >>> x, y = BitVecs('x y', 32)
03285 >>> x >> y
03286 x >> y
03287 >>> (x >> y).sexpr()
03288 '(bvashr x y)'
03289 >>> LShR(x, y).sexpr()
03290 '(bvlshr x y)'
03291 >>> BitVecVal(4, 3)
03292 4
03293 >>> BitVecVal(4, 3).as_signed_long()
03294 -4
03295 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
03296 -2
03297 >>> simplify(BitVecVal(4, 3) >> 1)
03298 6
03299 >>> simplify(LShR(BitVecVal(4, 3), 1))
03300 2
03301 >>> simplify(BitVecVal(2, 3) >> 1)
03302 1
03303 >>> simplify(LShR(BitVecVal(2, 3), 1))
03304 1
03305 """
03306 a, b = _coerce_exprs(self, other)
03307 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03308
03309 def __lshift__(self, other):
03310 """Create the Z3 expression left shift `self << other`
03311
03312 >>> x, y = BitVecs('x y', 32)
03313 >>> x << y
03314 x << y
03315 >>> (x << y).sexpr()
03316 '(bvshl x y)'
03317 >>> simplify(BitVecVal(2, 3) << 1)
03318 4
03319 """
03320 a, b = _coerce_exprs(self, other)
03321 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
03322
03323 def __rrshift__(self, other):
03324 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
03325
03326 Use the function LShR() for the right logical shift
03327
03328 >>> x = BitVec('x', 32)
03329 >>> 10 >> x
03330 10 >> x
03331 >>> (10 >> x).sexpr()
03332 '(bvashr #x0000000a x)'
03333 """
03334 a, b = _coerce_exprs(self, other)
03335 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03336
03337 def __rlshift__(self, other):
03338 """Create the Z3 expression left shift `other << self`.
03339
03340 Use the function LShR() for the right logical shift
03341
03342 >>> x = BitVec('x', 32)
03343 >>> 10 << x
03344 10 << x
03345 >>> (10 << x).sexpr()
03346 '(bvshl #x0000000a x)'
03347 """
03348 a, b = _coerce_exprs(self, other)
03349 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
03350
03351 class BitVecNumRef(BitVecRef):
03352 """Bit-vector values."""
03353
03354 def as_long(self):
03355 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
03356
03357 >>> v = BitVecVal(0xbadc0de, 32)
03358 >>> v
03359 195936478
03360 >>> print("0x%.8x" % v.as_long())
03361 0x0badc0de
03362 """
03363 return int(self.as_string())
03364
03365 def as_signed_long(self):
03366 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign.
03367
03368 >>> BitVecVal(4, 3).as_signed_long()
03369 -4
03370 >>> BitVecVal(7, 3).as_signed_long()
03371 -1
03372 >>> BitVecVal(3, 3).as_signed_long()
03373 3
03374 >>> BitVecVal(2**32 - 1, 32).as_signed_long()
03375 -1
03376 >>> BitVecVal(2**64 - 1, 64).as_signed_long()
03377 -1
03378 """
03379 sz = self.size()
03380 val = self.as_long()
03381 if val >= 2**(sz - 1):
03382 val = val - 2**sz
03383 if val < -2**(sz - 1):
03384 val = val + 2**sz
03385 return int(val)
03386
03387 def as_string(self):
03388 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
03389
03390 def is_bv(a):
03391 """Return `True` if `a` is a Z3 bit-vector expression.
03392
03393 >>> b = BitVec('b', 32)
03394 >>> is_bv(b)
03395 True
03396 >>> is_bv(b + 10)
03397 True
03398 >>> is_bv(Int('x'))
03399 False
03400 """
03401 return isinstance(a, BitVecRef)
03402
03403 def is_bv_value(a):
03404 """Return `True` if `a` is a Z3 bit-vector numeral value.
03405
03406 >>> b = BitVec('b', 32)
03407 >>> is_bv_value(b)
03408 False
03409 >>> b = BitVecVal(10, 32)
03410 >>> b
03411 10
03412 >>> is_bv_value(b)
03413 True
03414 """
03415 return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
03416
03417 def BV2Int(a):
03418 """Return the Z3 expression BV2Int(a).
03419
03420 >>> b = BitVec('b', 3)
03421 >>> BV2Int(b).sort()
03422 Int
03423 >>> x = Int('x')
03424 >>> x > BV2Int(b)
03425 x > BV2Int(b)
03426 >>> solve(x > BV2Int(b), b == 1, x < 3)
03427 [b = 1, x = 2]
03428 """
03429 if __debug__:
03430 _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
03431 ctx = a.ctx
03432 ## investigate problem with bv2int
03433 return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)
03434
03435 def BitVecSort(sz, ctx=None):
03436 """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
03437
03438 >>> Byte = BitVecSort(8)
03439 >>> Word = BitVecSort(16)
03440 >>> Byte
03441 BitVec(8)
03442 >>> x = Const('x', Byte)
03443 >>> eq(x, BitVec('x', 8))
03444 True
03445 """
03446 ctx = _get_ctx(ctx)
03447 return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
03448
03449 def BitVecVal(val, bv, ctx=None):
03450 """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
03451
03452 >>> v = BitVecVal(10, 32)
03453 >>> v
03454 10
03455 >>> print("0x%.8x" % v.as_long())
03456 0x0000000a
03457 """
03458 if is_bv_sort(bv):
03459 ctx = bv.ctx
03460 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
03461 else:
03462 ctx = _get_ctx(ctx)
03463 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
03464
03465 def BitVec(name, bv, ctx=None):
03466 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
03467 If `ctx=None`, then the global context is used.
03468
03469 >>> x = BitVec('x', 16)
03470 >>> is_bv(x)
03471 True
03472 >>> x.size()
03473 16
03474 >>> x.sort()
03475 BitVec(16)
03476 >>> word = BitVecSort(16)
03477 >>> x2 = BitVec('x', word)
03478 >>> eq(x, x2)
03479 True
03480 """
03481 if isinstance(bv, BitVecSortRef):
03482 ctx = bv.ctx
03483 else:
03484 ctx = _get_ctx(ctx)
03485 bv = BitVecSort(bv, ctx)
03486 return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
03487
03488 def BitVecs(names, bv, ctx=None):
03489 """Return a tuple of bit-vector constants of size bv.
03490
03491 >>> x, y, z = BitVecs('x y z', 16)
03492 >>> x.size()
03493 16
03494 >>> x.sort()
03495 BitVec(16)
03496 >>> Sum(x, y, z)
03497 0 + x + y + z
03498 >>> Product(x, y, z)
03499 1*x*y*z
03500 >>> simplify(Product(x, y, z))
03501 x*y*z
03502 """
03503 ctx = _get_ctx(ctx)
03504 if isinstance(names, str):
03505 names = names.split(" ")
03506 return [BitVec(name, bv, ctx) for name in names]
03507
03508 def Concat(*args):
03509 """Create a Z3 bit-vector concatenation expression.
03510
03511 >>> v = BitVecVal(1, 4)
03512 >>> Concat(v, v+1, v)
03513 Concat(Concat(1, 1 + 1), 1)
03514 >>> simplify(Concat(v, v+1, v))
03515 289
03516 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
03517 121
03518 """
03519 args = _get_args(args)
03520 if __debug__:
03521 _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
03522 _z3_assert(len(args) >= 2, "At least two arguments expected.")
03523 ctx = args[0].ctx
03524 r = args[0]
03525 for i in range(len(args) - 1):
03526 r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
03527 return r
03528
03529 def Extract(high, low, a):
03530 """Create a Z3 bit-vector extraction expression.
03531
03532 >>> x = BitVec('x', 8)
03533 >>> Extract(6, 2, x)
03534 Extract(6, 2, x)
03535 >>> Extract(6, 2, x).sort()
03536 BitVec(5)
03537 """
03538 if __debug__:
03539 _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
03540 _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
03541 _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
03542 return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
03543
03544 def _check_bv_args(a, b):
03545 if __debug__:
03546 _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression")
03547
03548 def ULE(a, b):
03549 """Create the Z3 expression (unsigned) `other <= self`.
03550
03551 Use the operator <= for signed less than or equal to.
03552
03553 >>> x, y = BitVecs('x y', 32)
03554 >>> ULE(x, y)
03555 ULE(x, y)
03556 >>> (x <= y).sexpr()
03557 '(bvsle x y)'
03558 >>> ULE(x, y).sexpr()
03559 '(bvule x y)'
03560 """
03561 _check_bv_args(a, b)
03562 a, b = _coerce_exprs(a, b)
03563 return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03564
03565 def ULT(a, b):
03566 """Create the Z3 expression (unsigned) `other < self`.
03567
03568 Use the operator < for signed less than.
03569
03570 >>> x, y = BitVecs('x y', 32)
03571 >>> ULT(x, y)
03572 ULT(x, y)
03573 >>> (x < y).sexpr()
03574 '(bvslt x y)'
03575 >>> ULT(x, y).sexpr()
03576 '(bvult x y)'
03577 """
03578 _check_bv_args(a, b)
03579 a, b = _coerce_exprs(a, b)
03580 return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03581
03582 def UGE(a, b):
03583 """Create the Z3 expression (unsigned) `other >= self`.
03584
03585 Use the operator >= for signed greater than or equal to.
03586
03587 >>> x, y = BitVecs('x y', 32)
03588 >>> UGE(x, y)
03589 UGE(x, y)
03590 >>> (x >= y).sexpr()
03591 '(bvsge x y)'
03592 >>> UGE(x, y).sexpr()
03593 '(bvuge x y)'
03594 """
03595 _check_bv_args(a, b)
03596 a, b = _coerce_exprs(a, b)
03597 return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03598
03599 def UGT(a, b):
03600 """Create the Z3 expression (unsigned) `other > self`.
03601
03602 Use the operator > for signed greater than.
03603
03604 >>> x, y = BitVecs('x y', 32)
03605 >>> UGT(x, y)
03606 UGT(x, y)
03607 >>> (x > y).sexpr()
03608 '(bvsgt x y)'
03609 >>> UGT(x, y).sexpr()
03610 '(bvugt x y)'
03611 """
03612 _check_bv_args(a, b)
03613 a, b = _coerce_exprs(a, b)
03614 return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03615
03616 def UDiv(a, b):
03617 """Create the Z3 expression (unsigned) division `self / other`.
03618
03619 Use the operator / for signed division.
03620
03621 >>> x = BitVec('x', 32)
03622 >>> y = BitVec('y', 32)
03623 >>> UDiv(x, y)
03624 UDiv(x, y)
03625 >>> UDiv(x, y).sort()
03626 BitVec(32)
03627 >>> (x / y).sexpr()
03628 '(bvsdiv x y)'
03629 >>> UDiv(x, y).sexpr()
03630 '(bvudiv x y)'
03631 """
03632 _check_bv_args(a, b)
03633 a, b = _coerce_exprs(a, b)
03634 return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03635
03636 def URem(a, b):
03637 """Create the Z3 expression (unsigned) remainder `self % other`.
03638
03639 Use the operator % for signed modulus, and SRem() for signed remainder.
03640
03641 >>> x = BitVec('x', 32)
03642 >>> y = BitVec('y', 32)
03643 >>> URem(x, y)
03644 URem(x, y)
03645 >>> URem(x, y).sort()
03646 BitVec(32)
03647 >>> (x % y).sexpr()
03648 '(bvsmod x y)'
03649 >>> URem(x, y).sexpr()
03650 '(bvurem x y)'
03651 """
03652 _check_bv_args(a, b)
03653 a, b = _coerce_exprs(a, b)
03654 return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03655
03656 def SRem(a, b):
03657 """Create the Z3 expression signed remainder.
03658
03659 Use the operator % for signed modulus, and URem() for unsigned remainder.
03660
03661 >>> x = BitVec('x', 32)
03662 >>> y = BitVec('y', 32)
03663 >>> SRem(x, y)
03664 SRem(x, y)
03665 >>> SRem(x, y).sort()
03666 BitVec(32)
03667 >>> (x % y).sexpr()
03668 '(bvsmod x y)'
03669 >>> SRem(x, y).sexpr()
03670 '(bvsrem x y)'
03671 """
03672 _check_bv_args(a, b)
03673 a, b = _coerce_exprs(a, b)
03674 return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03675
03676 def LShR(a, b):
03677 """Create the Z3 expression logical right shift.
03678
03679 Use the operator >> for the arithmetical right shift.
03680
03681 >>> x, y = BitVecs('x y', 32)
03682 >>> LShR(x, y)
03683 LShR(x, y)
03684 >>> (x >> y).sexpr()
03685 '(bvashr x y)'
03686 >>> LShR(x, y).sexpr()
03687 '(bvlshr x y)'
03688 >>> BitVecVal(4, 3)
03689 4
03690 >>> BitVecVal(4, 3).as_signed_long()
03691 -4
03692 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
03693 -2
03694 >>> simplify(BitVecVal(4, 3) >> 1)
03695 6
03696 >>> simplify(LShR(BitVecVal(4, 3), 1))
03697 2
03698 >>> simplify(BitVecVal(2, 3) >> 1)
03699 1
03700 >>> simplify(LShR(BitVecVal(2, 3), 1))
03701 1
03702 """
03703 _check_bv_args(a, b)
03704 a, b = _coerce_exprs(a, b)
03705 return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03706
03707 def RotateLeft(a, b):
03708 """Return an expression representing `a` rotated to the left `b` times.
03709
03710 >>> a, b = BitVecs('a b', 16)
03711 >>> RotateLeft(a, b)
03712 RotateLeft(a, b)
03713 >>> simplify(RotateLeft(a, 0))
03714 a
03715 >>> simplify(RotateLeft(a, 16))
03716 a
03717 """
03718 _check_bv_args(a, b)
03719 a, b = _coerce_exprs(a, b)
03720 return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03721
03722 def RotateRight(a, b):
03723 """Return an expression representing `a` rotated to the right `b` times.
03724
03725 >>> a, b = BitVecs('a b', 16)
03726 >>> RotateRight(a, b)
03727 RotateRight(a, b)
03728 >>> simplify(RotateRight(a, 0))
03729 a
03730 >>> simplify(RotateRight(a, 16))
03731 a
03732 """
03733 _check_bv_args(a, b)
03734 a, b = _coerce_exprs(a, b)
03735 return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
03736
03737 def SignExt(n, a):
03738 """Return a bit-vector expression with `n` extra sign-bits.
03739
03740 >>> x = BitVec('x', 16)
03741 >>> n = SignExt(8, x)
03742 >>> n.size()
03743 24
03744 >>> n
03745 SignExt(8, x)
03746 >>> n.sort()
03747 BitVec(24)
03748 >>> v0 = BitVecVal(2, 2)
03749 >>> v0
03750 2
03751 >>> v0.size()
03752 2
03753 >>> v = simplify(SignExt(6, v0))
03754 >>> v
03755 254
03756 >>> v.size()
03757 8
03758 >>> print("%.x" % v.as_long())
03759 fe
03760 """
03761 if __debug__:
03762 _z3_assert(isinstance(n, int), "First argument must be an integer")
03763 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
03764 return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
03765
03766 def ZeroExt(n, a):
03767 """Return a bit-vector expression with `n` extra zero-bits.
03768
03769 >>> x = BitVec('x', 16)
03770 >>> n = ZeroExt(8, x)
03771 >>> n.size()
03772 24
03773 >>> n
03774 ZeroExt(8, x)
03775 >>> n.sort()
03776 BitVec(24)
03777 >>> v0 = BitVecVal(2, 2)
03778 >>> v0
03779 2
03780 >>> v0.size()
03781 2
03782 >>> v = simplify(ZeroExt(6, v0))
03783 >>> v
03784 2
03785 >>> v.size()
03786 8
03787 """
03788 if __debug__:
03789 _z3_assert(isinstance(n, int), "First argument must be an integer")
03790 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
03791 return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
03792
03793 def RepeatBitVec(n, a):
03794 """Return an expression representing `n` copies of `a`.
03795
03796 >>> x = BitVec('x', 8)
03797 >>> n = RepeatBitVec(4, x)
03798 >>> n
03799 RepeatBitVec(4, x)
03800 >>> n.size()
03801 32
03802 >>> v0 = BitVecVal(10, 4)
03803 >>> print("%.x" % v0.as_long())
03804 a
03805 >>> v = simplify(RepeatBitVec(4, v0))
03806 >>> v.size()
03807 16
03808 >>> print("%.x" % v.as_long())
03809 aaaa
03810 """
03811 if __debug__:
03812 _z3_assert(isinstance(n, int), "First argument must be an integer")
03813 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
03814 return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
03815
03816 #########################################
03817 #
03818 # Arrays
03819 #
03820 #########################################
03821
03822 class ArraySortRef(SortRef):
03823 """Array sorts."""
03824
03825 def domain(self):
03826 """Return the domain of the array sort `self`.
03827
03828 >>> A = ArraySort(IntSort(), BoolSort())
03829 >>> A.domain()
03830 Int
03831 """
03832 return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx)
03833
03834 def range(self):
03835 """Return the range of the array sort `self`.
03836
03837 >>> A = ArraySort(IntSort(), BoolSort())
03838 >>> A.range()
03839 Bool
03840 """
03841 return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)
03842
03843 class ArrayRef(ExprRef):
03844 """Array expressions. """
03845
03846 def sort(self):
03847 """Return the array sort of the array expression `self`.
03848
03849 >>> a = Array('a', IntSort(), BoolSort())
03850 >>> a.sort()
03851 Array(Int, Bool)
03852 """
03853 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
03854
03855 def domain(self):
03856 """Shorthand for `self.sort().domain()`.
03857
03858 >>> a = Array('a', IntSort(), BoolSort())
03859 >>> a.domain()
03860 Int
03861 """
03862 return self.sort().domain()
03863
03864 def range(self):
03865 """Shorthand for `self.sort().range()`.
03866
03867 >>> a = Array('a', IntSort(), BoolSort())
03868 >>> a.range()
03869 Bool
03870 """
03871 return self.sort().range()
03872
03873 def __getitem__(self, arg):
03874 """Return the Z3 expression `self[arg]`.
03875
03876 >>> a = Array('a', IntSort(), BoolSort())
03877 >>> i = Int('i')
03878 >>> a[i]
03879 a[i]
03880 >>> a[i].sexpr()
03881 '(select a i)'
03882 """
03883 arg = self.domain().cast(arg)
03884 return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
03885
03886 def is_array(a):
03887 """Return `True` if `a` is a Z3 array expression.
03888
03889 >>> a = Array('a', IntSort(), IntSort())
03890 >>> is_array(a)
03891 True
03892 >>> is_array(Store(a, 0, 1))
03893 True
03894 >>> is_array(a[0])
03895 False
03896 """
03897 return isinstance(a, ArrayRef)
03898
03899 def is_const_array(a):
03900 """Return `True` if `a` is a Z3 constant array.
03901
03902 >>> a = K(IntSort(), 10)
03903 >>> is_const_array(a)
03904 True
03905 >>> a = Array('a', IntSort(), IntSort())
03906 >>> is_const_array(a)
03907 False
03908 """
03909 return is_app_of(a, Z3_OP_CONST_ARRAY)
03910
03911 def is_K(a):
03912 """Return `True` if `a` is a Z3 constant array.
03913
03914 >>> a = K(IntSort(), 10)
03915 >>> is_K(a)
03916 True
03917 >>> a = Array('a', IntSort(), IntSort())
03918 >>> is_K(a)
03919 False
03920 """
03921 return is_app_of(a, Z3_OP_CONST_ARRAY)
03922
03923 def is_map(a):
03924 """Return `True` if `a` is a Z3 map array expression.
03925
03926 >>> f = Function('f', IntSort(), IntSort())
03927 >>> b = Array('b', IntSort(), IntSort())
03928 >>> a = Map(f, b)
03929 >>> a
03930 Map(f, b)
03931 >>> is_map(a)
03932 True
03933 >>> is_map(b)
03934 False
03935 """
03936 return is_app_of(a, Z3_OP_ARRAY_MAP)
03937
03938 def get_map_func(a):
03939 """Return the function declaration associated with a Z3 map array expression.
03940
03941 >>> f = Function('f', IntSort(), IntSort())
03942 >>> b = Array('b', IntSort(), IntSort())
03943 >>> a = Map(f, b)
03944 >>> eq(f, get_map_func(a))
03945 True
03946 >>> get_map_func(a)
03947 f
03948 >>> get_map_func(a)(0)
03949 f(0)
03950 """
03951 if __debug__:
03952 _z3_assert(is_map(a), "Z3 array map expression expected.")
03953 return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
03954
03955 def ArraySort(d, r):
03956 """Return the Z3 array sort with the given domain and range sorts.
03957
03958 >>> A = ArraySort(IntSort(), BoolSort())
03959 >>> A
03960 Array(Int, Bool)
03961 >>> A.domain()
03962 Int
03963 >>> A.range()
03964 Bool
03965 >>> AA = ArraySort(IntSort(), A)
03966 >>> AA
03967 Array(Int, Array(Int, Bool))
03968 """
03969 if __debug__:
03970 _z3_assert(is_sort(d), "Z3 sort expected")
03971 _z3_assert(is_sort(r), "Z3 sort expected")
03972 _z3_assert(d.ctx == r.ctx, "Context mismatch")
03973 ctx = d.ctx
03974 return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
03975
03976 def Array(name, dom, rng):
03977 """Return an array constant named `name` with the given domain and range sorts.
03978
03979 >>> a = Array('a', IntSort(), IntSort())
03980 >>> a.sort()
03981 Array(Int, Int)
03982 >>> a[0]
03983 a[0]
03984 """
03985 s = ArraySort(dom, rng)
03986 ctx = s.ctx
03987 return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
03988
03989 def Update(a, i, v):
03990 """Return a Z3 store array expression.
03991
03992 >>> a = Array('a', IntSort(), IntSort())
03993 >>> i, v = Ints('i v')
03994 >>> s = Update(a, i, v)
03995 >>> s.sort()
03996 Array(Int, Int)
03997 >>> prove(s[i] == v)
03998 proved
03999 >>> j = Int('j')
04000 >>> prove(Implies(i != j, s[j] == a[j]))
04001 proved
04002 """
04003 if __debug__:
04004 _z3_assert(is_array(a), "First argument must be a Z3 array expression")
04005 i = a.domain().cast(i)
04006 v = a.range().cast(v)
04007 ctx = a.ctx
04008 return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
04009
04010 def Store(a, i, v):
04011 """Return a Z3 store array expression.
04012
04013 >>> a = Array('a', IntSort(), IntSort())
04014 >>> i, v = Ints('i v')
04015 >>> s = Store(a, i, v)
04016 >>> s.sort()
04017 Array(Int, Int)
04018 >>> prove(s[i] == v)
04019 proved
04020 >>> j = Int('j')
04021 >>> prove(Implies(i != j, s[j] == a[j]))
04022 proved
04023 """
04024 return Update(a, i, v)
04025
04026 def Select(a, i):
04027 """Return a Z3 select array expression.
04028
04029 >>> a = Array('a', IntSort(), IntSort())
04030 >>> i = Int('i')
04031 >>> Select(a, i)
04032 a[i]
04033 >>> eq(Select(a, i), a[i])
04034 True
04035 """
04036 if __debug__:
04037 _z3_assert(is_array(a), "First argument must be a Z3 array expression")
04038 return a[i]
04039
04040 def Map(f, *args):
04041 """Return a Z3 map array expression.
04042
04043 >>> f = Function('f', IntSort(), IntSort(), IntSort())
04044 >>> a1 = Array('a1', IntSort(), IntSort())
04045 >>> a2 = Array('a2', IntSort(), IntSort())
04046 >>> b = Map(f, a1, a2)
04047 >>> b
04048 Map(f, a1, a2)
04049 >>> prove(b[0] == f(a1[0], a2[0]))
04050 proved
04051 """
04052 args = _get_args(args)
04053 if __debug__:
04054 _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
04055 _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
04056 _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
04057 _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
04058 _args, sz = _to_ast_array(args)
04059 ctx = f.ctx
04060 return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
04061
04062 def K(dom, v):
04063 """Return a Z3 constant array expression.
04064
04065 >>> a = K(IntSort(), 10)
04066 >>> a
04067 K(Int, 10)
04068 >>> a.sort()
04069 Array(Int, Int)
04070 >>> i = Int('i')
04071 >>> a[i]
04072 K(Int, 10)[i]
04073 >>> simplify(a[i])
04074 10
04075 """
04076 if __debug__:
04077 _z3_assert(is_sort(dom), "Z3 sort expected")
04078 ctx = dom.ctx
04079 if not is_expr(v):
04080 v = _py2expr(v, ctx)
04081 return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
04082
04083 def is_select(a):
04084 """Return `True` if `a` is a Z3 array select application.
04085
04086 >>> a = Array('a', IntSort(), IntSort())
04087 >>> is_select(a)
04088 False
04089 >>> i = Int('i')
04090 >>> is_select(a[i])
04091 True
04092 """
04093 return is_app_of(a, Z3_OP_SELECT)
04094
04095 def is_store(a):
04096 """Return `True` if `a` is a Z3 array store application.
04097
04098 >>> a = Array('a', IntSort(), IntSort())
04099 >>> is_store(a)
04100 False
04101 >>> is_store(Store(a, 0, 1))
04102 True
04103 """
04104 return is_app_of(a, Z3_OP_STORE)
04105
04106 #########################################
04107 #
04108 # Datatypes
04109 #
04110 #########################################
04111
04112 def _valid_accessor(acc):
04113 """Return `True` if acc is pair of the form (String, Datatype or Sort). """
04114 return isinstance(acc, tuple) and len(acc) == 2 and isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1]))
04115
04116 class Datatype:
04117 """Helper class for declaring Z3 datatypes.
04118
04119 >>> List = Datatype('List')
04120 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04121 >>> List.declare('nil')
04122 >>> List = List.create()
04123 >>>
04124 >>> List.nil
04125 nil
04126 >>> List.cons(10, List.nil)
04127 cons(10, nil)
04128 >>> List.cons(10, List.nil).sort()
04129 List
04130 >>> cons = List.cons
04131 >>> nil = List.nil
04132 >>> car = List.car
04133 >>> cdr = List.cdr
04134 >>> n = cons(1, cons(0, nil))
04135 >>> n
04136 cons(1, cons(0, nil))
04137 >>> simplify(cdr(n))
04138 cons(0, nil)
04139 >>> simplify(car(n))
04140 1
04141 """
04142 def __init__(self, name, ctx=None):
04143 self.ctx = _get_ctx(ctx)
04144 self.name = name
04145 self.constructors = []
04146
04147 def declare_core(self, name, rec_name, *args):
04148 if __debug__:
04149 _z3_assert(isinstance(name, str), "String expected")
04150 _z3_assert(isinstance(rec_name, str), "String expected")
04151 _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)")
04152 self.constructors.append((name, rec_name, args))
04153
04154 def declare(self, name, *args):
04155 """Declare constructor named `name` with the given accessors `args`.
04156 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.
04157
04158 In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
04159 declares the constructor named `cons` that builds a new List using an integer and a List.
04160 It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
04161 and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create
04162 the actual datatype in Z3.
04163
04164 >>> List = Datatype('List')
04165 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04166 >>> List.declare('nil')
04167 >>> List = List.create()
04168 """
04169 if __debug__:
04170 _z3_assert(isinstance(name, str), "String expected")
04171 _z3_assert(name != "", "Constructor name cannot be empty")
04172 return self.declare_core(name, "is_" + name, *args)
04173
04174 def __repr__(self):
04175 return "Datatype(%s, %s)" % (self.name, self.constructors)
04176
04177 def create(self):
04178 """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`.
04179
04180 The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
04181
04182 >>> List = Datatype('List')
04183 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04184 >>> List.declare('nil')
04185 >>> List = List.create()
04186 >>> List.nil
04187 nil
04188 >>> List.cons(10, List.nil)
04189 cons(10, nil)
04190 """
04191 return CreateDatatypes([self])[0]
04192
04193 class ScopedConstructor:
04194 """Auxiliary object used to create Z3 datatypes."""
04195 def __init__(self, c, ctx):
04196 self.c = c
04197 self.ctx = ctx
04198 def __del__(self):
04199 Z3_del_constructor(self.ctx.ref(), self.c)
04200
04201 class ScopedConstructorList:
04202 """Auxiliary object used to create Z3 datatypes."""
04203 def __init__(self, c, ctx):
04204 self.c = c
04205 self.ctx = ctx
04206 def __del__(self):
04207 Z3_del_constructor_list(self.ctx.ref(), self.c)
04208
04209 def CreateDatatypes(*ds):
04210 """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
04211
04212 In the following example we define a Tree-List using two mutually recursive datatypes.
04213
04214 >>> TreeList = Datatype('TreeList')
04215 >>> Tree = Datatype('Tree')
04216 >>>
04217 >>> Tree.declare('leaf', ('val', IntSort()))
04218 >>>
04219 >>> Tree.declare('node', ('children', TreeList))
04220 >>> TreeList.declare('nil')
04221 >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
04222 >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
04223 >>> Tree.val(Tree.leaf(10))
04224 val(leaf(10))
04225 >>> simplify(Tree.val(Tree.leaf(10)))
04226 10
04227 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
04228 >>> n1
04229 node(cons(leaf(10), cons(leaf(20), nil)))
04230 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
04231 >>> simplify(n2 == n1)
04232 False
04233 >>> simplify(TreeList.car(Tree.children(n2)) == n1)
04234 True
04235 """
04236 ds = _get_args(ds)
04237 if __debug__:
04238 _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
04239 _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
04240 _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
04241 _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
04242 ctx = ds[0].ctx
04243 num = len(ds)
04244 names = (Symbol * num)()
04245 out = (Sort * num)()
04246 clists = (ConstructorList * num)()
04247 to_delete = []
04248 for i in range(num):
04249 d = ds[i]
04250 names[i] = to_symbol(d.name, ctx)
04251 num_cs = len(d.constructors)
04252 cs = (Constructor * num_cs)()
04253 for j in range(num_cs):
04254 c = d.constructors[j]
04255 cname = to_symbol(c[0], ctx)
04256 rname = to_symbol(c[1], ctx)
04257 fs = c[2]
04258 num_fs = len(fs)
04259 fnames = (Symbol * num_fs)()
04260 sorts = (Sort * num_fs)()
04261 refs = (ctypes.c_uint * num_fs)()
04262 for k in range(num_fs):
04263 fname = fs[k][0]
04264 ftype = fs[k][1]
04265 fnames[k] = to_symbol(fname, ctx)
04266 if isinstance(ftype, Datatype):
04267 if __debug__:
04268 _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
04269 sorts[k] = None
04270 refs[k] = ds.index(ftype)
04271 else:
04272 if __debug__:
04273 _z3_assert(is_sort(ftype), "Z3 sort expected")
04274 sorts[k] = ftype.ast
04275 refs[k] = 0
04276 cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
04277 to_delete.append(ScopedConstructor(cs[j], ctx))
04278 clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
04279 to_delete.append(ScopedConstructorList(clists[i], ctx))
04280 Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
04281 result = []
04282 ## Create a field for every constructor, recognizer and accessor
04283 for i in range(num):
04284 dref = DatatypeSortRef(out[i], ctx)
04285 num_cs = dref.num_constructors()
04286 for j in range(num_cs):
04287 cref = dref.constructor(j)
04288 cref_name = cref.name()
04289 cref_arity = cref.arity()
04290 if cref.arity() == 0:
04291 cref = cref()
04292 setattr(dref, cref_name, cref)
04293 rref = dref.recognizer(j)
04294 setattr(dref, rref.name(), rref)
04295 for k in range(cref_arity):
04296 aref = dref.accessor(j, k)
04297 setattr(dref, aref.name(), aref)
04298 result.append(dref)
04299 return tuple(result)
04300
04301 class DatatypeSortRef(SortRef):
04302 """Datatype sorts."""
04303 def num_constructors(self):
04304 """Return the number of constructors in the given Z3 datatype.
04305
04306 >>> List = Datatype('List')
04307 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04308 >>> List.declare('nil')
04309 >>> List = List.create()
04310 >>>
04311 >>> List.num_constructors()
04312 2
04313 """
04314 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
04315
04316 def constructor(self, idx):
04317 """Return a constructor of the datatype `self`.
04318
04319 >>> List = Datatype('List')
04320 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04321 >>> List.declare('nil')
04322 >>> List = List.create()
04323 >>>
04324 >>> List.num_constructors()
04325 2
04326 >>> List.constructor(0)
04327 cons
04328 >>> List.constructor(1)
04329 nil
04330 """
04331 if __debug__:
04332 _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
04333 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
04334
04335 def recognizer(self, idx):
04336 """In Z3, each constructor has an associated recognizer predicate.
04337
04338 If the constructor is named `name`, then the recognizer `is_name`.
04339
04340 >>> List = Datatype('List')
04341 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04342 >>> List.declare('nil')
04343 >>> List = List.create()
04344 >>>
04345 >>> List.num_constructors()
04346 2
04347 >>> List.recognizer(0)
04348 is_cons
04349 >>> List.recognizer(1)
04350 is_nil
04351 >>> simplify(List.is_nil(List.cons(10, List.nil)))
04352 False
04353 >>> simplify(List.is_cons(List.cons(10, List.nil)))
04354 True
04355 >>> l = Const('l', List)
04356 >>> simplify(List.is_cons(l))
04357 is_cons(l)
04358 """
04359 if __debug__:
04360 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
04361 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
04362
04363 def accessor(self, i, j):
04364 """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
04365
04366 >>> List = Datatype('List')
04367 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04368 >>> List.declare('nil')
04369 >>> List = List.create()
04370 >>> List.num_constructors()
04371 2
04372 >>> List.constructor(0)
04373 cons
04374 >>> num_accs = List.constructor(0).arity()
04375 >>> num_accs
04376 2
04377 >>> List.accessor(0, 0)
04378 car
04379 >>> List.accessor(0, 1)
04380 cdr
04381 >>> List.constructor(1)
04382 nil
04383 >>> num_accs = List.constructor(1).arity()
04384 >>> num_accs
04385 0
04386 """
04387 if __debug__:
04388 _z3_assert(i < self.num_constructors(), "Invalid constructor index")
04389 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
04390 return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
04391
04392 class DatatypeRef(ExprRef):
04393 """Datatype expressions."""
04394 def sort(self):
04395 """Return the datatype sort of the datatype expression `self`."""
04396 return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
04397
04398 def EnumSort(name, values, ctx=None):
04399 """Return a new enumeration sort named `name` containing the given values.
04400
04401 The result is a pair (sort, list of constants).
04402 Example:
04403 >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
04404 """
04405 if __debug__:
04406 _z3_assert(isinstance(name, str), "Name must be a string")
04407 _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
04408 _z3_assert(len(values) > 0, "At least one value expected")
04409 ctx = _get_ctx(ctx)
04410 num = len(values)
04411 _val_names = (Symbol * num)()
04412 for i in range(num):
04413 _val_names[i] = to_symbol(values[i])
04414 _values = (FuncDecl * num)()
04415 _testers = (FuncDecl * num)()
04416 name = to_symbol(name)
04417 S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
04418 V = []
04419 for i in range(num):
04420 V.append(FuncDeclRef(_values[i], ctx))
04421 V = [a() for a in V]
04422 return S, V
04423
04424 #########################################
04425 #
04426 # Parameter Sets
04427 #
04428 #########################################
04429
04430 class ParamsRef:
04431 """Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3.
04432
04433 Consider using the function `args2params` to create instances of this object.
04434 """
04435 def __init__(self, ctx=None):
04436 self.ctx = _get_ctx(ctx)
04437 self.params = Z3_mk_params(self.ctx.ref())
04438 Z3_params_inc_ref(self.ctx.ref(), self.params)
04439
04440 def __del__(self):
04441 Z3_params_dec_ref(self.ctx.ref(), self.params)
04442
04443 def set(self, name, val):
04444 """Set parameter name with value val."""
04445 if __debug__:
04446 _z3_assert(isinstance(name, str), "parameter name must be a string")
04447 name_sym = to_symbol(name, self.ctx)
04448 if isinstance(val, bool):
04449 Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val)
04450 elif isinstance(val, int):
04451 Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val)
04452 elif isinstance(val, float):
04453 Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val)
04454 elif isinstance(val, str):
04455 Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx))
04456 else:
04457 if __debug__:
04458 _z3_assert(False, "invalid parameter value")
04459
04460 def __repr__(self):
04461 return Z3_params_to_string(self.ctx.ref(), self.params)
04462
04463 def validate(self, ds):
04464 _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected")
04465 Z3_params_validate(self.ctx.ref(), self.params, ds.descr)
04466
04467 def args2params(arguments, keywords, ctx=None):
04468 """Convert python arguments into a Z3_params object.
04469 A ':' is added to the keywords, and '_' is replaced with '-'
04470
04471 >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
04472 (params model true relevancy 2 elim_and true)
04473 """
04474 if __debug__:
04475 _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
04476 prev = None
04477 r = ParamsRef(ctx)
04478 for a in arguments:
04479 if prev == None:
04480 prev = a
04481 else:
04482 r.set(prev, a)
04483 prev = None
04484 for k in keywords:
04485 v = keywords[k]
04486 r.set(k, v)
04487 return r
04488
04489 class ParamDescrsRef:
04490 """Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3.
04491 """
04492 def __init__(self, descr, ctx=None):
04493 _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected")
04494 self.ctx = _get_ctx(ctx)
04495 self.descr = descr
04496 Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr)
04497
04498 def __del__(self):
04499 Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
04500
04501 def size(self):
04502 """Return the size of in the parameter description `self`.
04503 """
04504 return int(Z3_param_descrs_size(self.ctx.ref(), self.descr))
04505
04506 def __len__(self):
04507 """Return the size of in the parameter description `self`.
04508 """
04509 return self.size()
04510
04511 def get_name(self, i):
04512 """Return the i-th parameter name in the parameter description `self`.
04513 """
04514 return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i))
04515
04516 def get_kind(self, n):
04517 """Return the kind of the parameter named `n`.
04518 """
04519 return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
04520
04521 def __getitem__(self, arg):
04522 if _is_int(arg):
04523 return self.get_name(arg)
04524 else:
04525 return self.get_kind(arg)
04526
04527 def __repr__(self):
04528 return Z3_param_descrs_to_string(self.ctx.ref(), self.descr)
04529
04530 #########################################
04531 #
04532 # Goals
04533 #
04534 #########################################
04535
04536 class Goal(Z3PPObject):
04537 """Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible).
04538
04539 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
04540 A goal has a solution if one of its subgoals has a solution.
04541 A goal is unsatisfiable if all subgoals are unsatisfiable.
04542 """
04543
04544 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
04545 if __debug__:
04546 _z3_assert(goal == None or ctx != None, "If goal is different from None, then ctx must be also different from None")
04547 self.ctx = _get_ctx(ctx)
04548 self.goal = goal
04549 if self.goal == None:
04550 self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
04551 Z3_goal_inc_ref(self.ctx.ref(), self.goal)
04552
04553 def __del__(self):
04554 if self.goal != None:
04555 Z3_goal_dec_ref(self.ctx.ref(), self.goal)
04556
04557 def depth(self):
04558 """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
04559
04560 >>> x, y = Ints('x y')
04561 >>> g = Goal()
04562 >>> g.add(x == 0, y >= x + 1)
04563 >>> g.depth()
04564 0
04565 >>> r = Then('simplify', 'solve-eqs')(g)
04566 >>>
04567 >>> len(r)
04568 1
04569 >>> r[0].depth()
04570 2
04571 """
04572 return int(Z3_goal_depth(self.ctx.ref(), self.goal))
04573
04574 def inconsistent(self):
04575 """Return `True` if `self` contains the `False` constraints.
04576
04577 >>> x, y = Ints('x y')
04578 >>> g = Goal()
04579 >>> g.inconsistent()
04580 False
04581 >>> g.add(x == 0, x == 1)
04582 >>> g
04583 [x == 0, x == 1]
04584 >>> g.inconsistent()
04585 False
04586 >>> g2 = Tactic('propagate-values')(g)[0]
04587 >>> g2.inconsistent()
04588 True
04589 """
04590 return Z3_goal_inconsistent(self.ctx.ref(), self.goal)
04591
04592 def prec(self):
04593 """Return the precision (under-approximation, over-approximation, or precise) of the goal `self`.
04594
04595 >>> g = Goal()
04596 >>> g.prec() == Z3_GOAL_PRECISE
04597 True
04598 >>> x, y = Ints('x y')
04599 >>> g.add(x == y + 1)
04600 >>> g.prec() == Z3_GOAL_PRECISE
04601 True
04602 >>> t = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10)
04603 >>> g2 = t(g)[0]
04604 >>> g2
04605 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
04606 >>> g2.prec() == Z3_GOAL_PRECISE
04607 False
04608 >>> g2.prec() == Z3_GOAL_UNDER
04609 True
04610 """
04611 return Z3_goal_precision(self.ctx.ref(), self.goal)
04612
04613 def precision(self):
04614 """Alias for `prec()`.
04615
04616 >>> g = Goal()
04617 >>> g.precision() == Z3_GOAL_PRECISE
04618 True
04619 """
04620 return self.prec()
04621
04622 def size(self):
04623 """Return the number of constraints in the goal `self`.
04624
04625 >>> g = Goal()
04626 >>> g.size()
04627 0
04628 >>> x, y = Ints('x y')
04629 >>> g.add(x == 0, y > x)
04630 >>> g.size()
04631 2
04632 """
04633 return int(Z3_goal_size(self.ctx.ref(), self.goal))
04634
04635 def __len__(self):
04636 """Return the number of constraints in the goal `self`.
04637
04638 >>> g = Goal()
04639 >>> len(g)
04640 0
04641 >>> x, y = Ints('x y')
04642 >>> g.add(x == 0, y > x)
04643 >>> len(g)
04644 2
04645 """
04646 return self.size()
04647
04648 def get(self, i):
04649 """Return a constraint in the goal `self`.
04650
04651 >>> g = Goal()
04652 >>> x, y = Ints('x y')
04653 >>> g.add(x == 0, y > x)
04654 >>> g.get(0)
04655 x == 0
04656 >>> g.get(1)
04657 y > x
04658 """
04659 return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx)
04660
04661 def __getitem__(self, arg):
04662 """Return a constraint in the goal `self`.
04663
04664 >>> g = Goal()
04665 >>> x, y = Ints('x y')
04666 >>> g.add(x == 0, y > x)
04667 >>> g[0]
04668 x == 0
04669 >>> g[1]
04670 y > x
04671 """
04672 if arg >= len(self):
04673 raise IndexError
04674 return self.get(arg)
04675
04676 def assert_exprs(self, *args):
04677 """Assert constraints into the goal.
04678
04679 >>> x = Int('x')
04680 >>> g = Goal()
04681 >>> g.assert_exprs(x > 0, x < 2)
04682 >>> g
04683 [x > 0, x < 2]
04684 """
04685 args = _get_args(args)
04686 s = BoolSort(self.ctx)
04687 for arg in args:
04688 arg = s.cast(arg)
04689 Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast())
04690
04691 def append(self, *args):
04692 """Add constraints.
04693
04694 >>> x = Int('x')
04695 >>> g = Goal()
04696 >>> g.append(x > 0, x < 2)
04697 >>> g
04698 [x > 0, x < 2]
04699 """
04700 self.assert_exprs(*args)
04701
04702 def insert(self, *args):
04703 """Add constraints.
04704
04705 >>> x = Int('x')
04706 >>> g = Goal()
04707 >>> g.insert(x > 0, x < 2)
04708 >>> g
04709 [x > 0, x < 2]
04710 """
04711 self.assert_exprs(*args)
04712
04713 def add(self, *args):
04714 """Add constraints.
04715
04716 >>> x = Int('x')
04717 >>> g = Goal()
04718 >>> g.add(x > 0, x < 2)
04719 >>> g
04720 [x > 0, x < 2]
04721 """
04722 self.assert_exprs(*args)
04723
04724 def __repr__(self):
04725 return obj_to_string(self)
04726
04727 def sexpr(self):
04728 """Return a textual representation of the s-expression representing the goal."""
04729 return Z3_goal_to_string(self.ctx.ref(), self.goal)
04730
04731 def translate(self, target):
04732 """Copy goal `self` to context `target`.
04733
04734 >>> x = Int('x')
04735 >>> g = Goal()
04736 >>> g.add(x > 10)
04737 >>> g
04738 [x > 10]
04739 >>> c2 = Context()
04740 >>> g2 = g.translate(c2)
04741 >>> g2
04742 [x > 10]
04743 >>> g.ctx == main_ctx()
04744 True
04745 >>> g2.ctx == c2
04746 True
04747 >>> g2.ctx == main_ctx()
04748 False
04749 """
04750 if __debug__:
04751 _z3_assert(isinstance(target, Context), "target must be a context")
04752 return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target)
04753
04754 def simplify(self, *arguments, **keywords):
04755 """Return a new simplified goal.
04756
04757 This method is essentially invoking the simplify tactic.
04758
04759 >>> g = Goal()
04760 >>> x = Int('x')
04761 >>> g.add(x + 1 >= 2)
04762 >>> g
04763 [x + 1 >= 2]
04764 >>> g2 = g.simplify()
04765 >>> g2
04766 [x >= 1]
04767 >>>
04768 >>> g
04769 [x + 1 >= 2]
04770 """
04771 t = Tactic('simplify')
04772 return t.apply(self, *arguments, **keywords)[0]
04773
04774 def as_expr(self):
04775 """Return goal `self` as a single Z3 expression.
04776
04777 >>> x = Int('x')
04778 >>> g = Goal()
04779 >>> g.as_expr()
04780 True
04781 >>> g.add(x > 1)
04782 >>> g.as_expr()
04783 x > 1
04784 >>> g.add(x < 10)
04785 >>> g.as_expr()
04786 And(x > 1, x < 10)
04787 """
04788 sz = len(self)
04789 if sz == 0:
04790 return BoolVal(True, self.ctx)
04791 elif sz == 1:
04792 return self.get(0)
04793 else:
04794 return And([ self.get(i) for i in range(len(self)) ])
04795
04796 #########################################
04797 #
04798 # AST Vector
04799 #
04800 #########################################
04801 class AstVector(Z3PPObject):
04802 """A collection (vector) of ASTs."""
04803
04804 def __init__(self, v=None, ctx=None):
04805 self.vector = None
04806 if v == None:
04807 self.ctx = _get_ctx(ctx)
04808 self.vector = Z3_mk_ast_vector(self.ctx.ref())
04809 else:
04810 self.vector = v
04811 assert ctx != None
04812 self.ctx = ctx
04813 Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
04814
04815 def __del__(self):
04816 if self.vector != None:
04817 Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
04818
04819 def __len__(self):
04820 """Return the size of the vector `self`.
04821
04822 >>> A = AstVector()
04823 >>> len(A)
04824 0
04825 >>> A.push(Int('x'))
04826 >>> A.push(Int('x'))
04827 >>> len(A)
04828 2
04829 """
04830 return int(Z3_ast_vector_size(self.ctx.ref(), self.vector))
04831
04832 def __getitem__(self, i):
04833 """Return the AST at position `i`.
04834
04835 >>> A = AstVector()
04836 >>> A.push(Int('x') + 1)
04837 >>> A.push(Int('y'))
04838 >>> A[0]
04839 x + 1
04840 >>> A[1]
04841 y
04842 """
04843 if i >= self.__len__():
04844 raise IndexError
04845 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
04846
04847 def __setitem__(self, i, v):
04848 """Update AST at position `i`.
04849
04850 >>> A = AstVector()
04851 >>> A.push(Int('x') + 1)
04852 >>> A.push(Int('y'))
04853 >>> A[0]
04854 x + 1
04855 >>> A[0] = Int('x')
04856 >>> A[0]
04857 x
04858 """
04859 if i >= self.__len__():
04860 raise IndexError
04861 Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast())
04862
04863 def push(self, v):
04864 """Add `v` in the end of the vector.
04865
04866 >>> A = AstVector()
04867 >>> len(A)
04868 0
04869 >>> A.push(Int('x'))
04870 >>> len(A)
04871 1
04872 """
04873 Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast())
04874
04875 def resize(self, sz):
04876 """Resize the vector to `sz` elements.
04877
04878 >>> A = AstVector()
04879 >>> A.resize(10)
04880 >>> len(A)
04881 10
04882 >>> for i in range(10): A[i] = Int('x')
04883 >>> A[5]
04884 x
04885 """
04886 Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz)
04887
04888 def __contains__(self, item):
04889 """Return `True` if the vector contains `item`.
04890
04891 >>> x = Int('x')
04892 >>> A = AstVector()
04893 >>> x in A
04894 False
04895 >>> A.push(x)
04896 >>> x in A
04897 True
04898 >>> (x+1) in A
04899 False
04900 >>> A.push(x+1)
04901 >>> (x+1) in A
04902 True
04903 >>> A
04904 [x, x + 1]
04905 """
04906 for elem in self:
04907 if elem.eq(item):
04908 return True
04909 return False
04910
04911 def translate(self, other_ctx):
04912 """Copy vector `self` to context `other_ctx`.
04913
04914 >>> x = Int('x')
04915 >>> A = AstVector()
04916 >>> A.push(x)
04917 >>> c2 = Context()
04918 >>> B = A.translate(c2)
04919 >>> B
04920 [x]
04921 """
04922 return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx)
04923
04924 def __repr__(self):
04925 return obj_to_string(self)
04926
04927 def sexpr(self):
04928 """Return a textual representation of the s-expression representing the vector."""
04929 return Z3_ast_vector_to_string(self.ctx.ref(), self.vector)
04930
04931 #########################################
04932 #
04933 # AST Map
04934 #
04935 #########################################
04936 class AstMap:
04937 """A mapping from ASTs to ASTs."""
04938
04939 def __init__(self, m=None, ctx=None):
04940 self.map = None
04941 if m == None:
04942 self.ctx = _get_ctx(ctx)
04943 self.map = Z3_mk_ast_map(self.ctx.ref())
04944 else:
04945 self.map = m
04946 assert ctx != None
04947 self.ctx = ctx
04948 Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
04949
04950 def __del__(self):
04951 if self.map != None:
04952 Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
04953
04954 def __len__(self):
04955 """Return the size of the map.
04956
04957 >>> M = AstMap()
04958 >>> len(M)
04959 0
04960 >>> x = Int('x')
04961 >>> M[x] = IntVal(1)
04962 >>> len(M)
04963 1
04964 """
04965 return int(Z3_ast_map_size(self.ctx.ref(), self.map))
04966
04967 def __contains__(self, key):
04968 """Return `True` if the map contains key `key`.
04969
04970 >>> M = AstMap()
04971 >>> x = Int('x')
04972 >>> M[x] = x + 1
04973 >>> x in M
04974 True
04975 >>> x+1 in M
04976 False
04977 """
04978 return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast())
04979
04980 def __getitem__(self, key):
04981 """Retrieve the value associated with key `key`.
04982
04983 >>> M = AstMap()
04984 >>> x = Int('x')
04985 >>> M[x] = x + 1
04986 >>> M[x]
04987 x + 1
04988 """
04989 return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx)
04990
04991 def __setitem__(self, k, v):
04992 """Add/Update key `k` with value `v`.
04993
04994 >>> M = AstMap()
04995 >>> x = Int('x')
04996 >>> M[x] = x + 1
04997 >>> len(M)
04998 1
04999 >>> M[x]
05000 x + 1
05001 >>> M[x] = IntVal(1)
05002 >>> M[x]
05003 1
05004 """
05005 Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast())
05006
05007 def __repr__(self):
05008 return Z3_ast_map_to_string(self.ctx.ref(), self.map)
05009
05010 def erase(self, k):
05011 """Remove the entry associated with key `k`.
05012
05013 >>> M = AstMap()
05014 >>> x = Int('x')
05015 >>> M[x] = x + 1
05016 >>> len(M)
05017 1
05018 >>> M.erase(x)
05019 >>> len(M)
05020 0
05021 """
05022 Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast())
05023
05024 def reset(self):
05025 """Remove all entries from the map.
05026
05027 >>> M = AstMap()
05028 >>> x = Int('x')
05029 >>> M[x] = x + 1
05030 >>> M[x+x] = IntVal(1)
05031 >>> len(M)
05032 2
05033 >>> M.reset()
05034 >>> len(M)
05035 0
05036 """
05037 Z3_ast_map_reset(self.ctx.ref(), self.map)
05038
05039 def keys(self):
05040 """Return an AstVector containing all keys in the map.
05041
05042 >>> M = AstMap()
05043 >>> x = Int('x')
05044 >>> M[x] = x + 1
05045 >>> M[x+x] = IntVal(1)
05046 >>> M.keys()
05047 [x, x + x]
05048 """
05049 return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx)
05050
05051 #########################################
05052 #
05053 # Model
05054 #
05055 #########################################
05056
05057 class FuncEntry:
05058 """Store the value of the interpretation of a function in a particular point."""
05059
05060 def __init__(self, entry, ctx):
05061 self.entry = entry
05062 self.ctx = ctx
05063 Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
05064
05065 def __del__(self):
05066 Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
05067
05068 def num_args(self):
05069 """Return the number of arguments in the given entry.
05070
05071 >>> f = Function('f', IntSort(), IntSort(), IntSort())
05072 >>> s = Solver()
05073 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
05074 >>> s.check()
05075 sat
05076 >>> m = s.model()
05077 >>> f_i = m[f]
05078 >>> f_i.num_entries()
05079 3
05080 >>> e = f_i.entry(0)
05081 >>> e.num_args()
05082 2
05083 """
05084 return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
05085
05086 def arg_value(self, idx):
05087 """Return the value of argument `idx`.
05088
05089 >>> f = Function('f', IntSort(), IntSort(), IntSort())
05090 >>> s = Solver()
05091 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
05092 >>> s.check()
05093 sat
05094 >>> m = s.model()
05095 >>> f_i = m[f]
05096 >>> f_i.num_entries()
05097 3
05098 >>> e = f_i.entry(0)
05099 >>> e
05100 [0, 1, 10]
05101 >>> e.num_args()
05102 2
05103 >>> e.arg_value(0)
05104 0
05105 >>> e.arg_value(1)
05106 1
05107 >>> try:
05108 ... e.arg_value(2)
05109 ... except IndexError:
05110 ... print("index error")
05111 index error
05112 """
05113 if idx >= self.num_args():
05114 raise IndexError
05115 return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
05116
05117 def value(self):
05118 """Return the value of the function at point `self`.
05119
05120 >>> f = Function('f', IntSort(), IntSort(), IntSort())
05121 >>> s = Solver()
05122 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
05123 >>> s.check()
05124 sat
05125 >>> m = s.model()
05126 >>> f_i = m[f]
05127 >>> f_i.num_entries()
05128 3
05129 >>> e = f_i.entry(0)
05130 >>> e
05131 [0, 1, 10]
05132 >>> e.num_args()
05133 2
05134 >>> e.value()
05135 10
05136 """
05137 return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
05138
05139 def as_list(self):
05140 """Return entry `self` as a Python list.
05141 >>> f = Function('f', IntSort(), IntSort(), IntSort())
05142 >>> s = Solver()
05143 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
05144 >>> s.check()
05145 sat
05146 >>> m = s.model()
05147 >>> f_i = m[f]
05148 >>> f_i.num_entries()
05149 3
05150 >>> e = f_i.entry(0)
05151 >>> e.as_list()
05152 [0, 1, 10]
05153 """
05154 args = [ self.arg_value(i) for i in range(self.num_args())]
05155 args.append(self.value())
05156 return args
05157
05158 def __repr__(self):
05159 return repr(self.as_list())
05160
05161 class FuncInterp(Z3PPObject):
05162 """Stores the interpretation of a function in a Z3 model."""
05163
05164 def __init__(self, f, ctx):
05165 self.f = f
05166 self.ctx = ctx
05167 if self.f != None:
05168 Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
05169
05170 def __del__(self):
05171 if self.f != None:
05172 Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
05173
05174 def else_value(self):
05175 """
05176 Return the `else` value for a function interpretation.
05177 Return None if Z3 did not specify the `else` value for
05178 this object.
05179
05180 >>> f = Function('f', IntSort(), IntSort())
05181 >>> s = Solver()
05182 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05183 >>> s.check()
05184 sat
05185 >>> m = s.model()
05186 >>> m[f]
05187 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05188 >>> m[f].else_value()
05189 1
05190 """
05191 r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
05192 if r:
05193 return _to_expr_ref(r, self.ctx)
05194 else:
05195 return None
05196
05197 def num_entries(self):
05198 """Return the number of entries/points in the function interpretation `self`.
05199
05200 >>> f = Function('f', IntSort(), IntSort())
05201 >>> s = Solver()
05202 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05203 >>> s.check()
05204 sat
05205 >>> m = s.model()
05206 >>> m[f]
05207 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05208 >>> m[f].num_entries()
05209 3
05210 """
05211 return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
05212
05213 def arity(self):
05214 """Return the number of arguments for each entry in the function interpretation `self`.
05215
05216 >>> f = Function('f', IntSort(), IntSort())
05217 >>> s = Solver()
05218 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05219 >>> s.check()
05220 sat
05221 >>> m = s.model()
05222 >>> m[f].arity()
05223 1
05224 """
05225 return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
05226
05227 def entry(self, idx):
05228 """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
05229
05230 >>> f = Function('f', IntSort(), IntSort())
05231 >>> s = Solver()
05232 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05233 >>> s.check()
05234 sat
05235 >>> m = s.model()
05236 >>> m[f]
05237 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05238 >>> m[f].num_entries()
05239 3
05240 >>> m[f].entry(0)
05241 [0, 1]
05242 >>> m[f].entry(1)
05243 [1, 1]
05244 >>> m[f].entry(2)
05245 [2, 0]
05246 """
05247 if idx >= self.num_entries():
05248 raise IndexError
05249 return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
05250
05251 def as_list(self):
05252 """Return the function interpretation as a Python list.
05253 >>> f = Function('f', IntSort(), IntSort())
05254 >>> s = Solver()
05255 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
05256 >>> s.check()
05257 sat
05258 >>> m = s.model()
05259 >>> m[f]
05260 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
05261 >>> m[f].as_list()
05262 [[0, 1], [1, 1], [2, 0], 1]
05263 """
05264 r = [ self.entry(i).as_list() for i in range(self.num_entries())]
05265 r.append(self.else_value())
05266 return r
05267
05268 def __repr__(self):
05269 return obj_to_string(self)
05270
05271 class ModelRef(Z3PPObject):
05272 """Model/Solution of a satisfiability problem (aka system of constraints)."""
05273
05274 def __init__(self, m, ctx):
05275 assert ctx != None
05276 self.model = m
05277 self.ctx = ctx
05278 Z3_model_inc_ref(self.ctx.ref(), self.model)
05279
05280 def __del__(self):
05281 Z3_model_dec_ref(self.ctx.ref(), self.model)
05282
05283 def __repr__(self):
05284 return obj_to_string(self)
05285
05286 def sexpr(self):
05287 """Return a textual representation of the s-expression representing the model."""
05288 return Z3_model_to_string(self.ctx.ref(), self.model)
05289
05290 def eval(self, t, model_completion=False):
05291 """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`.
05292
05293 >>> x = Int('x')
05294 >>> s = Solver()
05295 >>> s.add(x > 0, x < 2)
05296 >>> s.check()
05297 sat
05298 >>> m = s.model()
05299 >>> m.eval(x + 1)
05300 2
05301 >>> m.eval(x == 1)
05302 True
05303 >>> y = Int('y')
05304 >>> m.eval(y + x)
05305 1 + y
05306 >>> m.eval(y)
05307 y
05308 >>> m.eval(y, model_completion=True)
05309 0
05310 >>>
05311 >>> m.eval(y + x)
05312 1
05313 """
05314 r = (Ast * 1)()
05315 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
05316 return _to_expr_ref(r[0], self.ctx)
05317 raise Z3Exception("failed to evaluate expression in the model")
05318
05319 def evaluate(self, t, model_completion=False):
05320 """Alias for `eval`.
05321
05322 >>> x = Int('x')
05323 >>> s = Solver()
05324 >>> s.add(x > 0, x < 2)
05325 >>> s.check()
05326 sat
05327 >>> m = s.model()
05328 >>> m.evaluate(x + 1)
05329 2
05330 >>> m.evaluate(x == 1)
05331 True
05332 >>> y = Int('y')
05333 >>> m.evaluate(y + x)
05334 1 + y
05335 >>> m.evaluate(y)
05336 y
05337 >>> m.evaluate(y, model_completion=True)
05338 0
05339 >>>
05340 >>> m.evaluate(y + x)
05341 1
05342 """
05343 return self.eval(t, model_completion)
05344
05345 def __len__(self):
05346 """Return the number of constant and function declarations in the model `self`.
05347
05348 >>> f = Function('f', IntSort(), IntSort())
05349 >>> x = Int('x')
05350 >>> s = Solver()
05351 >>> s.add(x > 0, f(x) != x)
05352 >>> s.check()
05353 sat
05354 >>> m = s.model()
05355 >>> len(m)
05356 2
05357 """
05358 return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model))
05359
05360 def get_interp(self, decl):
05361 """Return the interpretation for a given declaration or constant.
05362
05363 >>> f = Function('f', IntSort(), IntSort())
05364 >>> x = Int('x')
05365 >>> s = Solver()
05366 >>> s.add(x > 0, x < 2, f(x) == 0)
05367 >>> s.check()
05368 sat
05369 >>> m = s.model()
05370 >>> m[x]
05371 1
05372 >>> m[f]
05373 [1 -> 0, else -> 0]
05374 """
05375 if __debug__:
05376 _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected")
05377 if is_const(decl):
05378 decl = decl.decl()
05379 try:
05380 if decl.arity() == 0:
05381 r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
05382 if is_as_array(r):
05383 return self.get_interp(get_as_array_func(r))
05384 else:
05385 return r
05386 else:
05387 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
05388 except Z3Exception:
05389 return None
05390
05391 def num_sorts(self):
05392 """Return the number of unintepreted sorts that contain an interpretation in the model `self`.
05393
05394 >>> A = DeclareSort('A')
05395 >>> a, b = Consts('a b', A)
05396 >>> s = Solver()
05397 >>> s.add(a != b)
05398 >>> s.check()
05399 sat
05400 >>> m = s.model()
05401 >>> m.num_sorts()
05402 1
05403 """
05404 return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model))
05405
05406 def get_sort(self, idx):
05407 """Return the unintepreted sort at position `idx` < self.num_sorts().
05408
05409 >>> A = DeclareSort('A')
05410 >>> B = DeclareSort('B')
05411 >>> a1, a2 = Consts('a1 a2', A)
05412 >>> b1, b2 = Consts('b1 b2', B)
05413 >>> s = Solver()
05414 >>> s.add(a1 != a2, b1 != b2)
05415 >>> s.check()
05416 sat
05417 >>> m = s.model()
05418 >>> m.num_sorts()
05419 2
05420 >>> m.get_sort(0)
05421 A
05422 >>> m.get_sort(1)
05423 B
05424 """
05425 if idx >= self.num_sorts():
05426 raise IndexError
05427 return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx)
05428
05429 def sorts(self):
05430 """Return all uninterpreted sorts that have an interpretation in the model `self`.
05431
05432 >>> A = DeclareSort('A')
05433 >>> B = DeclareSort('B')
05434 >>> a1, a2 = Consts('a1 a2', A)
05435 >>> b1, b2 = Consts('b1 b2', B)
05436 >>> s = Solver()
05437 >>> s.add(a1 != a2, b1 != b2)
05438 >>> s.check()
05439 sat
05440 >>> m = s.model()
05441 >>> m.sorts()
05442 [A, B]
05443 """
05444 return [ self.get_sort(i) for i in range(self.num_sorts()) ]
05445
05446 def get_universe(self, s):
05447 """Return the intepretation for the uninterpreted sort `s` in the model `self`.
05448
05449 >>> A = DeclareSort('A')
05450 >>> a, b = Consts('a b', A)
05451 >>> s = Solver()
05452 >>> s.add(a != b)
05453 >>> s.check()
05454 sat
05455 >>> m = s.model()
05456 >>> m.get_universe(A)
05457 [A!val!0, A!val!1]
05458 """
05459 if __debug__:
05460 _z3_assert(isinstance(s, SortRef), "Z3 sort expected")
05461 try:
05462 return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx)
05463 except Z3Exception:
05464 return None
05465
05466 def __getitem__(self, idx):
05467 """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.
05468
05469 The elements can be retrieved using position or the actual declaration.
05470
05471 >>> f = Function('f', IntSort(), IntSort())
05472 >>> x = Int('x')
05473 >>> s = Solver()
05474 >>> s.add(x > 0, x < 2, f(x) == 0)
05475 >>> s.check()
05476 sat
05477 >>> m = s.model()
05478 >>> len(m)
05479 2
05480 >>> m[0]
05481 x
05482 >>> m[1]
05483 f
05484 >>> m[x]
05485 1
05486 >>> m[f]
05487 [1 -> 0, else -> 0]
05488 >>> for d in m: print("%s -> %s" % (d, m[d]))
05489 x -> 1
05490 f -> [1 -> 0, else -> 0]
05491 """
05492 if isinstance(idx, int):
05493 if idx >= len(self):
05494 raise IndexError
05495 num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
05496 if (idx < num_consts):
05497 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx)
05498 else:
05499 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx)
05500 if isinstance(idx, FuncDeclRef):
05501 return self.get_interp(idx)
05502 if is_const(idx):
05503 return self.get_interp(idx.decl())
05504 if isinstance(idx, SortRef):
05505 return self.get_universe(idx)
05506 if __debug__:
05507 _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected")
05508 return None
05509
05510 def decls(self):
05511 """Return a list with all symbols that have an interpreation in the model `self`.
05512 >>> f = Function('f', IntSort(), IntSort())
05513 >>> x = Int('x')
05514 >>> s = Solver()
05515 >>> s.add(x > 0, x < 2, f(x) == 0)
05516 >>> s.check()
05517 sat
05518 >>> m = s.model()
05519 >>> m.decls()
05520 [x, f]
05521 """
05522 r = []
05523 for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)):
05524 r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx))
05525 for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)):
05526 r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
05527 return r
05528
05529 def is_as_array(n):
05530 """Return true if n is a Z3 expression of the form (_ as-array f)."""
05531 return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
05532
05533 def get_as_array_func(n):
05534 """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
05535 if __debug__:
05536 _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
05537 return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
05538
05539 #########################################
05540 #
05541 # Statistics
05542 #
05543 #########################################
05544 class Statistics:
05545 """Statistics for `Solver.check()`."""
05546
05547 def __init__(self, stats, ctx):
05548 self.stats = stats
05549 self.ctx = ctx
05550 Z3_stats_inc_ref(self.ctx.ref(), self.stats)
05551
05552 def __del__(self):
05553 Z3_stats_dec_ref(self.ctx.ref(), self.stats)
05554
05555 def __repr__(self):
05556 if in_html_mode():
05557 out = io.StringIO()
05558 even = True
05559 out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
05560 for k, v in self:
05561 if even:
05562 out.write(u('<tr style="background-color:#CFCFCF">'))
05563 even = False
05564 else:
05565 out.write(u('<tr>'))
05566 even = True
05567 out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
05568 out.write(u('</table>'))
05569 return out.getvalue()
05570 else:
05571 return Z3_stats_to_string(self.ctx.ref(), self.stats)
05572
05573 def __len__(self):
05574 """Return the number of statistical counters.
05575
05576 >>> x = Int('x')
05577 >>> s = Then('simplify', 'nlsat').solver()
05578 >>> s.add(x > 0)
05579 >>> s.check()
05580 sat
05581 >>> st = s.statistics()
05582 >>> len(st)
05583 2
05584 """
05585 return int(Z3_stats_size(self.ctx.ref(), self.stats))
05586
05587 def __getitem__(self, idx):
05588 """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
05589
05590 >>> x = Int('x')
05591 >>> s = Then('simplify', 'nlsat').solver()
05592 >>> s.add(x > 0)
05593 >>> s.check()
05594 sat
05595 >>> st = s.statistics()
05596 >>> len(st)
05597 2
05598 >>> st[0]
05599 ('nlsat propagations', 2)
05600 >>> st[1]
05601 ('nlsat stages', 2)
05602 """
05603 if idx >= len(self):
05604 raise IndexError
05605 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
05606 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
05607 else:
05608 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
05609 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
05610
05611 def keys(self):
05612 """Return the list of statistical counters.
05613
05614 >>> x = Int('x')
05615 >>> s = Then('simplify', 'nlsat').solver()
05616 >>> s.add(x > 0)
05617 >>> s.check()
05618 sat
05619 >>> st = s.statistics()
05620 >>> st.keys()
05621 ['nlsat propagations', 'nlsat stages']
05622 """
05623 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
05624
05625 def get_key_value(self, key):
05626 """Return the value of a particular statistical counter.
05627
05628 >>> x = Int('x')
05629 >>> s = Then('simplify', 'nlsat').solver()
05630 >>> s.add(x > 0)
05631 >>> s.check()
05632 sat
05633 >>> st = s.statistics()
05634 >>> st.get_key_value('nlsat propagations')
05635 2
05636 """
05637 for idx in range(len(self)):
05638 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
05639 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
05640 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
05641 else:
05642 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
05643 raise Z3Exception("unknown key")
05644
05645 def __getattr__(self, name):
05646 """Access the value of statistical using attributes.
05647
05648 Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
05649 we should use '_' (e.g., 'nlsat_propagations').
05650
05651 >>> x = Int('x')
05652 >>> s = Then('simplify', 'nlsat').solver()
05653 >>> s.add(x > 0)
05654 >>> s.check()
05655 sat
05656 >>> st = s.statistics()
05657 >>> st.keys()
05658 ['nlsat propagations', 'nlsat stages']
05659 >>> st.nlsat_propagations
05660 2
05661 >>> st.nlsat_stages
05662 2
05663 """
05664 key = name.replace('_', ' ')
05665 try:
05666 return self.get_key_value(key)
05667 except Z3Exception:
05668 raise AttributeError
05669
05670 #########################################
05671 #
05672 # Solver
05673 #
05674 #########################################
05675 class CheckSatResult:
05676 """Represents the result of a satisfiability check: sat, unsat, unknown.
05677
05678 >>> s = Solver()
05679 >>> s.check()
05680 sat
05681 >>> r = s.check()
05682 >>> isinstance(r, CheckSatResult)
05683 True
05684 """
05685
05686 def __init__(self, r):
05687 self.r = r
05688
05689 def __eq__(self, other):
05690 return isinstance(other, CheckSatResult) and self.r == other.r
05691
05692 def __ne__(self, other):
05693 return not self.__eq__(other)
05694
05695 def __repr__(self):
05696 if in_html_mode():
05697 if self.r == Z3_L_TRUE:
05698 return "<b>sat</b>"
05699 elif self.r == Z3_L_FALSE:
05700 return "<b>unsat</b>"
05701 else:
05702 return "<b>unknown</b>"
05703 else:
05704 if self.r == Z3_L_TRUE:
05705 return "sat"
05706 elif self.r == Z3_L_FALSE:
05707 return "unsat"
05708 else:
05709 return "unknown"
05710
05711 sat = CheckSatResult(Z3_L_TRUE)
05712 unsat = CheckSatResult(Z3_L_FALSE)
05713 unknown = CheckSatResult(Z3_L_UNDEF)
05714
05715 class Solver(Z3PPObject):
05716 """Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc."""
05717
05718 def __init__(self, solver=None, ctx=None):
05719 assert solver == None or ctx != None
05720 self.ctx = _get_ctx(ctx)
05721 self.solver = None
05722 if solver == None:
05723 self.solver = Z3_mk_solver(self.ctx.ref())
05724 else:
05725 self.solver = solver
05726 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
05727
05728 def __del__(self):
05729 if self.solver != None:
05730 Z3_solver_dec_ref(self.ctx.ref(), self.solver)
05731
05732 def set(self, *args, **keys):
05733 """Set a configuration option. The method `help()` return a string containing all available options.
05734
05735 >>> s = Solver()
05736 >>>
05737 >>> s.set(mbqi=True)
05738 >>> s.set('MBQI', True)
05739 >>> s.set(':mbqi', True)
05740 """
05741 p = args2params(args, keys, self.ctx)
05742 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
05743
05744 def push(self):
05745 """Create a backtracking point.
05746
05747 >>> x = Int('x')
05748 >>> s = Solver()
05749 >>> s.add(x > 0)
05750 >>> s
05751 [x > 0]
05752 >>> s.push()
05753 >>> s.add(x < 1)
05754 >>> s
05755 [x > 0, x < 1]
05756 >>> s.check()
05757 unsat
05758 >>> s.pop()
05759 >>> s.check()
05760 sat
05761 >>> s
05762 [x > 0]
05763 """
05764 Z3_solver_push(self.ctx.ref(), self.solver)
05765
05766 def pop(self, num=1):
05767 """Backtrack \c num backtracking points.
05768
05769 >>> x = Int('x')
05770 >>> s = Solver()
05771 >>> s.add(x > 0)
05772 >>> s
05773 [x > 0]
05774 >>> s.push()
05775 >>> s.add(x < 1)
05776 >>> s
05777 [x > 0, x < 1]
05778 >>> s.check()
05779 unsat
05780 >>> s.pop()
05781 >>> s.check()
05782 sat
05783 >>> s
05784 [x > 0]
05785 """
05786 Z3_solver_pop(self.ctx.ref(), self.solver, num)
05787
05788 def reset(self):
05789 """Remove all asserted constraints and backtracking points created using `push()`.
05790
05791 >>> x = Int('x')
05792 >>> s = Solver()
05793 >>> s.add(x > 0)
05794 >>> s
05795 [x > 0]
05796 >>> s.reset()
05797 >>> s
05798 []
05799 """
05800 Z3_solver_reset(self.ctx.ref(), self.solver)
05801
05802 def assert_exprs(self, *args):
05803 """Assert constraints into the solver.
05804
05805 >>> x = Int('x')
05806 >>> s = Solver()
05807 >>> s.assert_exprs(x > 0, x < 2)
05808 >>> s
05809 [x > 0, x < 2]
05810 """
05811 args = _get_args(args)
05812 s = BoolSort(self.ctx)
05813 for arg in args:
05814 if isinstance(arg, Goal) or isinstance(arg, AstVector):
05815 for f in arg:
05816 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
05817 else:
05818 arg = s.cast(arg)
05819 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
05820
05821 def add(self, *args):
05822 """Assert constraints into the solver.
05823
05824 >>> x = Int('x')
05825 >>> s = Solver()
05826 >>> s.add(x > 0, x < 2)
05827 >>> s
05828 [x > 0, x < 2]
05829 """
05830 self.assert_exprs(*args)
05831
05832 def append(self, *args):
05833 """Assert constraints into the solver.
05834
05835 >>> x = Int('x')
05836 >>> s = Solver()
05837 >>> s.append(x > 0, x < 2)
05838 >>> s
05839 [x > 0, x < 2]
05840 """
05841 self.assert_exprs(*args)
05842
05843 def insert(self, *args):
05844 """Assert constraints into the solver.
05845
05846 >>> x = Int('x')
05847 >>> s = Solver()
05848 >>> s.insert(x > 0, x < 2)
05849 >>> s
05850 [x > 0, x < 2]
05851 """
05852 self.assert_exprs(*args)
05853
05854 def assert_and_track(self, a, p):
05855 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
05856
05857 If `p` is a string, it will be automatically converted into a Boolean constant.
05858
05859 >>> x = Int('x')
05860 >>> p3 = Bool('p3')
05861 >>> s = Solver()
05862 >>> s.set(unsat_core=True)
05863 >>> s.assert_and_track(x > 0, 'p1')
05864 >>> s.assert_and_track(x != 1, 'p2')
05865 >>> s.assert_and_track(x < 0, p3)
05866 >>> print(s.check())
05867 unsat
05868 >>> c = s.unsat_core()
05869 >>> len(c)
05870 2
05871 >>> Bool('p1') in c
05872 True
05873 >>> Bool('p2') in c
05874 False
05875 >>> p3 in c
05876 True
05877 """
05878 if isinstance(p, str):
05879 p = Bool(p, self.ctx)
05880 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
05881 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
05882 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
05883
05884 def check(self, *assumptions):
05885 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
05886
05887 >>> x = Int('x')
05888 >>> s = Solver()
05889 >>> s.check()
05890 sat
05891 >>> s.add(x > 0, x < 2)
05892 >>> s.check()
05893 sat
05894 >>> s.model()
05895 [x = 1]
05896 >>> s.add(x < 1)
05897 >>> s.check()
05898 unsat
05899 >>> s.reset()
05900 >>> s.add(2**x == 4)
05901 >>> s.check()
05902 unknown
05903 """
05904 assumptions = _get_args(assumptions)
05905 num = len(assumptions)
05906 _assumptions = (Ast * num)()
05907 for i in range(num):
05908 _assumptions[i] = assumptions[i].as_ast()
05909 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
05910 return CheckSatResult(r)
05911
05912 def model(self):
05913 """Return a model for the last `check()`.
05914
05915 This function raises an exception if
05916 a model is not available (e.g., last `check()` returned unsat).
05917
05918 >>> s = Solver()
05919 >>> a = Int('a')
05920 >>> s.add(a + 2 == 0)
05921 >>> s.check()
05922 sat
05923 >>> s.model()
05924 [a = -2]
05925 """
05926 try:
05927 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
05928 except Z3Exception:
05929 raise Z3Exception("model is not available")
05930
05931 def unsat_core(self):
05932 """Return a subset (as an AST vector) of the assumptions provided to the last check().
05933
05934 These are the assumptions Z3 used in the unsatisfiability proof.
05935 Assumptions are available in Z3. They are used to extract unsatisfiable cores.
05936 They may be also used to "retract" assumptions. Note that, assumptions are not really
05937 "soft constraints", but they can be used to implement them.
05938
05939 >>> p1, p2, p3 = Bools('p1 p2 p3')
05940 >>> x, y = Ints('x y')
05941 >>> s = Solver()
05942 >>> s.add(Implies(p1, x > 0))
05943 >>> s.add(Implies(p2, y > x))
05944 >>> s.add(Implies(p2, y < 1))
05945 >>> s.add(Implies(p3, y > -3))
05946 >>> s.check(p1, p2, p3)
05947 unsat
05948 >>> core = s.unsat_core()
05949 >>> len(core)
05950 2
05951 >>> p1 in core
05952 True
05953 >>> p2 in core
05954 True
05955 >>> p3 in core
05956 False
05957 >>>
05958 >>> s.check(p1, p3)
05959 sat
05960 """
05961 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
05962
05963 def proof(self):
05964 """Return a proof for the last `check()`. Proof construction must be enabled."""
05965 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
05966
05967 def assertions(self):
05968 """Return an AST vector containing all added constraints.
05969
05970 >>> s = Solver()
05971 >>> s.assertions()
05972 []
05973 >>> a = Int('a')
05974 >>> s.add(a > 0)
05975 >>> s.add(a < 10)
05976 >>> s.assertions()
05977 [a > 0, a < 10]
05978 """
05979 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
05980
05981 def statistics(self):
05982 """Return statistics for the last `check()`.
05983
05984 >>> s = SimpleSolver()
05985 >>> x = Int('x')
05986 >>> s.add(x > 0)
05987 >>> s.check()
05988 sat
05989 >>> st = s.statistics()
05990 >>> st.get_key_value('final checks')
05991 1
05992 >>> len(st) > 0
05993 True
05994 >>> st[0] != 0
05995 True
05996 """
05997 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
05998
05999 def reason_unknown(self):
06000 """Return a string describing why the last `check()` returned `unknown`.
06001
06002 >>> x = Int('x')
06003 >>> s = SimpleSolver()
06004 >>> s.add(2**x == 4)
06005 >>> s.check()
06006 unknown
06007 >>> s.reason_unknown()
06008 '(incomplete (theory arithmetic))'
06009 """
06010 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
06011
06012 def help(self):
06013 """Display a string describing all available options."""
06014 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
06015
06016 def param_descrs(self):
06017 """Return the parameter description set."""
06018 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
06019
06020 def __repr__(self):
06021 """Return a formatted string with all added constraints."""
06022 return obj_to_string(self)
06023
06024 def sexpr(self):
06025 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
06026
06027 >>> x = Int('x')
06028 >>> s = Solver()
06029 >>> s.add(x > 0)
06030 >>> s.add(x < 2)
06031 >>> r = s.sexpr()
06032 """
06033 return Z3_solver_to_string(self.ctx.ref(), self.solver)
06034
06035 def to_smt2(self):
06036 """return SMTLIB2 formatted benchmark for solver's assertions"""
06037 es = self.assertions()
06038 sz = len(es)
06039 sz1 = sz
06040 if sz1 > 0:
06041 sz1 -= 1
06042 v = (Ast * sz1)()
06043 for i in range(sz1):
06044 v[i] = es[i].as_ast()
06045 if sz > 0:
06046 e = es[sz1].as_ast()
06047 else:
06048 e = BoolVal(True, self.ctx).as_ast()
06049 return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
06050
06051
06052
06053 def SolverFor(logic, ctx=None):
06054 """Create a solver customized for the given logic.
06055
06056 The parameter `logic` is a string. It should be contains
06057 the name of a SMT-LIB logic.
06058 See http://www.smtlib.org/ for the name of all available logics.
06059
06060 >>> s = SolverFor("QF_LIA")
06061 >>> x = Int('x')
06062 >>> s.add(x > 0)
06063 >>> s.add(x < 2)
06064 >>> s.check()
06065 sat
06066 >>> s.model()
06067 [x = 1]
06068 """
06069 ctx = _get_ctx(ctx)
06070 logic = to_symbol(logic)
06071 return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx)
06072
06073 def SimpleSolver(ctx=None):
06074 """Return a simple general purpose solver with limited amount of preprocessing.
06075
06076 >>> s = SimpleSolver()
06077 >>> x = Int('x')
06078 >>> s.add(x > 0)
06079 >>> s.check()
06080 sat
06081 """
06082 ctx = _get_ctx(ctx)
06083 return Solver(Z3_mk_simple_solver(ctx.ref()), ctx)
06084
06085
06086
06087
06088
06089
06090
06091 class Fixedpoint(Z3PPObject):
06092 """Fixedpoint API provides methods for solving with recursive predicates"""
06093
06094 def __init__(self, fixedpoint=None, ctx=None):
06095 assert fixedpoint == None or ctx != None
06096 self.ctx = _get_ctx(ctx)
06097 self.fixedpoint = None
06098 if fixedpoint == None:
06099 self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
06100 else:
06101 self.fixedpoint = fixedpoint
06102 Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
06103 self.vars = []
06104
06105 def __del__(self):
06106 if self.fixedpoint != None:
06107 Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
06108
06109 def set(self, *args, **keys):
06110 """Set a configuration option. The method `help()` return a string containing all available options.
06111 """
06112 p = args2params(args, keys, self.ctx)
06113 Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
06114
06115 def help(self):
06116 """Display a string describing all available options."""
06117 print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
06118
06119 def param_descrs(self):
06120 """Return the parameter description set."""
06121 return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
06122
06123 def assert_exprs(self, *args):
06124 """Assert constraints as background axioms for the fixedpoint solver."""
06125 args = _get_args(args)
06126 s = BoolSort(self.ctx)
06127 for arg in args:
06128 if isinstance(arg, Goal) or isinstance(arg, AstVector):
06129 for f in arg:
06130 f = self.abstract(f)
06131 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
06132 else:
06133 arg = s.cast(arg)
06134 arg = self.abstract(arg)
06135 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
06136
06137 def add(self, *args):
06138 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
06139 self.assert_exprs(*args)
06140
06141 def append(self, *args):
06142 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
06143 self.assert_exprs(*args)
06144
06145 def insert(self, *args):
06146 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
06147 self.assert_exprs(*args)
06148
06149 def add_rule(self, head, body = None, name = None):
06150 """Assert rules defining recursive predicates to the fixedpoint solver.
06151 >>> a = Bool('a')
06152 >>> b = Bool('b')
06153 >>> s = Fixedpoint()
06154 >>> s.register_relation(a.decl())
06155 >>> s.register_relation(b.decl())
06156 >>> s.fact(a)
06157 >>> s.rule(b, a)
06158 >>> s.query(b)
06159 sat
06160 """
06161 if name == None:
06162 name = ""
06163 name = to_symbol(name, self.ctx)
06164 if body == None:
06165 head = self.abstract(head)
06166 Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
06167 else:
06168 body = _get_args(body)
06169 f = self.abstract(Implies(And(body),head))
06170 Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
06171
06172 def rule(self, head, body = None, name = None):
06173 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
06174 self.add_rule(head, body, name)
06175
06176 def fact(self, head, name = None):
06177 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
06178 self.add_rule(head, None, name)
06179
06180 def query(self, *query):
06181 """Query the fixedpoint engine whether formula is derivable.
06182 You can also pass an tuple or list of recursive predicates.
06183 """
06184 query = _get_args(query)
06185 sz = len(query)
06186 if sz >= 1 and isinstance(query[0], FuncDecl):
06187 _decls = (FuncDecl * sz)()
06188 i = 0
06189 for q in query:
06190 _decls[i] = q.ast
06191 i = i + 1
06192 r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
06193 else:
06194 if sz == 1:
06195 query = query[0]
06196 else:
06197 query = And(query)
06198 query = self.abstract(query, False)
06199 r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
06200 return CheckSatResult(r)
06201
06202 def push(self):
06203 """create a backtracking point for added rules, facts and assertions"""
06204 Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint)
06205
06206 def pop(self):
06207 """restore to previously created backtracking point"""
06208 Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint)
06209
06210 def update_rule(self, head, body, name):
06211 """update rule"""
06212 if name == None:
06213 name = ""
06214 name = to_symbol(name, self.ctx)
06215 body = _get_args(body)
06216 f = self.abstract(Implies(And(body),head))
06217 Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
06218
06219 def get_answer(self):
06220 """Retrieve answer from last query call."""
06221 r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
06222 return _to_expr_ref(r, self.ctx)
06223
06224 def get_num_levels(self, predicate):
06225 """Retrieve number of levels used for predicate in PDR engine"""
06226 return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
06227
06228 def get_cover_delta(self, level, predicate):
06229 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
06230 r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
06231 return _to_expr_ref(r, self.ctx)
06232
06233 def add_cover(self, level, predicate, property):
06234 """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
06235 Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
06236
06237 def register_relation(self, *relations):
06238 """Register relation as recursive"""
06239 relations = _get_args(relations)
06240 for f in relations:
06241 Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
06242
06243 def set_predicate_representation(self, f, *representations):
06244 """Control how relation is represented"""
06245 representations = _get_args(representations)
06246 representations = [to_symbol(s) for s in representations]
06247 sz = len(representations)
06248 args = (Symbol * sz)()
06249 for i in range(sz):
06250 args[i] = representations[i]
06251 Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
06252
06253 def parse_string(self, s):
06254 """Parse rules and queries from a string"""
06255 return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
06256
06257 def parse_file(self, f):
06258 """Parse rules and queries from a file"""
06259 return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
06260
06261 def get_rules(self):
06262 """retrieve rules that have been added to fixedpoint context"""
06263 return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
06264
06265 def get_assertions(self):
06266 """retrieve assertions that have been added to fixedpoint context"""
06267 return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
06268
06269 def __repr__(self):
06270 """Return a formatted string with all added rules and constraints."""
06271 return self.sexpr()
06272
06273 def sexpr(self):
06274 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
06275 """
06276 return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
06277
06278 def to_string(self, queries):
06279 """Return a formatted string (in Lisp-like format) with all added constraints.
06280 We say the string is in s-expression format.
06281 Include also queries.
06282 """
06283 args, len = _to_ast_array(queries)
06284 return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
06285
06286 def statistics(self):
06287 """Return statistics for the last `query()`.
06288 """
06289 return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
06290
06291 def reason_unknown(self):
06292 """Return a string describing why the last `query()` returned `unknown`.
06293 """
06294 return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
06295
06296 def declare_var(self, *vars):
06297 """Add variable or several variables.
06298 The added variable or variables will be bound in the rules
06299 and queries
06300 """
06301 vars = _get_args(vars)
06302 for v in vars:
06303 self.vars += [v]
06304
06305 def abstract(self, fml, is_forall=True):
06306 if self.vars == []:
06307 return fml
06308 if is_forall:
06309 return ForAll(self.vars, fml)
06310 else:
06311 return Exists(self.vars, fml)
06312
06313
06314
06315
06316
06317
06318 class ApplyResult(Z3PPObject):
06319 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters."""
06320
06321 def __init__(self, result, ctx):
06322 self.result = result
06323 self.ctx = ctx
06324 Z3_apply_result_inc_ref(self.ctx.ref(), self.result)
06325
06326 def __del__(self):
06327 Z3_apply_result_dec_ref(self.ctx.ref(), self.result)
06328
06329 def __len__(self):
06330 """Return the number of subgoals in `self`.
06331
06332 >>> a, b = Ints('a b')
06333 >>> g = Goal()
06334 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
06335 >>> t = Tactic('split-clause')
06336 >>> r = t(g)
06337 >>> len(r)
06338 2
06339 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'))
06340 >>> len(t(g))
06341 4
06342 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values'))
06343 >>> len(t(g))
06344 1
06345 """
06346 return int(Z3_apply_result_get_num_subgoals(self.ctx.ref(), self.result))
06347
06348 def __getitem__(self, idx):
06349 """Return one of the subgoals stored in ApplyResult object `self`.
06350
06351 >>> a, b = Ints('a b')
06352 >>> g = Goal()
06353 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
06354 >>> t = Tactic('split-clause')
06355 >>> r = t(g)
06356 >>> r[0]
06357 [a == 0, Or(b == 0, b == 1), a > b]
06358 >>> r[1]
06359 [a == 1, Or(b == 0, b == 1), a > b]
06360 """
06361 if idx >= len(self):
06362 raise IndexError
06363 return Goal(goal=Z3_apply_result_get_subgoal(self.ctx.ref(), self.result, idx), ctx=self.ctx)
06364
06365 def __repr__(self):
06366 return obj_to_string(self)
06367
06368 def sexpr(self):
06369 """Return a textual representation of the s-expression representing the set of subgoals in `self`."""
06370 return Z3_apply_result_to_string(self.ctx.ref(), self.result)
06371
06372 def convert_model(self, model, idx=0):
06373 """Convert a model for a subgoal into a model for the original goal.
06374
06375 >>> a, b = Ints('a b')
06376 >>> g = Goal()
06377 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
06378 >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs'))
06379 >>> r = t(g)
06380 >>> r[0]
06381 [Or(b == 0, b == 1), Not(0 <= b)]
06382 >>> r[1]
06383 [Or(b == 0, b == 1), Not(1 <= b)]
06384 >>> # Remark: the subgoal r[0] is unsatisfiable
06385 >>> # Creating a solver for solving the second subgoal
06386 >>> s = Solver()
06387 >>> s.add(r[1])
06388 >>> s.check()
06389 sat
06390 >>> s.model()
06391 [b = 0]
06392 >>> # Model s.model() does not assign a value to `a`
06393 >>> # It is a model for subgoal `r[1]`, but not for goal `g`
06394 >>> # The method convert_model creates a model for `g` from a model for `r[1]`.
06395 >>> r.convert_model(s.model(), 1)
06396 [b = 0, a = 1]
06397 """
06398 if __debug__:
06399 _z3_assert(idx < len(self), "index out of bounds")
06400 _z3_assert(isinstance(model, ModelRef), "Z3 Model expected")
06401 return ModelRef(Z3_apply_result_convert_model(self.ctx.ref(), self.result, idx, model.model), self.ctx)
06402
06403 def as_expr(self):
06404 """Return a Z3 expression consisting of all subgoals.
06405
06406 >>> x = Int('x')
06407 >>> g = Goal()
06408 >>> g.add(x > 1)
06409 >>> g.add(Or(x == 2, x == 3))
06410 >>> r = Tactic('simplify')(g)
06411 >>> r
06412 [[Not(x <= 1), Or(x == 2, x == 3)]]
06413 >>> r.as_expr()
06414 And(Not(x <= 1), Or(x == 2, x == 3))
06415 >>> r = Tactic('split-clause')(g)
06416 >>> r
06417 [[x > 1, x == 2], [x > 1, x == 3]]
06418 >>> r.as_expr()
06419 Or(And(x > 1, x == 2), And(x > 1, x == 3))
06420 """
06421 sz = len(self)
06422 if sz == 0:
06423 return BoolVal(False, self.ctx)
06424 elif sz == 1:
06425 return self[0].as_expr()
06426 else:
06427 return Or([ self[i].as_expr() for i in range(len(self)) ])
06428
06429
06430
06431
06432
06433
06434 class Tactic:
06435 """Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver().
06436
06437 Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond().
06438 """
06439 def __init__(self, tactic, ctx=None):
06440 self.ctx = _get_ctx(ctx)
06441 self.tactic = None
06442 if isinstance(tactic, TacticObj):
06443 self.tactic = tactic
06444 else:
06445 if __debug__:
06446 _z3_assert(isinstance(tactic, str), "tactic name expected")
06447 try:
06448 self.tactic = Z3_mk_tactic(self.ctx.ref(), str(tactic))
06449 except Z3Exception:
06450 raise Z3Exception("unknown tactic '%s'" % tactic)
06451 Z3_tactic_inc_ref(self.ctx.ref(), self.tactic)
06452
06453 def __del__(self):
06454 if self.tactic != None:
06455 Z3_tactic_dec_ref(self.ctx.ref(), self.tactic)
06456
06457 def solver(self):
06458 """Create a solver using the tactic `self`.
06459
06460 The solver supports the methods `push()` and `pop()`, but it
06461 will always solve each `check()` from scratch.
06462
06463 >>> t = Then('simplify', 'nlsat')
06464 >>> s = t.solver()
06465 >>> x = Real('x')
06466 >>> s.add(x**2 == 2, x > 0)
06467 >>> s.check()
06468 sat
06469 >>> s.model()
06470 [x = 1.4142135623?]
06471 """
06472 return Solver(Z3_mk_solver_from_tactic(self.ctx.ref(), self.tactic), self.ctx)
06473
06474 def apply(self, goal, *arguments, **keywords):
06475 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
06476
06477 >>> x, y = Ints('x y')
06478 >>> t = Tactic('solve-eqs')
06479 >>> t.apply(And(x == 0, y >= x + 1))
06480 [[y >= 1]]
06481 """
06482 if __debug__:
06483 _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expressions expected")
06484 goal = _to_goal(goal)
06485 if len(arguments) > 0 or len(keywords) > 0:
06486 p = args2params(arguments, keywords, self.ctx)
06487 return ApplyResult(Z3_tactic_apply_ex(self.ctx.ref(), self.tactic, goal.goal, p.params), self.ctx)
06488 else:
06489 return ApplyResult(Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
06490
06491 def __call__(self, goal, *arguments, **keywords):
06492 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
06493
06494 >>> x, y = Ints('x y')
06495 >>> t = Tactic('solve-eqs')
06496 >>> t(And(x == 0, y >= x + 1))
06497 [[y >= 1]]
06498 """
06499 return self.apply(goal, *arguments, **keywords)
06500
06501 def help(self):
06502 """Display a string containing a description of the available options for the `self` tactic."""
06503 print(Z3_tactic_get_help(self.ctx.ref(), self.tactic))
06504
06505 def param_descrs(self):
06506 """Return the parameter description set."""
06507 return ParamDescrsRef(Z3_tactic_get_param_descrs(self.ctx.ref(), self.tactic), self.ctx)
06508
06509 def _to_goal(a):
06510 if isinstance(a, BoolRef):
06511 goal = Goal(ctx = a.ctx)
06512 goal.add(a)
06513 return goal
06514 else:
06515 return a
06516
06517 def _to_tactic(t, ctx=None):
06518 if isinstance(t, Tactic):
06519 return t
06520 else:
06521 return Tactic(t, ctx)
06522
06523 def _and_then(t1, t2, ctx=None):
06524 t1 = _to_tactic(t1, ctx)
06525 t2 = _to_tactic(t2, ctx)
06526 if __debug__:
06527 _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
06528 return Tactic(Z3_tactic_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
06529
06530 def _or_else(t1, t2, ctx=None):
06531 t1 = _to_tactic(t1, ctx)
06532 t2 = _to_tactic(t2, ctx)
06533 if __debug__:
06534 _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
06535 return Tactic(Z3_tactic_or_else(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
06536
06537 def AndThen(*ts, **ks):
06538 """Return a tactic that applies the tactics in `*ts` in sequence.
06539
06540 >>> x, y = Ints('x y')
06541 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
06542 >>> t(And(x == 0, y > x + 1))
06543 [[Not(y <= 1)]]
06544 >>> t(And(x == 0, y > x + 1)).as_expr()
06545 Not(y <= 1)
06546 """
06547 if __debug__:
06548 _z3_assert(len(ts) >= 2, "At least two arguments expected")
06549 ctx = ks.get('ctx', None)
06550 num = len(ts)
06551 r = ts[0]
06552 for i in range(num - 1):
06553 r = _and_then(r, ts[i+1], ctx)
06554 return r
06555
06556 def Then(*ts, **ks):
06557 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
06558
06559 >>> x, y = Ints('x y')
06560 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
06561 >>> t(And(x == 0, y > x + 1))
06562 [[Not(y <= 1)]]
06563 >>> t(And(x == 0, y > x + 1)).as_expr()
06564 Not(y <= 1)
06565 """
06566 return AndThen(*ts, **ks)
06567
06568 def OrElse(*ts, **ks):
06569 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
06570
06571 >>> x = Int('x')
06572 >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
06573 >>> # Tactic split-clause fails if there is no clause in the given goal.
06574 >>> t(x == 0)
06575 [[x == 0]]
06576 >>> t(Or(x == 0, x == 1))
06577 [[x == 0], [x == 1]]
06578 """
06579 if __debug__:
06580 _z3_assert(len(ts) >= 2, "At least two arguments expected")
06581 ctx = ks.get('ctx', None)
06582 num = len(ts)
06583 r = ts[0]
06584 for i in range(num - 1):
06585 r = _or_else(r, ts[i+1], ctx)
06586 return r
06587
06588 def ParOr(*ts, **ks):
06589 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
06590
06591 >>> x = Int('x')
06592 >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
06593 >>> t(x + 1 == 2)
06594 [[x == 1]]
06595 """
06596 if __debug__:
06597 _z3_assert(len(ts) >= 2, "At least two arguments expected")
06598 ctx = _get_ctx(ks.get('ctx', None))
06599 ts = [ _to_tactic(t, ctx) for t in ts ]
06600 sz = len(ts)
06601 _args = (TacticObj * sz)()
06602 for i in range(sz):
06603 _args[i] = ts[i].tactic
06604 return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)
06605
06606 def ParThen(t1, t2, ctx=None):
06607 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
06608
06609 >>> x, y = Ints('x y')
06610 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
06611 >>> t(And(Or(x == 1, x == 2), y == x + 1))
06612 [[x == 1, y == 2], [x == 2, y == 3]]
06613 """
06614 t1 = _to_tactic(t1, ctx)
06615 t2 = _to_tactic(t2, ctx)
06616 if __debug__:
06617 _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
06618 return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
06619
06620 def ParAndThen(t1, t2, ctx=None):
06621 """Alias for ParThen(t1, t2, ctx)."""
06622 return ParThen(t1, t2, ctx)
06623
06624 def With(t, *args, **keys):
06625 """Return a tactic that applies tactic `t` using the given configuration options.
06626
06627 >>> x, y = Ints('x y')
06628 >>> t = With(Tactic('simplify'), som=True)
06629 >>> t((x + 1)*(y + 2) == 0)
06630 [[2*x + y + x*y == -2]]
06631 """
06632 ctx = keys.get('ctx', None)
06633 t = _to_tactic(t, ctx)
06634 p = args2params(args, keys, t.ctx)
06635 return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
06636
06637 def Repeat(t, max=4294967295, ctx=None):
06638 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
06639
06640 >>> x, y = Ints('x y')
06641 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
06642 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
06643 >>> r = t(c)
06644 >>> for subgoal in r: print(subgoal)
06645 [x == 0, y == 0, x > y]
06646 [x == 0, y == 1, x > y]
06647 [x == 1, y == 0, x > y]
06648 [x == 1, y == 1, x > y]
06649 >>> t = Then(t, Tactic('propagate-values'))
06650 >>> t(c)
06651 [[x == 1, y == 0]]
06652 """
06653 t = _to_tactic(t, ctx)
06654 return Tactic(Z3_tactic_repeat(t.ctx.ref(), t.tactic, max), t.ctx)
06655
06656 def TryFor(t, ms, ctx=None):
06657 """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
06658
06659 If `t` does not terminate in `ms` milliseconds, then it fails.
06660 """
06661 t = _to_tactic(t, ctx)
06662 return Tactic(Z3_tactic_try_for(t.ctx.ref(), t.tactic, ms), t.ctx)
06663
06664 def tactics(ctx=None):
06665 """Return a list of all available tactics in Z3.
06666
06667 >>> l = tactics()
06668 >>> l.count('simplify') == 1
06669 True
06670 """
06671 ctx = _get_ctx(ctx)
06672 return [ Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref())) ]
06673
06674 def tactic_description(name, ctx=None):
06675 """Return a short description for the tactic named `name`.
06676
06677 >>> d = tactic_description('simplify')
06678 """
06679 ctx = _get_ctx(ctx)
06680 return Z3_tactic_get_descr(ctx.ref(), name)
06681
06682 def describe_tactics():
06683 """Display a (tabular) description of all available tactics in Z3."""
06684 if in_html_mode():
06685 even = True
06686 print('<table border="1" cellpadding="2" cellspacing="0">')
06687 for t in tactics():
06688 if even:
06689 print('<tr style="background-color:#CFCFCF">')
06690 even = False
06691 else:
06692 print('<tr>')
06693 even = True
06694 print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
06695 print('</table>')
06696 else:
06697 for t in tactics():
06698 print('%s : %s' % (t, tactic_description(t)))
06699
06700 class Probe:
06701 """Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used."""
06702 def __init__(self, probe, ctx=None):
06703 self.ctx = _get_ctx(ctx)
06704 self.probe = None
06705 if isinstance(probe, ProbeObj):
06706 self.probe = probe
06707 elif isinstance(probe, float):
06708 self.probe = Z3_probe_const(self.ctx.ref(), probe)
06709 elif _is_int(probe):
06710 self.probe = Z3_probe_const(self.ctx.ref(), float(probe))
06711 elif isinstance(probe, bool):
06712 if probe:
06713 self.probe = Z3_probe_const(self.ctx.ref(), 1.0)
06714 else:
06715 self.probe = Z3_probe_const(self.ctx.ref(), 0.0)
06716 else:
06717 if __debug__:
06718 _z3_assert(isinstance(probe, str), "probe name expected")
06719 try:
06720 self.probe = Z3_mk_probe(self.ctx.ref(), probe)
06721 except Z3Exception:
06722 raise Z3Exception("unknown probe '%s'" % probe)
06723 Z3_probe_inc_ref(self.ctx.ref(), self.probe)
06724
06725 def __del__(self):
06726 if self.probe != None:
06727 Z3_probe_dec_ref(self.ctx.ref(), self.probe)
06728
06729 def __lt__(self, other):
06730 """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`.
06731
06732 >>> p = Probe('size') < 10
06733 >>> x = Int('x')
06734 >>> g = Goal()
06735 >>> g.add(x > 0)
06736 >>> g.add(x < 10)
06737 >>> p(g)
06738 1.0
06739 """
06740 return Probe(Z3_probe_lt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
06741
06742 def __gt__(self, other):
06743 """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`.
06744
06745 >>> p = Probe('size') > 10
06746 >>> x = Int('x')
06747 >>> g = Goal()
06748 >>> g.add(x > 0)
06749 >>> g.add(x < 10)
06750 >>> p(g)
06751 0.0
06752 """
06753 return Probe(Z3_probe_gt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
06754
06755 def __le__(self, other):
06756 """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`.
06757
06758 >>> p = Probe('size') <= 2
06759 >>> x = Int('x')
06760 >>> g = Goal()
06761 >>> g.add(x > 0)
06762 >>> g.add(x < 10)
06763 >>> p(g)
06764 1.0
06765 """
06766 return Probe(Z3_probe_le(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
06767
06768 def __ge__(self, other):
06769 """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`.
06770
06771 >>> p = Probe('size') >= 2
06772 >>> x = Int('x')
06773 >>> g = Goal()
06774 >>> g.add(x > 0)
06775 >>> g.add(x < 10)
06776 >>> p(g)
06777 1.0
06778 """
06779 return Probe(Z3_probe_ge(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
06780
06781 def __eq__(self, other):
06782 """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`.
06783
06784 >>> p = Probe('size') == 2
06785 >>> x = Int('x')
06786 >>> g = Goal()
06787 >>> g.add(x > 0)
06788 >>> g.add(x < 10)
06789 >>> p(g)
06790 1.0
06791 """
06792 return Probe(Z3_probe_eq(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
06793
06794 def __ne__(self, other):
06795 """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`.
06796
06797 >>> p = Probe('size') != 2
06798 >>> x = Int('x')
06799 >>> g = Goal()
06800 >>> g.add(x > 0)
06801 >>> g.add(x < 10)
06802 >>> p(g)
06803 0.0
06804 """
06805 p = self.__eq__(other)
06806 return Probe(Z3_probe_not(self.ctx.ref(), p.probe), self.ctx)
06807
06808 def __call__(self, goal):
06809 """Evaluate the probe `self` in the given goal.
06810
06811 >>> p = Probe('size')
06812 >>> x = Int('x')
06813 >>> g = Goal()
06814 >>> g.add(x > 0)
06815 >>> g.add(x < 10)
06816 >>> p(g)
06817 2.0
06818 >>> g.add(x < 20)
06819 >>> p(g)
06820 3.0
06821 >>> p = Probe('num-consts')
06822 >>> p(g)
06823 1.0
06824 >>> p = Probe('is-propositional')
06825 >>> p(g)
06826 0.0
06827 >>> p = Probe('is-qflia')
06828 >>> p(g)
06829 1.0
06830 """
06831 if __debug__:
06832 _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expression expected")
06833 goal = _to_goal(goal)
06834 return Z3_probe_apply(self.ctx.ref(), self.probe, goal.goal)
06835
06836 def is_probe(p):
06837 """Return `True` if `p` is a Z3 probe.
06838
06839 >>> is_probe(Int('x'))
06840 False
06841 >>> is_probe(Probe('memory'))
06842 True
06843 """
06844 return isinstance(p, Probe)
06845
06846 def _to_probe(p, ctx=None):
06847 if is_probe(p):
06848 return p
06849 else:
06850 return Probe(p, ctx)
06851
06852 def probes(ctx=None):
06853 """Return a list of all available probes in Z3.
06854
06855 >>> l = probes()
06856 >>> l.count('memory') == 1
06857 True
06858 """
06859 ctx = _get_ctx(ctx)
06860 return [ Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref())) ]
06861
06862 def probe_description(name, ctx=None):
06863 """Return a short description for the probe named `name`.
06864
06865 >>> d = probe_description('memory')
06866 """
06867 ctx = _get_ctx(ctx)
06868 return Z3_probe_get_descr(ctx.ref(), name)
06869
06870 def describe_probes():
06871 """Display a (tabular) description of all available probes in Z3."""
06872 if in_html_mode():
06873 even = True
06874 print('<table border="1" cellpadding="2" cellspacing="0">')
06875 for p in probes():
06876 if even:
06877 print('<tr style="background-color:#CFCFCF">')
06878 even = False
06879 else:
06880 print('<tr>')
06881 even = True
06882 print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
06883 print('</table>')
06884 else:
06885 for p in probes():
06886 print('%s : %s' % (p, probe_description(p)))
06887
06888 def _probe_nary(f, args, ctx):
06889 if __debug__:
06890 _z3_assert(len(args) > 0, "At least one argument expected")
06891 num = len(args)
06892 r = _to_probe(args[0], ctx)
06893 for i in range(num - 1):
06894 r = Probe(f(ctx.ref(), r.probe, _to_probe(args[i+1], ctx).probe), ctx)
06895 return r
06896
06897 def _probe_and(args, ctx):
06898 return _probe_nary(Z3_probe_and, args, ctx)
06899
06900 def _probe_or(args, ctx):
06901 return _probe_nary(Z3_probe_or, args, ctx)
06902
06903 def FailIf(p, ctx=None):
06904 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
06905
06906 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
06907
06908 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
06909 >>> x, y = Ints('x y')
06910 >>> g = Goal()
06911 >>> g.add(x > 0)
06912 >>> g.add(y > 0)
06913 >>> t(g)
06914 [[x > 0, y > 0]]
06915 >>> g.add(x == y + 1)
06916 >>> t(g)
06917 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
06918 """
06919 p = _to_probe(p, ctx)
06920 return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
06921
06922 def When(p, t, ctx=None):
06923 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
06924
06925 >>> t = When(Probe('size') > 2, Tactic('simplify'))
06926 >>> x, y = Ints('x y')
06927 >>> g = Goal()
06928 >>> g.add(x > 0)
06929 >>> g.add(y > 0)
06930 >>> t(g)
06931 [[x > 0, y > 0]]
06932 >>> g.add(x == y + 1)
06933 >>> t(g)
06934 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
06935 """
06936 p = _to_probe(p, ctx)
06937 t = _to_tactic(t, ctx)
06938 return Tactic(Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)
06939
06940 def Cond(p, t1, t2, ctx=None):
06941 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
06942
06943 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
06944 """
06945 p = _to_probe(p, ctx)
06946 t1 = _to_tactic(t1, ctx)
06947 t2 = _to_tactic(t2, ctx)
06948 return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
06949
06950
06951
06952
06953
06954
06955
06956 def simplify(a, *arguments, **keywords):
06957 """Simplify the expression `a` using the given options.
06958
06959 This function has many options. Use `help_simplify` to obtain the complete list.
06960
06961 >>> x = Int('x')
06962 >>> y = Int('y')
06963 >>> simplify(x + 1 + y + x + 1)
06964 2 + 2*x + y
06965 >>> simplify((x + 1)*(y + 1), som=True)
06966 1 + x + y + x*y
06967 >>> simplify(Distinct(x, y, 1), blast_distinct=True)
06968 And(Not(x == y), Not(x == 1), Not(y == 1))
06969 >>> simplify(And(x == 0, y == 1), elim_and=True)
06970 Not(Or(Not(x == 0), Not(y == 1)))
06971 """
06972 if __debug__:
06973 _z3_assert(is_expr(a), "Z3 expression expected")
06974 if len(arguments) > 0 or len(keywords) > 0:
06975 p = args2params(arguments, keywords, a.ctx)
06976 return _to_expr_ref(Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
06977 else:
06978 return _to_expr_ref(Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
06979
06980 def help_simplify():
06981 """Return a string describing all options available for Z3 `simplify` procedure."""
06982 print(Z3_simplify_get_help(main_ctx().ref()))
06983
06984 def simplify_param_descrs():
06985 """Return the set of parameter descriptions for Z3 `simplify` procedure."""
06986 return ParamDescrsRef(Z3_simplify_get_param_descrs(main_ctx().ref()), main_ctx())
06987
06988 def substitute(t, *m):
06989 """Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to.
06990
06991 >>> x = Int('x')
06992 >>> y = Int('y')
06993 >>> substitute(x + 1, (x, y + 1))
06994 y + 1 + 1
06995 >>> f = Function('f', IntSort(), IntSort())
06996 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
06997 1 + 1
06998 """
06999 if isinstance(m, tuple):
07000 m1 = _get_args(m)
07001 if isinstance(m1, list):
07002 m = m1
07003 if __debug__:
07004 _z3_assert(is_expr(t), "Z3 expression expected")
07005 _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
07006 num = len(m)
07007 _from = (Ast * num)()
07008 _to = (Ast * num)()
07009 for i in range(num):
07010 _from[i] = m[i][0].as_ast()
07011 _to[i] = m[i][1].as_ast()
07012 return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
07013
07014 def substitute_vars(t, *m):
07015 """Substitute the free variables in t with the expression in m.
07016
07017 >>> v0 = Var(0, IntSort())
07018 >>> v1 = Var(1, IntSort())
07019 >>> x = Int('x')
07020 >>> f = Function('f', IntSort(), IntSort(), IntSort())
07021 >>> # replace v0 with x+1 and v1 with x
07022 >>> substitute_vars(f(v0, v1), x + 1, x)
07023 f(x + 1, x)
07024 """
07025 if __debug__:
07026 _z3_assert(is_expr(t), "Z3 expression expected")
07027 _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.")
07028 num = len(m)
07029 _to = (Ast * num)()
07030 for i in range(num):
07031 _to[i] = m[i].as_ast()
07032 return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
07033
07034 def Sum(*args):
07035 """Create the sum of the Z3 expressions.
07036
07037 >>> a, b, c = Ints('a b c')
07038 >>> Sum(a, b, c)
07039 a + b + c
07040 >>> Sum([a, b, c])
07041 a + b + c
07042 >>> A = IntVector('a', 5)
07043 >>> Sum(A)
07044 a__0 + a__1 + a__2 + a__3 + a__4
07045 """
07046 args = _get_args(args)
07047 if __debug__:
07048 _z3_assert(len(args) > 0, "Non empty list of arguments expected")
07049 ctx = _ctx_from_ast_arg_list(args)
07050 if __debug__:
07051 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
07052 args = _coerce_expr_list(args, ctx)
07053 if is_bv(args[0]):
07054 return _reduce(lambda a, b: a + b, args, 0)
07055 else:
07056 _args, sz = _to_ast_array(args)
07057 return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx)
07058
07059 def Product(*args):
07060 """Create the product of the Z3 expressions.
07061
07062 >>> a, b, c = Ints('a b c')
07063 >>> Product(a, b, c)
07064 a*b*c
07065 >>> Product([a, b, c])
07066 a*b*c
07067 >>> A = IntVector('a', 5)
07068 >>> Product(A)
07069 a__0*a__1*a__2*a__3*a__4
07070 """
07071 args = _get_args(args)
07072 if __debug__:
07073 _z3_assert(len(args) > 0, "Non empty list of arguments expected")
07074 ctx = _ctx_from_ast_arg_list(args)
07075 if __debug__:
07076 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
07077 args = _coerce_expr_list(args, ctx)
07078 if is_bv(args[0]):
07079 return _reduce(lambda a, b: a * b, args, 1)
07080 else:
07081 _args, sz = _to_ast_array(args)
07082 return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
07083
07084 def solve(*args, **keywords):
07085 """Solve the constraints `*args`.
07086
07087 This is a simple function for creating demonstrations. It creates a solver,
07088 configure it using the options in `keywords`, adds the constraints
07089 in `args`, and invokes check.
07090
07091 >>> a = Int('a')
07092 >>> solve(a > 0, a < 2)
07093 [a = 1]
07094 """
07095 s = Solver()
07096 s.set(**keywords)
07097 s.add(*args)
07098 if keywords.get('show', False):
07099 print(s)
07100 r = s.check()
07101 if r == unsat:
07102 print("no solution")
07103 elif r == unknown:
07104 print("failed to solve")
07105 try:
07106 print(s.model())
07107 except Z3Exception:
07108 return
07109 else:
07110 print(s.model())
07111
07112 def solve_using(s, *args, **keywords):
07113 """Solve the constraints `*args` using solver `s`.
07114
07115 This is a simple function for creating demonstrations. It is similar to `solve`,
07116 but it uses the given solver `s`.
07117 It configures solver `s` using the options in `keywords`, adds the constraints
07118 in `args`, and invokes check.
07119 """
07120 if __debug__:
07121 _z3_assert(isinstance(s, Solver), "Solver object expected")
07122 s.set(**keywords)
07123 s.add(*args)
07124 if keywords.get('show', False):
07125 print("Problem:")
07126 print(s)
07127 r = s.check()
07128 if r == unsat:
07129 print("no solution")
07130 elif r == unknown:
07131 print("failed to solve")
07132 try:
07133 print(s.model())
07134 except Z3Exception:
07135 return
07136 else:
07137 if keywords.get('show', False):
07138 print("Solution:")
07139 print(s.model())
07140
07141 def prove(claim, **keywords):
07142 """Try to prove the given claim.
07143
07144 This is a simple function for creating demonstrations. It tries to prove
07145 `claim` by showing the negation is unsatisfiable.
07146
07147 >>> p, q = Bools('p q')
07148 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
07149 proved
07150 """
07151 if __debug__:
07152 _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
07153 s = Solver()
07154 s.set(**keywords)
07155 s.add(Not(claim))
07156 if keywords.get('show', False):
07157 print(s)
07158 r = s.check()
07159 if r == unsat:
07160 print("proved")
07161 elif r == unknown:
07162 print("failed to prove")
07163 print(s.model())
07164 else:
07165 print("counterexample")
07166 print(s.model())
07167
07168 def _solve_html(*args, **keywords):
07169 """Version of funcion `solve` used in RiSE4Fun."""
07170 s = Solver()
07171 s.set(**keywords)
07172 s.add(*args)
07173 if keywords.get('show', False):
07174 print("<b>Problem:</b>")
07175 print(s)
07176 r = s.check()
07177 if r == unsat:
07178 print("<b>no solution</b>")
07179 elif r == unknown:
07180 print("<b>failed to solve</b>")
07181 try:
07182 print(s.model())
07183 except Z3Exception:
07184 return
07185 else:
07186 if keywords.get('show', False):
07187 print("<b>Solution:</b>")
07188 print(s.model())
07189
07190 def _solve_using_html(s, *args, **keywords):
07191 """Version of funcion `solve_using` used in RiSE4Fun."""
07192 if __debug__:
07193 _z3_assert(isinstance(s, Solver), "Solver object expected")
07194 s.set(**keywords)
07195 s.add(*args)
07196 if keywords.get('show', False):
07197 print("<b>Problem:</b>")
07198 print(s)
07199 r = s.check()
07200 if r == unsat:
07201 print("<b>no solution</b>")
07202 elif r == unknown:
07203 print("<b>failed to solve</b>")
07204 try:
07205 print(s.model())
07206 except Z3Exception:
07207 return
07208 else:
07209 if keywords.get('show', False):
07210 print("<b>Solution:</b>")
07211 print(s.model())
07212
07213 def _prove_html(claim, **keywords):
07214 """Version of funcion `prove` used in RiSE4Fun."""
07215 if __debug__:
07216 _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
07217 s = Solver()
07218 s.set(**keywords)
07219 s.add(Not(claim))
07220 if keywords.get('show', False):
07221 print(s)
07222 r = s.check()
07223 if r == unsat:
07224 print("<b>proved</b>")
07225 elif r == unknown:
07226 print("<b>failed to prove</b>")
07227 print(s.model())
07228 else:
07229 print("<b>counterexample</b>")
07230 print(s.model())
07231
07232 def _dict2sarray(sorts, ctx):
07233 sz = len(sorts)
07234 _names = (Symbol * sz)()
07235 _sorts = (Sort * sz) ()
07236 i = 0
07237 for k in sorts:
07238 v = sorts[k]
07239 if __debug__:
07240 _z3_assert(isinstance(k, str), "String expected")
07241 _z3_assert(is_sort(v), "Z3 sort expected")
07242 _names[i] = to_symbol(k, ctx)
07243 _sorts[i] = v.ast
07244 i = i + 1
07245 return sz, _names, _sorts
07246
07247 def _dict2darray(decls, ctx):
07248 sz = len(decls)
07249 _names = (Symbol * sz)()
07250 _decls = (FuncDecl * sz) ()
07251 i = 0
07252 for k in decls:
07253 v = decls[k]
07254 if __debug__:
07255 _z3_assert(isinstance(k, str), "String expected")
07256 _z3_assert(is_func_decl(v) or is_const(v), "Z3 declaration or constant expected")
07257 _names[i] = to_symbol(k, ctx)
07258 if is_const(v):
07259 _decls[i] = v.decl().ast
07260 else:
07261 _decls[i] = v.ast
07262 i = i + 1
07263 return sz, _names, _decls
07264
07265 def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
07266 """Parse a string in SMT 2.0 format using the given sorts and decls.
07267
07268 The arguments sorts and decls are Python dictionaries used to initialize
07269 the symbol table used for the SMT 2.0 parser.
07270
07271 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
07272 And(x > 0, x < 10)
07273 >>> x, y = Ints('x y')
07274 >>> f = Function('f', IntSort(), IntSort())
07275 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
07276 x + f(y) > 0
07277 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
07278 a > 0
07279 """
07280 ctx = _get_ctx(ctx)
07281 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
07282 dsz, dnames, ddecls = _dict2darray(decls, ctx)
07283 return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
07284
07285 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
07286 """Parse a file in SMT 2.0 format using the given sorts and decls.
07287
07288 This function is similar to parse_smt2_string().
07289 """
07290 ctx = _get_ctx(ctx)
07291 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
07292 dsz, dnames, ddecls = _dict2darray(decls, ctx)
07293 return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
07294
07295 def Interpolant(a,ctx=None):
07296 """Create an interpolation operator.
07297
07298 The argument is an interpolation pattern (see tree_interpolant).
07299
07300 >>> x = Int('x')
07301 >>> print Interpolant(x>0)
07302 interp(x > 0)
07303 """
07304 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
07305 s = BoolSort(ctx)
07306 a = s.cast(a)
07307 return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)
07308
07309 def tree_interpolant(pat,p=None,ctx=None):
07310 """Compute interpolant for a tree of formulas.
07311
07312 The input is an interpolation pattern over a set of formulas C.
07313 The pattern pat is a formula combining the formulas in C using
07314 logical conjunction and the "interp" operator (see Interp). This
07315 interp operator is logically the identity operator. It marks the
07316 sub-formulas of the pattern for which interpolants should be
07317 computed. The interpolant is a map sigma from marked subformulas
07318 to formulas, such that, for each marked subformula phi of pat
07319 (where phi sigma is phi with sigma(psi) substituted for each
07320 subformula psi of phi such that psi in dom(sigma)):
07321
07322 1) phi sigma implies sigma(phi), and
07323
07324 2) sigma(phi) is in the common uninterpreted vocabulary between
07325 the formulas of C occurring in phi and those not occurring in
07326 phi
07327
07328 and moreover pat sigma implies false. In the simplest case
07329 an interpolant for the pattern "(and (interp A) B)" maps A
07330 to an interpolant for A /\ B.
07331
07332 The return value is a vector of formulas representing sigma. This
07333 vector contains sigma(phi) for each marked subformula of pat, in
07334 pre-order traversal. This means that subformulas of phi occur before phi
07335 in the vector. Also, subformulas that occur multiply in pat will
07336 occur multiply in the result vector.
07337
07338 If pat is satisfiable, raises an object of class ModelRef
07339 that represents a model of pat.
07340
07341 If parameters p are supplied, these are used in creating the
07342 solver that determines satisfiability.
07343
07344 >>> x = Int('x')
07345 >>> y = Int('y')
07346 >>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
07347 [Not(x >= 0), Not(y <= 2)]
07348
07349 >>> g = And(Interpolant(x<0),x<2)
07350 >>> try:
07351 ... print tree_interpolant(g).sexpr()
07352 ... except ModelRef as m:
07353 ... print m.sexpr()
07354 (define-fun x () Int
07355 (- 1))
07356 """
07357 f = pat
07358 ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
07359 ptr = (AstVectorObj * 1)()
07360 mptr = (Model * 1)()
07361 if p == None:
07362 p = ParamsRef(ctx)
07363 res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
07364 if res == Z3_L_FALSE:
07365 return AstVector(ptr[0],ctx)
07366 raise ModelRef(mptr[0], ctx)
07367
07368 def binary_interpolant(a,b,p=None,ctx=None):
07369 """Compute an interpolant for a binary conjunction.
07370
07371 If a & b is unsatisfiable, returns an interpolant for a & b.
07372 This is a formula phi such that
07373
07374 1) a implies phi
07375 2) b implies not phi
07376 3) All the uninterpreted symbols of phi occur in both a and b.
07377
07378 If a & b is satisfiable, raises an object of class ModelRef
07379 that represents a model of a &b.
07380
07381 If parameters p are supplied, these are used in creating the
07382 solver that determines satisfiability.
07383
07384 x = Int('x')
07385 print binary_interpolant(x<0,x>2)
07386 Not(x >= 0)
07387 """
07388 f = And(Interpolant(a),b)
07389 return tree_interpolant(f,p,ctx)[0]
07390
07391 def sequence_interpolant(v,p=None,ctx=None):
07392 """Compute interpolant for a sequence of formulas.
07393
07394 If len(v) == N, and if the conjunction of the formulas in v is
07395 unsatisfiable, the interpolant is a sequence of formulas w
07396 such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
07397
07398 1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
07399 2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
07400 and v[i+1]..v[n]
07401
07402 Requires len(v) >= 1.
07403
07404 If a & b is satisfiable, raises an object of class ModelRef
07405 that represents a model of a & b.
07406
07407 If parameters p are supplied, these are used in creating the
07408 solver that determines satisfiability.
07409
07410 >>> x = Int('x')
07411 >>> y = Int('y')
07412 >>> print sequence_interpolant([x < 0, y == x , y > 2])
07413 [Not(x >= 0), Not(y >= 0)]
07414 """
07415 f = v[0]
07416 for i in range(1,len(v)):
07417 f = And(Interpolant(f),v[i])
07418 return tree_interpolant(f,p,ctx)
07419