9 """Z3 is a high performance theorem prover developed at Microsoft Research. Z3 is used in many applications such as: software/hardware verification and testing, constraint solving, analysis of hybrid systems, security, biology (in silico analysis), and geometrical problems.
11 Several online tutorials for Z3Py are available at:
12 http://rise4fun.com/Z3Py/tutorial/guide
14 Please send feedback, comments and/or corrections to leonardo@microsoft.com. Your comments are very valuable.
37 ... # the expression x + y is type incorrect
39 ... except Z3Exception as ex:
40 ... print("failed: %s" % ex)
45 from z3consts
import *
46 from z3printer
import *
47 from fractions
import Fraction
53 return isinstance(v, int)
or isinstance(v, long)
56 return isinstance(v, int)
65 major = ctypes.c_uint(0)
66 minor = ctypes.c_uint(0)
67 build = ctypes.c_uint(0)
68 rev = ctypes.c_uint(0)
70 return "%s.%s.%s" % (major.value, minor.value, build.value)
73 major = ctypes.c_uint(0)
74 minor = ctypes.c_uint(0)
75 build = ctypes.c_uint(0)
76 rev = ctypes.c_uint(0)
78 return (major.value, minor.value, build.value, rev.value)
82 def _z3_assert(cond, msg):
84 raise Z3Exception(msg)
87 """Log interaction to a file. This function must be invoked immediately after init(). """
91 """Append user-defined string to interaction log. """
95 """Convert an integer or string into a Z3 symbol."""
96 if isinstance(s, int):
101 def _symbol2py(ctx, s):
102 """Convert a Z3 symbol back into a Python object. """
108 _error_handler_fptr = ctypes.CFUNCTYPE(
None, ctypes.c_void_p, ctypes.c_uint)
114 if len(args) == 1
and (isinstance(args[0], tuple)
or isinstance(args[0], list)):
121 def _Z3python_error_handler_core(c, e):
128 def _to_param_value(val):
129 if isinstance(val, bool):
138 """A Context manages all other Z3 objects, global configuration options, etc.
140 Z3Py uses a default global context. For most applications this is sufficient.
141 An application may use multiple Z3 contexts. Objects created in one context
142 cannot be used in another one. However, several objects may be "translated" from
143 one context to another. It is not safe to access Z3 objects from multiple threads.
144 The only exception is the method `interrupt()` that can be used to interrupt() a long
146 The initialization method receives global configuration options for the new context.
150 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
165 lib().Z3_set_error_handler.restype =
None
166 lib().Z3_set_error_handler.argtypes = [ContextObj, _error_handler_fptr]
171 self.lib.Z3_del_context(self.
ctx)
174 """Return a reference to the actual C pointer to the Z3 context."""
178 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
180 This method can be invoked from a thread different from the one executing the
181 interruptable procedure.
189 """Return a reference to the global Z3 context.
192 >>> x.ctx == main_ctx()
197 >>> x2 = Real('x', c)
204 if _main_ctx ==
None:
215 """Set Z3 global (or module) parameters.
217 >>> set_param(precision=10)
220 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
224 if not set_pp_option(k, v):
238 """Reset all global (or module) parameters.
243 """Alias for 'set_param' for backward compatibility.
248 """Return the value of a Z3 global (or module) parameter
250 >>> get_param('nlsat.reorder')
253 ptr = (ctypes.c_char_p * 1)()
255 r = z3core._to_pystr(ptr[0])
257 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
267 """Superclass for all Z3 objects that have support for pretty printing."""
272 """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions."""
282 return obj_to_string(self)
285 return obj_to_string(self)
288 """Return an string representing the AST node in s-expression notation.
291 >>> ((x + 1)*x).sexpr()
297 """Return a pointer to the corresponding C Z3_ast object."""
301 """Return unique identifier for object. It can be used for hash-tables and maps."""
306 """Return a reference to the C context where this AST node is stored."""
307 return self.ctx.ref()
310 """Return `True` if `self` and `other` are structurally identical.
317 >>> n1 = simplify(n1)
318 >>> n2 = simplify(n2)
323 _z3_assert(
is_ast(other),
"Z3 AST expected")
327 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
333 >>> # Nodes in different contexts can't be mixed.
334 >>> # However, we can translate nodes from one context to another.
335 >>> x.translate(c2) + y
339 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
343 """Return a hashcode for the `self`.
345 >>> n1 = simplify(Int('x') + 1)
346 >>> n2 = simplify(2 + Int('x') - 1)
347 >>> n1.hash() == n2.hash()
353 """Return `True` if `a` is an AST node.
357 >>> is_ast(IntVal(10))
361 >>> is_ast(BoolSort())
363 >>> is_ast(Function('f', IntSort(), IntSort()))
370 return isinstance(a, AstRef)
373 """Return `True` if `a` and `b` are structurally identical AST nodes.
383 >>> eq(simplify(x + 1), simplify(1 + x))
390 def _ast_kind(ctx, a):
395 def _ctx_from_ast_arg_list(args, default_ctx=None):
403 _z3_assert(ctx == a.ctx,
"Context mismatch")
408 def _ctx_from_ast_args(*args):
409 return _ctx_from_ast_arg_list(args)
411 def _to_func_decl_array(args):
413 _args = (FuncDecl * sz)()
415 _args[i] = args[i].as_func_decl()
418 def _to_ast_array(args):
422 _args[i] = args[i].as_ast()
425 def _to_ref_array(ref, args):
429 _args[i] = args[i].as_ast()
432 def _to_ast_ref(a, ctx):
433 k = _ast_kind(ctx, a)
435 return _to_sort_ref(a, ctx)
436 elif k == Z3_FUNC_DECL_AST:
437 return _to_func_decl_ref(a, ctx)
439 return _to_expr_ref(a, ctx)
447 def _sort_kind(ctx, s):
451 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node."""
460 """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
463 >>> b.kind() == Z3_BOOL_SORT
465 >>> b.kind() == Z3_INT_SORT
467 >>> A = ArraySort(IntSort(), IntSort())
468 >>> A.kind() == Z3_ARRAY_SORT
470 >>> A.kind() == Z3_INT_SORT
473 return _sort_kind(self.
ctx, self.
ast)
476 """Return `True` if `self` is a subsort of `other`.
478 >>> IntSort().subsort(RealSort())
484 """Try to cast `val` as an element of sort `self`.
486 This method is used in Z3Py to convert Python objects such as integers,
487 floats, longs and strings into Z3 expressions.
490 >>> RealSort().cast(x)
494 _z3_assert(
is_expr(val),
"Z3 expression expected")
495 _z3_assert(self.
eq(val.sort()),
"Sort mismatch")
499 """Return the name (string) of sort `self`.
501 >>> BoolSort().name()
503 >>> ArraySort(IntSort(), IntSort()).name()
509 """Return `True` if `self` and `other` are the same Z3 sort.
512 >>> p.sort() == BoolSort()
514 >>> p.sort() == IntSort()
522 """Return `True` if `self` and `other` are not the same Z3 sort.
525 >>> p.sort() != BoolSort()
527 >>> p.sort() != IntSort()
533 """Return `True` if `s` is a Z3 sort.
535 >>> is_sort(IntSort())
537 >>> is_sort(Int('x'))
539 >>> is_expr(Int('x'))
542 return isinstance(s, SortRef)
544 def _to_sort_ref(s, ctx):
546 _z3_assert(isinstance(s, Sort),
"Z3 Sort expected")
547 k = _sort_kind(ctx, s)
548 if k == Z3_BOOL_SORT:
550 elif k == Z3_INT_SORT
or k == Z3_REAL_SORT:
552 elif k == Z3_BV_SORT:
554 elif k == Z3_ARRAY_SORT:
556 elif k == Z3_DATATYPE_SORT:
558 elif k == Z3_FLOATING_POINT_SORT:
560 elif k == Z3_ROUNDING_MODE_SORT:
565 return _to_sort_ref(
Z3_get_sort(ctx.ref(), a), ctx)
568 """Create a new uninterpred sort named `name`.
570 If `ctx=None`, then the new sort is declared in the global Z3Py context.
572 >>> A = DeclareSort('A')
573 >>> a = Const('a', A)
574 >>> b = Const('b', A)
592 """Function declaration. Every constant and function have an associated declaration.
594 The declaration assigns a name, a sort (i.e., type), and for function
595 the sort (i.e., type) of each of its arguments. Note that, in Z3,
596 a constant is a function with 0 arguments.
608 """Return the name of the function declaration `self`.
610 >>> f = Function('f', IntSort(), IntSort())
613 >>> isinstance(f.name(), str)
619 """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0.
621 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
628 """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`.
630 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
637 _z3_assert(i < self.
arity(),
"Index out of bounds")
641 """Return the sort of the range of a function declaration. For constants, this is the sort of the constant.
643 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
650 """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
653 >>> d = (x + 1).decl()
654 >>> d.kind() == Z3_OP_ADD
656 >>> d.kind() == Z3_OP_MUL
662 """Create a Z3 application expression using the function `self`, and the given arguments.
664 The arguments must be Z3 expressions. This method assumes that
665 the sorts of the elements in `args` match the sorts of the
666 domain. Limited coersion is supported. For example, if
667 args[0] is a Python integer, and the function expects a Z3
668 integer, then the argument is automatically converted into a
671 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
679 args = _get_args(args)
682 _z3_assert(num == self.
arity(),
"Incorrect number of arguments to %s" % self)
683 _args = (Ast * num)()
688 tmp = self.
domain(i).cast(args[i])
690 _args[i] = tmp.as_ast()
694 """Return `True` if `a` is a Z3 function declaration.
696 >>> f = Function('f', IntSort(), IntSort())
703 return isinstance(a, FuncDeclRef)
706 """Create a new Z3 uninterpreted function with the given sorts.
708 >>> f = Function('f', IntSort(), IntSort())
714 _z3_assert(len(sig) > 0,
"At least two arguments expected")
718 _z3_assert(
is_sort(rng),
"Z3 sort expected")
719 dom = (Sort * arity)()
720 for i
in range(arity):
722 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
727 def _to_func_decl_ref(a, ctx):
737 """Constraints, formulas and terms are expressions in Z3.
739 Expressions are ASTs. Every expression has a sort.
740 There are three main kinds of expressions:
741 function applications, quantifiers and bounded variables.
742 A constant is a function application with 0 arguments.
743 For quantifier free problems, all expressions are
744 function applications.
753 """Return the sort of expression `self`.
765 """Shorthand for `self.sort().kind()`.
767 >>> a = Array('a', IntSort(), IntSort())
768 >>> a.sort_kind() == Z3_ARRAY_SORT
770 >>> a.sort_kind() == Z3_INT_SORT
773 return self.
sort().kind()
776 """Return a Z3 expression that represents the constraint `self == other`.
778 If `other` is `None`, then this method simply returns `False`.
789 a, b = _coerce_exprs(self, other)
793 """Return a Z3 expression that represents the constraint `self != other`.
795 If `other` is `None`, then this method simply returns `True`.
806 a, b = _coerce_exprs(self, other)
807 _args, sz = _to_ast_array((a, b))
811 """Return the Z3 function declaration associated with a Z3 application.
813 >>> f = Function('f', IntSort(), IntSort())
822 _z3_assert(
is_app(self),
"Z3 application expected")
826 """Return the number of arguments of a Z3 application.
830 >>> (a + b).num_args()
832 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
838 _z3_assert(
is_app(self),
"Z3 application expected")
842 """Return argument `idx` of the application `self`.
844 This method assumes that `self` is a function application with at least `idx+1` arguments.
848 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
858 _z3_assert(
is_app(self),
"Z3 application expected")
859 _z3_assert(idx < self.
num_args(),
"Invalid argument index")
863 """Return a list containing the children of the given expression
867 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
873 return [self.
arg(i)
for i
in range(self.
num_args())]
877 def _to_expr_ref(a, ctx):
878 if isinstance(a, Pattern):
882 if k == Z3_QUANTIFIER_AST:
885 if sk == Z3_BOOL_SORT:
887 if sk == Z3_INT_SORT:
888 if k == Z3_NUMERAL_AST:
891 if sk == Z3_REAL_SORT:
892 if k == Z3_NUMERAL_AST:
894 if _is_algebraic(ctx, a):
898 if k == Z3_NUMERAL_AST:
902 if sk == Z3_ARRAY_SORT:
904 if sk == Z3_DATATYPE_SORT:
906 if sk == Z3_FLOATING_POINT_SORT:
907 if k == Z3_APP_AST
and _is_numeral(ctx, a):
911 if sk == Z3_ROUNDING_MODE_SORT:
915 def _coerce_expr_merge(s, a):
928 _z3_assert(s1.ctx == s.ctx,
"context mismatch")
929 _z3_assert(
False,
"sort mismatch")
933 def _coerce_exprs(a, b, ctx=None):
938 s = _coerce_expr_merge(s, a)
939 s = _coerce_expr_merge(s, b)
944 def _reduce(f, l, a):
950 def _coerce_expr_list(alist, ctx=None):
957 alist = [ _py2expr(a, ctx)
for a
in alist ]
958 s = _reduce(_coerce_expr_merge, alist,
None)
959 return [ s.cast(a)
for a
in alist ]
962 """Return `True` if `a` is a Z3 expression.
969 >>> is_expr(IntSort())
973 >>> is_expr(IntVal(1))
976 >>> is_expr(ForAll(x, x >= 0))
979 return isinstance(a, ExprRef)
982 """Return `True` if `a` is a Z3 function application.
984 Note that, constants are function applications with 0 arguments.
991 >>> is_app(IntSort())
995 >>> is_app(IntVal(1))
998 >>> is_app(ForAll(x, x >= 0))
1001 if not isinstance(a, ExprRef):
1003 k = _ast_kind(a.ctx, a)
1004 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
1007 """Return `True` if `a` is Z3 constant/variable expression.
1016 >>> is_const(IntVal(1))
1019 >>> is_const(ForAll(x, x >= 0))
1022 return is_app(a)
and a.num_args() == 0
1025 """Return `True` if `a` is variable.
1027 Z3 uses de-Bruijn indices for representing bound variables in
1035 >>> f = Function('f', IntSort(), IntSort())
1036 >>> # Z3 replaces x with bound variables when ForAll is executed.
1037 >>> q = ForAll(x, f(x) == x)
1043 >>> is_var(b.arg(1))
1046 return is_expr(a)
and _ast_kind(a.ctx, a) == Z3_VAR_AST
1049 """Return the de-Bruijn index of the Z3 bounded variable `a`.
1057 >>> f = Function('f', IntSort(), IntSort(), IntSort())
1058 >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1059 >>> q = ForAll([x, y], f(x, y) == x + y)
1061 f(Var(1), Var(0)) == Var(1) + Var(0)
1065 >>> v1 = b.arg(0).arg(0)
1066 >>> v2 = b.arg(0).arg(1)
1071 >>> get_var_index(v1)
1073 >>> get_var_index(v2)
1077 _z3_assert(
is_var(a),
"Z3 bound variable expected")
1081 """Return `True` if `a` is an application of the given kind `k`.
1085 >>> is_app_of(n, Z3_OP_ADD)
1087 >>> is_app_of(n, Z3_OP_MUL)
1090 return is_app(a)
and a.decl().kind() == k
1092 def If(a, b, c, ctx=None):
1093 """Create a Z3 if-then-else expression.
1097 >>> max = If(x > y, x, y)
1103 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1104 return Cond(a, b, c, ctx)
1106 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1109 b, c = _coerce_exprs(b, c, ctx)
1111 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1112 return _to_expr_ref(
Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1115 """Create a Z3 distinct expression.
1122 >>> Distinct(x, y, z)
1124 >>> simplify(Distinct(x, y, z))
1126 >>> simplify(Distinct(x, y, z), blast_distinct=True)
1127 And(Not(x == y), Not(x == z), Not(y == z))
1129 args = _get_args(args)
1130 ctx = _ctx_from_ast_arg_list(args)
1132 _z3_assert(ctx !=
None,
"At least one of the arguments must be a Z3 expression")
1133 args = _coerce_expr_list(args, ctx)
1134 _args, sz = _to_ast_array(args)
1137 def _mk_bin(f, a, b):
1140 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1141 args[0] = a.as_ast()
1142 args[1] = b.as_ast()
1143 return f(a.ctx.ref(), 2, args)
1146 """Create a constant of the given sort.
1148 >>> Const('x', IntSort())
1152 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
1157 """Create a several constants of the given sort.
1159 `names` is a string containing the names of all constants to be created.
1160 Blank spaces separate the names of different constants.
1162 >>> x, y, z = Consts('x y z', IntSort())
1166 if isinstance(names, str):
1167 names = names.split(
" ")
1168 return [
Const(name, sort)
for name
in names]
1171 """Create a Z3 free variable. Free variables are used to create quantified formulas.
1173 >>> Var(0, IntSort())
1175 >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1179 _z3_assert(
is_sort(s),
"Z3 sort expected")
1180 return _to_expr_ref(
Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1184 Create a real free variable. Free variables are used to create quantified formulas.
1185 They are also used to create polynomials.
1194 Create a list of Real free variables.
1195 The variables have ids: 0, 1, ..., n-1
1197 >>> x0, x1, x2, x3 = RealVarVector(4)
1201 return [
RealVar(i, ctx)
for i
in range(n) ]
1212 """Try to cast `val` as a Boolean.
1214 >>> x = BoolSort().cast(True)
1224 if isinstance(val, bool):
1227 _z3_assert(
is_expr(val),
"True, False or Z3 Boolean expression expected")
1228 _z3_assert(self.
eq(val.sort()),
"Value cannot be converted into a Z3 Boolean value")
1232 """All Boolean expressions are instances of this class."""
1237 """Return `True` if `a` is a Z3 Boolean expression.
1243 >>> is_bool(And(p, q))
1251 return isinstance(a, BoolRef)
1254 """Return `True` if `a` is the Z3 true expression.
1259 >>> is_true(simplify(p == p))
1264 >>> # True is a Python Boolean expression
1271 """Return `True` if `a` is the Z3 false expression.
1278 >>> is_false(BoolVal(False))
1284 """Return `True` if `a` is a Z3 and expression.
1286 >>> p, q = Bools('p q')
1287 >>> is_and(And(p, q))
1289 >>> is_and(Or(p, q))
1295 """Return `True` if `a` is a Z3 or expression.
1297 >>> p, q = Bools('p q')
1300 >>> is_or(And(p, q))
1306 """Return `True` if `a` is a Z3 not expression.
1317 """Return `True` if `a` is a Z3 equality expression.
1319 >>> x, y = Ints('x y')
1326 """Return `True` if `a` is a Z3 distinct expression.
1328 >>> x, y, z = Ints('x y z')
1329 >>> is_distinct(x == y)
1331 >>> is_distinct(Distinct(x, y, z))
1337 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1341 >>> p = Const('p', BoolSort())
1344 >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1351 return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
1353 def BoolVal(val, ctx=None):
1354 """Return the Boolean value `
True`
or `
False`. If `ctx=
None`, then the
global context
is used.
1367 return BoolRef(Z3_mk_false(ctx.ref()), ctx)
1369 return BoolRef(Z3_mk_true(ctx.ref()), ctx)
1371 def Bool(name, ctx=None):
1372 """Return a Boolean constant named `name`. If `ctx=
None`, then the
global context
is used.
1380 return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
1382 def Bools(names, ctx=None):
1383 """Return a tuple of Boolean constants.
1385 `names`
is a single string containing all names separated by blank spaces.
1386 If `ctx=
None`, then the
global context
is used.
1388 >>> p, q, r =
Bools(
'p q r')
1389 >>>
And(p,
Or(q, r))
1393 if isinstance(names, str):
1394 names = names.split(" ")
1395 return [Bool(name, ctx) for name in names]
1397 def BoolVector(prefix, sz, ctx=None):
1398 """Return a list of Boolean constants of size `sz`.
1400 The constants are named using the given prefix.
1401 If `ctx=
None`, then the
global context
is used.
1407 And(p__0, p__1, p__2)
1409 return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
1411 def FreshBool(prefix='b', ctx=None):
1412 """Return a fresh Boolean constant
in the given context using the given prefix.
1414 If `ctx=
None`, then the
global context
is used.
1422 return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
1424 def Implies(a, b, ctx=None):
1425 """Create a Z3 implies expression.
1427 >>> p, q =
Bools(
'p q')
1433 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1437 return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1439 def Xor(a, b, ctx=None):
1440 """Create a Z3 Xor expression.
1442 >>> p, q =
Bools(
'p q')
1448 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1452 return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
1454 def Not(a, ctx=None):
1455 """Create a Z3
not expression
or probe.
1463 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1465 # Not is also used to build probes
1466 return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx)
1470 return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
1472 def _has_probe(args):
1473 """Return `
True`
if one of the elements of the given collection
is a Z3 probe.
"""
1480 """Create a Z3
and-expression
or and-probe.
1482 >>> p, q, r =
Bools(
'p q r')
1487 And(p__0, p__1, p__2, p__3, p__4)
1491 last_arg = args[len(args)-1]
1492 if isinstance(last_arg, Context):
1493 ctx = args[len(args)-1]
1494 args = args[:len(args)-1]
1497 args = _get_args(args)
1498 ctx_args = _ctx_from_ast_arg_list(args, ctx)
1500 _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
1501 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
1502 if _has_probe(args):
1503 return _probe_and(args, ctx)
1505 args = _coerce_expr_list(args, ctx)
1506 _args, sz = _to_ast_array(args)
1507 return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
1510 """Create a Z3
or-expression
or or-probe.
1512 >>> p, q, r =
Bools(
'p q r')
1517 Or(p__0, p__1, p__2, p__3, p__4)
1521 last_arg = args[len(args)-1]
1522 if isinstance(last_arg, Context):
1523 ctx = args[len(args)-1]
1524 args = args[:len(args)-1]
1527 args = _get_args(args)
1528 ctx_args = _ctx_from_ast_arg_list(args, ctx)
1530 _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
1531 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
1532 if _has_probe(args):
1533 return _probe_or(args, ctx)
1535 args = _coerce_expr_list(args, ctx)
1536 _args, sz = _to_ast_array(args)
1537 return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
1539 #########################################
1543 #########################################
1545 class PatternRef(ExprRef):
1546 """Patterns are hints
for quantifier instantiation.
1548 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1551 return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
1554 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
1557 """Return `
True`
if `a`
is a Z3 pattern (hint
for quantifier instantiation.
1559 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1563 >>> q =
ForAll(x, f(x) == 0, patterns = [ f(x) ])
1566 >>> q.num_patterns()
1573 return isinstance(a, PatternRef)
1575 def MultiPattern(*args):
1576 """Create a Z3 multi-pattern using the given expressions `*args`
1578 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1586 >>> q.num_patterns()
1594 _z3_assert(len(args) > 0, "At least one argument expected")
1595 _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected")
1597 args, sz = _to_ast_array(args)
1598 return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
1600 def _to_pattern(arg):
1604 return MultiPattern(arg)
1606 #########################################
1610 #########################################
1612 class QuantifierRef(BoolRef):
1613 """Universally
and Existentially quantified formulas.
"""
1619 return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
1622 """Return the Boolean sort.
"""
1623 return BoolSort(self.ctx)
1625 def is_forall(self):
1626 """Return `
True`
if `self`
is a universal quantifier.
1630 >>> q =
ForAll(x, f(x) == 0)
1633 >>> q =
Exists(x, f(x) != 0)
1637 return Z3_is_quantifier_forall(self.ctx_ref(), self.ast)
1640 """Return the weight annotation of `self`.
1644 >>> q =
ForAll(x, f(x) == 0)
1647 >>> q =
ForAll(x, f(x) == 0, weight=10)
1651 return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast))
1653 def num_patterns(self):
1654 """Return the number of patterns (i.e., quantifier instantiation hints)
in `self`.
1659 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1660 >>> q.num_patterns()
1663 return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast))
1665 def pattern(self, idx):
1666 """Return a pattern (i.e., quantifier instantiation hints)
in `self`.
1671 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1672 >>> q.num_patterns()
1680 _z3_assert(idx < self.num_patterns(), "Invalid pattern idx")
1681 return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1683 def num_no_patterns(self):
1684 """Return the number of no-patterns.
"""
1685 return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast)
1687 def no_pattern(self, idx):
1688 """Return a no-pattern.
"""
1690 _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx")
1691 return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx)
1694 """Return the expression being quantified.
1698 >>> q =
ForAll(x, f(x) == 0)
1702 return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx)
1705 """Return the number of variables bounded by this quantifier.
1710 >>> q =
ForAll([x, y], f(x, y) >= x)
1714 return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast))
1716 def var_name(self, idx):
1717 """Return a string representing a name used when displaying the quantifier.
1722 >>> q =
ForAll([x, y], f(x, y) >= x)
1729 _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1730 return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx))
1732 def var_sort(self, idx):
1733 """Return the sort of a bound variable.
1738 >>> q =
ForAll([x, y], f(x, y) >= x)
1745 _z3_assert(idx < self.num_vars(), "Invalid variable idx")
1746 return SortRef(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
1749 """Return a list containing a single element self.
body()
1753 >>> q =
ForAll(x, f(x) == 0)
1757 return [ self.body() ]
1759 def is_quantifier(a):
1760 """Return `
True`
if `a`
is a Z3 quantifier.
1764 >>> q =
ForAll(x, f(x) == 0)
1770 return isinstance(a, QuantifierRef)
1772 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1774 _z3_assert(is_bool(body), "Z3 expression expected")
1775 _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)")
1776 _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected")
1777 _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions")
1782 _vs = (Ast * num_vars)()
1783 for i in range(num_vars):
1784 ## TODO: Check if is constant
1785 _vs[i] = vs[i].as_ast()
1786 patterns = [ _to_pattern(p) for p in patterns ]
1787 num_pats = len(patterns)
1788 _pats = (Pattern * num_pats)()
1789 for i in range(num_pats):
1790 _pats[i] = patterns[i].ast
1791 _no_pats, num_no_pats = _to_ast_array(no_patterns)
1792 qid = to_symbol(qid, ctx)
1793 skid = to_symbol(skid, ctx)
1794 return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid,
1797 num_no_pats, _no_pats,
1798 body.as_ast()), ctx)
1800 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1801 """Create a Z3 forall formula.
1803 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
1805 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1810 >>>
ForAll([x, y], f(x, y) >= x)
1811 ForAll([x, y], f(x, y) >= x)
1812 >>>
ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
1813 ForAll([x, y], f(x, y) >= x)
1814 >>>
ForAll([x, y], f(x, y) >= x, weight=10)
1815 ForAll([x, y], f(x, y) >= x)
1817 return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
1819 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1820 """Create a Z3 exists formula.
1822 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
1824 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1829 >>> q =
Exists([x, y], f(x, y) >= x, skid=
"foo")
1831 Exists([x, y], f(x, y) >= x)
1834 >>> r =
Tactic(
'nnf')(q).as_expr()
1838 return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
1840 #########################################
1844 #########################################
1846 class ArithSortRef(SortRef):
1847 """Real
and Integer sorts.
"""
1850 """Return `
True`
if `self`
is of the sort Real.
1861 return self.kind() == Z3_REAL_SORT
1864 """Return `
True`
if `self`
is of the sort Integer.
1875 return self.kind() == Z3_INT_SORT
1877 def subsort(self, other):
1878 """Return `
True`
if `self`
is a subsort of `other`.
"""
1879 return self.is_int() and is_arith_sort(other) and other.is_real()
1881 def cast(self, val):
1882 """Try to cast `val`
as an Integer
or Real.
1897 _z3_assert(self.ctx == val.ctx, "Context mismatch")
1901 if val_s.is_int() and self.is_real():
1904 _z3_assert(False, "Z3 Integer/Real expression expected" )
1907 return IntVal(val, self.ctx)
1909 return RealVal(val, self.ctx)
1911 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
1913 def is_arith_sort(s):
1914 """Return `
True`
if s
is an arithmetical sort (type).
1922 >>> n =
Int(
'x') + 1
1926 return isinstance(s, ArithSortRef)
1928 class ArithRef(ExprRef):
1929 """Integer
and Real expressions.
"""
1932 """Return the sort (type) of the arithmetical expression `self`.
1939 return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
1942 """Return `
True`
if `self`
is an integer expression.
1953 return self.sort().is_int()
1956 """Return `
True`
if `self`
is an real expression.
1964 return self.sort().is_real()
1966 def __add__(self, other):
1967 """Create the Z3 expression `self + other`.
1976 a, b = _coerce_exprs(self, other)
1977 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
1979 def __radd__(self, other):
1980 """Create the Z3 expression `other + self`.
1986 a, b = _coerce_exprs(self, other)
1987 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
1989 def __mul__(self, other):
1990 """Create the Z3 expression `self * other`.
1999 a, b = _coerce_exprs(self, other)
2000 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
2002 def __rmul__(self, other):
2003 """Create the Z3 expression `other * self`.
2009 a, b = _coerce_exprs(self, other)
2010 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
2012 def __sub__(self, other):
2013 """Create the Z3 expression `self - other`.
2022 a, b = _coerce_exprs(self, other)
2023 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
2025 def __rsub__(self, other):
2026 """Create the Z3 expression `other - self`.
2032 a, b = _coerce_exprs(self, other)
2033 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
2035 def __pow__(self, other):
2036 """Create the Z3 expression `self**other` (**
is the power operator).
2046 a, b = _coerce_exprs(self, other)
2047 return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2049 def __rpow__(self, other):
2050 """Create the Z3 expression `other**self` (**
is the power operator).
2060 a, b = _coerce_exprs(self, other)
2061 return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2063 def __div__(self, other):
2064 """Create the Z3 expression `other/self`.
2083 a, b = _coerce_exprs(self, other)
2084 return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2086 def __truediv__(self, other):
2087 """Create the Z3 expression `other/self`.
"""
2088 return self.__div__(other)
2090 def __rdiv__(self, other):
2091 """Create the Z3 expression `other/self`.
2104 a, b = _coerce_exprs(self, other)
2105 return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2107 def __rtruediv__(self, other):
2108 """Create the Z3 expression `other/self`.
"""
2109 return self.__rdiv__(other)
2111 def __mod__(self, other):
2112 """Create the Z3 expression `other%self`.
2121 a, b = _coerce_exprs(self, other)
2123 _z3_assert(a.is_int(), "Z3 integer expression expected")
2124 return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2126 def __rmod__(self, other):
2127 """Create the Z3 expression `other%self`.
2133 a, b = _coerce_exprs(self, other)
2135 _z3_assert(a.is_int(), "Z3 integer expression expected")
2136 return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2139 """Return an expression representing `-self`.
2147 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
2158 def __le__(self, other):
2159 """Create the Z3 expression `other <= self`.
2161 >>> x, y =
Ints(
'x y')
2168 a, b = _coerce_exprs(self, other)
2169 return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2171 def __lt__(self, other):
2172 """Create the Z3 expression `other < self`.
2174 >>> x, y =
Ints(
'x y')
2181 a, b = _coerce_exprs(self, other)
2182 return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2184 def __gt__(self, other):
2185 """Create the Z3 expression `other > self`.
2187 >>> x, y =
Ints(
'x y')
2194 a, b = _coerce_exprs(self, other)
2195 return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2197 def __ge__(self, other):
2198 """Create the Z3 expression `other >= self`.
2200 >>> x, y =
Ints(
'x y')
2207 a, b = _coerce_exprs(self, other)
2208 return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2211 """Return `
True`
if `a`
is an arithmetical expression.
2228 return isinstance(a, ArithRef)
2231 """Return `
True`
if `a`
is an integer expression.
2246 return is_arith(a) and a.is_int()
2249 """Return `
True`
if `a`
is a real expression.
2264 return is_arith(a) and a.is_real()
2266 def _is_numeral(ctx, a):
2267 return Z3_is_numeral_ast(ctx.ref(), a)
2269 def _is_algebraic(ctx, a):
2270 return Z3_is_algebraic_number(ctx.ref(), a)
2272 def is_int_value(a):
2273 """Return `
True`
if `a`
is an integer value of sort Int.
2281 >>> n =
Int(
'x') + 1
2293 return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
2295 def is_rational_value(a):
2296 """Return `
True`
if `a`
is rational value of sort Real.
2306 >>> n =
Real(
'x') + 1
2314 return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
2316 def is_algebraic_value(a):
2317 """Return `
True`
if `a`
is an algerbraic value of sort Real.
2327 return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
2330 """Return `
True`
if `a`
is an expression of the form b + c.
2332 >>> x, y =
Ints(
'x y')
2338 return is_app_of(a, Z3_OP_ADD)
2341 """Return `
True`
if `a`
is an expression of the form b * c.
2343 >>> x, y =
Ints(
'x y')
2349 return is_app_of(a, Z3_OP_MUL)
2352 """Return `
True`
if `a`
is an expression of the form b - c.
2354 >>> x, y =
Ints(
'x y')
2360 return is_app_of(a, Z3_OP_SUB)
2363 """Return `
True`
if `a`
is an expression of the form b / c.
2365 >>> x, y =
Reals(
'x y')
2370 >>> x, y =
Ints(
'x y')
2376 return is_app_of(a, Z3_OP_DIV)
2379 """Return `
True`
if `a`
is an expression of the form b div c.
2381 >>> x, y =
Ints(
'x y')
2387 return is_app_of(a, Z3_OP_IDIV)
2390 """Return `
True`
if `a`
is an expression of the form b % c.
2392 >>> x, y =
Ints(
'x y')
2398 return is_app_of(a, Z3_OP_MOD)
2401 """Return `
True`
if `a`
is an expression of the form b <= c.
2403 >>> x, y =
Ints(
'x y')
2409 return is_app_of(a, Z3_OP_LE)
2412 """Return `
True`
if `a`
is an expression of the form b < c.
2414 >>> x, y =
Ints(
'x y')
2420 return is_app_of(a, Z3_OP_LT)
2423 """Return `
True`
if `a`
is an expression of the form b >= c.
2425 >>> x, y =
Ints(
'x y')
2431 return is_app_of(a, Z3_OP_GE)
2434 """Return `
True`
if `a`
is an expression of the form b > c.
2436 >>> x, y =
Ints(
'x y')
2442 return is_app_of(a, Z3_OP_GT)
2445 """Return `
True`
if `a`
is an expression of the form
IsInt(b).
2453 return is_app_of(a, Z3_OP_IS_INT)
2456 """Return `
True`
if `a`
is an expression of the form
ToReal(b).
2467 return is_app_of(a, Z3_OP_TO_REAL)
2470 """Return `
True`
if `a`
is an expression of the form
ToInt(b).
2481 return is_app_of(a, Z3_OP_TO_INT)
2483 class IntNumRef(ArithRef):
2484 """Integer values.
"""
2487 """Return a Z3 integer numeral
as a Python long (bignum) numeral.
2496 _z3_assert(self.is_int(), "Integer value expected")
2497 return int(self.as_string())
2499 def as_string(self):
2500 """Return a Z3 integer numeral
as a Python string.
2505 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
2507 class RatNumRef(ArithRef):
2508 """Rational values.
"""
2510 def numerator(self):
2511 """ Return the numerator of a Z3 rational numeral.
2523 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
2525 def denominator(self):
2526 """ Return the denominator of a Z3 rational numeral.
2534 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
2536 def numerator_as_long(self):
2537 """ Return the numerator
as a Python long.
2544 >>> v.numerator_as_long() + 1 == 10000000001
2547 return self.numerator().as_long()
2549 def denominator_as_long(self):
2550 """ Return the denominator
as a Python long.
2555 >>> v.denominator_as_long()
2558 return self.denominator().as_long()
2560 def as_decimal(self, prec):
2561 """ Return a Z3 rational value
as a string
in decimal notation using at most `prec` decimal places.
2570 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
2572 def as_string(self):
2573 """Return a Z3 rational numeral
as a Python string.
2579 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
2581 def as_fraction(self):
2582 """Return a Z3 rational
as a Python Fraction object.
2588 return Fraction(self.numerator_as_long(), self.denominator_as_long())
2590 class AlgebraicNumRef(ArithRef):
2591 """Algebraic irrational values.
"""
2593 def approx(self, precision=10):
2594 """Return a Z3 rational number that approximates the algebraic number `self`.
2595 The result `r`
is such that |r - self| <= 1/10^precision
2599 6838717160008073720548335/4835703278458516698824704
2603 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
2604 def as_decimal(self, prec):
2605 """Return a string representation of the algebraic number `self`
in decimal notation using `prec` decimal places
2608 >>> x.as_decimal(10)
2610 >>> x.as_decimal(20)
2611 '1.41421356237309504880?'
2613 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
2615 def _py2expr(a, ctx=None):
2616 if isinstance(a, bool):
2617 return BoolVal(a, ctx)
2619 return IntVal(a, ctx)
2620 if isinstance(a, float):
2621 return RealVal(a, ctx)
2623 _z3_assert(False, "Python bool, int, long or float expected")
2625 def IntSort(ctx=None):
2626 """Return the interger sort
in the given context. If `ctx=
None`, then the
global context
is used.
2639 return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
2641 def RealSort(ctx=None):
2642 """Return the real sort
in the given context. If `ctx=
None`, then the
global context
is used.
2655 return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)
2657 def _to_int_str(val):
2658 if isinstance(val, float):
2659 return str(int(val))
2660 elif isinstance(val, bool):
2667 elif isinstance(val, str):
2670 _z3_assert(False, "Python value cannot be used as a Z3 integer")
2672 def IntVal(val, ctx=None):
2673 """Return a Z3 integer value. If `ctx=
None`, then the
global context
is used.
2681 return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
2683 def RealVal(val, ctx=None):
2684 """Return a Z3 real value.
2686 `val` may be a Python int, long, float
or string representing a number
in decimal
or rational notation.
2687 If `ctx=
None`, then the
global context
is used.
2699 return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
2701 def RatVal(a, b, ctx=None):
2702 """Return a Z3 rational a/b.
2704 If `ctx=
None`, then the
global context
is used.
2712 _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
2713 _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
2714 return simplify(RealVal(a, ctx)/RealVal(b, ctx))
2716 def Q(a, b, ctx=None):
2717 """Return a Z3 rational a/b.
2719 If `ctx=
None`, then the
global context
is used.
2726 return simplify(RatVal(a, b))
2728 def Int(name, ctx=None):
2729 """Return an integer constant named `name`. If `ctx=
None`, then the
global context
is used.
2738 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
2740 def Ints(names, ctx=None):
2741 """Return a tuple of Integer constants.
2743 >>> x, y, z =
Ints(
'x y z')
2748 if isinstance(names, str):
2749 names = names.split(" ")
2750 return [Int(name, ctx) for name in names]
2752 def IntVector(prefix, sz, ctx=None):
2753 """Return a list of integer constants of size `sz`.
2761 return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ]
2763 def FreshInt(prefix='x', ctx=None):
2764 """Return a fresh integer constant
in the given context using the given prefix.
2774 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
2776 def Real(name, ctx=None):
2777 """Return a real constant named `name`. If `ctx=
None`, then the
global context
is used.
2786 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)
2788 def Reals(names, ctx=None):
2789 """Return a tuple of real constants.
2791 >>> x, y, z =
Reals(
'x y z')
2794 >>>
Sum(x, y, z).sort()
2798 if isinstance(names, str):
2799 names = names.split(" ")
2800 return [Real(name, ctx) for name in names]
2802 def RealVector(prefix, sz, ctx=None):
2803 """Return a list of real constants of size `sz`.
2813 return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ]
2815 def FreshReal(prefix='b', ctx=None):
2816 """Return a fresh real constant
in the given context using the given prefix.
2826 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
2829 """ Return the Z3 expression
ToReal(a).
2841 _z3_assert(a.is_int(), "Z3 integer expression expected.")
2843 return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
2846 """ Return the Z3 expression
ToInt(a).
2858 _z3_assert(a.is_real(), "Z3 real expression expected.")
2860 return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)
2863 """ Return the Z3 predicate
IsInt(a).
2866 >>>
IsInt(x +
"1/2")
2870 >>>
solve(
IsInt(x +
"1/2"), x > 0, x < 1, x !=
"1/2")
2874 _z3_assert(a.is_real(), "Z3 real expression expected.")
2876 return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
2878 def Sqrt(a, ctx=None):
2879 """ Return a Z3 expression which represents the square root of a.
2890 def Cbrt(a, ctx=None):
2891 """ Return a Z3 expression which represents the cubic root of a.
2902 #########################################
2906 #########################################
2908 class BitVecSortRef(SortRef):
2909 """Bit-vector sort.
"""
2912 """Return the size (number of bits) of the bit-vector sort `self`.
2918 return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast))
2920 def subsort(self, other):
2921 return is_bv_sort(other) and self.size() < other.size()
2923 def cast(self, val):
2924 """Try to cast `val`
as a Bit-Vector.
2929 >>> b.cast(10).
sexpr()
2934 _z3_assert(self.ctx == val.ctx, "Context mismatch")
2935 # Idea: use sign_extend if sort of val is a bitvector of smaller size
2938 return BitVecVal(val, self)
2941 """Return
True if `s`
is a Z3 bit-vector sort.
2948 return isinstance(s, BitVecSortRef)
2950 class BitVecRef(ExprRef):
2951 """Bit-vector expressions.
"""
2954 """Return the sort of the bit-vector expression `self`.
2962 return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
2965 """Return the number of bits of the bit-vector expression `self`.
2973 return self.sort().size()
2975 def __add__(self, other):
2976 """Create the Z3 expression `self + other`.
2985 a, b = _coerce_exprs(self, other)
2986 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2988 def __radd__(self, other):
2989 """Create the Z3 expression `other + self`.
2995 a, b = _coerce_exprs(self, other)
2996 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2998 def __mul__(self, other):
2999 """Create the Z3 expression `self * other`.
3008 a, b = _coerce_exprs(self, other)
3009 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3011 def __rmul__(self, other):
3012 """Create the Z3 expression `other * self`.
3018 a, b = _coerce_exprs(self, other)
3019 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3021 def __sub__(self, other):
3022 """Create the Z3 expression `self - other`.
3031 a, b = _coerce_exprs(self, other)
3032 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3034 def __rsub__(self, other):
3035 """Create the Z3 expression `other - self`.
3041 a, b = _coerce_exprs(self, other)
3042 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3044 def __or__(self, other):
3045 """Create the Z3 expression bitwise-
or `self | other`.
3054 a, b = _coerce_exprs(self, other)
3055 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3057 def __ror__(self, other):
3058 """Create the Z3 expression bitwise-
or `other | self`.
3064 a, b = _coerce_exprs(self, other)
3065 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3067 def __and__(self, other):
3068 """Create the Z3 expression bitwise-
and `self & other`.
3077 a, b = _coerce_exprs(self, other)
3078 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3080 def __rand__(self, other):
3081 """Create the Z3 expression bitwise-
or `other & self`.
3087 a, b = _coerce_exprs(self, other)
3088 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3090 def __xor__(self, other):
3091 """Create the Z3 expression bitwise-xor `self ^ other`.
3100 a, b = _coerce_exprs(self, other)
3101 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3103 def __rxor__(self, other):
3104 """Create the Z3 expression bitwise-xor `other ^ self`.
3110 a, b = _coerce_exprs(self, other)
3111 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3123 """Return an expression representing `-self`.
3131 return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx)
3133 def __invert__(self):
3134 """Create the Z3 expression bitwise-
not `~self`.
3142 return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx)
3144 def __div__(self, other):
3145 """Create the Z3 expression (signed) division `self / other`.
3147 Use the function
UDiv()
for unsigned division.
3160 a, b = _coerce_exprs(self, other)
3161 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3163 def __truediv__(self, other):
3164 """Create the Z3 expression (signed) division `self / other`.
"""
3165 return self.__div__(other)
3167 def __rdiv__(self, other):
3168 """Create the Z3 expression (signed) division `other / self`.
3170 Use the function
UDiv()
for unsigned division.
3175 >>> (10 / x).
sexpr()
3176 '(bvsdiv #x0000000a x)'
3178 '(bvudiv #x0000000a x)'
3180 a, b = _coerce_exprs(self, other)
3181 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3183 def __rtruediv__(self, other):
3184 """Create the Z3 expression (signed) division `other / self`.
"""
3185 return self.__rdiv__(other)
3187 def __mod__(self, other):
3188 """Create the Z3 expression (signed) mod `self % other`.
3190 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3205 a, b = _coerce_exprs(self, other)
3206 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3208 def __rmod__(self, other):
3209 """Create the Z3 expression (signed) mod `other % self`.
3211 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3216 >>> (10 % x).
sexpr()
3217 '(bvsmod #x0000000a x)'
3219 '(bvurem #x0000000a x)'
3221 '(bvsrem #x0000000a x)'
3223 a, b = _coerce_exprs(self, other)
3224 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3226 def __le__(self, other):
3227 """Create the Z3 expression (signed) `other <= self`.
3229 Use the function
ULE()
for unsigned less than
or equal to.
3234 >>> (x <= y).
sexpr()
3239 a, b = _coerce_exprs(self, other)
3240 return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3242 def __lt__(self, other):
3243 """Create the Z3 expression (signed) `other < self`.
3245 Use the function
ULT()
for unsigned less than.
3255 a, b = _coerce_exprs(self, other)
3256 return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3258 def __gt__(self, other):
3259 """Create the Z3 expression (signed) `other > self`.
3261 Use the function
UGT()
for unsigned greater than.
3271 a, b = _coerce_exprs(self, other)
3272 return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3274 def __ge__(self, other):
3275 """Create the Z3 expression (signed) `other >= self`.
3277 Use the function
UGE()
for unsigned greater than
or equal to.
3282 >>> (x >= y).
sexpr()
3287 a, b = _coerce_exprs(self, other)
3288 return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3290 def __rshift__(self, other):
3291 """Create the Z3 expression (arithmetical) right shift `self >> other`
3293 Use the function
LShR()
for the right logical shift
3298 >>> (x >> y).
sexpr()
3317 a, b = _coerce_exprs(self, other)
3318 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3320 def __lshift__(self, other):
3321 """Create the Z3 expression left shift `self << other`
3326 >>> (x << y).
sexpr()
3331 a, b = _coerce_exprs(self, other)
3332 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
3334 def __rrshift__(self, other):
3335 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3337 Use the function
LShR()
for the right logical shift
3342 >>> (10 >> x).
sexpr()
3343 '(bvashr #x0000000a x)'
3345 a, b = _coerce_exprs(self, other)
3346 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3348 def __rlshift__(self, other):
3349 """Create the Z3 expression left shift `other << self`.
3351 Use the function
LShR()
for the right logical shift
3356 >>> (10 << x).
sexpr()
3357 '(bvshl #x0000000a x)'
3359 a, b = _coerce_exprs(self, other)
3360 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
3362 class BitVecNumRef(BitVecRef):
3363 """Bit-vector values.
"""
3366 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral.
3371 >>> print(
"0x%.8x" % v.as_long())
3374 return int(self.as_string())
3376 def as_signed_long(self):
3377 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral. The most significant bit
is assumed to be the sign.
3391 val = self.as_long()
3392 if val >= 2**(sz - 1):
3394 if val < -2**(sz - 1):
3398 def as_string(self):
3399 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
3402 """Return `
True`
if `a`
is a Z3 bit-vector expression.
3412 return isinstance(a, BitVecRef)
3415 """Return `
True`
if `a`
is a Z3 bit-vector numeral value.
3426 return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
3429 """Return the Z3 expression
BV2Int(a).
3441 _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
3443 ## investigate problem with bv2int
3444 return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)
3446 def BitVecSort(sz, ctx=None):
3447 """Return a Z3 bit-vector sort of the given size. If `ctx=
None`, then the
global context
is used.
3453 >>> x =
Const(
'x', Byte)
3458 return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
3460 def BitVecVal(val, bv, ctx=None):
3461 """Return a bit-vector value with the given number of bits. If `ctx=
None`, then the
global context
is used.
3466 >>> print(
"0x%.8x" % v.as_long())
3471 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3474 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
3476 def BitVec(name, bv, ctx=None):
3477 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3478 If `ctx=
None`, then the
global context
is used.
3488 >>> x2 =
BitVec(
'x', word)
3492 if isinstance(bv, BitVecSortRef):
3496 bv = BitVecSort(bv, ctx)
3497 return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
3499 def BitVecs(names, bv, ctx=None):
3500 """Return a tuple of bit-vector constants of size bv.
3502 >>> x, y, z =
BitVecs(
'x y z', 16)
3515 if isinstance(names, str):
3516 names = names.split(" ")
3517 return [BitVec(name, bv, ctx) for name in names]
3520 """Create a Z3 bit-vector concatenation expression.
3530 args = _get_args(args)
3532 _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
3533 _z3_assert(len(args) >= 2, "At least two arguments expected.")
3536 for i in range(len(args) - 1):
3537 r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
3540 def Extract(high, low, a):
3541 """Create a Z3 bit-vector extraction expression.
3550 _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
3551 _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
3552 _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
3553 return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
3555 def _check_bv_args(a, b):
3557 _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression")
3560 """Create the Z3 expression (unsigned) `other <= self`.
3562 Use the operator <=
for signed less than
or equal to.
3567 >>> (x <= y).sexpr()
3569 >>>
ULE(x, y).sexpr()
3572 _check_bv_args(a, b)
3573 a, b = _coerce_exprs(a, b)
3574 return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3577 """Create the Z3 expression (unsigned) `other < self`.
3579 Use the operator <
for signed less than.
3586 >>>
ULT(x, y).sexpr()
3589 _check_bv_args(a, b)
3590 a, b = _coerce_exprs(a, b)
3591 return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3594 """Create the Z3 expression (unsigned) `other >= self`.
3596 Use the operator >=
for signed greater than
or equal to.
3601 >>> (x >= y).sexpr()
3603 >>>
UGE(x, y).sexpr()
3606 _check_bv_args(a, b)
3607 a, b = _coerce_exprs(a, b)
3608 return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3611 """Create the Z3 expression (unsigned) `other > self`.
3613 Use the operator >
for signed greater than.
3620 >>>
UGT(x, y).sexpr()
3623 _check_bv_args(a, b)
3624 a, b = _coerce_exprs(a, b)
3625 return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3628 """Create the Z3 expression (unsigned) division `self / other`.
3630 Use the operator /
for signed division.
3636 >>>
UDiv(x, y).sort()
3640 >>>
UDiv(x, y).sexpr()
3643 _check_bv_args(a, b)
3644 a, b = _coerce_exprs(a, b)
3645 return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3648 """Create the Z3 expression (unsigned) remainder `self % other`.
3650 Use the operator %
for signed modulus,
and SRem()
for signed remainder.
3656 >>>
URem(x, y).sort()
3660 >>>
URem(x, y).sexpr()
3663 _check_bv_args(a, b)
3664 a, b = _coerce_exprs(a, b)
3665 return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3668 """Create the Z3 expression signed remainder.
3670 Use the operator %
for signed modulus,
and URem()
for unsigned remainder.
3676 >>>
SRem(x, y).sort()
3680 >>>
SRem(x, y).sexpr()
3683 _check_bv_args(a, b)
3684 a, b = _coerce_exprs(a, b)
3685 return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3688 """Create the Z3 expression logical right shift.
3690 Use the operator >>
for the arithmetical right shift.
3695 >>> (x >> y).sexpr()
3697 >>>
LShR(x, y).sexpr()
3714 _check_bv_args(a, b)
3715 a, b = _coerce_exprs(a, b)
3716 return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3718 def RotateLeft(a, b):
3719 """Return an expression representing `a` rotated to the left `b` times.
3729 _check_bv_args(a, b)
3730 a, b = _coerce_exprs(a, b)
3731 return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3733 def RotateRight(a, b):
3734 """Return an expression representing `a` rotated to the right `b` times.
3744 _check_bv_args(a, b)
3745 a, b = _coerce_exprs(a, b)
3746 return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
3749 """Return a bit-vector expression with `n` extra sign-bits.
3769 >>> print(
"%.x" % v.as_long())
3773 _z3_assert(isinstance(n, int), "First argument must be an integer")
3774 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3775 return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
3778 """Return a bit-vector expression with `n` extra zero-bits.
3800 _z3_assert(isinstance(n, int), "First argument must be an integer")
3801 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3802 return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
3804 def RepeatBitVec(n, a):
3805 """Return an expression representing `n` copies of `a`.
3814 >>> print(
"%.x" % v0.as_long())
3819 >>> print(
"%.x" % v.as_long())
3823 _z3_assert(isinstance(n, int), "First argument must be an integer")
3824 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
3825 return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
3828 """Return the reduction-
and expression of `a`.
"""
3830 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
3831 return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
3834 """Return the reduction-
or expression of `a`.
"""
3836 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
3837 return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
3839 #########################################
3843 #########################################
3845 class ArraySortRef(SortRef):
3849 """Return the domain of the array sort `self`.
3855 return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx)
3858 """Return the range of the array sort `self`.
3864 return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)
3866 class ArrayRef(ExprRef):
3867 """Array expressions.
"""
3870 """Return the array sort of the array expression `self`.
3876 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
3885 return self.sort().domain()
3894 return self.sort().range()
3896 def __getitem__(self, arg):
3897 """Return the Z3 expression `self[arg]`.
3906 arg = self.domain().cast(arg)
3907 return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
3910 """Return `
True`
if `a`
is a Z3 array expression.
3920 return isinstance(a, ArrayRef)
3922 def is_const_array(a):
3923 """Return `
True`
if `a`
is a Z3 constant array.
3932 return is_app_of(a, Z3_OP_CONST_ARRAY)
3935 """Return `
True`
if `a`
is a Z3 constant array.
3944 return is_app_of(a, Z3_OP_CONST_ARRAY)
3947 """Return `
True`
if `a`
is a Z3 map array expression.
3959 return is_app_of(a, Z3_OP_ARRAY_MAP)
3961 def get_map_func(a):
3962 """Return the function declaration associated with a Z3 map array expression.
3975 _z3_assert(is_map(a), "Z3 array map expression expected.")
3976 return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
3978 def ArraySort(d, r):
3979 """Return the Z3 array sort with the given domain
and range sorts.
3993 _z3_assert(is_sort(d), "Z3 sort expected")
3994 _z3_assert(is_sort(r), "Z3 sort expected")
3995 _z3_assert(d.ctx == r.ctx, "Context mismatch")
3997 return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
3999 def Array(name, dom, rng):
4000 """Return an array constant named `name` with the given domain
and range sorts.
4008 s = ArraySort(dom, rng)
4010 return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
4012 def Update(a, i, v):
4013 """Return a Z3 store array expression.
4016 >>> i, v =
Ints(
'i v')
4020 >>>
prove(s[i] == v)
4027 _z3_assert(is_array(a), "First argument must be a Z3 array expression")
4028 i = a.domain().cast(i)
4029 v = a.range().cast(v)
4031 return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
4034 """Return a Z3 store array expression.
4037 >>> i, v =
Ints(
'i v')
4038 >>> s =
Store(a, i, v)
4041 >>>
prove(s[i] == v)
4047 return Update(a, i, v)
4050 """Return a Z3 select array expression.
4060 _z3_assert(is_array(a), "First argument must be a Z3 array expression")
4064 """Return a Z3 map array expression.
4069 >>> b =
Map(f, a1, a2)
4072 >>>
prove(b[0] == f(a1[0], a2[0]))
4075 args = _get_args(args)
4077 _z3_assert(len(args) > 0, "At least one Z3 array expression expected")
4078 _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration")
4079 _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected")
4080 _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
4081 _args, sz = _to_ast_array(args)
4083 return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
4086 """Return a Z3 constant array expression.
4100 _z3_assert(is_sort(dom), "Z3 sort expected")
4103 v = _py2expr(v, ctx)
4104 return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
4107 """Return `
True`
if `a`
is a Z3 array select application.
4116 return is_app_of(a, Z3_OP_SELECT)
4119 """Return `
True`
if `a`
is a Z3 array store application.
4127 return is_app_of(a, Z3_OP_STORE)
4129 #########################################
4133 #########################################
4135 def _valid_accessor(acc):
4136 """Return `
True`
if acc
is pair of the form (String, Datatype
or Sort).
"""
4137 return isinstance(acc, tuple) and len(acc) == 2 and isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1]))
4140 """Helper
class for declaring Z3 datatypes.
4143 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4144 >>> List.declare(
'nil')
4145 >>> List = List.create()
4149 >>> List.cons(10, List.nil)
4151 >>> List.cons(10, List.nil).sort()
4153 >>> cons = List.cons
4157 >>> n = cons(1, cons(0, nil))
4159 cons(1, cons(0, nil))
4165 def __init__(self, name, ctx=None):
4166 self.ctx = _get_ctx(ctx)
4168 self.constructors = []
4170 def declare_core(self, name, rec_name, *args):
4172 _z3_assert(isinstance(name, str), "String expected")
4173 _z3_assert(isinstance(rec_name, str), "String expected")
4174 _z3_assert(all([_valid_accessor(a) for a in args]), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)")
4175 self.constructors.append((name, rec_name, args))
4177 def declare(self, name, *args):
4178 """Declare constructor named `name` with the given accessors `args`.
4179 Each accessor
is a pair `(name, sort)`, where `name`
is a string
and `sort` a Z3 sort
or a reference to the datatypes being declared.
4181 In the followin example `List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))`
4182 declares the constructor named `cons` that builds a new List using an integer
and a List.
4183 It also declares the accessors `car`
and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
4184 and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method
create() to create
4185 the actual datatype
in Z3.
4188 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4189 >>> List.declare(
'nil')
4190 >>> List = List.create()
4193 _z3_assert(isinstance(name, str), "String expected")
4194 _z3_assert(name != "", "Constructor name cannot be empty")
4195 return self.declare_core(name, "is_" + name, *args)
4198 return "Datatype(%s, %s)" % (self.name, self.constructors)
4201 """Create a Z3 datatype based on the constructors declared using the mehtod `
declare()`.
4203 The function `
CreateDatatypes()` must be used to define mutually recursive datatypes.
4206 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4207 >>> List.declare(
'nil')
4208 >>> List = List.create()
4211 >>> List.cons(10, List.nil)
4214 return CreateDatatypes([self])[0]
4216 class ScopedConstructor:
4217 """Auxiliary object used to create Z3 datatypes.
"""
4218 def __init__(self, c, ctx):
4222 Z3_del_constructor(self.ctx.ref(), self.c)
4224 class ScopedConstructorList:
4225 """Auxiliary object used to create Z3 datatypes.
"""
4226 def __init__(self, c, ctx):
4230 Z3_del_constructor_list(self.ctx.ref(), self.c)
4232 def CreateDatatypes(*ds):
4233 """Create mutually recursive Z3 datatypes using 1
or more Datatype helper objects.
4235 In the following example we define a Tree-List using two mutually recursive datatypes.
4237 >>> TreeList =
Datatype(
'TreeList')
4240 >>> Tree.declare(
'leaf', (
'val',
IntSort()))
4242 >>> Tree.declare(
'node', (
'children', TreeList))
4243 >>> TreeList.declare(
'nil')
4244 >>> TreeList.declare(
'cons', (
'car', Tree), (
'cdr', TreeList))
4246 >>> Tree.val(Tree.leaf(10))
4248 >>>
simplify(Tree.val(Tree.leaf(10)))
4250 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4252 node(cons(leaf(10), cons(leaf(20), nil)))
4253 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4256 >>>
simplify(TreeList.car(Tree.children(n2)) == n1)
4261 _z3_assert(len(ds) > 0, "At least one Datatype must be specified")
4262 _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
4263 _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
4264 _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
4267 names = (Symbol * num)()
4268 out = (Sort * num)()
4269 clists = (ConstructorList * num)()
4271 for i in range(num):
4273 names[i] = to_symbol(d.name, ctx)
4274 num_cs = len(d.constructors)
4275 cs = (Constructor * num_cs)()
4276 for j in range(num_cs):
4277 c = d.constructors[j]
4278 cname = to_symbol(c[0], ctx)
4279 rname = to_symbol(c[1], ctx)
4282 fnames = (Symbol * num_fs)()
4283 sorts = (Sort * num_fs)()
4284 refs = (ctypes.c_uint * num_fs)()
4285 for k in range(num_fs):
4288 fnames[k] = to_symbol(fname, ctx)
4289 if isinstance(ftype, Datatype):
4291 _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
4293 refs[k] = ds.index(ftype)
4296 _z3_assert(is_sort(ftype), "Z3 sort expected")
4297 sorts[k] = ftype.ast
4299 cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
4300 to_delete.append(ScopedConstructor(cs[j], ctx))
4301 clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
4302 to_delete.append(ScopedConstructorList(clists[i], ctx))
4303 Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
4305 ## Create a field for every constructor, recognizer and accessor
4306 for i in range(num):
4307 dref = DatatypeSortRef(out[i], ctx)
4308 num_cs = dref.num_constructors()
4309 for j in range(num_cs):
4310 cref = dref.constructor(j)
4311 cref_name = cref.name()
4312 cref_arity = cref.arity()
4313 if cref.arity() == 0:
4315 setattr(dref, cref_name, cref)
4316 rref = dref.recognizer(j)
4317 setattr(dref, rref.name(), rref)
4318 for k in range(cref_arity):
4319 aref = dref.accessor(j, k)
4320 setattr(dref, aref.name(), aref)
4322 return tuple(result)
4324 class DatatypeSortRef(SortRef):
4325 """Datatype sorts.
"""
4326 def num_constructors(self):
4327 """Return the number of constructors
in the given Z3 datatype.
4330 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4331 >>> List.declare(
'nil')
4332 >>> List = List.create()
4334 >>> List.num_constructors()
4337 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
4339 def constructor(self, idx):
4340 """Return a constructor of the datatype `self`.
4343 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4344 >>> List.declare(
'nil')
4345 >>> List = List.create()
4347 >>> List.num_constructors()
4349 >>> List.constructor(0)
4351 >>> List.constructor(1)
4355 _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
4356 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
4358 def recognizer(self, idx):
4359 """In Z3, each constructor has an associated recognizer predicate.
4361 If the constructor
is named `name`, then the recognizer `is_name`.
4364 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4365 >>> List.declare(
'nil')
4366 >>> List = List.create()
4368 >>> List.num_constructors()
4370 >>> List.recognizer(0)
4372 >>> List.recognizer(1)
4374 >>>
simplify(List.is_nil(List.cons(10, List.nil)))
4376 >>>
simplify(List.is_cons(List.cons(10, List.nil)))
4378 >>> l =
Const(
'l', List)
4383 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
4384 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
4386 def accessor(self, i, j):
4387 """In Z3, each constructor has 0
or more accessor. The number of accessors
is equal to the arity of the constructor.
4390 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4391 >>> List.declare(
'nil')
4392 >>> List = List.create()
4393 >>> List.num_constructors()
4395 >>> List.constructor(0)
4397 >>> num_accs = List.constructor(0).arity()
4400 >>> List.accessor(0, 0)
4402 >>> List.accessor(0, 1)
4404 >>> List.constructor(1)
4406 >>> num_accs = List.constructor(1).arity()
4411 _z3_assert(i < self.num_constructors(), "Invalid constructor index")
4412 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
4413 return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
4415 class DatatypeRef(ExprRef):
4416 """Datatype expressions.
"""
4418 """Return the datatype sort of the datatype expression `self`.
"""
4419 return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
4421 def EnumSort(name, values, ctx=None):
4422 """Return a new enumeration sort named `name` containing the given values.
4424 The result
is a pair (sort, list of constants).
4426 >>> Color, (red, green, blue) =
EnumSort(
'Color', [
'red',
'green',
'blue'])
4429 _z3_assert(isinstance(name, str), "Name must be a string")
4430 _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings")
4431 _z3_assert(len(values) > 0, "At least one value expected")
4434 _val_names = (Symbol * num)()
4435 for i in range(num):
4436 _val_names[i] = to_symbol(values[i])
4437 _values = (FuncDecl * num)()
4438 _testers = (FuncDecl * num)()
4439 name = to_symbol(name)
4440 S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
4442 for i in range(num):
4443 V.append(FuncDeclRef(_values[i], ctx))
4444 V = [a() for a in V]
4447 #########################################
4451 #########################################
4454 """Set of parameters used to configure Solvers, Tactics
and Simplifiers
in Z3.
4456 Consider using the function `args2params` to create instances of this object.
4458 def __init__(self, ctx=None):
4459 self.ctx = _get_ctx(ctx)
4460 self.params = Z3_mk_params(self.ctx.ref())
4461 Z3_params_inc_ref(self.ctx.ref(), self.params)
4464 Z3_params_dec_ref(self.ctx.ref(), self.params)
4466 def set(self, name, val):
4467 """Set parameter name with value val.
"""
4469 _z3_assert(isinstance(name, str), "parameter name must be a string")
4470 name_sym = to_symbol(name, self.ctx)
4471 if isinstance(val, bool):
4472 Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val)
4473 elif isinstance(val, int):
4474 Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val)
4475 elif isinstance(val, float):
4476 Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val)
4477 elif isinstance(val, str):
4478 Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx))
4481 _z3_assert(False, "invalid parameter value")
4484 return Z3_params_to_string(self.ctx.ref(), self.params)
4486 def validate(self, ds):
4487 _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected")
4488 Z3_params_validate(self.ctx.ref(), self.params, ds.descr)
4490 def args2params(arguments, keywords, ctx=None):
4491 """Convert python arguments into a Z3_params object.
4492 A
':' is added to the keywords,
and '_' is replaced with
'-'
4494 >>>
args2params([
'model',
True,
'relevancy', 2], {
'elim_and' :
True})
4495 (params model true relevancy 2 elim_and true)
4498 _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
4512 class ParamDescrsRef:
4513 """Set of parameter descriptions
for Solvers, Tactics
and Simplifiers
in Z3.
4515 def __init__(self, descr, ctx=None):
4516 _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected")
4517 self.ctx = _get_ctx(ctx)
4519 Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr)
4522 Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
4525 """Return the size of
in the parameter description `self`.
4527 return int(Z3_param_descrs_size(self.ctx.ref(), self.descr))
4530 """Return the size of
in the parameter description `self`.
4534 def get_name(self, i):
4535 """Return the i-th parameter name
in the parameter description `self`.
4537 return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i))
4539 def get_kind(self, n):
4540 """Return the kind of the parameter named `n`.
4542 return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
4544 def __getitem__(self, arg):
4546 return self.get_name(arg)
4548 return self.get_kind(arg)
4551 return Z3_param_descrs_to_string(self.ctx.ref(), self.descr)
4553 #########################################
4557 #########################################
4559 class Goal(Z3PPObject):
4560 """Goal
is a collection of constraints we want to find a solution
or show to be unsatisfiable (infeasible).
4562 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
4563 A goal has a solution
if one of its subgoals has a solution.
4564 A goal
is unsatisfiable
if all subgoals are unsatisfiable.
4567 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
4569 _z3_assert(goal == None or ctx != None, "If goal is different from None, then ctx must be also different from None")
4570 self.ctx = _get_ctx(ctx)
4572 if self.goal == None:
4573 self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
4574 Z3_goal_inc_ref(self.ctx.ref(), self.goal)
4577 if self.goal != None:
4578 Z3_goal_dec_ref(self.ctx.ref(), self.goal)
4581 """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
4583 >>> x, y =
Ints(
'x y')
4585 >>> g.add(x == 0, y >= x + 1)
4588 >>> r =
Then(
'simplify',
'solve-eqs')(g)
4595 return int(Z3_goal_depth(self.ctx.ref(), self.goal))
4597 def inconsistent(self):
4598 """Return `
True`
if `self` contains the `
False` constraints.
4600 >>> x, y =
Ints(
'x y')
4602 >>> g.inconsistent()
4604 >>> g.add(x == 0, x == 1)
4607 >>> g.inconsistent()
4609 >>> g2 =
Tactic(
'propagate-values')(g)[0]
4610 >>> g2.inconsistent()
4613 return Z3_goal_inconsistent(self.ctx.ref(), self.goal)
4616 """Return the precision (under-approximation, over-approximation,
or precise) of the goal `self`.
4619 >>> g.prec() == Z3_GOAL_PRECISE
4621 >>> x, y =
Ints(
'x y')
4622 >>> g.add(x == y + 1)
4623 >>> g.prec() == Z3_GOAL_PRECISE
4625 >>> t =
With(
Tactic(
'add-bounds'), add_bound_lower=0, add_bound_upper=10)
4628 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
4629 >>> g2.prec() == Z3_GOAL_PRECISE
4631 >>> g2.prec() == Z3_GOAL_UNDER
4634 return Z3_goal_precision(self.ctx.ref(), self.goal)
4636 def precision(self):
4637 """Alias
for `
prec()`.
4640 >>> g.precision() == Z3_GOAL_PRECISE
4646 """Return the number of constraints
in the goal `self`.
4651 >>> x, y =
Ints(
'x y')
4652 >>> g.add(x == 0, y > x)
4656 return int(Z3_goal_size(self.ctx.ref(), self.goal))
4659 """Return the number of constraints
in the goal `self`.
4664 >>> x, y =
Ints(
'x y')
4665 >>> g.add(x == 0, y > x)
4672 """Return a constraint
in the goal `self`.
4675 >>> x, y =
Ints(
'x y')
4676 >>> g.add(x == 0, y > x)
4682 return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx)
4684 def __getitem__(self, arg):
4685 """Return a constraint
in the goal `self`.
4688 >>> x, y =
Ints(
'x y')
4689 >>> g.add(x == 0, y > x)
4695 if arg >= len(self):
4697 return self.get(arg)
4699 def assert_exprs(self, *args):
4700 """Assert constraints into the goal.
4704 >>> g.assert_exprs(x > 0, x < 2)
4708 args = _get_args(args)
4709 s = BoolSort(self.ctx)
4712 Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast())
4714 def append(self, *args):
4719 >>> g.append(x > 0, x < 2)
4723 self.assert_exprs(*args)
4725 def insert(self, *args):
4730 >>> g.insert(x > 0, x < 2)
4734 self.assert_exprs(*args)
4736 def add(self, *args):
4741 >>> g.add(x > 0, x < 2)
4745 self.assert_exprs(*args)
4748 return obj_to_string(self)
4751 """Return a textual representation of the s-expression representing the goal.
"""
4752 return Z3_goal_to_string(self.ctx.ref(), self.goal)
4754 def translate(self, target):
4755 """Copy goal `self` to context `target`.
4763 >>> g2 = g.translate(c2)
4774 _z3_assert(isinstance(target, Context), "target must be a context")
4775 return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target)
4777 def simplify(self, *arguments, **keywords):
4778 """Return a new simplified goal.
4780 This method
is essentially invoking the simplify tactic.
4784 >>> g.add(x + 1 >= 2)
4787 >>> g2 = g.simplify()
4794 t = Tactic('simplify')
4795 return t.apply(self, *arguments, **keywords)[0]
4798 """Return goal `self`
as a single Z3 expression.
4813 return BoolVal(True, self.ctx)
4817 return And([ self.get(i) for i in range(len(self)) ])
4819 #########################################
4823 #########################################
4824 class AstVector(Z3PPObject):
4825 """A collection (vector) of ASTs.
"""
4827 def __init__(self, v=None, ctx=None):
4830 self.ctx = _get_ctx(ctx)
4831 self.vector = Z3_mk_ast_vector(self.ctx.ref())
4836 Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
4839 if self.vector != None:
4840 Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
4843 """Return the size of the vector `self`.
4848 >>> A.push(
Int(
'x'))
4849 >>> A.push(
Int(
'x'))
4853 return int(Z3_ast_vector_size(self.ctx.ref(), self.vector))
4855 def __getitem__(self, i):
4856 """Return the AST at position `i`.
4859 >>> A.push(
Int(
'x') + 1)
4860 >>> A.push(
Int(
'y'))
4866 if i >= self.__len__():
4868 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
4870 def __setitem__(self, i, v):
4871 """Update AST at position `i`.
4874 >>> A.push(
Int(
'x') + 1)
4875 >>> A.push(
Int(
'y'))
4882 if i >= self.__len__():
4884 Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast())
4887 """Add `v`
in the end of the vector.
4892 >>> A.push(
Int(
'x'))
4896 Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast())
4898 def resize(self, sz):
4899 """Resize the vector to `sz` elements.
4905 >>>
for i
in range(10): A[i] =
Int(
'x')
4909 Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz)
4911 def __contains__(self, item):
4912 """Return `
True`
if the vector contains `item`.
4934 def translate(self, other_ctx):
4935 """Copy vector `self` to context `other_ctx`.
4941 >>> B = A.translate(c2)
4945 return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx)
4948 return obj_to_string(self)
4951 """Return a textual representation of the s-expression representing the vector.
"""
4952 return Z3_ast_vector_to_string(self.ctx.ref(), self.vector)
4954 #########################################
4958 #########################################
4960 """A mapping
from ASTs to ASTs.
"""
4962 def __init__(self, m=None, ctx=None):
4965 self.ctx = _get_ctx(ctx)
4966 self.map = Z3_mk_ast_map(self.ctx.ref())
4971 Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
4974 if self.map != None:
4975 Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
4978 """Return the size of the map.
4988 return int(Z3_ast_map_size(self.ctx.ref(), self.map))
4990 def __contains__(self, key):
4991 """Return `
True`
if the map contains key `key`.
5001 return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast())
5003 def __getitem__(self, key):
5004 """Retrieve the value associated with key `key`.
5012 return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx)
5014 def __setitem__(self, k, v):
5015 """Add/Update key `k` with value `v`.
5028 Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast())
5031 return Z3_ast_map_to_string(self.ctx.ref(), self.map)
5034 """Remove the entry associated with key `k`.
5045 Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast())
5048 """Remove all entries
from the map.
5060 Z3_ast_map_reset(self.ctx.ref(), self.map)
5063 """Return an AstVector containing all keys
in the map.
5072 return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx)
5074 #########################################
5078 #########################################
5081 """Store the value of the interpretation of a function
in a particular point.
"""
5083 def __init__(self, entry, ctx):
5086 Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
5089 Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
5092 """Return the number of arguments
in the given entry.
5096 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5101 >>> f_i.num_entries()
5103 >>> e = f_i.entry(0)
5107 return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry))
5109 def arg_value(self, idx):
5110 """Return the value of argument `idx`.
5114 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5119 >>> f_i.num_entries()
5121 >>> e = f_i.entry(0)
5132 ...
except IndexError:
5133 ... print(
"index error")
5136 if idx >= self.num_args():
5138 return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx)
5141 """Return the value of the function at point `self`.
5145 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5150 >>> f_i.num_entries()
5152 >>> e = f_i.entry(0)
5160 return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx)
5163 """Return entry `self`
as a Python list.
5166 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5171 >>> f_i.num_entries()
5173 >>> e = f_i.entry(0)
5177 args = [ self.arg_value(i) for i in range(self.num_args())]
5178 args.append(self.value())
5182 return repr(self.as_list())
5184 class FuncInterp(Z3PPObject):
5185 """Stores the interpretation of a function
in a Z3 model.
"""
5187 def __init__(self, f, ctx):
5191 Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
5195 Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
5197 def else_value(self):
5199 Return the `
else` value
for a function interpretation.
5200 Return
None if Z3 did
not specify the `
else` value
for
5205 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5210 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5214 r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
5216 return _to_expr_ref(r, self.ctx)
5220 def num_entries(self):
5221 """Return the number of entries/points
in the function interpretation `self`.
5225 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5230 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5234 return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f))
5237 """Return the number of arguments
for each entry
in the function interpretation `self`.
5241 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5248 return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f))
5250 def entry(self, idx):
5251 """Return an entry at position `idx < self.
num_entries()`
in the function interpretation `self`.
5255 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5260 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5270 if idx >= self.num_entries():
5272 return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx)
5275 """Return the function interpretation
as a Python list.
5278 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5283 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5285 [[0, 1], [1, 1], [2, 0], 1]
5287 r = [ self.entry(i).as_list() for i in range(self.num_entries())]
5288 r.append(self.else_value())
5292 return obj_to_string(self)
5294 class ModelRef(Z3PPObject):
5295 """Model/Solution of a satisfiability problem (aka system of constraints).
"""
5297 def __init__(self, m, ctx):
5301 Z3_model_inc_ref(self.ctx.ref(), self.model)
5304 Z3_model_dec_ref(self.ctx.ref(), self.model)
5307 return obj_to_string(self)
5310 """Return a textual representation of the s-expression representing the model.
"""
5311 return Z3_model_to_string(self.ctx.ref(), self.model)
5313 def eval(self, t, model_completion=False):
5314 """Evaluate the expression `t`
in the model `self`. If `model_completion`
is enabled, then a default interpretation
is automatically added
for symbols that do
not have an interpretation
in the model `self`.
5318 >>> s.add(x > 0, x < 2)
5331 >>> m.eval(y, model_completion=
True)
5338 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
5339 return _to_expr_ref(r[0], self.ctx)
5340 raise Z3Exception("failed to evaluate expression in the model")
5342 def evaluate(self, t, model_completion=False):
5343 """Alias
for `eval`.
5347 >>> s.add(x > 0, x < 2)
5351 >>> m.evaluate(x + 1)
5353 >>> m.evaluate(x == 1)
5356 >>> m.evaluate(y + x)
5360 >>> m.evaluate(y, model_completion=
True)
5363 >>> m.evaluate(y + x)
5366 return self.eval(t, model_completion)
5369 """Return the number of constant
and function declarations
in the model `self`.
5374 >>> s.add(x > 0, f(x) != x)
5381 return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model))
5383 def get_interp(self, decl):
5384 """Return the interpretation
for a given declaration
or constant.
5389 >>> s.add(x > 0, x < 2, f(x) == 0)
5399 _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected")
5403 if decl.arity() == 0:
5404 r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
5406 return self.get_interp(get_as_array_func(r))
5410 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
5414 def num_sorts(self):
5415 """Return the number of unintepreted sorts that contain an interpretation
in the model `self`.
5418 >>> a, b =
Consts(
'a b', A)
5427 return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model))
5429 def get_sort(self, idx):
5430 """Return the unintepreted sort at position `idx` < self.
num_sorts().
5434 >>> a1, a2 =
Consts(
'a1 a2', A)
5435 >>> b1, b2 =
Consts(
'b1 b2', B)
5437 >>> s.add(a1 != a2, b1 != b2)
5448 if idx >= self.num_sorts():
5450 return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx)
5453 """Return all uninterpreted sorts that have an interpretation
in the model `self`.
5457 >>> a1, a2 =
Consts(
'a1 a2', A)
5458 >>> b1, b2 =
Consts(
'b1 b2', B)
5460 >>> s.add(a1 != a2, b1 != b2)
5467 return [ self.get_sort(i) for i in range(self.num_sorts()) ]
5469 def get_universe(self, s):
5470 """Return the intepretation
for the uninterpreted sort `s`
in the model `self`.
5473 >>> a, b =
Consts(
'a b', A)
5479 >>> m.get_universe(A)
5483 _z3_assert(isinstance(s, SortRef), "Z3 sort expected")
5485 return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx)
5489 def __getitem__(self, idx):
5490 """If `idx`
is an integer, then the declaration at position `idx`
in the model `self`
is returned. If `idx`
is a declaration, then the actual interpreation
is returned.
5492 The elements can be retrieved using position
or the actual declaration.
5497 >>> s.add(x > 0, x < 2, f(x) == 0)
5511 >>>
for d
in m: print(
"%s -> %s" % (d, m[d]))
5513 f -> [1 -> 0,
else -> 0]
5515 if isinstance(idx, int):
5516 if idx >= len(self):
5518 num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
5519 if (idx < num_consts):
5520 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx)
5522 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx)
5523 if isinstance(idx, FuncDeclRef):
5524 return self.get_interp(idx)
5526 return self.get_interp(idx.decl())
5527 if isinstance(idx, SortRef):
5528 return self.get_universe(idx)
5530 _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected")
5534 """Return a list with all symbols that have an interpreation
in the model `self`.
5538 >>> s.add(x > 0, x < 2, f(x) == 0)
5546 for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)):
5547 r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx))
5548 for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)):
5549 r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
5553 """Return true
if n
is a Z3 expression of the form (_
as-array f).
"""
5554 return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
5556 def get_as_array_func(n):
5557 """Return the function declaration f associated with a Z3 expression of the form (_
as-array f).
"""
5559 _z3_assert(is_as_array(n), "as-array Z3 expression expected.")
5560 return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
5562 #########################################
5566 #########################################
5568 """Statistics
for `Solver.check()`.
"""
5570 def __init__(self, stats, ctx):
5573 Z3_stats_inc_ref(self.ctx.ref(), self.stats)
5576 Z3_stats_dec_ref(self.ctx.ref(), self.stats)
5582 out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
5585 out.write(u('<tr style="background-color:#CFCFCF">'))
5588 out.write(u('<tr>'))
5590 out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
5591 out.write(u('</table>'))
5592 return out.getvalue()
5594 return Z3_stats_to_string(self.ctx.ref(), self.stats)
5597 """Return the number of statistical counters.
5600 >>> s =
Then(
'simplify',
'nlsat').solver()
5604 >>> st = s.statistics()
5608 return int(Z3_stats_size(self.ctx.ref(), self.stats))
5610 def __getitem__(self, idx):
5611 """Return the value of statistical counter at position `idx`. The result
is a pair (key, value).
5614 >>> s =
Then(
'simplify',
'nlsat').solver()
5618 >>> st = s.statistics()
5622 (
'nlsat propagations', 2)
5626 if idx >= len(self):
5628 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5629 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5631 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5632 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val)
5635 """Return the list of statistical counters.
5638 >>> s =
Then(
'simplify',
'nlsat').solver()
5642 >>> st = s.statistics()
5644 [
'nlsat propagations',
'nlsat stages']
5646 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
5648 def get_key_value(self, key):
5649 """Return the value of a particular statistical counter.
5652 >>> s =
Then(
'simplify',
'nlsat').solver()
5656 >>> st = s.statistics()
5657 >>> st.get_key_value(
'nlsat propagations')
5660 for idx in range(len(self)):
5661 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx):
5662 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx):
5663 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx))
5665 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx)
5666 raise Z3Exception("unknown key")
5668 def __getattr__(self, name):
5669 """Access the value of statistical using attributes.
5671 Remark: to access a counter containing blank spaces (e.g.,
'nlsat propagations'),
5672 we should use
'_' (e.g.,
'nlsat_propagations').
5675 >>> s =
Then(
'simplify',
'nlsat').solver()
5679 >>> st = s.statistics()
5681 [
'nlsat propagations',
'nlsat stages']
5682 >>> st.nlsat_propagations
5687 key = name.replace('_', ' ')
5689 return self.get_key_value(key)
5691 raise AttributeError
5693 #########################################
5697 #########################################
5698 class CheckSatResult:
5699 """Represents the result of a satisfiability check: sat, unsat, unknown.
5705 >>> isinstance(r, CheckSatResult)
5709 def __init__(self, r):
5712 def __eq__(self, other):
5713 return isinstance(other, CheckSatResult) and self.r == other.r
5715 def __ne__(self, other):
5716 return not self.__eq__(other)
5720 if self.r == Z3_L_TRUE:
5722 elif self.r == Z3_L_FALSE:
5723 return "<b>unsat</b>"
5725 return "<b>unknown</b>"
5727 if self.r == Z3_L_TRUE:
5729 elif self.r == Z3_L_FALSE:
5734 sat = CheckSatResult(Z3_L_TRUE)
5735 unsat = CheckSatResult(Z3_L_FALSE)
5736 unknown = CheckSatResult(Z3_L_UNDEF)
5738 class Solver(Z3PPObject):
5739 """Solver API provides methods
for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.
"""
5741 def __init__(self, solver=None, ctx=None):
5742 assert solver == None or ctx != None
5743 self.ctx = _get_ctx(ctx)
5746 self.solver = Z3_mk_solver(self.ctx.ref())
5748 self.solver = solver
5749 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
5752 if self.solver != None:
5753 Z3_solver_dec_ref(self.ctx.ref(), self.solver)
5755 def set(self, *args, **keys):
5756 """Set a configuration option. The method `
help()`
return a string containing all available options.
5760 >>> s.set(mbqi=
True)
5761 >>> s.set(
'MBQI',
True)
5762 >>> s.set(
':mbqi',
True)
5764 p = args2params(args, keys, self.ctx)
5765 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
5768 """Create a backtracking point.
5787 Z3_solver_push(self.ctx.ref(), self.solver)
5789 def pop(self, num=1):
5790 """Backtrack \c num backtracking points.
5809 Z3_solver_pop(self.ctx.ref(), self.solver, num)
5812 """Remove all asserted constraints
and backtracking points created using `
push()`.
5823 Z3_solver_reset(self.ctx.ref(), self.solver)
5825 def assert_exprs(self, *args):
5826 """Assert constraints into the solver.
5830 >>> s.assert_exprs(x > 0, x < 2)
5834 args = _get_args(args)
5835 s = BoolSort(self.ctx)
5837 if isinstance(arg, Goal) or isinstance(arg, AstVector):
5839 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
5842 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
5844 def add(self, *args):
5845 """Assert constraints into the solver.
5849 >>> s.add(x > 0, x < 2)
5853 self.assert_exprs(*args)
5855 def append(self, *args):
5856 """Assert constraints into the solver.
5860 >>> s.append(x > 0, x < 2)
5864 self.assert_exprs(*args)
5866 def insert(self, *args):
5867 """Assert constraints into the solver.
5871 >>> s.insert(x > 0, x < 2)
5875 self.assert_exprs(*args)
5877 def assert_and_track(self, a, p):
5878 """Assert constraint `a`
and track it
in the unsat core using the Boolean constant `p`.
5880 If `p`
is a string, it will be automatically converted into a Boolean constant.
5885 >>> s.set(unsat_core=
True)
5886 >>> s.assert_and_track(x > 0,
'p1')
5887 >>> s.assert_and_track(x != 1,
'p2')
5888 >>> s.assert_and_track(x < 0, p3)
5889 >>> print(s.check())
5891 >>> c = s.unsat_core()
5901 if isinstance(p, str):
5902 p = Bool(p, self.ctx)
5903 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
5904 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
5905 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
5907 def check(self, *assumptions):
5908 """Check whether the assertions
in the given solver plus the optional assumptions are consistent
or not.
5914 >>> s.add(x > 0, x < 2)
5923 >>> s.add(2**x == 4)
5927 assumptions = _get_args(assumptions)
5928 num = len(assumptions)
5929 _assumptions = (Ast * num)()
5930 for i in range(num):
5931 _assumptions[i] = assumptions[i].as_ast()
5932 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
5933 return CheckSatResult(r)
5936 """Return a model
for the last `
check()`.
5938 This function raises an exception
if
5939 a model
is not available (e.g., last `
check()` returned unsat).
5943 >>> s.add(a + 2 == 0)
5950 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
5952 raise Z3Exception("model is not available")
5954 def unsat_core(self):
5955 """Return a subset (
as an AST vector) of the assumptions provided to the last
check().
5957 These are the assumptions Z3 used
in the unsatisfiability proof.
5958 Assumptions are available
in Z3. They are used to extract unsatisfiable cores.
5959 They may be also used to
"retract" assumptions. Note that, assumptions are
not really
5960 "soft constraints", but they can be used to implement them.
5962 >>> p1, p2, p3 =
Bools(
'p1 p2 p3')
5963 >>> x, y =
Ints(
'x y')
5968 >>> s.add(
Implies(p3, y > -3))
5969 >>> s.check(p1, p2, p3)
5971 >>> core = s.unsat_core()
5984 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
5987 """Return a proof
for the last `
check()`. Proof construction must be enabled.
"""
5988 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
5990 def assertions(self):
5991 """Return an AST vector containing all added constraints.
6002 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
6004 def statistics(self):
6005 """Return statistics
for the last `
check()`.
6012 >>> st = s.statistics()
6013 >>> st.get_key_value(
'final checks')
6020 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
6022 def reason_unknown(self):
6023 """Return a string describing why the last `
check()` returned `unknown`.
6027 >>> s.add(2**x == 4)
6030 >>> s.reason_unknown()
6031 '(incomplete (theory arithmetic))'
6033 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
6036 """Display a string describing all available options.
"""
6037 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
6039 def param_descrs(self):
6040 """Return the parameter description set.
"""
6041 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
6044 """Return a formatted string with all added constraints.
"""
6045 return obj_to_string(self)
6048 """Return a formatted string (
in Lisp-like format) with all added constraints. We say the string
is in s-expression format.
6056 return Z3_solver_to_string(self.ctx.ref(), self.solver)
6059 """return SMTLIB2 formatted benchmark
for solver
's assertions"""
6066 for i
in range(sz1):
6067 v[i] = es[i].as_ast()
6069 e = es[sz1].as_ast()
6077 """Create a solver customized for the given logic.
6079 The parameter `logic` is a string. It should be contains
6080 the name of a SMT-LIB logic.
6081 See http://www.smtlib.org/ for the name of all available logics.
6083 >>> s = SolverFor("QF_LIA")
6097 """Return a simple general purpose solver with limited amount of preprocessing.
6099 >>> s = SimpleSolver()
6115 """Fixedpoint API provides methods for solving with recursive predicates"""
6118 assert fixedpoint ==
None or ctx !=
None
6121 if fixedpoint ==
None:
6133 """Set a configuration option. The method `help()` return a string containing all available options.
6139 """Display a string describing all available options."""
6143 """Return the parameter description set."""
6147 """Assert constraints as background axioms for the fixedpoint solver."""
6148 args = _get_args(args)
6151 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
6161 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6165 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6169 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6173 """Assert rules defining recursive predicates to the fixedpoint solver.
6176 >>> s = Fixedpoint()
6177 >>> s.register_relation(a.decl())
6178 >>> s.register_relation(b.decl())
6191 body = _get_args(body)
6195 def rule(self, head, body = None, name = None):
6196 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6200 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6204 """Query the fixedpoint engine whether formula is derivable.
6205 You can also pass an tuple or list of recursive predicates.
6207 query = _get_args(query)
6209 if sz >= 1
and isinstance(query[0], FuncDeclRef):
6210 _decls = (FuncDecl * sz)()
6220 query =
And(query, self.
ctx)
6221 query = self.
abstract(query,
False)
6226 """create a backtracking point for added rules, facts and assertions"""
6230 """restore to previously created backtracking point"""
6238 body = _get_args(body)
6243 """Retrieve answer from last query call."""
6245 return _to_expr_ref(r, self.
ctx)
6248 """Retrieve number of levels used for predicate in PDR engine"""
6252 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
6254 return _to_expr_ref(r, self.
ctx)
6257 """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
6261 """Register relation as recursive"""
6262 relations = _get_args(relations)
6267 """Control how relation is represented"""
6268 representations = _get_args(representations)
6269 representations = [
to_symbol(s)
for s
in representations]
6270 sz = len(representations)
6271 args = (Symbol * sz)()
6273 args[i] = representations[i]
6277 """Parse rules and queries from a string"""
6281 """Parse rules and queries from a file"""
6285 """retrieve rules that have been added to fixedpoint context"""
6289 """retrieve assertions that have been added to fixedpoint context"""
6293 """Return a formatted string with all added rules and constraints."""
6297 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6302 """Return a formatted string (in Lisp-like format) with all added constraints.
6303 We say the string is in s-expression format.
6304 Include also queries.
6306 args, len = _to_ast_array(queries)
6310 """Return statistics for the last `query()`.
6315 """Return a string describing why the last `query()` returned `unknown`.
6320 """Add variable or several variables.
6321 The added variable or variables will be bound in the rules
6324 vars = _get_args(vars)
6342 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters."""
6353 """Return the number of subgoals in `self`.
6355 >>> a, b = Ints('a b')
6357 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
6358 >>> t = Tactic('split-clause')
6362 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'))
6365 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values'))
6372 """Return one of the subgoals stored in ApplyResult object `self`.
6374 >>> a, b = Ints('a b')
6376 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
6377 >>> t = Tactic('split-clause')
6380 [a == 0, Or(b == 0, b == 1), a > b]
6382 [a == 1, Or(b == 0, b == 1), a > b]
6384 if idx >= len(self):
6389 return obj_to_string(self)
6392 """Return a textual representation of the s-expression representing the set of subgoals in `self`."""
6396 """Convert a model for a subgoal into a model for the original goal.
6398 >>> a, b = Ints('a b')
6400 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
6401 >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs'))
6404 [Or(b == 0, b == 1), Not(0 <= b)]
6406 [Or(b == 0, b == 1), Not(1 <= b)]
6407 >>> # Remark: the subgoal r[0] is unsatisfiable
6408 >>> # Creating a solver for solving the second subgoal
6415 >>> # Model s.model() does not assign a value to `a`
6416 >>> # It is a model for subgoal `r[1]`, but not for goal `g`
6417 >>> # The method convert_model creates a model for `g` from a model for `r[1]`.
6418 >>> r.convert_model(s.model(), 1)
6422 _z3_assert(idx < len(self),
"index out of bounds")
6423 _z3_assert(isinstance(model, ModelRef),
"Z3 Model expected")
6427 """Return a Z3 expression consisting of all subgoals.
6432 >>> g.add(Or(x == 2, x == 3))
6433 >>> r = Tactic('simplify')(g)
6435 [[Not(x <= 1), Or(x == 2, x == 3)]]
6437 And(Not(x <= 1), Or(x == 2, x == 3))
6438 >>> r = Tactic('split-clause')(g)
6440 [[x > 1, x == 2], [x > 1, x == 3]]
6442 Or(And(x > 1, x == 2), And(x > 1, x == 3))
6450 return Or([ self[i].
as_expr()
for i
in range(len(self)) ])
6458 """Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver().
6460 Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond().
6465 if isinstance(tactic, TacticObj):
6469 _z3_assert(isinstance(tactic, str),
"tactic name expected")
6473 raise Z3Exception(
"unknown tactic '%s'" % tactic)
6481 """Create a solver using the tactic `self`.
6483 The solver supports the methods `push()` and `pop()`, but it
6484 will always solve each `check()` from scratch.
6486 >>> t = Then('simplify', 'nlsat')
6489 >>> s.add(x**2 == 2, x > 0)
6497 def apply(self, goal, *arguments, **keywords):
6498 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
6500 >>> x, y = Ints('x y')
6501 >>> t = Tactic('solve-eqs')
6502 >>> t.apply(And(x == 0, y >= x + 1))
6506 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expressions expected")
6507 goal = _to_goal(goal)
6508 if len(arguments) > 0
or len(keywords) > 0:
6515 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
6517 >>> x, y = Ints('x y')
6518 >>> t = Tactic('solve-eqs')
6519 >>> t(And(x == 0, y >= x + 1))
6522 return self.
apply(goal, *arguments, **keywords)
6525 """Display a string containing a description of the available options for the `self` tactic."""
6529 """Return the parameter description set."""
6533 if isinstance(a, BoolRef):
6534 goal =
Goal(ctx = a.ctx)
6540 def _to_tactic(t, ctx=None):
6541 if isinstance(t, Tactic):
6546 def _and_then(t1, t2, ctx=None):
6547 t1 = _to_tactic(t1, ctx)
6548 t2 = _to_tactic(t2, ctx)
6550 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
6553 def _or_else(t1, t2, ctx=None):
6554 t1 = _to_tactic(t1, ctx)
6555 t2 = _to_tactic(t2, ctx)
6557 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
6561 """Return a tactic that applies the tactics in `*ts` in sequence.
6563 >>> x, y = Ints('x y')
6564 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
6565 >>> t(And(x == 0, y > x + 1))
6567 >>> t(And(x == 0, y > x + 1)).as_expr()
6571 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
6572 ctx = ks.get(
'ctx',
None)
6575 for i
in range(num - 1):
6576 r = _and_then(r, ts[i+1], ctx)
6580 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
6582 >>> x, y = Ints('x y')
6583 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
6584 >>> t(And(x == 0, y > x + 1))
6586 >>> t(And(x == 0, y > x + 1)).as_expr()
6592 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
6595 >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
6596 >>> # Tactic split-clause fails if there is no clause in the given goal.
6599 >>> t(Or(x == 0, x == 1))
6600 [[x == 0], [x == 1]]
6603 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
6604 ctx = ks.get(
'ctx',
None)
6607 for i
in range(num - 1):
6608 r = _or_else(r, ts[i+1], ctx)
6612 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
6615 >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
6620 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
6621 ctx = _get_ctx(ks.get(
'ctx',
None))
6622 ts = [ _to_tactic(t, ctx)
for t
in ts ]
6624 _args = (TacticObj * sz)()
6626 _args[i] = ts[i].tactic
6630 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
6632 >>> x, y = Ints('x y')
6633 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
6634 >>> t(And(Or(x == 1, x == 2), y == x + 1))
6635 [[x == 1, y == 2], [x == 2, y == 3]]
6637 t1 = _to_tactic(t1, ctx)
6638 t2 = _to_tactic(t2, ctx)
6640 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
6644 """Alias for ParThen(t1, t2, ctx)."""
6648 """Return a tactic that applies tactic `t` using the given configuration options.
6650 >>> x, y = Ints('x y')
6651 >>> t = With(Tactic('simplify'), som=True)
6652 >>> t((x + 1)*(y + 2) == 0)
6653 [[2*x + y + x*y == -2]]
6655 ctx = keys.get(
'ctx',
None)
6656 t = _to_tactic(t, ctx)
6661 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
6663 >>> x, y = Ints('x y')
6664 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
6665 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
6667 >>> for subgoal in r: print(subgoal)
6668 [x == 0, y == 0, x > y]
6669 [x == 0, y == 1, x > y]
6670 [x == 1, y == 0, x > y]
6671 [x == 1, y == 1, x > y]
6672 >>> t = Then(t, Tactic('propagate-values'))
6676 t = _to_tactic(t, ctx)
6680 """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
6682 If `t` does not terminate in `ms` milliseconds, then it fails.
6684 t = _to_tactic(t, ctx)
6688 """Return a list of all available tactics in Z3.
6691 >>> l.count('simplify') == 1
6698 """Return a short description for the tactic named `name`.
6700 >>> d = tactic_description('simplify')
6706 """Display a (tabular) description of all available tactics in Z3."""
6709 print(
'<table border="1" cellpadding="2" cellspacing="0">')
6712 print(
'<tr style="background-color:#CFCFCF">')
6717 print(
'<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(
tactic_description(t), 40)))
6724 """Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used."""
6728 if isinstance(probe, ProbeObj):
6730 elif isinstance(probe, float):
6732 elif _is_int(probe):
6734 elif isinstance(probe, bool):
6741 _z3_assert(isinstance(probe, str),
"probe name expected")
6745 raise Z3Exception(
"unknown probe '%s'" % probe)
6749 if self.
probe !=
None:
6753 """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`.
6755 >>> p = Probe('size') < 10
6766 """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`.
6768 >>> p = Probe('size') > 10
6779 """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`.
6781 >>> p = Probe('size') <= 2
6792 """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`.
6794 >>> p = Probe('size') >= 2
6805 """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`.
6807 >>> p = Probe('size') == 2
6818 """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`.
6820 >>> p = Probe('size') != 2
6832 """Evaluate the probe `self` in the given goal.
6834 >>> p = Probe('size')
6844 >>> p = Probe('num-consts')
6847 >>> p = Probe('is-propositional')
6850 >>> p = Probe('is-qflia')
6855 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expression expected")
6856 goal = _to_goal(goal)
6860 """Return `True` if `p` is a Z3 probe.
6862 >>> is_probe(Int('x'))
6864 >>> is_probe(Probe('memory'))
6867 return isinstance(p, Probe)
6869 def _to_probe(p, ctx=None):
6873 return Probe(p, ctx)
6876 """Return a list of all available probes in Z3.
6879 >>> l.count('memory') == 1
6886 """Return a short description for the probe named `name`.
6888 >>> d = probe_description('memory')
6894 """Display a (tabular) description of all available probes in Z3."""
6897 print(
'<table border="1" cellpadding="2" cellspacing="0">')
6900 print(
'<tr style="background-color:#CFCFCF">')
6905 print(
'<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(
probe_description(p), 40)))
6911 def _probe_nary(f, args, ctx):
6913 _z3_assert(len(args) > 0,
"At least one argument expected")
6915 r = _to_probe(args[0], ctx)
6916 for i
in range(num - 1):
6917 r =
Probe(f(ctx.ref(), r.probe, _to_probe(args[i+1], ctx).probe), ctx)
6920 def _probe_and(args, ctx):
6921 return _probe_nary(Z3_probe_and, args, ctx)
6923 def _probe_or(args, ctx):
6924 return _probe_nary(Z3_probe_or, args, ctx)
6927 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
6929 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
6931 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
6932 >>> x, y = Ints('x y')
6938 >>> g.add(x == y + 1)
6940 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
6942 p = _to_probe(p, ctx)
6946 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
6948 >>> t = When(Probe('size') > 2, Tactic('simplify'))
6949 >>> x, y = Ints('x y')
6955 >>> g.add(x == y + 1)
6957 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
6959 p = _to_probe(p, ctx)
6960 t = _to_tactic(t, ctx)
6964 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
6966 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
6968 p = _to_probe(p, ctx)
6969 t1 = _to_tactic(t1, ctx)
6970 t2 = _to_tactic(t2, ctx)
6980 """Simplify the expression `a` using the given options.
6982 This function has many options. Use `help_simplify` to obtain the complete list.
6986 >>> simplify(x + 1 + y + x + 1)
6988 >>> simplify((x + 1)*(y + 1), som=True)
6990 >>> simplify(Distinct(x, y, 1), blast_distinct=True)
6991 And(Not(x == y), Not(x == 1), Not(y == 1))
6992 >>> simplify(And(x == 0, y == 1), elim_and=True)
6993 Not(Or(Not(x == 0), Not(y == 1)))
6996 _z3_assert(
is_expr(a),
"Z3 expression expected")
6997 if len(arguments) > 0
or len(keywords) > 0:
6999 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
7001 return _to_expr_ref(
Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
7004 """Return a string describing all options available for Z3 `simplify` procedure."""
7008 """Return the set of parameter descriptions for Z3 `simplify` procedure."""
7012 """Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to.
7016 >>> substitute(x + 1, (x, y + 1))
7018 >>> f = Function('f', IntSort(), IntSort())
7019 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
7022 if isinstance(m, tuple):
7024 if isinstance(m1, list):
7027 _z3_assert(
is_expr(t),
"Z3 expression expected")
7028 _z3_assert(all([isinstance(p, tuple)
and is_expr(p[0])
and is_expr(p[1])
and p[0].sort().
eq(p[1].sort())
for p
in m]),
"Z3 invalid substitution, expression pairs expected.")
7030 _from = (Ast * num)()
7032 for i
in range(num):
7033 _from[i] = m[i][0].as_ast()
7034 _to[i] = m[i][1].as_ast()
7035 return _to_expr_ref(
Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
7038 """Substitute the free variables in t with the expression in m.
7040 >>> v0 = Var(0, IntSort())
7041 >>> v1 = Var(1, IntSort())
7043 >>> f = Function('f', IntSort(), IntSort(), IntSort())
7044 >>> # replace v0 with x+1 and v1 with x
7045 >>> substitute_vars(f(v0, v1), x + 1, x)
7049 _z3_assert(
is_expr(t),
"Z3 expression expected")
7050 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
7053 for i
in range(num):
7054 _to[i] = m[i].as_ast()
7058 """Create the sum of the Z3 expressions.
7060 >>> a, b, c = Ints('a b c')
7065 >>> A = IntVector('a', 5)
7067 a__0 + a__1 + a__2 + a__3 + a__4
7069 args = _get_args(args)
7071 _z3_assert(len(args) > 0,
"Non empty list of arguments expected")
7072 ctx = _ctx_from_ast_arg_list(args)
7074 _z3_assert(ctx !=
None,
"At least one of the arguments must be a Z3 expression")
7075 args = _coerce_expr_list(args, ctx)
7077 return _reduce(
lambda a, b: a + b, args, 0)
7079 _args, sz = _to_ast_array(args)
7083 """Create the product of the Z3 expressions.
7085 >>> a, b, c = Ints('a b c')
7086 >>> Product(a, b, c)
7088 >>> Product([a, b, c])
7090 >>> A = IntVector('a', 5)
7092 a__0*a__1*a__2*a__3*a__4
7094 args = _get_args(args)
7096 _z3_assert(len(args) > 0,
"Non empty list of arguments expected")
7097 ctx = _ctx_from_ast_arg_list(args)
7099 _z3_assert(ctx !=
None,
"At least one of the arguments must be a Z3 expression")
7100 args = _coerce_expr_list(args, ctx)
7102 return _reduce(
lambda a, b: a * b, args, 1)
7104 _args, sz = _to_ast_array(args)
7108 """Solve the constraints `*args`.
7110 This is a simple function for creating demonstrations. It creates a solver,
7111 configure it using the options in `keywords`, adds the constraints
7112 in `args`, and invokes check.
7115 >>> solve(a > 0, a < 2)
7121 if keywords.get(
'show',
False):
7125 print(
"no solution")
7127 print(
"failed to solve")
7136 """Solve the constraints `*args` using solver `s`.
7138 This is a simple function for creating demonstrations. It is similar to `solve`,
7139 but it uses the given solver `s`.
7140 It configures solver `s` using the options in `keywords`, adds the constraints
7141 in `args`, and invokes check.
7144 _z3_assert(isinstance(s, Solver),
"Solver object expected")
7147 if keywords.get(
'show',
False):
7152 print(
"no solution")
7154 print(
"failed to solve")
7160 if keywords.get(
'show',
False):
7165 """Try to prove the given claim.
7167 This is a simple function for creating demonstrations. It tries to prove
7168 `claim` by showing the negation is unsatisfiable.
7170 >>> p, q = Bools('p q')
7171 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
7175 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
7179 if keywords.get(
'show',
False):
7185 print(
"failed to prove")
7188 print(
"counterexample")
7191 def _solve_html(*args, **keywords):
7192 """Version of funcion `solve` used in RiSE4Fun."""
7196 if keywords.get(
'show',
False):
7197 print(
"<b>Problem:</b>")
7201 print(
"<b>no solution</b>")
7203 print(
"<b>failed to solve</b>")
7209 if keywords.get(
'show',
False):
7210 print(
"<b>Solution:</b>")
7213 def _solve_using_html(s, *args, **keywords):
7214 """Version of funcion `solve_using` used in RiSE4Fun."""
7216 _z3_assert(isinstance(s, Solver),
"Solver object expected")
7219 if keywords.get(
'show',
False):
7220 print(
"<b>Problem:</b>")
7224 print(
"<b>no solution</b>")
7226 print(
"<b>failed to solve</b>")
7232 if keywords.get(
'show',
False):
7233 print(
"<b>Solution:</b>")
7236 def _prove_html(claim, **keywords):
7237 """Version of funcion `prove` used in RiSE4Fun."""
7239 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
7243 if keywords.get(
'show',
False):
7247 print(
"<b>proved</b>")
7249 print(
"<b>failed to prove</b>")
7252 print(
"<b>counterexample</b>")
7255 def _dict2sarray(sorts, ctx):
7257 _names = (Symbol * sz)()
7258 _sorts = (Sort * sz) ()
7263 _z3_assert(isinstance(k, str),
"String expected")
7264 _z3_assert(
is_sort(v),
"Z3 sort expected")
7268 return sz, _names, _sorts
7270 def _dict2darray(decls, ctx):
7272 _names = (Symbol * sz)()
7273 _decls = (FuncDecl * sz) ()
7278 _z3_assert(isinstance(k, str),
"String expected")
7282 _decls[i] = v.decl().ast
7286 return sz, _names, _decls
7289 """Parse a string in SMT 2.0 format using the given sorts and decls.
7291 The arguments sorts and decls are Python dictionaries used to initialize
7292 the symbol table used for the SMT 2.0 parser.
7294 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
7296 >>> x, y = Ints('x y')
7297 >>> f = Function('f', IntSort(), IntSort())
7298 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
7300 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
7304 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
7305 dsz, dnames, ddecls = _dict2darray(decls, ctx)
7306 return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
7308 def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
7309 """Parse a file
in SMT 2.0 format using the given sorts
and decls.
7314 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
7315 dsz, dnames, ddecls = _dict2darray(decls, ctx)
7316 return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
7318 def Interpolant(a,ctx=None):
7319 """Create an interpolation operator.
7321 The argument
is an interpolation pattern (see tree_interpolant).
7327 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
7330 return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)
7332 def tree_interpolant(pat,p=None,ctx=None):
7333 """Compute interpolant
for a tree of formulas.
7335 The input
is an interpolation pattern over a set of formulas C.
7336 The pattern pat
is a formula combining the formulas
in C using
7337 logical conjunction
and the
"interp" operator (see Interp). This
7338 interp operator
is logically the identity operator. It marks the
7339 sub-formulas of the pattern
for which interpolants should be
7340 computed. The interpolant
is a map sigma
from marked subformulas
7341 to formulas, such that,
for each marked subformula phi of pat
7342 (where phi sigma
is phi with sigma(psi) substituted
for each
7343 subformula psi of phi such that psi
in dom(sigma)):
7345 1) phi sigma implies sigma(phi),
and
7347 2) sigma(phi)
is in the common uninterpreted vocabulary between
7348 the formulas of C occurring
in phi
and those
not occurring
in
7351 and moreover pat sigma implies false. In the simplest case
7352 an interpolant
for the pattern
"(and (interp A) B)" maps A
7353 to an interpolant
for A /\ B.
7355 The
return value
is a vector of formulas representing sigma. This
7356 vector contains sigma(phi)
for each marked subformula of pat,
in
7357 pre-order traversal. This means that subformulas of phi occur before phi
7358 in the vector. Also, subformulas that occur multiply
in pat will
7359 occur multiply
in the result vector.
7361 If pat
is satisfiable, raises an object of
class ModelRef
7362 that represents a model of pat.
7364 If parameters p are supplied, these are used
in creating the
7365 solver that determines satisfiability.
7370 [
Not(x >= 0),
Not(y <= 2)]
7375 ...
except ModelRef
as m:
7377 (define-fun x () Int
7381 ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
7382 ptr = (AstVectorObj * 1)()
7383 mptr = (Model * 1)()
7386 res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
7387 if res == Z3_L_FALSE:
7388 return AstVector(ptr[0],ctx)
7389 raise ModelRef(mptr[0], ctx)
7391 def binary_interpolant(a,b,p=None,ctx=None):
7392 """Compute an interpolant
for a binary conjunction.
7394 If a & b
is unsatisfiable, returns an interpolant
for a & b.
7395 This
is a formula phi such that
7398 2) b implies
not phi
7399 3) All the uninterpreted symbols of phi occur
in both a
and b.
7401 If a & b
is satisfiable, raises an object of
class ModelRef
7402 that represents a model of a &b.
7404 If parameters p are supplied, these are used
in creating the
7405 solver that determines satisfiability.
7411 f = And(Interpolant(a),b)
7412 return tree_interpolant(f,p,ctx)[0]
7414 def sequence_interpolant(v,p=None,ctx=None):
7415 """Compute interpolant
for a sequence of formulas.
7417 If len(v) == N,
and if the conjunction of the formulas
in v
is
7418 unsatisfiable, the interpolant
is a sequence of formulas w
7419 such that len(w) = N-1
and v[0] implies w[0]
and for i
in 0..N-1:
7421 1) w[i] & v[i+1] implies w[i+1] (
or false
if i+1 = N)
7422 2) All uninterpreted symbols
in w[i] occur
in both v[0]..v[i]
7425 Requires len(v) >= 1.
7427 If a & b
is satisfiable, raises an object of
class ModelRef
7428 that represents a model of a & b.
7430 If parameters p are supplied, these are used
in creating the
7431 solver that determines satisfiability.
7436 [
Not(x >= 0),
Not(y >= 0)]
7439 for i in range(1,len(v)):
7440 f = And(Interpolant(f),v[i])
7441 return tree_interpolant(f,p,ctx)
7443 #########################################
7445 # Floating-Point Arithmetic
7447 #########################################
7450 # Global default rounding mode
7451 _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO
7452 _dflt_fpsort_ebits = 11
7453 _dflt_fpsort_sbits = 53
7455 def get_default_rounding_mode(ctx=None):
7456 """Retrieves the
global default rounding mode.
"""
7457 global _dflt_rounding_mode
7458 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
7460 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
7462 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
7464 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
7466 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
7469 def set_default_rounding_mode(rm, ctx=None):
7470 global _dflt_rounding_mode
7471 if is_fprm_value(rm):
7472 _dflt_rounding_mode = rm.decl().kind()
7474 _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO or
7475 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE or
7476 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE or
7477 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN or
7478 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
7479 "illegal rounding mode")
7480 _dflt_rounding_mode = rm
7482 def get_default_fp_sort(ctx=None):
7483 return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
7485 def set_default_fp_sort(ebits, sbits, ctx=None):
7486 global _dflt_fpsort_ebits
7487 global _dflt_fpsort_sbits
7488 _dflt_fpsort_ebits = ebits
7489 _dflt_fpsort_sbits = sbits
7491 def _dflt_rm(ctx=None):
7492 return get_default_rounding_mode(ctx)
7494 def _dflt_fps(ctx=None):
7495 return get_default_fp_sort(ctx)
7499 class FPSortRef(SortRef):
7500 """Floating-point sort.
"""
7503 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint sort `self`.
7508 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast))
7511 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint sort `self`.
7516 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast))
7518 def cast(self, val):
7519 """Try to cast `val`
as a Floating-point expression
7524 >>> b.cast(1.0).
sexpr()
7525 '(fp #b0 #x7f #b00000000000000000000000)'
7529 _z3_assert(self.ctx == val.ctx, "Context mismatch")
7532 return FPVal(val, None, self, self.ctx)
7535 def Float16(ctx=None):
7536 """Floating-point 16-bit (half) sort.
"""
7538 return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
7540 def FloatHalf(ctx=None):
7541 """Floating-point 16-bit (half) sort.
"""
7543 return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
7545 def Float32(ctx=None):
7546 """Floating-point 32-bit (single) sort.
"""
7548 return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
7550 def FloatSingle(ctx=None):
7551 """Floating-point 32-bit (single) sort.
"""
7553 return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
7555 def Float64(ctx=None):
7556 """Floating-point 64-bit (double) sort.
"""
7558 return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
7560 def FloatSingle(ctx=None):
7561 """Floating-point 64-bit (double) sort.
"""
7563 return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
7565 def Float128(ctx=None):
7566 """Floating-point 128-bit (quadruple) sort.
"""
7568 return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
7570 def FloatSingle(ctx=None):
7571 """Floating-point 128-bit (quadruple) sort.
"""
7573 return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
7575 class FPRMSortRef(SortRef):
7576 """"Floating-point rounding mode sort."""
7580 """Return True if `s` is a Z3 floating-point sort.
7587 return isinstance(s, FPSortRef)
7589 def is_fprm_sort(s):
7590 """Return
True if `s`
is a Z3 floating-point rounding mode sort.
7597 return isinstance(s, FPRMSortRef)
7601 class FPRef(ExprRef):
7602 """Floating-point expressions.
"""
7605 """Return the sort of the floating-point expression `self`.
7610 >>> x.sort() ==
FPSort(8, 24)
7613 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
7616 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
7621 return self.sort().ebits();
7624 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
7629 return self.sort().sbits();
7631 def as_string(self):
7632 """Return a Z3 floating point expression
as a Python string.
"""
7633 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
7635 def __le__(self, other):
7636 return fpLEQ(self, other)
7638 def __lt__(self, other):
7639 return fpLEQ(self, other)
7641 def __ge__(self, other):
7642 return fpGEQ(self, other)
7644 def __gt__(self, other):
7645 return fpGT(self, other)
7647 def __ne__(self, other):
7648 return fpNEQ(self, other)
7651 def __add__(self, other):
7652 """Create the Z3 expression `self + other`.
7661 a, b = z3._coerce_exprs(self, other)
7662 return fpAdd(_dflt_rm(), self, other)
7664 def __radd__(self, other):
7665 """Create the Z3 expression `other + self`.
7671 a, b = _coerce_exprs(self, other)
7672 return fpAdd(_dflt_rm(), other, self)
7674 def __sub__(self, other):
7675 """Create the Z3 expression `self - other`.
7684 a, b = z3._coerce_exprs(self, other)
7685 return fpSub(_dflt_rm(), self, other)
7687 def __rsub__(self, other):
7688 """Create the Z3 expression `other - self`.
7694 a, b = _coerce_exprs(self, other)
7695 return fpSub(_dflt_rm(), other, self)
7697 def __mul__(self, other):
7698 """Create the Z3 expression `self * other`.
7709 a, b = z3._coerce_exprs(self, other)
7710 return fpMul(_dflt_rm(), self, other)
7712 def __rmul__(self, other):
7713 """Create the Z3 expression `other * self`.
7722 a, b = _coerce_exprs(self, other)
7723 return fpMul(_dflt_rm(), other, self)
7726 """Create the Z3 expression `+self`.
"""
7730 """Create the Z3 expression `-self`.
"""
7731 return FPRef(fpNeg(self))
7733 def __truediv__(self, other):
7734 """Create the Z3 expression division `self / other`.
"""
7735 return self.__div__(other)
7737 def __rtruediv__(self, other):
7738 """Create the Z3 expression division `other / self`.
"""
7739 return self.__rdiv__(other)
7741 def __mod__(self, other):
7742 """Create the Z3 expression mod `self % other`.
"""
7743 return fpRem(self, other)
7745 def __rmod__(self, other):
7746 """Create the Z3 expression mod `other % self`.
"""
7747 return fpRem(other, self)
7749 class FPRMRef(ExprRef):
7750 """Floating-point rounding mode expressions
"""
7752 def as_string(self):
7753 """Return a Z3 floating point expression
as a Python string.
"""
7754 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
7757 def RoundNearestTiesToEven(ctx=None):
7759 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
7763 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
7765 def RoundNearestTiesToAway(ctx=None):
7767 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
7771 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
7773 def RoundTowardPositive(ctx=None):
7775 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
7779 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
7781 def RoundTowardNegative(ctx=None):
7783 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
7787 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
7789 def RoundTowardZero(ctx=None):
7791 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
7795 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
7798 """Return `
True`
if `a`
is a Z3 floating-point rounding mode expression.
7807 return isinstance(a, FPRMRef)
7809 def is_fprm_value(a):
7810 """Return `
True`
if `a`
is a Z3 floating-point rounding mode numeral value.
"""
7811 return is_fprm(a) and _is_numeral(a.ctx, a.ast)
7815 class FPNumRef(FPRef):
7817 return self.decl().kind() == Z3_OP_FPA_NAN
7820 return self.decl().kind() == Z3_OP_FPA_PLUS_INF or self.decl().kind() == Z3_OP_FPA_MINUS_INF
7823 return self.decl().kind() == Z3_OP_FPA_PLUS_ZERO or self.decl().kind() == Z3_OP_FPA_MINUS_ZERO
7825 def isNegative(self):
7826 k = self.decl().kind()
7827 return (self.num_args() == 0 and (k == Z3_OP_FPA_MINUS_INF or k == Z3_OP_FPA_MINUS_ZERO)) or (self.sign() == True)
7830 The sign of the numeral
7840 l = (ctypes.c_int)()
7841 if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False:
7842 raise Z3Exception("error retrieving the sign of a numeral.")
7846 The significand of the numeral
7851 def significand(self):
7852 return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())
7855 The exponent of the numeral
7862 return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast())
7865 The exponent of the numeral
as a long
7870 def exponent_as_long(self):
7871 ptr = (ctypes.c_longlong * 1)()
7872 if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr):
7873 raise Z3Exception("error retrieving the exponent of a numeral.")
7877 The string representation of the numeral
7882 def as_string(self):
7883 s = Z3_fpa_get_numeral_string(self.ctx.ref(), self.as_ast())
7884 return ("FPVal(%s, %s)" % (s, FPSortRef(self.sort()).as_string()))
7887 def _to_fpnum(num, ctx=None):
7888 if isinstance(num, FPNum):
7891 return FPNum(num, ctx)
7894 """Return `
True`
if `a`
is a Z3 floating-point expression.
7904 return isinstance(a, FPRef)
7907 """Return `
True`
if `a`
is a Z3 floating-point numeral value.
7918 return is_fp(a) and _is_numeral(a.ctx, a.ast)
7920 def FPSort(ebits, sbits, ctx=None):
7921 """Return a Z3 floating-point sort of the given sizes. If `ctx=
None`, then the
global context
is used.
7923 >>> Single =
FPSort(8, 24)
7924 >>> Double =
FPSort(11, 53)
7927 >>> x =
Const(
'x', Single)
7931 ctx = z3._get_ctx(ctx)
7932 return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
7934 def _to_float_str(val):
7935 if isinstance(val, float):
7937 elif isinstance(val, bool):
7944 elif isinstance(val, str):
7947 _z3_assert(False, "Python value cannot be used as a double")
7950 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
7951 return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
7953 def fpPlusInfinity(s):
7954 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
7955 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
7957 def fpMinusInfinity(s):
7958 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
7959 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
7961 def fpInfinity(s, negative):
7962 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
7963 _z3_assert(isinstance(negative, bool), "expected Boolean flag")
7964 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
7967 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
7968 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
7971 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
7972 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
7974 def fpZero(s, negative):
7975 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
7976 _z3_assert(isinstance(negative, bool), "expected Boolean flag")
7977 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
7979 def FPVal(sig, exp=None, fps=None, ctx=None):
7980 """Return a floating-point value of value `val`
and sort `fps`. If `ctx=
None`, then the
global context
is used.
7985 >>> print(
"0x%.8x" % v.exponent_as_long())
7999 fps = _dflt_fps(ctx)
8000 _z3_assert(is_fp_sort(fps), "sort mismatch")
8003 val = _to_float_str(sig)
8005 val = val + _to_int_str(exp)
8006 return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
8008 def FP(name, fpsort, ctx=None):
8009 """Return a floating-point constant named `name`.
8010 `fpsort`
is the floating-point sort.
8011 If `ctx=
None`, then the
global context
is used.
8021 >>> x2 =
FP(
'x', word)
8026 return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
8028 def FPs(names, fpsort, ctx=None):
8029 """Return an array of floating-point constants.
8031 >>> x, y, z =
BitVecs(
'x y z', 16)
8043 ctx = z3._get_ctx(ctx)
8044 if isinstance(names, str):
8045 names = names.split(" ")
8046 return [FP(name, fpsort, ctx) for name in names]
8049 """Create a Z3 floating-point absolute value expression.
8053 >>> x =
FPVal(1.0, s)
8056 >>> y =
FPVal(-20.0, s)
8061 >>>
fpAbs(-1.25*(2**4))
8069 s = get_default_fp_sort(ctx)
8074 _z3_assert(is_fp(a), "First argument must be Z3 floating-point expression")
8075 return FPRef(Z3_mk_fpa_abs(a.ctx_ref(), a.as_ast()), a.ctx)
8078 """Create a Z3 floating-point addition expression.
8091 s = get_default_fp_sort(ctx)
8096 _z3_assert(is_fp(a), "First argument must be Z3 floating-point expression")
8097 return FPRef(Z3_mk_fpa_neg(a.ctx_ref(), a.as_ast()), a.ctx)
8099 def fpAdd(rm, a, b):
8100 """Create a Z3 floating-point addition expression.
8108 >>>
fpAdd(rm, x, y).sort()
8112 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
8113 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
8114 a, b = _coerce_exprs(a, b)
8115 return FPRef(Z3_mk_fpa_add(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)
8117 def fpSub(rm, a, b):
8118 """Create a Z3 floating-point subtraction expression.
8126 >>>
fpSub(rm, x, y).sort()
8130 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
8131 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
8132 a, b = _coerce_exprs(a, b)
8133 return FPRef(Z3_mk_fpa_sub(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)
8135 def fpMul(rm, a, b):
8136 """Create a Z3 floating-point multiplication expression.
8144 >>>
fpMul(rm, x, y).sort()
8148 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
8149 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
8150 a, b = _coerce_exprs(a, b)
8151 return FPRef(Z3_mk_fpa_mul(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)
8153 def fpDiv(rm, a, b):
8154 """Create a Z3 floating-point divison expression.
8162 >>>
fpDiv(rm, x, y).sort()
8166 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
8167 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
8168 a, b = _coerce_exprs(a, b)
8169 return FPRef(Z3_mk_fpa_div(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)
8172 """Create a Z3 floating-point remainder expression.
8179 >>>
fpRem(x, y).sort()
8183 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
8184 a, b = _coerce_exprs(a, b)
8185 return FPRef(Z3_mk_fpa_rem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
8188 """Create a Z3 floating-point minimium expression.
8196 >>>
fpMin(x, y).sort()
8200 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
8201 a, b = _coerce_exprs(a, b)
8202 return FPRef(Z3_mk_fpa_min(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
8205 """Create a Z3 floating-point maximum expression.
8213 >>>
fpMax(x, y).sort()
8217 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
8218 a, b = _coerce_exprs(a, b)
8219 return FPRef(Z3_mk_fpa_max(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
8221 def fpFMA(rm, a, b, c):
8222 """Create a Z3 floating-point fused multiply-add expression.
8225 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
8226 _z3_assert(is_fp(a) or is_fp(b) or is_fp(c), "Second, third, or fourth argument must be a Z3 floating-point expression")
8227 a, b, c = _coerce_expr_list([a, b, c])
8228 return FPRef(Z3_mk_fpa_fma(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), rm.ctx)
8231 """Create a Z3 floating-point square root expression.
8236 s = get_default_fp_sort(ctx)
8241 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
8242 _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expressions")
8243 return FPRef(Z3_mk_fpa_sqrt(rm.ctx_ref(), rm.as_ast(), a.as_ast()), rm.ctx)
8245 def fpRoundToIntegral(rm, a):
8246 """Create a Z3 floating-point roundToIntegral expression.
8251 s = get_default_fp_sort(ctx)
8256 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
8257 _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expressions")
8258 return FPRef(Z3_mk_fpa_round_to_integral(rm.ctx_ref(), rm.as_ast(), a.as_ast()), rm.ctx)
8261 """Create a Z3 floating-point isNaN expression.
8264 _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
8265 return FPRef(Z3_mk_fpa_is_nan(a.ctx_ref(), a.as_ast()), a.ctx)
8267 def fpIsInfinite(a):
8268 """Create a Z3 floating-point isNaN expression.
8271 _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
8272 return FPRef(Z3_mk_fpa_is_infinite(a.ctx_ref(), a.as_ast()), a.ctx)
8275 """Create a Z3 floating-point isNaN expression.
8278 _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
8279 return FPRef(Z3_mk_fpa_is_zero(a.ctx_ref(), a.as_ast()), a.ctx)
8282 """Create a Z3 floating-point isNaN expression.
8285 _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
8286 return FPRef(Z3_mk_fpa_is_normal(a.ctx_ref(), a.as_ast()), a.ctx)
8288 def fpIsSubnormal(a):
8289 """Create a Z3 floating-point isNaN expression.
8292 _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
8293 return FPRef(Z3_mk_fpa_is_subnormal(a.ctx_ref(), a.as_ast()), a.ctx)
8295 def fpIsNegative(a):
8296 """Create a Z3 floating-point isNaN expression.
8299 _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
8300 return FPRef(Z3_mk_fpa_is_negative(a.ctx_ref(), a.as_ast()), a.ctx)
8302 def fpIsPositive(a):
8303 """Create a Z3 floating-point isNaN expression.
8306 _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
8307 return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx)
8309 def _check_fp_args(a, b):
8311 _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression")
8314 """Create the Z3 floating-point expression `other <= self`.
8319 >>> (x <= y).sexpr()
8322 _check_fp_args(a, b)
8323 a, b = _coerce_exprs(a, b)
8324 return BoolRef(Z3_mk_fpa_lt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
8327 """Create the Z3 floating-point expression `other <= self`.
8332 >>> (x <= y).sexpr()
8335 _check_fp_args(a, b)
8336 a, b = _coerce_exprs(a, b)
8337 return BoolRef(Z3_mk_fpa_leq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
8340 """Create the Z3 floating-point expression `other <= self`.
8348 _check_fp_args(a, b)
8349 a, b = _coerce_exprs(a, b)
8350 return BoolRef(Z3_mk_fpa_gt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
8354 """Create the Z3 floating-point expression `other <= self`.
8361 >>> (x >= y).sexpr()
8364 _check_fp_args(a, b)
8365 a, b = _coerce_exprs(a, b)
8366 return BoolRef(Z3_mk_fpa_geq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
8369 """Create the Z3 floating-point expression `other <= self`.
8374 >>>
fpEQ(x, y).sexpr()
8377 _check_fp_args(a, b)
8378 a, b = _coerce_exprs(a, b)
8379 return BoolRef(Z3_mk_fpa_eq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
8382 """Create the Z3 floating-point expression `other <= self`.
8387 >>> (x != y).sexpr()
8390 _check_fp_args(a, b)
8391 a, b = _coerce_exprs(a, b)
8392 return Not(BoolRef(Z3_mk_fpa_eq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx), a.ctx)
8396 def fpFP(sgn, exp, sig):
8397 """Create the Z3 floating-point value `
fpFP(sgn, sig, exp)`
from the three bit-vectorssgn, sig,
and exp.
"""
8398 _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
8399 _z3_assert(sgn.sort().size() == 1, "sort mismatch")
8400 return FPRef(Z3_mk_fpa_fp(sgn.ctx_ref(), sgn.ast, exp.ast, sig.ast), sgn.ctx)
8403 def fpToFP(a1, a2=None, a3=None):
8404 """Create a Z3 floating-point conversion expression
from other terms.
"""
8405 if is_bv(a1) and is_fp_sort(a2):
8406 return FPRef(Z3_mk_fpa_to_fp_bv(a1.ctx_ref(), a1.ast, a2.ast), a1.ctx)
8407 elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
8408 return FPRef(Z3_mk_fpa_to_fp_float(a1.ctx_ref(), a1.ast, a2.ast, a3.ast), a1.ctx)
8409 elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
8410 return FPRef(Z3_mk_fpa_to_fp_real(a1.ctx_ref(), a1.ast, a2.ast, a3.ast), a1.ctx)
8411 elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
8412 return FPRef(Z3_mk_fpa_to_fp_signed(a1.ctx_ref(), a1.ast, a2.ast, a3.ast), a1.ctx)
8414 raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
8416 def fpToFPUnsigned(rm, x, s):
8417 """Create a Z3 floating-point conversion expression,
from unsigned bit-vector to floating-point expression.
"""
8419 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
8420 _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
8421 _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
8422 return FPRef(Z3_mk_fpa_to_fp_unsigned(rm.ctx_ref(), rm.ast, x.ast, s.ast), rm.ctx)
8424 def fpToSBV(rm, x, s):
8425 """Create a Z3 floating-point conversion expression,
from floating-point expression to signed bit-vector.
8439 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
8440 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
8441 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
8442 return BitVecRef(Z3_mk_fpa_to_sbv(rm.ctx_ref(), rm.ast, x.ast, s.size()), rm.ctx)
8444 def fpToUBV(rm, x, s):
8445 """Create a Z3 floating-point conversion expression,
from floating-point expression to unsigned bit-vector.
8459 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
8460 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
8461 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
8462 return BitVecRef(Z3_mk_fpa_to_ubv(rm.ctx_ref(), rm.ast, x.ast, s.size()), rm.ctx)
8465 """Create a Z3 floating-point conversion expression,
from floating-point expression to real.
8479 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
8480 return ArithRef(Z3_mk_fpa_to_real(x.ctx_ref(), x.ast), x.ctx)
8483 """\brief Conversion of a floating-point term into a bit-vector term
in IEEE 754-2008 format.
8485 The size of the resulting bit-vector
is automatically determined.
8487 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
8488 knows only one NaN
and it will always produce the same bit-vector represenatation of
8503 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
8504 return BitVecRef(Z3_mk_fpa_to_ieee_bv(x.ctx_ref(), x.ast), x.ctx)
Z3_ast Z3_API Z3_mk_const(__in Z3_context c, __in Z3_symbol s, __in Z3_sort ty)
Declare and create a constant.
def simplify(a, arguments, keywords)
Utils.
Z3_tactic Z3_API Z3_tactic_par_and_then(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1...
void Z3_API Z3_fixedpoint_assert(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast axiom)
Assert a constraint to the fixedpoint context.
Z3_context Z3_API Z3_mk_context_rc(__in 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_ast Z3_API Z3_translate(__in Z3_context source, __in Z3_ast a, __in Z3_context target)
Translate/Copy the AST a from context source to context target. AST a must have been created using co...
Z3_ast Z3_API Z3_mk_mul(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].The array args must have num_args el...
Z3_string Z3_API Z3_fixedpoint_get_help(__in Z3_context c, __in Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
def update_rule(self, head, body, name)
void Z3_API Z3_inc_ref(__in Z3_context c, __in Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
def get_cover_delta(self, level, predicate)
void Z3_API Z3_apply_result_inc_ref(__in Z3_context c, __in Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
def __getitem__(self, idx)
Z3_tactic Z3_API Z3_mk_tactic(__in Z3_context c, __in Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
Z3_string Z3_API Z3_tactic_get_help(__in Z3_context c, __in Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
Z3_string Z3_API Z3_get_tactic_name(__in Z3_context c, unsigned i)
Return the name of the idx tactic.
Z3_ast Z3_API Z3_mk_bound(__in Z3_context c, __in unsigned index, __in Z3_sort ty)
Create a bound variable.
Z3_symbol Z3_API Z3_get_decl_name(__in Z3_context c, __in Z3_func_decl d)
Return the constant declaration name as a symbol.
Z3_probe Z3_API Z3_probe_eq(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
void Z3_API Z3_fixedpoint_update_rule(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast a, __in Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created. ...
Z3_ast Z3_API Z3_substitute_vars(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
Z3_tactic Z3_API Z3_tactic_fail_if(__in Z3_context c, __in Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
unsigned Z3_API Z3_get_app_num_args(__in Z3_context c, __in Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
def substitute_vars(t, m)
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(__in Z3_context c, __in Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
Z3_bool Z3_API Z3_global_param_get(__in Z3_string param_id, __out Z3_string_ptr param_value)
Get a global (or module) parameter.
def declare(self, name, args)
void Z3_API Z3_enable_trace(__in Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
def set_option(args, kws)
Z3_apply_result Z3_API Z3_tactic_apply(__in Z3_context c, __in Z3_tactic t, __in Z3_goal g)
Apply tactic t to the goal g.
Z3_model Z3_API Z3_apply_result_convert_model(__in Z3_context c, __in Z3_apply_result r, __in unsigned i, __in Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
Z3_bool Z3_API Z3_open_log(__in Z3_string filename)
Log interaction to a file.
Z3_symbol Z3_API Z3_mk_string_symbol(__in Z3_context c, __in Z3_string s)
Create a Z3 symbol using a C string.
unsigned Z3_API Z3_get_num_tactics(__in Z3_context c)
Return the number of builtin tactics available in Z3.
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(__in Z3_context c, __in Z3_fixedpoint f, __in Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context...
Z3_sort Z3_API Z3_get_range(__in Z3_context c, __in Z3_func_decl d)
Return the range of the given declaration.
def assert_exprs(self, args)
Z3_probe Z3_API Z3_probe_gt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
Z3_ast Z3_API Z3_substitute(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const from[], __in_ecount(num_exprs) 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_bool Z3_API Z3_is_eq_ast(__in Z3_context c, __in Z3_ast t1, Z3_ast t2)
compare terms.
def register_relation(self, relations)
void Z3_API Z3_global_param_set(__in Z3_string param_id, __in Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
void Z3_API Z3_set_ast_print_mode(__in Z3_context c, __in Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
Z3_string Z3_API Z3_apply_result_to_string(__in Z3_context c, __in Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(__in Z3_context c, __in Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
void Z3_API Z3_apply_result_dec_ref(__in Z3_context c, __in Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(__in Z3_context c, __in Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
Z3_tactic Z3_API Z3_tactic_repeat(__in Z3_context c, __in 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_ast_kind Z3_API Z3_get_ast_kind(__in Z3_context c, __in Z3_ast a)
Return the kind of the given AST.
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d)
Backtrack one backtracking point.
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(__in Z3_string string)
Append user-defined string to interaction log.
void Z3_API Z3_get_version(__out unsigned *major, __out unsigned *minor, __out unsigned *build_number, __out unsigned *revision_number)
Return Z3 version number information.
Z3_goal Z3_API Z3_apply_result_get_subgoal(__in Z3_context c, __in Z3_apply_result r, __in unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_decl_kind Z3_API Z3_get_decl_kind(__in Z3_context c, __in Z3_func_decl d)
Return declaration kind corresponding to declaration.
Z3_tactic Z3_API Z3_tactic_try_for(__in Z3_context c, __in Z3_tactic t, __in unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
def Array(name, dom, rng)
Z3_tactic Z3_API Z3_tactic_using_params(__in Z3_context c, __in Z3_tactic t, __in Z3_params p)
Return a tactic that applies t using the given set of parameters.
void Z3_API Z3_dec_ref(__in Z3_context c, __in Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_tactic Z3_API Z3_tactic_and_then(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d)
Create a backtracking point.
Z3_ast Z3_API Z3_simplify(__in Z3_context c, __in Z3_ast a)
Interface to simplifier.
def simplify_param_descrs()
Z3_solver Z3_API Z3_mk_solver_for_logic(__in Z3_context c, __in Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
void Z3_API Z3_probe_inc_ref(__in Z3_context c, __in Z3_probe p)
Increment the reference counter of the given probe.
Z3_string Z3_API Z3_fixedpoint_to_string(__in Z3_context c, __in Z3_fixedpoint f, __in unsigned num_queries, __in_ecount(num_queries) Z3_ast queries[])
Print the current rules and background axioms as a string.
Z3_probe Z3_API Z3_probe_not(__in Z3_context x, __in Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_symbol_kind Z3_API Z3_get_symbol_kind(__in Z3_context c, __in Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
Z3_lbool Z3_API Z3_fixedpoint_query(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast query)
Pose a query against the asserted rules.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(__in Z3_context c, __in Z3_fixedpoint d, __in unsigned num_relations, __in_ecount(num_relations) Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
def __init__(self, args, kws)
Z3_ast Z3_API Z3_mk_ite(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_tactic Z3_API Z3_tactic_cond(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t1, __in 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_string Z3_API Z3_probe_get_descr(__in Z3_context c, __in Z3_string name)
Return a string containing a description of the probe with the given name.
def Extract(high, low, a)
void Z3_API Z3_fixedpoint_inc_ref(__in Z3_context c, __in Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
def solve_using(s, args, keywords)
def set_predicate_representation(self, f, representations)
void Z3_API Z3_fixedpoint_add_rule(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_ast rule, __in Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form: ...
unsigned Z3_API Z3_get_arity(__in Z3_context c, __in Z3_func_decl d)
Alias for Z3_get_domain_size.
int Z3_API Z3_get_symbol_int(__in Z3_context c, __in Z3_symbol s)
Return the symbol int value.
unsigned Z3_API Z3_get_ast_id(__in 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.
unsigned Z3_API Z3_get_ast_hash(__in Z3_context c, __in Z3_ast a)
Return a hash code for the given AST. The hash code is structural. You can use Z3_get_ast_id intercha...
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(__in Z3_context c, __in Z3_fixedpoint f, __in Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context...
def apply(self, goal, arguments, keywords)
def solve(args, keywords)
def check(self, assumptions)
Z3_string Z3_API Z3_ast_to_string(__in Z3_context c, __in Z3_ast a)
Convert the given AST node into a string.
def __call__(self, goal, arguments, keywords)
Z3_solver Z3_API Z3_mk_simple_solver(__in Z3_context c)
Create a new (incremental) solver.
Z3_probe Z3_API Z3_probe_const(__in Z3_context x, __in double val)
Return a probe that always evaluates to val.
def prove(claim, keywords)
Z3_string Z3_API Z3_tactic_get_descr(__in Z3_context c, __in Z3_string name)
Return a string containing a description of the tactic with the given name.
void Z3_API Z3_set_error_handler(__in Z3_context c, __in Z3_error_handler h)
Register a Z3 error handler.
Z3_stats Z3_API Z3_fixedpoint_get_statistics(__in Z3_context c, __in Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
Z3_string Z3_API Z3_simplify_get_help(__in Z3_context c)
Return a string describing all available parameters.
Z3_string Z3_API Z3_get_probe_name(__in Z3_context c, unsigned i)
Return the name of the i probe.
void Z3_API Z3_disable_trace(__in Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
Z3_string Z3_API Z3_benchmark_to_smtlib_string(__in Z3_context c, __in Z3_string name, __in Z3_string logic, __in Z3_string status, __in Z3_string attributes, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[], __in Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
Z3_probe Z3_API Z3_probe_ge(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
void Z3_API Z3_del_config(__in Z3_config c)
Delete the given configuration object.
void Z3_API Z3_fixedpoint_dec_ref(__in Z3_context c, __in Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
Z3_ast Z3_API Z3_sort_to_ast(__in Z3_context c, __in Z3_sort s)
Convert a Z3_sort into Z3_ast. This is just type casting.
Z3_sort Z3_API Z3_get_sort(__in Z3_context c, __in Z3_ast a)
Return the sort of an AST node.
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(__in Z3_context c, __in Z3_tactic t)
Return the parameter description set for the given tactic object.
def translate(self, target)
Z3_func_decl Z3_API Z3_get_app_decl(__in Z3_context c, __in Z3_app a)
Return the declaration of a constant or function application.
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. ...
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...
unsigned Z3_API Z3_get_num_probes(__in Z3_context c)
Return the number of builtin probes available in Z3.
Z3_sort Z3_API Z3_get_domain(__in Z3_context c, __in Z3_func_decl d, __in unsigned i)
Return the sort of the i-th parameter of the given function declaration.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
void Z3_API Z3_tactic_dec_ref(__in Z3_context c, __in Z3_tactic g)
Decrement the reference counter of the given tactic.
def to_string(self, queries)
Z3_ast Z3_API Z3_mk_distinct(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).The distinct construct is us...
void Z3_API Z3_interrupt(__in Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
Z3_symbol Z3_API Z3_get_sort_name(__in Z3_context c, __in Z3_sort d)
Return the sort name as a symbol.
def parse_string(self, s)
Z3_tactic Z3_API Z3_tactic_when(__in Z3_context c, __in Z3_probe p, __in 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_probe Z3_API Z3_probe_le(__in Z3_context x, __in Z3_probe p1, __in 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 declare_var(self, vars)
unsigned Z3_API Z3_get_index_value(__in Z3_context c, __in Z3_ast a)
Return index of de-Brujin bound variable.
Z3_solver Z3_API Z3_mk_solver_from_tactic(__in Z3_context c, __in Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
void Z3_API Z3_fixedpoint_register_relation(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...
Z3_ast Z3_API Z3_func_decl_to_ast(__in Z3_context c, __in Z3_func_decl f)
Convert a Z3_func_decl into Z3_ast. This is just type casting.
Z3_probe Z3_API Z3_probe_lt(__in Z3_context x, __in Z3_probe p1, __in Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(__in Z3_context c)
Create a new fixedpoint context.
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(__in Z3_context c, __in Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query. ...
Z3_string Z3_API Z3_get_symbol_string(__in Z3_context c, __in Z3_symbol s)
Return the symbol name.
void Z3_API Z3_probe_dec_ref(__in Z3_context c, __in Z3_probe p)
Decrement the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_eq(__in Z3_context c, __in Z3_ast l, __in Z3_ast r)
Create an AST node representing l = r.
Z3_tactic Z3_API Z3_tactic_par_or(__in Z3_context c, __in unsigned num, __in_ecount(num) Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
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...
def get_num_levels(self, predicate)
void Z3_API Z3_fixedpoint_set_predicate_representation(__in Z3_context c, __in Z3_fixedpoint d, __in Z3_func_decl f, __in unsigned num_relations, __in_ecount(num_relations) Z3_symbol const relation_kinds[])
Configure the predicate representation.
Z3_sort_kind Z3_API Z3_get_sort_kind(__in Z3_context c, __in Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
Z3_ast Z3_API Z3_mk_app(__in Z3_context c, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create a constant or function application.
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
def __init__(self, result, ctx)
def set(self, args, keys)
def add_cover(self, level, predicate, property)
Z3_tactic Z3_API Z3_tactic_or_else(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
void Z3_API Z3_fixedpoint_set_params(__in Z3_context c, __in Z3_fixedpoint f, __in Z3_params p)
Set parameters on fixedpoint context.
tuple _error_handler_fptr
Z3_symbol Z3_API Z3_mk_int_symbol(__in Z3_context c, __in int i)
Create a Z3 symbol using an integer.
Z3_ast Z3_API Z3_mk_add(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].The array args must have num_args el...
Z3_ast Z3_API Z3_get_app_arg(__in Z3_context c, __in Z3_app a, __in unsigned i)
Return the i-th argument of the given application.
void Z3_API Z3_set_param_value(__in Z3_config c, __in Z3_string param_id, __in Z3_string param_value)
Set a configuration parameter.
Z3_probe Z3_API Z3_mk_probe(__in Z3_context c, __in Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
void Z3_API Z3_tactic_inc_ref(__in Z3_context c, __in Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(__in Z3_context c, __in Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.
double Z3_API Z3_probe_apply(__in Z3_context c, __in Z3_probe p, __in Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
Z3_ast Z3_API Z3_simplify_ex(__in Z3_context c, __in Z3_ast a, __in Z3_params p)
Interface to simplifier.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(__in Z3_context c)
Return the parameter description set for the simplify procedure.
unsigned Z3_API Z3_apply_result_get_num_subgoals(__in Z3_context c, __in Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
def is_algebraic_value(a)
Z3_bool Z3_API Z3_is_eq_sort(__in Z3_context c, __in Z3_sort s1, __in Z3_sort s2)
compare sorts.
Z3_ast Z3_API Z3_fixedpoint_get_answer(__in Z3_context c, __in Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.