9"""Z3 is a high performance theorem prover developed at Microsoft Research.
11Z3 is used in many applications such as: software/hardware verification and testing,
12constraint solving, analysis of hybrid systems, security, biology (in silico analysis),
13and geometrical problems.
16Please send feedback, comments and/or corrections on the Issue tracker for
17https://github.com/Z3prover/z3.git. Your comments are very valuable.
38... x = BitVec('x', 32)
40... # the expression x + y is type incorrect
42... except Z3Exception as ex:
43... print("failed: %s" % ex)
49from .z3consts
import *
50from .z3printer
import *
51from fractions
import Fraction
56if sys.version_info.major >= 3:
57 from typing
import Iterable
67if sys.version_info.major < 3:
69 return isinstance(v, (int, long))
72 return isinstance(v, int)
84 major = ctypes.c_uint(0)
85 minor = ctypes.c_uint(0)
86 build = ctypes.c_uint(0)
87 rev = ctypes.c_uint(0)
89 return "%s.%s.%s" % (major.value, minor.value, build.value)
93 major = ctypes.c_uint(0)
94 minor = ctypes.c_uint(0)
95 build = ctypes.c_uint(0)
96 rev = ctypes.c_uint(0)
98 return (major.value, minor.value, build.value, rev.value)
107 raise Z3Exception(msg)
111 _z3_assert(ctypes.c_int(n).value == n, name +
" is too large")
115 """Log interaction to a file. This function must be invoked immediately after init(). """
120 """Append user-defined string to interaction log. """
125 """Convert an integer or string into a Z3 symbol."""
133 """Convert a Z3 symbol back into a Python object. """
146 if len(args) == 1
and (isinstance(args[0], tuple)
or isinstance(args[0], list)):
148 elif len(args) == 1
and (isinstance(args[0], set)
or isinstance(args[0], AstVector)):
149 return [arg
for arg
in args[0]]
160 if isinstance(args, (set, AstVector, tuple)):
161 return [arg
for arg
in args]
169 if isinstance(val, bool):
170 return "true" if val
else "false"
181 """A Context manages all other Z3 objects, global configuration options, etc.
183 Z3Py uses a default global context. For most applications this is sufficient.
184 An application may use multiple Z3 contexts. Objects created in one context
185 cannot be used in another one. However, several objects may be "translated" from
186 one context to another. It is not safe to access Z3 objects from multiple threads.
187 The only exception is the method `interrupt()` that can be used to interrupt() a long
189 The initialization method receives global configuration options for the new context.
194 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
213 if Z3_del_context
is not None and self.
owner:
219 """Return a reference to the actual C pointer to the Z3 context."""
223 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
225 This method can be invoked from a thread different from the one executing the
226 interruptible procedure.
231 """Return the global parameter description set."""
240 """Return a reference to the global Z3 context.
243 >>> x.ctx == main_ctx()
248 >>> x2 = Real('x', c)
255 if _main_ctx
is None:
272 """Set Z3 global (or module) parameters.
274 >>> set_param(precision=10)
277 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
281 if not set_pp_option(k, v):
296 """Reset all global (or module) parameters.
302 """Alias for 'set_param' for backward compatibility.
308 """Return the value of a Z3 global (or module) parameter
310 >>> get_param('nlsat.reorder')
313 ptr = (ctypes.c_char_p * 1)()
315 r = z3core._to_pystr(ptr[0])
317 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
329 """Superclass for all Z3 objects that have support for pretty printing."""
335 in_html = in_html_mode()
338 set_html_mode(in_html)
343 """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions."""
351 if self.
ctx.ref()
is not None and self.
ast is not None and Z3_dec_ref
is not None:
359 return obj_to_string(self)
362 return obj_to_string(self)
365 return self.
eq(other)
378 elif is_eq(self)
and self.num_args() == 2:
379 return self.arg(0).
eq(self.arg(1))
381 raise Z3Exception(
"Symbolic expressions cannot be cast to concrete Boolean values.")
384 """Return a string representing the AST node in s-expression notation.
387 >>> ((x + 1)*x).sexpr()
393 """Return a pointer to the corresponding C Z3_ast object."""
397 """Return unique identifier for object. It can be used for hash-tables and maps."""
401 """Return a reference to the C context where this AST node is stored."""
402 return self.
ctx.ref()
405 """Return `True` if `self` and `other` are structurally identical.
412 >>> n1 = simplify(n1)
413 >>> n2 = simplify(n2)
422 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
428 >>> # Nodes in different contexts can't be mixed.
429 >>> # However, we can translate nodes from one context to another.
430 >>> x.translate(c2) + y
434 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
441 """Return a hashcode for the `self`.
443 >>> n1 = simplify(Int('x') + 1)
444 >>> n2 = simplify(2 + Int('x') - 1)
445 >>> n1.hash() == n2.hash()
452 """Return `True` if `a` is an AST node.
456 >>> is_ast(IntVal(10))
460 >>> is_ast(BoolSort())
462 >>> is_ast(Function('f', IntSort(), IntSort()))
469 return isinstance(a, AstRef)
473 """Return `True` if `a` and `b` are structurally identical AST nodes.
483 >>> eq(simplify(x + 1), simplify(1 + x))
517 _args = (FuncDecl * sz)()
519 _args[i] = args[i].as_func_decl()
527 _args[i] = args[i].as_ast()
535 _args[i] = args[i].as_ast()
543 elif k == Z3_FUNC_DECL_AST:
560 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node."""
569 """Return the Z3 internal kind of a sort.
570 This method can be used to test if `self` is one of the Z3 builtin sorts.
573 >>> b.kind() == Z3_BOOL_SORT
575 >>> b.kind() == Z3_INT_SORT
577 >>> A = ArraySort(IntSort(), IntSort())
578 >>> A.kind() == Z3_ARRAY_SORT
580 >>> A.kind() == Z3_INT_SORT
586 """Return `True` if `self` is a subsort of `other`.
588 >>> IntSort().subsort(RealSort())
594 """Try to cast `val` as an element of sort `self`.
596 This method is used in Z3Py to convert Python objects such as integers,
597 floats, longs and strings into Z3 expressions.
600 >>> RealSort().cast(x)
609 """Return the name (string) of sort `self`.
611 >>> BoolSort().name()
613 >>> ArraySort(IntSort(), IntSort()).name()
619 """Return `True` if `self` and `other` are the same Z3 sort.
622 >>> p.sort() == BoolSort()
624 >>> p.sort() == IntSort()
632 """Return `True` if `self` and `other` are not the same Z3 sort.
635 >>> p.sort() != BoolSort()
637 >>> p.sort() != IntSort()
644 return AstRef.__hash__(self)
648 """Return `True` if `s` is a Z3 sort.
650 >>> is_sort(IntSort())
652 >>> is_sort(Int('x'))
654 >>> is_expr(Int('x'))
657 return isinstance(s, SortRef)
662 _z3_assert(isinstance(s, Sort),
"Z3 Sort expected")
664 if k == Z3_BOOL_SORT:
666 elif k == Z3_INT_SORT
or k == Z3_REAL_SORT:
668 elif k == Z3_BV_SORT:
670 elif k == Z3_ARRAY_SORT:
672 elif k == Z3_DATATYPE_SORT:
674 elif k == Z3_FINITE_DOMAIN_SORT:
676 elif k == Z3_FLOATING_POINT_SORT:
678 elif k == Z3_ROUNDING_MODE_SORT:
680 elif k == Z3_RE_SORT:
682 elif k == Z3_SEQ_SORT:
684 elif k == Z3_CHAR_SORT:
686 elif k == Z3_TYPE_VAR:
696 """Create a new uninterpreted sort named `name`.
698 If `ctx=None`, then the new sort is declared in the global Z3Py context.
700 >>> A = DeclareSort('A')
701 >>> a = Const('a', A)
702 >>> b = Const('b', A)
714 """Type variable reference"""
724 """Create a new type variable named `name`.
726 If `ctx=None`, then the new sort is declared in the global Z3Py context.
741 """Function declaration. Every constant and function have an associated declaration.
743 The declaration assigns a name, a sort (i.e., type), and for function
744 the sort (i.e., type) of each of its arguments. Note that, in Z3,
745 a constant is a function with 0 arguments.
758 """Return the name of the function declaration `self`.
760 >>> f = Function('f', IntSort(), IntSort())
763 >>> isinstance(f.name(), str)
769 """Return the number of arguments of a function declaration.
770 If `self` is a constant, then `self.arity()` is 0.
772 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
779 """Return the sort of the argument `i` of a function declaration.
780 This method assumes that `0 <= i < self.arity()`.
782 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
791 """Return the sort of the range of a function declaration.
792 For constants, this is the sort of the constant.
794 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
801 """Return the internal kind of a function declaration.
802 It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
805 >>> d = (x + 1).decl()
806 >>> d.kind() == Z3_OP_ADD
808 >>> d.kind() == Z3_OP_MUL
816 result = [
None for i
in range(n)]
819 if k == Z3_PARAMETER_INT:
821 elif k == Z3_PARAMETER_DOUBLE:
823 elif k == Z3_PARAMETER_RATIONAL:
825 elif k == Z3_PARAMETER_SYMBOL:
827 elif k == Z3_PARAMETER_SORT:
829 elif k == Z3_PARAMETER_AST:
831 elif k == Z3_PARAMETER_FUNC_DECL:
838 """Create a Z3 application expression using the function `self`, and the given arguments.
840 The arguments must be Z3 expressions. This method assumes that
841 the sorts of the elements in `args` match the sorts of the
842 domain. Limited coercion is supported. For example, if
843 args[0] is a Python integer, and the function expects a Z3
844 integer, then the argument is automatically converted into a
847 >>> f = Function('f', IntSort(), RealSort(), BoolSort())
857 _args = (Ast * num)()
862 tmp = self.
domain(i).cast(args[i])
864 _args[i] = tmp.as_ast()
869 """Return `True` if `a` is a Z3 function declaration.
871 >>> f = Function('f', IntSort(), IntSort())
878 return isinstance(a, FuncDeclRef)
882 """Create a new Z3 uninterpreted function with the given sorts.
884 >>> f = Function('f', IntSort(), IntSort())
890 _z3_assert(len(sig) > 0,
"At least two arguments expected")
895 dom = (Sort * arity)()
896 for i
in range(arity):
905 """Create a new fresh Z3 uninterpreted function with the given sorts.
909 _z3_assert(len(sig) > 0,
"At least two arguments expected")
914 dom = (z3.Sort * arity)()
915 for i
in range(arity):
928 """Create a new Z3 recursive with the given sorts."""
931 _z3_assert(len(sig) > 0,
"At least two arguments expected")
936 dom = (Sort * arity)()
937 for i
in range(arity):
946 """Set the body of a recursive function.
947 Recursive definitions can be simplified if they are applied to ground
950 >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
951 >>> n = Int('n', ctx)
952 >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
955 >>> s = Solver(ctx=ctx)
956 >>> s.add(fac(n) < 3)
959 >>> s.model().eval(fac(5))
969 _args[i] = args[i].ast
980 """Constraints, formulas and terms are expressions in Z3.
982 Expressions are ASTs. Every expression has a sort.
983 There are three main kinds of expressions:
984 function applications, quantifiers and bounded variables.
985 A constant is a function application with 0 arguments.
986 For quantifier free problems, all expressions are
987 function applications.
997 """Return the sort of expression `self`.
1009 """Shorthand for `self.sort().kind()`.
1011 >>> a = Array('a', IntSort(), IntSort())
1012 >>> a.sort_kind() == Z3_ARRAY_SORT
1014 >>> a.sort_kind() == Z3_INT_SORT
1020 """Return a Z3 expression that represents the constraint `self == other`.
1022 If `other` is `None`, then this method simply returns `False`.
1038 return AstRef.__hash__(self)
1041 """Return a Z3 expression that represents the constraint `self != other`.
1043 If `other` is `None`, then this method simply returns `True`.
1062 """Return the Z3 function declaration associated with a Z3 application.
1064 >>> f = Function('f', IntSort(), IntSort())
1077 """Return the Z3 internal kind of a function application."""
1084 """Return the number of arguments of a Z3 application.
1088 >>> (a + b).num_args()
1090 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1100 """Return argument `idx` of the application `self`.
1102 This method assumes that `self` is a function application with at least `idx+1` arguments.
1106 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1121 """Return a list containing the children of the given expression
1125 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
1131 return [self.
arg(i)
for i
in range(self.
num_args())]
1145 """inverse function to the serialize method on ExprRef.
1146 It is made available to make it easier for users to serialize expressions back and forth between
1147 strings. Solvers can be serialized using the 'sexpr()' method.
1151 if len(s.assertions()) != 1:
1152 raise Z3Exception(
"single assertion expected")
1153 fml = s.assertions()[0]
1154 if fml.num_args() != 1:
1155 raise Z3Exception(
"dummy function 'F' expected")
1159 if isinstance(a, Pattern):
1163 if k == Z3_QUANTIFIER_AST:
1166 if sk == Z3_BOOL_SORT:
1168 if sk == Z3_INT_SORT:
1169 if k == Z3_NUMERAL_AST:
1172 if sk == Z3_REAL_SORT:
1173 if k == Z3_NUMERAL_AST:
1178 if sk == Z3_BV_SORT:
1179 if k == Z3_NUMERAL_AST:
1183 if sk == Z3_ARRAY_SORT:
1185 if sk == Z3_DATATYPE_SORT:
1187 if sk == Z3_FLOATING_POINT_SORT:
1191 return FPRef(a, ctx)
1192 if sk == Z3_FINITE_DOMAIN_SORT:
1193 if k == Z3_NUMERAL_AST:
1197 if sk == Z3_ROUNDING_MODE_SORT:
1199 if sk == Z3_SEQ_SORT:
1201 if sk == Z3_CHAR_SORT:
1203 if sk == Z3_RE_SORT:
1204 return ReRef(a, ctx)
1221 _z3_assert(s1.ctx == s.ctx,
"context mismatch")
1231 if isinstance(a, str)
and isinstance(b, SeqRef):
1233 if isinstance(b, str)
and isinstance(a, SeqRef):
1235 if isinstance(a, float)
and isinstance(b, ArithRef):
1237 if isinstance(b, float)
and isinstance(a, ArithRef):
1250 for element
in sequence:
1251 result = func(result, element)
1262 alist = [
_py2expr(a, ctx)
for a
in alist]
1263 s =
_reduce(_coerce_expr_merge, alist,
None)
1264 return [s.cast(a)
for a
in alist]
1268 """Return `True` if `a` is a Z3 expression.
1275 >>> is_expr(IntSort())
1279 >>> is_expr(IntVal(1))
1282 >>> is_expr(ForAll(x, x >= 0))
1284 >>> is_expr(FPVal(1.0))
1287 return isinstance(a, ExprRef)
1291 """Return `True` if `a` is a Z3 function application.
1293 Note that, constants are function applications with 0 arguments.
1300 >>> is_app(IntSort())
1304 >>> is_app(IntVal(1))
1307 >>> is_app(ForAll(x, x >= 0))
1310 if not isinstance(a, ExprRef):
1313 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
1317 """Return `True` if `a` is Z3 constant/variable expression.
1326 >>> is_const(IntVal(1))
1329 >>> is_const(ForAll(x, x >= 0))
1332 return is_app(a)
and a.num_args() == 0
1336 """Return `True` if `a` is variable.
1338 Z3 uses de-Bruijn indices for representing bound variables in
1346 >>> f = Function('f', IntSort(), IntSort())
1347 >>> # Z3 replaces x with bound variables when ForAll is executed.
1348 >>> q = ForAll(x, f(x) == x)
1354 >>> is_var(b.arg(1))
1361 """Return the de-Bruijn index of the Z3 bounded variable `a`.
1369 >>> f = Function('f', IntSort(), IntSort(), IntSort())
1370 >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1371 >>> q = ForAll([x, y], f(x, y) == x + y)
1373 f(Var(1), Var(0)) == Var(1) + Var(0)
1377 >>> v1 = b.arg(0).arg(0)
1378 >>> v2 = b.arg(0).arg(1)
1383 >>> get_var_index(v1)
1385 >>> get_var_index(v2)
1394 """Return `True` if `a` is an application of the given kind `k`.
1398 >>> is_app_of(n, Z3_OP_ADD)
1400 >>> is_app_of(n, Z3_OP_MUL)
1403 return is_app(a)
and a.kind() == k
1406def If(a, b, c, ctx=None):
1407 """Create a Z3 if-then-else expression.
1411 >>> max = If(x > y, x, y)
1417 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1418 return Cond(a, b, c, ctx)
1425 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1430 """Create a Z3 distinct expression.
1437 >>> Distinct(x, y, z)
1439 >>> simplify(Distinct(x, y, z))
1441 >>> simplify(Distinct(x, y, z), blast_distinct=True)
1442 And(Not(x == y), Not(x == z), Not(y == z))
1447 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1456 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1457 args[0] = a.as_ast()
1458 args[1] = b.as_ast()
1459 return f(a.ctx.ref(), 2, args)
1463 """Create a constant of the given sort.
1465 >>> Const('x', IntSort())
1469 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
1475 """Create several constants of the given sort.
1477 `names` is a string containing the names of all constants to be created.
1478 Blank spaces separate the names of different constants.
1480 >>> x, y, z = Consts('x y z', IntSort())
1484 if isinstance(names, str):
1485 names = names.split(
" ")
1486 return [
Const(name, sort)
for name
in names]
1490 """Create a fresh constant of a specified sort"""
1496 """Create a Z3 free variable. Free variables are used to create quantified formulas.
1497 A free variable with index n is bound when it occurs within the scope of n+1 quantified
1500 >>> Var(0, IntSort())
1502 >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1512 Create a real free variable. Free variables are used to create quantified formulas.
1513 They are also used to create polynomials.
1523 Create a list of Real free variables.
1524 The variables have ids: 0, 1, ..., n-1
1526 >>> x0, x1, x2, x3 = RealVarVector(4)
1530 return [
RealVar(i, ctx)
for i
in range(n)]
1543 """Try to cast `val` as a Boolean.
1545 >>> x = BoolSort().cast(True)
1555 if isinstance(val, bool):
1559 msg =
"True, False or Z3 Boolean expression expected. Received %s of type %s"
1561 if not self.
eq(val.sort()):
1562 _z3_assert(self.
eq(val.sort()),
"Value cannot be converted into a Z3 Boolean value")
1566 return isinstance(other, ArithSortRef)
1576 """All Boolean expressions are instances of this class."""
1582 if isinstance(other, BoolRef):
1583 other =
If(other, 1, 0)
1584 return If(self, 1, 0) + other
1593 """Create the Z3 expression `self * other`.
1595 if isinstance(other, int)
and other == 1:
1596 return If(self, 1, 0)
1597 if isinstance(other, int)
and other == 0:
1599 if isinstance(other, BoolRef):
1600 other =
If(other, 1, 0)
1601 return If(self, other, 0)
1604 return And(self, other)
1607 return Or(self, other)
1610 return Xor(self, other)
1619 """Return `True` if `a` is a Z3 Boolean expression.
1625 >>> is_bool(And(p, q))
1633 return isinstance(a, BoolRef)
1637 """Return `True` if `a` is the Z3 true expression.
1642 >>> is_true(simplify(p == p))
1647 >>> # True is a Python Boolean expression
1655 """Return `True` if `a` is the Z3 false expression.
1662 >>> is_false(BoolVal(False))
1669 """Return `True` if `a` is a Z3 and expression.
1671 >>> p, q = Bools('p q')
1672 >>> is_and(And(p, q))
1674 >>> is_and(Or(p, q))
1681 """Return `True` if `a` is a Z3 or expression.
1683 >>> p, q = Bools('p q')
1686 >>> is_or(And(p, q))
1693 """Return `True` if `a` is a Z3 implication expression.
1695 >>> p, q = Bools('p q')
1696 >>> is_implies(Implies(p, q))
1698 >>> is_implies(And(p, q))
1705 """Return `True` if `a` is a Z3 not expression.
1717 """Return `True` if `a` is a Z3 equality expression.
1719 >>> x, y = Ints('x y')
1727 """Return `True` if `a` is a Z3 distinct expression.
1729 >>> x, y, z = Ints('x y z')
1730 >>> is_distinct(x == y)
1732 >>> is_distinct(Distinct(x, y, z))
1739 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1743 >>> p = Const('p', BoolSort())
1746 >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1749 >>> is_bool(r(0, 1))
1757 """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
1761 >>> is_true(BoolVal(True))
1765 >>> is_false(BoolVal(False))
1776 """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
1788 """Return a tuple of Boolean constants.
1790 `names` is a single string containing all names separated by blank spaces.
1791 If `ctx=None`, then the global context is used.
1793 >>> p, q, r = Bools('p q r')
1794 >>> And(p, Or(q, r))
1798 if isinstance(names, str):
1799 names = names.split(
" ")
1800 return [
Bool(name, ctx)
for name
in names]
1804 """Return a list of Boolean constants of size `sz`.
1806 The constants are named using the given prefix.
1807 If `ctx=None`, then the global context is used.
1809 >>> P = BoolVector('p', 3)
1813 And(p__0, p__1, p__2)
1815 return [
Bool(
"%s__%s" % (prefix, i))
for i
in range(sz)]
1819 """Return a fresh Boolean constant in the given context using the given prefix.
1821 If `ctx=None`, then the global context is used.
1823 >>> b1 = FreshBool()
1824 >>> b2 = FreshBool()
1833 """Create a Z3 implies expression.
1835 >>> p, q = Bools('p q')
1847 """Create a Z3 Xor expression.
1849 >>> p, q = Bools('p q')
1852 >>> simplify(Xor(p, q))
1863 """Create a Z3 not expression or probe.
1868 >>> simplify(Not(Not(p)))
1889 """Return `True` if one of the elements of the given collection is a Z3 probe."""
1897 """Create a Z3 and-expression or and-probe.
1899 >>> p, q, r = Bools('p q r')
1902 >>> P = BoolVector('p', 5)
1904 And(p__0, p__1, p__2, p__3, p__4)
1908 last_arg = args[len(args) - 1]
1909 if isinstance(last_arg, Context):
1910 ctx = args[len(args) - 1]
1911 args = args[:len(args) - 1]
1912 elif len(args) == 1
and isinstance(args[0], AstVector):
1914 args = [a
for a
in args[0]]
1920 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1930 """Create a Z3 or-expression or or-probe.
1932 >>> p, q, r = Bools('p q r')
1935 >>> P = BoolVector('p', 5)
1937 Or(p__0, p__1, p__2, p__3, p__4)
1941 last_arg = args[len(args) - 1]
1942 if isinstance(last_arg, Context):
1943 ctx = args[len(args) - 1]
1944 args = args[:len(args) - 1]
1945 elif len(args) == 1
and isinstance(args[0], AstVector):
1947 args = [a
for a
in args[0]]
1953 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1969 """Patterns are hints for quantifier instantiation.
1981 """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1983 >>> f = Function('f', IntSort(), IntSort())
1985 >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1987 ForAll(x, f(x) == 0)
1988 >>> q.num_patterns()
1990 >>> is_pattern(q.pattern(0))
1995 return isinstance(a, PatternRef)
1999 """Create a Z3 multi-pattern using the given expressions `*args`
2001 >>> f = Function('f', IntSort(), IntSort())
2002 >>> g = Function('g', IntSort(), IntSort())
2004 >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
2006 ForAll(x, f(x) != g(x))
2007 >>> q.num_patterns()
2009 >>> is_pattern(q.pattern(0))
2012 MultiPattern(f(Var(0)), g(Var(0)))
2015 _z3_assert(len(args) > 0,
"At least one argument expected")
2036 """Universally and Existentially quantified formulas."""
2045 """Return the Boolean sort or sort of Lambda."""
2051 """Return `True` if `self` is a universal quantifier.
2053 >>> f = Function('f', IntSort(), IntSort())
2055 >>> q = ForAll(x, f(x) == 0)
2058 >>> q = Exists(x, f(x) != 0)
2065 """Return `True` if `self` is an existential quantifier.
2067 >>> f = Function('f', IntSort(), IntSort())
2069 >>> q = ForAll(x, f(x) == 0)
2072 >>> q = Exists(x, f(x) != 0)
2079 """Return `True` if `self` is a lambda expression.
2081 >>> f = Function('f', IntSort(), IntSort())
2083 >>> q = Lambda(x, f(x))
2086 >>> q = Exists(x, f(x) != 0)
2093 """Return the Z3 expression `self[arg]`.
2100 """Return the weight annotation of `self`.
2102 >>> f = Function('f', IntSort(), IntSort())
2104 >>> q = ForAll(x, f(x) == 0)
2107 >>> q = ForAll(x, f(x) == 0, weight=10)
2114 """Return the skolem id of `self`.
2119 """Return the quantifier id of `self`.
2124 """Return the number of patterns (i.e., quantifier instantiation hints) in `self`.
2126 >>> f = Function('f', IntSort(), IntSort())
2127 >>> g = Function('g', IntSort(), IntSort())
2129 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2130 >>> q.num_patterns()
2136 """Return a pattern (i.e., quantifier instantiation hints) in `self`.
2138 >>> f = Function('f', IntSort(), IntSort())
2139 >>> g = Function('g', IntSort(), IntSort())
2141 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
2142 >>> q.num_patterns()
2154 """Return the number of no-patterns."""
2158 """Return a no-pattern."""
2164 """Return the expression being quantified.
2166 >>> f = Function('f', IntSort(), IntSort())
2168 >>> q = ForAll(x, f(x) == 0)
2175 """Return the number of variables bounded by this quantifier.
2177 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2180 >>> q = ForAll([x, y], f(x, y) >= x)
2187 """Return a string representing a name used when displaying the quantifier.
2189 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2192 >>> q = ForAll([x, y], f(x, y) >= x)
2203 """Return the sort of a bound variable.
2205 >>> f = Function('f', IntSort(), RealSort(), IntSort())
2208 >>> q = ForAll([x, y], f(x, y) >= x)
2219 """Return a list containing a single element self.body()
2221 >>> f = Function('f', IntSort(), IntSort())
2223 >>> q = ForAll(x, f(x) == 0)
2227 return [self.
body()]
2231 """Return `True` if `a` is a Z3 quantifier.
2233 >>> f = Function('f', IntSort(), IntSort())
2235 >>> q = ForAll(x, f(x) == 0)
2236 >>> is_quantifier(q)
2238 >>> is_quantifier(f(x))
2241 return isinstance(a, QuantifierRef)
2244def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2249 _z3_assert(all([
is_expr(p)
for p
in no_patterns]),
"no patterns are Z3 expressions")
2260 _vs = (Ast * num_vars)()
2261 for i
in range(num_vars):
2263 _vs[i] = vs[i].as_ast()
2265 num_pats = len(patterns)
2266 _pats = (Pattern * num_pats)()
2267 for i
in range(num_pats):
2268 _pats[i] = patterns[i].ast
2275 num_no_pats, _no_pats,
2276 body.as_ast()), ctx)
2279def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2280 """Create a Z3 forall formula.
2282 The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2284 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2287 >>> ForAll([x, y], f(x, y) >= x)
2288 ForAll([x, y], f(x, y) >= x)
2289 >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2290 ForAll([x, y], f(x, y) >= x)
2291 >>> ForAll([x, y], f(x, y) >= x, weight=10)
2292 ForAll([x, y], f(x, y) >= x)
2294 return _mk_quantifier(
True, vs, body, weight, qid, skid, patterns, no_patterns)
2297def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2298 """Create a Z3 exists formula.
2300 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2303 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2306 >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2308 Exists([x, y], f(x, y) >= x)
2309 >>> is_quantifier(q)
2311 >>> r = Tactic('nnf')(q).as_expr()
2312 >>> is_quantifier(r)
2315 return _mk_quantifier(
False, vs, body, weight, qid, skid, patterns, no_patterns)
2319 """Create a Z3 lambda expression.
2321 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2322 >>> mem0 = Array('mem0', IntSort(), IntSort())
2323 >>> lo, hi, e, i = Ints('lo hi e i')
2324 >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
2326 Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
2332 _vs = (Ast * num_vars)()
2333 for i
in range(num_vars):
2335 _vs[i] = vs[i].as_ast()
2346 """Real and Integer sorts."""
2349 """Return `True` if `self` is of the sort Real.
2354 >>> (x + 1).is_real()
2360 return self.
kind() == Z3_REAL_SORT
2363 """Return `True` if `self` is of the sort Integer.
2368 >>> (x + 1).is_int()
2374 return self.
kind() == Z3_INT_SORT
2380 """Return `True` if `self` is a subsort of `other`."""
2384 """Try to cast `val` as an Integer or Real.
2386 >>> IntSort().cast(10)
2388 >>> is_int(IntSort().cast(10))
2392 >>> RealSort().cast(10)
2394 >>> is_real(RealSort().cast(10))
2403 if val_s.is_int()
and self.
is_real():
2405 if val_s.is_bool()
and self.
is_int():
2406 return If(val, 1, 0)
2407 if val_s.is_bool()
and self.
is_real():
2410 _z3_assert(
False,
"Z3 Integer/Real expression expected")
2417 msg =
"int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s"
2422 """Return `True` if s is an arithmetical sort (type).
2424 >>> is_arith_sort(IntSort())
2426 >>> is_arith_sort(RealSort())
2428 >>> is_arith_sort(BoolSort())
2430 >>> n = Int('x') + 1
2431 >>> is_arith_sort(n.sort())
2434 return isinstance(s, ArithSortRef)
2438 """Integer and Real expressions."""
2441 """Return the sort (type) of the arithmetical expression `self`.
2445 >>> (Real('x') + 1).sort()
2451 """Return `True` if `self` is an integer expression.
2456 >>> (x + 1).is_int()
2459 >>> (x + y).is_int()
2465 """Return `True` if `self` is an real expression.
2470 >>> (x + 1).is_real()
2476 """Create the Z3 expression `self + other`.
2489 """Create the Z3 expression `other + self`.
2499 """Create the Z3 expression `self * other`.
2508 if isinstance(other, BoolRef):
2509 return If(other, self, 0)
2514 """Create the Z3 expression `other * self`.
2524 """Create the Z3 expression `self - other`.
2537 """Create the Z3 expression `other - self`.
2547 """Create the Z3 expression `self**other` (** is the power operator).
2554 >>> simplify(IntVal(2)**8)
2561 """Create the Z3 expression `other**self` (** is the power operator).
2568 >>> simplify(2**IntVal(8))
2575 """Create the Z3 expression `other/self`.
2598 """Create the Z3 expression `other/self`."""
2602 """Create the Z3 expression `other/self`.
2619 """Create the Z3 expression `other/self`."""
2623 """Create the Z3 expression `other%self`.
2629 >>> simplify(IntVal(10) % IntVal(3))
2634 _z3_assert(a.is_int(),
"Z3 integer expression expected")
2638 """Create the Z3 expression `other%self`.
2646 _z3_assert(a.is_int(),
"Z3 integer expression expected")
2650 """Return an expression representing `-self`.
2670 """Create the Z3 expression `other <= self`.
2672 >>> x, y = Ints('x y')
2683 """Create the Z3 expression `other < self`.
2685 >>> x, y = Ints('x y')
2696 """Create the Z3 expression `other > self`.
2698 >>> x, y = Ints('x y')
2709 """Create the Z3 expression `other >= self`.
2711 >>> x, y = Ints('x y')
2723 """Return `True` if `a` is an arithmetical expression.
2732 >>> is_arith(IntVal(1))
2740 return isinstance(a, ArithRef)
2744 """Return `True` if `a` is an integer expression.
2751 >>> is_int(IntVal(1))
2763 """Return `True` if `a` is a real expression.
2775 >>> is_real(RealVal(1))
2790 """Return `True` if `a` is an integer value of sort Int.
2792 >>> is_int_value(IntVal(1))
2796 >>> is_int_value(Int('x'))
2798 >>> n = Int('x') + 1
2803 >>> is_int_value(n.arg(1))
2805 >>> is_int_value(RealVal("1/3"))
2807 >>> is_int_value(RealVal(1))
2814 """Return `True` if `a` is rational value of sort Real.
2816 >>> is_rational_value(RealVal(1))
2818 >>> is_rational_value(RealVal("3/5"))
2820 >>> is_rational_value(IntVal(1))
2822 >>> is_rational_value(1)
2824 >>> n = Real('x') + 1
2827 >>> is_rational_value(n.arg(1))
2829 >>> is_rational_value(Real('x'))
2836 """Return `True` if `a` is an algebraic value of sort Real.
2838 >>> is_algebraic_value(RealVal("3/5"))
2840 >>> n = simplify(Sqrt(2))
2843 >>> is_algebraic_value(n)
2850 """Return `True` if `a` is an expression of the form b + c.
2852 >>> x, y = Ints('x y')
2862 """Return `True` if `a` is an expression of the form b * c.
2864 >>> x, y = Ints('x y')
2874 """Return `True` if `a` is an expression of the form b - c.
2876 >>> x, y = Ints('x y')
2886 """Return `True` if `a` is an expression of the form b / c.
2888 >>> x, y = Reals('x y')
2893 >>> x, y = Ints('x y')
2903 """Return `True` if `a` is an expression of the form b div c.
2905 >>> x, y = Ints('x y')
2915 """Return `True` if `a` is an expression of the form b % c.
2917 >>> x, y = Ints('x y')
2927 """Return `True` if `a` is an expression of the form b <= c.
2929 >>> x, y = Ints('x y')
2939 """Return `True` if `a` is an expression of the form b < c.
2941 >>> x, y = Ints('x y')
2951 """Return `True` if `a` is an expression of the form b >= c.
2953 >>> x, y = Ints('x y')
2963 """Return `True` if `a` is an expression of the form b > c.
2965 >>> x, y = Ints('x y')
2975 """Return `True` if `a` is an expression of the form IsInt(b).
2978 >>> is_is_int(IsInt(x))
2987 """Return `True` if `a` is an expression of the form ToReal(b).
3002 """Return `True` if `a` is an expression of the form ToInt(b).
3017 """Integer values."""
3020 """Return a Z3 integer numeral as a Python long (bignum) numeral.
3033 """Return a Z3 integer numeral as a Python string.
3041 """Return a Z3 integer numeral as a Python binary string.
3043 >>> v.as_binary_string()
3050 """Rational values."""
3053 """ Return the numerator of a Z3 rational numeral.
3055 >>> is_rational_value(RealVal("3/5"))
3057 >>> n = RealVal("3/5")
3060 >>> is_rational_value(Q(3,5))
3062 >>> Q(3,5).numerator()
3068 """ Return the denominator of a Z3 rational numeral.
3070 >>> is_rational_value(Q(3,5))
3079 """ Return the numerator as a Python long.
3081 >>> v = RealVal(10000000000)
3086 >>> v.numerator_as_long() + 1 == 10000000001
3092 """ Return the denominator as a Python long.
3094 >>> v = RealVal("1/3")
3097 >>> v.denominator_as_long()
3116 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
3118 >>> v = RealVal("1/5")
3121 >>> v = RealVal("1/3")
3128 """Return a Z3 rational numeral as a Python string.
3137 """Return a Z3 rational as a Python Fraction object.
3139 >>> v = RealVal("1/5")
3147 """Algebraic irrational values."""
3150 """Return a Z3 rational number that approximates the algebraic number `self`.
3151 The result `r` is such that |r - self| <= 1/10^precision
3153 >>> x = simplify(Sqrt(2))
3155 6838717160008073720548335/4835703278458516698824704
3162 """Return a string representation of the algebraic number `self` in decimal notation
3163 using `prec` decimal places.
3165 >>> x = simplify(Sqrt(2))
3166 >>> x.as_decimal(10)
3168 >>> x.as_decimal(20)
3169 '1.41421356237309504880?'
3181 if isinstance(a, bool):
3185 if isinstance(a, float):
3187 if isinstance(a, str):
3192 _z3_assert(
False,
"Python bool, int, long or float expected")
3196 """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
3200 >>> x = Const('x', IntSort())
3203 >>> x.sort() == IntSort()
3205 >>> x.sort() == BoolSort()
3213 """Return the real sort in the given context. If `ctx=None`, then the global context is used.
3217 >>> x = Const('x', RealSort())
3222 >>> x.sort() == RealSort()
3230 if isinstance(val, float):
3231 return str(int(val))
3232 elif isinstance(val, bool):
3242 """Return a Z3 integer value. If `ctx=None`, then the global context is used.
3254 """Return a Z3 real value.
3256 `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
3257 If `ctx=None`, then the global context is used.
3261 >>> RealVal(1).sort()
3273 """Return a Z3 rational a/b.
3275 If `ctx=None`, then the global context is used.
3279 >>> RatVal(3,5).sort()
3283 _z3_assert(
_is_int(a)
or isinstance(a, str),
"First argument cannot be converted into an integer")
3284 _z3_assert(
_is_int(b)
or isinstance(b, str),
"Second argument cannot be converted into an integer")
3288def Q(a, b, ctx=None):
3289 """Return a Z3 rational a/b.
3291 If `ctx=None`, then the global context is used.
3302 """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
3315 """Return a tuple of Integer constants.
3317 >>> x, y, z = Ints('x y z')
3322 if isinstance(names, str):
3323 names = names.split(
" ")
3324 return [
Int(name, ctx)
for name
in names]
3328 """Return a list of integer constants of size `sz`.
3330 >>> X = IntVector('x', 3)
3337 return [
Int(
"%s__%s" % (prefix, i), ctx)
for i
in range(sz)]
3341 """Return a fresh integer constant in the given context using the given prefix.
3355 """Return a real constant named `name`. If `ctx=None`, then the global context is used.
3368 """Return a tuple of real constants.
3370 >>> x, y, z = Reals('x y z')
3373 >>> Sum(x, y, z).sort()
3377 if isinstance(names, str):
3378 names = names.split(
" ")
3379 return [
Real(name, ctx)
for name
in names]
3383 """Return a list of real constants of size `sz`.
3385 >>> X = RealVector('x', 3)
3394 return [
Real(
"%s__%s" % (prefix, i), ctx)
for i
in range(sz)]
3398 """Return a fresh real constant in the given context using the given prefix.
3412 """ Return the Z3 expression ToReal(a).
3424 _z3_assert(a.is_int(),
"Z3 integer expression expected.")
3430 """ Return the Z3 expression ToInt(a).
3442 _z3_assert(a.is_real(),
"Z3 real expression expected.")
3448 """ Return the Z3 predicate IsInt(a).
3451 >>> IsInt(x + "1/2")
3453 >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
3455 >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
3459 _z3_assert(a.is_real(),
"Z3 real expression expected.")
3465 """ Return a Z3 expression which represents the square root of a.
3478 """ Return a Z3 expression which represents the cubic root of a.
3497 """Bit-vector sort."""
3500 """Return the size (number of bits) of the bit-vector sort `self`.
3502 >>> b = BitVecSort(32)
3512 """Try to cast `val` as a Bit-Vector.
3514 >>> b = BitVecSort(32)
3517 >>> b.cast(10).sexpr()
3530 """Return True if `s` is a Z3 bit-vector sort.
3532 >>> is_bv_sort(BitVecSort(32))
3534 >>> is_bv_sort(IntSort())
3537 return isinstance(s, BitVecSortRef)
3541 """Bit-vector expressions."""
3544 """Return the sort of the bit-vector expression `self`.
3546 >>> x = BitVec('x', 32)
3549 >>> x.sort() == BitVecSort(32)
3555 """Return the number of bits of the bit-vector expression `self`.
3557 >>> x = BitVec('x', 32)
3560 >>> Concat(x, x).size()
3566 """Create the Z3 expression `self + other`.
3568 >>> x = BitVec('x', 32)
3569 >>> y = BitVec('y', 32)
3579 """Create the Z3 expression `other + self`.
3581 >>> x = BitVec('x', 32)
3589 """Create the Z3 expression `self * other`.
3591 >>> x = BitVec('x', 32)
3592 >>> y = BitVec('y', 32)
3602 """Create the Z3 expression `other * self`.
3604 >>> x = BitVec('x', 32)
3612 """Create the Z3 expression `self - other`.
3614 >>> x = BitVec('x', 32)
3615 >>> y = BitVec('y', 32)
3625 """Create the Z3 expression `other - self`.
3627 >>> x = BitVec('x', 32)
3635 """Create the Z3 expression bitwise-or `self | other`.
3637 >>> x = BitVec('x', 32)
3638 >>> y = BitVec('y', 32)
3648 """Create the Z3 expression bitwise-or `other | self`.
3650 >>> x = BitVec('x', 32)
3658 """Create the Z3 expression bitwise-and `self & other`.
3660 >>> x = BitVec('x', 32)
3661 >>> y = BitVec('y', 32)
3671 """Create the Z3 expression bitwise-or `other & self`.
3673 >>> x = BitVec('x', 32)
3681 """Create the Z3 expression bitwise-xor `self ^ other`.
3683 >>> x = BitVec('x', 32)
3684 >>> y = BitVec('y', 32)
3694 """Create the Z3 expression bitwise-xor `other ^ self`.
3696 >>> x = BitVec('x', 32)
3706 >>> x = BitVec('x', 32)
3713 """Return an expression representing `-self`.
3715 >>> x = BitVec('x', 32)
3724 """Create the Z3 expression bitwise-not `~self`.
3726 >>> x = BitVec('x', 32)
3735 """Create the Z3 expression (signed) division `self / other`.
3737 Use the function UDiv() for unsigned division.
3739 >>> x = BitVec('x', 32)
3740 >>> y = BitVec('y', 32)
3747 >>> UDiv(x, y).sexpr()
3754 """Create the Z3 expression (signed) division `self / other`."""
3758 """Create the Z3 expression (signed) division `other / self`.
3760 Use the function UDiv() for unsigned division.
3762 >>> x = BitVec('x', 32)
3765 >>> (10 / x).sexpr()
3766 '(bvsdiv #x0000000a x)'
3767 >>> UDiv(10, x).sexpr()
3768 '(bvudiv #x0000000a x)'
3774 """Create the Z3 expression (signed) division `other / self`."""
3778 """Create the Z3 expression (signed) mod `self % other`.
3780 Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3782 >>> x = BitVec('x', 32)
3783 >>> y = BitVec('y', 32)
3790 >>> URem(x, y).sexpr()
3792 >>> SRem(x, y).sexpr()
3799 """Create the Z3 expression (signed) mod `other % self`.
3801 Use the function URem() for unsigned remainder, and SRem() for signed remainder.
3803 >>> x = BitVec('x', 32)
3806 >>> (10 % x).sexpr()
3807 '(bvsmod #x0000000a x)'
3808 >>> URem(10, x).sexpr()
3809 '(bvurem #x0000000a x)'
3810 >>> SRem(10, x).sexpr()
3811 '(bvsrem #x0000000a x)'
3817 """Create the Z3 expression (signed) `other <= self`.
3819 Use the function ULE() for unsigned less than or equal to.
3821 >>> x, y = BitVecs('x y', 32)
3824 >>> (x <= y).sexpr()
3826 >>> ULE(x, y).sexpr()
3833 """Create the Z3 expression (signed) `other < self`.
3835 Use the function ULT() for unsigned less than.
3837 >>> x, y = BitVecs('x y', 32)
3842 >>> ULT(x, y).sexpr()
3849 """Create the Z3 expression (signed) `other > self`.
3851 Use the function UGT() for unsigned greater than.
3853 >>> x, y = BitVecs('x y', 32)
3858 >>> UGT(x, y).sexpr()
3865 """Create the Z3 expression (signed) `other >= self`.
3867 Use the function UGE() for unsigned greater than or equal to.
3869 >>> x, y = BitVecs('x y', 32)
3872 >>> (x >= y).sexpr()
3874 >>> UGE(x, y).sexpr()
3881 """Create the Z3 expression (arithmetical) right shift `self >> other`
3883 Use the function LShR() for the right logical shift
3885 >>> x, y = BitVecs('x y', 32)
3888 >>> (x >> y).sexpr()
3890 >>> LShR(x, y).sexpr()
3894 >>> BitVecVal(4, 3).as_signed_long()
3896 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
3898 >>> simplify(BitVecVal(4, 3) >> 1)
3900 >>> simplify(LShR(BitVecVal(4, 3), 1))
3902 >>> simplify(BitVecVal(2, 3) >> 1)
3904 >>> simplify(LShR(BitVecVal(2, 3), 1))
3911 """Create the Z3 expression left shift `self << other`
3913 >>> x, y = BitVecs('x y', 32)
3916 >>> (x << y).sexpr()
3918 >>> simplify(BitVecVal(2, 3) << 1)
3925 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3927 Use the function LShR() for the right logical shift
3929 >>> x = BitVec('x', 32)
3932 >>> (10 >> x).sexpr()
3933 '(bvashr #x0000000a x)'
3939 """Create the Z3 expression left shift `other << self`.
3941 Use the function LShR() for the right logical shift
3943 >>> x = BitVec('x', 32)
3946 >>> (10 << x).sexpr()
3947 '(bvshl #x0000000a x)'
3954 """Bit-vector values."""
3957 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
3959 >>> v = BitVecVal(0xbadc0de, 32)
3962 >>> print("0x%.8x" % v.as_long())
3968 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
3969 The most significant bit is assumed to be the sign.
3971 >>> BitVecVal(4, 3).as_signed_long()
3973 >>> BitVecVal(7, 3).as_signed_long()
3975 >>> BitVecVal(3, 3).as_signed_long()
3977 >>> BitVecVal(2**32 - 1, 32).as_signed_long()
3979 >>> BitVecVal(2**64 - 1, 64).as_signed_long()
3984 if val >= 2**(sz - 1):
3986 if val < -2**(sz - 1):
3998 """Return `True` if `a` is a Z3 bit-vector expression.
4000 >>> b = BitVec('b', 32)
4008 return isinstance(a, BitVecRef)
4012 """Return `True` if `a` is a Z3 bit-vector numeral value.
4014 >>> b = BitVec('b', 32)
4017 >>> b = BitVecVal(10, 32)
4027 """Return the Z3 expression BV2Int(a).
4029 >>> b = BitVec('b', 3)
4030 >>> BV2Int(b).sort()
4035 >>> x > BV2Int(b, is_signed=False)
4037 >>> x > BV2Int(b, is_signed=True)
4038 x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
4039 >>> solve(x > BV2Int(b), b == 1, x < 3)
4043 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
4050 """Return the z3 expression Int2BV(a, num_bits).
4051 It is a bit-vector of width num_bits and represents the
4052 modulo of a by 2^num_bits
4059 """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
4061 >>> Byte = BitVecSort(8)
4062 >>> Word = BitVecSort(16)
4065 >>> x = Const('x', Byte)
4066 >>> eq(x, BitVec('x', 8))
4074 """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
4076 >>> v = BitVecVal(10, 32)
4079 >>> print("0x%.8x" % v.as_long())
4091 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
4092 If `ctx=None`, then the global context is used.
4094 >>> x = BitVec('x', 16)
4101 >>> word = BitVecSort(16)
4102 >>> x2 = BitVec('x', word)
4106 if isinstance(bv, BitVecSortRef):
4115 """Return a tuple of bit-vector constants of size bv.
4117 >>> x, y, z = BitVecs('x y z', 16)
4124 >>> Product(x, y, z)
4126 >>> simplify(Product(x, y, z))
4130 if isinstance(names, str):
4131 names = names.split(
" ")
4132 return [
BitVec(name, bv, ctx)
for name
in names]
4136 """Create a Z3 bit-vector concatenation expression.
4138 >>> v = BitVecVal(1, 4)
4139 >>> Concat(v, v+1, v)
4140 Concat(Concat(1, 1 + 1), 1)
4141 >>> simplify(Concat(v, v+1, v))
4143 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
4149 _z3_assert(sz >= 2,
"At least two arguments expected.")
4156 if is_seq(args[0])
or isinstance(args[0], str):
4159 _z3_assert(all([
is_seq(a)
for a
in args]),
"All arguments must be sequence expressions.")
4162 v[i] = args[i].as_ast()
4167 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
4170 v[i] = args[i].as_ast()
4174 _z3_assert(all([
is_bv(a)
for a
in args]),
"All arguments must be Z3 bit-vector expressions.")
4176 for i
in range(sz - 1):
4182 """Create a Z3 bit-vector extraction expression.
4183 Extract is overloaded to also work on sequence extraction.
4184 The functions SubString and SubSeq are redirected to Extract.
4185 For this case, the arguments are reinterpreted as:
4186 high - is a sequence (string)
4188 a - is the length to be extracted
4190 >>> x = BitVec('x', 8)
4191 >>> Extract(6, 2, x)
4193 >>> Extract(6, 2, x).sort()
4195 >>> simplify(Extract(StringVal("abcd"),2,1))
4198 if isinstance(high, str):
4205 _z3_assert(low <= high,
"First argument must be greater than or equal to second argument")
4207 "First and second arguments must be non negative integers")
4208 _z3_assert(
is_bv(a),
"Third argument must be a Z3 bit-vector expression")
4214 _z3_assert(
is_bv(a)
or is_bv(b),
"First or second argument must be a Z3 bit-vector expression")
4218 """Create the Z3 expression (unsigned) `other <= self`.
4220 Use the operator <= for signed less than or equal to.
4222 >>> x, y = BitVecs('x y', 32)
4225 >>> (x <= y).sexpr()
4227 >>> ULE(x, y).sexpr()
4236 """Create the Z3 expression (unsigned) `other < self`.
4238 Use the operator < for signed less than.
4240 >>> x, y = BitVecs('x y', 32)
4245 >>> ULT(x, y).sexpr()
4254 """Create the Z3 expression (unsigned) `other >= self`.
4256 Use the operator >= for signed greater than or equal to.
4258 >>> x, y = BitVecs('x y', 32)
4261 >>> (x >= y).sexpr()
4263 >>> UGE(x, y).sexpr()
4272 """Create the Z3 expression (unsigned) `other > self`.
4274 Use the operator > for signed greater than.
4276 >>> x, y = BitVecs('x y', 32)
4281 >>> UGT(x, y).sexpr()
4290 """Create the Z3 expression (unsigned) division `self / other`.
4292 Use the operator / for signed division.
4294 >>> x = BitVec('x', 32)
4295 >>> y = BitVec('y', 32)
4298 >>> UDiv(x, y).sort()
4302 >>> UDiv(x, y).sexpr()
4311 """Create the Z3 expression (unsigned) remainder `self % other`.
4313 Use the operator % for signed modulus, and SRem() for signed remainder.
4315 >>> x = BitVec('x', 32)
4316 >>> y = BitVec('y', 32)
4319 >>> URem(x, y).sort()
4323 >>> URem(x, y).sexpr()
4332 """Create the Z3 expression signed remainder.
4334 Use the operator % for signed modulus, and URem() for unsigned remainder.
4336 >>> x = BitVec('x', 32)
4337 >>> y = BitVec('y', 32)
4340 >>> SRem(x, y).sort()
4344 >>> SRem(x, y).sexpr()
4353 """Create the Z3 expression logical right shift.
4355 Use the operator >> for the arithmetical right shift.
4357 >>> x, y = BitVecs('x y', 32)
4360 >>> (x >> y).sexpr()
4362 >>> LShR(x, y).sexpr()
4366 >>> BitVecVal(4, 3).as_signed_long()
4368 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
4370 >>> simplify(BitVecVal(4, 3) >> 1)
4372 >>> simplify(LShR(BitVecVal(4, 3), 1))
4374 >>> simplify(BitVecVal(2, 3) >> 1)
4376 >>> simplify(LShR(BitVecVal(2, 3), 1))
4385 """Return an expression representing `a` rotated to the left `b` times.
4387 >>> a, b = BitVecs('a b', 16)
4388 >>> RotateLeft(a, b)
4390 >>> simplify(RotateLeft(a, 0))
4392 >>> simplify(RotateLeft(a, 16))
4401 """Return an expression representing `a` rotated to the right `b` times.
4403 >>> a, b = BitVecs('a b', 16)
4404 >>> RotateRight(a, b)
4406 >>> simplify(RotateRight(a, 0))
4408 >>> simplify(RotateRight(a, 16))
4417 """Return a bit-vector expression with `n` extra sign-bits.
4419 >>> x = BitVec('x', 16)
4420 >>> n = SignExt(8, x)
4427 >>> v0 = BitVecVal(2, 2)
4432 >>> v = simplify(SignExt(6, v0))
4437 >>> print("%.x" % v.as_long())
4442 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4447 """Return a bit-vector expression with `n` extra zero-bits.
4449 >>> x = BitVec('x', 16)
4450 >>> n = ZeroExt(8, x)
4457 >>> v0 = BitVecVal(2, 2)
4462 >>> v = simplify(ZeroExt(6, v0))
4470 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4475 """Return an expression representing `n` copies of `a`.
4477 >>> x = BitVec('x', 8)
4478 >>> n = RepeatBitVec(4, x)
4483 >>> v0 = BitVecVal(10, 4)
4484 >>> print("%.x" % v0.as_long())
4486 >>> v = simplify(RepeatBitVec(4, v0))
4489 >>> print("%.x" % v.as_long())
4494 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4499 """Return the reduction-and expression of `a`."""
4501 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
4506 """Return the reduction-or expression of `a`."""
4508 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
4513 """A predicate the determines that bit-vector addition does not overflow"""
4520 """A predicate the determines that signed bit-vector addition does not underflow"""
4527 """A predicate the determines that bit-vector subtraction does not overflow"""
4534 """A predicate the determines that bit-vector subtraction does not underflow"""
4541 """A predicate the determines that bit-vector signed division does not overflow"""
4548 """A predicate the determines that bit-vector unary negation does not overflow"""
4550 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
4555 """A predicate the determines that bit-vector multiplication does not overflow"""
4562 """A predicate the determines that bit-vector signed multiplication does not underflow"""
4578 """Return the domain of the array sort `self`.
4580 >>> A = ArraySort(IntSort(), BoolSort())
4587 """Return the domain of the array sort `self`.
4592 """Return the range of the array sort `self`.
4594 >>> A = ArraySort(IntSort(), BoolSort())
4602 """Array expressions. """
4605 """Return the array sort of the array expression `self`.
4607 >>> a = Array('a', IntSort(), BoolSort())
4614 """Shorthand for `self.sort().domain()`.
4616 >>> a = Array('a', IntSort(), BoolSort())
4623 """Shorthand for self.sort().domain_n(i)`."""
4627 """Shorthand for `self.sort().range()`.
4629 >>> a = Array('a', IntSort(), BoolSort())
4636 """Return the Z3 expression `self[arg]`.
4638 >>> a = Array('a', IntSort(), BoolSort())
4652 if isinstance(arg, tuple):
4653 args = [ar.sort().domain_n(i).cast(arg[i])
for i
in range(len(arg))]
4656 arg = ar.sort().domain().cast(arg)
4665 """Return `True` if `a` is a Z3 array expression.
4667 >>> a = Array('a', IntSort(), IntSort())
4670 >>> is_array(Store(a, 0, 1))
4675 return isinstance(a, ArrayRef)
4679 """Return `True` if `a` is a Z3 constant array.
4681 >>> a = K(IntSort(), 10)
4682 >>> is_const_array(a)
4684 >>> a = Array('a', IntSort(), IntSort())
4685 >>> is_const_array(a)
4692 """Return `True` if `a` is a Z3 constant array.
4694 >>> a = K(IntSort(), 10)
4697 >>> a = Array('a', IntSort(), IntSort())
4705 """Return `True` if `a` is a Z3 map array expression.
4707 >>> f = Function('f', IntSort(), IntSort())
4708 >>> b = Array('b', IntSort(), IntSort())
4721 """Return `True` if `a` is a Z3 default array expression.
4722 >>> d = Default(K(IntSort(), 10))
4726 return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4730 """Return the function declaration associated with a Z3 map array expression.
4732 >>> f = Function('f', IntSort(), IntSort())
4733 >>> b = Array('b', IntSort(), IntSort())
4735 >>> eq(f, get_map_func(a))
4739 >>> get_map_func(a)(0)
4754 """Return the Z3 array sort with the given domain and range sorts.
4756 >>> A = ArraySort(IntSort(), BoolSort())
4763 >>> AA = ArraySort(IntSort(), A)
4765 Array(Int, Array(Int, Bool))
4769 _z3_assert(len(sig) > 1,
"At least two arguments expected")
4770 arity = len(sig) - 1
4776 _z3_assert(s.ctx == r.ctx,
"Context mismatch")
4780 dom = (Sort * arity)()
4781 for i
in range(arity):
4787 """Return an array constant named `name` with the given domain and range sorts.
4789 >>> a = Array('a', IntSort(), IntSort())
4801 """Return a Z3 store array expression.
4803 >>> a = Array('a', IntSort(), IntSort())
4804 >>> i, v = Ints('i v')
4805 >>> s = Update(a, i, v)
4808 >>> prove(s[i] == v)
4811 >>> prove(Implies(i != j, s[j] == a[j]))
4819 raise Z3Exception(
"array update requires index and value arguments")
4823 i = a.sort().domain().cast(i)
4824 v = a.sort().range().cast(v)
4826 v = a.sort().range().cast(args[-1])
4827 idxs = [a.sort().domain_n(i).cast(args[i])
for i
in range(len(args)-1)]
4833 """ Return a default value for array expression.
4834 >>> b = K(IntSort(), 1)
4835 >>> prove(Default(b) == 1)
4844 """Return a Z3 store array expression.
4846 >>> a = Array('a', IntSort(), IntSort())
4847 >>> i, v = Ints('i v')
4848 >>> s = Store(a, i, v)
4851 >>> prove(s[i] == v)
4854 >>> prove(Implies(i != j, s[j] == a[j]))
4861 """Return a Z3 select array expression.
4863 >>> a = Array('a', IntSort(), IntSort())
4867 >>> eq(Select(a, i), a[i])
4877 """Return a Z3 map array expression.
4879 >>> f = Function('f', IntSort(), IntSort(), IntSort())
4880 >>> a1 = Array('a1', IntSort(), IntSort())
4881 >>> a2 = Array('a2', IntSort(), IntSort())
4882 >>> b = Map(f, a1, a2)
4885 >>> prove(b[0] == f(a1[0], a2[0]))
4890 _z3_assert(len(args) > 0,
"At least one Z3 array expression expected")
4893 _z3_assert(len(args) == f.arity(),
"Number of arguments mismatch")
4900 """Return a Z3 constant array expression.
4902 >>> a = K(IntSort(), 10)
4922 """Return extensionality index for one-dimensional arrays.
4923 >> a, b = Consts('a b', SetSort(IntSort()))
4940 """Return `True` if `a` is a Z3 array select application.
4942 >>> a = Array('a', IntSort(), IntSort())
4953 """Return `True` if `a` is a Z3 array store application.
4955 >>> a = Array('a', IntSort(), IntSort())
4958 >>> is_store(Store(a, 0, 1))
4971 """ Create a set sort over element sort s"""
4976 """Create the empty set
4977 >>> EmptySet(IntSort())
4985 """Create the full set
4986 >>> FullSet(IntSort())
4994 """ Take the union of sets
4995 >>> a = Const('a', SetSort(IntSort()))
4996 >>> b = Const('b', SetSort(IntSort()))
5007 """ Take the union of sets
5008 >>> a = Const('a', SetSort(IntSort()))
5009 >>> b = Const('b', SetSort(IntSort()))
5010 >>> SetIntersect(a, b)
5020 """ Add element e to set s
5021 >>> a = Const('a', SetSort(IntSort()))
5031 """ Remove element e to set s
5032 >>> a = Const('a', SetSort(IntSort()))
5042 """ The complement of set s
5043 >>> a = Const('a', SetSort(IntSort()))
5044 >>> SetComplement(a)
5052 """ The set difference of a and b
5053 >>> a = Const('a', SetSort(IntSort()))
5054 >>> b = Const('b', SetSort(IntSort()))
5055 >>> SetDifference(a, b)
5063 """ Check if e is a member of set s
5064 >>> a = Const('a', SetSort(IntSort()))
5074 """ Check if a is a subset of b
5075 >>> a = Const('a', SetSort(IntSort()))
5076 >>> b = Const('b', SetSort(IntSort()))
5091 """Return `True` if acc is pair of the form (String, Datatype or Sort). """
5092 if not isinstance(acc, tuple):
5096 return isinstance(acc[0], str)
and (isinstance(acc[1], Datatype)
or is_sort(acc[1]))
5100 """Helper class for declaring Z3 datatypes.
5102 >>> List = Datatype('List')
5103 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5104 >>> List.declare('nil')
5105 >>> List = List.create()
5106 >>> # List is now a Z3 declaration
5109 >>> List.cons(10, List.nil)
5111 >>> List.cons(10, List.nil).sort()
5113 >>> cons = List.cons
5117 >>> n = cons(1, cons(0, nil))
5119 cons(1, cons(0, nil))
5120 >>> simplify(cdr(n))
5122 >>> simplify(car(n))
5138 _z3_assert(isinstance(name, str),
"String expected")
5139 _z3_assert(isinstance(rec_name, str),
"String expected")
5142 "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)",
5147 """Declare constructor named `name` with the given accessors `args`.
5148 Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort
5149 or a reference to the datatypes being declared.
5151 In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
5152 declares the constructor named `cons` that builds a new List using an integer and a List.
5153 It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer
5154 of a `cons` cell, and `cdr` the list of a `cons` cell. After all constructors were declared,
5155 we use the method create() to create the actual datatype in Z3.
5157 >>> List = Datatype('List')
5158 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5159 >>> List.declare('nil')
5160 >>> List = List.create()
5163 _z3_assert(isinstance(name, str),
"String expected")
5164 _z3_assert(name !=
"",
"Constructor name cannot be empty")
5171 """Create a Z3 datatype based on the constructors declared using the method `declare()`.
5173 The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
5175 >>> List = Datatype('List')
5176 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5177 >>> List.declare('nil')
5178 >>> List = List.create()
5181 >>> List.cons(10, List.nil)
5188 """Auxiliary object used to create Z3 datatypes."""
5195 if self.
ctx.ref()
is not None and Z3_del_constructor
is not None:
5200 """Auxiliary object used to create Z3 datatypes."""
5207 if self.
ctx.ref()
is not None and Z3_del_constructor_list
is not None:
5212 """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
5214 In the following example we define a Tree-List using two mutually recursive datatypes.
5216 >>> TreeList = Datatype('TreeList')
5217 >>> Tree = Datatype('Tree')
5218 >>> # Tree has two constructors: leaf and node
5219 >>> Tree.declare('leaf', ('val', IntSort()))
5220 >>> # a node contains a list of trees
5221 >>> Tree.declare('node', ('children', TreeList))
5222 >>> TreeList.declare('nil')
5223 >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
5224 >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
5225 >>> Tree.val(Tree.leaf(10))
5227 >>> simplify(Tree.val(Tree.leaf(10)))
5229 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
5231 node(cons(leaf(10), cons(leaf(20), nil)))
5232 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
5233 >>> simplify(n2 == n1)
5235 >>> simplify(TreeList.car(Tree.children(n2)) == n1)
5240 _z3_assert(len(ds) > 0,
"At least one Datatype must be specified")
5241 _z3_assert(all([isinstance(d, Datatype)
for d
in ds]),
"Arguments must be Datatypes")
5242 _z3_assert(all([d.ctx == ds[0].ctx
for d
in ds]),
"Context mismatch")
5243 _z3_assert(all([d.constructors != []
for d
in ds]),
"Non-empty Datatypes expected")
5246 names = (Symbol * num)()
5247 out = (Sort * num)()
5248 clists = (ConstructorList * num)()
5250 for i
in range(num):
5253 num_cs = len(d.constructors)
5254 cs = (Constructor * num_cs)()
5255 for j
in range(num_cs):
5256 c = d.constructors[j]
5261 fnames = (Symbol * num_fs)()
5262 sorts = (Sort * num_fs)()
5263 refs = (ctypes.c_uint * num_fs)()
5264 for k
in range(num_fs):
5268 if isinstance(ftype, Datatype):
5271 ds.count(ftype) == 1,
5272 "One and only one occurrence of each datatype is expected",
5275 refs[k] = ds.index(ftype)
5279 sorts[k] = ftype.ast
5288 for i
in range(num):
5290 num_cs = dref.num_constructors()
5291 for j
in range(num_cs):
5292 cref = dref.constructor(j)
5293 cref_name = cref.name()
5294 cref_arity = cref.arity()
5295 if cref.arity() == 0:
5297 setattr(dref, cref_name, cref)
5298 rref = dref.recognizer(j)
5299 setattr(dref,
"is_" + cref_name, rref)
5300 for k
in range(cref_arity):
5301 aref = dref.accessor(j, k)
5302 setattr(dref, aref.name(), aref)
5304 return tuple(result)
5308 """Datatype sorts."""
5311 """Return the number of constructors in the given Z3 datatype.
5313 >>> List = Datatype('List')
5314 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5315 >>> List.declare('nil')
5316 >>> List = List.create()
5317 >>> # List is now a Z3 declaration
5318 >>> List.num_constructors()
5324 """Return a constructor of the datatype `self`.
5326 >>> List = Datatype('List')
5327 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5328 >>> List.declare('nil')
5329 >>> List = List.create()
5330 >>> # List is now a Z3 declaration
5331 >>> List.num_constructors()
5333 >>> List.constructor(0)
5335 >>> List.constructor(1)
5343 """In Z3, each constructor has an associated recognizer predicate.
5345 If the constructor is named `name`, then the recognizer `is_name`.
5347 >>> List = Datatype('List')
5348 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5349 >>> List.declare('nil')
5350 >>> List = List.create()
5351 >>> # List is now a Z3 declaration
5352 >>> List.num_constructors()
5354 >>> List.recognizer(0)
5356 >>> List.recognizer(1)
5358 >>> simplify(List.is_nil(List.cons(10, List.nil)))
5360 >>> simplify(List.is_cons(List.cons(10, List.nil)))
5362 >>> l = Const('l', List)
5363 >>> simplify(List.is_cons(l))
5371 """In Z3, each constructor has 0 or more accessor.
5372 The number of accessors is equal to the arity of the constructor.
5374 >>> List = Datatype('List')
5375 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5376 >>> List.declare('nil')
5377 >>> List = List.create()
5378 >>> List.num_constructors()
5380 >>> List.constructor(0)
5382 >>> num_accs = List.constructor(0).arity()
5385 >>> List.accessor(0, 0)
5387 >>> List.accessor(0, 1)
5389 >>> List.constructor(1)
5391 >>> num_accs = List.constructor(1).arity()
5405 """Datatype expressions."""
5408 """Return the datatype sort of the datatype expression `self`."""
5412 """Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""
5417 """Create a named tuple sort base on a set of underlying sorts
5419 >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])
5422 projects = [(
"project%d" % i, sorts[i])
for i
in range(len(sorts))]
5423 tuple.declare(name, *projects)
5424 tuple = tuple.create()
5425 return tuple, tuple.constructor(0), [tuple.accessor(0, i)
for i
in range(len(sorts))]
5429 """Create a named tagged union sort base on a set of underlying sorts
5431 >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
5434 for i
in range(len(sorts)):
5435 sum.declare(
"inject%d" % i, (
"project%d" % i, sorts[i]))
5437 return sum, [(sum.constructor(i), sum.accessor(i, 0))
for i
in range(len(sorts))]
5441 """Return a new enumeration sort named `name` containing the given values.
5443 The result is a pair (sort, list of constants).
5445 >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5448 _z3_assert(isinstance(name, str),
"Name must be a string")
5449 _z3_assert(all([isinstance(v, str)
for v
in values]),
"Enumeration sort values must be strings")
5450 _z3_assert(len(values) > 0,
"At least one value expected")
5453 _val_names = (Symbol * num)()
5454 for i
in range(num):
5455 _val_names[i] =
to_symbol(values[i], ctx)
5456 _values = (FuncDecl * num)()
5457 _testers = (FuncDecl * num)()
5461 for i
in range(num):
5463 V = [a()
for a
in V]
5474 """Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3.
5476 Consider using the function `args2params` to create instances of this object.
5491 if self.
ctx.ref()
is not None and Z3_params_dec_ref
is not None:
5495 """Set parameter name with value val."""
5497 _z3_assert(isinstance(name, str),
"parameter name must be a string")
5499 if isinstance(val, bool):
5503 elif isinstance(val, float):
5505 elif isinstance(val, str):
5515 _z3_assert(isinstance(ds, ParamDescrsRef),
"parameter description set expected")
5520 """Convert python arguments into a Z3_params object.
5521 A ':' is added to the keywords, and '_' is replaced with '-'
5523 >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5524 (params model true relevancy 2 elim_and true)
5527 _z3_assert(len(arguments) % 2 == 0,
"Argument list must have an even number of elements.")
5543 """Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3.
5547 _z3_assert(isinstance(descr, ParamDescrs),
"parameter description object expected")
5553 return ParamsDescrsRef(self.
descr, self.
ctx)
5556 if self.
ctx.ref()
is not None and Z3_param_descrs_dec_ref
is not None:
5560 """Return the size of in the parameter description `self`.
5565 """Return the size of in the parameter description `self`.
5570 """Return the i-th parameter name in the parameter description `self`.
5575 """Return the kind of the parameter named `n`.
5580 """Return the documentation string of the parameter named `n`.
5601 """Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible).
5603 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
5604 A goal has a solution if one of its subgoals has a solution.
5605 A goal is unsatisfiable if all subgoals are unsatisfiable.
5608 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
5611 "If goal is different from None, then ctx must be also different from None")
5614 if self.
goal is None:
5619 if self.
goal is not None and self.
ctx.ref()
is not None and Z3_goal_dec_ref
is not None:
5623 """Return the depth of the goal `self`.
5624 The depth corresponds to the number of tactics applied to `self`.
5626 >>> x, y = Ints('x y')
5628 >>> g.add(x == 0, y >= x + 1)
5631 >>> r = Then('simplify', 'solve-eqs')(g)
5632 >>> # r has 1 subgoal
5641 """Return `True` if `self` contains the `False` constraints.
5643 >>> x, y = Ints('x y')
5645 >>> g.inconsistent()
5647 >>> g.add(x == 0, x == 1)
5650 >>> g.inconsistent()
5652 >>> g2 = Tactic('propagate-values')(g)[0]
5653 >>> g2.inconsistent()
5659 """Return the precision (under-approximation, over-approximation, or precise) of the goal `self`.
5662 >>> g.prec() == Z3_GOAL_PRECISE
5664 >>> x, y = Ints('x y')
5665 >>> g.add(x == y + 1)
5666 >>> g.prec() == Z3_GOAL_PRECISE
5668 >>> t = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10)
5671 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
5672 >>> g2.prec() == Z3_GOAL_PRECISE
5674 >>> g2.prec() == Z3_GOAL_UNDER
5680 """Alias for `prec()`.
5683 >>> g.precision() == Z3_GOAL_PRECISE
5689 """Return the number of constraints in the goal `self`.
5694 >>> x, y = Ints('x y')
5695 >>> g.add(x == 0, y > x)
5702 """Return the number of constraints in the goal `self`.
5707 >>> x, y = Ints('x y')
5708 >>> g.add(x == 0, y > x)
5715 """Return a constraint in the goal `self`.
5718 >>> x, y = Ints('x y')
5719 >>> g.add(x == 0, y > x)
5728 """Return a constraint in the goal `self`.
5731 >>> x, y = Ints('x y')
5732 >>> g.add(x == 0, y > x)
5738 if arg >= len(self):
5740 return self.
get(arg)
5743 """Assert constraints into the goal.
5747 >>> g.assert_exprs(x > 0, x < 2)
5762 >>> g.append(x > 0, x < 2)
5773 >>> g.insert(x > 0, x < 2)
5784 >>> g.add(x > 0, x < 2)
5791 """Retrieve model from a satisfiable goal
5792 >>> a, b = Ints('a b')
5794 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
5795 >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs'))
5798 [Or(b == 0, b == 1), Not(0 <= b)]
5800 [Or(b == 0, b == 1), Not(1 <= b)]
5801 >>> # Remark: the subgoal r[0] is unsatisfiable
5802 >>> # Creating a solver for solving the second subgoal
5809 >>> # Model s.model() does not assign a value to `a`
5810 >>> # It is a model for subgoal `r[1]`, but not for goal `g`
5811 >>> # The method convert_model creates a model for `g` from a model for `r[1]`.
5812 >>> r[1].convert_model(s.model())
5816 _z3_assert(isinstance(model, ModelRef),
"Z3 Model expected")
5820 return obj_to_string(self)
5823 """Return a textual representation of the s-expression representing the goal."""
5827 """Return a textual representation of the goal in DIMACS format."""
5831 """Copy goal `self` to context `target`.
5839 >>> g2 = g.translate(c2)
5842 >>> g.ctx == main_ctx()
5846 >>> g2.ctx == main_ctx()
5850 _z3_assert(isinstance(target, Context),
"target must be a context")
5860 """Return a new simplified goal.
5862 This method is essentially invoking the simplify tactic.
5866 >>> g.add(x + 1 >= 2)
5869 >>> g2 = g.simplify()
5872 >>> # g was not modified
5877 return t.apply(self, *arguments, **keywords)[0]
5880 """Return goal `self` as a single Z3 expression.
5899 return And([self.
get(i)
for i
in range(len(self))], self.
ctx)
5909 """A collection (vector) of ASTs."""
5918 assert ctx
is not None
5923 if self.
vector is not None and self.
ctx.ref()
is not None and Z3_ast_vector_dec_ref
is not None:
5927 """Return the size of the vector `self`.
5932 >>> A.push(Int('x'))
5933 >>> A.push(Int('x'))
5940 """Return the AST at position `i`.
5943 >>> A.push(Int('x') + 1)
5944 >>> A.push(Int('y'))
5951 if isinstance(i, int):
5959 elif isinstance(i, slice):
5961 for ii
in range(*i.indices(self.
__len__())):
5969 """Update AST at position `i`.
5972 >>> A.push(Int('x') + 1)
5973 >>> A.push(Int('y'))
5985 """Add `v` in the end of the vector.
5990 >>> A.push(Int('x'))
5997 """Resize the vector to `sz` elements.
6003 >>> for i in range(10): A[i] = Int('x')
6010 """Return `True` if the vector contains `item`.
6033 """Copy vector `self` to context `other_ctx`.
6039 >>> B = A.translate(c2)
6055 return obj_to_string(self)
6058 """Return a textual representation of the s-expression representing the vector."""
6069 """A mapping from ASTs to ASTs."""
6078 assert ctx
is not None
6086 if self.
map is not None and self.
ctx.ref()
is not None and Z3_ast_map_dec_ref
is not None:
6090 """Return the size of the map.
6096 >>> M[x] = IntVal(1)
6103 """Return `True` if the map contains key `key`.
6116 """Retrieve the value associated with key `key`.
6127 """Add/Update key `k` with value `v`.
6136 >>> M[x] = IntVal(1)
6146 """Remove the entry associated with key `k`.
6160 """Remove all entries from the map.
6165 >>> M[x+x] = IntVal(1)
6175 """Return an AstVector containing all keys in the map.
6180 >>> M[x+x] = IntVal(1)
6194 """Store the value of the interpretation of a function in a particular point."""
6205 if self.
ctx.ref()
is not None and Z3_func_entry_dec_ref
is not None:
6209 """Return the number of arguments in the given entry.
6211 >>> f = Function('f', IntSort(), IntSort(), IntSort())
6213 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6218 >>> f_i.num_entries()
6220 >>> e = f_i.entry(0)
6227 """Return the value of argument `idx`.
6229 >>> f = Function('f', IntSort(), IntSort(), IntSort())
6231 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6236 >>> f_i.num_entries()
6238 >>> e = f_i.entry(0)
6249 ... except IndexError:
6250 ... print("index error")
6258 """Return the value of the function at point `self`.
6260 >>> f = Function('f', IntSort(), IntSort(), IntSort())
6262 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6267 >>> f_i.num_entries()
6269 >>> e = f_i.entry(0)
6280 """Return entry `self` as a Python list.
6281 >>> f = Function('f', IntSort(), IntSort(), IntSort())
6283 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
6288 >>> f_i.num_entries()
6290 >>> e = f_i.entry(0)
6295 args.append(self.
value())
6303 """Stores the interpretation of a function in a Z3 model."""
6308 if self.
f is not None:
6312 if self.
f is not None and self.
ctx.ref()
is not None and Z3_func_interp_dec_ref
is not None:
6317 Return the `else` value for a function interpretation.
6318 Return None if Z3 did not specify the `else` value for
6321 >>> f = Function('f', IntSort(), IntSort())
6323 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
6329 >>> m[f].else_value()
6339 """Return the number of entries/points in the function interpretation `self`.
6341 >>> f = Function('f', IntSort(), IntSort())
6343 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
6349 >>> m[f].num_entries()
6355 """Return the number of arguments for each entry in the function interpretation `self`.
6357 >>> f = Function('f', IntSort(), IntSort())
6359 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
6369 """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
6371 >>> f = Function('f', IntSort(), IntSort())
6373 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
6379 >>> m[f].num_entries()
6389 """Copy model 'self' to context 'other_ctx'.
6400 """Return the function interpretation as a Python list.
6401 >>> f = Function('f', IntSort(), IntSort())
6403 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
6417 return obj_to_string(self)
6421 """Model/Solution of a satisfiability problem (aka system of constraints)."""
6424 assert ctx
is not None
6430 if self.
ctx.ref()
is not None and Z3_model_dec_ref
is not None:
6434 return obj_to_string(self)
6437 """Return a textual representation of the s-expression representing the model."""
6440 def eval(self, t, model_completion=False):
6441 """Evaluate the expression `t` in the model `self`.
6442 If `model_completion` is enabled, then a default interpretation is automatically added
6443 for symbols that do not have an interpretation in the model `self`.
6447 >>> s.add(x > 0, x < 2)
6460 >>> m.eval(y, model_completion=True)
6462 >>> # Now, m contains an interpretation for y
6469 raise Z3Exception(
"failed to evaluate expression in the model")
6472 """Alias for `eval`.
6476 >>> s.add(x > 0, x < 2)
6480 >>> m.evaluate(x + 1)
6482 >>> m.evaluate(x == 1)
6485 >>> m.evaluate(y + x)
6489 >>> m.evaluate(y, model_completion=True)
6491 >>> # Now, m contains an interpretation for y
6492 >>> m.evaluate(y + x)
6495 return self.
eval(t, model_completion)
6498 """Return the number of constant and function declarations in the model `self`.
6500 >>> f = Function('f', IntSort(), IntSort())
6503 >>> s.add(x > 0, f(x) != x)
6512 return num_consts + num_funcs
6515 """Return the interpretation for a given declaration or constant.
6517 >>> f = Function('f', IntSort(), IntSort())
6520 >>> s.add(x > 0, x < 2, f(x) == 0)
6530 _z3_assert(isinstance(decl, FuncDeclRef)
or is_const(decl),
"Z3 declaration expected")
6534 if decl.arity() == 0:
6536 if _r.value
is None:
6552 sz = fi.num_entries()
6556 e =
Store(e, fe.arg_value(0), fe.value())
6567 """Return the number of uninterpreted sorts that contain an interpretation in the model `self`.
6569 >>> A = DeclareSort('A')
6570 >>> a, b = Consts('a b', A)
6582 """Return the uninterpreted sort at position `idx` < self.num_sorts().
6584 >>> A = DeclareSort('A')
6585 >>> B = DeclareSort('B')
6586 >>> a1, a2 = Consts('a1 a2', A)
6587 >>> b1, b2 = Consts('b1 b2', B)
6589 >>> s.add(a1 != a2, b1 != b2)
6605 """Return all uninterpreted sorts that have an interpretation in the model `self`.
6607 >>> A = DeclareSort('A')
6608 >>> B = DeclareSort('B')
6609 >>> a1, a2 = Consts('a1 a2', A)
6610 >>> b1, b2 = Consts('b1 b2', B)
6612 >>> s.add(a1 != a2, b1 != b2)
6622 """Return the interpretation for the uninterpreted sort `s` in the model `self`.
6624 >>> A = DeclareSort('A')
6625 >>> a, b = Consts('a b', A)
6631 >>> m.get_universe(A)
6635 _z3_assert(isinstance(s, SortRef),
"Z3 sort expected")
6642 """If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned.
6643 If `idx` is a declaration, then the actual interpretation is returned.
6645 The elements can be retrieved using position or the actual declaration.
6647 >>> f = Function('f', IntSort(), IntSort())
6650 >>> s.add(x > 0, x < 2, f(x) == 0)
6664 >>> for d in m: print("%s -> %s" % (d, m[d]))
6669 if idx >= len(self):
6672 if (idx < num_consts):
6676 if isinstance(idx, FuncDeclRef):
6680 if isinstance(idx, SortRef):
6683 _z3_assert(
False,
"Integer, Z3 declaration, or Z3 constant expected")
6687 """Return a list with all symbols that have an interpretation in the model `self`.
6688 >>> f = Function('f', IntSort(), IntSort())
6691 >>> s.add(x > 0, x < 2, f(x) == 0)
6706 """Update the interpretation of a constant"""
6709 if is_func_decl(x)
and x.arity() != 0
and isinstance(value, FuncInterp):
6713 for i
in range(value.num_entries()):
6718 v.push(e.arg_value(j))
6723 raise Z3Exception(
"Expecting 0-ary function or constant expression")
6728 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6731 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
6736 """Perform model-based projection on fml with respect to vars.
6737 Assume that the model satisfies fml. Then compute a projection fml_p, such
6738 that vars do not occur free in fml_p, fml_p is true in the model and
6739 fml_p => exists vars . fml
6741 ctx = self.
ctx.ref()
6742 _vars = (Ast * len(vars))()
6743 for i
in range(len(vars)):
6744 _vars[i] = vars[i].as_ast()
6748 """Perform model-based projection, but also include realizer terms for the projected variables"""
6749 ctx = self.
ctx.ref()
6750 _vars = (Ast * len(vars))()
6751 for i
in range(len(vars)):
6752 _vars[i] = vars[i].as_ast()
6754 result = Z3_qe_model_project_with_witness(ctx, self.
model, len(vars), _vars, fml.ast, defs.map)
6769 for k, v
in eval.items():
6770 mdl.update_value(k, v)
6775 """Return true if n is a Z3 expression of the form (_ as-array f)."""
6776 return isinstance(n, ExprRef)
and Z3_is_as_array(n.ctx.ref(), n.as_ast())
6780 """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6793 """Statistics for `Solver.check()`."""
6804 if self.
ctx.ref()
is not None and Z3_stats_dec_ref
is not None:
6811 out.write(u(
'<table border="1" cellpadding="2" cellspacing="0">'))
6814 out.write(u(
'<tr style="background-color:#CFCFCF">'))
6817 out.write(u(
"<tr>"))
6819 out.write(u(
"<td>%s</td><td>%s</td></tr>" % (k, v)))
6820 out.write(u(
"</table>"))
6821 return out.getvalue()
6826 """Return the number of statistical counters.
6829 >>> s = Then('simplify', 'nlsat').solver()
6833 >>> st = s.statistics()
6840 """Return the value of statistical counter at position `idx`. The result is a pair (key, value).
6843 >>> s = Then('simplify', 'nlsat').solver()
6847 >>> st = s.statistics()
6851 ('nlsat propagations', 2)
6853 ('nlsat restarts', 1)
6855 if idx >= len(self):
6864 """Return the list of statistical counters.
6867 >>> s = Then('simplify', 'nlsat').solver()
6871 >>> st = s.statistics()
6876 """Return the value of a particular statistical counter.
6879 >>> s = Then('simplify', 'nlsat').solver()
6883 >>> st = s.statistics()
6884 >>> st.get_key_value('nlsat propagations')
6887 for idx
in range(len(self)):
6893 raise Z3Exception(
"unknown key")
6896 """Access the value of statistical using attributes.
6898 Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
6899 we should use '_' (e.g., 'nlsat_propagations').
6902 >>> s = Then('simplify', 'nlsat').solver()
6906 >>> st = s.statistics()
6907 >>> st.nlsat_propagations
6912 key = name.replace(
"_",
" ")
6916 raise AttributeError
6926 """Represents the result of a satisfiability check: sat, unsat, unknown.
6932 >>> isinstance(r, CheckSatResult)
6943 return isinstance(other, CheckSatResult)
and self.
r == other.r
6946 return not self.
__eq__(other)
6950 if self.
r == Z3_L_TRUE:
6952 elif self.
r == Z3_L_FALSE:
6953 return "<b>unsat</b>"
6955 return "<b>unknown</b>"
6957 if self.
r == Z3_L_TRUE:
6959 elif self.
r == Z3_L_FALSE:
6965 in_html = in_html_mode()
6968 set_html_mode(in_html)
6979 Solver API provides methods for implementing the main SMT 2.0 commands:
6980 push, pop, check, get-model, etc.
6983 def __init__(self, solver=None, ctx=None, logFile=None):
6984 assert solver
is None or ctx
is not None
6993 if logFile
is not None:
6994 self.
set(
"smtlib2_log", logFile)
6997 if self.
solver is not None and self.
ctx.ref()
is not None and Z3_solver_dec_ref
is not None:
7008 """Set a configuration option.
7009 The method `help()` return a string containing all available options.
7012 >>> # The option MBQI can be set using three different approaches.
7013 >>> s.set(mbqi=True)
7014 >>> s.set('MBQI', True)
7015 >>> s.set(':mbqi', True)
7021 """Create a backtracking point.
7043 """Backtrack \\c num backtracking points.
7065 """Return the current number of backtracking points.
7083 """Remove all asserted constraints and backtracking points created using `push()`.
7097 """Assert constraints into the solver.
7101 >>> s.assert_exprs(x > 0, x < 2)
7108 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
7116 """Assert constraints into the solver.
7120 >>> s.add(x > 0, x < 2)
7131 """Assert constraints into the solver.
7135 >>> s.append(x > 0, x < 2)
7142 """Assert constraints into the solver.
7146 >>> s.insert(x > 0, x < 2)
7153 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7155 If `p` is a string, it will be automatically converted into a Boolean constant.
7160 >>> s.set(unsat_core=True)
7161 >>> s.assert_and_track(x > 0, 'p1')
7162 >>> s.assert_and_track(x != 1, 'p2')
7163 >>> s.assert_and_track(x < 0, p3)
7164 >>> print(s.check())
7166 >>> c = s.unsat_core()
7176 if isinstance(p, str):
7178 _z3_assert(isinstance(a, BoolRef),
"Boolean expression expected")
7183 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
7189 >>> s.add(x > 0, x < 2)
7192 >>> s.model().eval(x)
7198 >>> s.add(2**x == 4)
7204 num = len(assumptions)
7205 _assumptions = (Ast * num)()
7206 for i
in range(num):
7207 _assumptions[i] = s.cast(assumptions[i]).as_ast()
7212 """Return a model for the last `check()`.
7214 This function raises an exception if
7215 a model is not available (e.g., last `check()` returned unsat).
7219 >>> s.add(a + 2 == 0)
7228 raise Z3Exception(
"model is not available")
7231 """Import model converter from other into the current solver"""
7232 Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7234 def interrupt(self):
7235 """Interrupt the execution of the solver object.
7236 Remarks: This ensures that the interrupt applies only
7237 to the given solver object and it applies only if it is running.
7239 Z3_solver_interrupt(self.ctx.ref(), self.solver)
7241 def unsat_core(self):
7242 """Return a subset (as an AST vector) of the assumptions provided to the last check().
7244 These are the assumptions Z3 used in the unsatisfiability proof.
7245 Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7246 They may be also used to "retract" assumptions. Note that, assumptions are not really
7247 "soft constraints", but they can be used to implement them.
7249 >>> p1, p2, p3 = Bools('p1 p2 p3')
7250 >>> x, y = Ints('x y')
7252 >>> s.add(Implies(p1, x > 0))
7253 >>> s.add(Implies(p2, y > x))
7254 >>> s.add(Implies(p2, y < 1))
7255 >>> s.add(Implies(p3, y > -3))
7256 >>> s.check(p1, p2, p3)
7258 >>> core = s.unsat_core()
7267 >>> # "Retracting" p2
7271 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7273 def consequences(self, assumptions, variables):
7274 """Determine fixed values for the variables based on the solver state and assumptions.
7276 >>> a, b, c, d = Bools('a b c d')
7277 >>> s.add(Implies(a,b), Implies(b, c))
7278 >>> s.consequences([a],[b,c,d])
7279 (sat, [Implies(a, b), Implies(a, c)])
7280 >>> s.consequences([Not(c),d],[a,b,c,d])
7281 (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7283 if isinstance(assumptions, list):
7284 _asms = AstVector(None, self.ctx)
7285 for a in assumptions:
7288 if isinstance(variables, list):
7289 _vars = AstVector(None, self.ctx)
7293 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7294 _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7295 consequences = AstVector(None, self.ctx)
7296 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7297 variables.vector, consequences.vector)
7298 sz = len(consequences)
7299 consequences = [consequences[i] for i in range(sz)]
7300 return CheckSatResult(r), consequences
7302 def from_file(self, filename):
7303 """Parse assertions from a file"""
7304 Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7306 def from_string(self, s):
7307 """Parse assertions from a string"""
7308 Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7310 def cube(self, vars=None):
7312 The method takes an optional set of variables that restrict which
7313 variables may be used as a starting point for cubing.
7314 If vars is not None, then the first case split is based on a variable in
7317 self.cube_vs = AstVector(None, self.ctx)
7318 if vars is not None:
7320 self.cube_vs.push(v)
7322 lvl = self.backtrack_level
7323 self.backtrack_level = 4000000000
7324 r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7325 if (len(r) == 1 and is_false(r[0])):
7331 def cube_vars(self):
7332 """Access the set of variables that were touched by the most recently generated cube.
7333 This set of variables can be used as a starting point for additional cubes.
7334 The idea is that variables that appear in clauses that are reduced by the most recent
7335 cube are likely more useful to cube on."""
7339 t = _py2expr(t, self.ctx)
7340 """Retrieve congruence closure root of the term t relative to the current search state
7341 The function primarily works for SimpleSolver. Terms and variables that are
7342 eliminated during pre-processing are not visible to the congruence closure.
7344 return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
7347 t = _py2expr(t, self.ctx)
7348 """Retrieve congruence closure sibling of the term t relative to the current search state
7349 The function primarily works for SimpleSolver. Terms and variables that are
7350 eliminated during pre-processing are not visible to the congruence closure.
7352 return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
7354 def solve_for(self, t):
7355 t = _py2expr(t, self.ctx)
7356 """Retrieve a solution for t relative to linear equations maintained in the current state.
7357 The function primarily works for SimpleSolver and when there is a solution using linear arithmetic."""
7358 return _to_expr_ref(Z3_solver_solve_for(self.ctx.ref(), self.solver, t.ast), self.ctx)
7361 """Return a proof for the last `check()`. Proof construction must be enabled."""
7362 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7364 def assertions(self):
7365 """Return an AST vector containing all added constraints.
7376 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7379 """Return an AST vector containing all currently inferred units.
7381 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7383 def non_units(self):
7384 """Return an AST vector containing all atomic formulas in solver state that are not units.
7386 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7388 def trail_levels(self):
7389 """Return trail and decision levels of the solver state after a check() call.
7391 trail = self.trail()
7392 levels = (ctypes.c_uint * len(trail))()
7393 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7394 return trail, levels
7396 def set_initial_value(self, var, value):
7397 """initialize the solver's state by setting the initial value of var to value
7400 value = s.cast(value)
7401 Z3_solver_set_initial_value(self.ctx.ref(), self.solver, var.ast, value.ast)
7404 """Return trail of the solver state after a check() call.
7406 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7408 def statistics(self):
7409 """Return statistics for the last `check()`.
7411 >>> s = SimpleSolver()
7416 >>> st = s.statistics()
7417 >>> st.get_key_value('final checks')
7424 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7426 def reason_unknown(self):
7427 """Return a string describing why the last `check()` returned `unknown`.
7430 >>> s = SimpleSolver()
7431 >>> s.add(2**x == 4)
7434 >>> s.reason_unknown()
7435 '(incomplete (theory arithmetic))'
7437 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7440 """Display a string describing all available options."""
7441 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7443 def param_descrs(self):
7444 """Return the parameter description set."""
7445 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7448 """Return a formatted string with all added constraints."""
7449 return obj_to_string(self)
7451 def translate(self, target):
7452 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7456 >>> s1 = Solver(ctx=c1)
7457 >>> s2 = s1.translate(c2)
7460 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7461 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7462 return Solver(solver, target)
7465 return self.translate(self.ctx)
7467 def __deepcopy__(self, memo={}):
7468 return self.translate(self.ctx)
7471 """Return a formatted string (in Lisp-like format) with all added constraints.
7472 We say the string is in s-expression format.
7480 return Z3_solver_to_string(self.ctx.ref(), self.solver)
7482 def dimacs(self, include_names=True):
7483 """Return a textual representation of the solver in DIMACS format."""
7484 return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7487 """return SMTLIB2 formatted benchmark for solver's assertions"""
7488 es = self.assertions()
7494 for i in range(sz1):
7495 v[i] = es[i].as_ast()
7497 e = es[sz1].as_ast()
7499 e = BoolVal(True, self.ctx).as_ast()
7500 return Z3_benchmark_to_smtlib_string(
7501 self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7505def SolverFor(logic, ctx=None, logFile=None):
7506 """Create a solver customized for the given logic.
7508 The parameter `logic` is a string. It should be contains
7509 the name of a SMT-LIB logic.
7510 See http://www.smtlib.org/ for the name of all available logics.
7512 >>> s = SolverFor("QF_LIA")
7522 logic = to_symbol(logic)
7523 return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx, logFile)
7526def SimpleSolver(ctx=None, logFile=None):
7527 """Return a simple general purpose solver with limited amount of preprocessing.
7529 >>> s = SimpleSolver()
7536 return Solver(Z3_mk_simple_solver(ctx.ref()), ctx, logFile)
7538#########################################
7542#########################################
7545class Fixedpoint(Z3PPObject):
7546 """Fixedpoint API provides methods for solving with recursive predicates"""
7548 def __init__(self, fixedpoint=None, ctx=None):
7549 assert fixedpoint is None or ctx is not None
7550 self.ctx = _get_ctx(ctx)
7551 self.fixedpoint = None
7552 if fixedpoint is None:
7553 self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
7555 self.fixedpoint = fixedpoint
7556 Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
7559 def __deepcopy__(self, memo={}):
7560 return FixedPoint(self.fixedpoint, self.ctx)
7563 if self.fixedpoint is not None and self.ctx.ref() is not None and Z3_fixedpoint_dec_ref is not None:
7564 Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
7566 def set(self, *args, **keys):
7567 """Set a configuration option. The method `help()` return a string containing all available options.
7569 p = args2params(args, keys, self.ctx)
7570 Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
7573 """Display a string describing all available options."""
7574 print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
7576 def param_descrs(self):
7577 """Return the parameter description set."""
7578 return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
7580 def assert_exprs(self, *args):
7581 """Assert constraints as background axioms for the fixedpoint solver."""
7582 args = _get_args(args)
7583 s = BoolSort(self.ctx)
7585 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7587 f = self.abstract(f)
7588 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
7591 arg = self.abstract(arg)
7592 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
7594 def add(self, *args):
7595 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7596 self.assert_exprs(*args)
7598 def __iadd__(self, fml):
7602 def append(self, *args):
7603 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7604 self.assert_exprs(*args)
7606 def insert(self, *args):
7607 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7608 self.assert_exprs(*args)
7610 def add_rule(self, head, body=None, name=None):
7611 """Assert rules defining recursive predicates to the fixedpoint solver.
7614 >>> s = Fixedpoint()
7615 >>> s.register_relation(a.decl())
7616 >>> s.register_relation(b.decl())
7624 name = to_symbol(name, self.ctx)
7626 head = self.abstract(head)
7627 Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
7629 body = _get_args(body)
7630 f = self.abstract(Implies(And(body, self.ctx), head))
7631 Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
7633 def rule(self, head, body=None, name=None):
7634 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7635 self.add_rule(head, body, name)
7637 def fact(self, head, name=None):
7638 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7639 self.add_rule(head, None, name)
7641 def query(self, *query):
7642 """Query the fixedpoint engine whether formula is derivable.
7643 You can also pass an tuple or list of recursive predicates.
7645 query = _get_args(query)
7647 if sz >= 1 and isinstance(query[0], FuncDeclRef):
7648 _decls = (FuncDecl * sz)()
7653 r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
7658 query = And(query, self.ctx)
7659 query = self.abstract(query, False)
7660 r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
7661 return CheckSatResult(r)
7663 def query_from_lvl(self, lvl, *query):
7664 """Query the fixedpoint engine whether formula is derivable starting at the given query level.
7666 query = _get_args(query)
7668 if sz >= 1 and isinstance(query[0], FuncDecl):
7669 _z3_assert(False, "unsupported")
7675 query = self.abstract(query, False)
7676 r = Z3_fixedpoint_query_from_lvl(self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
7677 return CheckSatResult(r)
7679 def update_rule(self, head, body, name):
7683 name = to_symbol(name, self.ctx)
7684 body = _get_args(body)
7685 f = self.abstract(Implies(And(body, self.ctx), head))
7686 Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
7688 def get_answer(self):
7689 """Retrieve answer from last query call."""
7690 r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
7691 return _to_expr_ref(r, self.ctx)
7693 def get_ground_sat_answer(self):
7694 """Retrieve a ground cex from last query call."""
7695 r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)
7696 return _to_expr_ref(r, self.ctx)
7698 def get_rules_along_trace(self):
7699 """retrieve rules along the counterexample trace"""
7700 return AstVector(Z3_fixedpoint_get_rules_along_trace(self.ctx.ref(), self.fixedpoint), self.ctx)
7702 def get_rule_names_along_trace(self):
7703 """retrieve rule names along the counterexample trace"""
7704 # this is a hack as I don't know how to return a list of symbols from C++;
7705 # obtain names as a single string separated by semicolons
7706 names = _symbol2py(self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
7707 # split into individual names
7708 return names.split(";")
7710 def get_num_levels(self, predicate):
7711 """Retrieve number of levels used for predicate in PDR engine"""
7712 return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
7714 def get_cover_delta(self, level, predicate):
7715 """Retrieve properties known about predicate for the level'th unfolding.
7716 -1 is treated as the limit (infinity)
7718 r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
7719 return _to_expr_ref(r, self.ctx)
7721 def add_cover(self, level, predicate, property):
7722 """Add property to predicate for the level'th unfolding.
7723 -1 is treated as infinity (infinity)
7725 Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
7727 def register_relation(self, *relations):
7728 """Register relation as recursive"""
7729 relations = _get_args(relations)
7731 Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
7733 def set_predicate_representation(self, f, *representations):
7734 """Control how relation is represented"""
7735 representations = _get_args(representations)
7736 representations = [to_symbol(s) for s in representations]
7737 sz = len(representations)
7738 args = (Symbol * sz)()
7740 args[i] = representations[i]
7741 Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
7743 def parse_string(self, s):
7744 """Parse rules and queries from a string"""
7745 return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
7747 def parse_file(self, f):
7748 """Parse rules and queries from a file"""
7749 return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
7751 def get_rules(self):
7752 """retrieve rules that have been added to fixedpoint context"""
7753 return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
7755 def get_assertions(self):
7756 """retrieve assertions that have been added to fixedpoint context"""
7757 return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
7760 """Return a formatted string with all added rules and constraints."""
7764 """Return a formatted string (in Lisp-like format) with all added constraints.
7765 We say the string is in s-expression format.
7767 return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
7769 def to_string(self, queries):
7770 """Return a formatted string (in Lisp-like format) with all added constraints.
7771 We say the string is in s-expression format.
7772 Include also queries.
7774 args, len = _to_ast_array(queries)
7775 return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
7777 def statistics(self):
7778 """Return statistics for the last `query()`.
7780 return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
7782 def reason_unknown(self):
7783 """Return a string describing why the last `query()` returned `unknown`.
7785 return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
7787 def declare_var(self, *vars):
7788 """Add variable or several variables.
7789 The added variable or variables will be bound in the rules
7792 vars = _get_args(vars)
7796 def abstract(self, fml, is_forall=True):
7800 return ForAll(self.vars, fml)
7802 return Exists(self.vars, fml)
7805#########################################
7809#########################################
7811class FiniteDomainSortRef(SortRef):
7812 """Finite domain sort."""
7815 """Return the size of the finite domain sort"""
7816 r = (ctypes.c_ulonglong * 1)()
7817 if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast, r):
7820 raise Z3Exception("Failed to retrieve finite domain sort size")
7823def FiniteDomainSort(name, sz, ctx=None):
7824 """Create a named finite domain sort of a given size sz"""
7825 if not isinstance(name, Symbol):
7826 name = to_symbol(name)
7828 return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
7831def is_finite_domain_sort(s):
7832 """Return True if `s` is a Z3 finite-domain sort.
7834 >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7836 >>> is_finite_domain_sort(IntSort())
7839 return isinstance(s, FiniteDomainSortRef)
7842class FiniteDomainRef(ExprRef):
7843 """Finite-domain expressions."""
7846 """Return the sort of the finite-domain expression `self`."""
7847 return FiniteDomainSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
7849 def as_string(self):
7850 """Return a Z3 floating point expression as a Python string."""
7851 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
7854def is_finite_domain(a):
7855 """Return `True` if `a` is a Z3 finite-domain expression.
7857 >>> s = FiniteDomainSort('S', 100)
7858 >>> b = Const('b', s)
7859 >>> is_finite_domain(b)
7861 >>> is_finite_domain(Int('x'))
7864 return isinstance(a, FiniteDomainRef)
7867class FiniteDomainNumRef(FiniteDomainRef):
7868 """Integer values."""
7871 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral.
7873 >>> s = FiniteDomainSort('S', 100)
7874 >>> v = FiniteDomainVal(3, s)
7880 return int(self.as_string())
7882 def as_string(self):
7883 """Return a Z3 finite-domain numeral as a Python string.
7885 >>> s = FiniteDomainSort('S', 100)
7886 >>> v = FiniteDomainVal(42, s)
7890 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
7893def FiniteDomainVal(val, sort, ctx=None):
7894 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7896 >>> s = FiniteDomainSort('S', 256)
7897 >>> FiniteDomainVal(255, s)
7899 >>> FiniteDomainVal('100', s)
7903 _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort")
7905 return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
7908def is_finite_domain_value(a):
7909 """Return `True` if `a` is a Z3 finite-domain value.
7911 >>> s = FiniteDomainSort('S', 100)
7912 >>> b = Const('b', s)
7913 >>> is_finite_domain_value(b)
7915 >>> b = FiniteDomainVal(10, s)
7918 >>> is_finite_domain_value(b)
7921 return is_finite_domain(a) and _is_numeral(a.ctx, a.as_ast())
7924#########################################
7928#########################################
7930class OptimizeObjective:
7931 def __init__(self, opt, value, is_max):
7934 self._is_max = is_max
7938 return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7942 return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7944 def lower_values(self):
7946 return AstVector(Z3_optimize_get_lower_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7948 def upper_values(self):
7950 return AstVector(Z3_optimize_get_upper_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7959 return "%s:%s" % (self._value, self._is_max)
7965def _global_on_model(ctx):
7966 (fn, mdl) = _on_models[ctx]
7970_on_model_eh = on_model_eh_type(_global_on_model)
7973class Optimize(Z3PPObject):
7974 """Optimize API provides methods for solving using objective functions and weighted soft constraints"""
7976 def __init__(self, optimize=None, ctx=None):
7977 self.ctx = _get_ctx(ctx)
7978 if optimize is None:
7979 self.optimize = Z3_mk_optimize(self.ctx.ref())
7981 self.optimize = optimize
7982 self._on_models_id = None
7983 Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7985 def __deepcopy__(self, memo={}):
7986 return Optimize(self.optimize, self.ctx)
7989 if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
7990 Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7991 if self._on_models_id is not None:
7992 del _on_models[self._on_models_id]
7994 def __enter__(self):
7998 def __exit__(self, *exc_info):
8001 def set(self, *args, **keys):
8002 """Set a configuration option.
8003 The method `help()` return a string containing all available options.
8005 p = args2params(args, keys, self.ctx)
8006 Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
8009 """Display a string describing all available options."""
8010 print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
8012 def param_descrs(self):
8013 """Return the parameter description set."""
8014 return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
8016 def assert_exprs(self, *args):
8017 """Assert constraints as background axioms for the optimize solver."""
8018 args = _get_args(args)
8019 s = BoolSort(self.ctx)
8021 if isinstance(arg, Goal) or isinstance(arg, AstVector):
8023 Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
8026 Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
8028 def add(self, *args):
8029 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
8030 self.assert_exprs(*args)
8032 def __iadd__(self, fml):
8036 def assert_and_track(self, a, p):
8037 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
8039 If `p` is a string, it will be automatically converted into a Boolean constant.
8044 >>> s.assert_and_track(x > 0, 'p1')
8045 >>> s.assert_and_track(x != 1, 'p2')
8046 >>> s.assert_and_track(x < 0, p3)
8047 >>> print(s.check())
8049 >>> c = s.unsat_core()
8059 if isinstance(p, str):
8060 p = Bool(p, self.ctx)
8061 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
8062 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
8063 Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
8065 def add_soft(self, arg, weight="1", id=None):
8066 """Add soft constraint with optional weight and optional identifier.
8067 If no weight is supplied, then the penalty for violating the soft constraint
8069 Soft constraints are grouped by identifiers. Soft constraints that are
8070 added without identifiers are grouped by default.
8073 weight = "%d" % weight
8074 elif isinstance(weight, float):
8075 weight = "%f" % weight
8076 if not isinstance(weight, str):
8077 raise Z3Exception("weight should be a string or an integer")
8080 id = to_symbol(id, self.ctx)
8083 v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
8084 return OptimizeObjective(self, v, False)
8085 if sys.version_info.major >= 3 and isinstance(arg, Iterable):
8086 return [asoft(a) for a in arg]
8089 def set_initial_value(self, var, value):
8090 """initialize the solver's state by setting the initial value of var to value
8093 value = s.cast(value)
8094 Z3_optimize_set_initial_value(self.ctx.ref(), self.optimize, var.ast, value.ast)
8096 def maximize(self, arg):
8097 """Add objective function to maximize."""
8098 return OptimizeObjective(
8100 Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
8104 def minimize(self, arg):
8105 """Add objective function to minimize."""
8106 return OptimizeObjective(
8108 Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
8113 """create a backtracking point for added rules, facts and assertions"""
8114 Z3_optimize_push(self.ctx.ref(), self.optimize)
8117 """restore to previously created backtracking point"""
8118 Z3_optimize_pop(self.ctx.ref(), self.optimize)
8120 def check(self, *assumptions):
8121 """Check consistency and produce optimal values."""
8122 assumptions = _get_args(assumptions)
8123 num = len(assumptions)
8124 _assumptions = (Ast * num)()
8125 for i in range(num):
8126 _assumptions[i] = assumptions[i].as_ast()
8127 return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
8129 def reason_unknown(self):
8130 """Return a string that describes why the last `check()` returned `unknown`."""
8131 return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
8134 """Return a model for the last check()."""
8136 return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
8138 raise Z3Exception("model is not available")
8140 def unsat_core(self):
8141 return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
8143 def lower(self, obj):
8144 if not isinstance(obj, OptimizeObjective):
8145 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8148 def upper(self, obj):
8149 if not isinstance(obj, OptimizeObjective):
8150 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8153 def lower_values(self, obj):
8154 if not isinstance(obj, OptimizeObjective):
8155 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8156 return obj.lower_values()
8158 def upper_values(self, obj):
8159 if not isinstance(obj, OptimizeObjective):
8160 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8161 return obj.upper_values()
8163 def from_file(self, filename):
8164 """Parse assertions and objectives from a file"""
8165 Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
8167 def from_string(self, s):
8168 """Parse assertions and objectives from a string"""
8169 Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
8171 def assertions(self):
8172 """Return an AST vector containing all added constraints."""
8173 return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
8175 def objectives(self):
8176 """returns set of objective functions"""
8177 return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8180 """Return a formatted string with all added rules and constraints."""
8184 """Return a formatted string (in Lisp-like format) with all added constraints.
8185 We say the string is in s-expression format.
8187 return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
8189 def statistics(self):
8190 """Return statistics for the last check`.
8192 return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8194 def set_on_model(self, on_model):
8195 """Register a callback that is invoked with every incremental improvement to
8196 objective values. The callback takes a model as argument.
8197 The life-time of the model is limited to the callback so the
8198 model has to be (deep) copied if it is to be used after the callback
8200 id = len(_on_models) + 41
8201 mdl = Model(self.ctx)
8202 _on_models[id] = (on_model, mdl)
8203 self._on_models_id = id
8204 Z3_optimize_register_model_eh(
8205 self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
8209#########################################
8213#########################################
8214class ApplyResult(Z3PPObject):
8215 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal.
8216 It also contains model and proof converters.
8219 def __init__(self, result, ctx):
8220 self.result = result
8222 Z3_apply_result_inc_ref(self.ctx.ref(), self.result)
8224 def __deepcopy__(self, memo={}):
8225 return ApplyResult(self.result, self.ctx)
8228 if self.ctx.ref() is not None and Z3_apply_result_dec_ref is not None:
8229 Z3_apply_result_dec_ref(self.ctx.ref(), self.result)
8232 """Return the number of subgoals in `self`.
8234 >>> a, b = Ints('a b')
8236 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
8237 >>> t = Tactic('split-clause')
8241 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'))
8244 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values'))
8248 return int(Z3_apply_result_get_num_subgoals(self.ctx.ref(), self.result))
8250 def __getitem__(self, idx):
8251 """Return one of the subgoals stored in ApplyResult object `self`.
8253 >>> a, b = Ints('a b')
8255 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b)
8256 >>> t = Tactic('split-clause')
8259 [a == 0, Or(b == 0, b == 1), a > b]
8261 [a == 1, Or(b == 0, b == 1), a > b]
8263 if idx >= len(self):
8265 return Goal(goal=Z3_apply_result_get_subgoal(self.ctx.ref(), self.result, idx), ctx=self.ctx)
8268 return obj_to_string(self)
8271 """Return a textual representation of the s-expression representing the set of subgoals in `self`."""
8272 return Z3_apply_result_to_string(self.ctx.ref(), self.result)
8275 """Return a Z3 expression consisting of all subgoals.
8280 >>> g.add(Or(x == 2, x == 3))
8281 >>> r = Tactic('simplify')(g)
8283 [[Not(x <= 1), Or(x == 2, x == 3)]]
8285 And(Not(x <= 1), Or(x == 2, x == 3))
8286 >>> r = Tactic('split-clause')(g)
8288 [[x > 1, x == 2], [x > 1, x == 3]]
8290 Or(And(x > 1, x == 2), And(x > 1, x == 3))
8294 return BoolVal(False, self.ctx)
8296 return self[0].as_expr()
8298 return Or([self[i].as_expr() for i in range(len(self))])
8300#########################################
8304#########################################
8307 """Simplifiers act as pre-processing utilities for solvers.
8308 Build a custom simplifier and add it to a solve
r"""
8310 def __init__(self, simplifier, ctx=None):
8311 self.ctx = _get_ctx(ctx)
8312 self.simplifier = None
8313 if isinstance(simplifier, SimplifierObj):
8314 self.simplifier = simplifier
8315 elif isinstance(simplifier, list):
8316 simps = [Simplifier(s, ctx) for s in simplifier]
8317 self.simplifier = simps[0].simplifier
8318 for i in range(1, len(simps)):
8319 self.simplifier = Z3_simplifier_and_then(self.ctx.ref(), self.simplifier, simps[i].simplifier)
8320 Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
8324 _z3_assert(isinstance(simplifier, str), "simplifier name expected")
8326 self.simplifier = Z3_mk_simplifier(self.ctx.ref(), str(simplifier))
8328 raise Z3Exception("unknown simplifier '%s'" % simplifier)
8329 Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
8331 def __deepcopy__(self, memo={}):
8332 return Simplifier(self.simplifier, self.ctx)
8335 if self.simplifier is not None and self.ctx.ref() is not None and Z3_simplifier_dec_ref is not None:
8336 Z3_simplifier_dec_ref(self.ctx.ref(), self.simplifier)
8338 def using_params(self, *args, **keys):
8339 """Return a simplifier that uses the given configuration options"""
8340 p = args2params(args, keys, self.ctx)
8341 return Simplifier(Z3_simplifier_using_params(self.ctx.ref(), self.simplifier, p.params), self.ctx)
8343 def add(self, solver):
8344 """Return a solver that applies the simplification pre-processing specified by the simplifie
r"""
8345 return Solver(Z3_solver_add_simplifier(self.ctx.ref(), solver.solver, self.simplifier), self.ctx)
8348 """Display a string containing a description of the available options for the `self` simplifier."""
8349 print(Z3_simplifier_get_help(self.ctx.ref(), self.simplifier))
8351 def param_descrs(self):
8352 """Return the parameter description set."""
8353 return ParamDescrsRef(Z3_simplifier_get_param_descrs(self.ctx.ref(), self.simplifier), self.ctx)
8356#########################################
8360#########################################
8364 """Tactics transform, solver and/or simplify sets of constraints (Goal).
8365 A Tactic can be converted into a Solver using the method solver().
8367 Several combinators are available for creating new tactics using the built-in ones:
8368 Then(), OrElse(), FailIf(), Repeat(), When(), Cond().
8371 def __init__(self, tactic, ctx=None):
8372 self.ctx = _get_ctx(ctx)
8374 if isinstance(tactic, TacticObj):
8375 self.tactic = tactic
8378 _z3_assert(isinstance(tactic, str), "tactic name expected")
8380 self.tactic = Z3_mk_tactic(self.ctx.ref(), str(tactic))
8382 raise Z3Exception("unknown tactic '%s'" % tactic)
8383 Z3_tactic_inc_ref(self.ctx.ref(), self.tactic)
8385 def __deepcopy__(self, memo={}):
8386 return Tactic(self.tactic, self.ctx)
8389 if self.tactic is not None and self.ctx.ref() is not None and Z3_tactic_dec_ref is not None:
8390 Z3_tactic_dec_ref(self.ctx.ref(), self.tactic)
8392 def solver(self, logFile=None):
8393 """Create a solver using the tactic `self`.
8395 The solver supports the methods `push()` and `pop()`, but it
8396 will always solve each `check()` from scratch.
8398 >>> t = Then('simplify', 'nlsat')
8401 >>> s.add(x**2 == 2, x > 0)
8407 return Solver(Z3_mk_solver_from_tactic(self.ctx.ref(), self.tactic), self.ctx, logFile)
8409 def apply(self, goal, *arguments, **keywords):
8410 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
8412 >>> x, y = Ints('x y')
8413 >>> t = Tactic('solve-eqs')
8414 >>> t.apply(And(x == 0, y >= x + 1))
8418 _z3_assert(isinstance(goal, (Goal, BoolRef)), "Z3 Goal or Boolean expressions expected")
8419 goal = _to_goal(goal)
8420 if len(arguments) > 0 or len(keywords) > 0:
8421 p = args2params(arguments, keywords, self.ctx)
8422 return ApplyResult(Z3_tactic_apply_ex(self.ctx.ref(), self.tactic, goal.goal, p.params), self.ctx)
8424 return ApplyResult(Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
8426 def __call__(self, goal, *arguments, **keywords):
8427 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
8429 >>> x, y = Ints('x y')
8430 >>> t = Tactic('solve-eqs')
8431 >>> t(And(x == 0, y >= x + 1))
8434 return self.apply(goal, *arguments, **keywords)
8437 """Display a string containing a description of the available options for the `self` tactic."""
8438 print(Z3_tactic_get_help(self.ctx.ref(), self.tactic))
8440 def param_descrs(self):
8441 """Return the parameter description set."""
8442 return ParamDescrsRef(Z3_tactic_get_param_descrs(self.ctx.ref(), self.tactic), self.ctx)
8446 if isinstance(a, BoolRef):
8447 goal = Goal(ctx=a.ctx)
8454def _to_tactic(t, ctx=None):
8455 if isinstance(t, Tactic):
8458 return Tactic(t, ctx)
8461def _and_then(t1, t2, ctx=None):
8462 t1 = _to_tactic(t1, ctx)
8463 t2 = _to_tactic(t2, ctx)
8465 _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
8466 return Tactic(Z3_tactic_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
8469def _or_else(t1, t2, ctx=None):
8470 t1 = _to_tactic(t1, ctx)
8471 t2 = _to_tactic(t2, ctx)
8473 _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
8474 return Tactic(Z3_tactic_or_else(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
8477def AndThen(*ts, **ks):
8478 """Return a tactic that applies the tactics in `*ts` in sequence.
8480 >>> x, y = Ints('x y')
8481 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
8482 >>> t(And(x == 0, y > x + 1))
8484 >>> t(And(x == 0, y > x + 1)).as_expr()
8488 _z3_assert(len(ts) >= 2, "At least two arguments expected")
8489 ctx = ks.get("ctx", None)
8492 for i in range(num - 1):
8493 r = _and_then(r, ts[i + 1], ctx)
8498 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
8500 >>> x, y = Ints('x y')
8501 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
8502 >>> t(And(x == 0, y > x + 1))
8504 >>> t(And(x == 0, y > x + 1)).as_expr()
8507 return AndThen(*ts, **ks)
8510def OrElse(*ts, **ks):
8511 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
8514 >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
8515 >>> # Tactic split-clause fails if there is no clause in the given goal.
8518 >>> t(Or(x == 0, x == 1))
8519 [[x == 0], [x == 1]]
8522 _z3_assert(len(ts) >= 2, "At least two arguments expected")
8523 ctx = ks.get("ctx", None)
8526 for i in range(num - 1):
8527 r = _or_else(r, ts[i + 1], ctx)
8531def ParOr(*ts, **ks):
8532 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
8535 >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
8540 _z3_assert(len(ts) >= 2, "At least two arguments expected")
8541 ctx = _get_ctx(ks.get("ctx", None))
8542 ts = [_to_tactic(t, ctx) for t in ts]
8544 _args = (TacticObj * sz)()
8546 _args[i] = ts[i].tactic
8547 return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)
8550def ParThen(t1, t2, ctx=None):
8551 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1.
8552 The subgoals are processed in parallel.
8554 >>> x, y = Ints('x y')
8555 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
8556 >>> t(And(Or(x == 1, x == 2), y == x + 1))
8557 [[x == 1, y == 2], [x == 2, y == 3]]
8559 t1 = _to_tactic(t1, ctx)
8560 t2 = _to_tactic(t2, ctx)
8562 _z3_assert(t1.ctx == t2.ctx, "Context mismatch")
8563 return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
8566def ParAndThen(t1, t2, ctx=None):
8567 """Alias for ParThen(t1, t2, ctx)."""
8568 return ParThen(t1, t2, ctx)
8571def With(t, *args, **keys):
8572 """Return a tactic that applies tactic `t` using the given configuration options.
8574 >>> x, y = Ints('x y')
8575 >>> t = With(Tactic('simplify'), som=True)
8576 >>> t((x + 1)*(y + 2) == 0)
8577 [[2*x + y + x*y == -2]]
8579 ctx = keys.pop("ctx", None)
8580 t = _to_tactic(t, ctx)
8581 p = args2params(args, keys, t.ctx)
8582 return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
8585def WithParams(t, p):
8586 """Return a tactic that applies tactic `t` using the given configuration options.
8588 >>> x, y = Ints('x y')
8590 >>> p.set("som", True)
8591 >>> t = WithParams(Tactic('simplify'), p)
8592 >>> t((x + 1)*(y + 2) == 0)
8593 [[2*x + y + x*y == -2]]
8595 t = _to_tactic(t, None)
8596 return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
8599def Repeat(t, max=4294967295, ctx=None):
8600 """Return a tactic that keeps applying `t` until the goal is not modified anymore
8601 or the maximum number of iterations `max` is reached.
8603 >>> x, y = Ints('x y')
8604 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
8605 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
8607 >>> for subgoal in r: print(subgoal)
8608 [x == 0, y == 0, x > y]
8609 [x == 0, y == 1, x > y]
8610 [x == 1, y == 0, x > y]
8611 [x == 1, y == 1, x > y]
8612 >>> t = Then(t, Tactic('propagate-values'))
8616 t = _to_tactic(t, ctx)
8617 return Tactic(Z3_tactic_repeat(t.ctx.ref(), t.tactic, max), t.ctx)
8620def TryFor(t, ms, ctx=None):
8621 """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
8623 If `t` does not terminate in `ms` milliseconds, then it fails.
8625 t = _to_tactic(t, ctx)
8626 return Tactic(Z3_tactic_try_for(t.ctx.ref(), t.tactic, ms), t.ctx)
8629def tactics(ctx=None):
8630 """Return a list of all available tactics in Z3.
8633 >>> l.count('simplify') == 1
8637 return [Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref()))]
8640def tactic_description(name, ctx=None):
8641 """Return a short description for the tactic named `name`.
8643 >>> d = tactic_description('simplify')
8646 return Z3_tactic_get_descr(ctx.ref(), name)
8649def describe_tactics():
8650 """Display a (tabular) description of all available tactics in Z3."""
8653 print('<table border="1" cellpadding="2" cellspacing="0">')
8656 print('<tr style="background-color:#CFCFCF">')
8661 print("<td>%s</td><td>%s</td></tr>" % (t, insert_line_breaks(tactic_description(t), 40)))
8665 print("%s : %s" % (t, tactic_description(t)))
8669 """Probes are used to inspect a goal (aka problem) and collect information that may be used
8670 to decide which solver and/or preprocessing step will be used.
8673 def __init__(self, probe, ctx=None):
8674 self.ctx = _get_ctx(ctx)
8676 if isinstance(probe, ProbeObj):
8678 elif isinstance(probe, float):
8679 self.probe = Z3_probe_const(self.ctx.ref(), probe)
8680 elif _is_int(probe):
8681 self.probe = Z3_probe_const(self.ctx.ref(), float(probe))
8682 elif isinstance(probe, bool):
8684 self.probe = Z3_probe_const(self.ctx.ref(), 1.0)
8686 self.probe = Z3_probe_const(self.ctx.ref(), 0.0)
8689 _z3_assert(isinstance(probe, str), "probe name expected")
8691 self.probe = Z3_mk_probe(self.ctx.ref(), probe)
8693 raise Z3Exception("unknown probe '%s'" % probe)
8694 Z3_probe_inc_ref(self.ctx.ref(), self.probe)
8696 def __deepcopy__(self, memo={}):
8697 return Probe(self.probe, self.ctx)
8700 if self.probe is not None and self.ctx.ref() is not None and Z3_probe_dec_ref is not None:
8701 Z3_probe_dec_ref(self.ctx.ref(), self.probe)
8703 def __lt__(self, other):
8704 """Return a probe that evaluates to "true" when the value returned by `self`
8705 is less than the value returned by `other`.
8707 >>> p = Probe('size') < 10
8715 return Probe(Z3_probe_lt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
8717 def __gt__(self, other):
8718 """Return a probe that evaluates to "true" when the value returned by `self`
8719 is greater than the value returned by `other`.
8721 >>> p = Probe('size') > 10
8729 return Probe(Z3_probe_gt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
8731 def __le__(self, other):
8732 """Return a probe that evaluates to "true" when the value returned by `self`
8733 is less than or equal to the value returned by `other`.
8735 >>> p = Probe('size') <= 2
8743 return Probe(Z3_probe_le(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
8745 def __ge__(self, other):
8746 """Return a probe that evaluates to "true" when the value returned by `self`
8747 is greater than or equal to the value returned by `other`.
8749 >>> p = Probe('size') >= 2
8757 return Probe(Z3_probe_ge(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
8759 def __eq__(self, other):
8760 """Return a probe that evaluates to "true" when the value returned by `self`
8761 is equal to the value returned by `other`.
8763 >>> p = Probe('size') == 2
8771 return Probe(Z3_probe_eq(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
8773 def __ne__(self, other):
8774 """Return a probe that evaluates to "true" when the value returned by `self`
8775 is not equal to the value returned by `other`.
8777 >>> p = Probe('size') != 2
8785 p = self.__eq__(other)
8786 return Probe(Z3_probe_not(self.ctx.ref(), p.probe), self.ctx)
8788 def __call__(self, goal):
8789 """Evaluate the probe `self` in the given goal.
8791 >>> p = Probe('size')
8801 >>> p = Probe('num-consts')
8804 >>> p = Probe('is-propositional')
8807 >>> p = Probe('is-qflia')
8812 _z3_assert(isinstance(goal, (Goal, BoolRef)), "Z3 Goal or Boolean expression expected")
8813 goal = _to_goal(goal)
8814 return Z3_probe_apply(self.ctx.ref(), self.probe, goal.goal)
8818 """Return `True` if `p` is a Z3 probe.
8820 >>> is_probe(Int('x'))
8822 >>> is_probe(Probe('memory'))
8825 return isinstance(p, Probe)
8828def _to_probe(p, ctx=None):
8832 return Probe(p, ctx)
8835def probes(ctx=None):
8836 """Return a list of all available probes in Z3.
8839 >>> l.count('memory') == 1
8843 return [Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref()))]
8846def probe_description(name, ctx=None):
8847 """Return a short description for the probe named `name`.
8849 >>> d = probe_description('memory')
8852 return Z3_probe_get_descr(ctx.ref(), name)
8855def describe_probes():
8856 """Display a (tabular) description of all available probes in Z3."""
8859 print('<table border="1" cellpadding="2" cellspacing="0">')
8862 print('<tr style="background-color:#CFCFCF">')
8867 print("<td>%s</td><td>%s</td></tr>" % (p, insert_line_breaks(probe_description(p), 40)))
8871 print("%s : %s" % (p, probe_description(p)))
8874def _probe_nary(f, args, ctx):
8876 _z3_assert(len(args) > 0, "At least one argument expected")
8878 r = _to_probe(args[0], ctx)
8879 for i in range(num - 1):
8880 r = Probe(f(ctx.ref(), r.probe, _to_probe(args[i + 1], ctx).probe), ctx)
8884def _probe_and(args, ctx):
8885 return _probe_nary(Z3_probe_and, args, ctx)
8888def _probe_or(args, ctx):
8889 return _probe_nary(Z3_probe_or, args, ctx)
8892def FailIf(p, ctx=None):
8893 """Return a tactic that fails if the probe `p` evaluates to true.
8894 Otherwise, it returns the input goal unmodified.
8896 In the following example, the tactic applies 'simplify' if and only if there are
8897 more than 2 constraints in the goal.
8899 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8900 >>> x, y = Ints('x y')
8906 >>> g.add(x == y + 1)
8908 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8910 p = _to_probe(p, ctx)
8911 return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
8914def When(p, t, ctx=None):
8915 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true.
8916 Otherwise, it returns the input goal unmodified.
8918 >>> t = When(Probe('size') > 2, Tactic('simplify'))
8919 >>> x, y = Ints('x y')
8925 >>> g.add(x == y + 1)
8927 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8929 p = _to_probe(p, ctx)
8930 t = _to_tactic(t, ctx)
8931 return Tactic(Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)
8934def Cond(p, t1, t2, ctx=None):
8935 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8937 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8939 p = _to_probe(p, ctx)
8940 t1 = _to_tactic(t1, ctx)
8941 t2 = _to_tactic(t2, ctx)
8942 return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
8944#########################################
8948#########################################
8951def simplify(a, *arguments, **keywords):
8952 """Simplify the expression `a` using the given options.
8954 This function has many options. Use `help_simplify` to obtain the complete list.
8958 >>> simplify(x + 1 + y + x + 1)
8960 >>> simplify((x + 1)*(y + 1), som=True)
8962 >>> simplify(Distinct(x, y, 1), blast_distinct=True)
8963 And(Not(x == y), Not(x == 1), Not(y == 1))
8964 >>> simplify(And(x == 0, y == 1), elim_and=True)
8965 Not(Or(Not(x == 0), Not(y == 1)))
8968 _z3_assert(is_expr(a), "Z3 expression expected")
8969 if len(arguments) > 0 or len(keywords) > 0:
8970 p = args2params(arguments, keywords, a.ctx)
8971 return _to_expr_ref(Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
8973 return _to_expr_ref(Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
8977 """Return a string describing all options available for Z3 `simplify` procedure."""
8978 print(Z3_simplify_get_help(main_ctx().ref()))
8981def simplify_param_descrs():
8982 """Return the set of parameter descriptions for Z3 `simplify` procedure."""
8983 return ParamDescrsRef(Z3_simplify_get_param_descrs(main_ctx().ref()), main_ctx())
8986def substitute(t, *m):
8987 """Apply substitution m on t, m is a list of pairs of the form (from, to).
8988 Every occurrence in t of from is replaced with to.
8992 >>> substitute(x + 1, (x, y + 1))
8994 >>> f = Function('f', IntSort(), IntSort())
8995 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
8998 if isinstance(m, tuple):
9000 if isinstance(m1, list) and all(isinstance(p, tuple) for p in m1):
9003 _z3_assert(is_expr(t), "Z3 expression expected")
9005 all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) for p in m]),
9006 "Z3 invalid substitution, expression pairs expected.")
9008 all([p[0].sort().eq(p[1].sort()) for p in m]),
9009 'Z3 invalid substitution, mismatching "from" and "to" sorts.')
9011 _from = (Ast * num)()
9013 for i in range(num):
9014 _from[i] = m[i][0].as_ast()
9015 _to[i] = m[i][1].as_ast()
9016 return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
9019def substitute_vars(t, *m):
9020 """Substitute the free variables in t with the expression in m.
9022 >>> v0 = Var(0, IntSort())
9023 >>> v1 = Var(1, IntSort())
9025 >>> f = Function('f', IntSort(), IntSort(), IntSort())
9026 >>> # replace v0 with x+1 and v1 with x
9027 >>> substitute_vars(f(v0, v1), x + 1, x)
9031 _z3_assert(is_expr(t), "Z3 expression expected")
9032 _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.")
9035 for i in range(num):
9036 _to[i] = m[i].as_ast()
9037 return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
9039def substitute_funs(t, *m):
9040 """Apply substitution m on t, m is a list of pairs of a function and expression (from, to)
9041 Every occurrence in to of the function from is replaced with the expression to.
9042 The expression to can have free variables, that refer to the arguments of from.
9045 if isinstance(m, tuple):
9047 if isinstance(m1, list) and all(isinstance(p, tuple) for p in m1):
9050 _z3_assert(is_expr(t), "Z3 expression expected")
9051 _z3_assert(all([isinstance(p, tuple) and is_func_decl(p[0]) and is_expr(p[1]) for p in m]), "Z3 invalid substitution, function pairs expected.")
9053 _from = (FuncDecl * num)()
9055 for i in range(num):
9056 _from[i] = m[i][0].as_func_decl()
9057 _to[i] = m[i][1].as_ast()
9058 return _to_expr_ref(Z3_substitute_funs(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
9062 """Create the sum of the Z3 expressions.
9064 >>> a, b, c = Ints('a b c')
9069 >>> A = IntVector('a', 5)
9071 a__0 + a__1 + a__2 + a__3 + a__4
9073 args = _get_args(args)
9076 ctx = _ctx_from_ast_arg_list(args)
9078 return _reduce(lambda a, b: a + b, args, 0)
9079 args = _coerce_expr_list(args, ctx)
9081 return _reduce(lambda a, b: a + b, args, 0)
9083 _args, sz = _to_ast_array(args)
9084 return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx)
9088 """Create the product of the Z3 expressions.
9090 >>> a, b, c = Ints('a b c')
9091 >>> Product(a, b, c)
9093 >>> Product([a, b, c])
9095 >>> A = IntVector('a', 5)
9097 a__0*a__1*a__2*a__3*a__4
9099 args = _get_args(args)
9102 ctx = _ctx_from_ast_arg_list(args)
9104 return _reduce(lambda a, b: a * b, args, 1)
9105 args = _coerce_expr_list(args, ctx)
9107 return _reduce(lambda a, b: a * b, args, 1)
9109 _args, sz = _to_ast_array(args)
9110 return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
9113 """Create the absolute value of an arithmetic expression"""
9114 return If(arg > 0, arg, -arg)
9118 """Create an at-most Pseudo-Boolean k constraint.
9120 >>> a, b, c = Bools('a b c')
9121 >>> f = AtMost(a, b, c, 2)
9123 args = _get_args(args)
9125 _z3_assert(len(args) > 1, "Non empty list of arguments expected")
9126 ctx = _ctx_from_ast_arg_list(args)
9128 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
9129 args1 = _coerce_expr_list(args[:-1], ctx)
9131 _args, sz = _to_ast_array(args1)
9132 return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
9136 """Create an at-least Pseudo-Boolean k constraint.
9138 >>> a, b, c = Bools('a b c')
9139 >>> f = AtLeast(a, b, c, 2)
9141 args = _get_args(args)
9143 _z3_assert(len(args) > 1, "Non empty list of arguments expected")
9144 ctx = _ctx_from_ast_arg_list(args)
9146 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
9147 args1 = _coerce_expr_list(args[:-1], ctx)
9149 _args, sz = _to_ast_array(args1)
9150 return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
9153def _reorder_pb_arg(arg):
9155 if not _is_int(b) and _is_int(a):
9160def _pb_args_coeffs(args, default_ctx=None):
9161 args = _get_args_ast_list(args)
9163 return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
9164 args = [_reorder_pb_arg(arg) for arg in args]
9165 args, coeffs = zip(*args)
9167 _z3_assert(len(args) > 0, "Non empty list of arguments expected")
9168 ctx = _ctx_from_ast_arg_list(args)
9170 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
9171 args = _coerce_expr_list(args, ctx)
9172 _args, sz = _to_ast_array(args)
9173 _coeffs = (ctypes.c_int * len(coeffs))()
9174 for i in range(len(coeffs)):
9175 _z3_check_cint_overflow(coeffs[i], "coefficient")
9176 _coeffs[i] = coeffs[i]
9177 return ctx, sz, _args, _coeffs, args
9181 """Create a Pseudo-Boolean inequality k constraint.
9183 >>> a, b, c = Bools('a b c')
9184 >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
9186 _z3_check_cint_overflow(k, "k")
9187 ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
9188 return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
9192 """Create a Pseudo-Boolean inequality k constraint.
9194 >>> a, b, c = Bools('a b c')
9195 >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
9197 _z3_check_cint_overflow(k, "k")
9198 ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
9199 return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
9202def PbEq(args, k, ctx=None):
9203 """Create a Pseudo-Boolean equality k constraint.
9205 >>> a, b, c = Bools('a b c')
9206 >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
9208 _z3_check_cint_overflow(k, "k")
9209 ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
9210 return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
9213def solve(*args, **keywords):
9214 """Solve the constraints `*args`.
9216 This is a simple function for creating demonstrations. It creates a solver,
9217 configure it using the options in `keywords`, adds the constraints
9218 in `args`, and invokes check.
9221 >>> solve(a > 0, a < 2)
9224 show = keywords.pop("show", False)
9232 print("no solution")
9234 print("failed to solve")
9243def solve_using(s, *args, **keywords):
9244 """Solve the constraints `*args` using solver `s`.
9246 This is a simple function for creating demonstrations. It is similar to `solve`,
9247 but it uses the given solver `s`.
9248 It configures solver `s` using the options in `keywords`, adds the constraints
9249 in `args`, and invokes check.
9251 show = keywords.pop("show", False)
9253 _z3_assert(isinstance(s, Solver), "Solver object expected")
9261 print("no solution")
9263 print("failed to solve")
9274def prove(claim, show=False, **keywords):
9275 """Try to prove the given claim.
9277 This is a simple function for creating demonstrations. It tries to prove
9278 `claim` by showing the negation is unsatisfiable.
9280 >>> p, q = Bools('p q')
9281 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
9285 _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
9295 print("failed to prove")
9298 print("counterexample")
9302def _solve_html(*args, **keywords):
9303 """Version of function `solve` that renders HTML output."""
9304 show = keywords.pop("show", False)
9309 print("<b>Problem:</b>")
9313 print("<b>no solution</b>")
9315 print("<b>failed to solve</b>")
9322 print("<b>Solution:</b>")
9326def _solve_using_html(s, *args, **keywords):
9327 """Version of function `solve_using` that renders HTML."""
9328 show = keywords.pop("show", False)
9330 _z3_assert(isinstance(s, Solver), "Solver object expected")
9334 print("<b>Problem:</b>")
9338 print("<b>no solution</b>")
9340 print("<b>failed to solve</b>")
9347 print("<b>Solution:</b>")
9351def _prove_html(claim, show=False, **keywords):
9352 """Version of function `prove` that renders HTML."""
9354 _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
9362 print("<b>proved</b>")
9364 print("<b>failed to prove</b>")
9367 print("<b>counterexample</b>")
9371def _dict2sarray(sorts, ctx):
9373 _names = (Symbol * sz)()
9374 _sorts = (Sort * sz)()
9379 _z3_assert(isinstance(k, str), "String expected")
9380 _z3_assert(is_sort(v), "Z3 sort expected")
9381 _names[i] = to_symbol(k, ctx)
9384 return sz, _names, _sorts
9387def _dict2darray(decls, ctx):
9389 _names = (Symbol * sz)()
9390 _decls = (FuncDecl * sz)()
9395 _z3_assert(isinstance(k, str), "String expected")
9396 _z3_assert(is_func_decl(v) or is_const(v), "Z3 declaration or constant expected")
9397 _names[i] = to_symbol(k, ctx)
9399 _decls[i] = v.decl().ast
9403 return sz, _names, _decls
9406 def __init__(self, ctx= None):
9407 self.ctx = _get_ctx(ctx)
9408 self.pctx = Z3_mk_parser_context(self.ctx.ref())
9409 Z3_parser_context_inc_ref(self.ctx.ref(), self.pctx)
9412 if self.ctx.ref() is not None and self.pctx is not None and Z3_parser_context_dec_ref is not None:
9413 Z3_parser_context_dec_ref(self.ctx.ref(), self.pctx)
9416 def add_sort(self, sort):
9417 Z3_parser_context_add_sort(self.ctx.ref(), self.pctx, sort.as_ast())
9419 def add_decl(self, decl):
9420 Z3_parser_context_add_decl(self.ctx.ref(), self.pctx, decl.as_ast())
9422 def from_string(self, s):
9423 return AstVector(Z3_parser_context_from_string(self.ctx.ref(), self.pctx, s), self.ctx)
9425def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
9426 """Parse a string in SMT 2.0 format using the given sorts and decls.
9428 The arguments sorts and decls are Python dictionaries used to initialize
9429 the symbol table used for the SMT 2.0 parser.
9431 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
9433 >>> x, y = Ints('x y')
9434 >>> f = Function('f', IntSort(), IntSort())
9435 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
9437 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
9441 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
9442 dsz, dnames, ddecls = _dict2darray(decls, ctx)
9443 return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
9446def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
9447 """Parse a file in SMT 2.0 format using the given sorts and decls.
9449 This function is similar to parse_smt2_string().
9452 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
9453 dsz, dnames, ddecls = _dict2darray(decls, ctx)
9454 return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
9457#########################################
9459# Floating-Point Arithmetic
9461#########################################
9464# Global default rounding mode
9465_dflt_rounding_mode = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
9466_dflt_fpsort_ebits = 11
9467_dflt_fpsort_sbits = 53
9470def get_default_rounding_mode(ctx=None):
9471 """Retrieves the global default rounding mode."""
9472 global _dflt_rounding_mode
9473 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
9475 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
9477 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
9479 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
9481 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
9485_ROUNDING_MODES = frozenset({
9486 Z3_OP_FPA_RM_TOWARD_ZERO,
9487 Z3_OP_FPA_RM_TOWARD_NEGATIVE,
9488 Z3_OP_FPA_RM_TOWARD_POSITIVE,
9489 Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
9490 Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
9494def set_default_rounding_mode(rm, ctx=None):
9495 global _dflt_rounding_mode
9496 if is_fprm_value(rm):
9497 _dflt_rounding_mode = rm.kind()
9499 _z3_assert(_dflt_rounding_mode in _ROUNDING_MODES, "illegal rounding mode")
9500 _dflt_rounding_mode = rm
9503def get_default_fp_sort(ctx=None):
9504 return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
9507def set_default_fp_sort(ebits, sbits, ctx=None):
9508 global _dflt_fpsort_ebits
9509 global _dflt_fpsort_sbits
9510 _dflt_fpsort_ebits = ebits
9511 _dflt_fpsort_sbits = sbits
9514def _dflt_rm(ctx=None):
9515 return get_default_rounding_mode(ctx)
9518def _dflt_fps(ctx=None):
9519 return get_default_fp_sort(ctx)
9522def _coerce_fp_expr_list(alist, ctx):
9523 first_fp_sort = None
9526 if first_fp_sort is None:
9527 first_fp_sort = a.sort()
9528 elif first_fp_sort == a.sort():
9529 pass # OK, same as before
9531 # we saw at least 2 different float sorts; something will
9532 # throw a sort mismatch later, for now assume None.
9533 first_fp_sort = None
9537 for i in range(len(alist)):
9539 is_repr = isinstance(a, str) and a.contains("2**(") and a.endswith(")")
9540 if is_repr or _is_int(a) or isinstance(a, (float, bool)):
9541 r.append(FPVal(a, None, first_fp_sort, ctx))
9544 return _coerce_expr_list(r, ctx)
9549class FPSortRef(SortRef):
9550 """Floating-point sort."""
9553 """Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`.
9554 >>> b = FPSort(8, 24)
9558 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast))
9561 """Retrieves the number of bits reserved for the significand in the FloatingPoint sort `self`.
9562 >>> b = FPSort(8, 24)
9566 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast))
9568 def cast(self, val):
9569 """Try to cast `val` as a floating-point expression.
9570 >>> b = FPSort(8, 24)
9573 >>> b.cast(1.0).sexpr()
9574 '(fp #b0 #x7f #b00000000000000000000000)'
9578 _z3_assert(self.ctx == val.ctx, "Context mismatch")
9581 return FPVal(val, None, self, self.ctx)
9584def Float16(ctx=None):
9585 """Floating-point 16-bit (half) sort."""
9587 return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
9590def FloatHalf(ctx=None):
9591 """Floating-point 16-bit (half) sort."""
9593 return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
9596def Float32(ctx=None):
9597 """Floating-point 32-bit (single) sort."""
9599 return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
9602def FloatSingle(ctx=None):
9603 """Floating-point 32-bit (single) sort."""
9605 return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
9608def Float64(ctx=None):
9609 """Floating-point 64-bit (double) sort."""
9611 return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
9614def FloatDouble(ctx=None):
9615 """Floating-point 64-bit (double) sort."""
9617 return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
9620def Float128(ctx=None):
9621 """Floating-point 128-bit (quadruple) sort."""
9623 return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
9626def FloatQuadruple(ctx=None):
9627 """Floating-point 128-bit (quadruple) sort."""
9629 return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
9632class FPRMSortRef(SortRef):
9633 """"Floating-point rounding mode sort."""
9637 """Return True if `s` is a Z3 floating-point sort.
9639 >>> is_fp_sort(FPSort(8, 24))
9641 >>> is_fp_sort(IntSort())
9644 return isinstance(s, FPSortRef)
9648 """Return True if `s` is a Z3 floating-point rounding mode sort.
9650 >>> is_fprm_sort(FPSort(8, 24))
9652 >>> is_fprm_sort(RNE().sort())
9655 return isinstance(s, FPRMSortRef)
9660class FPRef(ExprRef):
9661 """Floating-point expressions."""
9664 """Return the sort of the floating-point expression `self`.
9666 >>> x = FP('1.0', FPSort(8, 24))
9669 >>> x.sort() == FPSort(8, 24)
9672 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
9675 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
9676 >>> b = FPSort(8, 24)
9680 return self.sort().ebits()
9683 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
9684 >>> b = FPSort(8, 24)
9688 return self.sort().sbits()
9690 def as_string(self):
9691 """Return a Z3 floating point expression as a Python string."""
9692 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
9694 def __le__(self, other):
9695 return fpLEQ(self, other, self.ctx)
9697 def __lt__(self, other):
9698 return fpLT(self, other, self.ctx)
9700 def __ge__(self, other):
9701 return fpGEQ(self, other, self.ctx)
9703 def __gt__(self, other):
9704 return fpGT(self, other, self.ctx)
9706 def __add__(self, other):
9707 """Create the Z3 expression `self + other`.
9709 >>> x = FP('x', FPSort(8, 24))
9710 >>> y = FP('y', FPSort(8, 24))
9716 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9717 return fpAdd(_dflt_rm(), a, b, self.ctx)
9719 def __radd__(self, other):
9720 """Create the Z3 expression `other + self`.
9722 >>> x = FP('x', FPSort(8, 24))
9726 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9727 return fpAdd(_dflt_rm(), a, b, self.ctx)
9729 def __sub__(self, other):
9730 """Create the Z3 expression `self - other`.
9732 >>> x = FP('x', FPSort(8, 24))
9733 >>> y = FP('y', FPSort(8, 24))
9739 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9740 return fpSub(_dflt_rm(), a, b, self.ctx)
9742 def __rsub__(self, other):
9743 """Create the Z3 expression `other - self`.
9745 >>> x = FP('x', FPSort(8, 24))
9749 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9750 return fpSub(_dflt_rm(), a, b, self.ctx)
9752 def __mul__(self, other):
9753 """Create the Z3 expression `self * other`.
9755 >>> x = FP('x', FPSort(8, 24))
9756 >>> y = FP('y', FPSort(8, 24))
9764 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9765 return fpMul(_dflt_rm(), a, b, self.ctx)
9767 def __rmul__(self, other):
9768 """Create the Z3 expression `other * self`.
9770 >>> x = FP('x', FPSort(8, 24))
9771 >>> y = FP('y', FPSort(8, 24))
9777 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9778 return fpMul(_dflt_rm(), a, b, self.ctx)
9781 """Create the Z3 expression `+self`."""
9785 """Create the Z3 expression `-self`.
9787 >>> x = FP('x', Float32())
9793 def __div__(self, other):
9794 """Create the Z3 expression `self / other`.
9796 >>> x = FP('x', FPSort(8, 24))
9797 >>> y = FP('y', FPSort(8, 24))
9805 [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
9806 return fpDiv(_dflt_rm(), a, b, self.ctx)
9808 def __rdiv__(self, other):
9809 """Create the Z3 expression `other / self`.
9811 >>> x = FP('x', FPSort(8, 24))
9812 >>> y = FP('y', FPSort(8, 24))
9818 [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
9819 return fpDiv(_dflt_rm(), a, b, self.ctx)
9821 def __truediv__(self, other):
9822 """Create the Z3 expression division `self / other`."""
9823 return self.__div__(other)
9825 def __rtruediv__(self, other):
9826 """Create the Z3 expression division `other / self`."""
9827 return self.__rdiv__(other)
9829 def __mod__(self, other):
9830 """Create the Z3 expression mod `self % other`."""
9831 return fpRem(self, other)
9833 def __rmod__(self, other):
9834 """Create the Z3 expression mod `other % self`."""
9835 return fpRem(other, self)
9838class FPRMRef(ExprRef):
9839 """Floating-point rounding mode expressions"""
9841 def as_string(self):
9842 """Return a Z3 floating point expression as a Python string."""
9843 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
9846def RoundNearestTiesToEven(ctx=None):
9848 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
9853 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
9856def RoundNearestTiesToAway(ctx=None):
9858 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
9863 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
9866def RoundTowardPositive(ctx=None):
9868 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
9873 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
9876def RoundTowardNegative(ctx=None):
9878 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
9883 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
9886def RoundTowardZero(ctx=None):
9888 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
9893 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
9897 """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9906 return isinstance(a, FPRMRef)
9909def is_fprm_value(a):
9910 """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9911 return is_fprm(a) and _is_numeral(a.ctx, a.ast)
9916class FPNumRef(FPRef):
9917 """The sign of the numeral.
9919 >>> x = FPVal(+1.0, FPSort(8, 24))
9922 >>> x = FPVal(-1.0, FPSort(8, 24))
9928 num = (ctypes.c_int)()
9929 nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num))
9931 raise Z3Exception("error retrieving the sign of a numeral.")
9932 return num.value != 0
9934 """The sign of a floating-point numeral as a bit-vector expression.
9936 Remark: NaN's are invalid arguments.
9939 def sign_as_bv(self):
9940 return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx)
9942 """The significand of the numeral.
9944 >>> x = FPVal(2.5, FPSort(8, 24))
9949 def significand(self):
9950 return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())
9952 """The significand of the numeral as a long.
9954 >>> x = FPVal(2.5, FPSort(8, 24))
9955 >>> x.significand_as_long()
9959 def significand_as_long(self):
9960 ptr = (ctypes.c_ulonglong * 1)()
9961 if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr):
9962 raise Z3Exception("error retrieving the significand of a numeral.")
9965 """The significand of the numeral as a bit-vector expression.
9967 Remark: NaN are invalid arguments.
9970 def significand_as_bv(self):
9971 return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx)
9973 """The exponent of the numeral.
9975 >>> x = FPVal(2.5, FPSort(8, 24))
9980 def exponent(self, biased=True):
9981 return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased)
9983 """The exponent of the numeral as a long.
9985 >>> x = FPVal(2.5, FPSort(8, 24))
9986 >>> x.exponent_as_long()
9990 def exponent_as_long(self, biased=True):
9991 ptr = (ctypes.c_longlong * 1)()
9992 if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased):
9993 raise Z3Exception("error retrieving the exponent of a numeral.")
9996 """The exponent of the numeral as a bit-vector expression.
9998 Remark: NaNs are invalid arguments.
10001 def exponent_as_bv(self, biased=True):
10002 return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx)
10004 """Indicates whether the numeral is a NaN."""
10007 return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast())
10009 """Indicates whether the numeral is +oo or -oo."""
10012 return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast())
10014 """Indicates whether the numeral is +zero or -zero."""
10017 return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast())
10019 """Indicates whether the numeral is normal."""
10021 def isNormal(self):
10022 return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast())
10024 """Indicates whether the numeral is subnormal."""
10026 def isSubnormal(self):
10027 return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
10029 """Indicates whether the numeral is positive."""
10031 def isPositive(self):
10032 return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
10034 """Indicates whether the numeral is negative."""
10036 def isNegative(self):
10037 return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast())
10040 The string representation of the numeral.
10042 >>> x = FPVal(20, FPSort(8, 24))
10047 def as_string(self):
10048 s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast())
10049 return ("FPVal(%s, %s)" % (s, self.sort()))
10053 """Return `True` if `a` is a Z3 floating-point expression.
10055 >>> b = FP('b', FPSort(8, 24))
10060 >>> is_fp(Int('x'))
10063 return isinstance(a, FPRef)
10067 """Return `True` if `a` is a Z3 floating-point numeral value.
10069 >>> b = FP('b', FPSort(8, 24))
10072 >>> b = FPVal(1.0, FPSort(8, 24))
10078 return is_fp(a) and _is_numeral(a.ctx, a.ast)
10081def FPSort(ebits, sbits, ctx=None):
10082 """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
10084 >>> Single = FPSort(8, 24)
10085 >>> Double = FPSort(11, 53)
10088 >>> x = Const('x', Single)
10089 >>> eq(x, FP('x', FPSort(8, 24)))
10092 ctx = _get_ctx(ctx)
10093 return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
10096def _to_float_str(val, exp=0):
10097 if isinstance(val, float):
10098 if math.isnan(val):
10101 sone = math.copysign(1.0, val)
10106 elif val == float("+inf"):
10108 elif val == float("-inf"):
10111 v = val.as_integer_ratio()
10114 rvs = str(num) + "/" + str(den)
10115 res = rvs + "p" + _to_int_str(exp)
10116 elif isinstance(val, bool):
10123 elif isinstance(val, str):
10124 inx = val.find("*(2**")
10127 elif val[-1] == ")":
10129 exp = str(int(val[inx + 5:-1]) + int(exp))
10131 _z3_assert(False, "String does not have floating-point numeral form.")
10133 _z3_assert(False, "Python value cannot be used to create floating-point numerals.")
10137 return res + "p" + exp
10141 """Create a Z3 floating-point NaN term.
10143 >>> s = FPSort(8, 24)
10144 >>> set_fpa_pretty(True)
10147 >>> pb = get_fpa_pretty()
10148 >>> set_fpa_pretty(False)
10150 fpNaN(FPSort(8, 24))
10151 >>> set_fpa_pretty(pb)
10153 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10154 return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
10157def fpPlusInfinity(s):
10158 """Create a Z3 floating-point +oo term.
10160 >>> s = FPSort(8, 24)
10161 >>> pb = get_fpa_pretty()
10162 >>> set_fpa_pretty(True)
10163 >>> fpPlusInfinity(s)
10165 >>> set_fpa_pretty(False)
10166 >>> fpPlusInfinity(s)
10167 fpPlusInfinity(FPSort(8, 24))
10168 >>> set_fpa_pretty(pb)
10170 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10171 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
10174def fpMinusInfinity(s):
10175 """Create a Z3 floating-point -oo term."""
10176 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10177 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
10180def fpInfinity(s, negative):
10181 """Create a Z3 floating-point +oo or -oo term."""
10182 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10183 _z3_assert(isinstance(negative, bool), "expected Boolean flag")
10184 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
10188 """Create a Z3 floating-point +0.0 term."""
10189 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10190 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
10194 """Create a Z3 floating-point -0.0 term."""
10195 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10196 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
10199def fpZero(s, negative):
10200 """Create a Z3 floating-point +0.0 or -0.0 term."""
10201 _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
10202 _z3_assert(isinstance(negative, bool), "expected Boolean flag")
10203 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
10206def FPVal(sig, exp=None, fps=None, ctx=None):
10207 """Return a floating-point value of value `val` and sort `fps`.
10208 If `ctx=None`, then the global context is used.
10210 >>> v = FPVal(20.0, FPSort(8, 24))
10213 >>> print("0x%.8x" % v.exponent_as_long(False))
10215 >>> v = FPVal(2.25, FPSort(8, 24))
10218 >>> v = FPVal(-2.25, FPSort(8, 24))
10221 >>> FPVal(-0.0, FPSort(8, 24))
10223 >>> FPVal(0.0, FPSort(8, 24))
10225 >>> FPVal(+0.0, FPSort(8, 24))
10228 ctx = _get_ctx(ctx)
10229 if is_fp_sort(exp):
10233 fps = _dflt_fps(ctx)
10234 _z3_assert(is_fp_sort(fps), "sort mismatch")
10237 val = _to_float_str(sig)
10238 if val == "NaN" or val == "nan":
10240 elif val == "-0.0":
10241 return fpMinusZero(fps)
10242 elif val == "0.0" or val == "+0.0":
10243 return fpPlusZero(fps)
10244 elif val == "+oo" or val == "+inf" or val == "+Inf":
10245 return fpPlusInfinity(fps)
10246 elif val == "-oo" or val == "-inf" or val == "-Inf":
10247 return fpMinusInfinity(fps)
10249 return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
10252def FP(name, fpsort, ctx=None):
10253 """Return a floating-point constant named `name`.
10254 `fpsort` is the floating-point sort.
10255 If `ctx=None`, then the global context is used.
10257 >>> x = FP('x', FPSort(8, 24))
10264 >>> word = FPSort(8, 24)
10265 >>> x2 = FP('x', word)
10269 if isinstance(fpsort, FPSortRef) and ctx is None:
10272 ctx = _get_ctx(ctx)
10273 return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
10276def FPs(names, fpsort, ctx=None):
10277 """Return an array of floating-point constants.
10279 >>> x, y, z = FPs('x y z', FPSort(8, 24))
10286 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
10289 ctx = _get_ctx(ctx)
10290 if isinstance(names, str):
10291 names = names.split(" ")
10292 return [FP(name, fpsort, ctx) for name in names]
10295def fpAbs(a, ctx=None):
10296 """Create a Z3 floating-point absolute value expression.
10298 >>> s = FPSort(8, 24)
10300 >>> x = FPVal(1.0, s)
10303 >>> y = FPVal(-20.0, s)
10307 fpAbs(-1.25*(2**4))
10308 >>> fpAbs(-1.25*(2**4))
10309 fpAbs(-1.25*(2**4))
10310 >>> fpAbs(x).sort()
10313 ctx = _get_ctx(ctx)
10314 [a] = _coerce_fp_expr_list([a], ctx)
10315 return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
10318def fpNeg(a, ctx=None):
10319 """Create a Z3 floating-point addition expression.
10321 >>> s = FPSort(8, 24)
10326 >>> fpNeg(x).sort()
10329 ctx = _get_ctx(ctx)
10330 [a] = _coerce_fp_expr_list([a], ctx)
10331 return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
10334def _mk_fp_unary(f, rm, a, ctx):
10335 ctx = _get_ctx(ctx)
10336 [a] = _coerce_fp_expr_list([a], ctx)
10338 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10339 _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression")
10340 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx)
10343def _mk_fp_unary_pred(f, a, ctx):
10344 ctx = _get_ctx(ctx)
10345 [a] = _coerce_fp_expr_list([a], ctx)
10347 _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression")
10348 return BoolRef(f(ctx.ref(), a.as_ast()), ctx)
10351def _mk_fp_bin(f, rm, a, b, ctx):
10352 ctx = _get_ctx(ctx)
10353 [a, b] = _coerce_fp_expr_list([a, b], ctx)
10355 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10356 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
10357 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx)
10360def _mk_fp_bin_norm(f, a, b, ctx):
10361 ctx = _get_ctx(ctx)
10362 [a, b] = _coerce_fp_expr_list([a, b], ctx)
10364 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression")
10365 return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
10368def _mk_fp_bin_pred(f, a, b, ctx):
10369 ctx = _get_ctx(ctx)
10370 [a, b] = _coerce_fp_expr_list([a, b], ctx)
10372 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression")
10373 return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
10376def _mk_fp_tern(f, rm, a, b, c, ctx):
10377 ctx = _get_ctx(ctx)
10378 [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx)
10380 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10381 _z3_assert(is_fp(a) or is_fp(b) or is_fp(
10382 c), "Second, third or fourth argument must be a Z3 floating-point expression")
10383 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
10386def fpAdd(rm, a, b, ctx=None):
10387 """Create a Z3 floating-point addition expression.
10389 >>> s = FPSort(8, 24)
10393 >>> fpAdd(rm, x, y)
10395 >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
10397 >>> fpAdd(rm, x, y).sort()
10400 return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
10403def fpSub(rm, a, b, ctx=None):
10404 """Create a Z3 floating-point subtraction expression.
10406 >>> s = FPSort(8, 24)
10410 >>> fpSub(rm, x, y)
10412 >>> fpSub(rm, x, y).sort()
10415 return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
10418def fpMul(rm, a, b, ctx=None):
10419 """Create a Z3 floating-point multiplication expression.
10421 >>> s = FPSort(8, 24)
10425 >>> fpMul(rm, x, y)
10427 >>> fpMul(rm, x, y).sort()
10430 return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
10433def fpDiv(rm, a, b, ctx=None):
10434 """Create a Z3 floating-point division expression.
10436 >>> s = FPSort(8, 24)
10440 >>> fpDiv(rm, x, y)
10442 >>> fpDiv(rm, x, y).sort()
10445 return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
10448def fpRem(a, b, ctx=None):
10449 """Create a Z3 floating-point remainder expression.
10451 >>> s = FPSort(8, 24)
10456 >>> fpRem(x, y).sort()
10459 return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
10462def fpMin(a, b, ctx=None):
10463 """Create a Z3 floating-point minimum expression.
10465 >>> s = FPSort(8, 24)
10471 >>> fpMin(x, y).sort()
10474 return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
10477def fpMax(a, b, ctx=None):
10478 """Create a Z3 floating-point maximum expression.
10480 >>> s = FPSort(8, 24)
10486 >>> fpMax(x, y).sort()
10489 return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
10492def fpFMA(rm, a, b, c, ctx=None):
10493 """Create a Z3 floating-point fused multiply-add expression.
10495 return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
10498def fpSqrt(rm, a, ctx=None):
10499 """Create a Z3 floating-point square root expression.
10501 return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
10504def fpRoundToIntegral(rm, a, ctx=None):
10505 """Create a Z3 floating-point roundToIntegral expression.
10507 return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
10510def fpIsNaN(a, ctx=None):
10511 """Create a Z3 floating-point isNaN expression.
10513 >>> s = FPSort(8, 24)
10519 return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
10522def fpIsInf(a, ctx=None):
10523 """Create a Z3 floating-point isInfinite expression.
10525 >>> s = FPSort(8, 24)
10530 return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
10533def fpIsZero(a, ctx=None):
10534 """Create a Z3 floating-point isZero expression.
10536 return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
10539def fpIsNormal(a, ctx=None):
10540 """Create a Z3 floating-point isNormal expression.
10542 return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
10545def fpIsSubnormal(a, ctx=None):
10546 """Create a Z3 floating-point isSubnormal expression.
10548 return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
10551def fpIsNegative(a, ctx=None):
10552 """Create a Z3 floating-point isNegative expression.
10554 return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
10557def fpIsPositive(a, ctx=None):
10558 """Create a Z3 floating-point isPositive expression.
10560 return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
10563def _check_fp_args(a, b):
10565 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression")
10568def fpLT(a, b, ctx=None):
10569 """Create the Z3 floating-point expression `other < self`.
10571 >>> x, y = FPs('x y', FPSort(8, 24))
10574 >>> (x < y).sexpr()
10577 return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
10580def fpLEQ(a, b, ctx=None):
10581 """Create the Z3 floating-point expression `other <= self`.
10583 >>> x, y = FPs('x y', FPSort(8, 24))
10586 >>> (x <= y).sexpr()
10589 return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
10592def fpGT(a, b, ctx=None):
10593 """Create the Z3 floating-point expression `other > self`.
10595 >>> x, y = FPs('x y', FPSort(8, 24))
10598 >>> (x > y).sexpr()
10601 return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
10604def fpGEQ(a, b, ctx=None):
10605 """Create the Z3 floating-point expression `other >= self`.
10607 >>> x, y = FPs('x y', FPSort(8, 24))
10610 >>> (x >= y).sexpr()
10613 return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
10616def fpEQ(a, b, ctx=None):
10617 """Create the Z3 floating-point expression `fpEQ(other, self)`.
10619 >>> x, y = FPs('x y', FPSort(8, 24))
10622 >>> fpEQ(x, y).sexpr()
10625 return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
10628def fpNEQ(a, b, ctx=None):
10629 """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
10631 >>> x, y = FPs('x y', FPSort(8, 24))
10634 >>> (x != y).sexpr()
10637 return Not(fpEQ(a, b, ctx))
10640def fpFP(sgn, exp, sig, ctx=None):
10641 """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
10643 >>> s = FPSort(8, 24)
10644 >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
10646 fpFP(1, 127, 4194304)
10647 >>> xv = FPVal(-1.5, s)
10650 >>> slvr = Solver()
10651 >>> slvr.add(fpEQ(x, xv))
10654 >>> xv = FPVal(+1.5, s)
10657 >>> slvr = Solver()
10658 >>> slvr.add(fpEQ(x, xv))
10662 _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
10663 _z3_assert(sgn.sort().size() == 1, "sort mismatch")
10664 ctx = _get_ctx(ctx)
10665 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
10666 return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
10669def fpToFP(a1, a2=None, a3=None, ctx=None):
10670 """Create a Z3 floating-point conversion expression from other term sorts
10673 From a bit-vector term in IEEE 754-2008 format:
10674 >>> x = FPVal(1.0, Float32())
10675 >>> x_bv = fpToIEEEBV(x)
10676 >>> simplify(fpToFP(x_bv, Float32()))
10679 From a floating-point term with different precision:
10680 >>> x = FPVal(1.0, Float32())
10681 >>> x_db = fpToFP(RNE(), x, Float64())
10686 >>> x_r = RealVal(1.5)
10687 >>> simplify(fpToFP(RNE(), x_r, Float32()))
10690 From a signed bit-vector term:
10691 >>> x_signed = BitVecVal(-5, BitVecSort(32))
10692 >>> simplify(fpToFP(RNE(), x_signed, Float32()))
10695 ctx = _get_ctx(ctx)
10696 if is_bv(a1) and is_fp_sort(a2):
10697 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
10698 elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
10699 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10700 elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
10701 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10702 elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
10703 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
10705 raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
10708def fpBVToFP(v, sort, ctx=None):
10709 """Create a Z3 floating-point conversion expression that represents the
10710 conversion from a bit-vector term to a floating-point term.
10712 >>> x_bv = BitVecVal(0x3F800000, 32)
10713 >>> x_fp = fpBVToFP(x_bv, Float32())
10719 _z3_assert(is_bv(v), "First argument must be a Z3 bit-vector expression")
10720 _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.")
10721 ctx = _get_ctx(ctx)
10722 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
10725def fpFPToFP(rm, v, sort, ctx=None):
10726 """Create a Z3 floating-point conversion expression that represents the
10727 conversion from a floating-point term to a floating-point term of different precision.
10729 >>> x_sgl = FPVal(1.0, Float32())
10730 >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
10733 >>> simplify(x_dbl)
10738 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10739 _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.")
10740 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10741 ctx = _get_ctx(ctx)
10742 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10745def fpRealToFP(rm, v, sort, ctx=None):
10746 """Create a Z3 floating-point conversion expression that represents the
10747 conversion from a real term to a floating-point term.
10749 >>> x_r = RealVal(1.5)
10750 >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
10756 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10757 _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.")
10758 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10759 ctx = _get_ctx(ctx)
10760 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10763def fpSignedToFP(rm, v, sort, ctx=None):
10764 """Create a Z3 floating-point conversion expression that represents the
10765 conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
10767 >>> x_signed = BitVecVal(-5, BitVecSort(32))
10768 >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
10770 fpToFP(RNE(), 4294967291)
10774 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10775 _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10776 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10777 ctx = _get_ctx(ctx)
10778 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10781def fpUnsignedToFP(rm, v, sort, ctx=None):
10782 """Create a Z3 floating-point conversion expression that represents the
10783 conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
10785 >>> x_signed = BitVecVal(-5, BitVecSort(32))
10786 >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
10788 fpToFPUnsigned(RNE(), 4294967291)
10792 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.")
10793 _z3_assert(is_bv(v), "Second argument must be a Z3 bit-vector expression")
10794 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.")
10795 ctx = _get_ctx(ctx)
10796 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
10799def fpToFPUnsigned(rm, x, s, ctx=None):
10800 """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
10802 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10803 _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
10804 _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
10805 ctx = _get_ctx(ctx)
10806 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
10809def fpToSBV(rm, x, s, ctx=None):
10810 """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
10812 >>> x = FP('x', FPSort(8, 24))
10813 >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
10814 >>> print(is_fp(x))
10816 >>> print(is_bv(y))
10818 >>> print(is_fp(y))
10820 >>> print(is_bv(x))
10824 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10825 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10826 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10827 ctx = _get_ctx(ctx)
10828 return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10831def fpToUBV(rm, x, s, ctx=None):
10832 """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
10834 >>> x = FP('x', FPSort(8, 24))
10835 >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
10836 >>> print(is_fp(x))
10838 >>> print(is_bv(y))
10840 >>> print(is_fp(y))
10842 >>> print(is_bv(x))
10846 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
10847 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
10848 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
10849 ctx = _get_ctx(ctx)
10850 return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
10853def fpToReal(x, ctx=None):
10854 """Create a Z3 floating-point conversion expression, from floating-point expression to real.
10856 >>> x = FP('x', FPSort(8, 24))
10857 >>> y = fpToReal(x)
10858 >>> print(is_fp(x))
10860 >>> print(is_real(y))
10862 >>> print(is_fp(y))
10864 >>> print(is_real(x))
10868 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10869 ctx = _get_ctx(ctx)
10870 return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
10873def fpToIEEEBV(x, ctx=None):
10874 """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
10876 The size of the resulting bit-vector is automatically determined.
10878 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
10879 knows only one NaN and it will always produce the same bit-vector representation of
10882 >>> x = FP('x', FPSort(8, 24))
10883 >>> y = fpToIEEEBV(x)
10884 >>> print(is_fp(x))
10886 >>> print(is_bv(y))
10888 >>> print(is_fp(y))
10890 >>> print(is_bv(x))
10894 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
10895 ctx = _get_ctx(ctx)
10896 return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
10899#########################################
10901# Strings, Sequences and Regular expressions
10903#########################################
10905class SeqSortRef(SortRef):
10906 """Sequence sort."""
10908 def is_string(self):
10909 """Determine if sort is a string
10910 >>> s = StringSort()
10913 >>> s = SeqSort(IntSort())
10917 return Z3_is_string_sort(self.ctx_ref(), self.ast)
10920 return _to_sort_ref(Z3_get_seq_sort_basis(self.ctx_ref(), self.ast), self.ctx)
10922class CharSortRef(SortRef):
10923 """Character sort."""
10926def StringSort(ctx=None):
10927 """Create a string sort
10928 >>> s = StringSort()
10932 ctx = _get_ctx(ctx)
10933 return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx)
10935def CharSort(ctx=None):
10936 """Create a character sort
10937 >>> ch = CharSort()
10941 ctx = _get_ctx(ctx)
10942 return CharSortRef(Z3_mk_char_sort(ctx.ref()), ctx)
10946 """Create a sequence sort over elements provided in the argument
10947 >>> s = SeqSort(IntSort())
10948 >>> s == Unit(IntVal(1)).sort()
10951 return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx)
10954class SeqRef(ExprRef):
10955 """Sequence expression."""
10958 return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
10960 def __add__(self, other):
10961 return Concat(self, other)
10963 def __radd__(self, other):
10964 return Concat(other, self)
10966 def __getitem__(self, i):
10968 i = IntVal(i, self.ctx)
10969 return _to_expr_ref(Z3_mk_seq_nth(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
10973 i = IntVal(i, self.ctx)
10974 return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
10976 def is_string(self):
10977 return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast()))
10979 def is_string_value(self):
10980 return Z3_is_string(self.ctx_ref(), self.as_ast())
10982 def as_string(self):
10983 """Return a string representation of sequence expression."""
10984 if self.is_string_value():
10985 string_length = ctypes.c_uint()
10986 chars = Z3_get_lstring(self.ctx_ref(), self.as_ast(), byref(string_length))
10987 return string_at(chars, size=string_length.value).decode("latin-1")
10988 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
10990 def __le__(self, other):
10991 return _to_expr_ref(Z3_mk_str_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
10993 def __lt__(self, other):
10994 return _to_expr_ref(Z3_mk_str_lt(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
10996 def __ge__(self, other):
10997 return _to_expr_ref(Z3_mk_str_le(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
10999 def __gt__(self, other):
11000 return _to_expr_ref(Z3_mk_str_lt(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
11003def _coerce_char(ch, ctx=None):
11004 if isinstance(ch, str):
11005 ctx = _get_ctx(ctx)
11006 ch = CharVal(ch, ctx)
11007 if not is_expr(ch):
11008 raise Z3Exception("Character expression expected")
11011class CharRef(ExprRef):
11012 """Character expression."""
11014 def __le__(self, other):
11015 other = _coerce_char(other, self.ctx)
11016 return _to_expr_ref(Z3_mk_char_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
11019 return _to_expr_ref(Z3_mk_char_to_int(self.ctx_ref(), self.as_ast()), self.ctx)
11022 return _to_expr_ref(Z3_mk_char_to_bv(self.ctx_ref(), self.as_ast()), self.ctx)
11024 def is_digit(self):
11025 return _to_expr_ref(Z3_mk_char_is_digit(self.ctx_ref(), self.as_ast()), self.ctx)
11028def CharVal(ch, ctx=None):
11029 ctx = _get_ctx(ctx)
11030 if isinstance(ch, str):
11032 if not isinstance(ch, int):
11033 raise Z3Exception("character value should be an ordinal")
11034 return _to_expr_ref(Z3_mk_char(ctx.ref(), ch), ctx)
11037 if not is_expr(bv):
11038 raise Z3Exception("Bit-vector expression needed")
11039 return _to_expr_ref(Z3_mk_char_from_bv(bv.ctx_ref(), bv.as_ast()), bv.ctx)
11041def CharToBv(ch, ctx=None):
11042 ch = _coerce_char(ch, ctx)
11045def CharToInt(ch, ctx=None):
11046 ch = _coerce_char(ch, ctx)
11049def CharIsDigit(ch, ctx=None):
11050 ch = _coerce_char(ch, ctx)
11051 return ch.is_digit()
11053def _coerce_seq(s, ctx=None):
11054 if isinstance(s, str):
11055 ctx = _get_ctx(ctx)
11056 s = StringVal(s, ctx)
11058 raise Z3Exception("Non-expression passed as a sequence")
11060 raise Z3Exception("Non-sequence passed as a sequence")
11064def _get_ctx2(a, b, ctx=None):
11075 """Return `True` if `a` is a Z3 sequence expression.
11076 >>> print (is_seq(Unit(IntVal(0))))
11078 >>> print (is_seq(StringVal("abc")))
11081 return isinstance(a, SeqRef)
11085 """Return `True` if `a` is a Z3 string expression.
11086 >>> print (is_string(StringVal("ab")))
11089 return isinstance(a, SeqRef) and a.is_string()
11092def is_string_value(a):
11093 """return 'True' if 'a' is a Z3 string constant expression.
11094 >>> print (is_string_value(StringVal("a")))
11096 >>> print (is_string_value(StringVal("a") + StringVal("b")))
11099 return isinstance(a, SeqRef) and a.is_string_value()
11101def StringVal(s, ctx=None):
11102 """create a string expression"""
11103 s = "".join(str(ch) if 32 <= ord(ch) and ord(ch) < 127 else "\\u{%x}" % (ord(ch)) for ch in s)
11104 ctx = _get_ctx(ctx)
11105 return SeqRef(Z3_mk_string(ctx.ref(), s), ctx)
11108def String(name, ctx=None):
11109 """Return a string constant named `name`. If `ctx=None`, then the global context is used.
11111 >>> x = String('x')
11113 ctx = _get_ctx(ctx)
11114 return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx)
11117def Strings(names, ctx=None):
11118 """Return a tuple of String constants. """
11119 ctx = _get_ctx(ctx)
11120 if isinstance(names, str):
11121 names = names.split(" ")
11122 return [String(name, ctx) for name in names]
11125def SubString(s, offset, length):
11126 """Extract substring or subsequence starting at offset"""
11127 return Extract(s, offset, length)
11130def SubSeq(s, offset, length):
11131 """Extract substring or subsequence starting at offset"""
11132 return Extract(s, offset, length)
11136 """Create the empty sequence of the given sort
11137 >>> e = Empty(StringSort())
11138 >>> e2 = StringVal("")
11139 >>> print(e.eq(e2))
11141 >>> e3 = Empty(SeqSort(IntSort()))
11144 >>> e4 = Empty(ReSort(SeqSort(IntSort())))
11146 Empty(ReSort(Seq(Int)))
11148 if isinstance(s, SeqSortRef):
11149 return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
11150 if isinstance(s, ReSortRef):
11151 return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
11152 raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
11156 """Create the regular expression that accepts the universal language
11157 >>> e = Full(ReSort(SeqSort(IntSort())))
11159 Full(ReSort(Seq(Int)))
11160 >>> e1 = Full(ReSort(StringSort()))
11162 Full(ReSort(String))
11164 if isinstance(s, ReSortRef):
11165 return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
11166 raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
11171 """Create a singleton sequence"""
11172 return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx)
11176 """Check if 'a' is a prefix of 'b'
11177 >>> s1 = PrefixOf("ab", "abc")
11180 >>> s2 = PrefixOf("bc", "abc")
11184 ctx = _get_ctx2(a, b)
11185 a = _coerce_seq(a, ctx)
11186 b = _coerce_seq(b, ctx)
11187 return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
11191 """Check if 'a' is a suffix of 'b'
11192 >>> s1 = SuffixOf("ab", "abc")
11195 >>> s2 = SuffixOf("bc", "abc")
11199 ctx = _get_ctx2(a, b)
11200 a = _coerce_seq(a, ctx)
11201 b = _coerce_seq(b, ctx)
11202 return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
11206 """Check if 'a' contains 'b'
11207 >>> s1 = Contains("abc", "ab")
11210 >>> s2 = Contains("abc", "bc")
11213 >>> x, y, z = Strings('x y z')
11214 >>> s3 = Contains(Concat(x,y,z), y)
11218 ctx = _get_ctx2(a, b)
11219 a = _coerce_seq(a, ctx)
11220 b = _coerce_seq(b, ctx)
11221 return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
11224def Replace(s, src, dst):
11225 """Replace the first occurrence of 'src' by 'dst' in 's'
11226 >>> r = Replace("aaa", "a", "b")
11230 ctx = _get_ctx2(dst, s)
11231 if ctx is None and is_expr(src):
11233 src = _coerce_seq(src, ctx)
11234 dst = _coerce_seq(dst, ctx)
11235 s = _coerce_seq(s, ctx)
11236 return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx)
11239def IndexOf(s, substr, offset=None):
11240 """Retrieve the index of substring within a string starting at a specified offset.
11241 >>> simplify(IndexOf("abcabc", "bc", 0))
11243 >>> simplify(IndexOf("abcabc", "bc", 2))
11249 if is_expr(offset):
11251 ctx = _get_ctx2(s, substr, ctx)
11252 s = _coerce_seq(s, ctx)
11253 substr = _coerce_seq(substr, ctx)
11254 if _is_int(offset):
11255 offset = IntVal(offset, ctx)
11256 return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
11259def LastIndexOf(s, substr):
11260 """Retrieve the last index of substring within a string"""
11262 ctx = _get_ctx2(s, substr, ctx)
11263 s = _coerce_seq(s, ctx)
11264 substr = _coerce_seq(substr, ctx)
11265 return ArithRef(Z3_mk_seq_last_index(s.ctx_ref(), s.as_ast(), substr.as_ast()), s.ctx)
11269 """Obtain the length of a sequence 's'
11270 >>> l = Length(StringVal("abc"))
11275 return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
11278 """Map function 'f' over sequence 's'"""
11279 ctx = _get_ctx2(f, s)
11280 s = _coerce_seq(s, ctx)
11281 return _to_expr_ref(Z3_mk_seq_map(s.ctx_ref(), f.as_ast(), s.as_ast()), ctx)
11283def SeqMapI(f, i, s):
11284 """Map function 'f' over sequence 's' at index 'i'"""
11285 ctx = _get_ctx(f, s)
11286 s = _coerce_seq(s, ctx)
11289 return _to_expr_ref(Z3_mk_seq_mapi(s.ctx_ref(), f.as_ast(), i.as_ast(), s.as_ast()), ctx)
11291def SeqFoldLeft(f, a, s):
11292 ctx = _get_ctx2(f, s)
11293 s = _coerce_seq(s, ctx)
11295 return _to_expr_ref(Z3_mk_seq_foldl(s.ctx_ref(), f.as_ast(), a.as_ast(), s.as_ast()), ctx)
11297def SeqFoldLeftI(f, i, a, s):
11298 ctx = _get_ctx2(f, s)
11299 s = _coerce_seq(s, ctx)
11302 return _to_expr_ref(Z3_mk_seq_foldli(s.ctx_ref(), f.as_ast(), i.as_ast(), a.as_ast(), s.as_ast()), ctx)
11305 """Convert string expression to integer
11306 >>> a = StrToInt("1")
11307 >>> simplify(1 == a)
11309 >>> b = StrToInt("2")
11310 >>> simplify(1 == b)
11312 >>> c = StrToInt(IntToStr(2))
11313 >>> simplify(1 == c)
11317 return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx)
11321 """Convert integer expression to string"""
11324 return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
11328 """Convert a unit length string to integer code"""
11331 return ArithRef(Z3_mk_string_to_code(s.ctx_ref(), s.as_ast()), s.ctx)
11334 """Convert code to a string"""
11337 return SeqRef(Z3_mk_string_from_code(c.ctx_ref(), c.as_ast()), c.ctx)
11339def Re(s, ctx=None):
11340 """The regular expression that accepts sequence 's'
11342 >>> s2 = Re(StringVal("ab"))
11343 >>> s3 = Re(Unit(BoolVal(True)))
11345 s = _coerce_seq(s, ctx)
11346 return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx)
11349# Regular expressions
11351class ReSortRef(SortRef):
11352 """Regular expression sort."""
11355 return _to_sort_ref(Z3_get_re_sort_basis(self.ctx_ref(), self.ast), self.ctx)
11360 return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx)
11361 if s is None or isinstance(s, Context):
11363 return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), s.ctx)
11364 raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument")
11367class ReRef(ExprRef):
11368 """Regular expressions."""
11370 def __add__(self, other):
11371 return Union(self, other)
11375 return isinstance(s, ReRef)
11379 """Create regular expression membership test
11380 >>> re = Union(Re("a"),Re("b"))
11381 >>> print (simplify(InRe("a", re)))
11383 >>> print (simplify(InRe("b", re)))
11385 >>> print (simplify(InRe("c", re)))
11388 s = _coerce_seq(s, re.ctx)
11389 return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
11393 """Create union of regular expressions.
11394 >>> re = Union(Re("a"), Re("b"), Re("c"))
11395 >>> print (simplify(InRe("d", re)))
11398 args = _get_args(args)
11401 _z3_assert(sz > 0, "At least one argument expected.")
11402 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
11407 for i in range(sz):
11408 v[i] = args[i].as_ast()
11409 return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx)
11412def Intersect(*args):
11413 """Create intersection of regular expressions.
11414 >>> re = Intersect(Re("a"), Re("b"), Re("c"))
11416 args = _get_args(args)
11419 _z3_assert(sz > 0, "At least one argument expected.")
11420 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
11425 for i in range(sz):
11426 v[i] = args[i].as_ast()
11427 return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)
11431 """Create the regular expression accepting one or more repetitions of argument.
11432 >>> re = Plus(Re("a"))
11433 >>> print(simplify(InRe("aa", re)))
11435 >>> print(simplify(InRe("ab", re)))
11437 >>> print(simplify(InRe("", re)))
11441 _z3_assert(is_expr(re), "expression expected")
11442 return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)
11446 """Create the regular expression that optionally accepts the argument.
11447 >>> re = Option(Re("a"))
11448 >>> print(simplify(InRe("a", re)))
11450 >>> print(simplify(InRe("", re)))
11452 >>> print(simplify(InRe("aa", re)))
11456 _z3_assert(is_expr(re), "expression expected")
11457 return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)
11461 """Create the complement regular expression."""
11462 return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
11466 """Create the regular expression accepting zero or more repetitions of argument.
11467 >>> re = Star(Re("a"))
11468 >>> print(simplify(InRe("aa", re)))
11470 >>> print(simplify(InRe("ab", re)))
11472 >>> print(simplify(InRe("", re)))
11476 _z3_assert(is_expr(re), "expression expected")
11477 return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)
11480def Loop(re, lo, hi=0):
11481 """Create the regular expression accepting between a lower and upper bound repetitions
11482 >>> re = Loop(Re("a"), 1, 3)
11483 >>> print(simplify(InRe("aa", re)))
11485 >>> print(simplify(InRe("aaaa", re)))
11487 >>> print(simplify(InRe("", re)))
11491 _z3_assert(is_expr(re), "expression expected")
11492 return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)
11495def Range(lo, hi, ctx=None):
11496 """Create the range regular expression over two sequences of length 1
11497 >>> range = Range("a","z")
11498 >>> print(simplify(InRe("b", range)))
11500 >>> print(simplify(InRe("bb", range)))
11503 lo = _coerce_seq(lo, ctx)
11504 hi = _coerce_seq(hi, ctx)
11506 _z3_assert(is_expr(lo), "expression expected")
11507 _z3_assert(is_expr(hi), "expression expected")
11508 return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)
11510def Diff(a, b, ctx=None):
11511 """Create the difference regular expression
11514 _z3_assert(is_expr(a), "expression expected")
11515 _z3_assert(is_expr(b), "expression expected")
11516 return ReRef(Z3_mk_re_diff(a.ctx_ref(), a.ast, b.ast), a.ctx)
11518def AllChar(regex_sort, ctx=None):
11519 """Create a regular expression that accepts all single character strings
11521 return ReRef(Z3_mk_re_allchar(regex_sort.ctx_ref(), regex_sort.ast), regex_sort.ctx)
11526def PartialOrder(a, index):
11527 return FuncDeclRef(Z3_mk_partial_order(a.ctx_ref(), a.ast, index), a.ctx)
11530def LinearOrder(a, index):
11531 return FuncDeclRef(Z3_mk_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
11534def TreeOrder(a, index):
11535 return FuncDeclRef(Z3_mk_tree_order(a.ctx_ref(), a.ast, index), a.ctx)
11538def PiecewiseLinearOrder(a, index):
11539 return FuncDeclRef(Z3_mk_piecewise_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
11542def TransitiveClosure(f):
11543 """Given a binary relation R, such that the two arguments have the same sort
11544 create the transitive closure relation R+.
11545 The transitive closure R+ is a new relation.
11547 return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.ctx)
11551 super(ctypes.c_void_p, ast).__init__(ptr)
11554def to_ContextObj(ptr,):
11555 ctx = ContextObj(ptr)
11556 super(ctypes.c_void_p, ctx).__init__(ptr)
11559def to_AstVectorObj(ptr,):
11560 v = AstVectorObj(ptr)
11561 super(ctypes.c_void_p, v).__init__(ptr)
11564# NB. my-hacky-class only works for a single instance of OnClause
11565# it should be replaced with a proper correlation between OnClause
11566# and object references that can be passed over the FFI.
11567# for UserPropagator we use a global dictionary, which isn't great code.
11569_my_hacky_class = None
11570def on_clause_eh(ctx, p, n, dep, clause):
11571 onc = _my_hacky_class
11572 p = _to_expr_ref(to_Ast(p), onc.ctx)
11573 clause = AstVector(to_AstVectorObj(clause), onc.ctx)
11574 deps = [dep[i] for i in range(n)]
11575 onc.on_clause(p, deps, clause)
11577_on_clause_eh = Z3_on_clause_eh(on_clause_eh)
11580 def __init__(self, s, on_clause):
11583 self.on_clause = on_clause
11585 global _my_hacky_class
11586 _my_hacky_class = self
11587 Z3_solver_register_on_clause(self.ctx.ref(), self.s.solver, self.idx, _on_clause_eh)
11591 def __init__(self):
11595 def set_threaded(self):
11596 if self.lock is None:
11598 self.lock = threading.Lock()
11600 def get(self, ctx):
11603 r = self.bases[ctx]
11605 r = self.bases[ctx]
11608 def set(self, ctx, r):
11611 self.bases[ctx] = r
11613 self.bases[ctx] = r
11615 def insert(self, r):
11618 id = len(self.bases) + 3
11621 id = len(self.bases) + 3
11626_prop_closures = None
11629def ensure_prop_closures():
11630 global _prop_closures
11631 if _prop_closures is None:
11632 _prop_closures = PropClosures()
11635def user_prop_push(ctx, cb):
11636 prop = _prop_closures.get(ctx)
11641def user_prop_pop(ctx, cb, num_scopes):
11642 prop = _prop_closures.get(ctx)
11644 prop.pop(num_scopes)
11647def user_prop_fresh(ctx, _new_ctx):
11648 _prop_closures.set_threaded()
11649 prop = _prop_closures.get(ctx)
11651 Z3_del_context(nctx.ctx)
11652 new_ctx = to_ContextObj(_new_ctx)
11654 nctx.eh = Z3_set_error_handler(new_ctx, z3_error_handler)
11656 new_prop = prop.fresh(nctx)
11657 _prop_closures.set(new_prop.id, new_prop)
11661def user_prop_fixed(ctx, cb, id, value):
11662 prop = _prop_closures.get(ctx)
11665 id = _to_expr_ref(to_Ast(id), prop.ctx())
11666 value = _to_expr_ref(to_Ast(value), prop.ctx())
11667 prop.fixed(id, value)
11670def user_prop_created(ctx, cb, id):
11671 prop = _prop_closures.get(ctx)
11674 id = _to_expr_ref(to_Ast(id), prop.ctx())
11679def user_prop_final(ctx, cb):
11680 prop = _prop_closures.get(ctx)
11686def user_prop_eq(ctx, cb, x, y):
11687 prop = _prop_closures.get(ctx)
11690 x = _to_expr_ref(to_Ast(x), prop.ctx())
11691 y = _to_expr_ref(to_Ast(y), prop.ctx())
11695def user_prop_diseq(ctx, cb, x, y):
11696 prop = _prop_closures.get(ctx)
11699 x = _to_expr_ref(to_Ast(x), prop.ctx())
11700 y = _to_expr_ref(to_Ast(y), prop.ctx())
11704def user_prop_decide(ctx, cb, t_ref, idx, phase):
11705 prop = _prop_closures.get(ctx)
11708 t = _to_expr_ref(to_Ast(t_ref), prop.ctx())
11709 prop.decide(t, idx, phase)
11713_user_prop_push = Z3_push_eh(user_prop_push)
11714_user_prop_pop = Z3_pop_eh(user_prop_pop)
11715_user_prop_fresh = Z3_fresh_eh(user_prop_fresh)
11716_user_prop_fixed = Z3_fixed_eh(user_prop_fixed)
11717_user_prop_created = Z3_created_eh(user_prop_created)
11718_user_prop_final = Z3_final_eh(user_prop_final)
11719_user_prop_eq = Z3_eq_eh(user_prop_eq)
11720_user_prop_diseq = Z3_eq_eh(user_prop_diseq)
11721_user_prop_decide = Z3_decide_eh(user_prop_decide)
11724def PropagateFunction(name, *sig):
11725 """Create a function that gets tracked by user propagator.
11726 Every term headed by this function symbol is tracked.
11727 If a term is fixed and the fixed callback is registered a
11728 callback is invoked that the term headed by this function is fixed.
11730 sig = _get_args(sig)
11732 _z3_assert(len(sig) > 0, "At least two arguments expected")
11733 arity = len(sig) - 1
11736 _z3_assert(is_sort(rng), "Z3 sort expected")
11737 dom = (Sort * arity)()
11738 for i in range(arity):
11740 _z3_assert(is_sort(sig[i]), "Z3 sort expected")
11741 dom[i] = sig[i].ast
11743 return FuncDeclRef(Z3_solver_propagate_declare(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
11747class UserPropagateBase:
11750 # Either solver is set or ctx is set.
11751 # Propagators that are created through callbacks
11752 # to "fresh" inherit the context of that is supplied
11753 # as argument to the callback.
11754 # This context should not be deleted. It is owned by the solver.
11756 def __init__(self, s, ctx=None):
11757 assert s is None or ctx is None
11758 ensure_prop_closures()
11761 self.fresh_ctx = None
11763 self.id = _prop_closures.insert(self)
11769 self.created = None
11771 self.fresh_ctx = ctx
11773 Z3_solver_propagate_init(self.ctx_ref(),
11775 ctypes.c_void_p(self.id),
11782 self._ctx.ctx = None
11786 return self.fresh_ctx
11788 return self.solver.ctx
11791 return self.ctx().ref()
11793 def add_fixed(self, fixed):
11794 assert not self.fixed
11795 assert not self._ctx
11797 Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
11800 def add_created(self, created):
11801 assert not self.created
11802 assert not self._ctx
11804 Z3_solver_propagate_created(self.ctx_ref(), self.solver.solver, _user_prop_created)
11805 self.created = created
11807 def add_final(self, final):
11808 assert not self.final
11809 assert not self._ctx
11811 Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final)
11814 def add_eq(self, eq):
11816 assert not self._ctx
11818 Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq)
11821 def add_diseq(self, diseq):
11822 assert not self.diseq
11823 assert not self._ctx
11825 Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq)
11828 def add_decide(self, decide):
11829 assert not self.decide
11830 assert not self._ctx
11832 Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide)
11833 self.decide = decide
11836 raise Z3Exception("push needs to be overwritten")
11838 def pop(self, num_scopes):
11839 raise Z3Exception("pop needs to be overwritten")
11841 def fresh(self, new_ctx):
11842 raise Z3Exception("fresh needs to be overwritten")
11845 assert not self._ctx
11847 Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
11849 Z3_solver_propagate_register_cb(self.ctx_ref(), ctypes.c_void_p(self.cb), e.ast)
11852 # Tell the solver to perform the next split on a given term
11853 # If the term is a bit-vector the index idx specifies the index of the Boolean variable being
11854 # split on. A phase of true = 1/false = -1/undef = 0 = let solver decide is the last argument.
11856 def next_split(self, t, idx, phase):
11857 return Z3_solver_next_split(self.ctx_ref(), ctypes.c_void_p(self.cb), t.ast, idx, phase)
11860 # Propagation can only be invoked as during a fixed or final callback.
11862 def propagate(self, e, ids, eqs=[]):
11863 _ids, num_fixed = _to_ast_array(ids)
11865 _lhs, _num_lhs = _to_ast_array([x for x, y in eqs])
11866 _rhs, _num_rhs = _to_ast_array([y for x, y in eqs])
11867 return Z3_solver_propagate_consequence(e.ctx.ref(), ctypes.c_void_p(
11868 self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
11870 def conflict(self, deps = [], eqs = []):
11871 self.propagate(BoolVal(False, self.ctx()), deps, eqs)
approx(self, precision=10)
__rtruediv__(self, other)
__deepcopy__(self, memo={})
__init__(self, m=None, ctx=None)
__deepcopy__(self, memo={})
__init__(self, ast, ctx=None)
__deepcopy__(self, memo={})
translate(self, other_ctx)
__init__(self, v=None, ctx=None)
__rtruediv__(self, other)
__deepcopy__(self, memo={})
__init__(self, *args, **kws)
__deepcopy__(self, memo={})
__init__(self, name, ctx=None)
declare(self, name, *args)
declare_core(self, name, rec_name, *args)
__deepcopy__(self, memo={})
__init__(self, entry, ctx)
__deepcopy__(self, memo={})
translate(self, other_ctx)
__deepcopy__(self, memo={})
assert_exprs(self, *args)
dimacs(self, include_names=True)
simplify(self, *arguments, **keywords)
convert_model(self, model)
__init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None)
__deepcopy__(self, memo={})
eval(self, t, model_completion=False)
project_with_witness(self, vars, fml)
update_value(self, x, value)
evaluate(self, t, model_completion=False)
__deepcopy__(self, memo={})
__init__(self, descr, ctx=None)
get_documentation(self, n)
__deepcopy__(self, memo={})
__init__(self, ctx=None, params=None)
denominator_as_long(self)
Strings, Sequences and Regular expressions.
__init__(self, solver=None, ctx=None, logFile=None)
assert_and_track(self, a, p)
import_model_converter(self, other)
assert_exprs(self, *args)
check(self, *assumptions)
__exit__(self, *exc_info)
__deepcopy__(self, memo={})
__init__(self, stats, ctx)
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL,...
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
void Z3_API Z3_ast_map_inc_ref(Z3_context c, Z3_ast_map m)
Increment the reference counter of the given AST map.
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
Z3_ast Z3_API Z3_ast_map_find(Z3_context c, Z3_ast_map m, Z3_ast k)
Return the value associated with the key k.
Z3_string Z3_API Z3_ast_map_to_string(Z3_context c, Z3_ast_map m)
Convert the given map into a string.
Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p)
Convert a parameter description set into a string. This function is mainly used for printing the cont...
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the intersection of a list of sets.
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n)
Return the kind associated with the given parameter name n.
void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)
Define the body of a recursive function.
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value)
Create a fresh func_interp object, add it to a model for a specified function. It has reference count...
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a)
Update position i of the AST vector v with the AST a.
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k)
Return true if the map m contains the AST key k.
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
Z3_symbol Z3_API Z3_get_quantifier_skolem_id(Z3_context c, Z3_ast a)
Obtain skolem id of quantifier.
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal. The formula is split according to the following procedure that...
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)
Return the name of the parameter at given index i.
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_ast_vector Z3_API Z3_ast_map_keys(Z3_context c, Z3_ast_map m)
Return the keys stored in the given map.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m)
Convert a model of the formulas of a goal to a model of an original goal. The model may be null,...
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context....
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
void Z3_API Z3_enable_trace(Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.
Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i)
Return symbol of the i'th bound variable.
bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a unsigned integer.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array)
Access the array default value. Produces the default range value, for arrays that can be represented ...
unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m)
Return the number of uninterpreted sorts that m assigns an interpretation to.
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])
Create a constructor.
Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t)
Translate the AST vector v from context s into an AST vector in context t.
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target)
Copy a goal g from the context source to the context target.
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)
Convert AST vector into a string.
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a)
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a)
The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3....
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v)
Add a Boolean parameter k with value v to the parameter set p.
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read.
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i,...
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs)
n-ary Array read. The argument a is the array and idxs are the indices of the array that gets read.
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v)
Add a double parameter k with value v to the parameter set p.
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s)
Retrieve documentation string corresponding to parameter name s.
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)
create a forward reference to a recursive datatype being declared. The forward reference can be used ...
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a)
Return the function declaration f associated with a (_ as_array f) node.
Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the left t2 times.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.
Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i)
Return a uninterpreted sort that m assigns an interpretation.
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
Z3_sort Z3_API Z3_get_array_sort_domain_n(Z3_context c, Z3_sort t, unsigned idx)
Return the i'th domain sort of an n-dimensional array.
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.
Z3_ast Z3_API Z3_mk_quantifier_const_ex(Z3_context c, bool is_forall, unsigned weight, Z3_symbol quantifier_id, Z3_symbol skolem_id, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], unsigned num_no_patterns, Z3_ast const no_patterns[], Z3_ast body)
Create a universal or existential quantifier using a list of constants that will form the set of boun...
Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[])
Create a pattern for quantifier instantiation.
Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t)
Return the domain of the given array sort. In the case of a multi-dimensional array,...
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f)
Convert a Z3_func_decl into Z3_ast. This is just type casting.
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
unsigned Z3_API Z3_ast_map_size(Z3_context c, Z3_ast_map m)
Return the size of the given map.
unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p)
Return the number of parameters in the given parameter description set.
Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names)
Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF...
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th no_pattern.
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it.
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p)
Convert a Z3_pattern into Z3_ast. This is just type casting.
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f)
Return the arity (number of arguments) of the given function interpretation.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t)
Return the size of the given bit-vector sort.
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
void Z3_API Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m)
Decrement the reference counter of the given AST map.
Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...
Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c)
Retrieve description of global parameters.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target)
Translate/Copy the AST a from context source to context target. AST a must have been created using co...
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s)
Return the finite set of distinct values that represent the interpretation for sort s.
void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p)
Decrement the reference counter of the given parameter description set.
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.
Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t)
Return the range of the given array sort.
void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist)
Reclaim memory allocated for constructor list.
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a variable.
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v)
Increment the reference counter of the given AST vector.
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
Z3_ast Z3_API Z3_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k)
Create predicate that holds if Boolean array set has k elements set to true.
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
void Z3_API Z3_ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k)
Erase a key from the map.
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a)
Return a hash code for the given AST. The hash code is structural but two different AST objects can m...
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d)
Validate the parameter set p against the parameter description set d.
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.
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...
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
Z3_ast_map Z3_API Z3_mk_ast_map(Z3_context c)
Return an empty mapping from AST to AST.
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const *args)
Map f on the argument arrays.
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p)
Increment the reference counter of the given parameter description set.
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create array extensionality index given two arrays with the same sort. The meaning is given by the ax...
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s)
Convert a Z3_sort into Z3_ast. This is just type casting.
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function interpretation. It represents the value of f in a particular p...
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality....
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the sort value associated with a sort parameter.
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)
n-ary Array update.
Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i)
Return the sort of the i-th parameter of the given function declaration.
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i)
Return the AST at position i in the AST vector v.
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a)
Convert an AST into a FUNC_DECL_AST. This is just type casting.
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th pattern.
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
Z3_sort Z3_API Z3_mk_type_variable(Z3_context c, Z3_symbol s)
Create a type variable.
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a decimal string of a numeric constant term.
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)
add a function entry to a function interpretation.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a)
Return numeral value, as a binary string of a numeric constant term.
Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i)
Return sort of the i'th bound variable.
void Z3_API Z3_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
void Z3_API Z3_ast_map_insert(Z3_context c, Z3_ast_map m, Z3_ast k, Z3_ast v)
Store/Replace a new key, value pair in the given map.
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1)
Coerce a real to an integer.
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
Z3_symbol Z3_API Z3_get_quantifier_id(Z3_context c, Z3_ast a)
Obtain id of quantifier.
Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the right t2 times.
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places.
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a)
Return idx_a'th accessor for the idx_c'th constructor.
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
void Z3_API Z3_ast_map_reset(Z3_context c, Z3_ast_map m)
Remove all keys from the given map.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
BitVecVal(val, bv, ctx=None)
_coerce_exprs(a, b, ctx=None)
_ctx_from_ast_args(*args)
_to_func_decl_ref(a, ctx)
_valid_accessor(acc)
Datatypes.
BitVec(name, bv, ctx=None)
DeclareSort(name, ctx=None)
RecAddDefinition(f, args, body)
DeclareTypeVar(name, ctx=None)
_z3_check_cint_overflow(n, name)
TupleSort(name, sorts, ctx=None)
_coerce_expr_list(alist, ctx=None)
RealVector(prefix, sz, ctx=None)
BitVecs(names, bv, ctx=None)
BoolVector(prefix, sz, ctx=None)
FreshConst(sort, prefix="c")
EnumSort(name, values, ctx=None)
simplify(a, *arguments, **keywords)
Utils.
BV2Int(a, is_signed=False)
FreshInt(prefix="x", ctx=None)
_to_func_decl_array(args)
args2params(arguments, keywords, ctx=None)
Cond(p, t1, t2, ctx=None)
FreshReal(prefix="b", ctx=None)
_reduce(func, sequence, initial)
BVAddNoOverflow(a, b, signed)
FreshBool(prefix="b", ctx=None)
_ctx_from_ast_arg_list(args, default_ctx=None)
IntVector(prefix, sz, ctx=None)
RealVarVector(n, ctx=None)
DisjointSum(name, sorts, ctx=None)
Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
BVSubNoUnderflow(a, b, signed)
DatatypeSort(name, ctx=None)
BVMulNoOverflow(a, b, signed)
_mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])