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, Iterator
59 from collections.abc
import Callable
75 if sys.version_info.major < 3:
77 return isinstance(v, (int, long))
80 return isinstance(v, int)
92 major = ctypes.c_uint(0)
93 minor = ctypes.c_uint(0)
94 build = ctypes.c_uint(0)
95 rev = ctypes.c_uint(0)
97 return "%s.%s.%s" % (major.value, minor.value, build.value)
101 major = ctypes.c_uint(0)
102 minor = ctypes.c_uint(0)
103 build = ctypes.c_uint(0)
104 rev = ctypes.c_uint(0)
106 return (major.value, minor.value, build.value, rev.value)
113 def _z3_assert(cond, msg):
115 raise Z3Exception(msg)
118 def _z3_check_cint_overflow(n, name):
119 _z3_assert(ctypes.c_int(n).value == n, name +
" is too large")
123 """Log interaction to a file. This function must be invoked immediately after init(). """
128 """Append user-defined string to interaction log. """
133 """Convert an integer or string into a Z3 symbol."""
140 def _symbol2py(ctx, s):
141 """Convert a Z3 symbol back into a Python object. """
154 if len(args) == 1
and (isinstance(args[0], tuple)
or isinstance(args[0], list)):
156 elif len(args) == 1
and (isinstance(args[0], set)
or isinstance(args[0], AstVector)):
157 return [arg
for arg
in args[0]]
158 elif len(args) == 1
and isinstance(args[0], Iterator):
168 def _get_args_ast_list(args):
170 if isinstance(args, (set, AstVector, tuple)):
171 return [arg
for arg
in args]
178 def _to_param_value(val):
179 if isinstance(val, bool):
180 return "true" if val
else "false"
191 """A Context manages all other Z3 objects, global configuration options, etc.
193 Z3Py uses a default global context. For most applications this is sufficient.
194 An application may use multiple Z3 contexts. Objects created in one context
195 cannot be used in another one. However, several objects may be "translated" from
196 one context to another. It is not safe to access Z3 objects from multiple threads.
197 The only exception is the method `interrupt()` that can be used to interrupt() a long
199 The initialization method receives global configuration options for the new context.
204 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
223 if Z3_del_context
is not None and self.
owner:
229 """Return a reference to the actual C pointer to the Z3 context."""
233 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
235 This method can be invoked from a thread different from the one executing the
236 interruptible procedure.
241 """Return the global parameter description set."""
250 """Return a reference to the global Z3 context.
253 >>> x.ctx == main_ctx()
258 >>> x2 = Real('x', c)
265 if _main_ctx
is None:
270 def _get_ctx(ctx) -> Context:
282 """Set Z3 global (or module) parameters.
284 >>> set_param(precision=10)
287 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
291 if not set_pp_option(k, v):
306 """Reset all global (or module) parameters.
312 """Alias for 'set_param' for backward compatibility.
318 """Return the value of a Z3 global (or module) parameter
320 >>> get_param('nlsat.reorder')
323 ptr = (ctypes.c_char_p * 1)()
325 r = z3core._to_pystr(ptr[0])
327 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
339 """Superclass for all Z3 objects that have support for pretty printing."""
344 def _repr_html_(self):
345 in_html = in_html_mode()
348 set_html_mode(in_html)
353 """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions."""
361 if self.ctx.ref()
is not None and self.
ast is not None and Z3_dec_ref
is not None:
366 return _to_ast_ref(self.
ast, self.
ctx)
369 return obj_to_string(self)
372 return obj_to_string(self)
375 return self.
eq(other)
388 elif is_eq(self)
and self.num_args() == 2:
389 return self.arg(0).
eq(self.arg(1))
391 raise Z3Exception(
"Symbolic expressions cannot be cast to concrete Boolean values.")
394 """Return a string representing the AST node in s-expression notation.
397 >>> ((x + 1)*x).sexpr()
403 """Return a pointer to the corresponding C Z3_ast object."""
407 """Return unique identifier for object. It can be used for hash-tables and maps."""
411 """Return a reference to the C context where this AST node is stored."""
412 return self.ctx.ref()
415 """Return `True` if `self` and `other` are structurally identical.
422 >>> n1 = simplify(n1)
423 >>> n2 = simplify(n2)
428 _z3_assert(
is_ast(other),
"Z3 AST expected")
432 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
438 >>> # Nodes in different contexts can't be mixed.
439 >>> # However, we can translate nodes from one context to another.
440 >>> x.translate(c2) + y
444 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
451 """Return a hashcode for the `self`.
453 >>> n1 = simplify(Int('x') + 1)
454 >>> n2 = simplify(2 + Int('x') - 1)
455 >>> n1.hash() == n2.hash()
461 """Return a Python value that is equivalent to `self`."""
466 """Return `True` if `a` is an AST node.
470 >>> is_ast(IntVal(10))
474 >>> is_ast(BoolSort())
476 >>> is_ast(Function('f', IntSort(), IntSort()))
483 return isinstance(a, AstRef)
486 def eq(a : AstRef, b : AstRef) -> bool:
487 """Return `True` if `a` and `b` are structurally identical AST nodes.
497 >>> eq(simplify(x + 1), simplify(1 + x))
505 def _ast_kind(ctx : Context, a : Any) -> int:
511 def _ctx_from_ast_arg_list(args, default_ctx=None):
519 _z3_assert(ctx == a.ctx,
"Context mismatch")
525 def _ctx_from_ast_args(*args):
526 return _ctx_from_ast_arg_list(args)
529 def _to_func_decl_array(args):
531 _args = (FuncDecl * sz)()
533 _args[i] = args[i].as_func_decl()
537 def _to_ast_array(args):
541 _args[i] = args[i].as_ast()
545 def _to_ref_array(ref, args):
549 _args[i] = args[i].as_ast()
553 def _to_ast_ref(a, ctx):
554 k = _ast_kind(ctx, a)
556 return _to_sort_ref(a, ctx)
557 elif k == Z3_FUNC_DECL_AST:
558 return _to_func_decl_ref(a, ctx)
560 return _to_expr_ref(a, ctx)
569 def _sort_kind(ctx, s):
574 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node."""
583 """Return the Z3 internal kind of a sort.
584 This method can be used to test if `self` is one of the Z3 builtin sorts.
587 >>> b.kind() == Z3_BOOL_SORT
589 >>> b.kind() == Z3_INT_SORT
591 >>> A = ArraySort(IntSort(), IntSort())
592 >>> A.kind() == Z3_ARRAY_SORT
594 >>> A.kind() == Z3_INT_SORT
597 return _sort_kind(self.
ctx, self.
ast)
600 """Return `True` if `self` is a subsort of `other`.
602 >>> IntSort().subsort(RealSort())
608 """Try to cast `val` as an element of sort `self`.
610 This method is used in Z3Py to convert Python objects such as integers,
611 floats, longs and strings into Z3 expressions.
614 >>> RealSort().cast(x)
618 _z3_assert(
is_expr(val),
"Z3 expression expected")
619 _z3_assert(self.
eq(val.sort()),
"Sort mismatch")
623 """Return the name (string) of sort `self`.
625 >>> BoolSort().name()
627 >>> ArraySort(IntSort(), IntSort()).name()
633 """Return `True` if `self` and `other` are the same Z3 sort.
636 >>> p.sort() == BoolSort()
638 >>> p.sort() == IntSort()
646 """Return `True` if `self` and `other` are not the same Z3 sort.
649 >>> p.sort() != BoolSort()
651 >>> p.sort() != IntSort()
658 return AstRef.__hash__(self)
662 """Return `True` if `s` is a Z3 sort.
664 >>> is_sort(IntSort())
666 >>> is_sort(Int('x'))
668 >>> is_expr(Int('x'))
671 return isinstance(s, SortRef)
674 def _to_sort_ref(s, ctx):
676 _z3_assert(isinstance(s, Sort),
"Z3 Sort expected")
677 k = _sort_kind(ctx, s)
678 if k == Z3_BOOL_SORT:
680 elif k == Z3_INT_SORT
or k == Z3_REAL_SORT:
682 elif k == Z3_BV_SORT:
684 elif k == Z3_ARRAY_SORT:
686 elif k == Z3_DATATYPE_SORT:
688 elif k == Z3_FINITE_DOMAIN_SORT:
690 elif k == Z3_FLOATING_POINT_SORT:
692 elif k == Z3_ROUNDING_MODE_SORT:
694 elif k == Z3_RE_SORT:
696 elif k == Z3_SEQ_SORT:
698 elif k == Z3_CHAR_SORT:
700 elif k == Z3_TYPE_VAR:
705 def _sort(ctx : Context, a : Any) -> SortRef:
706 return _to_sort_ref(
Z3_get_sort(ctx.ref(), a), ctx)
710 """Create a new uninterpreted sort named `name`.
712 If `ctx=None`, then the new sort is declared in the global Z3Py context.
714 >>> A = DeclareSort('A')
715 >>> a = Const('a', A)
716 >>> b = Const('b', A)
728 """Type variable reference"""
738 """Create a new type variable named `name`.
740 If `ctx=None`, then the new sort is declared in the global Z3Py context.
755 """Function declaration. Every constant and function have an associated declaration.
757 The declaration assigns a name, a sort (i.e., type), and for function
758 the sort (i.e., type) of each of its arguments. Note that, in Z3,
759 a constant is a function with 0 arguments.
772 """Return the name of the function declaration `self`.
774 >>> f = Function('f', IntSort(), IntSort())
777 >>> isinstance(f.name(), str)
783 """Return the number of arguments of a function declaration.
784 If `self` is a constant, then `self.arity()` is 0.
786 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
793 """Return the sort of the argument `i` of a function declaration.
794 This method assumes that `0 <= i < self.arity()`.
796 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
805 """Return the sort of the range of a function declaration.
806 For constants, this is the sort of the constant.
808 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
815 """Return the internal kind of a function declaration.
816 It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
819 >>> d = (x + 1).decl()
820 >>> d.kind() == Z3_OP_ADD
822 >>> d.kind() == Z3_OP_MUL
830 result = [
None for i
in range(n)]
833 if k == Z3_PARAMETER_INT:
835 elif k == Z3_PARAMETER_DOUBLE:
837 elif k == Z3_PARAMETER_RATIONAL:
839 elif k == Z3_PARAMETER_SYMBOL:
841 elif k == Z3_PARAMETER_SORT:
843 elif k == Z3_PARAMETER_AST:
845 elif k == Z3_PARAMETER_FUNC_DECL:
847 elif k == Z3_PARAMETER_INTERNAL:
848 result[i] =
"internal parameter"
849 elif k == Z3_PARAMETER_ZSTRING:
850 result[i] =
"internal string"
856 """Create a Z3 application expression using the function `self`, and the given arguments.
858 The arguments must be Z3 expressions. This method assumes that
859 the sorts of the elements in `args` match the sorts of the
860 domain. Limited coercion is supported. For example, if
861 args[0] is a Python integer, and the function expects a Z3
862 integer, then the argument is automatically converted into a
865 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
873 args = _get_args(args)
875 _args = (Ast * num)()
880 tmp = self.
domain(i).cast(args[i])
882 _args[i] = tmp.as_ast()
887 """Return `True` if `a` is a Z3 function declaration.
889 >>> f = Function('f', IntSort(), IntSort())
896 return isinstance(a, FuncDeclRef)
900 """Create a new Z3 uninterpreted function with the given sorts.
902 >>> f = Function('f', IntSort(), IntSort())
908 _z3_assert(len(sig) > 0,
"At least two arguments expected")
912 _z3_assert(
is_sort(rng),
"Z3 sort expected")
913 dom = (Sort * arity)()
914 for i
in range(arity):
916 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
923 """Create a new fresh Z3 uninterpreted function with the given sorts.
927 _z3_assert(len(sig) > 0,
"At least two arguments expected")
931 _z3_assert(
is_sort(rng),
"Z3 sort expected")
932 dom = (z3.Sort * arity)()
933 for i
in range(arity):
935 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
941 def _to_func_decl_ref(a, ctx):
946 """Create a new Z3 recursive with the given sorts."""
949 _z3_assert(len(sig) > 0,
"At least two arguments expected")
953 _z3_assert(
is_sort(rng),
"Z3 sort expected")
954 dom = (Sort * arity)()
955 for i
in range(arity):
957 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
964 """Set the body of a recursive function.
965 Recursive definitions can be simplified if they are applied to ground
968 >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
969 >>> n = Int('n', ctx)
970 >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
973 >>> s = Solver(ctx=ctx)
974 >>> s.add(fac(n) < 3)
977 >>> s.model().eval(fac(5))
983 args = _get_args(args)
987 _args[i] = args[i].ast
998 """Constraints, formulas and terms are expressions in Z3.
1000 Expressions are ASTs. Every expression has a sort.
1001 There are three main kinds of expressions:
1002 function applications, quantifiers and bounded variables.
1003 A constant is a function application with 0 arguments.
1004 For quantifier free problems, all expressions are
1005 function applications.
1015 """Return the sort of expression `self`.
1027 """Shorthand for `self.sort().kind()`.
1029 >>> a = Array('a', IntSort(), IntSort())
1030 >>> a.sort_kind() == Z3_ARRAY_SORT
1032 >>> a.sort_kind() == Z3_INT_SORT
1038 """Return a Z3 expression that represents the constraint `self == other`.
1040 If `other` is `None`, then this method simply returns `False`.
1051 a, b = _coerce_exprs(self, other)
1056 return AstRef.__hash__(self)
1059 """Return a Z3 expression that represents the constraint `self != other`.
1061 If `other` is `None`, then this method simply returns `True`.
1072 a, b = _coerce_exprs(self, other)
1073 _args, sz = _to_ast_array((a, b))
1080 """Return the Z3 function declaration associated with a Z3 application.
1082 >>> f = Function('f', IntSort(), IntSort())
1091 _z3_assert(
is_app(self),
"Z3 application expected")
1095 """Return the Z3 internal kind of a function application."""
1097 _z3_assert(
is_app(self),
"Z3 application expected")
1102 """Return the number of arguments of a Z3 application.
1106 >>> (a + b).num_args()
1108 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1114 _z3_assert(
is_app(self),
"Z3 application expected")
1118 """Return argument `idx` of the application `self`.
1120 This method assumes that `self` is a function application with at least `idx+1` arguments.
1124 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1134 _z3_assert(
is_app(self),
"Z3 application expected")
1135 _z3_assert(idx < self.
num_args(),
"Invalid argument index")
1139 """Return a list containing the children of the given expression
1143 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1163 """inverse function to the serialize method on ExprRef.
1164 It is made available to make it easier for users to serialize expressions back and forth between
1165 strings. Solvers can be serialized using the 'sexpr()' method.
1169 if len(s.assertions()) != 1:
1170 raise Z3Exception(
"single assertion expected")
1171 fml = s.assertions()[0]
1172 if fml.num_args() != 1:
1173 raise Z3Exception(
"dummy function 'F' expected")
1176 def _to_expr_ref(a, ctx):
1177 if isinstance(a, Pattern):
1181 if k == Z3_QUANTIFIER_AST:
1184 if sk == Z3_BOOL_SORT:
1186 if sk == Z3_INT_SORT:
1187 if k == Z3_NUMERAL_AST:
1190 if sk == Z3_REAL_SORT:
1191 if k == Z3_NUMERAL_AST:
1193 if _is_algebraic(ctx, a):
1196 if sk == Z3_BV_SORT:
1197 if k == Z3_NUMERAL_AST:
1201 if sk == Z3_ARRAY_SORT:
1203 if sk == Z3_DATATYPE_SORT:
1205 if sk == Z3_FLOATING_POINT_SORT:
1206 if k == Z3_APP_AST
and _is_numeral(ctx, a):
1209 return FPRef(a, ctx)
1210 if sk == Z3_FINITE_DOMAIN_SORT:
1211 if k == Z3_NUMERAL_AST:
1215 if sk == Z3_ROUNDING_MODE_SORT:
1217 if sk == Z3_SEQ_SORT:
1219 if sk == Z3_CHAR_SORT:
1221 if sk == Z3_RE_SORT:
1222 return ReRef(a, ctx)
1226 def _coerce_expr_merge(s, a):
1239 _z3_assert(s1.ctx == s.ctx,
"context mismatch")
1240 _z3_assert(
False,
"sort mismatch")
1245 def _coerce_exprs(a, b, ctx=None):
1247 a = _py2expr(a, ctx)
1248 b = _py2expr(b, ctx)
1249 if isinstance(a, str)
and isinstance(b, SeqRef):
1251 if isinstance(b, str)
and isinstance(a, SeqRef):
1253 if isinstance(a, float)
and isinstance(b, ArithRef):
1255 if isinstance(b, float)
and isinstance(a, ArithRef):
1259 s = _coerce_expr_merge(s, a)
1260 s = _coerce_expr_merge(s, b)
1266 def _reduce(func, sequence, initial):
1268 for element
in sequence:
1269 result = func(result, element)
1273 def _coerce_expr_list(alist, ctx=None):
1280 alist = [_py2expr(a, ctx)
for a
in alist]
1281 s = _reduce(_coerce_expr_merge, alist,
None)
1282 return [s.cast(a)
for a
in alist]
1286 """Return `True` if `a` is a Z3 expression.
1293 >>> is_expr(IntSort())
1297 >>> is_expr(IntVal(1))
1300 >>> is_expr(ForAll(x, x >= 0))
1302 >>> is_expr(FPVal(1.0))
1305 return isinstance(a, ExprRef)
1309 """Return `True` if `a` is a Z3 function application.
1311 Note that, constants are function applications with 0 arguments.
1318 >>> is_app(IntSort())
1322 >>> is_app(IntVal(1))
1325 >>> is_app(ForAll(x, x >= 0))
1328 if not isinstance(a, ExprRef):
1330 k = _ast_kind(a.ctx, a)
1331 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
1335 """Return `True` if `a` is Z3 constant/variable expression.
1344 >>> is_const(IntVal(1))
1347 >>> is_const(ForAll(x, x >= 0))
1350 return is_app(a)
and a.num_args() == 0
1354 """Return `True` if `a` is variable.
1356 Z3 uses de-Bruijn indices for representing bound variables in
1364 >>> f = Function('f', IntSort(), IntSort())
1365 >>> # Z3 replaces x with bound variables when ForAll is executed.
1366 >>> q = ForAll(x, f(x) == x)
1372 >>> is_var(b.arg(1))
1375 return is_expr(a)
and _ast_kind(a.ctx, a) == Z3_VAR_AST
1379 """Return the de-Bruijn index of the Z3 bounded variable `a`.
1387 >>> f = Function('f', IntSort(), IntSort(), IntSort())
1388 >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1389 >>> q = ForAll([x, y], f(x, y) == x + y)
1391 f(Var(1), Var(0)) == Var(1) + Var(0)
1395 >>> v1 = b.arg(0).arg(0)
1396 >>> v2 = b.arg(0).arg(1)
1401 >>> get_var_index(v1)
1403 >>> get_var_index(v2)
1407 _z3_assert(
is_var(a),
"Z3 bound variable expected")
1412 """Return `True` if `a` is an application of the given kind `k`.
1416 >>> is_app_of(n, Z3_OP_ADD)
1418 >>> is_app_of(n, Z3_OP_MUL)
1421 return is_app(a)
and a.kind() == k
1424 def If(a, b, c, ctx=None):
1425 """Create a Z3 if-then-else expression.
1429 >>> max = If(x > y, x, y)
1435 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1436 return Cond(a, b, c, ctx)
1438 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1441 b, c = _coerce_exprs(b, c, ctx)
1443 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1444 return _to_expr_ref(
Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1448 """Create a Z3 distinct expression.
1455 >>> Distinct(x, y, z)
1457 >>> simplify(Distinct(x, y, z))
1459 >>> simplify(Distinct(x, y, z), blast_distinct=True)
1460 And(Not(x == y), Not(x == z), Not(y == z))
1462 args = _get_args(args)
1463 ctx = _ctx_from_ast_arg_list(args)
1465 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1466 args = _coerce_expr_list(args, ctx)
1467 _args, sz = _to_ast_array(args)
1471 def _mk_bin(f, a, b):
1474 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1475 args[0] = a.as_ast()
1476 args[1] = b.as_ast()
1477 return f(a.ctx.ref(), 2, args)
1481 """Create a constant of the given sort.
1483 >>> Const('x', IntSort())
1487 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
1493 """Create several constants of the given sort.
1495 `names` is a string containing the names of all constants to be created.
1496 Blank spaces separate the names of different constants.
1498 >>> x, y, z = Consts('x y z', IntSort())
1502 if isinstance(names, str):
1503 names = names.split(
" ")
1504 return [
Const(name, sort)
for name
in names]
1508 """Create a fresh constant of a specified sort"""
1509 ctx = _get_ctx(sort.ctx)
1513 def Var(idx : int, s : SortRef) -> ExprRef:
1514 """Create a Z3 free variable. Free variables are used to create quantified formulas.
1515 A free variable with index n is bound when it occurs within the scope of n+1 quantified
1518 >>> Var(0, IntSort())
1520 >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1524 _z3_assert(
is_sort(s),
"Z3 sort expected")
1525 return _to_expr_ref(
Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1530 Create a real free variable. Free variables are used to create quantified formulas.
1531 They are also used to create polynomials.
1540 Create a list of Real free variables.
1541 The variables have ids: 0, 1, ..., n-1
1543 >>> x0, x1, x2, x3 = RealVarVector(4)
1560 """Try to cast `val` as a Boolean.
1562 >>> x = BoolSort().cast(True)
1572 if isinstance(val, bool):
1576 msg =
"True, False or Z3 Boolean expression expected. Received %s of type %s"
1577 _z3_assert(
is_expr(val), msg % (val, type(val)))
1578 if not self.
eq(val.sort()):
1579 _z3_assert(self.
eq(val.sort()),
"Value cannot be converted into a Z3 Boolean value")
1583 return isinstance(other, ArithSortRef)
1593 """All Boolean expressions are instances of this class."""
1599 if isinstance(other, BoolRef):
1600 other =
If(other, 1, 0)
1601 return If(self, 1, 0) + other
1610 """Create the Z3 expression `self * other`.
1612 if isinstance(other, int)
and other == 1:
1613 return If(self, 1, 0)
1614 if isinstance(other, int)
and other == 0:
1616 if isinstance(other, BoolRef):
1617 other =
If(other, 1, 0)
1618 return If(self, other, 0)
1621 return And(self, other)
1624 return Or(self, other)
1627 return Xor(self, other)
1643 """Return `True` if `a` is a Z3 Boolean expression.
1649 >>> is_bool(And(p, q))
1657 return isinstance(a, BoolRef)
1661 """Return `True` if `a` is the Z3 true expression.
1666 >>> is_true(simplify(p == p))
1671 >>> # True is a Python Boolean expression
1679 """Return `True` if `a` is the Z3 false expression.
1686 >>> is_false(BoolVal(False))
1693 """Return `True` if `a` is a Z3 and expression.
1695 >>> p, q = Bools('p q')
1696 >>> is_and(And(p, q))
1698 >>> is_and(Or(p, q))
1705 """Return `True` if `a` is a Z3 or expression.
1707 >>> p, q = Bools('p q')
1710 >>> is_or(And(p, q))
1717 """Return `True` if `a` is a Z3 implication expression.
1719 >>> p, q = Bools('p q')
1720 >>> is_implies(Implies(p, q))
1722 >>> is_implies(And(p, q))
1729 """Return `True` if `a` is a Z3 not expression.
1741 """Return `True` if `a` is a Z3 equality expression.
1743 >>> x, y = Ints('x y')
1751 """Return `True` if `a` is a Z3 distinct expression.
1753 >>> x, y, z = Ints('x y z')
1754 >>> is_distinct(x == y)
1756 >>> is_distinct(Distinct(x, y, z))
1763 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1767 >>> p = Const('p', BoolSort())
1770 >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1777 return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1780 def BoolVal(val, ctx=None):
1781 """Return the Boolean value `
True`
or `
False`. If `ctx=
None`, then the
global context
is used.
1794 return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1796 return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1799 def Bool(name, ctx=None):
1800 """Return a Boolean constant named `name`. If `ctx=
None`, then the
global context
is used.
1808 return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1811 def Bools(names, ctx=None):
1812 """Return a tuple of Boolean constants.
1814 `names`
is a single string containing all names separated by blank spaces.
1815 If `ctx=
None`, then the
global context
is used.
1817 >>> p, q, r =
Bools(
'p q r')
1818 >>>
And(p,
Or(q, r))
1822 if isinstance(names, str):
1823 names = names.split(" ")
1824 return [Bool(name, ctx) for name in names]
1827 def BoolVector(prefix, sz, ctx=None):
1828 """Return a list of Boolean constants of size `sz`.
1830 The constants are named using the given prefix.
1831 If `ctx=
None`, then the
global context
is used.
1837 And(p__0, p__1, p__2)
1839 return [Bool("%s__%s" % (prefix, i)) for i in range(sz)]
1842 def FreshBool(prefix="b", ctx=None):
1843 """Return a fresh Boolean constant
in the given context using the given prefix.
1845 If `ctx=
None`, then the
global context
is used.
1853 return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1856 def Implies(a, b, ctx=None):
1857 """Create a Z3 implies expression.
1859 >>> p, q =
Bools(
'p q')
1863 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1867 return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1870 def Xor(a, b, ctx=None):
1871 """Create a Z3 Xor expression.
1873 >>> p, q =
Bools(
'p q')
1879 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1883 return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1886 def Not(a, ctx=None):
1887 """Create a Z3
not expression
or probe.
1895 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1897 # Not is also used to build probes
1898 return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
1902 return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
1912 def _has_probe(args):
1913 """Return `
True`
if one of the elements of the given collection
is a Z3 probe.
"""
1921 """Create a Z3
and-expression
or and-probe.
1923 >>> p, q, r =
Bools(
'p q r')
1928 And(p__0, p__1, p__2, p__3, p__4)
1932 last_arg = args[len(args) - 1]
1933 if isinstance(last_arg, Context):
1934 ctx = args[len(args) - 1]
1935 args = args[:len(args) - 1]
1936 elif len(args) == 1 and isinstance(args[0], AstVector):
1938 args = [a for a in args[0]]
1941 args = _get_args(args)
1942 ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1944 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1945 if _has_probe(args):
1946 return _probe_and(args, ctx)
1948 args = _coerce_expr_list(args, ctx)
1949 _args, sz = _to_ast_array(args)
1950 return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1954 """Create a Z3
or-expression
or or-probe.
1956 >>> p, q, r =
Bools(
'p q r')
1961 Or(p__0, p__1, p__2, p__3, p__4)
1965 last_arg = args[len(args) - 1]
1966 if isinstance(last_arg, Context):
1967 ctx = args[len(args) - 1]
1968 args = args[:len(args) - 1]
1969 elif len(args) == 1 and isinstance(args[0], AstVector):
1971 args = [a for a in args[0]]
1974 args = _get_args(args)
1975 ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1977 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
1978 if _has_probe(args):
1979 return _probe_or(args, ctx)
1981 args = _coerce_expr_list(args, ctx)
1982 _args, sz = _to_ast_array(args)
1983 return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
1985 #########################################
1989 #########################################
1992 class PatternRef(ExprRef):
1993 """Patterns are hints
for quantifier instantiation.
1998 return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
2001 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
2005 """Return `
True`
if `a`
is a Z3 pattern (hint
for quantifier instantiation.
2009 >>> q =
ForAll(x, f(x) == 0, patterns = [ f(x) ])
2012 >>> q.num_patterns()
2019 return isinstance(a, PatternRef)
2022 def MultiPattern(*args):
2023 """Create a Z3 multi-pattern using the given expressions `*args`
2031 >>> q.num_patterns()
2039 _z3_assert(len(args) > 0, "At least one argument expected")
2040 _z3_assert(all([is_expr(a) for a in args]), "Z3 expressions expected")
2042 args, sz = _to_ast_array(args)
2043 return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
2046 def _to_pattern(arg):
2050 return MultiPattern(arg)
2052 #########################################
2056 #########################################
2059 class QuantifierRef(BoolRef):
2060 """Universally
and Existentially quantified formulas.
"""
2066 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
2069 """Return the Boolean sort
or sort of Lambda.
"""
2070 if self.is_lambda():
2071 return _sort(self.ctx, self.as_ast())
2072 return BoolSort(self.ctx)
2074 def is_forall(self):
2075 """Return `
True`
if `self`
is a universal quantifier.
2079 >>> q =
ForAll(x, f(x) == 0)
2082 >>> q =
Exists(x, f(x) != 0)
2086 return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
2088 def is_exists(self):
2089 """Return `
True`
if `self`
is an existential quantifier.
2093 >>> q =
ForAll(x, f(x) == 0)
2096 >>> q =
Exists(x, f(x) != 0)
2100 return Z3_is_quantifier_exists(self.ctx_ref(), self.ast)
2102 def is_lambda(self):
2103 """Return `
True`
if `self`
is a
lambda expression.
2110 >>> q =
Exists(x, f(x) != 0)
2114 return Z3_is_lambda(self.ctx_ref(), self.ast)
2116 def __getitem__(self, arg):
2117 """Return the Z3 expression `self[arg]`.
2120 _z3_assert(self.is_lambda(), "quantifier should be a lambda expression")
2121 return _array_select(self, arg)
2124 """Return the weight annotation of `self`.
2128 >>> q =
ForAll(x, f(x) == 0)
2131 >>> q =
ForAll(x, f(x) == 0, weight=10)
2135 return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
2137 def skolem_id(self):
2138 """Return the skolem id of `self`.
2140 return _symbol2py(self.ctx, Z3_get_quantifier_skolem_id(self.ctx_ref(), self.ast))
2143 """Return the quantifier id of `self`.
2145 return _symbol2py(self.ctx, Z3_get_quantifier_id(self.ctx_ref(), self.ast))
2147 def num_patterns(self):
2148 """Return the number of patterns (i.e., quantifier instantiation hints)
in `self`.
2153 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2154 >>> q.num_patterns()
2157 return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
2159 def pattern(self, idx):
2160 """Return a pattern (i.e., quantifier instantiation hints)
in `self`.
2165 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2166 >>> q.num_patterns()
2174 _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
2175 return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
2177 def num_no_patterns(self):
2178 """Return the number of no-patterns.
"""
2179 return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
2181 def no_pattern(self, idx):
2182 """Return a no-pattern.
"""
2184 _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
2185 return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
2188 """Return the expression being quantified.
2192 >>> q =
ForAll(x, f(x) == 0)
2196 return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
2199 """Return the number of variables bounded by this quantifier.
2204 >>> q =
ForAll([x, y], f(x, y) >= x)
2208 return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
2210 def var_name(self, idx):
2211 """Return a string representing a name used when displaying the quantifier.
2216 >>> q =
ForAll([x, y], f(x, y) >= x)
2223 _z3_assert(idx < self.num_vars(), "Invalid variable idx")
2224 return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
2226 def var_sort(self, idx):
2227 """Return the sort of a bound variable.
2232 >>> q =
ForAll([x, y], f(x, y) >= x)
2239 _z3_assert(idx < self.num_vars(), "Invalid variable idx")
2240 return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
2243 """Return a list containing a single element self.
body()
2247 >>> q =
ForAll(x, f(x) == 0)
2251 return [self.body()]
2254 def is_quantifier(a):
2255 """Return `
True`
if `a`
is a Z3 quantifier.
2259 >>> q =
ForAll(x, f(x) == 0)
2265 return isinstance(a, QuantifierRef)
2268 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2270 _z3_assert(is_bool(body) or is_app(vs) or (len(vs) > 0 and is_app(vs[0])), "Z3 expression expected")
2271 _z3_assert(is_const(vs) or (len(vs) > 0 and all([is_const(v) for v in vs])), "Invalid bounded variable(s)")
2272 _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected")
2273 _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions")
2279 if not is_expr(body):
2280 body = BoolVal(body, ctx)
2284 _vs = (Ast * num_vars)()
2285 for i in range(num_vars):
2286 # TODO: Check if is constant
2287 _vs[i] = vs[i].as_ast()
2288 patterns = [_to_pattern(p) for p in patterns]
2289 num_pats = len(patterns)
2290 _pats = (Pattern * num_pats)()
2291 for i in range(num_pats):
2292 _pats[i] = patterns[i].ast
2293 _no_pats, num_no_pats = _to_ast_array(no_patterns)
2294 qid = to_symbol(qid, ctx)
2295 skid = to_symbol(skid, ctx)
2296 return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid,
2299 num_no_pats, _no_pats,
2300 body.as_ast()), ctx)
2303 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2304 """Create a Z3 forall formula.
2306 The parameters `weight`, `qid`, `skid`, `patterns`
and `no_patterns` are optional annotations.
2311 >>>
ForAll([x, y], f(x, y) >= x)
2312 ForAll([x, y], f(x, y) >= x)
2313 >>>
ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2314 ForAll([x, y], f(x, y) >= x)
2315 >>>
ForAll([x, y], f(x, y) >= x, weight=10)
2316 ForAll([x, y], f(x, y) >= x)
2318 return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
2321 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2322 """Create a Z3 exists formula.
2324 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
2330 >>> q =
Exists([x, y], f(x, y) >= x, skid=
"foo")
2332 Exists([x, y], f(x, y) >= x)
2335 >>> r =
Tactic(
'nnf')(q).as_expr()
2339 return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
2342 def Lambda(vs, body):
2343 """Create a Z3
lambda expression.
2347 >>> lo, hi, e, i =
Ints(
'lo hi e i')
2348 >>> mem1 =
Lambda([i],
If(
And(lo <= i, i <= hi), e, mem0[i]))
2356 _vs = (Ast * num_vars)()
2357 for i in range(num_vars):
2358 # TODO: Check if is constant
2359 _vs[i] = vs[i].as_ast()
2360 return QuantifierRef(Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx)
2362 #########################################
2366 #########################################
2369 class ArithSortRef(SortRef):
2370 """Real
and Integer sorts.
"""
2373 """Return `
True`
if `self`
is of the sort Real.
2384 return self.kind() == Z3_REAL_SORT
2387 """Return `
True`
if `self`
is of the sort Integer.
2398 return self.kind() == Z3_INT_SORT
2403 def subsort(self, other):
2404 """Return `
True`
if `self`
is a subsort of `other`.
"""
2405 return self.is_int() and is_arith_sort(other) and other.is_real()
2407 def cast(self, val):
2408 """Try to cast `val`
as an Integer
or Real.
2423 _z3_assert(self.ctx == val.ctx, "Context mismatch")
2427 if val_s.is_int() and self.is_real():
2429 if val_s.is_bool() and self.is_int():
2430 return If(val, 1, 0)
2431 if val_s.is_bool() and self.is_real():
2432 return ToReal(If(val, 1, 0))
2434 _z3_assert(False, "Z3 Integer/Real expression expected")
2437 return IntVal(val, self.ctx)
2439 return RealVal(val, self.ctx)
2441 msg = "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s"
2442 _z3_assert(False, msg % self)
2445 def is_arith_sort(s : Any) -> bool:
2446 """Return `
True`
if s
is an arithmetical sort (type).
2454 >>> n =
Int(
'x') + 1
2458 return isinstance(s, ArithSortRef)
2461 class ArithRef(ExprRef):
2462 """Integer
and Real expressions.
"""
2465 """Return the sort (type) of the arithmetical expression `self`.
2472 return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
2475 """Return `
True`
if `self`
is an integer expression.
2486 return self.sort().is_int()
2489 """Return `
True`
if `self`
is an real expression.
2497 return self.sort().is_real()
2499 def __add__(self, other):
2500 """Create the Z3 expression `self + other`.
2509 a, b = _coerce_exprs(self, other)
2510 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
2512 def __radd__(self, other):
2513 """Create the Z3 expression `other + self`.
2519 a, b = _coerce_exprs(self, other)
2520 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
2522 def __mul__(self, other):
2523 """Create the Z3 expression `self * other`.
2532 if isinstance(other, BoolRef):
2533 return If(other, self, 0)
2534 a, b = _coerce_exprs(self, other)
2535 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
2537 def __rmul__(self, other):
2538 """Create the Z3 expression `other * self`.
2544 a, b = _coerce_exprs(self, other)
2545 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
2547 def __sub__(self, other):
2548 """Create the Z3 expression `self - other`.
2557 a, b = _coerce_exprs(self, other)
2558 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
2560 def __rsub__(self, other):
2561 """Create the Z3 expression `other - self`.
2567 a, b = _coerce_exprs(self, other)
2568 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
2570 def __pow__(self, other):
2571 """Create the Z3 expression `self**other` (**
is the power operator).
2581 a, b = _coerce_exprs(self, other)
2582 return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2584 def __rpow__(self, other):
2585 """Create the Z3 expression `other**self` (**
is the power operator).
2595 a, b = _coerce_exprs(self, other)
2596 return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2598 def __div__(self, other):
2599 """Create the Z3 expression `other/self`.
2618 a, b = _coerce_exprs(self, other)
2619 return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2621 def __truediv__(self, other):
2622 """Create the Z3 expression `other/self`.
"""
2623 return self.__div__(other)
2625 def __rdiv__(self, other):
2626 """Create the Z3 expression `other/self`.
2639 a, b = _coerce_exprs(self, other)
2640 return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2642 def __rtruediv__(self, other):
2643 """Create the Z3 expression `other/self`.
"""
2644 return self.__rdiv__(other)
2646 def __mod__(self, other):
2647 """Create the Z3 expression `other%self`.
2656 a, b = _coerce_exprs(self, other)
2658 _z3_assert(a.is_int(), "Z3 integer expression expected")
2659 return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2661 def __rmod__(self, other):
2662 """Create the Z3 expression `other%self`.
2668 a, b = _coerce_exprs(self, other)
2670 _z3_assert(a.is_int(), "Z3 integer expression expected")
2671 return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2674 """Return an expression representing `-self`.
2682 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
2693 def __le__(self, other):
2694 """Create the Z3 expression `other <= self`.
2696 >>> x, y =
Ints(
'x y')
2703 a, b = _coerce_exprs(self, other)
2704 return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2706 def __lt__(self, other):
2707 """Create the Z3 expression `other < self`.
2709 >>> x, y =
Ints(
'x y')
2716 a, b = _coerce_exprs(self, other)
2717 return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2719 def __gt__(self, other):
2720 """Create the Z3 expression `other > self`.
2722 >>> x, y =
Ints(
'x y')
2729 a, b = _coerce_exprs(self, other)
2730 return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2732 def __ge__(self, other):
2733 """Create the Z3 expression `other >= self`.
2735 >>> x, y =
Ints(
'x y')
2742 a, b = _coerce_exprs(self, other)
2743 return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2747 """Return `
True`
if `a`
is an arithmetical expression.
2764 return isinstance(a, ArithRef)
2767 def is_int(a) -> bool:
2768 """Return `
True`
if `a`
is an integer expression.
2783 return is_arith(a) and a.is_int()
2787 """Return `
True`
if `a`
is a real expression.
2802 return is_arith(a) and a.is_real()
2805 def _is_numeral(ctx, a):
2806 return Z3_is_numeral_ast(ctx.ref(), a)
2809 def _is_algebraic(ctx, a):
2810 return Z3_is_algebraic_number(ctx.ref(), a)
2813 def is_int_value(a):
2814 """Return `
True`
if `a`
is an integer value of sort Int.
2822 >>> n =
Int(
'x') + 1
2834 return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2837 def is_rational_value(a):
2838 """Return `
True`
if `a`
is rational value of sort Real.
2848 >>> n =
Real(
'x') + 1
2856 return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2859 def is_algebraic_value(a):
2860 """Return `
True`
if `a`
is an algebraic value of sort Real.
2870 return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2873 def is_add(a : Any) -> bool:
2874 """Return `
True`
if `a`
is an expression of the form b + c.
2876 >>> x, y =
Ints(
'x y')
2882 return is_app_of(a, Z3_OP_ADD)
2885 def is_mul(a : Any) -> bool:
2886 """Return `
True`
if `a`
is an expression of the form b * c.
2888 >>> x, y =
Ints(
'x y')
2894 return is_app_of(a, Z3_OP_MUL)
2897 def is_sub(a : Any) -> bool:
2898 """Return `
True`
if `a`
is an expression of the form b - c.
2900 >>> x, y =
Ints(
'x y')
2906 return is_app_of(a, Z3_OP_SUB)
2909 def is_div(a : Any) -> bool:
2910 """Return `
True`
if `a`
is an expression of the form b / c.
2912 >>> x, y =
Reals(
'x y')
2917 >>> x, y =
Ints(
'x y')
2923 return is_app_of(a, Z3_OP_DIV)
2926 def is_idiv(a : Any) -> bool:
2927 """Return `
True`
if `a`
is an expression of the form b div c.
2929 >>> x, y =
Ints(
'x y')
2935 return is_app_of(a, Z3_OP_IDIV)
2938 def is_mod(a : Any) -> bool:
2939 """Return `
True`
if `a`
is an expression of the form b % c.
2941 >>> x, y =
Ints(
'x y')
2947 return is_app_of(a, Z3_OP_MOD)
2950 def is_le(a : Any) -> bool:
2951 """Return `
True`
if `a`
is an expression of the form b <= c.
2953 >>> x, y =
Ints(
'x y')
2959 return is_app_of(a, Z3_OP_LE)
2962 def is_lt(a : Any) -> bool:
2963 """Return `
True`
if `a`
is an expression of the form b < c.
2965 >>> x, y =
Ints(
'x y')
2971 return is_app_of(a, Z3_OP_LT)
2974 def is_ge(a : Any) -> bool:
2975 """Return `
True`
if `a`
is an expression of the form b >= c.
2977 >>> x, y =
Ints(
'x y')
2983 return is_app_of(a, Z3_OP_GE)
2986 def is_gt(a : Any) -> bool:
2987 """Return `
True`
if `a`
is an expression of the form b > c.
2989 >>> x, y =
Ints(
'x y')
2995 return is_app_of(a, Z3_OP_GT)
2998 def is_is_int(a : Any) -> bool:
2999 """Return `
True`
if `a`
is an expression of the form
IsInt(b).
3007 return is_app_of(a, Z3_OP_IS_INT)
3010 def is_to_real(a : Any) -> bool:
3011 """Return `
True`
if `a`
is an expression of the form
ToReal(b).
3022 return is_app_of(a, Z3_OP_TO_REAL)
3025 def is_to_int(a : Any) -> bool:
3026 """Return `
True`
if `a`
is an expression of the form
ToInt(b).
3037 return is_app_of(a, Z3_OP_TO_INT)
3040 class IntNumRef(ArithRef):
3041 """Integer values.
"""
3044 """Return a Z3 integer numeral
as a Python long (bignum) numeral.
3053 _z3_assert(self.is_int(), "Integer value expected")
3054 return int(self.as_string())
3056 def as_string(self):
3057 """Return a Z3 integer numeral
as a Python string.
3062 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
3064 def as_binary_string(self):
3065 """Return a Z3 integer numeral
as a Python binary string.
3067 >>> v.as_binary_string()
3070 return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
3073 return self.as_long()
3076 class RatNumRef(ArithRef):
3077 """Rational values.
"""
3079 def numerator(self):
3080 """ Return the numerator of a Z3 rational numeral.
3092 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
3094 def denominator(self):
3095 """ Return the denominator of a Z3 rational numeral.
3103 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
3105 def numerator_as_long(self):
3106 """ Return the numerator
as a Python long.
3113 >>> v.numerator_as_long() + 1 == 10000000001
3116 return self.numerator().as_long()
3118 def denominator_as_long(self):
3119 """ Return the denominator
as a Python long.
3124 >>> v.denominator_as_long()
3127 return self.denominator().as_long()
3135 def is_int_value(self):
3136 return self.denominator().is_int() and self.denominator_as_long() == 1
3139 _z3_assert(self.is_int_value(), "Expected integer fraction")
3140 return self.numerator_as_long()
3142 def as_decimal(self, prec):
3143 """ Return a Z3 rational value
as a string
in decimal notation using at most `prec` decimal places.
3152 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
3154 def as_string(self):
3155 """Return a Z3 rational numeral
as a Python string.
3161 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
3163 def as_fraction(self):
3164 """Return a Z3 rational
as a Python Fraction object.
3170 return Fraction(self.numerator_as_long(), self.denominator_as_long())
3173 return Z3_get_numeral_double(self.ctx_ref(), self.as_ast())
3176 class AlgebraicNumRef(ArithRef):
3177 """Algebraic irrational values.
"""
3179 def approx(self, precision=10):
3180 """Return a Z3 rational number that approximates the algebraic number `self`.
3181 The result `r`
is such that |r - self| <= 1/10^precision
3185 6838717160008073720548335/4835703278458516698824704
3189 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
3191 def as_decimal(self, prec):
3192 """Return a string representation of the algebraic number `self`
in decimal notation
3193 using `prec` decimal places.
3196 >>> x.as_decimal(10)
3198 >>> x.as_decimal(20)
3199 '1.41421356237309504880?'
3201 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
3204 return AstVector(Z3_algebraic_get_poly(self.ctx_ref(), self.as_ast()), self.ctx)
3207 return Z3_algebraic_get_i(self.ctx_ref(), self.as_ast())
3210 def _py2expr(a, ctx=None):
3211 if isinstance(a, bool):
3212 return BoolVal(a, ctx)
3214 return IntVal(a, ctx)
3215 if isinstance(a, float):
3216 return RealVal(a, ctx)
3217 if isinstance(a, str):
3218 return StringVal(a, ctx)
3222 _z3_assert(False, "Python bool, int, long or float expected")
3225 def IntSort(ctx=None):
3226 """Return the integer sort
in the given context. If `ctx=
None`, then the
global context
is used.
3239 return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
3242 def RealSort(ctx=None):
3243 """Return the real sort
in the given context. If `ctx=
None`, then the
global context
is used.
3256 return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)
3259 def _to_int_str(val):
3260 if isinstance(val, float):
3261 return str(int(val))
3262 elif isinstance(val, bool):
3271 def IntVal(val, ctx=None):
3272 """Return a Z3 integer value. If `ctx=
None`, then the
global context
is used.
3280 return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
3283 def RealVal(val, ctx=None):
3284 """Return a Z3 real value.
3286 `val` may be a Python int, long, float
or string representing a number
in decimal
or rational notation.
3287 If `ctx=
None`, then the
global context
is used.
3299 return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
3302 def RatVal(a, b, ctx=None):
3303 """Return a Z3 rational a/b.
3305 If `ctx=
None`, then the
global context
is used.
3313 _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
3314 _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
3315 return simplify(RealVal(a, ctx) / RealVal(b, ctx))
3318 def Q(a, b, ctx=None):
3319 """Return a Z3 rational a/b.
3321 If `ctx=
None`, then the
global context
is used.
3328 return simplify(RatVal(a, b, ctx=ctx))
3331 def Int(name, ctx=None):
3332 """Return an integer constant named `name`. If `ctx=
None`, then the
global context
is used.
3341 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
3344 def Ints(names, ctx=None):
3345 """Return a tuple of Integer constants.
3347 >>> x, y, z =
Ints(
'x y z')
3352 if isinstance(names, str):
3353 names = names.split(" ")
3354 return [Int(name, ctx) for name in names]
3357 def IntVector(prefix, sz, ctx=None):
3358 """Return a list of integer constants of size `sz`.
3367 return [Int("%s__%s" % (prefix, i), ctx) for i in range(sz)]
3370 def FreshInt(prefix="x", ctx=None):
3371 """Return a fresh integer constant
in the given context using the given prefix.
3381 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
3384 def Real(name, ctx=None):
3385 """Return a real constant named `name`. If `ctx=
None`, then the
global context
is used.
3394 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)
3397 def Reals(names, ctx=None):
3398 """Return a tuple of real constants.
3400 >>> x, y, z =
Reals(
'x y z')
3403 >>>
Sum(x, y, z).sort()
3407 if isinstance(names, str):
3408 names = names.split(" ")
3409 return [Real(name, ctx) for name in names]
3412 def RealVector(prefix, sz, ctx=None):
3413 """Return a list of real constants of size `sz`.
3424 return [Real("%s__%s" % (prefix, i), ctx) for i in range(sz)]
3427 def FreshReal(prefix="b", ctx=None):
3428 """Return a fresh real constant
in the given context using the given prefix.
3438 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
3442 """ Return the Z3 expression
ToReal(a).
3454 if isinstance(a, BoolRef):
3455 return If(a, RealVal(1, ctx), RealVal(0, ctx))
3457 _z3_assert(a.is_int(), "Z3 integer expression expected.")
3458 return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
3462 """ Return the Z3 expression
ToInt(a).
3474 _z3_assert(a.is_real(), "Z3 real expression expected.")
3476 return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)
3480 """ Return the Z3 predicate
IsInt(a).
3483 >>>
IsInt(x +
"1/2")
3487 >>>
solve(
IsInt(x +
"1/2"), x > 0, x < 1, x !=
"1/2")
3491 _z3_assert(a.is_real(), "Z3 real expression expected.")
3493 return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
3496 def Sqrt(a, ctx=None):
3497 """ Return a Z3 expression which represents the square root of a.
3509 def Cbrt(a, ctx=None):
3510 """ Return a Z3 expression which represents the cubic root of a.
3521 #########################################
3525 #########################################
3528 class BitVecSortRef(SortRef):
3529 """Bit-vector sort.
"""
3532 """Return the size (number of bits) of the bit-vector sort `self`.
3538 return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast))
3540 def subsort(self, other):
3541 return is_bv_sort(other) and self.size() < other.size()
3543 def cast(self, val):
3544 """Try to cast `val`
as a Bit-Vector.
3549 >>> b.cast(10).
sexpr()
3554 _z3_assert(self.ctx == val.ctx, "Context mismatch")
3555 # Idea: use sign_extend if sort of val is a bitvector of smaller size
3558 return BitVecVal(val, self)
3562 """Return
True if `s`
is a Z3 bit-vector sort.
3569 return isinstance(s, BitVecSortRef)
3572 class BitVecRef(ExprRef):
3573 """Bit-vector expressions.
"""
3576 """Return the sort of the bit-vector expression `self`.
3584 return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
3587 """Return the number of bits of the bit-vector expression `self`.
3595 return self.sort().size()
3597 def __add__(self, other):
3598 """Create the Z3 expression `self + other`.
3607 a, b = _coerce_exprs(self, other)
3608 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3610 def __radd__(self, other):
3611 """Create the Z3 expression `other + self`.
3617 a, b = _coerce_exprs(self, other)
3618 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3620 def __mul__(self, other):
3621 """Create the Z3 expression `self * other`.
3630 a, b = _coerce_exprs(self, other)
3631 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3633 def __rmul__(self, other):
3634 """Create the Z3 expression `other * self`.
3640 a, b = _coerce_exprs(self, other)
3641 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3643 def __sub__(self, other):
3644 """Create the Z3 expression `self - other`.
3653 a, b = _coerce_exprs(self, other)
3654 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3656 def __rsub__(self, other):
3657 """Create the Z3 expression `other - self`.
3663 a, b = _coerce_exprs(self, other)
3664 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3666 def __or__(self, other):
3667 """Create the Z3 expression bitwise-
or `self | other`.
3676 a, b = _coerce_exprs(self, other)
3677 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3679 def __ror__(self, other):
3680 """Create the Z3 expression bitwise-
or `other | self`.
3686 a, b = _coerce_exprs(self, other)
3687 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3689 def __and__(self, other):
3690 """Create the Z3 expression bitwise-
and `self & other`.
3699 a, b = _coerce_exprs(self, other)
3700 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3702 def __rand__(self, other):
3703 """Create the Z3 expression bitwise-
or `other & self`.
3709 a, b = _coerce_exprs(self, other)
3710 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3712 def __xor__(self, other):
3713 """Create the Z3 expression bitwise-xor `self ^ other`.
3722 a, b = _coerce_exprs(self, other)
3723 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3725 def __rxor__(self, other):
3726 """Create the Z3 expression bitwise-xor `other ^ self`.
3732 a, b = _coerce_exprs(self, other)
3733 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3745 """Return an expression representing `-self`.
3753 return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx)
3755 def __invert__(self):
3756 """Create the Z3 expression bitwise-
not `~self`.
3764 return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx)
3766 def __div__(self, other):
3767 """Create the Z3 expression (signed) division `self / other`.
3769 Use the function
UDiv()
for unsigned division.
3782 a, b = _coerce_exprs(self, other)
3783 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3785 def __truediv__(self, other):
3786 """Create the Z3 expression (signed) division `self / other`.
"""
3787 return self.__div__(other)
3789 def __rdiv__(self, other):
3790 """Create the Z3 expression (signed) division `other / self`.
3792 Use the function
UDiv()
for unsigned division.
3797 >>> (10 / x).
sexpr()
3798 '(bvsdiv #x0000000a x)'
3800 '(bvudiv #x0000000a x)'
3802 a, b = _coerce_exprs(self, other)
3803 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3805 def __rtruediv__(self, other):
3806 """Create the Z3 expression (signed) division `other / self`.
"""
3807 return self.__rdiv__(other)
3809 def __mod__(self, other):
3810 """Create the Z3 expression (signed) mod `self % other`.
3812 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3827 a, b = _coerce_exprs(self, other)
3828 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3830 def __rmod__(self, other):
3831 """Create the Z3 expression (signed) mod `other % self`.
3833 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3838 >>> (10 % x).
sexpr()
3839 '(bvsmod #x0000000a x)'
3841 '(bvurem #x0000000a x)'
3843 '(bvsrem #x0000000a x)'
3845 a, b = _coerce_exprs(self, other)
3846 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3848 def __le__(self, other):
3849 """Create the Z3 expression (signed) `other <= self`.
3851 Use the function
ULE()
for unsigned less than
or equal to.
3856 >>> (x <= y).
sexpr()
3861 a, b = _coerce_exprs(self, other)
3862 return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3864 def __lt__(self, other):
3865 """Create the Z3 expression (signed) `other < self`.
3867 Use the function
ULT()
for unsigned less than.
3877 a, b = _coerce_exprs(self, other)
3878 return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3880 def __gt__(self, other):
3881 """Create the Z3 expression (signed) `other > self`.
3883 Use the function
UGT()
for unsigned greater than.
3893 a, b = _coerce_exprs(self, other)
3894 return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3896 def __ge__(self, other):
3897 """Create the Z3 expression (signed) `other >= self`.
3899 Use the function
UGE()
for unsigned greater than
or equal to.
3904 >>> (x >= y).
sexpr()
3909 a, b = _coerce_exprs(self, other)
3910 return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3912 def __rshift__(self, other):
3913 """Create the Z3 expression (arithmetical) right shift `self >> other`
3915 Use the function
LShR()
for the right logical shift
3920 >>> (x >> y).
sexpr()
3939 a, b = _coerce_exprs(self, other)
3940 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3942 def __lshift__(self, other):
3943 """Create the Z3 expression left shift `self << other`
3948 >>> (x << y).
sexpr()
3953 a, b = _coerce_exprs(self, other)
3954 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3956 def __rrshift__(self, other):
3957 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3959 Use the function
LShR()
for the right logical shift
3964 >>> (10 >> x).
sexpr()
3965 '(bvashr #x0000000a x)'
3967 a, b = _coerce_exprs(self, other)
3968 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3970 def __rlshift__(self, other):
3971 """Create the Z3 expression left shift `other << self`.
3973 Use the function
LShR()
for the right logical shift
3978 >>> (10 << x).
sexpr()
3979 '(bvshl #x0000000a x)'
3981 a, b = _coerce_exprs(self, other)
3982 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3985 class BitVecNumRef(BitVecRef):
3986 """Bit-vector values.
"""
3989 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral.
3994 >>> print(
"0x%.8x" % v.as_long())
3997 return int(self.as_string())
3999 def as_signed_long(self):
4000 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral.
4001 The most significant bit
is assumed to be the sign.
4015 val = self.as_long()
4016 if val >= 2**(sz - 1):
4018 if val < -2**(sz - 1):
4022 def as_string(self):
4023 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
4025 def as_binary_string(self):
4026 return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
4029 """Return the Python value of a Z3 bit-vector numeral.
"""
4030 return self.as_long()
4035 """Return `
True`
if `a`
is a Z3 bit-vector expression.
4045 return isinstance(a, BitVecRef)
4049 """Return `
True`
if `a`
is a Z3 bit-vector numeral value.
4060 return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
4063 def BV2Int(a, is_signed=False):
4064 """Return the Z3 expression
BV2Int(a).
4072 >>> x >
BV2Int(b, is_signed=
False)
4074 >>> x >
BV2Int(b, is_signed=
True)
4080 _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4082 # investigate problem with bv2int
4083 return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
4086 def Int2BV(a, num_bits):
4087 """Return the z3 expression
Int2BV(a, num_bits).
4088 It
is a bit-vector of width num_bits
and represents the
4089 modulo of a by 2^num_bits
4092 return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
4095 def BitVecSort(sz, ctx=None):
4096 """Return a Z3 bit-vector sort of the given size. If `ctx=
None`, then the
global context
is used.
4102 >>> x =
Const(
'x', Byte)
4107 return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
4110 def BitVecVal(val, bv, ctx=None):
4111 """Return a bit-vector value with the given number of bits. If `ctx=
None`, then the
global context
is used.
4116 >>> print(
"0x%.8x" % v.as_long())
4121 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
4124 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
4127 def BitVec(name, bv, ctx=None):
4128 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
4129 If `ctx=
None`, then the
global context
is used.
4139 >>> x2 =
BitVec(
'x', word)
4143 if isinstance(bv, BitVecSortRef):
4147 bv = BitVecSort(bv, ctx)
4148 return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
4151 def BitVecs(names, bv, ctx=None):
4152 """Return a tuple of bit-vector constants of size bv.
4154 >>> x, y, z =
BitVecs(
'x y z', 16)
4167 if isinstance(names, str):
4168 names = names.split(" ")
4169 return [BitVec(name, bv, ctx) for name in names]
4173 """Create a Z3 bit-vector concatenation expression.
4183 args = _get_args(args)
4186 _z3_assert(sz >= 2, "At least two arguments expected.")
4193 if is_seq(args[0]) or isinstance(args[0], str):
4194 args = [_coerce_seq(s, ctx) for s in args]
4196 _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
4199 v[i] = args[i].as_ast()
4200 return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
4204 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
4207 v[i] = args[i].as_ast()
4208 return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
4211 _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
4213 for i in range(sz - 1):
4214 r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i + 1].as_ast()), ctx)
4218 def Extract(high, low, a):
4219 """Create a Z3 bit-vector extraction expression.
4220 Extract
is overloaded to also work on sequence extraction.
4221 The functions SubString
and SubSeq are redirected to Extract.
4222 For this case, the arguments are reinterpreted
as:
4223 high -
is a sequence (string)
4225 a -
is the length to be extracted
4235 if isinstance(high, str):
4236 high = StringVal(high)
4239 offset, length = _coerce_exprs(low, a, s.ctx)
4240 return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
4242 _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
4243 _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0,
4244 "First and second arguments must be non negative integers")
4245 _z3_assert(is_bv(a), "Third argument must be a Z3 bit-vector expression")
4246 return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
4249 def _check_bv_args(a, b):
4251 _z3_assert(is_bv(a) or is_bv(b), "First or second argument must be a Z3 bit-vector expression")
4255 """Create the Z3 expression (unsigned) `other <= self`.
4257 Use the operator <=
for signed less than
or equal to.
4262 >>> (x <= y).sexpr()
4264 >>>
ULE(x, y).sexpr()
4267 _check_bv_args(a, b)
4268 a, b = _coerce_exprs(a, b)
4269 return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4273 """Create the Z3 expression (unsigned) `other < self`.
4275 Use the operator <
for signed less than.
4282 >>>
ULT(x, y).sexpr()
4285 _check_bv_args(a, b)
4286 a, b = _coerce_exprs(a, b)
4287 return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4291 """Create the Z3 expression (unsigned) `other >= self`.
4293 Use the operator >=
for signed greater than
or equal to.
4298 >>> (x >= y).sexpr()
4300 >>>
UGE(x, y).sexpr()
4303 _check_bv_args(a, b)
4304 a, b = _coerce_exprs(a, b)
4305 return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4309 """Create the Z3 expression (unsigned) `other > self`.
4311 Use the operator >
for signed greater than.
4318 >>>
UGT(x, y).sexpr()
4321 _check_bv_args(a, b)
4322 a, b = _coerce_exprs(a, b)
4323 return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4327 """Create the Z3 expression (unsigned) division `self / other`.
4329 Use the operator /
for signed division.
4335 >>>
UDiv(x, y).sort()
4339 >>>
UDiv(x, y).sexpr()
4342 _check_bv_args(a, b)
4343 a, b = _coerce_exprs(a, b)
4344 return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4348 """Create the Z3 expression (unsigned) remainder `self % other`.
4350 Use the operator %
for signed modulus,
and SRem()
for signed remainder.
4356 >>>
URem(x, y).sort()
4360 >>>
URem(x, y).sexpr()
4363 _check_bv_args(a, b)
4364 a, b = _coerce_exprs(a, b)
4365 return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4369 """Create the Z3 expression signed remainder.
4371 Use the operator %
for signed modulus,
and URem()
for unsigned remainder.
4377 >>>
SRem(x, y).sort()
4381 >>>
SRem(x, y).sexpr()
4384 _check_bv_args(a, b)
4385 a, b = _coerce_exprs(a, b)
4386 return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4390 """Create the Z3 expression logical right shift.
4392 Use the operator >>
for the arithmetical right shift.
4397 >>> (x >> y).sexpr()
4399 >>>
LShR(x, y).sexpr()
4416 _check_bv_args(a, b)
4417 a, b = _coerce_exprs(a, b)
4418 return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4421 def RotateLeft(a, b):
4422 """Return an expression representing `a` rotated to the left `b` times.
4432 _check_bv_args(a, b)
4433 a, b = _coerce_exprs(a, b)
4434 return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4437 def RotateRight(a, b):
4438 """Return an expression representing `a` rotated to the right `b` times.
4448 _check_bv_args(a, b)
4449 a, b = _coerce_exprs(a, b)
4450 return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4454 """Return a bit-vector expression with `n` extra sign-bits.
4474 >>> print(
"%.x" % v.as_long())
4478 _z3_assert(_is_int(n), "First argument must be an integer")
4479 _z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
4480 return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
4484 """Return a bit-vector expression with `n` extra zero-bits.
4506 _z3_assert(_is_int(n), "First argument must be an integer")
4507 _z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
4508 return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
4511 def RepeatBitVec(n, a):
4512 """Return an expression representing `n` copies of `a`.
4521 >>> print(
"%.x" % v0.as_long())
4526 >>> print(
"%.x" % v.as_long())
4530 _z3_assert(_is_int(n), "First argument must be an integer")
4531 _z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
4532 return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
4536 """Return the reduction-
and expression of `a`.
"""
4538 _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4539 return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
4543 """Return the reduction-
or expression of `a`.
"""
4545 _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4546 return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
4549 def BVAddNoOverflow(a, b, signed):
4550 """A predicate the determines that bit-vector addition does
not overflow
"""
4551 _check_bv_args(a, b)
4552 a, b = _coerce_exprs(a, b)
4553 return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4556 def BVAddNoUnderflow(a, b):
4557 """A predicate the determines that signed bit-vector addition does
not underflow
"""
4558 _check_bv_args(a, b)
4559 a, b = _coerce_exprs(a, b)
4560 return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4563 def BVSubNoOverflow(a, b):
4564 """A predicate the determines that bit-vector subtraction does
not overflow
"""
4565 _check_bv_args(a, b)
4566 a, b = _coerce_exprs(a, b)
4567 return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4570 def BVSubNoUnderflow(a, b, signed):
4571 """A predicate the determines that bit-vector subtraction does
not underflow
"""
4572 _check_bv_args(a, b)
4573 a, b = _coerce_exprs(a, b)
4574 return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4577 def BVSDivNoOverflow(a, b):
4578 """A predicate the determines that bit-vector signed division does
not overflow
"""
4579 _check_bv_args(a, b)
4580 a, b = _coerce_exprs(a, b)
4581 return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4584 def BVSNegNoOverflow(a):
4585 """A predicate the determines that bit-vector unary negation does
not overflow
"""
4587 _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
4588 return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
4591 def BVMulNoOverflow(a, b, signed):
4592 """A predicate the determines that bit-vector multiplication does
not overflow
"""
4593 _check_bv_args(a, b)
4594 a, b = _coerce_exprs(a, b)
4595 return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
4598 def BVMulNoUnderflow(a, b):
4599 """A predicate the determines that bit-vector signed multiplication does
not underflow
"""
4600 _check_bv_args(a, b)
4601 a, b = _coerce_exprs(a, b)
4602 return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
4605 #########################################
4609 #########################################
4611 class ArraySortRef(SortRef):
4615 """Return the domain of the array sort `self`.
4621 return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx)
4623 def domain_n(self, i):
4624 """Return the domain of the array sort `self`.
4626 return _to_sort_ref(Z3_get_array_sort_domain_n(self.ctx_ref(), self.ast, i), self.ctx)
4629 """Return the range of the array sort `self`.
4635 return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)
4638 class ArrayRef(ExprRef):
4639 """Array expressions.
"""
4642 """Return the array sort of the array expression `self`.
4648 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
4657 return self.sort().domain()
4659 def domain_n(self, i):
4661 return self.sort().domain_n(i)
4670 return self.sort().range()
4672 def __getitem__(self, arg):
4673 """Return the Z3 expression `self[arg]`.
4682 return _array_select(self, arg)
4685 return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx)
4688 def _array_select(ar, arg):
4689 if isinstance(arg, tuple):
4690 args = [ar.sort().domain_n(i).cast(arg[i]) for i in range(len(arg))]
4691 _args, sz = _to_ast_array(args)
4692 return _to_expr_ref(Z3_mk_select_n(ar.ctx_ref(), ar.as_ast(), sz, _args), ar.ctx)
4693 arg = ar.sort().domain().cast(arg)
4694 return _to_expr_ref(Z3_mk_select(ar.ctx_ref(), ar.as_ast(), arg.as_ast()), ar.ctx)
4697 def is_array_sort(a):
4698 return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
4701 def is_array(a : Any) -> bool:
4702 """Return `
True`
if `a`
is a Z3 array expression.
4712 return isinstance(a, ArrayRef)
4715 def is_const_array(a):
4716 """Return `
True`
if `a`
is a Z3 constant array.
4725 return is_app_of(a, Z3_OP_CONST_ARRAY)
4729 """Return `
True`
if `a`
is a Z3 constant array.
4738 return is_app_of(a, Z3_OP_CONST_ARRAY)
4742 """Return `
True`
if `a`
is a Z3 map array expression.
4754 return is_app_of(a, Z3_OP_ARRAY_MAP)
4758 """Return `
True`
if `a`
is a Z3 default array expression.
4763 return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4766 def get_map_func(a):
4767 """Return the function declaration associated with a Z3 map array expression.
4780 _z3_assert(is_map(a), "Z3 array map expression expected.")
4784 Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0),
4790 def ArraySort(*sig):
4791 """Return the Z3 array sort with the given domain
and range sorts.
4804 sig = _get_args(sig)
4806 _z3_assert(len(sig) > 1, "At least two arguments expected")
4807 arity = len(sig) - 1
4812 _z3_assert(is_sort(s), "Z3 sort expected")
4813 _z3_assert(s.ctx == r.ctx, "Context mismatch")
4816 return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
4817 dom = (Sort * arity)()
4818 for i in range(arity):
4820 return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)
4823 def Array(name, *sorts):
4824 """Return an array constant named `name` with the given domain
and range sorts.
4832 s = ArraySort(sorts)
4834 return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
4837 def Update(a, *args):
4838 """Return a Z3 store array expression.
4841 >>> i, v =
Ints(
'i v')
4845 >>>
prove(s[i] == v)
4852 _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4853 args = _get_args(args)
4856 raise Z3Exception("array update requires index and value arguments")
4860 i = a.sort().domain().cast(i)
4861 v = a.sort().range().cast(v)
4862 return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
4863 v = a.sort().range().cast(args[-1])
4864 idxs = [a.sort().domain_n(i).cast(args[i]) for i in range(len(args)-1)]
4865 _args, sz = _to_ast_array(idxs)
4866 return _to_expr_ref(Z3_mk_store_n(ctx.ref(), a.as_ast(), sz, _args, v.as_ast()), ctx)
4870 """ Return a default value
for array expression.
4876 _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4880 def Store(a, *args):
4881 """Return a Z3 store array expression.
4884 >>> i, v =
Ints(
'i v')
4885 >>> s =
Store(a, i, v)
4888 >>>
prove(s[i] == v)
4894 return Update(a, args)
4897 def Select(a, *args):
4898 """Return a Z3 select array expression.
4907 args = _get_args(args)
4909 _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
4914 """Return a Z3 map array expression.
4919 >>> b =
Map(f, a1, a2)
4922 >>>
prove(b[0] == f(a1[0], a2[0]))
4925 args = _get_args(args)
4927 _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
4928 _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
4929 _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
4930 _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
4931 _args, sz = _to_ast_array(args)
4933 return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
4937 """Return a Z3 constant array expression.
4951 _z3_assert(is_sort(dom), "Z3 sort expected")
4954 v = _py2expr(v, ctx)
4955 return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
4959 """Return extensionality index
for one-dimensional arrays.
4966 _z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays")
4967 return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
4970 def SetHasSize(a, k):
4972 k = _py2expr(k, ctx)
4973 return _to_expr_ref(Z3_mk_set_has_size(ctx.ref(), a.as_ast(), k.as_ast()), ctx)
4977 """Return `
True`
if `a`
is a Z3 array select application.
4986 return is_app_of(a, Z3_OP_SELECT)
4990 """Return `
True`
if `a`
is a Z3 array store application.
4998 return is_app_of(a, Z3_OP_STORE)
5000 #########################################
5004 #########################################
5008 """ Create a set sort over element sort s
"""
5009 return ArraySort(s, BoolSort())
5013 """Create the empty set
5018 return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
5022 """Create the full set
5027 return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
5030 def SetUnion(*args):
5031 """ Take the union of sets
5037 args = _get_args(args)
5038 ctx = _ctx_from_ast_arg_list(args)
5039 _args, sz = _to_ast_array(args)
5040 return ArrayRef(Z3_mk_set_union(ctx.ref(), sz, _args), ctx)
5043 def SetIntersect(*args):
5044 """ Take the union of sets
5050 args = _get_args(args)
5051 ctx = _ctx_from_ast_arg_list(args)
5052 _args, sz = _to_ast_array(args)
5053 return ArrayRef(Z3_mk_set_intersect(ctx.ref(), sz, _args), ctx)
5057 """ Add element e to set s
5062 ctx = _ctx_from_ast_arg_list([s, e])
5063 e = _py2expr(e, ctx)
5064 return ArrayRef(Z3_mk_set_add(ctx.ref(), s.as_ast(), e.as_ast()), ctx)
5068 """ Remove element e to set s
5073 ctx = _ctx_from_ast_arg_list([s, e])
5074 e = _py2expr(e, ctx)
5075 return ArrayRef(Z3_mk_set_del(ctx.ref(), s.as_ast(), e.as_ast()), ctx)
5078 def SetComplement(s):
5079 """ The complement of set s
5085 return ArrayRef(Z3_mk_set_complement(ctx.ref(), s.as_ast()), ctx)
5088 def SetDifference(a, b):
5089 """ The set difference of a
and b
5095 ctx = _ctx_from_ast_arg_list([a, b])
5096 return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
5100 """ Check
if e
is a member of set s
5105 ctx = _ctx_from_ast_arg_list([s, e])
5106 e = _py2expr(e, ctx)
5107 return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx)
5111 """ Check
if a
is a subset of b
5117 ctx = _ctx_from_ast_arg_list([a, b])
5118 return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
5121 #########################################
5125 #########################################
5127 def _valid_accessor(acc):
5128 """Return `
True`
if acc
is pair of the form (String, Datatype
or Sort).
"""
5129 if not isinstance(acc, tuple):
5133 return isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1]))
5137 """Helper
class for declaring Z3 datatypes.
5140 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
5141 >>> List.declare(
'nil')
5142 >>> List = List.create()
5146 >>> List.cons(10, List.nil)
5148 >>> List.cons(10, List.nil).sort()
5150 >>> cons = List.cons
5154 >>> n = cons(1, cons(0, nil))
5156 cons(1, cons(0, nil))
5163 def __init__(self, name, ctx=None):
5164 self.ctx = _get_ctx(ctx)
5166 self.constructors = []
5168 def __deepcopy__(self, memo={}):
5169 r = Datatype(self.name, self.ctx)
5170 r.constructors = copy.deepcopy(self.constructors)
5173 def declare_core(self, name, rec_name, *args):
5175 _z3_assert(isinstance(name, str), "String expected")
5176 _z3_assert(isinstance(rec_name, str), "String expected")
5178 all([_valid_accessor(a) for a in args]),
5179 "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)",
5181 self.constructors.append((name, rec_name, args))
5183 def declare(self, name, *args):
5184 """Declare constructor named `name` with the given accessors `args`.
5185 Each accessor
is a pair `(name, sort)`, where `name`
is a string
and `sort` a Z3 sort
5186 or a reference to the datatypes being declared.
5188 In the following example `List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))`
5189 declares the constructor named `cons` that builds a new List using an integer
and a List.
5190 It also declares the accessors `car`
and `cdr`. The accessor `car` extracts the integer
5191 of a `cons` cell,
and `cdr` the list of a `cons` cell. After all constructors were declared,
5192 we use the method
create() to create the actual datatype
in Z3.
5195 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
5196 >>> List.declare(
'nil')
5197 >>> List = List.create()
5200 _z3_assert(isinstance(name, str), "String expected")
5201 _z3_assert(name != "", "Constructor name cannot be empty")
5202 return self.declare_core(name, "is-" + name, *args)
5205 return "Datatype(%s, %s)" % (self.name, self.constructors)
5208 """Create a Z3 datatype based on the constructors declared using the method `
declare()`.
5210 The function `
CreateDatatypes()` must be used to define mutually recursive datatypes.
5213 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
5214 >>> List.declare(
'nil')
5215 >>> List = List.create()
5218 >>> List.cons(10, List.nil)
5221 return CreateDatatypes([self])[0]
5224 class ScopedConstructor:
5225 """Auxiliary object used to create Z3 datatypes.
"""
5227 def __init__(self, c, ctx):
5232 if self.ctx.ref() is not None and Z3_del_constructor is not None:
5233 Z3_del_constructor(self.ctx.ref(), self.c)
5236 class ScopedConstructorList:
5237 """Auxiliary object used to create Z3 datatypes.
"""
5239 def __init__(self, c, ctx):
5244 if self.ctx.ref() is not None and Z3_del_constructor_list is not None:
5245 Z3_del_constructor_list(self.ctx.ref(), self.c)
5248 def CreateDatatypes(*ds):
5249 """Create mutually recursive Z3 datatypes using 1
or more Datatype helper objects.
5251 In the following example we define a Tree-List using two mutually recursive datatypes.
5253 >>> TreeList =
Datatype(
'TreeList')
5256 >>> Tree.declare(
'leaf', (
'val',
IntSort()))
5258 >>> Tree.declare(
'node', (
'children', TreeList))
5259 >>> TreeList.declare(
'nil')
5260 >>> TreeList.declare(
'cons', (
'car', Tree), (
'cdr', TreeList))
5262 >>> Tree.val(Tree.leaf(10))
5264 >>>
simplify(Tree.val(Tree.leaf(10)))
5266 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
5268 node(cons(leaf(10), cons(leaf(20), nil)))
5269 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
5272 >>>
simplify(TreeList.car(Tree.children(n2)) == n1)
5277 _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
5278 _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
5279 _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
5280 _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
5283 names = (Symbol * num)()
5284 out = (Sort * num)()
5285 clists = (ConstructorList * num)()
5287 for i in range(num):
5289 names[i] = to_symbol(d.name, ctx)
5290 num_cs = len(d.constructors)
5291 cs = (Constructor * num_cs)()
5292 for j in range(num_cs):
5293 c = d.constructors[j]
5294 cname = to_symbol(c[0], ctx)
5295 rname = to_symbol(c[1], ctx)
5298 fnames = (Symbol * num_fs)()
5299 sorts = (Sort * num_fs)()
5300 refs = (ctypes.c_uint * num_fs)()
5301 for k in range(num_fs):
5304 fnames[k] = to_symbol(fname, ctx)
5305 if isinstance(ftype, Datatype):
5308 ds.count(ftype) == 1,
5309 "One and only one occurrence of each datatype is expected",
5312 refs[k] = ds.index(ftype)
5315 _z3_assert(is_sort(ftype), "Z3 sort expected")
5316 sorts[k] = ftype.ast
5318 cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
5319 to_delete.append(ScopedConstructor(cs[j], ctx))
5320 clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
5321 to_delete.append(ScopedConstructorList(clists[i], ctx))
5322 Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
5324 # Create a field for every constructor, recognizer and accessor
5325 for i in range(num):
5326 dref = DatatypeSortRef(out[i], ctx)
5327 num_cs = dref.num_constructors()
5328 for j in range(num_cs):
5329 cref = dref.constructor(j)
5330 cref_name = cref.name()
5331 cref_arity = cref.arity()
5332 if cref.arity() == 0:
5334 setattr(dref, cref_name, cref)
5335 rref = dref.recognizer(j)
5336 setattr(dref, "is_" + cref_name, rref)
5337 for k in range(cref_arity):
5338 aref = dref.accessor(j, k)
5339 setattr(dref, aref.name(), aref)
5341 return tuple(result)
5344 class DatatypeSortRef(SortRef):
5345 """Datatype sorts.
"""
5347 def num_constructors(self):
5348 """Return the number of constructors
in the given Z3 datatype.
5351 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
5352 >>> List.declare(
'nil')
5353 >>> List = List.create()
5355 >>> List.num_constructors()
5358 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
5360 def constructor(self, idx):
5361 """Return a constructor of the datatype `self`.
5364 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
5365 >>> List.declare(
'nil')
5366 >>> List = List.create()
5368 >>> List.num_constructors()
5370 >>> List.constructor(0)
5372 >>> List.constructor(1)
5376 _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
5377 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
5379 def recognizer(self, idx):
5380 """In Z3, each constructor has an associated recognizer predicate.
5382 If the constructor
is named `name`, then the recognizer `is_name`.
5385 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
5386 >>> List.declare(
'nil')
5387 >>> List = List.create()
5389 >>> List.num_constructors()
5391 >>> List.recognizer(0)
5393 >>> List.recognizer(1)
5395 >>>
simplify(List.is_nil(List.cons(10, List.nil)))
5397 >>>
simplify(List.is_cons(List.cons(10, List.nil)))
5399 >>> l =
Const(
'l', List)
5404 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
5405 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
5407 def accessor(self, i, j):
5408 """In Z3, each constructor has 0
or more accessor.
5409 The number of accessors
is equal to the arity of the constructor.
5412 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
5413 >>> List.declare(
'nil')
5414 >>> List = List.create()
5415 >>> List.num_constructors()
5417 >>> List.constructor(0)
5419 >>> num_accs = List.constructor(0).arity()
5422 >>> List.accessor(0, 0)
5424 >>> List.accessor(0, 1)
5426 >>> List.constructor(1)
5428 >>> num_accs = List.constructor(1).arity()
5433 _z3_assert(i < self.num_constructors(), "Invalid constructor index")
5434 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
5436 Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j),
5441 class DatatypeRef(ExprRef):
5442 """Datatype expressions.
"""
5445 """Return the datatype sort of the datatype expression `self`.
"""
5446 return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
5448 def DatatypeSort(name, ctx = None):
5449 """Create a reference to a sort that was declared,
or will be declared,
as a recursive datatype
"""
5451 return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
5453 def TupleSort(name, sorts, ctx=None):
5454 """Create a named tuple sort base on a set of underlying sorts
5458 tuple = Datatype(name, ctx)
5459 projects = [("project%d" % i, sorts[i]) for i in range(len(sorts))]
5460 tuple.declare(name, *projects)
5461 tuple = tuple.create()
5462 return tuple, tuple.constructor(0), [tuple.accessor(0, i) for i in range(len(sorts))]
5465 def DisjointSum(name, sorts, ctx=None):
5466 """Create a named tagged union sort base on a set of underlying sorts
5470 sum = Datatype(name, ctx)
5471 for i in range(len(sorts)):
5472 sum.declare("inject%d" % i, ("project%d" % i, sorts[i]))
5474 return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))]
5477 def EnumSort(name, values, ctx=None):
5478 """Return a new enumeration sort named `name` containing the given values.
5480 The result
is a pair (sort, list of constants).
5482 >>> Color, (red, green, blue) =
EnumSort(
'Color', [
'red',
'green',
'blue'])
5485 _z3_assert(isinstance(name, str), "Name must be a string")
5486 _z3_assert(all([isinstance(v, str) for v in values]), "Enumeration sort values must be strings")
5487 _z3_assert(len(values) > 0, "At least one value expected")
5490 _val_names = (Symbol * num)()
5491 for i in range(num):
5492 _val_names[i] = to_symbol(values[i], ctx)
5493 _values = (FuncDecl * num)()
5494 _testers = (FuncDecl * num)()
5495 name = to_symbol(name, ctx)
5496 S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
5498 for i in range(num):
5499 V.append(FuncDeclRef(_values[i], ctx))
5500 V = [a() for a in V]
5503 #########################################
5507 #########################################
5511 """Set of parameters used to configure Solvers, Tactics
and Simplifiers
in Z3.
5513 Consider using the function `args2params` to create instances of this object.
5516 def __init__(self, ctx=None, params=None):
5517 self.ctx = _get_ctx(ctx)
5519 self.params = Z3_mk_params(self.ctx.ref())
5521 self.params = params
5522 Z3_params_inc_ref(self.ctx.ref(), self.params)
5524 def __deepcopy__(self, memo={}):
5525 return ParamsRef(self.ctx, self.params)
5528 if self.ctx.ref() is not None and Z3_params_dec_ref is not None:
5529 Z3_params_dec_ref(self.ctx.ref(), self.params)
5531 def set(self, name, val):
5532 """Set parameter name with value val.
"""
5534 _z3_assert(isinstance(name, str), "parameter name must be a string")
5535 name_sym = to_symbol(name, self.ctx)
5536 if isinstance(val, bool):
5537 Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val)
5539 Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val)
5540 elif isinstance(val, float):
5541 Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val)
5542 elif isinstance(val, str):
5543 Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx))
5546 _z3_assert(False, "invalid parameter value")
5549 return Z3_params_to_string(self.ctx.ref(), self.params)
5551 def validate(self, ds):
5552 _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected")
5553 Z3_params_validate(self.ctx.ref(), self.params, ds.descr)
5556 def args2params(arguments, keywords, ctx=None):
5557 """Convert python arguments into a Z3_params object.
5558 A
':' is added to the keywords,
and '_' is replaced with
'-'
5560 >>>
args2params([
'model',
True,
'relevancy', 2], {
'elim_and' :
True})
5561 (params model true relevancy 2 elim_and true)
5564 _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
5579 class ParamDescrsRef:
5580 """Set of parameter descriptions
for Solvers, Tactics
and Simplifiers
in Z3.
5583 def __init__(self, descr, ctx=None):
5584 _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected")
5585 self.ctx = _get_ctx(ctx)
5587 Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr)
5589 def __deepcopy__(self, memo={}):
5590 return ParamsDescrsRef(self.descr, self.ctx)
5593 if self.ctx.ref() is not None and Z3_param_descrs_dec_ref is not None:
5594 Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
5597 """Return the size of
in the parameter description `self`.
5599 return int(Z3_param_descrs_size(self.ctx.ref(), self.descr))
5602 """Return the size of
in the parameter description `self`.
5606 def get_name(self, i):
5607 """Return the i-th parameter name
in the parameter description `self`.
5609 return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i))
5611 def get_kind(self, n):
5612 """Return the kind of the parameter named `n`.
5614 return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
5616 def get_documentation(self, n):
5617 """Return the documentation string of the parameter named `n`.
5619 return Z3_param_descrs_get_documentation(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
5621 def __getitem__(self, arg):
5623 return self.get_name(arg)
5625 return self.get_kind(arg)
5628 return Z3_param_descrs_to_string(self.ctx.ref(), self.descr)
5630 #########################################
5634 #########################################
5637 class Goal(Z3PPObject):
5638 """Goal
is a collection of constraints we want to find a solution
or show to be unsatisfiable (infeasible).
5640 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
5641 A goal has a solution
if one of its subgoals has a solution.
5642 A goal
is unsatisfiable
if all subgoals are unsatisfiable.
5645 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
5647 _z3_assert(goal is None or ctx is not None,
5648 "If goal is different from None, then ctx must be also different from None")
5649 self.ctx = _get_ctx(ctx)
5651 if self.goal is None:
5652 self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
5653 Z3_goal_inc_ref(self.ctx.ref(), self.goal)
5656 if self.goal is not None and self.ctx.ref() is not None and Z3_goal_dec_ref is not None:
5657 Z3_goal_dec_ref(self.ctx.ref(), self.goal)
5660 """Return the depth of the goal `self`.
5661 The depth corresponds to the number of tactics applied to `self`.
5663 >>> x, y =
Ints(
'x y')
5665 >>> g.add(x == 0, y >= x + 1)
5668 >>> r =
Then(
'simplify',
'solve-eqs')(g)
5675 return int(Z3_goal_depth(self.ctx.ref(), self.goal))
5677 def inconsistent(self):
5678 """Return `
True`
if `self` contains the `
False` constraints.
5680 >>> x, y =
Ints(
'x y')
5682 >>> g.inconsistent()
5684 >>> g.add(x == 0, x == 1)
5687 >>> g.inconsistent()
5689 >>> g2 =
Tactic(
'propagate-values')(g)[0]
5690 >>> g2.inconsistent()
5693 return Z3_goal_inconsistent(self.ctx.ref(), self.goal)
5696 """Return the precision (under-approximation, over-approximation,
or precise) of the goal `self`.
5699 >>> g.prec() == Z3_GOAL_PRECISE
5701 >>> x, y =
Ints(
'x y')
5702 >>> g.add(x == y + 1)
5703 >>> g.prec() == Z3_GOAL_PRECISE
5705 >>> t =
With(
Tactic(
'add-bounds'), add_bound_lower=0, add_bound_upper=10)
5708 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
5709 >>> g2.prec() == Z3_GOAL_PRECISE
5711 >>> g2.prec() == Z3_GOAL_UNDER
5714 return Z3_goal_precision(self.ctx.ref(), self.goal)
5716 def precision(self):
5717 """Alias
for `
prec()`.
5720 >>> g.precision() == Z3_GOAL_PRECISE
5726 """Return the number of constraints
in the goal `self`.
5731 >>> x, y =
Ints(
'x y')
5732 >>> g.add(x == 0, y > x)
5736 return int(Z3_goal_size(self.ctx.ref(), self.goal))
5739 """Return the number of constraints
in the goal `self`.
5744 >>> x, y =
Ints(
'x y')
5745 >>> g.add(x == 0, y > x)
5752 """Return a constraint
in the goal `self`.
5755 >>> x, y =
Ints(
'x y')
5756 >>> g.add(x == 0, y > x)
5762 return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx)
5764 def __getitem__(self, arg):
5765 """Return a constraint
in the goal `self`.
5768 >>> x, y =
Ints(
'x y')
5769 >>> g.add(x == 0, y > x)
5775 if arg >= len(self):
5777 return self.get(arg)
5779 def assert_exprs(self, *args):
5780 """Assert constraints into the goal.
5784 >>> g.assert_exprs(x > 0, x < 2)
5788 args = _get_args(args)
5789 s = BoolSort(self.ctx)
5792 Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast())
5794 def append(self, *args):
5799 >>> g.append(x > 0, x < 2)
5803 self.assert_exprs(*args)
5805 def insert(self, *args):
5810 >>> g.insert(x > 0, x < 2)
5814 self.assert_exprs(*args)
5816 def add(self, *args):
5821 >>> g.add(x > 0, x < 2)
5825 self.assert_exprs(*args)
5827 def convert_model(self, model):
5828 """Retrieve model
from a satisfiable goal
5829 >>> a, b =
Ints(
'a b')
5831 >>> g.add(
Or(a == 0, a == 1),
Or(b == 0, b == 1), a > b)
5835 [
Or(b == 0, b == 1),
Not(0 <= b)]
5837 [
Or(b == 0, b == 1),
Not(1 <= b)]
5853 _z3_assert(isinstance(model, ModelRef), "Z3 Model expected")
5854 return ModelRef(Z3_goal_convert_model(self.ctx.ref(), self.goal, model.model), self.ctx)
5857 return obj_to_string(self)
5860 """Return a textual representation of the s-expression representing the goal.
"""
5861 return Z3_goal_to_string(self.ctx.ref(), self.goal)
5863 def dimacs(self, include_names=True):
5864 """Return a textual representation of the goal
in DIMACS format.
"""
5865 return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal, include_names)
5867 def translate(self, target):
5868 """Copy goal `self` to context `target`.
5876 >>> g2 = g.translate(c2)
5887 _z3_assert(isinstance(target, Context), "target must be a context")
5888 return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target)
5891 return self.translate(self.ctx)
5893 def __deepcopy__(self, memo={}):
5894 return self.translate(self.ctx)
5896 def simplify(self, *arguments, **keywords):
5897 """Return a new simplified goal.
5899 This method
is essentially invoking the simplify tactic.
5903 >>> g.add(x + 1 >= 2)
5906 >>> g2 = g.simplify()
5913 t = Tactic("simplify")
5914 return t.apply(self, *arguments, **keywords)[0]
5917 """Return goal `self`
as a single Z3 expression.
5932 return BoolVal(True, self.ctx)
5936 return And([self.get(i) for i in range(len(self))], self.ctx)
5938 #########################################
5942 #########################################
5945 class AstVector(Z3PPObject):
5946 """A collection (vector) of ASTs.
"""
5948 def __init__(self, v=None, ctx=None):
5951 self.ctx = _get_ctx(ctx)
5952 self.vector = Z3_mk_ast_vector(self.ctx.ref())
5955 assert ctx is not None
5957 Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
5960 if self.vector is not None and self.ctx.ref() is not None and Z3_ast_vector_dec_ref is not None:
5961 Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
5964 """Return the size of the vector `self`.
5969 >>> A.push(
Int(
'x'))
5970 >>> A.push(
Int(
'x'))
5974 return int(Z3_ast_vector_size(self.ctx.ref(), self.vector))
5976 def __getitem__(self, i):
5977 """Return the AST at position `i`.
5980 >>> A.push(
Int(
'x') + 1)
5981 >>> A.push(
Int(
'y'))
5988 if isinstance(i, int):
5992 if i >= self.__len__():
5994 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
5996 elif isinstance(i, slice):
5998 for ii in range(*i.indices(self.__len__())):
5999 result.append(_to_ast_ref(
6000 Z3_ast_vector_get(self.ctx.ref(), self.vector, ii),
6005 def __setitem__(self, i, v):
6006 """Update AST at position `i`.
6009 >>> A.push(
Int(
'x') + 1)
6010 >>> A.push(
Int(
'y'))
6017 if i >= self.__len__():
6019 Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast())
6022 """Add `v`
in the end of the vector.
6027 >>> A.push(
Int(
'x'))
6031 Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast())
6033 def resize(self, sz):
6034 """Resize the vector to `sz` elements.
6040 >>>
for i
in range(10): A[i] =
Int(
'x')
6044 Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz)
6046 def __contains__(self, item):
6047 """Return `
True`
if the vector contains `item`.
6069 def translate(self, other_ctx):
6070 """Copy vector `self` to context `other_ctx`.
6076 >>> B = A.translate(c2)
6081 Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()),
6086 return self.translate(self.ctx)
6088 def __deepcopy__(self, memo={}):
6089 return self.translate(self.ctx)
6092 return obj_to_string(self)
6095 """Return a textual representation of the s-expression representing the vector.
"""
6096 return Z3_ast_vector_to_string(self.ctx.ref(), self.vector)
6098 #########################################
6102 #########################################
6106 """A mapping
from ASTs to ASTs.
"""
6108 def __init__(self, m=None, ctx=None):
6111 self.ctx = _get_ctx(ctx)
6112 self.map = Z3_mk_ast_map(self.ctx.ref())
6115 assert ctx is not None
6117 Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
6119 def __deepcopy__(self, memo={}):
6120 return AstMap(self.map, self.ctx)
6123 if self.map is not None and self.ctx.ref() is not None and Z3_ast_map_dec_ref is not None:
6124 Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
6127 """Return the size of the map.
6137 return int(Z3_ast_map_size(self.ctx.ref(), self.map))
6139 def __contains__(self, key):
6140 """Return `
True`
if the map contains key `key`.
6150 return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast())
6152 def __getitem__(self, key):
6153 """Retrieve the value associated with key `key`.
6161 return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx)
6163 def __setitem__(self, k, v):
6164 """Add/Update key `k` with value `v`.
6177 Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast())
6180 return Z3_ast_map_to_string(self.ctx.ref(), self.map)
6183 """Remove the entry associated with key `k`.
6194 Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast())
6197 """Remove all entries
from the map.
6209 Z3_ast_map_reset(self.ctx.ref(), self.map)
6212 """Return an AstVector containing all keys
in the map.
6221 return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx)
6223 #########################################
6227 #########################################
6231 """Store the value of the interpretation of a function
in a particular point.
"""
6233 def __init__(self, entry, ctx):
6236 Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
6238 def __deepcopy__(self, memo={}):
6239 return FuncEntry(self.entry, self.ctx)
6242 if self.ctx.ref() is not None and Z3_func_entry_dec_ref is not None:
6243 Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
6246 """Return the number of arguments
in the given entry.
6250 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6255 >>> f_i.num_entries()
6257 >>> e = f_i.entry(0)
6261 return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
6263 def arg_value(self, idx):
6264 """Return the value of argument `idx`.
6268 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6273 >>> f_i.num_entries()
6275 >>> e = f_i.entry(0)
6286 ...
except IndexError:
6287 ... print(
"index error")
6290 if idx >= self.num_args():
6292 return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
6295 """Return the value of the function at point `self`.
6299 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6304 >>> f_i.num_entries()
6306 >>> e = f_i.entry(0)
6314 return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
6317 """Return entry `self`
as a Python list.
6320 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6325 >>> f_i.num_entries()
6327 >>> e = f_i.entry(0)
6331 args = [self.arg_value(i) for i in range(self.num_args())]
6332 args.append(self.value())
6336 return repr(self.as_list())
6339 class FuncInterp(Z3PPObject):
6340 """Stores the interpretation of a function
in a Z3 model.
"""
6342 def __init__(self, f, ctx):
6345 if self.f is not None:
6346 Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
6349 if self.f is not None and self.ctx.ref() is not None and Z3_func_interp_dec_ref is not None:
6350 Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
6352 def else_value(self):
6354 Return the `
else` value
for a function interpretation.
6355 Return
None if Z3 did
not specify the `
else` value
for
6360 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
6369 r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
6371 return _to_expr_ref(r, self.ctx)
6375 def num_entries(self):
6376 """Return the number of entries/points
in the function interpretation `self`.
6380 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
6389 return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
6392 """Return the number of arguments
for each entry
in the function interpretation `self`.
6396 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
6403 return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
6405 def entry(self, idx):
6406 """Return an entry at position `idx < self.
num_entries()`
in the function interpretation `self`.
6410 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
6421 if idx >= self.num_entries():
6423 return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
6425 def translate(self, other_ctx):
6426 """Copy model
'self' to context
'other_ctx'.
6428 return ModelRef(Z3_model_translate(self.ctx.ref(), self.model, other_ctx.ref()), other_ctx)
6431 return self.translate(self.ctx)
6433 def __deepcopy__(self, memo={}):
6434 return self.translate(self.ctx)
6437 """Return the function interpretation
as a Python list.
6440 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
6449 r = [self.entry(i).as_list() for i in range(self.num_entries())]
6450 r.append(self.else_value())
6454 return obj_to_string(self)
6457 class ModelRef(Z3PPObject):
6458 """Model/Solution of a satisfiability problem (aka system of constraints).
"""
6460 def __init__(self, m, ctx):
6461 assert ctx is not None
6464 Z3_model_inc_ref(self.ctx.ref(), self.model)
6467 if self.ctx.ref() is not None and Z3_model_dec_ref is not None:
6468 Z3_model_dec_ref(self.ctx.ref(), self.model)
6471 return obj_to_string(self)
6474 """Return a textual representation of the s-expression representing the model.
"""
6475 return Z3_model_to_string(self.ctx.ref(), self.model)
6477 def eval(self, t, model_completion=False):
6478 """Evaluate the expression `t`
in the model `self`.
6479 If `model_completion`
is enabled, then a default interpretation
is automatically added
6480 for symbols that do
not have an interpretation
in the model `self`.
6484 >>> s.add(x > 0, x < 2)
6497 >>> m.eval(y, model_completion=
True)
6504 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
6505 return _to_expr_ref(r[0], self.ctx)
6506 raise Z3Exception("failed to evaluate expression in the model")
6508 def evaluate(self, t, model_completion=False):
6509 """Alias
for `eval`.
6513 >>> s.add(x > 0, x < 2)
6517 >>> m.evaluate(x + 1)
6519 >>> m.evaluate(x == 1)
6522 >>> m.evaluate(y + x)
6526 >>> m.evaluate(y, model_completion=
True)
6529 >>> m.evaluate(y + x)
6532 return self.eval(t, model_completion)
6535 """Return the number of constant
and function declarations
in the model `self`.
6540 >>> s.add(x > 0, f(x) != x)
6547 num_consts = int(Z3_model_get_num_consts(self.ctx.ref(), self.model))
6548 num_funcs = int(Z3_model_get_num_funcs(self.ctx.ref(), self.model))
6549 return num_consts + num_funcs
6551 def get_interp(self, decl):
6552 """Return the interpretation
for a given declaration
or constant.
6557 >>> s.add(x > 0, x < 2, f(x) == 0)
6567 _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected")
6571 if decl.arity() == 0:
6572 _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast)
6573 if _r.value is None:
6575 r = _to_expr_ref(_r, self.ctx)
6577 fi = self.get_interp(get_as_array_func(r))
6589 sz = fi.num_entries()
6593 e = Store(e, fe.arg_value(0), fe.value())
6599 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
6603 def num_sorts(self):
6604 """Return the number of uninterpreted sorts that contain an interpretation
in the model `self`.
6607 >>> a, b =
Consts(
'a b', A)
6616 return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model))
6618 def get_sort(self, idx):
6619 """Return the uninterpreted sort at position `idx` < self.
num_sorts().
6623 >>> a1, a2 =
Consts(
'a1 a2', A)
6624 >>> b1, b2 =
Consts(
'b1 b2', B)
6626 >>> s.add(a1 != a2, b1 != b2)
6637 if idx >= self.num_sorts():
6639 return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx)
6642 """Return all uninterpreted sorts that have an interpretation
in the model `self`.
6646 >>> a1, a2 =
Consts(
'a1 a2', A)
6647 >>> b1, b2 =
Consts(
'b1 b2', B)
6649 >>> s.add(a1 != a2, b1 != b2)
6656 return [self.get_sort(i) for i in range(self.num_sorts())]
6658 def get_universe(self, s):
6659 """Return the interpretation
for the uninterpreted sort `s`
in the model `self`.
6662 >>> a, b =
Consts(
'a b', A)
6668 >>> m.get_universe(A)
6672 _z3_assert(isinstance(s, SortRef), "Z3 sort expected")
6674 return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx)
6678 def __getitem__(self, idx):
6679 """If `idx`
is an integer, then the declaration at position `idx`
in the model `self`
is returned.
6680 If `idx`
is a declaration, then the actual interpretation
is returned.
6682 The elements can be retrieved using position
or the actual declaration.
6687 >>> s.add(x > 0, x < 2, f(x) == 0)
6701 >>>
for d
in m: print(
"%s -> %s" % (d, m[d]))
6706 if idx >= len(self):
6708 num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
6709 if (idx < num_consts):
6710 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx)
6712 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx)
6713 if isinstance(idx, FuncDeclRef):
6714 return self.get_interp(idx)
6716 return self.get_interp(idx.decl())
6717 if isinstance(idx, SortRef):
6718 return self.get_universe(idx)
6720 _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected")
6724 """Return a list with all symbols that have an interpretation
in the model `self`.
6728 >>> s.add(x > 0, x < 2, f(x) == 0)
6736 for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)):
6737 r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx))
6738 for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)):
6739 r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
6742 def update_value(self, x, value):
6743 """Update the interpretation of a constant
"""
6746 if is_func_decl(x) and x.arity() != 0 and isinstance(value, FuncInterp):
6748 fi2 = Z3_add_func_interp(x.ctx_ref(), self.model, x.ast, value.else_value().ast);
6749 fi2 = FuncInterp(fi2, x.ctx)
6750 for i in range(value.num_entries()):
6752 n = Z3_func_entry_get_num_args(x.ctx_ref(), e.entry)
6755 v.push(e.arg_value(j))
6756 val = Z3_func_entry_get_value(x.ctx_ref(), e.entry)
6757 Z3_func_interp_add_entry(x.ctx_ref(), fi2.f, v.vector, val)
6759 if not is_func_decl(x) or x.arity() != 0:
6760 raise Z3Exception("Expecting 0-ary function or constant expression")
6761 value = _py2expr(value)
6762 Z3_add_const_interp(x.ctx_ref(), self.model, x.ast, value.ast)
6764 def translate(self, target):
6765 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
6768 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6769 model = Z3_model_translate(self.ctx.ref(), self.model, target.ref())
6770 return ModelRef(model, target)
6772 def project(self, vars, fml):
6773 """Perform model-based projection on fml with respect to vars.
6774 Assume that the model satisfies fml. Then compute a projection fml_p, such
6775 that vars do
not occur free
in fml_p, fml_p
is true
in the model
and
6776 fml_p => exists vars . fml
6778 ctx = self.ctx.ref()
6779 _vars = (Ast * len(vars))()
6780 for i in range(len(vars)):
6781 _vars[i] = vars[i].as_ast()
6782 return _to_expr_ref(Z3_qe_model_project(ctx, self.model, len(vars), _vars, fml.ast), self.ctx)
6784 def project_with_witness(self, vars, fml):
6785 """Perform model-based projection, but also include realizer terms
for the projected variables
"""
6786 ctx = self.ctx.ref()
6787 _vars = (Ast * len(vars))()
6788 for i in range(len(vars)):
6789 _vars[i] = vars[i].as_ast()
6791 result = Z3_qe_model_project_with_witness(ctx, self.model, len(vars), _vars, fml.ast, defs.map)
6792 result = _to_expr_ref(result, self.ctx)
6797 return self.translate(self.ctx)
6799 def __deepcopy__(self, memo={}):
6800 return self.translate(self.ctx)
6803 def Model(ctx=None, eval = {}):
6805 mdl = ModelRef(Z3_mk_model(ctx.ref()), ctx)
6806 for k, v in eval.items():
6807 mdl.update_value(k, v)
6812 """Return true
if n
is a Z3 expression of the form (_
as-array f).
"""
6813 return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
6816 def get_as_array_func(n):
6817 """Return the function declaration f associated with a Z3 expression of the form (_
as-array f).
"""
6819 _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
6820 return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
6822 #########################################
6826 #########################################
6830 """Statistics
for `Solver.check()`.
"""
6832 def __init__(self, stats, ctx):
6835 Z3_stats_inc_ref(self.ctx.ref(), self.stats)
6837 def __deepcopy__(self, memo={}):
6838 return Statistics(self.stats, self.ctx)
6841 if self.ctx.ref() is not None and Z3_stats_dec_ref is not None:
6842 Z3_stats_dec_ref(self.ctx.ref(), self.stats)
6848 out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
6851 out.write(u('<tr style="background-color:#CFCFCF">'))
6854 out.write(u("<tr>"))
6856 out.write(u("<td>%s</td><td>%s</td></tr>" % (k, v)))
6857 out.write(u("</table>"))
6858 return out.getvalue()
6860 return Z3_stats_to_string(self.ctx.ref(), self.stats)
6863 """Return the number of statistical counters.
6866 >>> s =
Then(
'simplify',
'nlsat').solver()
6870 >>> st = s.statistics()
6874 return int(Z3_stats_size(self.ctx.ref(), self.stats))
6876 def __getitem__(self, idx):
6877 """Return the value of statistical counter at position `idx`. The result
is a pair (key, value).
6880 >>> s =
Then(
'simplify',
'nlsat').solver()
6884 >>> st = s.statistics()
6888 (
'nlsat propagations', 2)
6890 (
'nlsat restarts', 1)
6892 if idx >= len(self):
6894 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
6895 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
6897 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
6898 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
6901 """Return the list of statistical counters.
6904 >>> s =
Then(
'simplify',
'nlsat').solver()
6908 >>> st = s.statistics()
6910 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
6912 def get_key_value(self, key):
6913 """Return the value of a particular statistical counter.
6916 >>> s =
Then(
'simplify',
'nlsat').solver()
6920 >>> st = s.statistics()
6921 >>> st.get_key_value(
'nlsat propagations')
6924 for idx in range(len(self)):
6925 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
6926 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
6927 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
6929 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
6930 raise Z3Exception("unknown key")
6932 def __getattr__(self, name):
6933 """Access the value of statistical using attributes.
6935 Remark: to access a counter containing blank spaces (e.g.,
'nlsat propagations'),
6936 we should use
'_' (e.g.,
'nlsat_propagations').
6939 >>> s =
Then(
'simplify',
'nlsat').solver()
6943 >>> st = s.statistics()
6944 >>> st.nlsat_propagations
6949 key = name.replace("_", " ")
6951 return self.get_key_value(key)
6953 raise AttributeError
6955 #########################################
6959 #########################################
6962 class CheckSatResult:
6963 """Represents the result of a satisfiability check: sat, unsat, unknown.
6969 >>> isinstance(r, CheckSatResult)
6973 def __init__(self, r):
6976 def __deepcopy__(self, memo={}):
6977 return CheckSatResult(self.r)
6979 def __eq__(self, other):
6980 return isinstance(other, CheckSatResult) and self.r == other.r
6982 def __ne__(self, other):
6983 return not self.__eq__(other)
6987 if self.r == Z3_L_TRUE:
6989 elif self.r == Z3_L_FALSE:
6990 return "<b>unsat</b>"
6992 return "<b>unknown</b>"
6994 if self.r == Z3_L_TRUE:
6996 elif self.r == Z3_L_FALSE:
7001 def _repr_html_(self):
7002 in_html = in_html_mode()
7005 set_html_mode(in_html)
7009 sat = CheckSatResult(Z3_L_TRUE)
7010 unsat = CheckSatResult(Z3_L_FALSE)
7011 unknown = CheckSatResult(Z3_L_UNDEF)
7014 class Solver(Z3PPObject):
7016 Solver API provides methods
for implementing the main SMT 2.0 commands:
7017 push, pop, check, get-model, etc.
7020 def __init__(self, solver=None, ctx=None, logFile=None):
7021 assert solver is None or ctx is not None
7022 self.ctx = _get_ctx(ctx)
7023 self.backtrack_level = 4000000000
7026 self.solver = Z3_mk_solver(self.ctx.ref())
7028 self.solver = solver
7029 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
7030 if logFile is not None:
7031 self.set("smtlib2_log", logFile)
7034 if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
7035 Z3_solver_dec_ref(self.ctx.ref(), self.solver)
7037 def __enter__(self):
7041 def __exit__(self, *exc_info):
7044 def set(self, *args, **keys):
7045 """Set a configuration option.
7046 The method `
help()`
return a string containing all available options.
7050 >>> s.set(mbqi=
True)
7051 >>> s.set(
'MBQI',
True)
7052 >>> s.set(
':mbqi',
True)
7054 p = args2params(args, keys, self.ctx)
7055 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
7058 """Create a backtracking point.
7077 Z3_solver_push(self.ctx.ref(), self.solver)
7079 def pop(self, num=1):
7080 """Backtrack \\c num backtracking points.
7099 Z3_solver_pop(self.ctx.ref(), self.solver, num)
7101 def num_scopes(self):
7102 """Return the current number of backtracking points.
7117 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
7120 """Remove all asserted constraints
and backtracking points created using `
push()`.
7131 Z3_solver_reset(self.ctx.ref(), self.solver)
7133 def assert_exprs(self, *args):
7134 """Assert constraints into the solver.
7138 >>> s.assert_exprs(x > 0, x < 2)
7142 args = _get_args(args)
7143 s = BoolSort(self.ctx)
7145 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7147 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
7150 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
7152 def add(self, *args):
7153 """Assert constraints into the solver.
7157 >>> s.add(x > 0, x < 2)
7161 self.assert_exprs(*args)
7163 def __iadd__(self, fml):
7167 def append(self, *args):
7168 """Assert constraints into the solver.
7172 >>> s.append(x > 0, x < 2)
7176 self.assert_exprs(*args)
7178 def insert(self, *args):
7179 """Assert constraints into the solver.
7183 >>> s.insert(x > 0, x < 2)
7187 self.assert_exprs(*args)
7189 def assert_and_track(self, a, p):
7190 """Assert constraint `a`
and track it
in the unsat core using the Boolean constant `p`.
7192 If `p`
is a string, it will be automatically converted into a Boolean constant.
7197 >>> s.set(unsat_core=
True)
7198 >>> s.assert_and_track(x > 0,
'p1')
7199 >>> s.assert_and_track(x != 1,
'p2')
7200 >>> s.assert_and_track(x < 0, p3)
7201 >>> print(s.check())
7203 >>> c = s.unsat_core()
7213 if isinstance(p, str):
7214 p = Bool(p, self.ctx)
7215 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7216 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7217 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
7219 def check(self, *assumptions):
7220 """Check whether the assertions
in the given solver plus the optional assumptions are consistent
or not.
7226 >>> s.add(x > 0, x < 2)
7229 >>> s.model().eval(x)
7235 >>> s.add(2**x == 4)
7239 s = BoolSort(self.ctx)
7240 assumptions = _get_args(assumptions)
7241 num = len(assumptions)
7242 _assumptions = (Ast * num)()
7243 for i in range(num):
7244 _assumptions[i] = s.cast(assumptions[i]).as_ast()
7245 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7246 return CheckSatResult(r)
7249 """Return a model
for the last `
check()`.
7251 This function raises an exception
if
7252 a model
is not available (e.g., last `
check()` returned unsat).
7256 >>> s.add(a + 2 == 0)
7263 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7265 raise Z3Exception("model is not available")
7267 def import_model_converter(self, other):
7268 """Import model converter
from other into the current solver
"""
7269 Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7271 def interrupt(self):
7272 """Interrupt the execution of the solver object.
7273 Remarks: This ensures that the interrupt applies only
7274 to the given solver object
and it applies only
if it
is running.
7276 Z3_solver_interrupt(self.ctx.ref(), self.solver)
7278 def unsat_core(self):
7279 """Return a subset (
as an AST vector) of the assumptions provided to the last
check().
7281 These are the assumptions Z3 used
in the unsatisfiability proof.
7282 Assumptions are available
in Z3. They are used to extract unsatisfiable cores.
7283 They may be also used to
"retract" assumptions. Note that, assumptions are
not really
7284 "soft constraints", but they can be used to implement them.
7286 >>> p1, p2, p3 =
Bools(
'p1 p2 p3')
7287 >>> x, y =
Ints(
'x y')
7292 >>> s.add(
Implies(p3, y > -3))
7293 >>> s.check(p1, p2, p3)
7295 >>> core = s.unsat_core()
7308 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7310 def consequences(self, assumptions, variables):
7311 """Determine fixed values
for the variables based on the solver state
and assumptions.
7313 >>> a, b, c, d =
Bools(
'a b c d')
7315 >>> s.consequences([a],[b,c,d])
7317 >>> s.consequences([
Not(c),d],[a,b,c,d])
7320 if isinstance(assumptions, list):
7321 _asms = AstVector(None, self.ctx)
7322 for a in assumptions:
7325 if isinstance(variables, list):
7326 _vars = AstVector(None, self.ctx)
7330 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7331 _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7332 consequences = AstVector(None, self.ctx)
7333 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7334 variables.vector, consequences.vector)
7335 sz = len(consequences)
7336 consequences = [consequences[i] for i in range(sz)]
7337 return CheckSatResult(r), consequences
7339 def from_file(self, filename):
7340 """Parse assertions
from a file
"""
7341 Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7343 def from_string(self, s):
7344 """Parse assertions
from a string
"""
7345 Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7347 def cube(self, vars=None):
7349 The method takes an optional set of variables that restrict which
7350 variables may be used
as a starting point
for cubing.
7351 If vars
is not None, then the first case split
is based on a variable
in
7354 self.cube_vs = AstVector(None, self.ctx)
7355 if vars is not None:
7357 self.cube_vs.push(v)
7359 lvl = self.backtrack_level
7360 self.backtrack_level = 4000000000
7361 r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7362 if (len(r) == 1 and is_false(r[0])):
7368 def cube_vars(self):
7369 """Access the set of variables that were touched by the most recently generated cube.
7370 This set of variables can be used
as a starting point
for additional cubes.
7371 The idea
is that variables that appear
in clauses that are reduced by the most recent
7372 cube are likely more useful to cube on.
"""
7376 """Retrieve congruence closure root of the term t relative to the current search state
7377 The function primarily works
for SimpleSolver. Terms
and variables that are
7378 eliminated during pre-processing are
not visible to the congruence closure.
7380 t = _py2expr(t, self.ctx)
7381 return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
7384 """Retrieve congruence closure sibling of the term t relative to the current search state
7385 The function primarily works
for SimpleSolver. Terms
and variables that are
7386 eliminated during pre-processing are
not visible to the congruence closure.
7388 t = _py2expr(t, self.ctx)
7389 return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
7391 def explain_congruent(self, a, b):
7392 """Explain congruence of a
and b relative to the current search state
"""
7393 a = _py2expr(a, self.ctx)
7394 b = _py2expr(b, self.ctx)
7395 return _to_expr_ref(Z3_solver_congruence_explain(self.ctx.ref(), self.solver, a.ast, b.ast), self.ctx)
7398 def solve_for(self, ts):
7399 """Retrieve a solution
for t relative to linear equations maintained
in the current state.
"""
7400 vars = AstVector(ctx=self.ctx);
7401 terms = AstVector(ctx=self.ctx);
7402 guards = AstVector(ctx=self.ctx);
7404 t = _py2expr(t, self.ctx)
7406 Z3_solver_solve_for(self.ctx.ref(), self.solver, vars.vector, terms.vector, guards.vector)
7407 return [(vars[i], terms[i], guards[i]) for i in range(len(vars))]
7411 """Return a proof
for the last `
check()`. Proof construction must be enabled.
"""
7412 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7414 def assertions(self):
7415 """Return an AST vector containing all added constraints.
7426 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7429 """Return an AST vector containing all currently inferred units.
7431 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7433 def non_units(self):
7434 """Return an AST vector containing all atomic formulas
in solver state that are
not units.
7436 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7438 def trail_levels(self):
7439 """Return trail
and decision levels of the solver state after a
check() call.
7441 trail = self.trail()
7442 levels = (ctypes.c_uint * len(trail))()
7443 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7444 return trail, levels
7446 def set_initial_value(self, var, value):
7447 """initialize the solver
's state by setting the initial value of var to value
7450 value = s.cast(value)
7451 Z3_solver_set_initial_value(self.ctx.ref(), self.solver, var.ast, value.ast)
7454 """Return trail of the solver state after a
check() call.
7456 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7458 def statistics(self):
7459 """Return statistics
for the last `
check()`.
7466 >>> st = s.statistics()
7467 >>> st.get_key_value(
'final checks')
7474 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7476 def reason_unknown(self):
7477 """Return a string describing why the last `
check()` returned `unknown`.
7481 >>> s.add(2**x == 4)
7484 >>> s.reason_unknown()
7485 '(incomplete (theory arithmetic))'
7487 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7490 """Display a string describing all available options.
"""
7491 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7493 def param_descrs(self):
7494 """Return the parameter description set.
"""
7495 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7498 """Return a formatted string with all added constraints.
"""
7499 return obj_to_string(self)
7501 def translate(self, target):
7502 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
7507 >>> s2 = s1.translate(c2)
7510 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7511 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7512 return Solver(solver, target)
7515 return self.translate(self.ctx)
7517 def __deepcopy__(self, memo={}):
7518 return self.translate(self.ctx)
7521 """Return a formatted string (
in Lisp-like format) with all added constraints.
7522 We say the string
is in s-expression format.
7530 return Z3_solver_to_string(self.ctx.ref(), self.solver)
7532 def dimacs(self, include_names=True):
7533 """Return a textual representation of the solver
in DIMACS format.
"""
7534 return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7537 """return SMTLIB2 formatted benchmark
for solver
's assertions"""
7544 for i
in range(sz1):
7545 v[i] = es[i].as_ast()
7547 e = es[sz1].as_ast()
7551 self.ctx.ref(),
"benchmark generated from python API",
"",
"unknown",
"", sz1, v, e,
7556 """Create a solver customized for the given logic.
7558 The parameter `logic` is a string. It should be contains
7559 the name of a SMT-LIB logic.
7560 See http://www.smtlib.org/ for the name of all available logics.
7562 >>> s = SolverFor("QF_LIA")
7577 """Return a simple general purpose solver with limited amount of preprocessing.
7579 >>> s = SimpleSolver()
7596 """Fixedpoint API provides methods for solving with recursive predicates"""
7599 assert fixedpoint
is None or ctx
is not None
7602 if fixedpoint
is None:
7613 if self.
fixedpoint is not None and self.ctx.ref()
is not None and Z3_fixedpoint_dec_ref
is not None:
7617 """Set a configuration option. The method `help()` return a string containing all available options.
7623 """Display a string describing all available options."""
7627 """Return the parameter description set."""
7631 """Assert constraints as background axioms for the fixedpoint solver."""
7632 args = _get_args(args)
7635 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
7645 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7653 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7657 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7661 """Assert rules defining recursive predicates to the fixedpoint solver.
7664 >>> s = Fixedpoint()
7665 >>> s.register_relation(a.decl())
7666 >>> s.register_relation(b.decl())
7679 body = _get_args(body)
7683 def rule(self, head, body=None, name=None):
7684 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7688 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7692 """Query the fixedpoint engine whether formula is derivable.
7693 You can also pass an tuple or list of recursive predicates.
7695 query = _get_args(query)
7697 if sz >= 1
and isinstance(query[0], FuncDeclRef):
7698 _decls = (FuncDecl * sz)()
7708 query =
And(query, self.
ctx)
7709 query = self.
abstract(query,
False)
7714 """Query the fixedpoint engine whether formula is derivable starting at the given query level.
7716 query = _get_args(query)
7718 if sz >= 1
and isinstance(query[0], FuncDecl):
7719 _z3_assert(
False,
"unsupported")
7725 query = self.
abstract(query,
False)
7726 r = Z3_fixedpoint_query_from_lvl(self.ctx.ref(), self.
fixedpoint, query.as_ast(), lvl)
7734 body = _get_args(body)
7739 """Retrieve answer from last query call."""
7741 return _to_expr_ref(r, self.
ctx)
7744 """Retrieve a ground cex from last query call."""
7745 r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.
fixedpoint)
7746 return _to_expr_ref(r, self.
ctx)
7749 """retrieve rules along the counterexample trace"""
7753 """retrieve rule names along the counterexample trace"""
7756 names = _symbol2py(self.
ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.
fixedpoint))
7758 return names.split(
";")
7761 """Retrieve number of levels used for predicate in PDR engine"""
7765 """Retrieve properties known about predicate for the level'th unfolding.
7766 -1 is treated as the limit (infinity)
7769 return _to_expr_ref(r, self.
ctx)
7772 """Add property to predicate for the level'th unfolding.
7773 -1 is treated as infinity (infinity)
7778 """Register relation as recursive"""
7779 relations = _get_args(relations)
7784 """Control how relation is represented"""
7785 representations = _get_args(representations)
7786 representations = [
to_symbol(s)
for s
in representations]
7787 sz = len(representations)
7788 args = (Symbol * sz)()
7790 args[i] = representations[i]
7794 """Parse rules and queries from a string"""
7798 """Parse rules and queries from a file"""
7802 """retrieve rules that have been added to fixedpoint context"""
7806 """retrieve assertions that have been added to fixedpoint context"""
7810 """Return a formatted string with all added rules and constraints."""
7814 """Return a formatted string (in Lisp-like format) with all added constraints.
7815 We say the string is in s-expression format.
7820 """Return a formatted string (in Lisp-like format) with all added constraints.
7821 We say the string is in s-expression format.
7822 Include also queries.
7824 args, len = _to_ast_array(queries)
7828 """Return statistics for the last `query()`.
7833 """Return a string describing why the last `query()` returned `unknown`.
7838 """Add variable or several variables.
7839 The added variable or variables will be bound in the rules
7842 vars = _get_args(vars)
7862 """Finite domain sort."""
7865 """Return the size of the finite domain sort"""
7866 r = (ctypes.c_ulonglong * 1)()
7870 raise Z3Exception(
"Failed to retrieve finite domain sort size")
7874 """Create a named finite domain sort of a given size sz"""
7875 if not isinstance(name, Symbol):
7882 """Return True if `s` is a Z3 finite-domain sort.
7884 >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7886 >>> is_finite_domain_sort(IntSort())
7889 return isinstance(s, FiniteDomainSortRef)
7893 """Finite-domain expressions."""
7896 """Return the sort of the finite-domain expression `self`."""
7900 """Return a Z3 floating point expression as a Python string."""
7905 """Return `True` if `a` is a Z3 finite-domain expression.
7907 >>> s = FiniteDomainSort('S', 100)
7908 >>> b = Const('b', s)
7909 >>> is_finite_domain(b)
7911 >>> is_finite_domain(Int('x'))
7914 return isinstance(a, FiniteDomainRef)
7918 """Integer values."""
7921 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral.
7923 >>> s = FiniteDomainSort('S', 100)
7924 >>> v = FiniteDomainVal(3, s)
7933 """Return a Z3 finite-domain numeral as a Python string.
7935 >>> s = FiniteDomainSort('S', 100)
7936 >>> v = FiniteDomainVal(42, s)
7944 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7946 >>> s = FiniteDomainSort('S', 256)
7947 >>> FiniteDomainVal(255, s)
7949 >>> FiniteDomainVal('100', s)
7959 """Return `True` if `a` is a Z3 finite-domain value.
7961 >>> s = FiniteDomainSort('S', 100)
7962 >>> b = Const('b', s)
7963 >>> is_finite_domain_value(b)
7965 >>> b = FiniteDomainVal(10, s)
7968 >>> is_finite_domain_value(b)
8015 def _global_on_model(ctx):
8016 (fn, mdl) = _on_models[ctx]
8020 _on_model_eh = on_model_eh_type(_global_on_model)
8024 """Optimize API provides methods for solving using objective functions and weighted soft constraints"""
8028 if optimize
is None:
8039 if self.
optimize is not None and self.ctx.ref()
is not None and Z3_optimize_dec_ref
is not None:
8052 """Set a configuration option.
8053 The method `help()` return a string containing all available options.
8059 """Display a string describing all available options."""
8063 """Return the parameter description set."""
8067 """Assert constraints as background axioms for the optimize solver."""
8068 args = _get_args(args)
8071 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
8079 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
8087 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
8089 If `p` is a string, it will be automatically converted into a Boolean constant.
8094 >>> s.assert_and_track(x > 0, 'p1')
8095 >>> s.assert_and_track(x != 1, 'p2')
8096 >>> s.assert_and_track(x < 0, p3)
8097 >>> print(s.check())
8099 >>> c = s.unsat_core()
8109 if isinstance(p, str):
8111 _z3_assert(isinstance(a, BoolRef),
"Boolean expression expected")
8112 _z3_assert(isinstance(p, BoolRef)
and is_const(p),
"Boolean expression expected")
8116 """Add soft constraint with optional weight and optional identifier.
8117 If no weight is supplied, then the penalty for violating the soft constraint
8119 Soft constraints are grouped by identifiers. Soft constraints that are
8120 added without identifiers are grouped by default.
8123 weight =
"%d" % weight
8124 elif isinstance(weight, float):
8125 weight =
"%f" % weight
8126 if not isinstance(weight, str):
8127 raise Z3Exception(
"weight should be a string or an integer")
8135 if sys.version_info.major >= 3
and isinstance(arg, Iterable):
8136 return [asoft(a)
for a
in arg]
8140 """initialize the solver's state by setting the initial value of var to value
8143 value = s.cast(value)
8147 """Add objective function to maximize."""
8155 """Add objective function to minimize."""
8163 """create a backtracking point for added rules, facts and assertions"""
8167 """restore to previously created backtracking point"""
8171 """Check consistency and produce optimal values."""
8172 assumptions = _get_args(assumptions)
8173 num = len(assumptions)
8174 _assumptions = (Ast * num)()
8175 for i
in range(num):
8176 _assumptions[i] = assumptions[i].as_ast()
8180 """Return a string that describes why the last `check()` returned `unknown`."""
8184 """Return a model for the last check()."""
8188 raise Z3Exception(
"model is not available")
8194 if not isinstance(obj, OptimizeObjective):
8195 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
8199 if not isinstance(obj, OptimizeObjective):
8200 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
8204 if not isinstance(obj, OptimizeObjective):
8205 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
8206 return obj.lower_values()
8209 if not isinstance(obj, OptimizeObjective):
8210 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
8211 return obj.upper_values()
8214 """Parse assertions and objectives from a file"""
8218 """Parse assertions and objectives from a string"""
8222 """Return an AST vector containing all added constraints."""
8226 """returns set of objective functions"""
8230 """Return a formatted string with all added rules and constraints."""
8234 """Return a formatted string (in Lisp-like format) with all added constraints.
8235 We say the string is in s-expression format.
8240 """Return statistics for the last check`.
8245 """Register a callback that is invoked with every incremental improvement to
8246 objective values. The callback takes a model as argument.
8247 The life-time of the model is limited to the callback so the
8248 model has to be (deep) copied if it is to be used after the callback
8250 id = len(_on_models) + 41
8252 _on_models[id] = (on_model, mdl)
8255 self.ctx.ref(), self.
optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
8265 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal.
8266 It also contains model and proof converters.
8278 if self.ctx.ref()
is not None and Z3_apply_result_dec_ref
is not None:
8282 """Return the number of subgoals in `self`.
8284 >>> a, b = Ints('a b')
8286 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
8287 >>> t = Tactic('split-clause')
8291 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'))
8294 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values'))
8301 """Return one of the subgoals stored in ApplyResult object `self`.
8303 >>> a, b = Ints('a b')
8305 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
8306 >>> t = Tactic('split-clause')
8309 [a == 0, Or(b == 0, b == 1), a > b]
8311 [a == 1, Or(b == 0, b == 1), a > b]
8313 if idx >= len(self):
8318 return obj_to_string(self)
8321 """Return a textual representation of the s-expression representing the set of subgoals in `self`."""
8325 """Return a Z3 expression consisting of all subgoals.
8330 >>> g.add(Or(x == 2, x == 3))
8331 >>> r = Tactic('simplify')(g)
8333 [[Not(x <= 1), Or(x == 2, x == 3)]]
8335 And(Not(x <= 1), Or(x == 2, x == 3))
8336 >>> r = Tactic('split-clause')(g)
8338 [[x > 1, x == 2], [x > 1, x == 3]]
8340 Or(And(x > 1, x == 2), And(x > 1, x == 3))
8357 """Simplifiers act as pre-processing utilities for solvers.
8358 Build a custom simplifier and add it to a solver"""
8363 if isinstance(simplifier, SimplifierObj):
8365 elif isinstance(simplifier, list):
8366 simps = [
Simplifier(s, ctx)
for s
in simplifier]
8368 for i
in range(1, len(simps)):
8374 _z3_assert(isinstance(simplifier, str),
"simplifier name expected")
8378 raise Z3Exception(
"unknown simplifier '%s'" % simplifier)
8385 if self.
simplifier is not None and self.ctx.ref()
is not None and Z3_simplifier_dec_ref
is not None:
8389 """Return a simplifier that uses the given configuration options"""
8394 """Return a solver that applies the simplification pre-processing specified by the simplifier"""
8398 """Display a string containing a description of the available options for the `self` simplifier."""
8402 """Return the parameter description set."""
8414 """Tactics transform, solver and/or simplify sets of constraints (Goal).
8415 A Tactic can be converted into a Solver using the method solver().
8417 Several combinators are available for creating new tactics using the built-in ones:
8418 Then(), OrElse(), FailIf(), Repeat(), When(), Cond().
8424 if isinstance(tactic, TacticObj):
8428 _z3_assert(isinstance(tactic, str),
"tactic name expected")
8432 raise Z3Exception(
"unknown tactic '%s'" % tactic)
8439 if self.
tactic is not None and self.ctx.ref()
is not None and Z3_tactic_dec_ref
is not None:
8443 """Create a solver using the tactic `self`.
8445 The solver supports the methods `push()` and `pop()`, but it
8446 will always solve each `check()` from scratch.
8448 >>> t = Then('simplify', 'nlsat')
8451 >>> s.add(x**2 == 2, x > 0)
8459 def apply(self, goal, *arguments, **keywords):
8460 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
8462 >>> x, y = Ints('x y')
8463 >>> t = Tactic('solve-eqs')
8464 >>> t.apply(And(x == 0, y >= x + 1))
8468 _z3_assert(isinstance(goal, (Goal, BoolRef)),
"Z3 Goal or Boolean expressions expected")
8469 goal = _to_goal(goal)
8470 if len(arguments) > 0
or len(keywords) > 0:
8477 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
8479 >>> x, y = Ints('x y')
8480 >>> t = Tactic('solve-eqs')
8481 >>> t(And(x == 0, y >= x + 1))
8484 return self.
apply(goal, *arguments, **keywords)
8487 """Display a string containing a description of the available options for the `self` tactic."""
8491 """Return the parameter description set."""
8496 if isinstance(a, BoolRef):
8497 goal =
Goal(ctx=a.ctx)
8504 def _to_tactic(t, ctx=None):
8505 if isinstance(t, Tactic):
8511 def _and_then(t1, t2, ctx=None):
8512 t1 = _to_tactic(t1, ctx)
8513 t2 = _to_tactic(t2, ctx)
8515 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
8519 def _or_else(t1, t2, ctx=None):
8520 t1 = _to_tactic(t1, ctx)
8521 t2 = _to_tactic(t2, ctx)
8523 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
8528 """Return a tactic that applies the tactics in `*ts` in sequence.
8530 >>> x, y = Ints('x y')
8531 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
8532 >>> t(And(x == 0, y > x + 1))
8534 >>> t(And(x == 0, y > x + 1)).as_expr()
8538 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
8539 ctx = ks.get(
"ctx",
None)
8542 for i
in range(num - 1):
8543 r = _and_then(r, ts[i + 1], ctx)
8548 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
8550 >>> x, y = Ints('x y')
8551 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
8552 >>> t(And(x == 0, y > x + 1))
8554 >>> t(And(x == 0, y > x + 1)).as_expr()
8561 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
8564 >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
8565 >>> # Tactic split-clause fails if there is no clause in the given goal.
8568 >>> t(Or(x == 0, x == 1))
8569 [[x == 0], [x == 1]]
8572 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
8573 ctx = ks.get(
"ctx",
None)
8576 for i
in range(num - 1):
8577 r = _or_else(r, ts[i + 1], ctx)
8582 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
8585 >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
8590 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
8591 ctx = _get_ctx(ks.get(
"ctx",
None))
8592 ts = [_to_tactic(t, ctx)
for t
in ts]
8594 _args = (TacticObj * sz)()
8596 _args[i] = ts[i].tactic
8601 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1.
8602 The subgoals are processed in parallel.
8604 >>> x, y = Ints('x y')
8605 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
8606 >>> t(And(Or(x == 1, x == 2), y == x + 1))
8607 [[x == 1, y == 2], [x == 2, y == 3]]
8609 t1 = _to_tactic(t1, ctx)
8610 t2 = _to_tactic(t2, ctx)
8612 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
8617 """Alias for ParThen(t1, t2, ctx)."""
8622 """Return a tactic that applies tactic `t` using the given configuration options.
8624 >>> x, y = Ints('x y')
8625 >>> t = With(Tactic('simplify'), som=True)
8626 >>> t((x + 1)*(y + 2) == 0)
8627 [[2*x + y + x*y == -2]]
8629 ctx = keys.pop(
"ctx",
None)
8630 t = _to_tactic(t, ctx)
8636 """Return a tactic that applies tactic `t` using the given configuration options.
8638 >>> x, y = Ints('x y')
8640 >>> p.set("som", True)
8641 >>> t = WithParams(Tactic('simplify'), p)
8642 >>> t((x + 1)*(y + 2) == 0)
8643 [[2*x + y + x*y == -2]]
8645 t = _to_tactic(t,
None)
8650 """Return a tactic that keeps applying `t` until the goal is not modified anymore
8651 or the maximum number of iterations `max` is reached.
8653 >>> x, y = Ints('x y')
8654 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
8655 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
8657 >>> for subgoal in r: print(subgoal)
8658 [x == 0, y == 0, x > y]
8659 [x == 0, y == 1, x > y]
8660 [x == 1, y == 0, x > y]
8661 [x == 1, y == 1, x > y]
8662 >>> t = Then(t, Tactic('propagate-values'))
8666 t = _to_tactic(t, ctx)
8671 """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
8673 If `t` does not terminate in `ms` milliseconds, then it fails.
8675 t = _to_tactic(t, ctx)
8680 """Return a list of all available tactics in Z3.
8683 >>> l.count('simplify') == 1
8691 """Return a short description for the tactic named `name`.
8693 >>> d = tactic_description('simplify')
8700 """Display a (tabular) description of all available tactics in Z3."""
8703 print(
'<table border="1" cellpadding="2" cellspacing="0">')
8706 print(
'<tr style="background-color:#CFCFCF">')
8711 print(
"<td>%s</td><td>%s</td></tr>" % (t, insert_line_breaks(
tactic_description(t), 40)))
8719 """Probes are used to inspect a goal (aka problem) and collect information that may be used
8720 to decide which solver and/or preprocessing step will be used.
8726 if isinstance(probe, ProbeObj):
8728 elif isinstance(probe, float):
8730 elif _is_int(probe):
8732 elif isinstance(probe, bool):
8739 _z3_assert(isinstance(probe, str),
"probe name expected")
8743 raise Z3Exception(
"unknown probe '%s'" % probe)
8750 if self.
probe is not None and self.ctx.ref()
is not None and Z3_probe_dec_ref
is not None:
8754 """Return a probe that evaluates to "true" when the value returned by `self`
8755 is less than the value returned by `other`.
8757 >>> p = Probe('size') < 10
8768 """Return a probe that evaluates to "true" when the value returned by `self`
8769 is greater than the value returned by `other`.
8771 >>> p = Probe('size') > 10
8782 """Return a probe that evaluates to "true" when the value returned by `self`
8783 is less than or equal to the value returned by `other`.
8785 >>> p = Probe('size') <= 2
8796 """Return a probe that evaluates to "true" when the value returned by `self`
8797 is greater than or equal to the value returned by `other`.
8799 >>> p = Probe('size') >= 2
8810 """Return a probe that evaluates to "true" when the value returned by `self`
8811 is equal to the value returned by `other`.
8813 >>> p = Probe('size') == 2
8824 """Return a probe that evaluates to "true" when the value returned by `self`
8825 is not equal to the value returned by `other`.
8827 >>> p = Probe('size') != 2
8839 """Evaluate the probe `self` in the given goal.
8841 >>> p = Probe('size')
8851 >>> p = Probe('num-consts')
8854 >>> p = Probe('is-propositional')
8857 >>> p = Probe('is-qflia')
8862 _z3_assert(isinstance(goal, (Goal, BoolRef)),
"Z3 Goal or Boolean expression expected")
8863 goal = _to_goal(goal)
8868 """Return `True` if `p` is a Z3 probe.
8870 >>> is_probe(Int('x'))
8872 >>> is_probe(Probe('memory'))
8875 return isinstance(p, Probe)
8878 def _to_probe(p, ctx=None):
8882 return Probe(p, ctx)
8886 """Return a list of all available probes in Z3.
8889 >>> l.count('memory') == 1
8897 """Return a short description for the probe named `name`.
8899 >>> d = probe_description('memory')
8906 """Display a (tabular) description of all available probes in Z3."""
8909 print(
'<table border="1" cellpadding="2" cellspacing="0">')
8912 print(
'<tr style="background-color:#CFCFCF">')
8917 print(
"<td>%s</td><td>%s</td></tr>" % (p, insert_line_breaks(
probe_description(p), 40)))
8924 def _probe_nary(f, args, ctx):
8926 _z3_assert(len(args) > 0,
"At least one argument expected")
8928 r = _to_probe(args[0], ctx)
8929 for i
in range(num - 1):
8930 r =
Probe(f(ctx.ref(), r.probe, _to_probe(args[i + 1], ctx).probe), ctx)
8934 def _probe_and(args, ctx):
8935 return _probe_nary(Z3_probe_and, args, ctx)
8938 def _probe_or(args, ctx):
8939 return _probe_nary(Z3_probe_or, args, ctx)
8943 """Return a tactic that fails if the probe `p` evaluates to true.
8944 Otherwise, it returns the input goal unmodified.
8946 In the following example, the tactic applies 'simplify' if and only if there are
8947 more than 2 constraints in the goal.
8949 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8950 >>> x, y = Ints('x y')
8956 >>> g.add(x == y + 1)
8958 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8960 p = _to_probe(p, ctx)
8965 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true.
8966 Otherwise, it returns the input goal unmodified.
8968 >>> t = When(Probe('size') > 2, Tactic('simplify'))
8969 >>> x, y = Ints('x y')
8975 >>> g.add(x == y + 1)
8977 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8979 p = _to_probe(p, ctx)
8980 t = _to_tactic(t, ctx)
8985 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8987 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8989 p = _to_probe(p, ctx)
8990 t1 = _to_tactic(t1, ctx)
8991 t2 = _to_tactic(t2, ctx)
9002 """Simplify the expression `a` using the given options.
9004 This function has many options. Use `help_simplify` to obtain the complete list.
9008 >>> simplify(x + 1 + y + x + 1)
9010 >>> simplify((x + 1)*(y + 1), som=True)
9012 >>> simplify(Distinct(x, y, 1), blast_distinct=True)
9013 And(Not(x == y), Not(x == 1), Not(y == 1))
9014 >>> simplify(And(x == 0, y == 1), elim_and=True)
9015 Not(Or(Not(x == 0), Not(y == 1)))
9018 _z3_assert(
is_expr(a),
"Z3 expression expected")
9019 if len(arguments) > 0
or len(keywords) > 0:
9021 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
9023 return _to_expr_ref(
Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
9027 """Return a string describing all options available for Z3 `simplify` procedure."""
9032 """Return the set of parameter descriptions for Z3 `simplify` procedure."""
9037 """Apply substitution m on t, m is a list of pairs of the form (from, to).
9038 Every occurrence in t of from is replaced with to.
9042 >>> substitute(x + 1, (x, y + 1))
9044 >>> f = Function('f', IntSort(), IntSort())
9045 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
9048 if isinstance(m, tuple):
9050 if isinstance(m1, list)
and all(isinstance(p, tuple)
for p
in m1):
9053 _z3_assert(
is_expr(t),
"Z3 expression expected")
9055 all([isinstance(p, tuple)
and is_expr(p[0])
and is_expr(p[1])
for p
in m]),
9056 "Z3 invalid substitution, expression pairs expected.")
9058 all([p[0].sort().
eq(p[1].sort())
for p
in m]),
9059 'Z3 invalid substitution, mismatching "from" and "to" sorts.')
9061 _from = (Ast * num)()
9063 for i
in range(num):
9064 _from[i] = m[i][0].as_ast()
9065 _to[i] = m[i][1].as_ast()
9066 return _to_expr_ref(
Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
9070 """Substitute the free variables in t with the expression in m.
9072 >>> v0 = Var(0, IntSort())
9073 >>> v1 = Var(1, IntSort())
9075 >>> f = Function('f', IntSort(), IntSort(), IntSort())
9076 >>> # replace v0 with x+1 and v1 with x
9077 >>> substitute_vars(f(v0, v1), x + 1, x)
9081 _z3_assert(
is_expr(t),
"Z3 expression expected")
9082 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
9085 for i
in range(num):
9086 _to[i] = m[i].as_ast()
9090 """Apply substitution m on t, m is a list of pairs of a function and expression (from, to)
9091 Every occurrence in to of the function from is replaced with the expression to.
9092 The expression to can have free variables, that refer to the arguments of from.
9095 if isinstance(m, tuple):
9097 if isinstance(m1, list)
and all(isinstance(p, tuple)
for p
in m1):
9100 _z3_assert(
is_expr(t),
"Z3 expression expected")
9101 _z3_assert(all([isinstance(p, tuple)
and is_func_decl(p[0])
and is_expr(p[1])
for p
in m]),
"Z3 invalid substitution, function pairs expected.")
9103 _from = (FuncDecl * num)()
9105 for i
in range(num):
9106 _from[i] = m[i][0].as_func_decl()
9107 _to[i] = m[i][1].as_ast()
9108 return _to_expr_ref(
Z3_substitute_funs(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
9112 """Create the sum of the Z3 expressions.
9114 >>> a, b, c = Ints('a b c')
9119 >>> A = IntVector('a', 5)
9121 a__0 + a__1 + a__2 + a__3 + a__4
9123 args = _get_args(args)
9126 ctx = _ctx_from_ast_arg_list(args)
9128 return _reduce(
lambda a, b: a + b, args, 0)
9129 args = _coerce_expr_list(args, ctx)
9131 return _reduce(
lambda a, b: a + b, args, 0)
9133 _args, sz = _to_ast_array(args)
9138 """Create the product of the Z3 expressions.
9140 >>> a, b, c = Ints('a b c')
9141 >>> Product(a, b, c)
9143 >>> Product([a, b, c])
9145 >>> A = IntVector('a', 5)
9147 a__0*a__1*a__2*a__3*a__4
9149 args = _get_args(args)
9152 ctx = _ctx_from_ast_arg_list(args)
9154 return _reduce(
lambda a, b: a * b, args, 1)
9155 args = _coerce_expr_list(args, ctx)
9157 return _reduce(
lambda a, b: a * b, args, 1)
9159 _args, sz = _to_ast_array(args)
9163 """Create the absolute value of an arithmetic expression"""
9164 return If(arg > 0, arg, -arg)
9168 """Create an at-most Pseudo-Boolean k constraint.
9170 >>> a, b, c = Bools('a b c')
9171 >>> f = AtMost(a, b, c, 2)
9173 args = _get_args(args)
9175 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
9176 ctx = _ctx_from_ast_arg_list(args)
9178 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
9179 args1 = _coerce_expr_list(args[:-1], ctx)
9181 _args, sz = _to_ast_array(args1)
9186 """Create an at-least Pseudo-Boolean k constraint.
9188 >>> a, b, c = Bools('a b c')
9189 >>> f = AtLeast(a, b, c, 2)
9191 args = _get_args(args)
9193 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
9194 ctx = _ctx_from_ast_arg_list(args)
9196 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
9197 args1 = _coerce_expr_list(args[:-1], ctx)
9199 _args, sz = _to_ast_array(args1)
9203 def _reorder_pb_arg(arg):
9205 if not _is_int(b)
and _is_int(a):
9210 def _pb_args_coeffs(args, default_ctx=None):
9211 args = _get_args_ast_list(args)
9213 return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
9214 args = [_reorder_pb_arg(arg)
for arg
in args]
9215 args, coeffs = zip(*args)
9217 _z3_assert(len(args) > 0,
"Non empty list of arguments expected")
9218 ctx = _ctx_from_ast_arg_list(args)
9220 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
9221 args = _coerce_expr_list(args, ctx)
9222 _args, sz = _to_ast_array(args)
9223 _coeffs = (ctypes.c_int * len(coeffs))()
9224 for i
in range(len(coeffs)):
9225 _z3_check_cint_overflow(coeffs[i],
"coefficient")
9226 _coeffs[i] = coeffs[i]
9227 return ctx, sz, _args, _coeffs, args
9231 """Create a Pseudo-Boolean inequality k constraint.
9233 >>> a, b, c = Bools('a b c')
9234 >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
9236 _z3_check_cint_overflow(k,
"k")
9237 ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
9242 """Create a Pseudo-Boolean inequality k constraint.
9244 >>> a, b, c = Bools('a b c')
9245 >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
9247 _z3_check_cint_overflow(k,
"k")
9248 ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
9253 """Create a Pseudo-Boolean equality k constraint.
9255 >>> a, b, c = Bools('a b c')
9256 >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
9258 _z3_check_cint_overflow(k,
"k")
9259 ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
9264 """Solve the constraints `*args`.
9266 This is a simple function for creating demonstrations. It creates a solver,
9267 configure it using the options in `keywords`, adds the constraints
9268 in `args`, and invokes check.
9271 >>> solve(a > 0, a < 2)
9274 show = keywords.pop(
"show",
False)
9282 print(
"no solution")
9284 print(
"failed to solve")
9294 """Solve the constraints `*args` using solver `s`.
9296 This is a simple function for creating demonstrations. It is similar to `solve`,
9297 but it uses the given solver `s`.
9298 It configures solver `s` using the options in `keywords`, adds the constraints
9299 in `args`, and invokes check.
9301 show = keywords.pop(
"show",
False)
9303 _z3_assert(isinstance(s, Solver),
"Solver object expected")
9311 print(
"no solution")
9313 print(
"failed to solve")
9324 def prove(claim, show=False, **keywords):
9325 """Try to prove the given claim.
9327 This is a simple function for creating demonstrations. It tries to prove
9328 `claim` by showing the negation is unsatisfiable.
9330 >>> p, q = Bools('p q')
9331 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
9335 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
9345 print(
"failed to prove")
9348 print(
"counterexample")
9352 def _solve_html(*args, **keywords):
9353 """Version of function `solve` that renders HTML output."""
9354 show = keywords.pop(
"show",
False)
9359 print(
"<b>Problem:</b>")
9363 print(
"<b>no solution</b>")
9365 print(
"<b>failed to solve</b>")
9372 print(
"<b>Solution:</b>")
9376 def _solve_using_html(s, *args, **keywords):
9377 """Version of function `solve_using` that renders HTML."""
9378 show = keywords.pop(
"show",
False)
9380 _z3_assert(isinstance(s, Solver),
"Solver object expected")
9384 print(
"<b>Problem:</b>")
9388 print(
"<b>no solution</b>")
9390 print(
"<b>failed to solve</b>")
9397 print(
"<b>Solution:</b>")
9401 def _prove_html(claim, show=False, **keywords):
9402 """Version of function `prove` that renders HTML."""
9404 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
9412 print(
"<b>proved</b>")
9414 print(
"<b>failed to prove</b>")
9417 print(
"<b>counterexample</b>")
9421 def _dict2sarray(sorts, ctx):
9423 _names = (Symbol * sz)()
9424 _sorts = (Sort * sz)()
9429 _z3_assert(isinstance(k, str),
"String expected")
9430 _z3_assert(
is_sort(v),
"Z3 sort expected")
9434 return sz, _names, _sorts
9437 def _dict2darray(decls, ctx):
9439 _names = (Symbol * sz)()
9440 _decls = (FuncDecl * sz)()
9445 _z3_assert(isinstance(k, str),
"String expected")
9449 _decls[i] = v.decl().ast
9453 return sz, _names, _decls
9462 if self.ctx.ref()
is not None and self.
pctx is not None and Z3_parser_context_dec_ref
is not None:
9476 """Parse a string in SMT 2.0 format using the given sorts and decls.
9478 The arguments sorts and decls are Python dictionaries used to initialize
9479 the symbol table used for the SMT 2.0 parser.
9481 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
9483 >>> x, y = Ints('x y')
9484 >>> f = Function('f', IntSort(), IntSort())
9485 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
9487 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
9491 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
9492 dsz, dnames, ddecls = _dict2darray(decls, ctx)
9493 return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
9496 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
9497 """Parse a file
in SMT 2.0 format using the given sorts
and decls.
9502 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
9503 dsz, dnames, ddecls = _dict2darray(decls, ctx)
9504 return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
9507 #########################################
9509 # Floating-Point Arithmetic
9511 #########################################
9514 # Global default rounding mode
9515 _dflt_rounding_mode = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
9516 _dflt_fpsort_ebits = 11
9517 _dflt_fpsort_sbits = 53
9520 def get_default_rounding_mode(ctx=None):
9521 """Retrieves the
global default rounding mode.
"""
9522 global _dflt_rounding_mode
9523 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
9525 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
9527 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
9529 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
9531 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
9535 _ROUNDING_MODES = frozenset({
9536 Z3_OP_FPA_RM_TOWARD_ZERO,
9537 Z3_OP_FPA_RM_TOWARD_NEGATIVE,
9538 Z3_OP_FPA_RM_TOWARD_POSITIVE,
9539 Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
9540 Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
9544 def set_default_rounding_mode(rm, ctx=None):
9545 global _dflt_rounding_mode
9546 if is_fprm_value(rm):
9547 _dflt_rounding_mode = rm.kind()
9549 _z3_assert(_dflt_rounding_mode in _ROUNDING_MODES, "illegal rounding mode")
9550 _dflt_rounding_mode = rm
9553 def get_default_fp_sort(ctx=None):
9554 return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
9557 def set_default_fp_sort(ebits, sbits, ctx=None):
9558 global _dflt_fpsort_ebits
9559 global _dflt_fpsort_sbits
9560 _dflt_fpsort_ebits = ebits
9561 _dflt_fpsort_sbits = sbits
9564 def _dflt_rm(ctx=None):
9565 return get_default_rounding_mode(ctx)
9568 def _dflt_fps(ctx=None):
9569 return get_default_fp_sort(ctx)
9572 def _coerce_fp_expr_list(alist, ctx):
9573 first_fp_sort = None
9576 if first_fp_sort is None:
9577 first_fp_sort = a.sort()
9578 elif first_fp_sort == a.sort():
9579 pass # OK, same as before
9581 # we saw at least 2 different float sorts; something will
9582 # throw a sort mismatch later, for now assume None.
9583 first_fp_sort = None
9587 for i in range(len(alist)):
9589 is_repr = isinstance(a, str) and a.contains("2**(") and a.endswith(")")
9590 if is_repr or _is_int(a) or isinstance(a, (float, bool)):
9591 r.append(FPVal(a, None, first_fp_sort, ctx))
9594 return _coerce_expr_list(r, ctx)
9599 class FPSortRef(SortRef):
9600 """Floating-point sort.
"""
9603 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint sort `self`.
9608 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast))
9611 """Retrieves the number of bits reserved
for the significand
in the FloatingPoint sort `self`.
9616 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast))
9618 def cast(self, val):
9619 """Try to cast `val`
as a floating-point expression.
9623 >>> b.cast(1.0).
sexpr()
9624 '(fp #b0 #x7f #b00000000000000000000000)'
9628 _z3_assert(self.ctx == val.ctx, "Context mismatch")
9631 return FPVal(val, None, self, self.ctx)
9634 def Float16(ctx=None):
9635 """Floating-point 16-bit (half) sort.
"""
9637 return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
9640 def FloatHalf(ctx=None):
9641 """Floating-point 16-bit (half) sort.
"""
9643 return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
9646 def Float32(ctx=None):
9647 """Floating-point 32-bit (single) sort.
"""
9649 return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
9652 def FloatSingle(ctx=None):
9653 """Floating-point 32-bit (single) sort.
"""
9655 return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
9658 def Float64(ctx=None):
9659 """Floating-point 64-bit (double) sort.
"""
9661 return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
9664 def FloatDouble(ctx=None):
9665 """Floating-point 64-bit (double) sort.
"""
9667 return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
9670 def Float128(ctx=None):
9671 """Floating-point 128-bit (quadruple) sort.
"""
9673 return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
9676 def FloatQuadruple(ctx=None):
9677 """Floating-point 128-bit (quadruple) sort.
"""
9679 return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
9682 class FPRMSortRef(SortRef):
9683 """"Floating-point rounding mode sort."""
9687 """Return True if `s` is a Z3 floating-point sort.
9694 return isinstance(s, FPSortRef)
9697 def is_fprm_sort(s):
9698 """Return
True if `s`
is a Z3 floating-point rounding mode sort.
9705 return isinstance(s, FPRMSortRef)
9710 class FPRef(ExprRef):
9711 """Floating-point expressions.
"""
9714 """Return the sort of the floating-point expression `self`.
9719 >>> x.sort() ==
FPSort(8, 24)
9722 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
9725 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
9730 return self.sort().ebits()
9733 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
9738 return self.sort().sbits()
9740 def as_string(self):
9741 """Return a Z3 floating point expression
as a Python string.
"""
9742 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
9744 def __le__(self, other):
9745 return fpLEQ(self, other, self.ctx)
9747 def __lt__(self, other):
9748 return fpLT(self, other, self.ctx)
9750 def __ge__(self, other):
9751 return fpGEQ(self, other, self.ctx)
9753 def __gt__(self, other):
9754 return fpGT(self, other, self.ctx)
9756 def __add__(self, other):
9757 """Create the Z3 expression `self + other`.
9766 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9767 return fpAdd(_dflt_rm(), a, b, self.ctx)
9769 def __radd__(self, other):
9770 """Create the Z3 expression `other + self`.
9776 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9777 return fpAdd(_dflt_rm(), a, b, self.ctx)
9779 def __sub__(self, other):
9780 """Create the Z3 expression `self - other`.
9789 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9790 return fpSub(_dflt_rm(), a, b, self.ctx)
9792 def __rsub__(self, other):
9793 """Create the Z3 expression `other - self`.
9799 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9800 return fpSub(_dflt_rm(), a, b, self.ctx)
9802 def __mul__(self, other):
9803 """Create the Z3 expression `self * other`.
9814 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9815 return fpMul(_dflt_rm(), a, b, self.ctx)
9817 def __rmul__(self, other):
9818 """Create the Z3 expression `other * self`.
9827 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9828 return fpMul(_dflt_rm(), a, b, self.ctx)
9831 """Create the Z3 expression `+self`.
"""
9835 """Create the Z3 expression `-self`.
9843 def __div__(self, other):
9844 """Create the Z3 expression `self / other`.
9855 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9856 return fpDiv(_dflt_rm(), a, b, self.ctx)
9858 def __rdiv__(self, other):
9859 """Create the Z3 expression `other / self`.
9868 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9869 return fpDiv(_dflt_rm(), a, b, self.ctx)
9871 def __truediv__(self, other):
9872 """Create the Z3 expression division `self / other`.
"""
9873 return self.__div__(other)
9875 def __rtruediv__(self, other):
9876 """Create the Z3 expression division `other / self`.
"""
9877 return self.__rdiv__(other)
9879 def __mod__(self, other):
9880 """Create the Z3 expression mod `self % other`.
"""
9881 return fpRem(self, other)
9883 def __rmod__(self, other):
9884 """Create the Z3 expression mod `other % self`.
"""
9885 return fpRem(other, self)
9888 class FPRMRef(ExprRef):
9889 """Floating-point rounding mode expressions
"""
9891 def as_string(self):
9892 """Return a Z3 floating point expression
as a Python string.
"""
9893 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
9896 def RoundNearestTiesToEven(ctx=None):
9898 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
9903 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
9906 def RoundNearestTiesToAway(ctx=None):
9908 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
9913 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
9916 def RoundTowardPositive(ctx=None):
9918 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
9923 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
9926 def RoundTowardNegative(ctx=None):
9928 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
9933 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
9936 def RoundTowardZero(ctx=None):
9938 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
9943 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
9947 """Return `
True`
if `a`
is a Z3 floating-point rounding mode expression.
9956 return isinstance(a, FPRMRef)
9959 def is_fprm_value(a):
9960 """Return `
True`
if `a`
is a Z3 floating-point rounding mode numeral value.
"""
9961 return is_fprm(a) and _is_numeral(a.ctx, a.ast)
9966 class FPNumRef(FPRef):
9967 """The sign of the numeral.
9978 num = (ctypes.c_int)()
9979 nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num))
9981 raise Z3Exception("error retrieving the sign of a numeral.")
9982 return num.value != 0
9984 """The sign of a floating-point numeral
as a bit-vector expression.
9986 Remark: NaN
's are invalid arguments.
9989 def sign_as_bv(self):
9990 return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx)
9992 """The significand of the numeral.
9999 def significand(self):
10000 return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())
10002 """The significand of the numeral
as a long.
10005 >>> x.significand_as_long()
10009 def significand_as_long(self):
10010 ptr = (ctypes.c_ulonglong * 1)()
10011 if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr):
10012 raise Z3Exception("error retrieving the significand of a numeral.")
10015 """The significand of the numeral
as a bit-vector expression.
10017 Remark: NaN are invalid arguments.
10020 def significand_as_bv(self):
10021 return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx)
10023 """The exponent of the numeral.
10030 def exponent(self, biased=True):
10031 return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased)
10033 """The exponent of the numeral
as a long.
10036 >>> x.exponent_as_long()
10040 def exponent_as_long(self, biased=True):
10041 ptr = (ctypes.c_longlong * 1)()
10042 if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased):
10043 raise Z3Exception("error retrieving the exponent of a numeral.")
10046 """The exponent of the numeral
as a bit-vector expression.
10048 Remark: NaNs are invalid arguments.
10051 def exponent_as_bv(self, biased=True):
10052 return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx)
10054 """Indicates whether the numeral
is a NaN.
"""
10057 return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast())
10059 """Indicates whether the numeral
is +oo
or -oo.
"""
10062 return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast())
10064 """Indicates whether the numeral
is +zero
or -zero.
"""
10067 return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast())
10069 """Indicates whether the numeral
is normal.
"""
10071 def isNormal(self):
10072 return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast())
10074 """Indicates whether the numeral
is subnormal.
"""
10076 def isSubnormal(self):
10077 return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
10079 """Indicates whether the numeral
is positive.
"""
10081 def isPositive(self):
10082 return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
10084 """Indicates whether the numeral
is negative.
"""
10086 def isNegative(self):
10087 return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast())
10090 The string representation of the numeral.
10097 def as_string(self):
10098 s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast())
10099 return ("FPVal(%s, %s)" % (s, self.sort()))
10101 def py_value(self):
10102 bv = simplify(fpToIEEEBV(self))
10103 binary = bv.py_value()
10104 if not isinstance(binary, int):
10106 # Decode the IEEE 754 binary representation
10108 bytes_rep = binary.to_bytes(8, byteorder='big')
10109 return struct.unpack('>d', bytes_rep)[0]
10113 """Return `
True`
if `a`
is a Z3 floating-point expression.
10123 return isinstance(a, FPRef)
10126 def is_fp_value(a):
10127 """Return `
True`
if `a`
is a Z3 floating-point numeral value.
10138 return is_fp(a) and _is_numeral(a.ctx, a.ast)
10141 def FPSort(ebits, sbits, ctx=None):
10142 """Return a Z3 floating-point sort of the given sizes. If `ctx=
None`, then the
global context
is used.
10144 >>> Single =
FPSort(8, 24)
10145 >>> Double =
FPSort(11, 53)
10148 >>> x =
Const(
'x', Single)
10152 ctx = _get_ctx(ctx)
10153 return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
10156 def _to_float_str(val, exp=0):
10157 if isinstance(val, float):
10158 if math.isnan(val):
10161 sone = math.copysign(1.0, val)
10166 elif val == float("+inf"):
10168 elif val == float("-inf"):
10171 v = val.as_integer_ratio()
10174 rvs = str(num) + "/" + str(den)
10175 res = rvs + "p" + _to_int_str(exp)
10176 elif isinstance(val, bool):
10183 elif isinstance(val, str):
10184 inx = val.find("*(2**")
10187 elif val[-1] == ")":
10189 exp = str(int(val[inx + 5:-1]) + int(exp))
10191 _z3_assert(False, "String does not have floating-point numeral form.")
10193 _z3_assert(False, "Python value cannot be used to create floating-point numerals.")
10197 return res + "p" + exp
10201 """Create a Z3 floating-point NaN term.
10204 >>> set_fpa_pretty(
True)
10207 >>> pb = get_fpa_pretty()
10208 >>> set_fpa_pretty(
False)
10211 >>> set_fpa_pretty(pb)
10213 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10214 return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
10217 def fpPlusInfinity(s):
10218 """Create a Z3 floating-point +oo term.
10221 >>> pb = get_fpa_pretty()
10222 >>> set_fpa_pretty(
True)
10225 >>> set_fpa_pretty(
False)
10228 >>> set_fpa_pretty(pb)
10230 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10231 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
10234 def fpMinusInfinity(s):
10235 """Create a Z3 floating-point -oo term.
"""
10236 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10237 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
10240 def fpInfinity(s, negative):
10241 """Create a Z3 floating-point +oo
or -oo term.
"""
10242 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10243 _z3_assert(isinstance(negative, bool), "expected Boolean flag")
10244 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
10248 """Create a Z3 floating-point +0.0 term.
"""
10249 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10250 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
10253 def fpMinusZero(s):
10254 """Create a Z3 floating-point -0.0 term.
"""
10255 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10256 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
10259 def fpZero(s, negative):
10260 """Create a Z3 floating-point +0.0
or -0.0 term.
"""
10261 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10262 _z3_assert(isinstance(negative, bool), "expected Boolean flag")
10263 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
10266 def FPVal(sig, exp=None, fps=None, ctx=None):
10267 """Return a floating-point value of value `val`
and sort `fps`.
10268 If `ctx=
None`, then the
global context
is used.
10273 >>> print(
"0x%.8x" % v.exponent_as_long(
False))
10288 ctx = _get_ctx(ctx)
10289 if is_fp_sort(exp):
10293 fps = _dflt_fps(ctx)
10294 _z3_assert(is_fp_sort(fps), "sort mismatch")
10297 val = _to_float_str(sig)
10298 if val == "NaN" or val == "nan":
10300 elif val == "-0.0":
10301 return fpMinusZero(fps)
10302 elif val == "0.0" or val == "+0.0":
10303 return fpPlusZero(fps)
10304 elif val == "+oo" or val == "+inf" or val == "+Inf":
10305 return fpPlusInfinity(fps)
10306 elif val == "-oo" or val == "-inf" or val == "-Inf":
10307 return fpMinusInfinity(fps)
10309 return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
10312 def FP(name, fpsort, ctx=None):
10313 """Return a floating-point constant named `name`.
10314 `fpsort`
is the floating-point sort.
10315 If `ctx=
None`, then the
global context
is used.
10324 >>> word =
FPSort(8, 24)
10325 >>> x2 =
FP(
'x', word)
10329 if isinstance(fpsort, FPSortRef) and ctx is None:
10332 ctx = _get_ctx(ctx)
10333 return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
10336 def FPs(names, fpsort, ctx=None):
10337 """Return an array of floating-point constants.
10339 >>> x, y, z =
FPs(
'x y z',
FPSort(8, 24))
10349 ctx = _get_ctx(ctx)
10350 if isinstance(names, str):
10351 names = names.split(" ")
10352 return [FP(name, fpsort, ctx) for name in names]
10355 def fpAbs(a, ctx=None):
10356 """Create a Z3 floating-point absolute value expression.
10360 >>> x =
FPVal(1.0, s)
10363 >>> y =
FPVal(-20.0, s)
10367 fpAbs(-1.25*(2**4))
10368 >>>
fpAbs(-1.25*(2**4))
10369 fpAbs(-1.25*(2**4))
10370 >>>
fpAbs(x).sort()
10373 ctx = _get_ctx(ctx)
10374 [a] = _coerce_fp_expr_list([a], ctx)
10375 return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
10378 def fpNeg(a, ctx=None):
10379 """Create a Z3 floating-point addition expression.
10386 >>>
fpNeg(x).sort()
10389 ctx = _get_ctx(ctx)
10390 [a] = _coerce_fp_expr_list([a], ctx)
10391 return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
10394 def _mk_fp_unary(f, rm, a, ctx):
10395 ctx = _get_ctx(ctx)
10396 [a] = _coerce_fp_expr_list([a], ctx)
10398 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10399 _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression")
10400 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx)
10403 def _mk_fp_unary_pred(f, a, ctx):
10404 ctx = _get_ctx(ctx)
10405 [a] = _coerce_fp_expr_list([a], ctx)
10407 _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression")
10408 return BoolRef(f(ctx.ref(), a.as_ast()), ctx)
10411 def _mk_fp_bin(f, rm, a, b, ctx):
10412 ctx = _get_ctx(ctx)
10413 [a, b] = _coerce_fp_expr_list([a, b], ctx)
10415 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10416 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
10417 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx)
10420 def _mk_fp_bin_norm(f, a, b, ctx):
10421 ctx = _get_ctx(ctx)
10422 [a, b] = _coerce_fp_expr_list([a, b], ctx)
10424 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression")
10425 return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
10428 def _mk_fp_bin_pred(f, a, b, ctx):
10429 ctx = _get_ctx(ctx)
10430 [a, b] = _coerce_fp_expr_list([a, b], ctx)
10432 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression")
10433 return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
10436 def _mk_fp_tern(f, rm, a, b, c, ctx):
10437 ctx = _get_ctx(ctx)
10438 [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx)
10440 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10441 _z3_assert(is_fp(a) or is_fp(b) or is_fp(
10442 c), "Second, third or fourth argument must be a Z3 floating-point expression")
10443 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
10446 def fpAdd(rm, a, b, ctx=None):
10447 """Create a Z3 floating-point addition expression.
10453 >>>
fpAdd(rm, x, y)
10457 >>>
fpAdd(rm, x, y).sort()
10460 return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
10463 def fpSub(rm, a, b, ctx=None):
10464 """Create a Z3 floating-point subtraction expression.
10470 >>>
fpSub(rm, x, y)
10472 >>>
fpSub(rm, x, y).sort()
10475 return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
10478 def fpMul(rm, a, b, ctx=None):
10479 """Create a Z3 floating-point multiplication expression.
10485 >>>
fpMul(rm, x, y)
10487 >>>
fpMul(rm, x, y).sort()
10490 return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
10493 def fpDiv(rm, a, b, ctx=None):
10494 """Create a Z3 floating-point division expression.
10500 >>>
fpDiv(rm, x, y)
10502 >>>
fpDiv(rm, x, y).sort()
10505 return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
10508 def fpRem(a, b, ctx=None):
10509 """Create a Z3 floating-point remainder expression.
10516 >>>
fpRem(x, y).sort()
10519 return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
10522 def fpMin(a, b, ctx=None):
10523 """Create a Z3 floating-point minimum expression.
10531 >>>
fpMin(x, y).sort()
10534 return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
10537 def fpMax(a, b, ctx=None):
10538 """Create a Z3 floating-point maximum expression.
10546 >>>
fpMax(x, y).sort()
10549 return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
10552 def fpFMA(rm, a, b, c, ctx=None):
10553 """Create a Z3 floating-point fused multiply-add expression.
10555 return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
10558 def fpSqrt(rm, a, ctx=None):
10559 """Create a Z3 floating-point square root expression.
10561 return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
10564 def fpRoundToIntegral(rm, a, ctx=None):
10565 """Create a Z3 floating-point roundToIntegral expression.
10567 return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
10570 def fpIsNaN(a, ctx=None):
10571 """Create a Z3 floating-point isNaN expression.
10579 return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
10582 def fpIsInf(a, ctx=None):
10583 """Create a Z3 floating-point isInfinite expression.
10590 return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
10593 def fpIsZero(a, ctx=None):
10594 """Create a Z3 floating-point isZero expression.
10596 return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
10599 def fpIsNormal(a, ctx=None):
10600 """Create a Z3 floating-point isNormal expression.
10602 return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
10605 def fpIsSubnormal(a, ctx=None):
10606 """Create a Z3 floating-point isSubnormal expression.
10608 return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
10611 def fpIsNegative(a, ctx=None):
10612 """Create a Z3 floating-point isNegative expression.
10614 return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
10617 def fpIsPositive(a, ctx=None):
10618 """Create a Z3 floating-point isPositive expression.
10620 return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
10623 def _check_fp_args(a, b):
10625 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression")
10628 def fpLT(a, b, ctx=None):
10629 """Create the Z3 floating-point expression `other < self`.
10634 >>> (x < y).sexpr()
10637 return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
10640 def fpLEQ(a, b, ctx=None):
10641 """Create the Z3 floating-point expression `other <= self`.
10646 >>> (x <= y).sexpr()
10649 return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
10652 def fpGT(a, b, ctx=None):
10653 """Create the Z3 floating-point expression `other > self`.
10658 >>> (x > y).sexpr()
10661 return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
10664 def fpGEQ(a, b, ctx=None):
10665 """Create the Z3 floating-point expression `other >= self`.
10670 >>> (x >= y).sexpr()
10673 return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
10676 def fpEQ(a, b, ctx=None):
10677 """Create the Z3 floating-point expression `
fpEQ(other, self)`.
10682 >>>
fpEQ(x, y).sexpr()
10685 return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
10688 def fpNEQ(a, b, ctx=None):
10689 """Create the Z3 floating-point expression `
Not(
fpEQ(other, self))`.
10694 >>> (x != y).sexpr()
10697 return Not(fpEQ(a, b, ctx))
10700 def fpFP(sgn, exp, sig, ctx=None):
10701 """Create the Z3 floating-point value `
fpFP(sgn, sig, exp)`
from the three bit-vectors sgn, sig,
and exp.
10706 fpFP(1, 127, 4194304)
10707 >>> xv =
FPVal(-1.5, s)
10711 >>> slvr.add(
fpEQ(x, xv))
10714 >>> xv =
FPVal(+1.5, s)
10718 >>> slvr.add(
fpEQ(x, xv))
10722 _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
10723 _z3_assert(sgn.sort().size() == 1, "sort mismatch")
10724 ctx = _get_ctx(ctx)
10725 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
10726 return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
10729 def fpToFP(a1, a2=None, a3=None, ctx=None):
10730 """Create a Z3 floating-point conversion expression
from other term sorts
10733 From a bit-vector term
in IEEE 754-2008 format:
10739 From a floating-point term with different precision:
10750 From a signed bit-vector term:
10755 ctx = _get_ctx(ctx)
10756 if is_bv(a1) and is_fp_sort(a2):
10757 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
10758 elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
10759 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10760 elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
10761 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10762 elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
10763 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10765 raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
10768 def fpBVToFP(v, sort, ctx=None):
10769 """Create a Z3 floating-point conversion expression that represents the
10770 conversion
from a bit-vector term to a floating-point term.
10779 _z3_assert(is_bv(v), "First argument must be a Z3 bit-vector expression")
10780 _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
10781 ctx = _get_ctx(ctx)
10782 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
10785 def fpFPToFP(rm, v, sort, ctx=None):
10786 """Create a Z3 floating-point conversion expression that represents the
10787 conversion
from a floating-point term to a floating-point term of different precision.
10798 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10799 _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
10800 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10801 ctx = _get_ctx(ctx)
10802 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10805 def fpRealToFP(rm, v, sort, ctx=None):
10806 """Create a Z3 floating-point conversion expression that represents the
10807 conversion
from a real term to a floating-point term.
10816 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10817 _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
10818 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10819 ctx = _get_ctx(ctx)
10820 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10823 def fpSignedToFP(rm, v, sort, ctx=None):
10824 """Create a Z3 floating-point conversion expression that represents the
10825 conversion
from a signed bit-vector term (encoding an integer) to a floating-point term.
10834 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10835 _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10836 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10837 ctx = _get_ctx(ctx)
10838 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10841 def fpUnsignedToFP(rm, v, sort, ctx=None):
10842 """Create a Z3 floating-point conversion expression that represents the
10843 conversion
from an unsigned bit-vector term (encoding an integer) to a floating-point term.
10852 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10853 _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10854 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10855 ctx = _get_ctx(ctx)
10856 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10859 def fpToFPUnsigned(rm, x, s, ctx=None):
10860 """Create a Z3 floating-point conversion expression,
from unsigned bit-vector to floating-point expression.
"""
10862 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10863 _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
10864 _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
10865 ctx = _get_ctx(ctx)
10866 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
10869 def fpToSBV(rm, x, s, ctx=None):
10870 """Create a Z3 floating-point conversion expression,
from floating-point expression to signed bit-vector.
10874 >>> print(
is_fp(x))
10876 >>> print(
is_bv(y))
10878 >>> print(
is_fp(y))
10880 >>> print(
is_bv(x))
10884 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10885 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10886 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10887 ctx = _get_ctx(ctx)
10888 return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10891 def fpToUBV(rm, x, s, ctx=None):
10892 """Create a Z3 floating-point conversion expression,
from floating-point expression to unsigned bit-vector.
10896 >>> print(
is_fp(x))
10898 >>> print(
is_bv(y))
10900 >>> print(
is_fp(y))
10902 >>> print(
is_bv(x))
10906 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10907 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10908 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10909 ctx = _get_ctx(ctx)
10910 return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10913 def fpToReal(x, ctx=None):
10914 """Create a Z3 floating-point conversion expression,
from floating-point expression to real.
10918 >>> print(
is_fp(x))
10922 >>> print(
is_fp(y))
10928 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10929 ctx = _get_ctx(ctx)
10930 return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
10933 def fpToIEEEBV(x, ctx=None):
10934 """\brief Conversion of a floating-point term into a bit-vector term
in IEEE 754-2008 format.
10936 The size of the resulting bit-vector
is automatically determined.
10938 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
10939 knows only one NaN
and it will always produce the same bit-vector representation of
10944 >>> print(
is_fp(x))
10946 >>> print(
is_bv(y))
10948 >>> print(
is_fp(y))
10950 >>> print(
is_bv(x))
10954 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10955 ctx = _get_ctx(ctx)
10956 return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
10959 #########################################
10961 # Strings, Sequences and Regular expressions
10963 #########################################
10965 class SeqSortRef(SortRef):
10966 """Sequence sort.
"""
10968 def is_string(self):
10969 """Determine
if sort
is a string
10977 return Z3_is_string_sort(self.ctx_ref(), self.ast)
10980 return _to_sort_ref(Z3_get_seq_sort_basis(self.ctx_ref(), self.ast), self.ctx)
10982 class CharSortRef(SortRef):
10983 """Character sort.
"""
10986 def StringSort(ctx=None):
10987 """Create a string sort
10992 ctx = _get_ctx(ctx)
10993 return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx)
10995 def CharSort(ctx=None):
10996 """Create a character sort
11001 ctx = _get_ctx(ctx)
11002 return CharSortRef(Z3_mk_char_sort(ctx.ref()), ctx)
11006 """Create a sequence sort over elements provided
in the argument
11011 return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx)
11014 class SeqRef(ExprRef):
11015 """Sequence expression.
"""
11018 return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
11020 def __add__(self, other):
11021 return Concat(self, other)
11023 def __radd__(self, other):
11024 return Concat(other, self)
11026 def __getitem__(self, i):
11028 i = IntVal(i, self.ctx)
11029 return _to_expr_ref(Z3_mk_seq_nth(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
11033 i = IntVal(i, self.ctx)
11034 return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
11036 def is_string(self):
11037 return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast()))
11039 def is_string_value(self):
11040 return Z3_is_string(self.ctx_ref(), self.as_ast())
11042 def as_string(self):
11043 """Return a string representation of sequence expression.
"""
11044 if self.is_string_value():
11045 string_length = ctypes.c_uint()
11046 chars = Z3_get_lstring(self.ctx_ref(), self.as_ast(), byref(string_length))
11047 return string_at(chars, size=string_length.value).decode("latin-1")
11048 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
11050 def py_value(self):
11051 return self.as_string()
11053 def __le__(self, other):
11054 return _to_expr_ref(Z3_mk_str_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
11056 def __lt__(self, other):
11057 return _to_expr_ref(Z3_mk_str_lt(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
11059 def __ge__(self, other):
11060 return _to_expr_ref(Z3_mk_str_le(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
11062 def __gt__(self, other):
11063 return _to_expr_ref(Z3_mk_str_lt(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
11066 def _coerce_char(ch, ctx=None):
11067 if isinstance(ch, str):
11068 ctx = _get_ctx(ctx)
11069 ch = CharVal(ch, ctx)
11070 if not is_expr(ch):
11071 raise Z3Exception("Character expression expected")
11074 class CharRef(ExprRef):
11075 """Character expression.
"""
11077 def __le__(self, other):
11078 other = _coerce_char(other, self.ctx)
11079 return _to_expr_ref(Z3_mk_char_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
11082 return _to_expr_ref(Z3_mk_char_to_int(self.ctx_ref(), self.as_ast()), self.ctx)
11085 return _to_expr_ref(Z3_mk_char_to_bv(self.ctx_ref(), self.as_ast()), self.ctx)
11087 def is_digit(self):
11088 return _to_expr_ref(Z3_mk_char_is_digit(self.ctx_ref(), self.as_ast()), self.ctx)
11091 def CharVal(ch, ctx=None):
11092 ctx = _get_ctx(ctx)
11093 if isinstance(ch, str):
11095 if not isinstance(ch, int):
11096 raise Z3Exception("character value should be an ordinal")
11097 return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx)
11099 def CharFromBv(bv):
11100 if not is_expr(bv):
11101 raise Z3Exception("Bit-vector expression needed")
11102 return _to_expr_ref(Z3_mk_char_from_bv(bv.ctx_ref(), bv.as_ast()), bv.ctx)
11104 def CharToBv(ch, ctx=None):
11105 ch = _coerce_char(ch, ctx)
11108 def CharToInt(ch, ctx=None):
11109 ch = _coerce_char(ch, ctx)
11112 def CharIsDigit(ch, ctx=None):
11113 ch = _coerce_char(ch, ctx)
11114 return ch.is_digit()
11116 def _coerce_seq(s, ctx=None):
11117 if isinstance(s, str):
11118 ctx = _get_ctx(ctx)
11119 s = StringVal(s, ctx)
11121 raise Z3Exception("Non-expression passed as a sequence")
11123 raise Z3Exception("Non-sequence passed as a sequence")
11127 def _get_ctx2(a, b, ctx=None):
11138 """Return `
True`
if `a`
is a Z3 sequence expression.
11144 return isinstance(a, SeqRef)
11147 def is_string(a: Any) -> bool:
11148 """Return `
True`
if `a`
is a Z3 string expression.
11152 return isinstance(a, SeqRef) and a.is_string()
11155 def is_string_value(a: Any) -> bool:
11156 """return 'True' if 'a' is a Z3 string constant expression.
11162 return isinstance(a, SeqRef) and a.is_string_value()
11164 def StringVal(s, ctx=None):
11165 """create a string expression
"""
11166 s = "".join(str(ch) if 32 <= ord(ch) and ord(ch) < 127 else "\\u{%x}" % (ord(ch)) for ch in s)
11167 ctx = _get_ctx(ctx)
11168 return SeqRef(Z3_mk_string(ctx.ref(), s), ctx)
11171 def String(name, ctx=None):
11172 """Return a string constant named `name`. If `ctx=
None`, then the
global context
is used.
11176 ctx = _get_ctx(ctx)
11177 return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx)
11180 def Strings(names, ctx=None):
11181 """Return a tuple of String constants.
"""
11182 ctx = _get_ctx(ctx)
11183 if isinstance(names, str):
11184 names = names.split(" ")
11185 return [String(name, ctx) for name in names]
11188 def SubString(s, offset, length):
11189 """Extract substring
or subsequence starting at offset
"""
11190 return Extract(s, offset, length)
11193 def SubSeq(s, offset, length):
11194 """Extract substring
or subsequence starting at offset
"""
11195 return Extract(s, offset, length)
11199 """Create the empty sequence of the given sort
11202 >>> print(e.eq(e2))
11211 if isinstance(s, SeqSortRef):
11212 return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
11213 if isinstance(s, ReSortRef):
11214 return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
11215 raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
11219 """Create the regular expression that accepts the universal language
11227 if isinstance(s, ReSortRef):
11228 return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
11229 raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
11234 """Create a singleton sequence
"""
11235 return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx)
11238 def PrefixOf(a, b):
11239 """Check
if 'a' is a prefix of
'b'
11247 ctx = _get_ctx2(a, b)
11248 a = _coerce_seq(a, ctx)
11249 b = _coerce_seq(b, ctx)
11250 return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
11253 def SuffixOf(a, b):
11254 """Check
if 'a' is a suffix of
'b'
11262 ctx = _get_ctx2(a, b)
11263 a = _coerce_seq(a, ctx)
11264 b = _coerce_seq(b, ctx)
11265 return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
11268 def Contains(a, b):
11269 """Check
if 'a' contains
'b'
11276 >>> x, y, z =
Strings(
'x y z')
11281 ctx = _get_ctx2(a, b)
11282 a = _coerce_seq(a, ctx)
11283 b = _coerce_seq(b, ctx)
11284 return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
11287 def Replace(s, src, dst):
11288 """Replace the first occurrence of
'src' by
'dst' in 's'
11289 >>> r =
Replace(
"aaa",
"a",
"b")
11293 ctx = _get_ctx2(dst, s)
11294 if ctx is None and is_expr(src):
11296 src = _coerce_seq(src, ctx)
11297 dst = _coerce_seq(dst, ctx)
11298 s = _coerce_seq(s, ctx)
11299 return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx)
11302 def IndexOf(s, substr, offset=None):
11303 """Retrieve the index of substring within a string starting at a specified offset.
11312 if is_expr(offset):
11314 ctx = _get_ctx2(s, substr, ctx)
11315 s = _coerce_seq(s, ctx)
11316 substr = _coerce_seq(substr, ctx)
11317 if _is_int(offset):
11318 offset = IntVal(offset, ctx)
11319 return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
11322 def LastIndexOf(s, substr):
11323 """Retrieve the last index of substring within a string
"""
11325 ctx = _get_ctx2(s, substr, ctx)
11326 s = _coerce_seq(s, ctx)
11327 substr = _coerce_seq(substr, ctx)
11328 return ArithRef(Z3_mk_seq_last_index(s.ctx_ref(), s.as_ast(), substr.as_ast()), s.ctx)
11332 """Obtain the length of a sequence
's'
11338 return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
11341 """Map function
'f' over sequence
's'"""
11342 ctx = _get_ctx2(f, s)
11343 s = _coerce_seq(s, ctx)
11344 return _to_expr_ref(Z3_mk_seq_map(s.ctx_ref(), f.as_ast(), s.as_ast()), ctx)
11346 def SeqMapI(f, i, s):
11347 """Map function
'f' over sequence
's' at index
'i'"""
11348 ctx = _get_ctx2(f, s)
11349 s = _coerce_seq(s, ctx)
11352 return _to_expr_ref(Z3_mk_seq_mapi(s.ctx_ref(), f.as_ast(), i.as_ast(), s.as_ast()), ctx)
11354 def SeqFoldLeft(f, a, s):
11355 ctx = _get_ctx2(f, s)
11356 s = _coerce_seq(s, ctx)
11358 return _to_expr_ref(Z3_mk_seq_foldl(s.ctx_ref(), f.as_ast(), a.as_ast(), s.as_ast()), ctx)
11360 def SeqFoldLeftI(f, i, a, s):
11361 ctx = _get_ctx2(f, s)
11362 s = _coerce_seq(s, ctx)
11365 return _to_expr_ref(Z3_mk_seq_foldli(s.ctx_ref(), f.as_ast(), i.as_ast(), a.as_ast(), s.as_ast()), ctx)
11368 """Convert string expression to integer
11380 return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx)
11384 """Convert integer expression to string
"""
11387 return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
11391 """Convert a unit length string to integer code
"""
11394 return ArithRef(Z3_mk_string_to_code(s.ctx_ref(), s.as_ast()), s.ctx)
11396 def StrFromCode(c):
11397 """Convert code to a string
"""
11400 return SeqRef(Z3_mk_string_from_code(c.ctx_ref(), c.as_ast()), c.ctx)
11402 def Re(s, ctx=None):
11403 """The regular expression that accepts sequence
's'
11408 s = _coerce_seq(s, ctx)
11409 return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx)
11412 # Regular expressions
11414 class ReSortRef(SortRef):
11415 """Regular expression sort.
"""
11418 return _to_sort_ref(Z3_get_re_sort_basis(self.ctx_ref(), self.ast), self.ctx)
11423 return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx)
11424 if s is None or isinstance(s, Context):
11426 return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), s.ctx)
11427 raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument")
11430 class ReRef(ExprRef):
11431 """Regular expressions.
"""
11433 def __add__(self, other):
11434 return Union(self, other)
11438 return isinstance(s, ReRef)
11442 """Create regular expression membership test
11451 s = _coerce_seq(s, re.ctx)
11452 return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
11456 """Create union of regular expressions.
11461 args = _get_args(args)
11464 _z3_assert(sz > 0, "At least one argument expected.")
11465 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
11470 for i in range(sz):
11471 v[i] = args[i].as_ast()
11472 return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx)
11475 def Intersect(*args):
11476 """Create intersection of regular expressions.
11479 args = _get_args(args)
11482 _z3_assert(sz > 0, "At least one argument expected.")
11483 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
11488 for i in range(sz):
11489 v[i] = args[i].as_ast()
11490 return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)
11494 """Create the regular expression accepting one
or more repetitions of argument.
11504 _z3_assert(is_expr(re), "expression expected")
11505 return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)
11509 """Create the regular expression that optionally accepts the argument.
11519 _z3_assert(is_expr(re), "expression expected")
11520 return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)
11523 def Complement(re):
11524 """Create the complement regular expression.
"""
11525 return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
11529 """Create the regular expression accepting zero
or more repetitions of argument.
11539 _z3_assert(is_expr(re), "expression expected")
11540 return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)
11543 def Loop(re, lo, hi=0):
11544 """Create the regular expression accepting between a lower
and upper bound repetitions
11545 >>> re =
Loop(
Re(
"a"), 1, 3)
11554 _z3_assert(is_expr(re), "expression expected")
11555 return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)
11558 def Range(lo, hi, ctx=None):
11559 """Create the range regular expression over two sequences of length 1
11560 >>> range =
Range(
"a",
"z")
11566 lo = _coerce_seq(lo, ctx)
11567 hi = _coerce_seq(hi, ctx)
11569 _z3_assert(is_expr(lo), "expression expected")
11570 _z3_assert(is_expr(hi), "expression expected")
11571 return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)
11573 def Diff(a, b, ctx=None):
11574 """Create the difference regular expression
11577 _z3_assert(is_expr(a), "expression expected")
11578 _z3_assert(is_expr(b), "expression expected")
11579 return ReRef(Z3_mk_re_diff(a.ctx_ref(), a.ast, b.ast), a.ctx)
11581 def AllChar(regex_sort, ctx=None):
11582 """Create a regular expression that accepts all single character strings
11584 return ReRef(Z3_mk_re_allchar(regex_sort.ctx_ref(), regex_sort.ast), regex_sort.ctx)
11586 # Special Relations
11589 def PartialOrder(a, index):
11590 return FuncDeclRef(Z3_mk_partial_order(a.ctx_ref(), a.ast, index), a.ctx)
11593 def LinearOrder(a, index):
11594 return FuncDeclRef(Z3_mk_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
11597 def TreeOrder(a, index):
11598 return FuncDeclRef(Z3_mk_tree_order(a.ctx_ref(), a.ast, index), a.ctx)
11601 def PiecewiseLinearOrder(a, index):
11602 return FuncDeclRef(Z3_mk_piecewise_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
11605 def TransitiveClosure(f):
11606 """Given a binary relation R, such that the two arguments have the same sort
11607 create the transitive closure relation R+.
11608 The transitive closure R+
is a new relation.
11610 return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.ctx)
11614 super(ctypes.c_void_p, ast).__init__(ptr)
11617 def to_ContextObj(ptr,):
11618 ctx = ContextObj(ptr)
11619 super(ctypes.c_void_p, ctx).__init__(ptr)
11622 def to_AstVectorObj(ptr,):
11623 v = AstVectorObj(ptr)
11624 super(ctypes.c_void_p, v).__init__(ptr)
11627 # NB. my-hacky-class only works for a single instance of OnClause
11628 # it should be replaced with a proper correlation between OnClause
11629 # and object references that can be passed over the FFI.
11630 # for UserPropagator we use a global dictionary, which isn't great code.
11632 _my_hacky_class = None
11633 def on_clause_eh(ctx, p, n, dep, clause):
11634 onc = _my_hacky_class
11635 p = _to_expr_ref(to_Ast(p), onc.ctx)
11636 clause = AstVector(to_AstVectorObj(clause), onc.ctx)
11637 deps = [dep[i] for i in range(n)]
11638 onc.on_clause(p, deps, clause)
11640 _on_clause_eh = Z3_on_clause_eh(on_clause_eh)
11643 def __init__(self, s, on_clause):
11646 self.on_clause = on_clause
11648 global _my_hacky_class
11649 _my_hacky_class = self
11650 Z3_solver_register_on_clause(self.ctx.ref(), self.s.solver, self.idx, _on_clause_eh)
11653 class PropClosures:
11654 def __init__(self):
11658 def set_threaded(self):
11659 if self.lock is None:
11661 self.lock = threading.Lock()
11663 def get(self, ctx):
11666 r = self.bases[ctx]
11668 r = self.bases[ctx]
11671 def set(self, ctx, r):
11674 self.bases[ctx] = r
11676 self.bases[ctx] = r
11678 def insert(self, r):
11681 id = len(self.bases) + 3
11684 id = len(self.bases) + 3
11689 _prop_closures = None
11692 def ensure_prop_closures():
11693 global _prop_closures
11694 if _prop_closures is None:
11695 _prop_closures = PropClosures()
11698 def user_prop_push(ctx, cb):
11699 prop = _prop_closures.get(ctx)
11704 def user_prop_pop(ctx, cb, num_scopes):
11705 prop = _prop_closures.get(ctx)
11707 prop.pop(num_scopes)
11710 def user_prop_fresh(ctx, _new_ctx):
11711 _prop_closures.set_threaded()
11712 prop = _prop_closures.get(ctx)
11714 Z3_del_context(nctx.ctx)
11715 new_ctx = to_ContextObj(_new_ctx)
11717 nctx.eh = Z3_set_error_handler(new_ctx, z3_error_handler)
11719 new_prop = prop.fresh(nctx)
11720 _prop_closures.set(new_prop.id, new_prop)
11724 def user_prop_fixed(ctx, cb, id, value):
11725 prop = _prop_closures.get(ctx)
11728 id = _to_expr_ref(to_Ast(id), prop.ctx())
11729 value = _to_expr_ref(to_Ast(value), prop.ctx())
11730 prop.fixed(id, value)
11733 def user_prop_created(ctx, cb, id):
11734 prop = _prop_closures.get(ctx)
11737 id = _to_expr_ref(to_Ast(id), prop.ctx())
11742 def user_prop_final(ctx, cb):
11743 prop = _prop_closures.get(ctx)
11749 def user_prop_eq(ctx, cb, x, y):
11750 prop = _prop_closures.get(ctx)
11753 x = _to_expr_ref(to_Ast(x), prop.ctx())
11754 y = _to_expr_ref(to_Ast(y), prop.ctx())
11758 def user_prop_diseq(ctx, cb, x, y):
11759 prop = _prop_closures.get(ctx)
11762 x = _to_expr_ref(to_Ast(x), prop.ctx())
11763 y = _to_expr_ref(to_Ast(y), prop.ctx())
11767 def user_prop_decide(ctx, cb, t_ref, idx, phase):
11768 prop = _prop_closures.get(ctx)
11771 t = _to_expr_ref(to_Ast(t_ref), prop.ctx())
11772 prop.decide(t, idx, phase)
11776 _user_prop_push = Z3_push_eh(user_prop_push)
11777 _user_prop_pop = Z3_pop_eh(user_prop_pop)
11778 _user_prop_fresh = Z3_fresh_eh(user_prop_fresh)
11779 _user_prop_fixed = Z3_fixed_eh(user_prop_fixed)
11780 _user_prop_created = Z3_created_eh(user_prop_created)
11781 _user_prop_final = Z3_final_eh(user_prop_final)
11782 _user_prop_eq = Z3_eq_eh(user_prop_eq)
11783 _user_prop_diseq = Z3_eq_eh(user_prop_diseq)
11784 _user_prop_decide = Z3_decide_eh(user_prop_decide)
11787 def PropagateFunction(name, *sig):
11788 """Create a function that gets tracked by user propagator.
11789 Every term headed by this function symbol
is tracked.
11790 If a term
is fixed
and the fixed callback
is registered a
11791 callback
is invoked that the term headed by this function
is fixed.
11793 sig = _get_args(sig)
11795 _z3_assert(len(sig) > 0, "At least two arguments expected")
11796 arity = len(sig) - 1
11799 _z3_assert(is_sort(rng), "Z3 sort expected")
11800 dom = (Sort * arity)()
11801 for i in range(arity):
11803 _z3_assert(is_sort(sig[i]), "Z3 sort expected")
11804 dom[i] = sig[i].ast
11806 return FuncDeclRef(Z3_solver_propagate_declare(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
11810 class UserPropagateBase:
11813 # Either solver is set or ctx is set.
11814 # Propagators that are created through callbacks
11815 # to "fresh" inherit the context of that is supplied
11816 # as argument to the callback.
11817 # This context should not be deleted. It is owned by the solver.
11819 def __init__(self, s, ctx=None):
11820 assert s is None or ctx is None
11821 ensure_prop_closures()
11824 self.fresh_ctx = None
11826 self.id = _prop_closures.insert(self)
11832 self.created = None
11834 self.fresh_ctx = ctx
11836 Z3_solver_propagate_init(self.ctx_ref(),
11838 ctypes.c_void_p(self.id),
11845 self._ctx.ctx = None
11849 return self.fresh_ctx
11851 return self.solver.ctx
11854 return self.ctx().ref()
11856 def add_fixed(self, fixed):
11857 assert not self.fixed
11858 assert not self._ctx
11860 Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
11863 def add_created(self, created):
11864 assert not self.created
11865 assert not self._ctx
11867 Z3_solver_propagate_created(self.ctx_ref(), self.solver.solver, _user_prop_created)
11868 self.created = created
11870 def add_final(self, final):
11871 assert not self.final
11872 assert not self._ctx
11874 Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final)
11877 def add_eq(self, eq):
11879 assert not self._ctx
11881 Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq)
11884 def add_diseq(self, diseq):
11885 assert not self.diseq
11886 assert not self._ctx
11888 Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq)
11891 def add_decide(self, decide):
11892 assert not self.decide
11893 assert not self._ctx
11895 Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide)
11896 self.decide = decide
11899 raise Z3Exception("push needs to be overwritten")
11901 def pop(self, num_scopes):
11902 raise Z3Exception("pop needs to be overwritten")
11904 def fresh(self, new_ctx):
11905 raise Z3Exception("fresh needs to be overwritten")
11908 assert not self._ctx
11910 Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
11912 Z3_solver_propagate_register_cb(self.ctx_ref(), ctypes.c_void_p(self.cb), e.ast)
11915 # Tell the solver to perform the next split on a given term
11916 # If the term is a bit-vector the index idx specifies the index of the Boolean variable being
11917 # split on. A phase of true = 1/false = -1/undef = 0 = let solver decide is the last argument.
11919 def next_split(self, t, idx, phase):
11920 return Z3_solver_next_split(self.ctx_ref(), ctypes.c_void_p(self.cb), t.ast, idx, phase)
11923 # Propagation can only be invoked as during a fixed or final callback.
11925 def propagate(self, e, ids, eqs=[]):
11926 _ids, num_fixed = _to_ast_array(ids)
11928 _lhs, _num_lhs = _to_ast_array([x for x, y in eqs])
11929 _rhs, _num_rhs = _to_ast_array([y for x, y in eqs])
11930 return Z3_solver_propagate_consequence(e.ctx.ref(), ctypes.c_void_p(
11931 self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
11933 def conflict(self, deps = [], eqs = []):
11934 self.propagate(BoolVal(False, self.ctx()), deps, eqs)
Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o)
Return the parameter description set for the given optimize object.
Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i)
Return the name of the i probe.
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)
Return objectives on the optimization context. If the objective function is a max-sat objective it is...
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
def simplify(a, arguments, keywords)
Utils.
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form: ...
def update_rule(self, head, body, name)
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
def get_cover_delta(self, level, predicate)
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a variable.
def upper_values(self, obj)
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
def __getitem__(self, idx)
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
void Z3_API Z3_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)
Decrement the reference counter of the given simplifier.
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
expr range(expr const &lo, expr const &hi)
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context...
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
def substitute_vars(t, m)
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2)
Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1...
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
def declare(self, name, args)
def assert_exprs(self, args)
def set_option(args, kws)
Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t)
Return the parameter description set for the given simplifier object.
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t *r)
Store the size of the sort in r. Return false if the call failed. That is, Z3_get_sort_kind(s) == Z3_...
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
def assert_exprs(self, args)
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)
Return the name of the idx tactic.
def lower_values(self, obj)
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f)
Convert a Z3_func_decl into Z3_ast. This is just type casting.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t)
Return a string containing a description of parameters accepted by the given simplifier.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
def register_relation(self, relations)
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size)
Create a named finite domain sort.
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
void Z3_API Z3_parser_context_dec_ref(Z3_context c, Z3_parser_context pc)
Decrement the reference counter of the given Z3_parser_context object.
bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
Assert a constraint to the fixedpoint context.
void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f)
Add a function declaration.
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p)
Apply tactic t to the goal g using the parameter set p.
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
def is_finite_domain_sort(s)
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.
def z3_error_handler(c, e)
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
Assert tracked hard constraint to the optimization context.
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
def get_rule_names_along_trace(self)
def simplify_param_descrs()
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p)
Return a simplifier that applies t using the given set of parameters.
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
def convert_model(self, model)
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the variables in a with the expressions in to. For every i smaller than num_exprs...
def __init__(self, args, kws)
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective.
void Z3_API Z3_optimize_register_model_eh(Z3_context c, Z3_optimize o, Z3_model m, void *ctx, Z3_model_eh model_eh)
register a model event handler for new models.
void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s)
Add a sort declaration.
def using_params(self, args, keys)
double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a)
Return a hash code for the given AST. The hash code is structural but two different AST objects can m...
def Extract(high, low, a)
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
def solve_using(s, args, keywords)
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context...
def set_predicate_representation(self, f, representations)
Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string s)
Parse a string of SMTLIB2 commands. Return assertions.
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1...
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query. ...
def RecFunction(name, sig)
Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s)
Convert a Z3_sort into Z3_ast. This is just type casting.
def set_initial_value(self, var, value)
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
void Z3_API Z3_enable_trace(Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
Strings, Sequences and Regular expressions.
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
def apply(self, goal, arguments, keywords)
def solve(args, keywords)
def __init__(self, opt, value, is_max)
def check(self, assumptions)
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
def __call__(self, goal, arguments, keywords)
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
def prove(claim, show=False, keywords)
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
def is_finite_domain_value(a)
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a decimal string of a numeric constant term.
def get_rules_along_trace(self)
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.
def assert_and_track(self, a, p)
def translate(self, target)
def __radd__(self, other)
def from_file(self, filename)
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
Query the PDR engine for the maximal levels properties are known about predicate. ...
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
def query_from_lvl(self, lvl, query)
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.
Z3_sort Z3_API Z3_mk_type_variable(Z3_context c, Z3_symbol s)
Create a type variable.
Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i)
Return the sort of the i-th parameter of the given function declaration.
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
def to_string(self, queries)
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created. ...
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
def set_on_model(self, on_model)
def parse_string(self, s)
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
def get_ground_sat_answer(self)
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)
Return the set of asserted formulas on the optimization context.
def declare_var(self, vars)
void Z3_API Z3_parser_context_inc_ref(Z3_context c, Z3_parser_context pc)
Increment the reference counter of the given Z3_parser_context object.
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)
Increment the reference counter of the given simplifier.
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
def __rmul__(self, other)
Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c)
Retrieve description of global parameters.
def RecAddDefinition(f, args, body)
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target)
Translate/Copy the AST a from context source to context target. AST a must have been created using co...
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d)
Retrieve a string that describes the last status returned by Z3_optimize_check.
Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier)
Attach simplifier to a solver. The solver will use the simplifier for incremental pre-processing...
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
def get_num_levels(self, predicate)
Z3_string Z3_API Z3_simplify_get_help(Z3_context c)
Return a string describing all available parameters.
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)
Define the body of a recursive function.
def __init__(self, result, ctx)
def set(self, args, keys)
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
def add_cover(self, level, predicate, property)
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
Z3_parser_context Z3_API Z3_mk_parser_context(Z3_context c)
Create a parser context.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective. The returned vector ...
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
void Z3_API Z3_fixedpoint_set_predicate_representation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f, unsigned num_relations, Z3_symbol const relation_kinds[])
Configure the predicate representation.
Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the probe with the given name.
def set(self, args, keys)
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)
Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...
def substitute_funs(t, m)
Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the tactic with the given name.
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
def check(self, assumptions)
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
def __exit__(self, exc_info)
def is_algebraic_value(a)
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast v, Z3_ast val)
provide an initialization hint to the solver. The initialization hint is used to calibrate an initial...
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.
Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])
Substitute functions in from with new expressions in to.
Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name)
Return a simplifier associated with the given name. The complete list of simplifiers may be obtained ...
Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the sort value associated with a sort parameter.
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.