9 """Z3 is a high performance theorem prover developed at Microsoft Research.
11 Z3 is used in many applications such as: software/hardware verification and testing,
12 constraint solving, analysis of hybrid systems, security, biology (in silico analysis),
13 and geometrical problems.
16 Please send feedback, comments and/or corrections on the Issue tracker for
17 https://github.com/Z3prover/z3.git. Your comments are very valuable.
38 ... x = BitVec('x', 32)
40 ... # the expression x + y is type incorrect
42 ... except Z3Exception as ex:
43 ... print("failed: %s" % ex)
48 from .z3types
import *
49 from .z3consts
import *
50 from .z3printer
import *
51 from fractions
import Fraction
56 if sys.version_info.major >= 3:
57 from typing
import Iterable
67 if sys.version_info.major < 3:
69 return isinstance(v, (int, long))
72 return isinstance(v, int)
84 major = ctypes.c_uint(0)
85 minor = ctypes.c_uint(0)
86 build = ctypes.c_uint(0)
87 rev = ctypes.c_uint(0)
89 return "%s.%s.%s" % (major.value, minor.value, build.value)
93 major = ctypes.c_uint(0)
94 minor = ctypes.c_uint(0)
95 build = ctypes.c_uint(0)
96 rev = ctypes.c_uint(0)
98 return (major.value, minor.value, build.value, rev.value)
105 def _z3_assert(cond, msg):
107 raise Z3Exception(msg)
110 def _z3_check_cint_overflow(n, name):
111 _z3_assert(ctypes.c_int(n).value == n, name +
" is too large")
115 """Log interaction to a file. This function must be invoked immediately after init(). """
120 """Append user-defined string to interaction log. """
125 """Convert an integer or string into a Z3 symbol."""
132 def _symbol2py(ctx, s):
133 """Convert a Z3 symbol back into a Python object. """
146 if len(args) == 1
and (isinstance(args[0], tuple)
or isinstance(args[0], list)):
148 elif len(args) == 1
and (isinstance(args[0], set)
or isinstance(args[0], AstVector)):
149 return [arg
for arg
in args[0]]
158 def _get_args_ast_list(args):
160 if isinstance(args, (set, AstVector, tuple)):
161 return [arg
for arg
in args]
168 def _to_param_value(val):
169 if isinstance(val, bool):
170 return "true" if val
else "false"
181 """A Context manages all other Z3 objects, global configuration options, etc.
183 Z3Py uses a default global context. For most applications this is sufficient.
184 An application may use multiple Z3 contexts. Objects created in one context
185 cannot be used in another one. However, several objects may be "translated" from
186 one context to another. It is not safe to access Z3 objects from multiple threads.
187 The only exception is the method `interrupt()` that can be used to interrupt() a long
189 The initialization method receives global configuration options for the new context.
194 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
213 if Z3_del_context
is not None and self.
ownerowner:
219 """Return a reference to the actual C pointer to the Z3 context."""
223 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
225 This method can be invoked from a thread different from the one executing the
226 interruptible procedure.
231 """Return the global parameter description set."""
240 """Return a reference to the global Z3 context.
243 >>> x.ctx == main_ctx()
248 >>> x2 = Real('x', c)
255 if _main_ctx
is None:
272 """Set Z3 global (or module) parameters.
274 >>> set_param(precision=10)
277 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
281 if not set_pp_option(k, v):
296 """Reset all global (or module) parameters.
302 """Alias for 'set_param' for backward compatibility.
308 """Return the value of a Z3 global (or module) parameter
310 >>> get_param('nlsat.reorder')
313 ptr = (ctypes.c_char_p * 1)()
315 r = z3core._to_pystr(ptr[0])
317 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
329 """Superclass for all Z3 objects that have support for pretty printing."""
334 def _repr_html_(self):
335 in_html = in_html_mode()
338 set_html_mode(in_html)
343 """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions."""
347 self.
ctxctx = _get_ctx(ctx)
351 if self.
ctxctx.ref()
is not None and self.
astast
is not None and Z3_dec_ref
is not None:
356 return _to_ast_ref(self.
astast, self.
ctxctx)
359 return obj_to_string(self)
362 return obj_to_string(self)
365 return self.
eqeq(other)
368 return self.
hashhash()
378 elif is_eq(self)
and self.num_args() == 2:
379 return self.arg(0).
eq(self.arg(1))
381 raise Z3Exception(
"Symbolic expressions cannot be cast to concrete Boolean values.")
384 """Return a string representing the AST node in s-expression notation.
387 >>> ((x + 1)*x).sexpr()
393 """Return a pointer to the corresponding C Z3_ast object."""
397 """Return unique identifier for object. It can be used for hash-tables and maps."""
401 """Return a reference to the C context where this AST node is stored."""
402 return self.
ctxctx.ref()
405 """Return `True` if `self` and `other` are structurally identical.
412 >>> n1 = simplify(n1)
413 >>> n2 = simplify(n2)
418 _z3_assert(
is_ast(other),
"Z3 AST expected")
422 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
428 >>> # Nodes in different contexts can't be mixed.
429 >>> # However, we can translate nodes from one context to another.
430 >>> x.translate(c2) + y
434 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
441 """Return a hashcode for the `self`.
443 >>> n1 = simplify(Int('x') + 1)
444 >>> n2 = simplify(2 + Int('x') - 1)
445 >>> n1.hash() == n2.hash()
452 """Return `True` if `a` is an AST node.
456 >>> is_ast(IntVal(10))
460 >>> is_ast(BoolSort())
462 >>> is_ast(Function('f', IntSort(), IntSort()))
469 return isinstance(a, AstRef)
473 """Return `True` if `a` and `b` are structurally identical AST nodes.
483 >>> eq(simplify(x + 1), simplify(1 + x))
491 def _ast_kind(ctx, a):
497 def _ctx_from_ast_arg_list(args, default_ctx=None):
505 _z3_assert(ctx == a.ctx,
"Context mismatch")
511 def _ctx_from_ast_args(*args):
512 return _ctx_from_ast_arg_list(args)
515 def _to_func_decl_array(args):
517 _args = (FuncDecl * sz)()
519 _args[i] = args[i].as_func_decl()
523 def _to_ast_array(args):
527 _args[i] = args[i].as_ast()
531 def _to_ref_array(ref, args):
535 _args[i] = args[i].as_ast()
539 def _to_ast_ref(a, ctx):
540 k = _ast_kind(ctx, a)
542 return _to_sort_ref(a, ctx)
543 elif k == Z3_FUNC_DECL_AST:
544 return _to_func_decl_ref(a, ctx)
546 return _to_expr_ref(a, ctx)
555 def _sort_kind(ctx, s):
560 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node."""
569 """Return the Z3 internal kind of a sort.
570 This method can be used to test if `self` is one of the Z3 builtin sorts.
573 >>> b.kind() == Z3_BOOL_SORT
575 >>> b.kind() == Z3_INT_SORT
577 >>> A = ArraySort(IntSort(), IntSort())
578 >>> A.kind() == Z3_ARRAY_SORT
580 >>> A.kind() == Z3_INT_SORT
583 return _sort_kind(self.
ctxctx, self.
astast)
586 """Return `True` if `self` is a subsort of `other`.
588 >>> IntSort().subsort(RealSort())
594 """Try to cast `val` as an element of sort `self`.
596 This method is used in Z3Py to convert Python objects such as integers,
597 floats, longs and strings into Z3 expressions.
600 >>> RealSort().cast(x)
604 _z3_assert(
is_expr(val),
"Z3 expression expected")
605 _z3_assert(self.
eqeq(val.sort()),
"Sort mismatch")
609 """Return the name (string) of sort `self`.
611 >>> BoolSort().name()
613 >>> ArraySort(IntSort(), IntSort()).name()
619 """Return `True` if `self` and `other` are the same Z3 sort.
622 >>> p.sort() == BoolSort()
624 >>> p.sort() == IntSort()
632 """Return `True` if `self` and `other` are not the same Z3 sort.
635 >>> p.sort() != BoolSort()
637 >>> p.sort() != IntSort()
644 return AstRef.__hash__(self)
648 """Return `True` if `s` is a Z3 sort.
650 >>> is_sort(IntSort())
652 >>> is_sort(Int('x'))
654 >>> is_expr(Int('x'))
657 return isinstance(s, SortRef)
660 def _to_sort_ref(s, ctx):
662 _z3_assert(isinstance(s, Sort),
"Z3 Sort expected")
663 k = _sort_kind(ctx, s)
664 if k == Z3_BOOL_SORT:
666 elif k == Z3_INT_SORT
or k == Z3_REAL_SORT:
668 elif k == Z3_BV_SORT:
670 elif k == Z3_ARRAY_SORT:
672 elif k == Z3_DATATYPE_SORT:
674 elif k == Z3_FINITE_DOMAIN_SORT:
676 elif k == Z3_FLOATING_POINT_SORT:
678 elif k == Z3_ROUNDING_MODE_SORT:
680 elif k == Z3_RE_SORT:
682 elif k == Z3_SEQ_SORT:
684 elif k == Z3_CHAR_SORT:
690 return _to_sort_ref(
Z3_get_sort(ctx.ref(), a), ctx)
694 """Create a new uninterpreted sort named `name`.
696 If `ctx=None`, then the new sort is declared in the global Z3Py context.
698 >>> A = DeclareSort('A')
699 >>> a = Const('a', A)
700 >>> b = Const('b', A)
719 """Function declaration. Every constant and function have an associated declaration.
721 The declaration assigns a name, a sort (i.e., type), and for function
722 the sort (i.e., type) of each of its arguments. Note that, in Z3,
723 a constant is a function with 0 arguments.
736 """Return the name of the function declaration `self`.
738 >>> f = Function('f', IntSort(), IntSort())
741 >>> isinstance(f.name(), str)
747 """Return the number of arguments of a function declaration.
748 If `self` is a constant, then `self.arity()` is 0.
750 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
757 """Return the sort of the argument `i` of a function declaration.
758 This method assumes that `0 <= i < self.arity()`.
760 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
767 _z3_assert(i < self.
arityarity(),
"Index out of bounds")
771 """Return the sort of the range of a function declaration.
772 For constants, this is the sort of the constant.
774 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
781 """Return the internal kind of a function declaration.
782 It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
785 >>> d = (x + 1).decl()
786 >>> d.kind() == Z3_OP_ADD
788 >>> d.kind() == Z3_OP_MUL
796 result = [
None for i
in range(n)]
799 if k == Z3_PARAMETER_INT:
801 elif k == Z3_PARAMETER_DOUBLE:
803 elif k == Z3_PARAMETER_RATIONAL:
805 elif k == Z3_PARAMETER_SYMBOL:
807 elif k == Z3_PARAMETER_SORT:
809 elif k == Z3_PARAMETER_AST:
811 elif k == Z3_PARAMETER_FUNC_DECL:
818 """Create a Z3 application expression using the function `self`, and the given arguments.
820 The arguments must be Z3 expressions. This method assumes that
821 the sorts of the elements in `args` match the sorts of the
822 domain. Limited coercion is supported. For example, if
823 args[0] is a Python integer, and the function expects a Z3
824 integer, then the argument is automatically converted into a
827 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
835 args = _get_args(args)
838 _z3_assert(num == self.
arityarity(),
"Incorrect number of arguments to %s" % self)
839 _args = (Ast * num)()
844 tmp = self.
domaindomain(i).cast(args[i])
846 _args[i] = tmp.as_ast()
851 """Return `True` if `a` is a Z3 function declaration.
853 >>> f = Function('f', IntSort(), IntSort())
860 return isinstance(a, FuncDeclRef)
864 """Create a new Z3 uninterpreted function with the given sorts.
866 >>> f = Function('f', IntSort(), IntSort())
872 _z3_assert(len(sig) > 0,
"At least two arguments expected")
876 _z3_assert(
is_sort(rng),
"Z3 sort expected")
877 dom = (Sort * arity)()
878 for i
in range(arity):
880 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
887 """Create a new fresh Z3 uninterpreted function with the given sorts.
891 _z3_assert(len(sig) > 0,
"At least two arguments expected")
895 _z3_assert(
is_sort(rng),
"Z3 sort expected")
896 dom = (z3.Sort * arity)()
897 for i
in range(arity):
899 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
905 def _to_func_decl_ref(a, ctx):
910 """Create a new Z3 recursive with the given sorts."""
913 _z3_assert(len(sig) > 0,
"At least two arguments expected")
917 _z3_assert(
is_sort(rng),
"Z3 sort expected")
918 dom = (Sort * arity)()
919 for i
in range(arity):
921 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
928 """Set the body of a recursive function.
929 Recursive definitions can be simplified if they are applied to ground
932 >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
933 >>> n = Int('n', ctx)
934 >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
937 >>> s = Solver(ctx=ctx)
938 >>> s.add(fac(n) < 3)
941 >>> s.model().eval(fac(5))
947 args = _get_args(args)
951 _args[i] = args[i].ast
962 """Constraints, formulas and terms are expressions in Z3.
964 Expressions are ASTs. Every expression has a sort.
965 There are three main kinds of expressions:
966 function applications, quantifiers and bounded variables.
967 A constant is a function application with 0 arguments.
968 For quantifier free problems, all expressions are
969 function applications.
979 """Return the sort of expression `self`.
991 """Shorthand for `self.sort().kind()`.
993 >>> a = Array('a', IntSort(), IntSort())
994 >>> a.sort_kind() == Z3_ARRAY_SORT
996 >>> a.sort_kind() == Z3_INT_SORT
999 return self.
sortsort().kind()
1002 """Return a Z3 expression that represents the constraint `self == other`.
1004 If `other` is `None`, then this method simply returns `False`.
1015 a, b = _coerce_exprs(self, other)
1020 return AstRef.__hash__(self)
1023 """Return a Z3 expression that represents the constraint `self != other`.
1025 If `other` is `None`, then this method simply returns `True`.
1036 a, b = _coerce_exprs(self, other)
1037 _args, sz = _to_ast_array((a, b))
1044 """Return the Z3 function declaration associated with a Z3 application.
1046 >>> f = Function('f', IntSort(), IntSort())
1055 _z3_assert(
is_app(self),
"Z3 application expected")
1059 """Return the number of arguments of a Z3 application.
1063 >>> (a + b).num_args()
1065 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1071 _z3_assert(
is_app(self),
"Z3 application expected")
1075 """Return argument `idx` of the application `self`.
1077 This method assumes that `self` is a function application with at least `idx+1` arguments.
1081 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1091 _z3_assert(
is_app(self),
"Z3 application expected")
1092 _z3_assert(idx < self.
num_argsnum_args(),
"Invalid argument index")
1096 """Return a list containing the children of the given expression
1100 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1120 """inverse function to the serialize method on ExprRef.
1121 It is made available to make it easier for users to serialize expressions back and forth between
1122 strings. Solvers can be serialized using the 'sexpr()' method.
1126 if len(s.assertions()) != 1:
1127 raise Z3Exception(
"single assertion expected")
1128 fml = s.assertions()[0]
1129 if fml.num_args() != 1:
1130 raise Z3Exception(
"dummy function 'F' expected")
1133 def _to_expr_ref(a, ctx):
1134 if isinstance(a, Pattern):
1138 if k == Z3_QUANTIFIER_AST:
1141 if sk == Z3_BOOL_SORT:
1143 if sk == Z3_INT_SORT:
1144 if k == Z3_NUMERAL_AST:
1147 if sk == Z3_REAL_SORT:
1148 if k == Z3_NUMERAL_AST:
1150 if _is_algebraic(ctx, a):
1153 if sk == Z3_BV_SORT:
1154 if k == Z3_NUMERAL_AST:
1158 if sk == Z3_ARRAY_SORT:
1160 if sk == Z3_DATATYPE_SORT:
1162 if sk == Z3_FLOATING_POINT_SORT:
1163 if k == Z3_APP_AST
and _is_numeral(ctx, a):
1166 return FPRef(a, ctx)
1167 if sk == Z3_FINITE_DOMAIN_SORT:
1168 if k == Z3_NUMERAL_AST:
1172 if sk == Z3_ROUNDING_MODE_SORT:
1174 if sk == Z3_SEQ_SORT:
1176 if sk == Z3_CHAR_SORT:
1178 if sk == Z3_RE_SORT:
1179 return ReRef(a, ctx)
1183 def _coerce_expr_merge(s, a):
1196 _z3_assert(s1.ctx == s.ctx,
"context mismatch")
1197 _z3_assert(
False,
"sort mismatch")
1202 def _coerce_exprs(a, b, ctx=None):
1204 a = _py2expr(a, ctx)
1205 b = _py2expr(b, ctx)
1206 if isinstance(a, str)
and isinstance(b, SeqRef):
1208 if isinstance(b, str)
and isinstance(a, SeqRef):
1210 if isinstance(a, float)
and isinstance(b, ArithRef):
1212 if isinstance(b, float)
and isinstance(a, ArithRef):
1216 s = _coerce_expr_merge(s, a)
1217 s = _coerce_expr_merge(s, b)
1223 def _reduce(func, sequence, initial):
1225 for element
in sequence:
1226 result = func(result, element)
1230 def _coerce_expr_list(alist, ctx=None):
1237 alist = [_py2expr(a, ctx)
for a
in alist]
1238 s = _reduce(_coerce_expr_merge, alist,
None)
1239 return [s.cast(a)
for a
in alist]
1243 """Return `True` if `a` is a Z3 expression.
1250 >>> is_expr(IntSort())
1254 >>> is_expr(IntVal(1))
1257 >>> is_expr(ForAll(x, x >= 0))
1259 >>> is_expr(FPVal(1.0))
1262 return isinstance(a, ExprRef)
1266 """Return `True` if `a` is a Z3 function application.
1268 Note that, constants are function applications with 0 arguments.
1275 >>> is_app(IntSort())
1279 >>> is_app(IntVal(1))
1282 >>> is_app(ForAll(x, x >= 0))
1285 if not isinstance(a, ExprRef):
1287 k = _ast_kind(a.ctx, a)
1288 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
1292 """Return `True` if `a` is Z3 constant/variable expression.
1301 >>> is_const(IntVal(1))
1304 >>> is_const(ForAll(x, x >= 0))
1307 return is_app(a)
and a.num_args() == 0
1311 """Return `True` if `a` is variable.
1313 Z3 uses de-Bruijn indices for representing bound variables in
1321 >>> f = Function('f', IntSort(), IntSort())
1322 >>> # Z3 replaces x with bound variables when ForAll is executed.
1323 >>> q = ForAll(x, f(x) == x)
1329 >>> is_var(b.arg(1))
1332 return is_expr(a)
and _ast_kind(a.ctx, a) == Z3_VAR_AST
1336 """Return the de-Bruijn index of the Z3 bounded variable `a`.
1344 >>> f = Function('f', IntSort(), IntSort(), IntSort())
1345 >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1346 >>> q = ForAll([x, y], f(x, y) == x + y)
1348 f(Var(1), Var(0)) == Var(1) + Var(0)
1352 >>> v1 = b.arg(0).arg(0)
1353 >>> v2 = b.arg(0).arg(1)
1358 >>> get_var_index(v1)
1360 >>> get_var_index(v2)
1364 _z3_assert(
is_var(a),
"Z3 bound variable expected")
1369 """Return `True` if `a` is an application of the given kind `k`.
1373 >>> is_app_of(n, Z3_OP_ADD)
1375 >>> is_app_of(n, Z3_OP_MUL)
1378 return is_app(a)
and a.decl().kind() == k
1381 def If(a, b, c, ctx=None):
1382 """Create a Z3 if-then-else expression.
1386 >>> max = If(x > y, x, y)
1392 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1393 return Cond(a, b, c, ctx)
1395 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1398 b, c = _coerce_exprs(b, c, ctx)
1400 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1401 return _to_expr_ref(
Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1405 """Create a Z3 distinct expression.
1412 >>> Distinct(x, y, z)
1414 >>> simplify(Distinct(x, y, z))
1416 >>> simplify(Distinct(x, y, z), blast_distinct=True)
1417 And(Not(x == y), Not(x == z), Not(y == z))
1419 args = _get_args(args)
1420 ctx = _ctx_from_ast_arg_list(args)
1422 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1423 args = _coerce_expr_list(args, ctx)
1424 _args, sz = _to_ast_array(args)
1428 def _mk_bin(f, a, b):
1431 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1432 args[0] = a.as_ast()
1433 args[1] = b.as_ast()
1434 return f(a.ctx.ref(), 2, args)
1438 """Create a constant of the given sort.
1440 >>> Const('x', IntSort())
1444 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
1450 """Create several constants of the given sort.
1452 `names` is a string containing the names of all constants to be created.
1453 Blank spaces separate the names of different constants.
1455 >>> x, y, z = Consts('x y z', IntSort())
1459 if isinstance(names, str):
1460 names = names.split(
" ")
1461 return [
Const(name, sort)
for name
in names]
1465 """Create a fresh constant of a specified sort"""
1466 ctx = _get_ctx(sort.ctx)
1471 """Create a Z3 free variable. Free variables are used to create quantified formulas.
1472 A free variable with index n is bound when it occurs within the scope of n+1 quantified
1475 >>> Var(0, IntSort())
1477 >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1481 _z3_assert(
is_sort(s),
"Z3 sort expected")
1482 return _to_expr_ref(
Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1487 Create a real free variable. Free variables are used to create quantified formulas.
1488 They are also used to create polynomials.
1498 Create a list of Real free variables.
1499 The variables have ids: 0, 1, ..., n-1
1501 >>> x0, x1, x2, x3 = RealVarVector(4)
1518 """Try to cast `val` as a Boolean.
1520 >>> x = BoolSort().cast(True)
1530 if isinstance(val, bool):
1534 msg =
"True, False or Z3 Boolean expression expected. Received %s of type %s"
1535 _z3_assert(
is_expr(val), msg % (val, type(val)))
1536 if not self.
eqeq(val.sort()):
1537 _z3_assert(self.
eqeq(val.sort()),
"Value cannot be converted into a Z3 Boolean value")
1541 return isinstance(other, ArithSortRef)
1551 """All Boolean expressions are instances of this class."""
1560 """Create the Z3 expression `self * other`.
1562 if isinstance(other, int)
and other == 1:
1563 return If(self, 1, 0)
1564 if isinstance(other, int)
and other == 0:
1566 if isinstance(other, BoolRef):
1567 other =
If(other, 1, 0)
1568 return If(self, other, 0)
1572 """Return `True` if `a` is a Z3 Boolean expression.
1578 >>> is_bool(And(p, q))
1586 return isinstance(a, BoolRef)
1590 """Return `True` if `a` is the Z3 true expression.
1595 >>> is_true(simplify(p == p))
1600 >>> # True is a Python Boolean expression
1608 """Return `True` if `a` is the Z3 false expression.
1615 >>> is_false(BoolVal(False))
1622 """Return `True` if `a` is a Z3 and expression.
1624 >>> p, q = Bools('p q')
1625 >>> is_and(And(p, q))
1627 >>> is_and(Or(p, q))
1634 """Return `True` if `a` is a Z3 or expression.
1636 >>> p, q = Bools('p q')
1639 >>> is_or(And(p, q))
1646 """Return `True` if `a` is a Z3 implication expression.
1648 >>> p, q = Bools('p q')
1649 >>> is_implies(Implies(p, q))
1651 >>> is_implies(And(p, q))
1658 """Return `True` if `a` is a Z3 not expression.
1670 """Return `True` if `a` is a Z3 equality expression.
1672 >>> x, y = Ints('x y')
1680 """Return `True` if `a` is a Z3 distinct expression.
1682 >>> x, y, z = Ints('x y z')
1683 >>> is_distinct(x == y)
1685 >>> is_distinct(Distinct(x, y, z))
1692 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1696 >>> p = Const('p', BoolSort())
1699 >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1702 >>> is_bool(r(0, 1))
1710 """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1714 >>> is_true(BoolVal(True))
1718 >>> is_false(BoolVal(False))
1729 """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1741 """Return a tuple of Boolean constants.
1743 `names` is a single string containing all names separated by blank spaces.
1744 If `ctx=None`, then the global context is used.
1746 >>> p, q, r = Bools('p q r')
1747 >>> And(p, Or(q, r))
1751 if isinstance(names, str):
1752 names = names.split(
" ")
1753 return [
Bool(name, ctx)
for name
in names]
1757 """Return a list of Boolean constants of size `sz`.
1759 The constants are named using the given prefix.
1760 If `ctx=None`, then the global context is used.
1762 >>> P = BoolVector('p', 3)
1766 And(p__0, p__1, p__2)
1768 return [
Bool(
"%s__%s" % (prefix, i))
for i
in range(sz)]
1772 """Return a fresh Boolean constant in the given context using the given prefix.
1774 If `ctx=None`, then the global context is used.
1776 >>> b1 = FreshBool()
1777 >>> b2 = FreshBool()
1786 """Create a Z3 implies expression.
1788 >>> p, q = Bools('p q')
1792 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1800 """Create a Z3 Xor expression.
1802 >>> p, q = Bools('p q')
1805 >>> simplify(Xor(p, q))
1808 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1816 """Create a Z3 not expression or probe.
1821 >>> simplify(Not(Not(p)))
1824 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1841 def _has_probe(args):
1842 """Return `True` if one of the elements of the given collection is a Z3 probe."""
1850 """Create a Z3 and-expression or and-probe.
1852 >>> p, q, r = Bools('p q r')
1855 >>> P = BoolVector('p', 5)
1857 And(p__0, p__1, p__2, p__3, p__4)
1861 last_arg = args[len(args) - 1]
1862 if isinstance(last_arg, Context):
1863 ctx = args[len(args) - 1]
1864 args = args[:len(args) - 1]
1865 elif len(args) == 1
and isinstance(args[0], AstVector):
1867 args = [a
for a
in args[0]]
1870 args = _get_args(args)
1871 ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1873 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1874 if _has_probe(args):
1875 return _probe_and(args, ctx)
1877 args = _coerce_expr_list(args, ctx)
1878 _args, sz = _to_ast_array(args)
1883 """Create a Z3 or-expression or or-probe.
1885 >>> p, q, r = Bools('p q r')
1888 >>> P = BoolVector('p', 5)
1890 Or(p__0, p__1, p__2, p__3, p__4)
1894 last_arg = args[len(args) - 1]
1895 if isinstance(last_arg, Context):
1896 ctx = args[len(args) - 1]
1897 args = args[:len(args) - 1]
1898 elif len(args) == 1
and isinstance(args[0], AstVector):
1900 args = [a
for a
in args[0]]
1903 args = _get_args(args)
1904 ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1906 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1907 if _has_probe(args):
1908 return _probe_or(args, ctx)
1910 args = _coerce_expr_list(args, ctx)
1911 _args, sz = _to_ast_array(args)
1922 """Patterns are hints for quantifier instantiation.
1934 """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1936 >>> f = Function('f', IntSort(), IntSort())
1938 >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1940 ForAll(x, f(x) == 0)
1941 >>> q.num_patterns()
1943 >>> is_pattern(q.pattern(0))
1948 return isinstance(a, PatternRef)
1952 """Create a Z3 multi-pattern using the given expressions `*args`
1954 >>> f = Function('f', IntSort(), IntSort())
1955 >>> g = Function('g', IntSort(), IntSort())
1957 >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1959 ForAll(x, f(x) != g(x))
1960 >>> q.num_patterns()
1962 >>> is_pattern(q.pattern(0))
1965 MultiPattern(f(Var(0)), g(Var(0)))
1968 _z3_assert(len(args) > 0,
"At least one argument expected")
1969 _z3_assert(all([
is_expr(a)
for a
in args]),
"Z3 expressions expected")
1971 args, sz = _to_ast_array(args)
1975 def _to_pattern(arg):
1989 """Universally and Existentially quantified formulas."""
1998 """Return the Boolean sort or sort of Lambda."""
2004 """Return `True` if `self` is a universal quantifier.
2006 >>> f = Function('f', IntSort(), IntSort())
2008 >>> q = ForAll(x, f(x) == 0)
2011 >>> q = Exists(x, f(x) != 0)
2018 """Return `True` if `self` is an existential quantifier.
2020 >>> f = Function('f', IntSort(), IntSort())
2022 >>> q = ForAll(x, f(x) == 0)
2025 >>> q = Exists(x, f(x) != 0)
2032 """Return `True` if `self` is a lambda expression.
2034 >>> f = Function('f', IntSort(), IntSort())
2036 >>> q = Lambda(x, f(x))
2039 >>> q = Exists(x, f(x) != 0)
2046 """Return the Z3 expression `self[arg]`.
2049 _z3_assert(self.
is_lambdais_lambda(),
"quantifier should be a lambda expression")
2050 return _array_select(self, arg)
2053 """Return the weight annotation of `self`.
2055 >>> f = Function('f', IntSort(), IntSort())
2057 >>> q = ForAll(x, f(x) == 0)
2060 >>> q = ForAll(x, f(x) == 0, weight=10)
2067 """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
2069 >>> f = Function('f', IntSort(), IntSort())
2070 >>> g = Function('g', IntSort(), IntSort())
2072 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2073 >>> q.num_patterns()
2079 """Return a pattern (i.e., quantifier instantiation hints) in `self`.
2081 >>> f = Function('f', IntSort(), IntSort())
2082 >>> g = Function('g', IntSort(), IntSort())
2084 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2085 >>> q.num_patterns()
2093 _z3_assert(idx < self.
num_patternsnum_patterns(),
"Invalid pattern idx")
2097 """Return the number of no-patterns."""
2101 """Return a no-pattern."""
2103 _z3_assert(idx < self.
num_no_patternsnum_no_patterns(),
"Invalid no-pattern idx")
2107 """Return the expression being quantified.
2109 >>> f = Function('f', IntSort(), IntSort())
2111 >>> q = ForAll(x, f(x) == 0)
2118 """Return the number of variables bounded by this quantifier.
2120 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2123 >>> q = ForAll([x, y], f(x, y) >= x)
2130 """Return a string representing a name used when displaying the quantifier.
2132 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2135 >>> q = ForAll([x, y], f(x, y) >= x)
2142 _z3_assert(idx < self.
num_varsnum_vars(),
"Invalid variable idx")
2146 """Return the sort of a bound variable.
2148 >>> f = Function('f', IntSort(), RealSort(), IntSort())
2151 >>> q = ForAll([x, y], f(x, y) >= x)
2158 _z3_assert(idx < self.
num_varsnum_vars(),
"Invalid variable idx")
2162 """Return a list containing a single element self.body()
2164 >>> f = Function('f', IntSort(), IntSort())
2166 >>> q = ForAll(x, f(x) == 0)
2170 return [self.
bodybody()]
2174 """Return `True` if `a` is a Z3 quantifier.
2176 >>> f = Function('f', IntSort(), IntSort())
2178 >>> q = ForAll(x, f(x) == 0)
2179 >>> is_quantifier(q)
2181 >>> is_quantifier(f(x))
2184 return isinstance(a, QuantifierRef)
2187 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2189 _z3_assert(
is_bool(body)
or is_app(vs)
or (len(vs) > 0
and is_app(vs[0])),
"Z3 expression expected")
2190 _z3_assert(
is_const(vs)
or (len(vs) > 0
and all([
is_const(v)
for v
in vs])),
"Invalid bounded variable(s)")
2191 _z3_assert(all([
is_pattern(a)
or is_expr(a)
for a
in patterns]),
"Z3 patterns expected")
2192 _z3_assert(all([
is_expr(p)
for p
in no_patterns]),
"no patterns are Z3 expressions")
2203 _vs = (Ast * num_vars)()
2204 for i
in range(num_vars):
2206 _vs[i] = vs[i].as_ast()
2207 patterns = [_to_pattern(p)
for p
in patterns]
2208 num_pats = len(patterns)
2209 _pats = (Pattern * num_pats)()
2210 for i
in range(num_pats):
2211 _pats[i] = patterns[i].ast
2212 _no_pats, num_no_pats = _to_ast_array(no_patterns)
2218 num_no_pats, _no_pats,
2219 body.as_ast()), ctx)
2222 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2223 """Create a Z3 forall formula.
2225 The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2227 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2230 >>> ForAll([x, y], f(x, y) >= x)
2231 ForAll([x, y], f(x, y) >= x)
2232 >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2233 ForAll([x, y], f(x, y) >= x)
2234 >>> ForAll([x, y], f(x, y) >= x, weight=10)
2235 ForAll([x, y], f(x, y) >= x)
2237 return _mk_quantifier(
True, vs, body, weight, qid, skid, patterns, no_patterns)
2240 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2241 """Create a Z3 exists formula.
2243 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2246 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2249 >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2251 Exists([x, y], f(x, y) >= x)
2252 >>> is_quantifier(q)
2254 >>> r = Tactic('nnf')(q).as_expr()
2255 >>> is_quantifier(r)
2258 return _mk_quantifier(
False, vs, body, weight, qid, skid, patterns, no_patterns)
2262 """Create a Z3 lambda expression.
2264 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2265 >>> mem0 = Array('mem0', IntSort(), IntSort())
2266 >>> lo, hi, e, i = Ints('lo hi e i')
2267 >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
2269 Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
2275 _vs = (Ast * num_vars)()
2276 for i
in range(num_vars):
2278 _vs[i] = vs[i].as_ast()
2289 """Real and Integer sorts."""
2292 """Return `True` if `self` is of the sort Real.
2297 >>> (x + 1).is_real()
2303 return self.
kindkind() == Z3_REAL_SORT
2306 """Return `True` if `self` is of the sort Integer.
2311 >>> (x + 1).is_int()
2317 return self.
kindkind() == Z3_INT_SORT
2323 """Return `True` if `self` is a subsort of `other`."""
2327 """Try to cast `val` as an Integer or Real.
2329 >>> IntSort().cast(10)
2331 >>> is_int(IntSort().cast(10))
2335 >>> RealSort().cast(10)
2337 >>> is_real(RealSort().cast(10))
2342 _z3_assert(self.
ctxctxctx == val.ctx,
"Context mismatch")
2344 if self.
eqeq(val_s):
2346 if val_s.is_int()
and self.
is_realis_real():
2348 if val_s.is_bool()
and self.
is_intis_int():
2349 return If(val, 1, 0)
2350 if val_s.is_bool()
and self.
is_realis_real():
2353 _z3_assert(
False,
"Z3 Integer/Real expression expected")
2360 msg =
"int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s"
2361 _z3_assert(
False, msg % self)
2365 """Return `True` if s is an arithmetical sort (type).
2367 >>> is_arith_sort(IntSort())
2369 >>> is_arith_sort(RealSort())
2371 >>> is_arith_sort(BoolSort())
2373 >>> n = Int('x') + 1
2374 >>> is_arith_sort(n.sort())
2377 return isinstance(s, ArithSortRef)
2381 """Integer and Real expressions."""
2384 """Return the sort (type) of the arithmetical expression `self`.
2388 >>> (Real('x') + 1).sort()
2394 """Return `True` if `self` is an integer expression.
2399 >>> (x + 1).is_int()
2402 >>> (x + y).is_int()
2408 """Return `True` if `self` is an real expression.
2413 >>> (x + 1).is_real()
2419 """Create the Z3 expression `self + other`.
2428 a, b = _coerce_exprs(self, other)
2429 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.
ctxctx)
2432 """Create the Z3 expression `other + self`.
2438 a, b = _coerce_exprs(self, other)
2439 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.
ctxctx)
2442 """Create the Z3 expression `self * other`.
2451 if isinstance(other, BoolRef):
2452 return If(other, self, 0)
2453 a, b = _coerce_exprs(self, other)
2454 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.
ctxctx)
2457 """Create the Z3 expression `other * self`.
2463 a, b = _coerce_exprs(self, other)
2464 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.
ctxctx)
2467 """Create the Z3 expression `self - other`.
2476 a, b = _coerce_exprs(self, other)
2477 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.
ctxctx)
2480 """Create the Z3 expression `other - self`.
2486 a, b = _coerce_exprs(self, other)
2487 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.
ctxctx)
2490 """Create the Z3 expression `self**other` (** is the power operator).
2497 >>> simplify(IntVal(2)**8)
2500 a, b = _coerce_exprs(self, other)
2504 """Create the Z3 expression `other**self` (** is the power operator).
2511 >>> simplify(2**IntVal(8))
2514 a, b = _coerce_exprs(self, other)
2518 """Create the Z3 expression `other/self`.
2537 a, b = _coerce_exprs(self, other)
2541 """Create the Z3 expression `other/self`."""
2542 return self.
__div____div__(other)
2545 """Create the Z3 expression `other/self`.
2558 a, b = _coerce_exprs(self, other)
2562 """Create the Z3 expression `other/self`."""
2563 return self.
__rdiv____rdiv__(other)
2566 """Create the Z3 expression `other%self`.
2572 >>> simplify(IntVal(10) % IntVal(3))
2575 a, b = _coerce_exprs(self, other)
2577 _z3_assert(a.is_int(),
"Z3 integer expression expected")
2581 """Create the Z3 expression `other%self`.
2587 a, b = _coerce_exprs(self, other)
2589 _z3_assert(a.is_int(),
"Z3 integer expression expected")
2593 """Return an expression representing `-self`.
2613 """Create the Z3 expression `other <= self`.
2615 >>> x, y = Ints('x y')
2622 a, b = _coerce_exprs(self, other)
2626 """Create the Z3 expression `other < self`.
2628 >>> x, y = Ints('x y')
2635 a, b = _coerce_exprs(self, other)
2639 """Create the Z3 expression `other > self`.
2641 >>> x, y = Ints('x y')
2648 a, b = _coerce_exprs(self, other)
2652 """Create the Z3 expression `other >= self`.
2654 >>> x, y = Ints('x y')
2661 a, b = _coerce_exprs(self, other)
2666 """Return `True` if `a` is an arithmetical expression.
2675 >>> is_arith(IntVal(1))
2683 return isinstance(a, ArithRef)
2687 """Return `True` if `a` is an integer expression.
2694 >>> is_int(IntVal(1))
2706 """Return `True` if `a` is a real expression.
2718 >>> is_real(RealVal(1))
2724 def _is_numeral(ctx, a):
2728 def _is_algebraic(ctx, a):
2733 """Return `True` if `a` is an integer value of sort Int.
2735 >>> is_int_value(IntVal(1))
2739 >>> is_int_value(Int('x'))
2741 >>> n = Int('x') + 1
2746 >>> is_int_value(n.arg(1))
2748 >>> is_int_value(RealVal("1/3"))
2750 >>> is_int_value(RealVal(1))
2753 return is_arith(a)
and a.is_int()
and _is_numeral(a.ctx, a.as_ast())
2757 """Return `True` if `a` is rational value of sort Real.
2759 >>> is_rational_value(RealVal(1))
2761 >>> is_rational_value(RealVal("3/5"))
2763 >>> is_rational_value(IntVal(1))
2765 >>> is_rational_value(1)
2767 >>> n = Real('x') + 1
2770 >>> is_rational_value(n.arg(1))
2772 >>> is_rational_value(Real('x'))
2775 return is_arith(a)
and a.is_real()
and _is_numeral(a.ctx, a.as_ast())
2779 """Return `True` if `a` is an algebraic value of sort Real.
2781 >>> is_algebraic_value(RealVal("3/5"))
2783 >>> n = simplify(Sqrt(2))
2786 >>> is_algebraic_value(n)
2789 return is_arith(a)
and a.is_real()
and _is_algebraic(a.ctx, a.as_ast())
2793 """Return `True` if `a` is an expression of the form b + c.
2795 >>> x, y = Ints('x y')
2805 """Return `True` if `a` is an expression of the form b * c.
2807 >>> x, y = Ints('x y')
2817 """Return `True` if `a` is an expression of the form b - c.
2819 >>> x, y = Ints('x y')
2829 """Return `True` if `a` is an expression of the form b / c.
2831 >>> x, y = Reals('x y')
2836 >>> x, y = Ints('x y')
2846 """Return `True` if `a` is an expression of the form b div c.
2848 >>> x, y = Ints('x y')
2858 """Return `True` if `a` is an expression of the form b % c.
2860 >>> x, y = Ints('x y')
2870 """Return `True` if `a` is an expression of the form b <= c.
2872 >>> x, y = Ints('x y')
2882 """Return `True` if `a` is an expression of the form b < c.
2884 >>> x, y = Ints('x y')
2894 """Return `True` if `a` is an expression of the form b >= c.
2896 >>> x, y = Ints('x y')
2906 """Return `True` if `a` is an expression of the form b > c.
2908 >>> x, y = Ints('x y')
2918 """Return `True` if `a` is an expression of the form IsInt(b).
2921 >>> is_is_int(IsInt(x))
2930 """Return `True` if `a` is an expression of the form ToReal(b).
2945 """Return `True` if `a` is an expression of the form ToInt(b).
2960 """Integer values."""
2963 """Return a Z3 integer numeral as a Python long (bignum) numeral.
2972 _z3_assert(self.
is_intis_int(),
"Integer value expected")
2976 """Return a Z3 integer numeral as a Python string.
2984 """Return a Z3 integer numeral as a Python binary string.
2986 >>> v.as_binary_string()
2993 """Rational values."""
2996 """ Return the numerator of a Z3 rational numeral.
2998 >>> is_rational_value(RealVal("3/5"))
3000 >>> n = RealVal("3/5")
3003 >>> is_rational_value(Q(3,5))
3005 >>> Q(3,5).numerator()
3011 """ Return the denominator of a Z3 rational numeral.
3013 >>> is_rational_value(Q(3,5))
3022 """ Return the numerator as a Python long.
3024 >>> v = RealVal(10000000000)
3029 >>> v.numerator_as_long() + 1 == 10000000001
3035 """ Return the denominator as a Python long.
3037 >>> v = RealVal("1/3")
3040 >>> v.denominator_as_long()
3055 _z3_assert(self.
is_int_valueis_int_value(),
"Expected integer fraction")
3059 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
3061 >>> v = RealVal("1/5")
3064 >>> v = RealVal("1/3")
3071 """Return a Z3 rational numeral as a Python string.
3080 """Return a Z3 rational as a Python Fraction object.
3082 >>> v = RealVal("1/5")
3090 """Algebraic irrational values."""
3093 """Return a Z3 rational number that approximates the algebraic number `self`.
3094 The result `r` is such that |r - self| <= 1/10^precision
3096 >>> x = simplify(Sqrt(2))
3098 6838717160008073720548335/4835703278458516698824704
3105 """Return a string representation of the algebraic number `self` in decimal notation
3106 using `prec` decimal places.
3108 >>> x = simplify(Sqrt(2))
3109 >>> x.as_decimal(10)
3111 >>> x.as_decimal(20)
3112 '1.41421356237309504880?'
3123 def _py2expr(a, ctx=None):
3124 if isinstance(a, bool):
3128 if isinstance(a, float):
3130 if isinstance(a, str):
3135 _z3_assert(
False,
"Python bool, int, long or float expected")
3139 """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
3143 >>> x = Const('x', IntSort())
3146 >>> x.sort() == IntSort()
3148 >>> x.sort() == BoolSort()
3156 """Return the real sort in the given context. If `ctx=None`, then the global context is used.
3160 >>> x = Const('x', RealSort())
3165 >>> x.sort() == RealSort()
3172 def _to_int_str(val):
3173 if isinstance(val, float):
3174 return str(int(val))
3175 elif isinstance(val, bool):
3182 elif isinstance(val, str):
3185 _z3_assert(
False,
"Python value cannot be used as a Z3 integer")
3189 """Return a Z3 integer value. If `ctx=None`, then the global context is used.
3201 """Return a Z3 real value.
3203 `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
3204 If `ctx=None`, then the global context is used.
3208 >>> RealVal(1).sort()
3220 """Return a Z3 rational a/b.
3222 If `ctx=None`, then the global context is used.
3226 >>> RatVal(3,5).sort()
3230 _z3_assert(_is_int(a)
or isinstance(a, str),
"First argument cannot be converted into an integer")
3231 _z3_assert(_is_int(b)
or isinstance(b, str),
"Second argument cannot be converted into an integer")
3235 def Q(a, b, ctx=None):
3236 """Return a Z3 rational a/b.
3238 If `ctx=None`, then the global context is used.
3249 """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
3262 """Return a tuple of Integer constants.
3264 >>> x, y, z = Ints('x y z')
3269 if isinstance(names, str):
3270 names = names.split(
" ")
3271 return [
Int(name, ctx)
for name
in names]
3275 """Return a list of integer constants of size `sz`.
3277 >>> X = IntVector('x', 3)
3284 return [
Int(
"%s__%s" % (prefix, i), ctx)
for i
in range(sz)]
3288 """Return a fresh integer constant in the given context using the given prefix.
3302 """Return a real constant named `name`. If `ctx=None`, then the global context is used.
3315 """Return a tuple of real constants.
3317 >>> x, y, z = Reals('x y z')
3320 >>> Sum(x, y, z).sort()
3324 if isinstance(names, str):
3325 names = names.split(
" ")
3326 return [
Real(name, ctx)
for name
in names]
3330 """Return a list of real constants of size `sz`.
3332 >>> X = RealVector('x', 3)
3341 return [
Real(
"%s__%s" % (prefix, i), ctx)
for i
in range(sz)]
3345 """Return a fresh real constant in the given context using the given prefix.
3359 """ Return the Z3 expression ToReal(a).
3371 _z3_assert(a.is_int(),
"Z3 integer expression expected.")
3377 """ Return the Z3 expression ToInt(a).
3389 _z3_assert(a.is_real(),
"Z3 real expression expected.")
3395 """ Return the Z3 predicate IsInt(a).
3398 >>> IsInt(x + "1/2")
3400 >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
3402 >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
3406 _z3_assert(a.is_real(),
"Z3 real expression expected.")
3412 """ Return a Z3 expression which represents the square root of a.
3425 """ Return a Z3 expression which represents the cubic root of a.
3444 """Bit-vector sort."""
3447 """Return the size (number of bits) of the bit-vector sort `self`.
3449 >>> b = BitVecSort(32)
3459 """Try to cast `val` as a Bit-Vector.
3461 >>> b = BitVecSort(32)
3464 >>> b.cast(10).sexpr()
3469 _z3_assert(self.
ctxctxctx == val.ctx,
"Context mismatch")
3477 """Return True if `s` is a Z3 bit-vector sort.
3479 >>> is_bv_sort(BitVecSort(32))
3481 >>> is_bv_sort(IntSort())
3484 return isinstance(s, BitVecSortRef)
3488 """Bit-vector expressions."""
3491 """Return the sort of the bit-vector expression `self`.
3493 >>> x = BitVec('x', 32)
3496 >>> x.sort() == BitVecSort(32)
3502 """Return the number of bits of the bit-vector expression `self`.
3504 >>> x = BitVec('x', 32)
3507 >>> Concat(x, x).size()
3513 """Create the Z3 expression `self + other`.
3515 >>> x = BitVec('x', 32)
3516 >>> y = BitVec('y', 32)
3522 a, b = _coerce_exprs(self, other)
3526 """Create the Z3 expression `other + self`.
3528 >>> x = BitVec('x', 32)
3532 a, b = _coerce_exprs(self, other)
3536 """Create the Z3 expression `self * other`.
3538 >>> x = BitVec('x', 32)
3539 >>> y = BitVec('y', 32)
3545 a, b = _coerce_exprs(self, other)
3549 """Create the Z3 expression `other * self`.
3551 >>> x = BitVec('x', 32)
3555 a, b = _coerce_exprs(self, other)
3559 """Create the Z3 expression `self - other`.
3561 >>> x = BitVec('x', 32)
3562 >>> y = BitVec('y', 32)
3568 a, b = _coerce_exprs(self, other)
3572 """Create the Z3 expression `other - self`.
3574 >>> x = BitVec('x', 32)
3578 a, b = _coerce_exprs(self, other)
3582 """Create the Z3 expression bitwise-or `self | other`.
3584 >>> x = BitVec('x', 32)
3585 >>> y = BitVec('y', 32)
3591 a, b = _coerce_exprs(self, other)
3595 """Create the Z3 expression bitwise-or `other | self`.
3597 >>> x = BitVec('x', 32)
3601 a, b = _coerce_exprs(self, other)
3605 """Create the Z3 expression bitwise-and `self & other`.
3607 >>> x = BitVec('x', 32)
3608 >>> y = BitVec('y', 32)
3614 a, b = _coerce_exprs(self, other)
3618 """Create the Z3 expression bitwise-or `other & self`.
3620 >>> x = BitVec('x', 32)
3624 a, b = _coerce_exprs(self, other)
3628 """Create the Z3 expression bitwise-xor `self ^ other`.
3630 >>> x = BitVec('x', 32)
3631 >>> y = BitVec('y', 32)
3637 a, b = _coerce_exprs(self, other)
3641 """Create the Z3 expression bitwise-xor `other ^ self`.
3643 >>> x = BitVec('x', 32)
3647 a, b = _coerce_exprs(self, other)
3653 >>> x = BitVec('x', 32)
3660 """Return an expression representing `-self`.
3662 >>> x = BitVec('x', 32)
3671 """Create the Z3 expression bitwise-not `~self`.
3673 >>> x = BitVec('x', 32)
3682 """Create the Z3 expression (signed) division `self / other`.
3684 Use the function UDiv() for unsigned division.
3686 >>> x = BitVec('x', 32)
3687 >>> y = BitVec('y', 32)
3694 >>> UDiv(x, y).sexpr()
3697 a, b = _coerce_exprs(self, other)
3701 """Create the Z3 expression (signed) division `self / other`."""
3702 return self.
__div____div__(other)
3705 """Create the Z3 expression (signed) division `other / self`.
3707 Use the function UDiv() for unsigned division.
3709 >>> x = BitVec('x', 32)
3712 >>> (10 / x).sexpr()
3713 '(bvsdiv #x0000000a x)'
3714 >>> UDiv(10, x).sexpr()
3715 '(bvudiv #x0000000a x)'
3717 a, b = _coerce_exprs(self, other)
3721 """Create the Z3 expression (signed) division `other / self`."""
3722 return self.
__rdiv____rdiv__(other)
3725 """Create the Z3 expression (signed) mod `self % other`.
3727 Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3729 >>> x = BitVec('x', 32)
3730 >>> y = BitVec('y', 32)
3737 >>> URem(x, y).sexpr()
3739 >>> SRem(x, y).sexpr()
3742 a, b = _coerce_exprs(self, other)
3746 """Create the Z3 expression (signed) mod `other % self`.
3748 Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3750 >>> x = BitVec('x', 32)
3753 >>> (10 % x).sexpr()
3754 '(bvsmod #x0000000a x)'
3755 >>> URem(10, x).sexpr()
3756 '(bvurem #x0000000a x)'
3757 >>> SRem(10, x).sexpr()
3758 '(bvsrem #x0000000a x)'
3760 a, b = _coerce_exprs(self, other)
3764 """Create the Z3 expression (signed) `other <= self`.
3766 Use the function ULE() for unsigned less than or equal to.
3768 >>> x, y = BitVecs('x y', 32)
3771 >>> (x <= y).sexpr()
3773 >>> ULE(x, y).sexpr()
3776 a, b = _coerce_exprs(self, other)
3780 """Create the Z3 expression (signed) `other < self`.
3782 Use the function ULT() for unsigned less than.
3784 >>> x, y = BitVecs('x y', 32)
3789 >>> ULT(x, y).sexpr()
3792 a, b = _coerce_exprs(self, other)
3796 """Create the Z3 expression (signed) `other > self`.
3798 Use the function UGT() for unsigned greater than.
3800 >>> x, y = BitVecs('x y', 32)
3805 >>> UGT(x, y).sexpr()
3808 a, b = _coerce_exprs(self, other)
3812 """Create the Z3 expression (signed) `other >= self`.
3814 Use the function UGE() for unsigned greater than or equal to.
3816 >>> x, y = BitVecs('x y', 32)
3819 >>> (x >= y).sexpr()
3821 >>> UGE(x, y).sexpr()
3824 a, b = _coerce_exprs(self, other)
3828 """Create the Z3 expression (arithmetical) right shift `self >> other`
3830 Use the function LShR() for the right logical shift
3832 >>> x, y = BitVecs('x y', 32)
3835 >>> (x >> y).sexpr()
3837 >>> LShR(x, y).sexpr()
3841 >>> BitVecVal(4, 3).as_signed_long()
3843 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3845 >>> simplify(BitVecVal(4, 3) >> 1)
3847 >>> simplify(LShR(BitVecVal(4, 3), 1))
3849 >>> simplify(BitVecVal(2, 3) >> 1)
3851 >>> simplify(LShR(BitVecVal(2, 3), 1))
3854 a, b = _coerce_exprs(self, other)
3858 """Create the Z3 expression left shift `self << other`
3860 >>> x, y = BitVecs('x y', 32)
3863 >>> (x << y).sexpr()
3865 >>> simplify(BitVecVal(2, 3) << 1)
3868 a, b = _coerce_exprs(self, other)
3872 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3874 Use the function LShR() for the right logical shift
3876 >>> x = BitVec('x', 32)
3879 >>> (10 >> x).sexpr()
3880 '(bvashr #x0000000a x)'
3882 a, b = _coerce_exprs(self, other)
3886 """Create the Z3 expression left shift `other << self`.
3888 Use the function LShR() for the right logical shift
3890 >>> x = BitVec('x', 32)
3893 >>> (10 << x).sexpr()
3894 '(bvshl #x0000000a x)'
3896 a, b = _coerce_exprs(self, other)
3901 """Bit-vector values."""
3904 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
3906 >>> v = BitVecVal(0xbadc0de, 32)
3909 >>> print("0x%.8x" % v.as_long())
3915 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
3916 The most significant bit is assumed to be the sign.
3918 >>> BitVecVal(4, 3).as_signed_long()
3920 >>> BitVecVal(7, 3).as_signed_long()
3922 >>> BitVecVal(3, 3).as_signed_long()
3924 >>> BitVecVal(2**32 - 1, 32).as_signed_long()
3926 >>> BitVecVal(2**64 - 1, 64).as_signed_long()
3929 sz = self.
sizesize()
3931 if val >= 2**(sz - 1):
3933 if val < -2**(sz - 1):
3945 """Return `True` if `a` is a Z3 bit-vector expression.
3947 >>> b = BitVec('b', 32)
3955 return isinstance(a, BitVecRef)
3959 """Return `True` if `a` is a Z3 bit-vector numeral value.
3961 >>> b = BitVec('b', 32)
3964 >>> b = BitVecVal(10, 32)
3970 return is_bv(a)
and _is_numeral(a.ctx, a.as_ast())
3974 """Return the Z3 expression BV2Int(a).
3976 >>> b = BitVec('b', 3)
3977 >>> BV2Int(b).sort()
3982 >>> x > BV2Int(b, is_signed=False)
3984 >>> x > BV2Int(b, is_signed=True)
3985 x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3986 >>> solve(x > BV2Int(b), b == 1, x < 3)
3990 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
3997 """Return the z3 expression Int2BV(a, num_bits).
3998 It is a bit-vector of width num_bits and represents the
3999 modulo of a by 2^num_bits
4006 """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
4008 >>> Byte = BitVecSort(8)
4009 >>> Word = BitVecSort(16)
4012 >>> x = Const('x', Byte)
4013 >>> eq(x, BitVec('x', 8))
4021 """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
4023 >>> v = BitVecVal(10, 32)
4026 >>> print("0x%.8x" % v.as_long())
4038 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
4039 If `ctx=None`, then the global context is used.
4041 >>> x = BitVec('x', 16)
4048 >>> word = BitVecSort(16)
4049 >>> x2 = BitVec('x', word)
4053 if isinstance(bv, BitVecSortRef):
4062 """Return a tuple of bit-vector constants of size bv.
4064 >>> x, y, z = BitVecs('x y z', 16)
4071 >>> Product(x, y, z)
4073 >>> simplify(Product(x, y, z))
4077 if isinstance(names, str):
4078 names = names.split(
" ")
4079 return [
BitVec(name, bv, ctx)
for name
in names]
4083 """Create a Z3 bit-vector concatenation expression.
4085 >>> v = BitVecVal(1, 4)
4086 >>> Concat(v, v+1, v)
4087 Concat(Concat(1, 1 + 1), 1)
4088 >>> simplify(Concat(v, v+1, v))
4090 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
4093 args = _get_args(args)
4096 _z3_assert(sz >= 2,
"At least two arguments expected.")
4103 if is_seq(args[0])
or isinstance(args[0], str):
4104 args = [_coerce_seq(s, ctx)
for s
in args]
4106 _z3_assert(all([
is_seq(a)
for a
in args]),
"All arguments must be sequence expressions.")
4109 v[i] = args[i].as_ast()
4114 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
4117 v[i] = args[i].as_ast()
4121 _z3_assert(all([
is_bv(a)
for a
in args]),
"All arguments must be Z3 bit-vector expressions.")
4123 for i
in range(sz - 1):
4129 """Create a Z3 bit-vector extraction expression.
4130 Extract is overloaded to also work on sequence extraction.
4131 The functions SubString and SubSeq are redirected to Extract.
4132 For this case, the arguments are reinterpreted as:
4133 high - is a sequence (string)
4135 a - is the length to be extracted
4137 >>> x = BitVec('x', 8)
4138 >>> Extract(6, 2, x)
4140 >>> Extract(6, 2, x).sort()
4142 >>> simplify(Extract(StringVal("abcd"),2,1))
4145 if isinstance(high, str):
4149 offset, length = _coerce_exprs(low, a, s.ctx)
4152 _z3_assert(low <= high,
"First argument must be greater than or equal to second argument")
4153 _z3_assert(_is_int(high)
and high >= 0
and _is_int(low)
and low >= 0,
4154 "First and second arguments must be non negative integers")
4155 _z3_assert(
is_bv(a),
"Third argument must be a Z3 bit-vector expression")
4159 def _check_bv_args(a, b):
4161 _z3_assert(
is_bv(a)
or is_bv(b),
"First or second argument must be a Z3 bit-vector expression")
4165 """Create the Z3 expression (unsigned) `other <= self`.
4167 Use the operator <= for signed less than or equal to.
4169 >>> x, y = BitVecs('x y', 32)
4172 >>> (x <= y).sexpr()
4174 >>> ULE(x, y).sexpr()
4177 _check_bv_args(a, b)
4178 a, b = _coerce_exprs(a, b)
4183 """Create the Z3 expression (unsigned) `other < self`.
4185 Use the operator < for signed less than.
4187 >>> x, y = BitVecs('x y', 32)
4192 >>> ULT(x, y).sexpr()
4195 _check_bv_args(a, b)
4196 a, b = _coerce_exprs(a, b)
4201 """Create the Z3 expression (unsigned) `other >= self`.
4203 Use the operator >= for signed greater than or equal to.
4205 >>> x, y = BitVecs('x y', 32)
4208 >>> (x >= y).sexpr()
4210 >>> UGE(x, y).sexpr()
4213 _check_bv_args(a, b)
4214 a, b = _coerce_exprs(a, b)
4219 """Create the Z3 expression (unsigned) `other > self`.
4221 Use the operator > for signed greater than.
4223 >>> x, y = BitVecs('x y', 32)
4228 >>> UGT(x, y).sexpr()
4231 _check_bv_args(a, b)
4232 a, b = _coerce_exprs(a, b)
4237 """Create the Z3 expression (unsigned) division `self / other`.
4239 Use the operator / for signed division.
4241 >>> x = BitVec('x', 32)
4242 >>> y = BitVec('y', 32)
4245 >>> UDiv(x, y).sort()
4249 >>> UDiv(x, y).sexpr()
4252 _check_bv_args(a, b)
4253 a, b = _coerce_exprs(a, b)
4258 """Create the Z3 expression (unsigned) remainder `self % other`.
4260 Use the operator % for signed modulus, and SRem() for signed remainder.
4262 >>> x = BitVec('x', 32)
4263 >>> y = BitVec('y', 32)
4266 >>> URem(x, y).sort()
4270 >>> URem(x, y).sexpr()
4273 _check_bv_args(a, b)
4274 a, b = _coerce_exprs(a, b)
4279 """Create the Z3 expression signed remainder.
4281 Use the operator % for signed modulus, and URem() for unsigned remainder.
4283 >>> x = BitVec('x', 32)
4284 >>> y = BitVec('y', 32)
4287 >>> SRem(x, y).sort()
4291 >>> SRem(x, y).sexpr()
4294 _check_bv_args(a, b)
4295 a, b = _coerce_exprs(a, b)
4300 """Create the Z3 expression logical right shift.
4302 Use the operator >> for the arithmetical right shift.
4304 >>> x, y = BitVecs('x y', 32)
4307 >>> (x >> y).sexpr()
4309 >>> LShR(x, y).sexpr()
4313 >>> BitVecVal(4, 3).as_signed_long()
4315 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
4317 >>> simplify(BitVecVal(4, 3) >> 1)
4319 >>> simplify(LShR(BitVecVal(4, 3), 1))
4321 >>> simplify(BitVecVal(2, 3) >> 1)
4323 >>> simplify(LShR(BitVecVal(2, 3), 1))
4326 _check_bv_args(a, b)
4327 a, b = _coerce_exprs(a, b)
4332 """Return an expression representing `a` rotated to the left `b` times.
4334 >>> a, b = BitVecs('a b', 16)
4335 >>> RotateLeft(a, b)
4337 >>> simplify(RotateLeft(a, 0))
4339 >>> simplify(RotateLeft(a, 16))
4342 _check_bv_args(a, b)
4343 a, b = _coerce_exprs(a, b)
4348 """Return an expression representing `a` rotated to the right `b` times.
4350 >>> a, b = BitVecs('a b', 16)
4351 >>> RotateRight(a, b)
4353 >>> simplify(RotateRight(a, 0))
4355 >>> simplify(RotateRight(a, 16))
4358 _check_bv_args(a, b)
4359 a, b = _coerce_exprs(a, b)
4364 """Return a bit-vector expression with `n` extra sign-bits.
4366 >>> x = BitVec('x', 16)
4367 >>> n = SignExt(8, x)
4374 >>> v0 = BitVecVal(2, 2)
4379 >>> v = simplify(SignExt(6, v0))
4384 >>> print("%.x" % v.as_long())
4388 _z3_assert(_is_int(n),
"First argument must be an integer")
4389 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4394 """Return a bit-vector expression with `n` extra zero-bits.
4396 >>> x = BitVec('x', 16)
4397 >>> n = ZeroExt(8, x)
4404 >>> v0 = BitVecVal(2, 2)
4409 >>> v = simplify(ZeroExt(6, v0))
4416 _z3_assert(_is_int(n),
"First argument must be an integer")
4417 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4422 """Return an expression representing `n` copies of `a`.
4424 >>> x = BitVec('x', 8)
4425 >>> n = RepeatBitVec(4, x)
4430 >>> v0 = BitVecVal(10, 4)
4431 >>> print("%.x" % v0.as_long())
4433 >>> v = simplify(RepeatBitVec(4, v0))
4436 >>> print("%.x" % v.as_long())
4440 _z3_assert(_is_int(n),
"First argument must be an integer")
4441 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4446 """Return the reduction-and expression of `a`."""
4448 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
4453 """Return the reduction-or expression of `a`."""
4455 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
4460 """A predicate the determines that bit-vector addition does not overflow"""
4461 _check_bv_args(a, b)
4462 a, b = _coerce_exprs(a, b)
4467 """A predicate the determines that signed bit-vector addition does not underflow"""
4468 _check_bv_args(a, b)
4469 a, b = _coerce_exprs(a, b)
4474 """A predicate the determines that bit-vector subtraction does not overflow"""
4475 _check_bv_args(a, b)
4476 a, b = _coerce_exprs(a, b)
4481 """A predicate the determines that bit-vector subtraction does not underflow"""
4482 _check_bv_args(a, b)
4483 a, b = _coerce_exprs(a, b)
4488 """A predicate the determines that bit-vector signed division does not overflow"""
4489 _check_bv_args(a, b)
4490 a, b = _coerce_exprs(a, b)
4495 """A predicate the determines that bit-vector unary negation does not overflow"""
4497 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
4502 """A predicate the determines that bit-vector multiplication does not overflow"""
4503 _check_bv_args(a, b)
4504 a, b = _coerce_exprs(a, b)
4509 """A predicate the determines that bit-vector signed multiplication does not underflow"""
4510 _check_bv_args(a, b)
4511 a, b = _coerce_exprs(a, b)
4525 """Return the domain of the array sort `self`.
4527 >>> A = ArraySort(IntSort(), BoolSort())
4534 """Return the domain of the array sort `self`.
4539 """Return the range of the array sort `self`.
4541 >>> A = ArraySort(IntSort(), BoolSort())
4549 """Array expressions. """
4552 """Return the array sort of the array expression `self`.
4554 >>> a = Array('a', IntSort(), BoolSort())
4561 """Shorthand for `self.sort().domain()`.
4563 >>> a = Array('a', IntSort(), BoolSort())
4570 """Shorthand for self.sort().domain_n(i)`."""
4574 """Shorthand for `self.sort().range()`.
4576 >>> a = Array('a', IntSort(), BoolSort())
4583 """Return the Z3 expression `self[arg]`.
4585 >>> a = Array('a', IntSort(), BoolSort())
4592 return _array_select(self, arg)
4598 def _array_select(ar, arg):
4599 if isinstance(arg, tuple):
4600 args = [ar.sort().
domain_n(i).cast(arg[i])
for i
in range(len(arg))]
4601 _args, sz = _to_ast_array(args)
4602 return _to_expr_ref(
Z3_mk_select_n(ar.ctx_ref(), ar.as_ast(), sz, _args), ar.ctx)
4603 arg = ar.sort().
domain().cast(arg)
4604 return _to_expr_ref(
Z3_mk_select(ar.ctx_ref(), ar.as_ast(), arg.as_ast()), ar.ctx)
4612 """Return `True` if `a` is a Z3 array expression.
4614 >>> a = Array('a', IntSort(), IntSort())
4617 >>> is_array(Store(a, 0, 1))
4622 return isinstance(a, ArrayRef)
4626 """Return `True` if `a` is a Z3 constant array.
4628 >>> a = K(IntSort(), 10)
4629 >>> is_const_array(a)
4631 >>> a = Array('a', IntSort(), IntSort())
4632 >>> is_const_array(a)
4639 """Return `True` if `a` is a Z3 constant array.
4641 >>> a = K(IntSort(), 10)
4644 >>> a = Array('a', IntSort(), IntSort())
4652 """Return `True` if `a` is a Z3 map array expression.
4654 >>> f = Function('f', IntSort(), IntSort())
4655 >>> b = Array('b', IntSort(), IntSort())
4668 """Return `True` if `a` is a Z3 default array expression.
4669 >>> d = Default(K(IntSort(), 10))
4673 return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4677 """Return the function declaration associated with a Z3 map array expression.
4679 >>> f = Function('f', IntSort(), IntSort())
4680 >>> b = Array('b', IntSort(), IntSort())
4682 >>> eq(f, get_map_func(a))
4686 >>> get_map_func(a)(0)
4690 _z3_assert(
is_map(a),
"Z3 array map expression expected.")
4701 """Return the Z3 array sort with the given domain and range sorts.
4703 >>> A = ArraySort(IntSort(), BoolSort())
4710 >>> AA = ArraySort(IntSort(), A)
4712 Array(Int, Array(Int, Bool))
4714 sig = _get_args(sig)
4716 _z3_assert(len(sig) > 1,
"At least two arguments expected")
4717 arity = len(sig) - 1
4722 _z3_assert(
is_sort(s),
"Z3 sort expected")
4723 _z3_assert(s.ctx == r.ctx,
"Context mismatch")
4727 dom = (Sort * arity)()
4728 for i
in range(arity):
4734 """Return an array constant named `name` with the given domain and range sorts.
4736 >>> a = Array('a', IntSort(), IntSort())
4748 """Return a Z3 store array expression.
4750 >>> a = Array('a', IntSort(), IntSort())
4751 >>> i, v = Ints('i v')
4752 >>> s = Update(a, i, v)
4755 >>> prove(s[i] == v)
4758 >>> prove(Implies(i != j, s[j] == a[j]))
4762 _z3_assert(
is_array_sort(a),
"First argument must be a Z3 array expression")
4763 args = _get_args(args)
4766 raise Z3Exception(
"array update requires index and value arguments")
4770 i = a.sort().domain().cast(i)
4771 v = a.sort().
range().cast(v)
4772 return _to_expr_ref(
Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
4773 v = a.sort().
range().cast(args[-1])
4774 idxs = [a.sort().domain_n(i).cast(args[i])
for i
in range(len(args)-1)]
4775 _args, sz = _to_ast_array(idxs)
4776 return _to_expr_ref(
Z3_mk_store_n(ctx.ref(), a.as_ast(), sz, _args, v.as_ast()), ctx)
4780 """ Return a default value for array expression.
4781 >>> b = K(IntSort(), 1)
4782 >>> prove(Default(b) == 1)
4786 _z3_assert(
is_array_sort(a),
"First argument must be a Z3 array expression")
4791 """Return a Z3 store array expression.
4793 >>> a = Array('a', IntSort(), IntSort())
4794 >>> i, v = Ints('i v')
4795 >>> s = Store(a, i, v)
4798 >>> prove(s[i] == v)
4801 >>> prove(Implies(i != j, s[j] == a[j]))
4808 """Return a Z3 select array expression.
4810 >>> a = Array('a', IntSort(), IntSort())
4814 >>> eq(Select(a, i), a[i])
4817 args = _get_args(args)
4819 _z3_assert(
is_array_sort(a),
"First argument must be a Z3 array expression")
4824 """Return a Z3 map array expression.
4826 >>> f = Function('f', IntSort(), IntSort(), IntSort())
4827 >>> a1 = Array('a1', IntSort(), IntSort())
4828 >>> a2 = Array('a2', IntSort(), IntSort())
4829 >>> b = Map(f, a1, a2)
4832 >>> prove(b[0] == f(a1[0], a2[0]))
4835 args = _get_args(args)
4837 _z3_assert(len(args) > 0,
"At least one Z3 array expression expected")
4838 _z3_assert(
is_func_decl(f),
"First argument must be a Z3 function declaration")
4839 _z3_assert(all([
is_array(a)
for a
in args]),
"Z3 array expected expected")
4840 _z3_assert(len(args) == f.arity(),
"Number of arguments mismatch")
4841 _args, sz = _to_ast_array(args)
4847 """Return a Z3 constant array expression.
4849 >>> a = K(IntSort(), 10)
4861 _z3_assert(
is_sort(dom),
"Z3 sort expected")
4864 v = _py2expr(v, ctx)
4869 """Return extensionality index for one-dimensional arrays.
4870 >> a, b = Consts('a b', SetSort(IntSort()))
4877 return _to_expr_ref(
Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4882 k = _py2expr(k, ctx)
4887 """Return `True` if `a` is a Z3 array select application.
4889 >>> a = Array('a', IntSort(), IntSort())
4900 """Return `True` if `a` is a Z3 array store application.
4902 >>> a = Array('a', IntSort(), IntSort())
4905 >>> is_store(Store(a, 0, 1))
4918 """ Create a set sort over element sort s"""
4923 """Create the empty set
4924 >>> EmptySet(IntSort())
4932 """Create the full set
4933 >>> FullSet(IntSort())
4941 """ Take the union of sets
4942 >>> a = Const('a', SetSort(IntSort()))
4943 >>> b = Const('b', SetSort(IntSort()))
4947 args = _get_args(args)
4948 ctx = _ctx_from_ast_arg_list(args)
4949 _args, sz = _to_ast_array(args)
4954 """ Take the union of sets
4955 >>> a = Const('a', SetSort(IntSort()))
4956 >>> b = Const('b', SetSort(IntSort()))
4957 >>> SetIntersect(a, b)
4960 args = _get_args(args)
4961 ctx = _ctx_from_ast_arg_list(args)
4962 _args, sz = _to_ast_array(args)
4967 """ Add element e to set s
4968 >>> a = Const('a', SetSort(IntSort()))
4972 ctx = _ctx_from_ast_arg_list([s, e])
4973 e = _py2expr(e, ctx)
4978 """ Remove element e to set s
4979 >>> a = Const('a', SetSort(IntSort()))
4983 ctx = _ctx_from_ast_arg_list([s, e])
4984 e = _py2expr(e, ctx)
4989 """ The complement of set s
4990 >>> a = Const('a', SetSort(IntSort()))
4991 >>> SetComplement(a)
4999 """ The set difference of a and b
5000 >>> a = Const('a', SetSort(IntSort()))
5001 >>> b = Const('b', SetSort(IntSort()))
5002 >>> SetDifference(a, b)
5005 ctx = _ctx_from_ast_arg_list([a, b])
5010 """ Check if e is a member of set s
5011 >>> a = Const('a', SetSort(IntSort()))
5015 ctx = _ctx_from_ast_arg_list([s, e])
5016 e = _py2expr(e, ctx)
5021 """ Check if a is a subset of b
5022 >>> a = Const('a', SetSort(IntSort()))
5023 >>> b = Const('b', SetSort(IntSort()))
5027 ctx = _ctx_from_ast_arg_list([a, b])
5037 def _valid_accessor(acc):
5038 """Return `True` if acc is pair of the form (String, Datatype or Sort). """
5039 if not isinstance(acc, tuple):
5043 return isinstance(acc[0], str)
and (isinstance(acc[1], Datatype)
or is_sort(acc[1]))
5047 """Helper class for declaring Z3 datatypes.
5049 >>> List = Datatype('List')
5050 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5051 >>> List.declare('nil')
5052 >>> List = List.create()
5053 >>> # List is now a Z3 declaration
5056 >>> List.cons(10, List.nil)
5058 >>> List.cons(10, List.nil).sort()
5060 >>> cons = List.cons
5064 >>> n = cons(1, cons(0, nil))
5066 cons(1, cons(0, nil))
5067 >>> simplify(cdr(n))
5069 >>> simplify(car(n))
5080 r.constructors = copy.deepcopy(self.
constructorsconstructors)
5085 _z3_assert(isinstance(name, str),
"String expected")
5086 _z3_assert(isinstance(rec_name, str),
"String expected")
5088 all([_valid_accessor(a)
for a
in args]),
5089 "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)",
5091 self.
constructorsconstructors.append((name, rec_name, args))
5094 """Declare constructor named `name` with the given accessors `args`.
5095 Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort
5096 or a reference to the datatypes being declared.
5098 In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
5099 declares the constructor named `cons` that builds a new List using an integer and a List.
5100 It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer
5101 of a `cons` cell, and `cdr` the list of a `cons` cell. After all constructors were declared,
5102 we use the method create() to create the actual datatype in Z3.
5104 >>> List = Datatype('List')
5105 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5106 >>> List.declare('nil')
5107 >>> List = List.create()
5110 _z3_assert(isinstance(name, str),
"String expected")
5111 _z3_assert(name !=
"",
"Constructor name cannot be empty")
5112 return self.
declare_coredeclare_core(name,
"is-" + name, *args)
5118 """Create a Z3 datatype based on the constructors declared using the method `declare()`.
5120 The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
5122 >>> List = Datatype('List')
5123 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5124 >>> List.declare('nil')
5125 >>> List = List.create()
5128 >>> List.cons(10, List.nil)
5135 """Auxiliary object used to create Z3 datatypes."""
5142 if self.
ctxctx.ref()
is not None and Z3_del_constructor
is not None:
5147 """Auxiliary object used to create Z3 datatypes."""
5154 if self.
ctxctx.ref()
is not None and Z3_del_constructor_list
is not None:
5159 """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
5161 In the following example we define a Tree-List using two mutually recursive datatypes.
5163 >>> TreeList = Datatype('TreeList')
5164 >>> Tree = Datatype('Tree')
5165 >>> # Tree has two constructors: leaf and node
5166 >>> Tree.declare('leaf', ('val', IntSort()))
5167 >>> # a node contains a list of trees
5168 >>> Tree.declare('node', ('children', TreeList))
5169 >>> TreeList.declare('nil')
5170 >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
5171 >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
5172 >>> Tree.val(Tree.leaf(10))
5174 >>> simplify(Tree.val(Tree.leaf(10)))
5176 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
5178 node(cons(leaf(10), cons(leaf(20), nil)))
5179 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
5180 >>> simplify(n2 == n1)
5182 >>> simplify(TreeList.car(Tree.children(n2)) == n1)
5187 _z3_assert(len(ds) > 0,
"At least one Datatype must be specified")
5188 _z3_assert(all([isinstance(d, Datatype)
for d
in ds]),
"Arguments must be Datatypes")
5189 _z3_assert(all([d.ctx == ds[0].ctx
for d
in ds]),
"Context mismatch")
5190 _z3_assert(all([d.constructors != []
for d
in ds]),
"Non-empty Datatypes expected")
5193 names = (Symbol * num)()
5194 out = (Sort * num)()
5195 clists = (ConstructorList * num)()
5197 for i
in range(num):
5200 num_cs = len(d.constructors)
5201 cs = (Constructor * num_cs)()
5202 for j
in range(num_cs):
5203 c = d.constructors[j]
5208 fnames = (Symbol * num_fs)()
5209 sorts = (Sort * num_fs)()
5210 refs = (ctypes.c_uint * num_fs)()
5211 for k
in range(num_fs):
5215 if isinstance(ftype, Datatype):
5218 ds.count(ftype) == 1,
5219 "One and only one occurrence of each datatype is expected",
5222 refs[k] = ds.index(ftype)
5225 _z3_assert(
is_sort(ftype),
"Z3 sort expected")
5226 sorts[k] = ftype.ast
5235 for i
in range(num):
5237 num_cs = dref.num_constructors()
5238 for j
in range(num_cs):
5239 cref = dref.constructor(j)
5240 cref_name = cref.name()
5241 cref_arity = cref.arity()
5242 if cref.arity() == 0:
5244 setattr(dref, cref_name, cref)
5245 rref = dref.recognizer(j)
5246 setattr(dref,
"is_" + cref_name, rref)
5247 for k
in range(cref_arity):
5248 aref = dref.accessor(j, k)
5249 setattr(dref, aref.name(), aref)
5251 return tuple(result)
5255 """Datatype sorts."""
5258 """Return the number of constructors in the given Z3 datatype.
5260 >>> List = Datatype('List')
5261 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5262 >>> List.declare('nil')
5263 >>> List = List.create()
5264 >>> # List is now a Z3 declaration
5265 >>> List.num_constructors()
5271 """Return a constructor of the datatype `self`.
5273 >>> List = Datatype('List')
5274 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5275 >>> List.declare('nil')
5276 >>> List = List.create()
5277 >>> # List is now a Z3 declaration
5278 >>> List.num_constructors()
5280 >>> List.constructor(0)
5282 >>> List.constructor(1)
5286 _z3_assert(idx < self.
num_constructorsnum_constructors(),
"Invalid constructor index")
5290 """In Z3, each constructor has an associated recognizer predicate.
5292 If the constructor is named `name`, then the recognizer `is_name`.
5294 >>> List = Datatype('List')
5295 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5296 >>> List.declare('nil')
5297 >>> List = List.create()
5298 >>> # List is now a Z3 declaration
5299 >>> List.num_constructors()
5301 >>> List.recognizer(0)
5303 >>> List.recognizer(1)
5305 >>> simplify(List.is_nil(List.cons(10, List.nil)))
5307 >>> simplify(List.is_cons(List.cons(10, List.nil)))
5309 >>> l = Const('l', List)
5310 >>> simplify(List.is_cons(l))
5314 _z3_assert(idx < self.
num_constructorsnum_constructors(),
"Invalid recognizer index")
5318 """In Z3, each constructor has 0 or more accessor.
5319 The number of accessors is equal to the arity of the constructor.
5321 >>> List = Datatype('List')
5322 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5323 >>> List.declare('nil')
5324 >>> List = List.create()
5325 >>> List.num_constructors()
5327 >>> List.constructor(0)
5329 >>> num_accs = List.constructor(0).arity()
5332 >>> List.accessor(0, 0)
5334 >>> List.accessor(0, 1)
5336 >>> List.constructor(1)
5338 >>> num_accs = List.constructor(1).arity()
5343 _z3_assert(i < self.
num_constructorsnum_constructors(),
"Invalid constructor index")
5344 _z3_assert(j < self.
constructorconstructor(i).arity(),
"Invalid accessor index")
5352 """Datatype expressions."""
5355 """Return the datatype sort of the datatype expression `self`."""
5359 """Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""
5364 """Create a named tuple sort base on a set of underlying sorts
5366 >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])
5369 projects = [(
"project%d" % i, sorts[i])
for i
in range(len(sorts))]
5370 tuple.declare(name, *projects)
5371 tuple = tuple.create()
5372 return tuple, tuple.constructor(0), [tuple.accessor(0, i)
for i
in range(len(sorts))]
5376 """Create a named tagged union sort base on a set of underlying sorts
5378 >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
5381 for i
in range(len(sorts)):
5382 sum.declare(
"inject%d" % i, (
"project%d" % i, sorts[i]))
5384 return sum, [(sum.constructor(i), sum.accessor(i, 0))
for i
in range(len(sorts))]
5388 """Return a new enumeration sort named `name` containing the given values.
5390 The result is a pair (sort, list of constants).
5392 >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5395 _z3_assert(isinstance(name, str),
"Name must be a string")
5396 _z3_assert(all([isinstance(v, str)
for v
in values]),
"Eumeration sort values must be strings")
5397 _z3_assert(len(values) > 0,
"At least one value expected")
5400 _val_names = (Symbol * num)()
5401 for i
in range(num):
5403 _values = (FuncDecl * num)()
5404 _testers = (FuncDecl * num)()
5408 for i
in range(num):
5410 V = [a()
for a
in V]
5421 """Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3.
5423 Consider using the function `args2params` to create instances of this object.
5431 self.
paramsparams = params
5438 if self.
ctxctx.ref()
is not None and Z3_params_dec_ref
is not None:
5442 """Set parameter name with value val."""
5444 _z3_assert(isinstance(name, str),
"parameter name must be a string")
5446 if isinstance(val, bool):
5450 elif isinstance(val, float):
5452 elif isinstance(val, str):
5456 _z3_assert(
False,
"invalid parameter value")
5462 _z3_assert(isinstance(ds, ParamDescrsRef),
"parameter description set expected")
5467 """Convert python arguments into a Z3_params object.
5468 A ':' is added to the keywords, and '_' is replaced with '-'
5470 >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5471 (params model true relevancy 2 elim_and true)
5474 _z3_assert(len(arguments) % 2 == 0,
"Argument list must have an even number of elements.")
5490 """Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3.
5494 _z3_assert(isinstance(descr, ParamDescrs),
"parameter description object expected")
5500 return ParamsDescrsRef(self.
descrdescr, self.
ctxctx)
5503 if self.
ctxctx.ref()
is not None and Z3_param_descrs_dec_ref
is not None:
5507 """Return the size of in the parameter description `self`.
5512 """Return the size of in the parameter description `self`.
5514 return self.
sizesize()
5517 """Return the i-th parameter name in the parameter description `self`.
5522 """Return the kind of the parameter named `n`.
5527 """Return the documentation string of the parameter named `n`.
5548 """Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible).
5550 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
5551 A goal has a solution if one of its subgoals has a solution.
5552 A goal is unsatisfiable if all subgoals are unsatisfiable.
5555 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
5557 _z3_assert(goal
is None or ctx
is not None,
5558 "If goal is different from None, then ctx must be also different from None")
5561 if self.
goalgoal
is None:
5566 if self.
goalgoal
is not None and self.
ctxctx.ref()
is not None and Z3_goal_dec_ref
is not None:
5570 """Return the depth of the goal `self`.
5571 The depth corresponds to the number of tactics applied to `self`.
5573 >>> x, y = Ints('x y')
5575 >>> g.add(x == 0, y >= x + 1)
5578 >>> r = Then('simplify', 'solve-eqs')(g)
5579 >>> # r has 1 subgoal
5588 """Return `True` if `self` contains the `False` constraints.
5590 >>> x, y = Ints('x y')
5592 >>> g.inconsistent()
5594 >>> g.add(x == 0, x == 1)
5597 >>> g.inconsistent()
5599 >>> g2 = Tactic('propagate-values')(g)[0]
5600 >>> g2.inconsistent()
5606 """Return the precision (under-approximation, over-approximation, or precise) of the goal `self`.
5609 >>> g.prec() == Z3_GOAL_PRECISE
5611 >>> x, y = Ints('x y')
5612 >>> g.add(x == y + 1)
5613 >>> g.prec() == Z3_GOAL_PRECISE
5615 >>> t = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10)
5618 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
5619 >>> g2.prec() == Z3_GOAL_PRECISE
5621 >>> g2.prec() == Z3_GOAL_UNDER
5627 """Alias for `prec()`.
5630 >>> g.precision() == Z3_GOAL_PRECISE
5633 return self.
precprec()
5636 """Return the number of constraints in the goal `self`.
5641 >>> x, y = Ints('x y')
5642 >>> g.add(x == 0, y > x)
5649 """Return the number of constraints in the goal `self`.
5654 >>> x, y = Ints('x y')
5655 >>> g.add(x == 0, y > x)
5659 return self.
sizesize()
5662 """Return a constraint in the goal `self`.
5665 >>> x, y = Ints('x y')
5666 >>> g.add(x == 0, y > x)
5675 """Return a constraint in the goal `self`.
5678 >>> x, y = Ints('x y')
5679 >>> g.add(x == 0, y > x)
5685 if arg >= len(self):
5687 return self.
getget(arg)
5690 """Assert constraints into the goal.
5694 >>> g.assert_exprs(x > 0, x < 2)
5698 args = _get_args(args)
5709 >>> g.append(x > 0, x < 2)
5720 >>> g.insert(x > 0, x < 2)
5731 >>> g.add(x > 0, x < 2)
5738 """Retrieve model from a satisfiable goal
5739 >>> a, b = Ints('a b')
5741 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
5742 >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs'))
5745 [Or(b == 0, b == 1), Not(0 <= b)]
5747 [Or(b == 0, b == 1), Not(1 <= b)]
5748 >>> # Remark: the subgoal r[0] is unsatisfiable
5749 >>> # Creating a solver for solving the second subgoal
5756 >>> # Model s.model() does not assign a value to `a`
5757 >>> # It is a model for subgoal `r[1]`, but not for goal `g`
5758 >>> # The method convert_model creates a model for `g` from a model for `r[1]`.
5759 >>> r[1].convert_model(s.model())
5763 _z3_assert(isinstance(model, ModelRef),
"Z3 Model expected")
5767 return obj_to_string(self)
5770 """Return a textual representation of the s-expression representing the goal."""
5774 """Return a textual representation of the goal in DIMACS format."""
5778 """Copy goal `self` to context `target`.
5786 >>> g2 = g.translate(c2)
5789 >>> g.ctx == main_ctx()
5793 >>> g2.ctx == main_ctx()
5797 _z3_assert(isinstance(target, Context),
"target must be a context")
5807 """Return a new simplified goal.
5809 This method is essentially invoking the simplify tactic.
5813 >>> g.add(x + 1 >= 2)
5816 >>> g2 = g.simplify()
5819 >>> # g was not modified
5824 return t.apply(self, *arguments, **keywords)[0]
5827 """Return goal `self` as a single Z3 expression.
5844 return self.
getget(0)
5846 return And([self.
getget(i)
for i
in range(len(self))], self.
ctxctx)
5856 """A collection (vector) of ASTs."""
5865 assert ctx
is not None
5870 if self.
vectorvector
is not None and self.
ctxctx.ref()
is not None and Z3_ast_vector_dec_ref
is not None:
5874 """Return the size of the vector `self`.
5879 >>> A.push(Int('x'))
5880 >>> A.push(Int('x'))
5887 """Return the AST at position `i`.
5890 >>> A.push(Int('x') + 1)
5891 >>> A.push(Int('y'))
5898 if isinstance(i, int):
5902 if i >= self.
__len____len__():
5906 elif isinstance(i, slice):
5909 result.append(_to_ast_ref(
5916 """Update AST at position `i`.
5919 >>> A.push(Int('x') + 1)
5920 >>> A.push(Int('y'))
5927 if i >= self.
__len____len__():
5932 """Add `v` in the end of the vector.
5937 >>> A.push(Int('x'))
5944 """Resize the vector to `sz` elements.
5950 >>> for i in range(10): A[i] = Int('x')