11 """Z3 is a high performance theorem prover developed at Microsoft Research. Z3 is used in many applications such as: software/hardware verification and testing, constraint solving, analysis of hybrid systems, security, biology (in silico analysis), and geometrical problems. 13 Several online tutorials for Z3Py are available at: 14 http://rise4fun.com/Z3Py/tutorial/guide 16 Please send feedback, comments and/or corrections on the Issue tracker for https://github.com/Z3prover/z3.git. Your comments are very valuable. 37 ... x = BitVec('x', 32) 39 ... # the expression x + y is type incorrect 41 ... except Z3Exception as ex: 42 ... print("failed: %s" % ex) 47 from .z3types
import *
48 from .z3consts
import *
49 from .z3printer
import *
50 from fractions
import Fraction
58 return isinstance(v, (int, long))
61 return isinstance(v, int)
70 major = ctypes.c_uint(0)
71 minor = ctypes.c_uint(0)
72 build = ctypes.c_uint(0)
73 rev = ctypes.c_uint(0)
75 return "%s.%s.%s" % (major.value, minor.value, build.value)
78 major = ctypes.c_uint(0)
79 minor = ctypes.c_uint(0)
80 build = ctypes.c_uint(0)
81 rev = ctypes.c_uint(0)
83 return (major.value, minor.value, build.value, rev.value)
90 def _z3_assert(cond, msg):
92 raise Z3Exception(msg)
94 def _z3_check_cint_overflow(n, name):
95 _z3_assert(ctypes.c_int(n).value == n, name +
" is too large")
98 """Log interaction to a file. This function must be invoked immediately after init(). """ 102 """Append user-defined string to interaction log. """ 106 """Convert an integer or string into a Z3 symbol.""" 112 def _symbol2py(ctx, s):
113 """Convert a Z3 symbol back into a Python object. """ 124 if len(args) == 1
and (isinstance(args[0], tuple)
or isinstance(args[0], list)):
126 elif len(args) == 1
and (isinstance(args[0], set)
or isinstance(args[0], AstVector)):
127 return [arg
for arg
in args[0]]
134 def _get_args_ast_list(args):
136 if isinstance(args, set)
or isinstance(args, AstVector)
or isinstance(args, tuple):
137 return [arg
for arg
in args]
143 def _to_param_value(val):
144 if isinstance(val, bool):
158 """A Context manages all other Z3 objects, global configuration options, etc. 160 Z3Py uses a default global context. For most applications this is sufficient. 161 An application may use multiple Z3 contexts. Objects created in one context 162 cannot be used in another one. However, several objects may be "translated" from 163 one context to another. It is not safe to access Z3 objects from multiple threads. 164 The only exception is the method `interrupt()` that can be used to interrupt() a long 166 The initialization method receives global configuration options for the new context. 170 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
193 """Return a reference to the actual C pointer to the Z3 context.""" 197 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions. 199 This method can be invoked from a thread different from the one executing the 200 interruptible procedure. 208 """Return a reference to the global Z3 context. 211 >>> x.ctx == main_ctx() 216 >>> x2 = Real('x', c) 223 if _main_ctx
is None:
234 """Set Z3 global (or module) parameters. 236 >>> set_param(precision=10) 239 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
243 if not set_pp_option(k, v):
257 """Reset all global (or module) parameters. 262 """Alias for 'set_param' for backward compatibility. 267 """Return the value of a Z3 global (or module) parameter 269 >>> get_param('nlsat.reorder') 272 ptr = (ctypes.c_char_p * 1)()
274 r = z3core._to_pystr(ptr[0])
276 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
286 """Superclass for all Z3 objects that have support for pretty printing.""" 291 """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions.""" 298 if self.
ctx.ref()
is not None:
302 return _to_ast_ref(self.
ast, self.
ctx)
305 return obj_to_string(self)
308 return obj_to_string(self)
311 return self.
eq(other)
324 elif is_eq(self)
and self.num_args() == 2:
325 return self.arg(0).
eq(self.arg(1))
327 raise Z3Exception(
"Symbolic expressions cannot be cast to concrete Boolean values.")
330 """Return a string representing the AST node in s-expression notation. 333 >>> ((x + 1)*x).sexpr() 339 """Return a pointer to the corresponding C Z3_ast object.""" 343 """Return unique identifier for object. It can be used for hash-tables and maps.""" 347 """Return a reference to the C context where this AST node is stored.""" 348 return self.
ctx.ref()
351 """Return `True` if `self` and `other` are structurally identical. 358 >>> n1 = simplify(n1) 359 >>> n2 = simplify(n2) 364 _z3_assert(
is_ast(other),
"Z3 AST expected")
368 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 374 >>> # Nodes in different contexts can't be mixed. 375 >>> # However, we can translate nodes from one context to another. 376 >>> x.translate(c2) + y 380 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
387 """Return a hashcode for the `self`. 389 >>> n1 = simplify(Int('x') + 1) 390 >>> n2 = simplify(2 + Int('x') - 1) 391 >>> n1.hash() == n2.hash() 397 """Return `True` if `a` is an AST node. 401 >>> is_ast(IntVal(10)) 405 >>> is_ast(BoolSort()) 407 >>> is_ast(Function('f', IntSort(), IntSort())) 414 return isinstance(a, AstRef)
417 """Return `True` if `a` and `b` are structurally identical AST nodes. 427 >>> eq(simplify(x + 1), simplify(1 + x)) 434 def _ast_kind(ctx, a):
439 def _ctx_from_ast_arg_list(args, default_ctx=None):
447 _z3_assert(ctx == a.ctx,
"Context mismatch")
452 def _ctx_from_ast_args(*args):
453 return _ctx_from_ast_arg_list(args)
455 def _to_func_decl_array(args):
457 _args = (FuncDecl * sz)()
459 _args[i] = args[i].as_func_decl()
462 def _to_ast_array(args):
466 _args[i] = args[i].as_ast()
469 def _to_ref_array(ref, args):
473 _args[i] = args[i].as_ast()
476 def _to_ast_ref(a, ctx):
477 k = _ast_kind(ctx, a)
479 return _to_sort_ref(a, ctx)
480 elif k == Z3_FUNC_DECL_AST:
481 return _to_func_decl_ref(a, ctx)
483 return _to_expr_ref(a, ctx)
491 def _sort_kind(ctx, s):
495 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.""" 503 """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts. 506 >>> b.kind() == Z3_BOOL_SORT 508 >>> b.kind() == Z3_INT_SORT 510 >>> A = ArraySort(IntSort(), IntSort()) 511 >>> A.kind() == Z3_ARRAY_SORT 513 >>> A.kind() == Z3_INT_SORT 516 return _sort_kind(self.
ctx, self.
ast)
519 """Return `True` if `self` is a subsort of `other`. 521 >>> IntSort().subsort(RealSort()) 527 """Try to cast `val` as an element of sort `self`. 529 This method is used in Z3Py to convert Python objects such as integers, 530 floats, longs and strings into Z3 expressions. 533 >>> RealSort().cast(x) 537 _z3_assert(
is_expr(val),
"Z3 expression expected")
538 _z3_assert(self.
eq(val.sort()),
"Sort mismatch")
542 """Return the name (string) of sort `self`. 544 >>> BoolSort().name() 546 >>> ArraySort(IntSort(), IntSort()).name() 552 """Return `True` if `self` and `other` are the same Z3 sort. 555 >>> p.sort() == BoolSort() 557 >>> p.sort() == IntSort() 565 """Return `True` if `self` and `other` are not the same Z3 sort. 568 >>> p.sort() != BoolSort() 570 >>> p.sort() != IntSort() 577 return AstRef.__hash__(self)
580 """Return `True` if `s` is a Z3 sort. 582 >>> is_sort(IntSort()) 584 >>> is_sort(Int('x')) 586 >>> is_expr(Int('x')) 589 return isinstance(s, SortRef)
591 def _to_sort_ref(s, ctx):
593 _z3_assert(isinstance(s, Sort),
"Z3 Sort expected")
594 k = _sort_kind(ctx, s)
595 if k == Z3_BOOL_SORT:
597 elif k == Z3_INT_SORT
or k == Z3_REAL_SORT:
599 elif k == Z3_BV_SORT:
601 elif k == Z3_ARRAY_SORT:
603 elif k == Z3_DATATYPE_SORT:
605 elif k == Z3_FINITE_DOMAIN_SORT:
607 elif k == Z3_FLOATING_POINT_SORT:
609 elif k == Z3_ROUNDING_MODE_SORT:
614 return _to_sort_ref(
Z3_get_sort(ctx.ref(), a), ctx)
617 """Create a new uninterpreted sort named `name`. 619 If `ctx=None`, then the new sort is declared in the global Z3Py context. 621 >>> A = DeclareSort('A') 622 >>> a = Const('a', A) 623 >>> b = Const('b', A) 641 """Function declaration. Every constant and function have an associated declaration. 643 The declaration assigns a name, a sort (i.e., type), and for function 644 the sort (i.e., type) of each of its arguments. Note that, in Z3, 645 a constant is a function with 0 arguments. 657 """Return the name of the function declaration `self`. 659 >>> f = Function('f', IntSort(), IntSort()) 662 >>> isinstance(f.name(), str) 668 """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0. 670 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 677 """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`. 679 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 686 _z3_assert(i < self.
arity(),
"Index out of bounds")
690 """Return the sort of the range of a function declaration. For constants, this is the sort of the constant. 692 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 699 """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc. 702 >>> d = (x + 1).decl() 703 >>> d.kind() == Z3_OP_ADD 705 >>> d.kind() == Z3_OP_MUL 713 result = [
None for i
in range(n) ]
716 if k == Z3_PARAMETER_INT:
718 elif k == Z3_PARAMETER_DOUBLE:
720 elif k == Z3_PARAMETER_RATIONAL:
722 elif k == Z3_PARAMETER_SYMBOL:
724 elif k == Z3_PARAMETER_SORT:
726 elif k == Z3_PARAMETER_AST:
728 elif k == Z3_PARAMETER_FUNC_DECL:
735 """Create a Z3 application expression using the function `self`, and the given arguments. 737 The arguments must be Z3 expressions. This method assumes that 738 the sorts of the elements in `args` match the sorts of the 739 domain. Limited coercion is supported. For example, if 740 args[0] is a Python integer, and the function expects a Z3 741 integer, then the argument is automatically converted into a 744 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 752 args = _get_args(args)
755 _z3_assert(num == self.
arity(),
"Incorrect number of arguments to %s" % self)
756 _args = (Ast * num)()
761 tmp = self.
domain(i).cast(args[i])
763 _args[i] = tmp.as_ast()
767 """Return `True` if `a` is a Z3 function declaration. 769 >>> f = Function('f', IntSort(), IntSort()) 776 return isinstance(a, FuncDeclRef)
779 """Create a new Z3 uninterpreted function with the given sorts. 781 >>> f = Function('f', IntSort(), IntSort()) 787 _z3_assert(len(sig) > 0,
"At least two arguments expected")
791 _z3_assert(
is_sort(rng),
"Z3 sort expected")
792 dom = (Sort * arity)()
793 for i
in range(arity):
795 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
800 def _to_func_decl_ref(a, ctx):
804 """Create a new Z3 recursive with the given sorts.""" 807 _z3_assert(len(sig) > 0,
"At least two arguments expected")
811 _z3_assert(
is_sort(rng),
"Z3 sort expected")
812 dom = (Sort * arity)()
813 for i
in range(arity):
815 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
821 """Set the body of a recursive function. 822 Recursive definitions are only unfolded during search. 824 >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx)) 825 >>> n = Int('n', ctx) 826 >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1))) 829 >>> s = Solver(ctx=ctx) 830 >>> s.add(fac(n) < 3) 833 >>> s.model().eval(fac(5)) 839 args = _get_args(args)
843 _args[i] = args[i].ast
853 """Constraints, formulas and terms are expressions in Z3. 855 Expressions are ASTs. Every expression has a sort. 856 There are three main kinds of expressions: 857 function applications, quantifiers and bounded variables. 858 A constant is a function application with 0 arguments. 859 For quantifier free problems, all expressions are 860 function applications. 869 """Return the sort of expression `self`. 881 """Shorthand for `self.sort().kind()`. 883 >>> a = Array('a', IntSort(), IntSort()) 884 >>> a.sort_kind() == Z3_ARRAY_SORT 886 >>> a.sort_kind() == Z3_INT_SORT 889 return self.
sort().kind()
892 """Return a Z3 expression that represents the constraint `self == other`. 894 If `other` is `None`, then this method simply returns `False`. 905 a, b = _coerce_exprs(self, other)
910 return AstRef.__hash__(self)
913 """Return a Z3 expression that represents the constraint `self != other`. 915 If `other` is `None`, then this method simply returns `True`. 926 a, b = _coerce_exprs(self, other)
927 _args, sz = _to_ast_array((a, b))
934 """Return the Z3 function declaration associated with a Z3 application. 936 >>> f = Function('f', IntSort(), IntSort()) 945 _z3_assert(
is_app(self),
"Z3 application expected")
949 """Return the number of arguments of a Z3 application. 953 >>> (a + b).num_args() 955 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 961 _z3_assert(
is_app(self),
"Z3 application expected")
965 """Return argument `idx` of the application `self`. 967 This method assumes that `self` is a function application with at least `idx+1` arguments. 971 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 981 _z3_assert(
is_app(self),
"Z3 application expected")
982 _z3_assert(idx < self.
num_args(),
"Invalid argument index")
986 """Return a list containing the children of the given expression 990 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 1000 def _to_expr_ref(a, ctx):
1001 if isinstance(a, Pattern):
1005 if k == Z3_QUANTIFIER_AST:
1008 if sk == Z3_BOOL_SORT:
1010 if sk == Z3_INT_SORT:
1011 if k == Z3_NUMERAL_AST:
1014 if sk == Z3_REAL_SORT:
1015 if k == Z3_NUMERAL_AST:
1017 if _is_algebraic(ctx, a):
1020 if sk == Z3_BV_SORT:
1021 if k == Z3_NUMERAL_AST:
1025 if sk == Z3_ARRAY_SORT:
1027 if sk == Z3_DATATYPE_SORT:
1029 if sk == Z3_FLOATING_POINT_SORT:
1030 if k == Z3_APP_AST
and _is_numeral(ctx, a):
1033 return FPRef(a, ctx)
1034 if sk == Z3_FINITE_DOMAIN_SORT:
1035 if k == Z3_NUMERAL_AST:
1039 if sk == Z3_ROUNDING_MODE_SORT:
1041 if sk == Z3_SEQ_SORT:
1043 if sk == Z3_RE_SORT:
1044 return ReRef(a, ctx)
1047 def _coerce_expr_merge(s, a):
1060 _z3_assert(s1.ctx == s.ctx,
"context mismatch")
1061 _z3_assert(
False,
"sort mismatch")
1065 def _coerce_exprs(a, b, ctx=None):
1067 a = _py2expr(a, ctx)
1068 b = _py2expr(b, ctx)
1070 s = _coerce_expr_merge(s, a)
1071 s = _coerce_expr_merge(s, b)
1077 def _reduce(f, l, a):
1083 def _coerce_expr_list(alist, ctx=None):
1090 alist = [ _py2expr(a, ctx)
for a
in alist ]
1091 s = _reduce(_coerce_expr_merge, alist,
None)
1092 return [ s.cast(a)
for a
in alist ]
1095 """Return `True` if `a` is a Z3 expression. 1102 >>> is_expr(IntSort()) 1106 >>> is_expr(IntVal(1)) 1109 >>> is_expr(ForAll(x, x >= 0)) 1111 >>> is_expr(FPVal(1.0)) 1114 return isinstance(a, ExprRef)
1117 """Return `True` if `a` is a Z3 function application. 1119 Note that, constants are function applications with 0 arguments. 1126 >>> is_app(IntSort()) 1130 >>> is_app(IntVal(1)) 1133 >>> is_app(ForAll(x, x >= 0)) 1136 if not isinstance(a, ExprRef):
1138 k = _ast_kind(a.ctx, a)
1139 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
1142 """Return `True` if `a` is Z3 constant/variable expression. 1151 >>> is_const(IntVal(1)) 1154 >>> is_const(ForAll(x, x >= 0)) 1157 return is_app(a)
and a.num_args() == 0
1160 """Return `True` if `a` is variable. 1162 Z3 uses de-Bruijn indices for representing bound variables in 1170 >>> f = Function('f', IntSort(), IntSort()) 1171 >>> # Z3 replaces x with bound variables when ForAll is executed. 1172 >>> q = ForAll(x, f(x) == x) 1178 >>> is_var(b.arg(1)) 1181 return is_expr(a)
and _ast_kind(a.ctx, a) == Z3_VAR_AST
1184 """Return the de-Bruijn index of the Z3 bounded variable `a`. 1192 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1193 >>> # Z3 replaces x and y with bound variables when ForAll is executed. 1194 >>> q = ForAll([x, y], f(x, y) == x + y) 1196 f(Var(1), Var(0)) == Var(1) + Var(0) 1200 >>> v1 = b.arg(0).arg(0) 1201 >>> v2 = b.arg(0).arg(1) 1206 >>> get_var_index(v1) 1208 >>> get_var_index(v2) 1212 _z3_assert(
is_var(a),
"Z3 bound variable expected")
1216 """Return `True` if `a` is an application of the given kind `k`. 1220 >>> is_app_of(n, Z3_OP_ADD) 1222 >>> is_app_of(n, Z3_OP_MUL) 1225 return is_app(a)
and a.decl().kind() == k
1227 def If(a, b, c, ctx=None):
1228 """Create a Z3 if-then-else expression. 1232 >>> max = If(x > y, x, y) 1238 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1239 return Cond(a, b, c, ctx)
1241 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1244 b, c = _coerce_exprs(b, c, ctx)
1246 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1247 return _to_expr_ref(
Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1250 """Create a Z3 distinct expression. 1257 >>> Distinct(x, y, z) 1259 >>> simplify(Distinct(x, y, z)) 1261 >>> simplify(Distinct(x, y, z), blast_distinct=True) 1262 And(Not(x == y), Not(x == z), Not(y == z)) 1264 args = _get_args(args)
1265 ctx = _ctx_from_ast_arg_list(args)
1267 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1268 args = _coerce_expr_list(args, ctx)
1269 _args, sz = _to_ast_array(args)
1272 def _mk_bin(f, a, b):
1275 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1276 args[0] = a.as_ast()
1277 args[1] = b.as_ast()
1278 return f(a.ctx.ref(), 2, args)
1281 """Create a constant of the given sort. 1283 >>> Const('x', IntSort()) 1287 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
1292 """Create a several constants of the given sort. 1294 `names` is a string containing the names of all constants to be created. 1295 Blank spaces separate the names of different constants. 1297 >>> x, y, z = Consts('x y z', IntSort()) 1301 if isinstance(names, str):
1302 names = names.split(
" ")
1303 return [
Const(name, sort)
for name
in names]
1306 """Create a fresh constant of a specified sort""" 1307 ctx = _get_ctx(sort.ctx)
1311 """Create a Z3 free variable. Free variables are used to create quantified formulas. 1313 >>> Var(0, IntSort()) 1315 >>> eq(Var(0, IntSort()), Var(0, BoolSort())) 1319 _z3_assert(
is_sort(s),
"Z3 sort expected")
1320 return _to_expr_ref(
Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1324 Create a real free variable. Free variables are used to create quantified formulas. 1325 They are also used to create polynomials. 1334 Create a list of Real free variables. 1335 The variables have ids: 0, 1, ..., n-1 1337 >>> x0, x1, x2, x3 = RealVarVector(4) 1352 """Try to cast `val` as a Boolean. 1354 >>> x = BoolSort().cast(True) 1364 if isinstance(val, bool):
1368 _z3_assert(
is_expr(val),
"True, False or Z3 Boolean expression expected. Received %s" % val)
1369 if not self.
eq(val.sort()):
1370 _z3_assert(self.
eq(val.sort()),
"Value cannot be converted into a Z3 Boolean value")
1374 return isinstance(other, ArithSortRef)
1384 """All Boolean expressions are instances of this class.""" 1392 """Create the Z3 expression `self * other`. 1398 return If(self, other, 0)
1402 """Return `True` if `a` is a Z3 Boolean expression. 1408 >>> is_bool(And(p, q)) 1416 return isinstance(a, BoolRef)
1419 """Return `True` if `a` is the Z3 true expression. 1424 >>> is_true(simplify(p == p)) 1429 >>> # True is a Python Boolean expression 1436 """Return `True` if `a` is the Z3 false expression. 1443 >>> is_false(BoolVal(False)) 1449 """Return `True` if `a` is a Z3 and expression. 1451 >>> p, q = Bools('p q') 1452 >>> is_and(And(p, q)) 1454 >>> is_and(Or(p, q)) 1460 """Return `True` if `a` is a Z3 or expression. 1462 >>> p, q = Bools('p q') 1465 >>> is_or(And(p, q)) 1471 """Return `True` if `a` is a Z3 implication expression. 1473 >>> p, q = Bools('p q') 1474 >>> is_implies(Implies(p, q)) 1476 >>> is_implies(And(p, q)) 1482 """Return `True` if `a` is a Z3 not expression. 1493 """Return `True` if `a` is a Z3 equality expression. 1495 >>> x, y = Ints('x y') 1502 """Return `True` if `a` is a Z3 distinct expression. 1504 >>> x, y, z = Ints('x y z') 1505 >>> is_distinct(x == y) 1507 >>> is_distinct(Distinct(x, y, z)) 1513 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. 1517 >>> p = Const('p', BoolSort()) 1520 >>> r = Function('r', IntSort(), IntSort(), BoolSort()) 1527 return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx) 1529 def BoolVal(val, ctx=None): 1530 """Return the Boolean value `
True`
or `
False`. If `ctx=
None`, then the
global context
is used.
1543 return BoolRef(Z3_mk_false(ctx.ref()), ctx) 1545 return BoolRef(Z3_mk_true(ctx.ref()), ctx) 1547 def Bool(name, ctx=None): 1548 """Return a Boolean constant named `name`. If `ctx=
None`, then the
global context
is used.
1556 return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx) 1558 def Bools(names, ctx=None): 1559 """Return a tuple of Boolean constants.
1561 `names`
is a single string containing all names separated by blank spaces.
1562 If `ctx=
None`, then the
global context
is used.
1564 >>> p, q, r =
Bools(
'p q r')
1565 >>>
And(p,
Or(q, r))
1569 if isinstance(names, str): 1570 names = names.split(" ") 1571 return [Bool(name, ctx) for name in names] 1573 def BoolVector(prefix, sz, ctx=None): 1574 """Return a list of Boolean constants of size `sz`.
1576 The constants are named using the given prefix.
1577 If `ctx=
None`, then the
global context
is used.
1583 And(p__0, p__1, p__2)
1585 return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ] 1587 def FreshBool(prefix='b', ctx=None): 1588 """Return a fresh Boolean constant
in the given context using the given prefix.
1590 If `ctx=
None`, then the
global context
is used.
1598 return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx) 1600 def Implies(a, b, ctx=None): 1601 """Create a Z3 implies expression.
1603 >>> p, q =
Bools(
'p q')
1609 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 1613 return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 1615 def Xor(a, b, ctx=None): 1616 """Create a Z3 Xor expression.
1618 >>> p, q =
Bools(
'p q')
1624 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 1628 return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 1630 def Not(a, ctx=None): 1631 """Create a Z3
not expression
or probe.
1639 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) 1641 # Not is also used to build probes 1642 return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx) 1646 return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx) 1648 def _has_probe(args): 1649 """Return `
True`
if one of the elements of the given collection
is a Z3 probe.
""" 1656 """Create a Z3
and-expression
or and-probe.
1658 >>> p, q, r =
Bools(
'p q r')
1663 And(p__0, p__1, p__2, p__3, p__4)
1667 last_arg = args[len(args)-1] 1668 if isinstance(last_arg, Context): 1669 ctx = args[len(args)-1] 1670 args = args[:len(args)-1] 1671 elif len(args) == 1 and isinstance(args[0], AstVector): 1673 args = [a for a in args[0]] 1676 args = _get_args(args) 1677 ctx_args = _ctx_from_ast_arg_list(args, ctx) 1679 _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") 1680 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") 1681 if _has_probe(args): 1682 return _probe_and(args, ctx) 1684 args = _coerce_expr_list(args, ctx) 1685 _args, sz = _to_ast_array(args) 1686 return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx) 1689 """Create a Z3
or-expression
or or-probe.
1691 >>> p, q, r =
Bools(
'p q r')
1696 Or(p__0, p__1, p__2, p__3, p__4)
1700 last_arg = args[len(args)-1] 1701 if isinstance(last_arg, Context): 1702 ctx = args[len(args)-1] 1703 args = args[:len(args)-1] 1706 args = _get_args(args) 1707 ctx_args = _ctx_from_ast_arg_list(args, ctx) 1709 _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") 1710 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") 1711 if _has_probe(args): 1712 return _probe_or(args, ctx) 1714 args = _coerce_expr_list(args, ctx) 1715 _args, sz = _to_ast_array(args) 1716 return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx) 1718 ######################################### 1722 ######################################### 1724 class PatternRef(ExprRef): 1725 """Patterns are hints
for quantifier instantiation.
1729 return Z3_pattern_to_ast(self.ctx_ref(), self.ast) 1732 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1735 """Return `
True`
if `a`
is a Z3 pattern (hint
for quantifier instantiation.
1739 >>> q =
ForAll(x, f(x) == 0, patterns = [ f(x) ])
1742 >>> q.num_patterns()
1749 return isinstance(a, PatternRef) 1751 def MultiPattern(*args): 1752 """Create a Z3 multi-pattern using the given expressions `*args`
1760 >>> q.num_patterns()
1768 _z3_assert(len(args) > 0, "At least one argument expected") 1769 _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected") 1771 args, sz = _to_ast_array(args) 1772 return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx) 1774 def _to_pattern(arg): 1778 return MultiPattern(arg) 1780 ######################################### 1784 ######################################### 1786 class QuantifierRef(BoolRef): 1787 """Universally
and Existentially quantified formulas.
""" 1793 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1796 """Return the Boolean sort
or sort of Lambda.
""" 1797 if self.is_lambda(): 1798 return _sort(self.ctx, self.as_ast()) 1799 return BoolSort(self.ctx) 1801 def is_forall(self): 1802 """Return `
True`
if `self`
is a universal quantifier.
1806 >>> q =
ForAll(x, f(x) == 0)
1809 >>> q =
Exists(x, f(x) != 0)
1813 return Z3_is_quantifier_forall(self.ctx_ref(), self.ast) 1815 def is_exists(self): 1816 """Return `
True`
if `self`
is an existential quantifier.
1820 >>> q =
ForAll(x, f(x) == 0)
1823 >>> q =
Exists(x, f(x) != 0)
1827 return Z3_is_quantifier_exists(self.ctx_ref(), self.ast) 1829 def is_lambda(self): 1830 """Return `
True`
if `self`
is a
lambda expression.
1837 >>> q =
Exists(x, f(x) != 0)
1841 return Z3_is_lambda(self.ctx_ref(), self.ast) 1844 """Return the weight annotation of `self`.
1848 >>> q =
ForAll(x, f(x) == 0)
1851 >>> q =
ForAll(x, f(x) == 0, weight=10)
1855 return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast)) 1857 def num_patterns(self): 1858 """Return the number of patterns (i.e., quantifier instantiation hints)
in `self`.
1863 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1864 >>> q.num_patterns()
1867 return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast)) 1869 def pattern(self, idx): 1870 """Return a pattern (i.e., quantifier instantiation hints)
in `self`.
1875 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1876 >>> q.num_patterns()
1884 _z3_assert(idx < self.num_patterns(), "Invalid pattern idx") 1885 return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1887 def num_no_patterns(self): 1888 """Return the number of no-patterns.
""" 1889 return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast) 1891 def no_pattern(self, idx): 1892 """Return a no-pattern.
""" 1894 _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx") 1895 return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1898 """Return the expression being quantified.
1902 >>> q =
ForAll(x, f(x) == 0)
1906 return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx) 1909 """Return the number of variables bounded by this quantifier.
1914 >>> q =
ForAll([x, y], f(x, y) >= x)
1918 return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast)) 1920 def var_name(self, idx): 1921 """Return a string representing a name used when displaying the quantifier.
1926 >>> q =
ForAll([x, y], f(x, y) >= x)
1933 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1934 return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx)) 1936 def var_sort(self, idx): 1937 """Return the sort of a bound variable.
1942 >>> q =
ForAll([x, y], f(x, y) >= x)
1949 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1950 return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx) 1953 """Return a list containing a single element self.
body()
1957 >>> q =
ForAll(x, f(x) == 0)
1961 return [ self.body() ] 1963 def is_quantifier(a): 1964 """Return `
True`
if `a`
is a Z3 quantifier.
1968 >>> q =
ForAll(x, f(x) == 0)
1974 return isinstance(a, QuantifierRef) 1976 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 1978 _z3_assert(is_bool(body) or is_app(vs) or (len(vs) > 0 and is_app(vs[0])), "Z3 expression expected") 1979 _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)") 1980 _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected") 1981 _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions") 1987 if not is_expr(body): 1988 body = BoolVal(body, ctx) 1992 _vs = (Ast * num_vars)() 1993 for i in range(num_vars): 1994 ## TODO: Check if is constant 1995 _vs[i] = vs[i].as_ast() 1996 patterns = [ _to_pattern(p) for p in patterns ] 1997 num_pats = len(patterns) 1998 _pats = (Pattern * num_pats)() 1999 for i in range(num_pats): 2000 _pats[i] = patterns[i].ast 2001 _no_pats, num_no_pats = _to_ast_array(no_patterns) 2002 qid = to_symbol(qid, ctx) 2003 skid = to_symbol(skid, ctx) 2004 return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid, 2007 num_no_pats, _no_pats, 2008 body.as_ast()), ctx) 2010 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 2011 """Create a Z3 forall formula.
2013 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
2018 >>>
ForAll([x, y], f(x, y) >= x)
2019 ForAll([x, y], f(x, y) >= x)
2020 >>>
ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2021 ForAll([x, y], f(x, y) >= x)
2022 >>>
ForAll([x, y], f(x, y) >= x, weight=10)
2023 ForAll([x, y], f(x, y) >= x)
2025 return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns) 2027 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 2028 """Create a Z3 exists formula.
2030 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
2036 >>> q =
Exists([x, y], f(x, y) >= x, skid=
"foo")
2038 Exists([x, y], f(x, y) >= x)
2041 >>> r =
Tactic(
'nnf')(q).as_expr()
2045 return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns) 2047 def Lambda(vs, body): 2048 """Create a Z3
lambda expression.
2052 >>> lo, hi, e, i =
Ints(
'lo hi e i')
2053 >>> mem1 =
Lambda([i],
If(
And(lo <= i, i <= hi), e, mem0[i]))
2061 _vs = (Ast * num_vars)() 2062 for i in range(num_vars): 2063 ## TODO: Check if is constant 2064 _vs[i] = vs[i].as_ast() 2065 return QuantifierRef(Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx) 2067 ######################################### 2071 ######################################### 2073 class ArithSortRef(SortRef): 2074 """Real
and Integer sorts.
""" 2077 """Return `
True`
if `self`
is of the sort Real.
2088 return self.kind() == Z3_REAL_SORT 2091 """Return `
True`
if `self`
is of the sort Integer.
2102 return self.kind() == Z3_INT_SORT 2104 def subsort(self, other): 2105 """Return `
True`
if `self`
is a subsort of `other`.
""" 2106 return self.is_int() and is_arith_sort(other) and other.is_real() 2108 def cast(self, val): 2109 """Try to cast `val`
as an Integer
or Real.
2124 _z3_assert(self.ctx == val.ctx, "Context mismatch") 2128 if val_s.is_int() and self.is_real(): 2130 if val_s.is_bool() and self.is_int(): 2131 return If(val, 1, 0) 2132 if val_s.is_bool() and self.is_real(): 2133 return ToReal(If(val, 1, 0)) 2135 _z3_assert(False, "Z3 Integer/Real expression expected" ) 2138 return IntVal(val, self.ctx) 2140 return RealVal(val, self.ctx) 2142 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self) 2144 def is_arith_sort(s): 2145 """Return `
True`
if s
is an arithmetical sort (type).
2153 >>> n =
Int(
'x') + 1
2157 return isinstance(s, ArithSortRef) 2159 class ArithRef(ExprRef): 2160 """Integer
and Real expressions.
""" 2163 """Return the sort (type) of the arithmetical expression `self`.
2170 return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 2173 """Return `
True`
if `self`
is an integer expression.
2184 return self.sort().is_int() 2187 """Return `
True`
if `self`
is an real expression.
2195 return self.sort().is_real() 2197 def __add__(self, other): 2198 """Create the Z3 expression `self + other`.
2207 a, b = _coerce_exprs(self, other) 2208 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx) 2210 def __radd__(self, other): 2211 """Create the Z3 expression `other + self`.
2217 a, b = _coerce_exprs(self, other) 2218 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx) 2220 def __mul__(self, other): 2221 """Create the Z3 expression `self * other`.
2230 if isinstance(other, BoolRef): 2231 return If(other, self, 0) 2232 a, b = _coerce_exprs(self, other) 2233 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx) 2235 def __rmul__(self, other): 2236 """Create the Z3 expression `other * self`.
2242 a, b = _coerce_exprs(self, other) 2243 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx) 2245 def __sub__(self, other): 2246 """Create the Z3 expression `self - other`.
2255 a, b = _coerce_exprs(self, other) 2256 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx) 2258 def __rsub__(self, other): 2259 """Create the Z3 expression `other - self`.
2265 a, b = _coerce_exprs(self, other) 2266 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx) 2268 def __pow__(self, other): 2269 """Create the Z3 expression `self**other` (**
is the power operator).
2279 a, b = _coerce_exprs(self, other) 2280 return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2282 def __rpow__(self, other): 2283 """Create the Z3 expression `other**self` (**
is the power operator).
2293 a, b = _coerce_exprs(self, other) 2294 return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2296 def __div__(self, other): 2297 """Create the Z3 expression `other/self`.
2316 a, b = _coerce_exprs(self, other) 2317 return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2319 def __truediv__(self, other): 2320 """Create the Z3 expression `other/self`.
""" 2321 return self.__div__(other) 2323 def __rdiv__(self, other): 2324 """Create the Z3 expression `other/self`.
2337 a, b = _coerce_exprs(self, other) 2338 return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2340 def __rtruediv__(self, other): 2341 """Create the Z3 expression `other/self`.
""" 2342 return self.__rdiv__(other) 2344 def __mod__(self, other): 2345 """Create the Z3 expression `other%self`.
2354 a, b = _coerce_exprs(self, other) 2356 _z3_assert(a.is_int(), "Z3 integer expression expected") 2357 return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2359 def __rmod__(self, other): 2360 """Create the Z3 expression `other%self`.
2366 a, b = _coerce_exprs(self, other) 2368 _z3_assert(a.is_int(), "Z3 integer expression expected") 2369 return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2372 """Return an expression representing `-self`.
2380 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx) 2391 def __le__(self, other): 2392 """Create the Z3 expression `other <= self`.
2394 >>> x, y =
Ints(
'x y')
2401 a, b = _coerce_exprs(self, other) 2402 return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2404 def __lt__(self, other): 2405 """Create the Z3 expression `other < self`.
2407 >>> x, y =
Ints(
'x y')
2414 a, b = _coerce_exprs(self, other) 2415 return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2417 def __gt__(self, other): 2418 """Create the Z3 expression `other > self`.
2420 >>> x, y =
Ints(
'x y')
2427 a, b = _coerce_exprs(self, other) 2428 return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2430 def __ge__(self, other): 2431 """Create the Z3 expression `other >= self`.
2433 >>> x, y =
Ints(
'x y')
2440 a, b = _coerce_exprs(self, other) 2441 return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2444 """Return `
True`
if `a`
is an arithmetical expression.
2461 return isinstance(a, ArithRef) 2464 """Return `
True`
if `a`
is an integer expression.
2479 return is_arith(a) and a.is_int() 2482 """Return `
True`
if `a`
is a real expression.
2497 return is_arith(a) and a.is_real() 2499 def _is_numeral(ctx, a): 2500 return Z3_is_numeral_ast(ctx.ref(), a) 2502 def _is_algebraic(ctx, a): 2503 return Z3_is_algebraic_number(ctx.ref(), a) 2505 def is_int_value(a): 2506 """Return `
True`
if `a`
is an integer value of sort Int.
2514 >>> n =
Int(
'x') + 1
2526 return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast()) 2528 def is_rational_value(a): 2529 """Return `
True`
if `a`
is rational value of sort Real.
2539 >>> n =
Real(
'x') + 1
2547 return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast()) 2549 def is_algebraic_value(a): 2550 """Return `
True`
if `a`
is an algebraic value of sort Real.
2560 return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast()) 2563 """Return `
True`
if `a`
is an expression of the form b + c.
2565 >>> x, y =
Ints(
'x y')
2571 return is_app_of(a, Z3_OP_ADD) 2574 """Return `
True`
if `a`
is an expression of the form b * c.
2576 >>> x, y =
Ints(
'x y')
2582 return is_app_of(a, Z3_OP_MUL) 2585 """Return `
True`
if `a`
is an expression of the form b - c.
2587 >>> x, y =
Ints(
'x y')
2593 return is_app_of(a, Z3_OP_SUB) 2596 """Return `
True`
if `a`
is an expression of the form b / c.
2598 >>> x, y =
Reals(
'x y')
2603 >>> x, y =
Ints(
'x y')
2609 return is_app_of(a, Z3_OP_DIV) 2612 """Return `
True`
if `a`
is an expression of the form b div c.
2614 >>> x, y =
Ints(
'x y')
2620 return is_app_of(a, Z3_OP_IDIV) 2623 """Return `
True`
if `a`
is an expression of the form b % c.
2625 >>> x, y =
Ints(
'x y')
2631 return is_app_of(a, Z3_OP_MOD) 2634 """Return `
True`
if `a`
is an expression of the form b <= c.
2636 >>> x, y =
Ints(
'x y')
2642 return is_app_of(a, Z3_OP_LE) 2645 """Return `
True`
if `a`
is an expression of the form b < c.
2647 >>> x, y =
Ints(
'x y')
2653 return is_app_of(a, Z3_OP_LT) 2656 """Return `
True`
if `a`
is an expression of the form b >= c.
2658 >>> x, y =
Ints(
'x y')
2664 return is_app_of(a, Z3_OP_GE) 2667 """Return `
True`
if `a`
is an expression of the form b > c.
2669 >>> x, y =
Ints(
'x y')
2675 return is_app_of(a, Z3_OP_GT) 2678 """Return `
True`
if `a`
is an expression of the form
IsInt(b).
2686 return is_app_of(a, Z3_OP_IS_INT) 2689 """Return `
True`
if `a`
is an expression of the form
ToReal(b).
2700 return is_app_of(a, Z3_OP_TO_REAL) 2703 """Return `
True`
if `a`
is an expression of the form
ToInt(b).
2714 return is_app_of(a, Z3_OP_TO_INT) 2716 class IntNumRef(ArithRef): 2717 """Integer values.
""" 2720 """Return a Z3 integer numeral
as a Python long (bignum) numeral.
2729 _z3_assert(self.is_int(), "Integer value expected") 2730 return int(self.as_string()) 2732 def as_string(self): 2733 """Return a Z3 integer numeral
as a Python string.
2738 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2740 class RatNumRef(ArithRef): 2741 """Rational values.
""" 2743 def numerator(self): 2744 """ Return the numerator of a Z3 rational numeral.
2756 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx) 2758 def denominator(self): 2759 """ Return the denominator of a Z3 rational numeral.
2767 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx) 2769 def numerator_as_long(self): 2770 """ Return the numerator
as a Python long.
2777 >>> v.numerator_as_long() + 1 == 10000000001
2780 return self.numerator().as_long() 2782 def denominator_as_long(self): 2783 """ Return the denominator
as a Python long.
2788 >>> v.denominator_as_long()
2791 return self.denominator().as_long() 2799 def is_int_value(self): 2800 return self.denominator().is_int() and self.denominator_as_long() == 1 2803 _z3_assert(self.is_int(), "Expected integer fraction") 2804 return self.numerator_as_long() 2806 def as_decimal(self, prec): 2807 """ Return a Z3 rational value
as a string
in decimal notation using at most `prec` decimal places.
2816 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2818 def as_string(self): 2819 """Return a Z3 rational numeral
as a Python string.
2825 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2827 def as_fraction(self): 2828 """Return a Z3 rational
as a Python Fraction object.
2834 return Fraction(self.numerator_as_long(), self.denominator_as_long()) 2836 class AlgebraicNumRef(ArithRef): 2837 """Algebraic irrational values.
""" 2839 def approx(self, precision=10): 2840 """Return a Z3 rational number that approximates the algebraic number `self`.
2841 The result `r`
is such that |r - self| <= 1/10^precision
2845 6838717160008073720548335/4835703278458516698824704
2849 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx) 2850 def as_decimal(self, prec): 2851 """Return a string representation of the algebraic number `self`
in decimal notation using `prec` decimal places
2854 >>> x.as_decimal(10)
2856 >>> x.as_decimal(20)
2857 '1.41421356237309504880?' 2859 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2861 def _py2expr(a, ctx=None): 2862 if isinstance(a, bool): 2863 return BoolVal(a, ctx) 2865 return IntVal(a, ctx) 2866 if isinstance(a, float): 2867 return RealVal(a, ctx) 2871 _z3_assert(False, "Python bool, int, long or float expected") 2873 def IntSort(ctx=None): 2874 """Return the integer sort
in the given context. If `ctx=
None`, then the
global context
is used.
2887 return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx) 2889 def RealSort(ctx=None): 2890 """Return the real sort
in the given context. If `ctx=
None`, then the
global context
is used.
2903 return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx) 2905 def _to_int_str(val): 2906 if isinstance(val, float): 2907 return str(int(val)) 2908 elif isinstance(val, bool): 2915 elif isinstance(val, str): 2918 _z3_assert(False, "Python value cannot be used as a Z3 integer") 2920 def IntVal(val, ctx=None): 2921 """Return a Z3 integer value. If `ctx=
None`, then the
global context
is used.
2929 return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx) 2931 def RealVal(val, ctx=None): 2932 """Return a Z3 real value.
2934 `val` may be a Python int, long, float
or string representing a number
in decimal
or rational notation.
2935 If `ctx=
None`, then the
global context
is used.
2947 return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx) 2949 def RatVal(a, b, ctx=None): 2950 """Return a Z3 rational a/b.
2952 If `ctx=
None`, then the
global context
is used.
2960 _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer") 2961 _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer") 2962 return simplify(RealVal(a, ctx)/RealVal(b, ctx)) 2964 def Q(a, b, ctx=None): 2965 """Return a Z3 rational a/b.
2967 If `ctx=
None`, then the
global context
is used.
2974 return simplify(RatVal(a, b)) 2976 def Int(name, ctx=None): 2977 """Return an integer constant named `name`. If `ctx=
None`, then the
global context
is used.
2986 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx) 2988 def Ints(names, ctx=None): 2989 """Return a tuple of Integer constants.
2991 >>> x, y, z =
Ints(
'x y z')
2996 if isinstance(names, str): 2997 names = names.split(" ") 2998 return [Int(name, ctx) for name in names] 3000 def IntVector(prefix, sz, ctx=None): 3001 """Return a list of integer constants of size `sz`.
3009 return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ] 3011 def FreshInt(prefix='x', ctx=None): 3012 """Return a fresh integer constant
in the given context using the given prefix.
3022 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx) 3024 def Real(name, ctx=None): 3025 """Return a real constant named `name`. If `ctx=
None`, then the
global context
is used.
3034 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx) 3036 def Reals(names, ctx=None): 3037 """Return a tuple of real constants.
3039 >>> x, y, z =
Reals(
'x y z')
3042 >>>
Sum(x, y, z).sort()
3046 if isinstance(names, str): 3047 names = names.split(" ") 3048 return [Real(name, ctx) for name in names] 3050 def RealVector(prefix, sz, ctx=None): 3051 """Return a list of real constants of size `sz`.
3061 return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ] 3063 def FreshReal(prefix='b', ctx=None): 3064 """Return a fresh real constant
in the given context using the given prefix.
3074 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx) 3077 """ Return the Z3 expression
ToReal(a).
3089 _z3_assert(a.is_int(), "Z3 integer expression expected.") 3091 return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx) 3094 """ Return the Z3 expression
ToInt(a).
3106 _z3_assert(a.is_real(), "Z3 real expression expected.") 3108 return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx) 3111 """ Return the Z3 predicate
IsInt(a).
3114 >>>
IsInt(x +
"1/2")
3118 >>>
solve(
IsInt(x +
"1/2"), x > 0, x < 1, x !=
"1/2")
3122 _z3_assert(a.is_real(), "Z3 real expression expected.") 3124 return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx) 3126 def Sqrt(a, ctx=None): 3127 """ Return a Z3 expression which represents the square root of a.
3138 def Cbrt(a, ctx=None): 3139 """ Return a Z3 expression which represents the cubic root of a.
3150 ######################################### 3154 ######################################### 3156 class BitVecSortRef(SortRef): 3157 """Bit-vector sort.
""" 3160 """Return the size (number of bits) of the bit-vector sort `self`.
3166 return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast)) 3168 def subsort(self, other): 3169 return is_bv_sort(other) and self.size() < other.size() 3171 def cast(self, val): 3172 """Try to cast `val`
as a Bit-Vector.
3177 >>> b.cast(10).
sexpr()
3182 _z3_assert(self.ctx == val.ctx, "Context mismatch") 3183 # Idea: use sign_extend if sort of val is a bitvector of smaller size 3186 return BitVecVal(val, self) 3189 """Return
True if `s`
is a Z3 bit-vector sort.
3196 return isinstance(s, BitVecSortRef) 3198 class BitVecRef(ExprRef): 3199 """Bit-vector expressions.
""" 3202 """Return the sort of the bit-vector expression `self`.
3210 return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 3213 """Return the number of bits of the bit-vector expression `self`.
3221 return self.sort().size() 3223 def __add__(self, other): 3224 """Create the Z3 expression `self + other`.
3233 a, b = _coerce_exprs(self, other) 3234 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3236 def __radd__(self, other): 3237 """Create the Z3 expression `other + self`.
3243 a, b = _coerce_exprs(self, other) 3244 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3246 def __mul__(self, other): 3247 """Create the Z3 expression `self * other`.
3256 a, b = _coerce_exprs(self, other) 3257 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3259 def __rmul__(self, other): 3260 """Create the Z3 expression `other * self`.
3266 a, b = _coerce_exprs(self, other) 3267 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3269 def __sub__(self, other): 3270 """Create the Z3 expression `self - other`.
3279 a, b = _coerce_exprs(self, other) 3280 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3282 def __rsub__(self, other): 3283 """Create the Z3 expression `other - self`.
3289 a, b = _coerce_exprs(self, other) 3290 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3292 def __or__(self, other): 3293 """Create the Z3 expression bitwise-
or `self | other`.
3302 a, b = _coerce_exprs(self, other) 3303 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3305 def __ror__(self, other): 3306 """Create the Z3 expression bitwise-
or `other | self`.
3312 a, b = _coerce_exprs(self, other) 3313 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3315 def __and__(self, other): 3316 """Create the Z3 expression bitwise-
and `self & other`.
3325 a, b = _coerce_exprs(self, other) 3326 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3328 def __rand__(self, other): 3329 """Create the Z3 expression bitwise-
or `other & self`.
3335 a, b = _coerce_exprs(self, other) 3336 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3338 def __xor__(self, other): 3339 """Create the Z3 expression bitwise-xor `self ^ other`.
3348 a, b = _coerce_exprs(self, other) 3349 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3351 def __rxor__(self, other): 3352 """Create the Z3 expression bitwise-xor `other ^ self`.
3358 a, b = _coerce_exprs(self, other) 3359 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3371 """Return an expression representing `-self`.
3379 return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx) 3381 def __invert__(self): 3382 """Create the Z3 expression bitwise-
not `~self`.
3390 return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx) 3392 def __div__(self, other): 3393 """Create the Z3 expression (signed) division `self / other`.
3395 Use the function
UDiv()
for unsigned division.
3408 a, b = _coerce_exprs(self, other) 3409 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3411 def __truediv__(self, other): 3412 """Create the Z3 expression (signed) division `self / other`.
""" 3413 return self.__div__(other) 3415 def __rdiv__(self, other): 3416 """Create the Z3 expression (signed) division `other / self`.
3418 Use the function
UDiv()
for unsigned division.
3423 >>> (10 / x).
sexpr()
3424 '(bvsdiv #x0000000a x)' 3426 '(bvudiv #x0000000a x)' 3428 a, b = _coerce_exprs(self, other) 3429 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3431 def __rtruediv__(self, other): 3432 """Create the Z3 expression (signed) division `other / self`.
""" 3433 return self.__rdiv__(other) 3435 def __mod__(self, other): 3436 """Create the Z3 expression (signed) mod `self % other`.
3438 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3453 a, b = _coerce_exprs(self, other) 3454 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3456 def __rmod__(self, other): 3457 """Create the Z3 expression (signed) mod `other % self`.
3459 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3464 >>> (10 % x).
sexpr()
3465 '(bvsmod #x0000000a x)' 3467 '(bvurem #x0000000a x)' 3469 '(bvsrem #x0000000a x)' 3471 a, b = _coerce_exprs(self, other) 3472 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3474 def __le__(self, other): 3475 """Create the Z3 expression (signed) `other <= self`.
3477 Use the function
ULE()
for unsigned less than
or equal to.
3482 >>> (x <= y).
sexpr()
3487 a, b = _coerce_exprs(self, other) 3488 return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3490 def __lt__(self, other): 3491 """Create the Z3 expression (signed) `other < self`.
3493 Use the function
ULT()
for unsigned less than.
3503 a, b = _coerce_exprs(self, other) 3504 return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3506 def __gt__(self, other): 3507 """Create the Z3 expression (signed) `other > self`.
3509 Use the function
UGT()
for unsigned greater than.
3519 a, b = _coerce_exprs(self, other) 3520 return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3522 def __ge__(self, other): 3523 """Create the Z3 expression (signed) `other >= self`.
3525 Use the function
UGE()
for unsigned greater than
or equal to.
3530 >>> (x >= y).
sexpr()
3535 a, b = _coerce_exprs(self, other) 3536 return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3538 def __rshift__(self, other): 3539 """Create the Z3 expression (arithmetical) right shift `self >> other`
3541 Use the function
LShR()
for the right logical shift
3546 >>> (x >> y).
sexpr()
3565 a, b = _coerce_exprs(self, other) 3566 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3568 def __lshift__(self, other): 3569 """Create the Z3 expression left shift `self << other`
3574 >>> (x << y).
sexpr()
3579 a, b = _coerce_exprs(self, other) 3580 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3582 def __rrshift__(self, other): 3583 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3585 Use the function
LShR()
for the right logical shift
3590 >>> (10 >> x).
sexpr()
3591 '(bvashr #x0000000a x)' 3593 a, b = _coerce_exprs(self, other) 3594 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3596 def __rlshift__(self, other): 3597 """Create the Z3 expression left shift `other << self`.
3599 Use the function
LShR()
for the right logical shift
3604 >>> (10 << x).
sexpr()
3605 '(bvshl #x0000000a x)' 3607 a, b = _coerce_exprs(self, other) 3608 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3610 class BitVecNumRef(BitVecRef): 3611 """Bit-vector values.
""" 3614 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral.
3619 >>> print(
"0x%.8x" % v.as_long())
3622 return int(self.as_string()) 3624 def as_signed_long(self): 3625 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral. The most significant bit
is assumed to be the sign.
3639 val = self.as_long() 3640 if val >= 2**(sz - 1): 3642 if val < -2**(sz - 1): 3646 def as_string(self): 3647 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 3650 """Return `
True`
if `a`
is a Z3 bit-vector expression.
3660 return isinstance(a, BitVecRef) 3663 """Return `
True`
if `a`
is a Z3 bit-vector numeral value.
3674 return is_bv(a) and _is_numeral(a.ctx, a.as_ast()) 3676 def BV2Int(a, is_signed=False): 3677 """Return the Z3 expression
BV2Int(a).
3685 >>> x >
BV2Int(b, is_signed=
False)
3687 >>> x >
BV2Int(b, is_signed=
True)
3693 _z3_assert(is_bv(a), "Z3 bit-vector expression expected") 3695 ## investigate problem with bv2int 3696 return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx) 3698 def Int2BV(a, num_bits): 3699 """Return the z3 expression
Int2BV(a, num_bits).
3700 It
is a bit-vector of width num_bits
and represents the
3701 modulo of a by 2^num_bits
3704 return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx) 3706 def BitVecSort(sz, ctx=None): 3707 """Return a Z3 bit-vector sort of the given size. If `ctx=
None`, then the
global context
is used.
3713 >>> x =
Const(
'x', Byte)
3718 return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx) 3720 def BitVecVal(val, bv, ctx=None): 3721 """Return a bit-vector value with the given number of bits. If `ctx=
None`, then the
global context
is used.
3726 >>> print(
"0x%.8x" % v.as_long())
3731 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx) 3734 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx) 3736 def BitVec(name, bv, ctx=None): 3737 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3738 If `ctx=
None`, then the
global context
is used.
3748 >>> x2 =
BitVec(
'x', word)
3752 if isinstance(bv, BitVecSortRef): 3756 bv = BitVecSort(bv, ctx) 3757 return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx) 3759 def BitVecs(names, bv, ctx=None): 3760 """Return a tuple of bit-vector constants of size bv.
3762 >>> x, y, z =
BitVecs(
'x y z', 16)
3775 if isinstance(names, str): 3776 names = names.split(" ") 3777 return [BitVec(name, bv, ctx) for name in names] 3780 """Create a Z3 bit-vector concatenation expression.
3790 args = _get_args(args) 3793 _z3_assert(sz >= 2, "At least two arguments expected.") 3800 if is_seq(args[0]) or isinstance(args[0], str): 3801 args = [_coerce_seq(s, ctx) for s in args] 3803 _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") 3806 v[i] = args[i].as_ast() 3807 return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) 3811 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 3814 v[i] = args[i].as_ast() 3815 return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx) 3818 _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") 3820 for i in range(sz - 1): 3821 r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx) 3824 def Extract(high, low, a): 3825 """Create a Z3 bit-vector extraction expression,
or create a string extraction expression.
3835 if isinstance(high, str): 3836 high = StringVal(high) 3839 offset, length = _coerce_exprs(low, a, s.ctx) 3840 return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) 3842 _z3_assert(low <= high, "First argument must be greater than or equal to second argument") 3843 _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers") 3844 _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression") 3845 return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx) 3847 def _check_bv_args(a, b): 3849 _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression") 3852 """Create the Z3 expression (unsigned) `other <= self`.
3854 Use the operator <=
for signed less than
or equal to.
3859 >>> (x <= y).sexpr()
3861 >>>
ULE(x, y).sexpr()
3864 _check_bv_args(a, b) 3865 a, b = _coerce_exprs(a, b) 3866 return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3869 """Create the Z3 expression (unsigned) `other < self`.
3871 Use the operator <
for signed less than.
3878 >>>
ULT(x, y).sexpr()
3881 _check_bv_args(a, b) 3882 a, b = _coerce_exprs(a, b) 3883 return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3886 """Create the Z3 expression (unsigned) `other >= self`.
3888 Use the operator >=
for signed greater than
or equal to.
3893 >>> (x >= y).sexpr()
3895 >>>
UGE(x, y).sexpr()
3898 _check_bv_args(a, b) 3899 a, b = _coerce_exprs(a, b) 3900 return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3903 """Create the Z3 expression (unsigned) `other > self`.
3905 Use the operator >
for signed greater than.
3912 >>>
UGT(x, y).sexpr()
3915 _check_bv_args(a, b) 3916 a, b = _coerce_exprs(a, b) 3917 return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3920 """Create the Z3 expression (unsigned) division `self / other`.
3922 Use the operator /
for signed division.
3928 >>>
UDiv(x, y).sort()
3932 >>>
UDiv(x, y).sexpr()
3935 _check_bv_args(a, b) 3936 a, b = _coerce_exprs(a, b) 3937 return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3940 """Create the Z3 expression (unsigned) remainder `self % other`.
3942 Use the operator %
for signed modulus,
and SRem()
for signed remainder.
3948 >>>
URem(x, y).sort()
3952 >>>
URem(x, y).sexpr()
3955 _check_bv_args(a, b) 3956 a, b = _coerce_exprs(a, b) 3957 return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3960 """Create the Z3 expression signed remainder.
3962 Use the operator %
for signed modulus,
and URem()
for unsigned remainder.
3968 >>>
SRem(x, y).sort()
3972 >>>
SRem(x, y).sexpr()
3975 _check_bv_args(a, b) 3976 a, b = _coerce_exprs(a, b) 3977 return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3980 """Create the Z3 expression logical right shift.
3982 Use the operator >>
for the arithmetical right shift.
3987 >>> (x >> y).sexpr()
3989 >>>
LShR(x, y).sexpr()
4006 _check_bv_args(a, b) 4007 a, b = _coerce_exprs(a, b) 4008 return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4010 def RotateLeft(a, b): 4011 """Return an expression representing `a` rotated to the left `b` times.
4021 _check_bv_args(a, b) 4022 a, b = _coerce_exprs(a, b) 4023 return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4025 def RotateRight(a, b): 4026 """Return an expression representing `a` rotated to the right `b` times.
4036 _check_bv_args(a, b) 4037 a, b = _coerce_exprs(a, b) 4038 return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4041 """Return a bit-vector expression with `n` extra sign-bits.
4061 >>> print(
"%.x" % v.as_long())
4065 _z3_assert(_is_int(n), "First argument must be an integer") 4066 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 4067 return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 4070 """Return a bit-vector expression with `n` extra zero-bits.
4092 _z3_assert(_is_int(n), "First argument must be an integer") 4093 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 4094 return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 4096 def RepeatBitVec(n, a): 4097 """Return an expression representing `n` copies of `a`.
4106 >>> print(
"%.x" % v0.as_long())
4111 >>> print(
"%.x" % v.as_long())
4115 _z3_assert(_is_int(n), "First argument must be an integer") 4116 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 4117 return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx) 4120 """Return the reduction-
and expression of `a`.
""" 4122 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 4123 return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) 4126 """Return the reduction-
or expression of `a`.
""" 4128 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 4129 return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) 4131 def BVAddNoOverflow(a, b, signed): 4132 """A predicate the determines that bit-vector addition does
not overflow
""" 4133 _check_bv_args(a, b) 4134 a, b = _coerce_exprs(a, b) 4135 return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4137 def BVAddNoUnderflow(a, b): 4138 """A predicate the determines that signed bit-vector addition does
not underflow
""" 4139 _check_bv_args(a, b) 4140 a, b = _coerce_exprs(a, b) 4141 return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4143 def BVSubNoOverflow(a, b): 4144 """A predicate the determines that bit-vector subtraction does
not overflow
""" 4145 _check_bv_args(a, b) 4146 a, b = _coerce_exprs(a, b) 4147 return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4150 def BVSubNoUnderflow(a, b, signed): 4151 """A predicate the determines that bit-vector subtraction does
not underflow
""" 4152 _check_bv_args(a, b) 4153 a, b = _coerce_exprs(a, b) 4154 return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4156 def BVSDivNoOverflow(a, b): 4157 """A predicate the determines that bit-vector signed division does
not overflow
""" 4158 _check_bv_args(a, b) 4159 a, b = _coerce_exprs(a, b) 4160 return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4162 def BVSNegNoOverflow(a): 4163 """A predicate the determines that bit-vector unary negation does
not overflow
""" 4165 _z3_assert(is_bv(a), "Argument should be a bit-vector") 4166 return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx) 4168 def BVMulNoOverflow(a, b, signed): 4169 """A predicate the determines that bit-vector multiplication does
not overflow
""" 4170 _check_bv_args(a, b) 4171 a, b = _coerce_exprs(a, b) 4172 return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4175 def BVMulNoUnderflow(a, b): 4176 """A predicate the determines that bit-vector signed multiplication does
not underflow
""" 4177 _check_bv_args(a, b) 4178 a, b = _coerce_exprs(a, b) 4179 return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4183 ######################################### 4187 ######################################### 4189 class ArraySortRef(SortRef): 4193 """Return the domain of the array sort `self`.
4199 return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx) 4202 """Return the range of the array sort `self`.
4208 return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx) 4210 class ArrayRef(ExprRef): 4211 """Array expressions.
""" 4214 """Return the array sort of the array expression `self`.
4220 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4229 return self.sort().domain() 4238 return self.sort().range() 4240 def __getitem__(self, arg): 4241 """Return the Z3 expression `self[arg]`.
4250 arg = self.domain().cast(arg) 4251 return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx) 4254 return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx) 4258 """Return `
True`
if `a`
is a Z3 array expression.
4268 return isinstance(a, ArrayRef) 4270 def is_const_array(a): 4271 """Return `
True`
if `a`
is a Z3 constant array.
4280 return is_app_of(a, Z3_OP_CONST_ARRAY) 4283 """Return `
True`
if `a`
is a Z3 constant array.
4292 return is_app_of(a, Z3_OP_CONST_ARRAY) 4295 """Return `
True`
if `a`
is a Z3 map array expression.
4307 return is_app_of(a, Z3_OP_ARRAY_MAP) 4310 """Return `
True`
if `a`
is a Z3 default array expression.
4315 return is_app_of(a, Z3_OP_ARRAY_DEFAULT) 4317 def get_map_func(a): 4318 """Return the function declaration associated with a Z3 map array expression.
4331 _z3_assert(is_map(a), "Z3 array map expression expected.") 4332 return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx) 4334 def ArraySort(*sig): 4335 """Return the Z3 array sort with the given domain
and range sorts.
4348 sig = _get_args(sig) 4350 _z3_assert(len(sig) > 1, "At least two arguments expected") 4351 arity = len(sig) - 1 4356 _z3_assert(is_sort(s), "Z3 sort expected") 4357 _z3_assert(s.ctx == r.ctx, "Context mismatch") 4360 return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx) 4361 dom = (Sort * arity)() 4362 for i in range(arity): 4364 return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx) 4366 def Array(name, dom, rng): 4367 """Return an array constant named `name` with the given domain
and range sorts.
4375 s = ArraySort(dom, rng) 4377 return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx) 4379 def Update(a, i, v): 4380 """Return a Z3 store array expression.
4383 >>> i, v =
Ints(
'i v')
4387 >>>
prove(s[i] == v)
4394 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4395 i = a.domain().cast(i) 4396 v = a.range().cast(v) 4398 return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx) 4401 """ Return a default value
for array expression.
4407 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4412 """Return a Z3 store array expression.
4415 >>> i, v =
Ints(
'i v')
4416 >>> s =
Store(a, i, v)
4419 >>>
prove(s[i] == v)
4425 return Update(a, i, v) 4428 """Return a Z3 select array expression.
4438 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4443 """Return a Z3 map array expression.
4448 >>> b =
Map(f, a1, a2)
4451 >>>
prove(b[0] == f(a1[0], a2[0]))
4454 args = _get_args(args) 4456 _z3_assert(len(args) > 0, "At least one Z3 array expression expected") 4457 _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration") 4458 _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected") 4459 _z3_assert(len(args) == f.arity(), "Number of arguments mismatch") 4460 _args, sz = _to_ast_array(args) 4462 return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx) 4465 """Return a Z3 constant array expression.
4479 _z3_assert(is_sort(dom), "Z3 sort expected") 4482 v = _py2expr(v, ctx) 4483 return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx) 4486 """Return extensionality index
for arrays.
4489 _z3_assert(is_array(a) and is_array(b)) 4490 return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast())); 4493 """Return `
True`
if `a`
is a Z3 array select application.
4502 return is_app_of(a, Z3_OP_SELECT) 4505 """Return `
True`
if `a`
is a Z3 array store application.
4513 return is_app_of(a, Z3_OP_STORE) 4515 ######################################### 4519 ######################################### 4523 """ Create a set sort over element sort s
""" 4524 return ArraySort(s, BoolSort()) 4527 """Create the empty set
4532 return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx) 4535 """Create the full set
4540 return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx) 4542 def SetUnion(*args): 4543 """ Take the union of sets
4549 args = _get_args(args) 4550 ctx = _ctx_from_ast_arg_list(args) 4551 _args, sz = _to_ast_array(args) 4552 return ArrayRef(Z3_mk_set_union(ctx.ref(), sz, _args), ctx) 4554 def SetIntersect(*args): 4555 """ Take the union of sets
4561 args = _get_args(args) 4562 ctx = _ctx_from_ast_arg_list(args) 4563 _args, sz = _to_ast_array(args) 4564 return ArrayRef(Z3_mk_set_intersect(ctx.ref(), sz, _args), ctx) 4567 """ Add element e to set s
4572 ctx = _ctx_from_ast_arg_list([s,e]) 4573 e = _py2expr(e, ctx) 4574 return ArrayRef(Z3_mk_set_add(ctx.ref(), s.as_ast(), e.as_ast()), ctx) 4577 """ Remove element e to set s
4582 ctx = _ctx_from_ast_arg_list([s,e]) 4583 e = _py2expr(e, ctx) 4584 return ArrayRef(Z3_mk_set_del(ctx.ref(), s.as_ast(), e.as_ast()), ctx) 4586 def SetComplement(s): 4587 """ The complement of set s
4593 return ArrayRef(Z3_mk_set_complement(ctx.ref(), s.as_ast()), ctx) 4595 def SetDifference(a, b): 4596 """ The set difference of a
and b
4602 ctx = _ctx_from_ast_arg_list([a, b]) 4603 return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 4606 """ Check
if e
is a member of set s
4611 ctx = _ctx_from_ast_arg_list([s,e]) 4612 e = _py2expr(e, ctx) 4613 return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx) 4616 """ Check
if a
is a subset of b
4622 ctx = _ctx_from_ast_arg_list([a, b]) 4623 return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 4626 ######################################### 4630 ######################################### 4632 def _valid_accessor(acc): 4633 """Return `
True`
if acc
is pair of the form (String, Datatype
or Sort).
""" 4634 return isinstance(acc, tuple) and len(acc) == 2 and isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1])) 4637 """Helper
class for declaring Z3 datatypes.
4640 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4641 >>> List.declare(
'nil')
4642 >>> List = List.create()
4646 >>> List.cons(10, List.nil)
4648 >>> List.cons(10, List.nil).sort()
4650 >>> cons = List.cons
4654 >>> n = cons(1, cons(0, nil))
4656 cons(1, cons(0, nil))
4662 def __init__(self, name, ctx=None): 4663 self.ctx = _get_ctx(ctx) 4665 self.constructors = [] 4667 def __deepcopy__(self, memo={}): 4668 r = Datatype(self.name, self.ctx) 4669 r.constructors = copy.deepcopy(self.constructors) 4672 def declare_core(self, name, rec_name, *args): 4674 _z3_assert(isinstance(name, str), "String expected") 4675 _z3_assert(isinstance(rec_name, str), "String expected") 4676 _z3_assert(all([_valid_accessor(a) for a in args]), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)") 4677 self.constructors.append((name, rec_name, args)) 4679 def declare(self, name, *args): 4680 """Declare constructor named `name` with the given accessors `args`.
4681 Each accessor
is a pair `(name, sort)`, where `name`
is a string
and `sort` a Z3 sort
or a reference to the datatypes being declared.
4683 In the following example `List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))`
4684 declares the constructor named `cons` that builds a new List using an integer
and a List.
4685 It also declares the accessors `car`
and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
4686 and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method
create() to create
4687 the actual datatype
in Z3.
4690 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4691 >>> List.declare(
'nil')
4692 >>> List = List.create()
4695 _z3_assert(isinstance(name, str), "String expected") 4696 _z3_assert(name != "", "Constructor name cannot be empty") 4697 return self.declare_core(name, "is-" + name, *args) 4700 return "Datatype(%s, %s)" % (self.name, self.constructors) 4703 """Create a Z3 datatype based on the constructors declared using the method `
declare()`.
4705 The function `
CreateDatatypes()` must be used to define mutually recursive datatypes.
4708 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4709 >>> List.declare(
'nil')
4710 >>> List = List.create()
4713 >>> List.cons(10, List.nil)
4716 return CreateDatatypes([self])[0] 4718 class ScopedConstructor: 4719 """Auxiliary object used to create Z3 datatypes.
""" 4720 def __init__(self, c, ctx): 4724 if self.ctx.ref() is not None: 4725 Z3_del_constructor(self.ctx.ref(), self.c) 4727 class ScopedConstructorList: 4728 """Auxiliary object used to create Z3 datatypes.
""" 4729 def __init__(self, c, ctx): 4733 if self.ctx.ref() is not None: 4734 Z3_del_constructor_list(self.ctx.ref(), self.c) 4736 def CreateDatatypes(*ds): 4737 """Create mutually recursive Z3 datatypes using 1
or more Datatype helper objects.
4739 In the following example we define a Tree-List using two mutually recursive datatypes.
4741 >>> TreeList =
Datatype(
'TreeList')
4744 >>> Tree.declare(
'leaf', (
'val',
IntSort()))
4746 >>> Tree.declare(
'node', (
'children', TreeList))
4747 >>> TreeList.declare(
'nil')
4748 >>> TreeList.declare(
'cons', (
'car', Tree), (
'cdr', TreeList))
4750 >>> Tree.val(Tree.leaf(10))
4752 >>>
simplify(Tree.val(Tree.leaf(10)))
4754 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4756 node(cons(leaf(10), cons(leaf(20), nil)))
4757 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4760 >>>
simplify(TreeList.car(Tree.children(n2)) == n1)
4765 _z3_assert(len(ds) > 0, "At least one Datatype must be specified") 4766 _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes") 4767 _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch") 4768 _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected") 4771 names = (Symbol * num)() 4772 out = (Sort * num)() 4773 clists = (ConstructorList * num)() 4775 for i in range(num): 4777 names[i] = to_symbol(d.name, ctx) 4778 num_cs = len(d.constructors) 4779 cs = (Constructor * num_cs)() 4780 for j in range(num_cs): 4781 c = d.constructors[j] 4782 cname = to_symbol(c[0], ctx) 4783 rname = to_symbol(c[1], ctx) 4786 fnames = (Symbol * num_fs)() 4787 sorts = (Sort * num_fs)() 4788 refs = (ctypes.c_uint * num_fs)() 4789 for k in range(num_fs): 4792 fnames[k] = to_symbol(fname, ctx) 4793 if isinstance(ftype, Datatype): 4795 _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected") 4797 refs[k] = ds.index(ftype) 4800 _z3_assert(is_sort(ftype), "Z3 sort expected") 4801 sorts[k] = ftype.ast 4803 cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs) 4804 to_delete.append(ScopedConstructor(cs[j], ctx)) 4805 clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs) 4806 to_delete.append(ScopedConstructorList(clists[i], ctx)) 4807 Z3_mk_datatypes(ctx.ref(), num, names, out, clists) 4809 ## Create a field for every constructor, recognizer and accessor 4810 for i in range(num): 4811 dref = DatatypeSortRef(out[i], ctx) 4812 num_cs = dref.num_constructors() 4813 for j in range(num_cs): 4814 cref = dref.constructor(j) 4815 cref_name = cref.name() 4816 cref_arity = cref.arity() 4817 if cref.arity() == 0: 4819 setattr(dref, cref_name, cref) 4820 rref = dref.recognizer(j) 4821 setattr(dref, "is_" + cref_name, rref) 4822 for k in range(cref_arity): 4823 aref = dref.accessor(j, k) 4824 setattr(dref, aref.name(), aref) 4826 return tuple(result) 4828 class DatatypeSortRef(SortRef): 4829 """Datatype sorts.
""" 4830 def num_constructors(self): 4831 """Return the number of constructors
in the given Z3 datatype.
4834 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4835 >>> List.declare(
'nil')
4836 >>> List = List.create()
4838 >>> List.num_constructors()
4841 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast)) 4843 def constructor(self, idx): 4844 """Return a constructor of the datatype `self`.
4847 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4848 >>> List.declare(
'nil')
4849 >>> List = List.create()
4851 >>> List.num_constructors()
4853 >>> List.constructor(0)
4855 >>> List.constructor(1)
4859 _z3_assert(idx < self.num_constructors(), "Invalid constructor index") 4860 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx) 4862 def recognizer(self, idx): 4863 """In Z3, each constructor has an associated recognizer predicate.
4865 If the constructor
is named `name`, then the recognizer `is_name`.
4868 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4869 >>> List.declare(
'nil')
4870 >>> List = List.create()
4872 >>> List.num_constructors()
4874 >>> List.recognizer(0)
4876 >>> List.recognizer(1)
4878 >>>
simplify(List.is_nil(List.cons(10, List.nil)))
4880 >>>
simplify(List.is_cons(List.cons(10, List.nil)))
4882 >>> l =
Const(
'l', List)
4887 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index") 4888 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx) 4890 def accessor(self, i, j): 4891 """In Z3, each constructor has 0
or more accessor. The number of accessors
is equal to the arity of the constructor.
4894 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4895 >>> List.declare(
'nil')
4896 >>> List = List.create()
4897 >>> List.num_constructors()
4899 >>> List.constructor(0)
4901 >>> num_accs = List.constructor(0).arity()
4904 >>> List.accessor(0, 0)
4906 >>> List.accessor(0, 1)
4908 >>> List.constructor(1)
4910 >>> num_accs = List.constructor(1).arity()
4915 _z3_assert(i < self.num_constructors(), "Invalid constructor index") 4916 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index") 4917 return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx) 4919 class DatatypeRef(ExprRef): 4920 """Datatype expressions.
""" 4922 """Return the datatype sort of the datatype expression `self`.
""" 4923 return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4925 def EnumSort(name, values, ctx=None): 4926 """Return a new enumeration sort named `name` containing the given values.
4928 The result
is a pair (sort, list of constants).
4930 >>> Color, (red, green, blue) =
EnumSort(
'Color', [
'red',
'green',
'blue'])
4933 _z3_assert(isinstance(name, str), "Name must be a string") 4934 _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings") 4935 _z3_assert(len(values) > 0, "At least one value expected") 4938 _val_names = (Symbol * num)() 4939 for i in range(num): 4940 _val_names[i] = to_symbol(values[i]) 4941 _values = (FuncDecl * num)() 4942 _testers = (FuncDecl * num)() 4943 name = to_symbol(name) 4944 S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx) 4946 for i in range(num): 4947 V.append(FuncDeclRef(_values[i], ctx)) 4948 V = [a() for a in V] 4951 ######################################### 4955 ######################################### 4958 """Set of parameters used to configure Solvers, Tactics
and Simplifiers
in Z3.
4960 Consider using the function `args2params` to create instances of this object.
4962 def __init__(self, ctx=None, params=None): 4963 self.ctx = _get_ctx(ctx) 4965 self.params = Z3_mk_params(self.ctx.ref()) 4967 self.params = params 4968 Z3_params_inc_ref(self.ctx.ref(), self.params) 4970 def __deepcopy__(self, memo={}): 4971 return ParamsRef(self.ctx, self.params) 4974 if self.ctx.ref() is not None: 4975 Z3_params_dec_ref(self.ctx.ref(), self.params) 4977 def set(self, name, val): 4978 """Set parameter name with value val.
""" 4980 _z3_assert(isinstance(name, str), "parameter name must be a string") 4981 name_sym = to_symbol(name, self.ctx) 4982 if isinstance(val, bool): 4983 Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val) 4985 Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val) 4986 elif isinstance(val, float): 4987 Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val) 4988 elif isinstance(val, str): 4989 Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx)) 4992 _z3_assert(False, "invalid parameter value") 4995 return Z3_params_to_string(self.ctx.ref(), self.params) 4997 def validate(self, ds): 4998 _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected") 4999 Z3_params_validate(self.ctx.ref(), self.params, ds.descr) 5001 def args2params(arguments, keywords, ctx=None): 5002 """Convert python arguments into a Z3_params object.
5003 A
':' is added to the keywords,
and '_' is replaced with
'-' 5005 >>>
args2params([
'model',
True,
'relevancy', 2], {
'elim_and' :
True})
5006 (params model true relevancy 2 elim_and true)
5009 _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") 5023 class ParamDescrsRef: 5024 """Set of parameter descriptions
for Solvers, Tactics
and Simplifiers
in Z3.
5026 def __init__(self, descr, ctx=None): 5027 _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected") 5028 self.ctx = _get_ctx(ctx) 5030 Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr) 5032 def __deepcopy__(self, memo={}): 5033 return ParamsDescrsRef(self.descr, self.ctx) 5036 if self.ctx.ref() is not None: 5037 Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr) 5040 """Return the size of
in the parameter description `self`.
5042 return int(Z3_param_descrs_size(self.ctx.ref(), self.descr)) 5045 """Return the size of
in the parameter description `self`.
5049 def get_name(self, i): 5050 """Return the i-th parameter name
in the parameter description `self`.
5052 return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i)) 5054 def get_kind(self, n): 5055 """Return the kind of the parameter named `n`.
5057 return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 5059 def get_documentation(self, n): 5060 """Return the documentation string of the parameter named `n`.
5062 return Z3_param_descrs_get_documentation(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 5064 def __getitem__(self, arg): 5066 return self.get_name(arg) 5068 return self.get_kind(arg) 5071 return Z3_param_descrs_to_string(self.ctx.ref(), self.descr) 5073 ######################################### 5077 ######################################### 5079 class Goal(Z3PPObject): 5080 """Goal
is a collection of constraints we want to find a solution
or show to be unsatisfiable (infeasible).
5082 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
5083 A goal has a solution
if one of its subgoals has a solution.
5084 A goal
is unsatisfiable
if all subgoals are unsatisfiable.
5087 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None): 5089 _z3_assert(goal is None or ctx is not None, "If goal is different from None, then ctx must be also different from None") 5090 self.ctx = _get_ctx(ctx) 5092 if self.goal is None: 5093 self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs) 5094 Z3_goal_inc_ref(self.ctx.ref(), self.goal) 5096 def __deepcopy__(self, memo={}): 5097 return Goal(False, False, False, self.ctx, self.goal) 5100 if self.goal is not None and self.ctx.ref() is not None: 5101 Z3_goal_dec_ref(self.ctx.ref(), self.goal) 5104 """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
5106 >>> x, y =
Ints(
'x y')
5108 >>> g.add(x == 0, y >= x + 1)
5111 >>> r =
Then(
'simplify',
'solve-eqs')(g)
5118 return int(Z3_goal_depth(self.ctx.ref(), self.goal)) 5120 def inconsistent(self): 5121 """Return `
True`
if `self` contains the `
False` constraints.
5123 >>> x, y =
Ints(
'x y')
5125 >>> g.inconsistent()
5127 >>> g.add(x == 0, x == 1)
5130 >>> g.inconsistent()
5132 >>> g2 =
Tactic(
'propagate-values')(g)[0]
5133 >>> g2.inconsistent()
5136 return Z3_goal_inconsistent(self.ctx.ref(), self.goal) 5139 """Return the precision (under-approximation, over-approximation,
or precise) of the goal `self`.
5142 >>> g.prec() == Z3_GOAL_PRECISE
5144 >>> x, y =
Ints(
'x y')
5145 >>> g.add(x == y + 1)
5146 >>> g.prec() == Z3_GOAL_PRECISE
5148 >>> t =
With(
Tactic(
'add-bounds'), add_bound_lower=0, add_bound_upper=10)
5151 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
5152 >>> g2.prec() == Z3_GOAL_PRECISE
5154 >>> g2.prec() == Z3_GOAL_UNDER
5157 return Z3_goal_precision(self.ctx.ref(), self.goal) 5159 def precision(self): 5160 """Alias
for `
prec()`.
5163 >>> g.precision() == Z3_GOAL_PRECISE
5169 """Return the number of constraints
in the goal `self`.
5174 >>> x, y =
Ints(
'x y')
5175 >>> g.add(x == 0, y > x)
5179 return int(Z3_goal_size(self.ctx.ref(), self.goal)) 5182 """Return the number of constraints
in the goal `self`.
5187 >>> x, y =
Ints(
'x y')
5188 >>> g.add(x == 0, y > x)
5195 """Return a constraint
in the goal `self`.
5198 >>> x, y =
Ints(
'x y')
5199 >>> g.add(x == 0, y > x)
5205 return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx) 5207 def __getitem__(self, arg): 5208 """Return a constraint
in the goal `self`.
5211 >>> x, y =
Ints(
'x y')
5212 >>> g.add(x == 0, y > x)
5218 if arg >= len(self): 5220 return self.get(arg) 5222 def assert_exprs(self, *args): 5223 """Assert constraints into the goal.
5227 >>> g.assert_exprs(x > 0, x < 2)
5231 args = _get_args(args) 5232 s = BoolSort(self.ctx) 5235 Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast()) 5237 def append(self, *args): 5242 >>> g.append(x > 0, x < 2)
5246 self.assert_exprs(*args) 5248 def insert(self, *args): 5253 >>> g.insert(x > 0, x < 2)
5257 self.assert_exprs(*args) 5259 def add(self, *args): 5264 >>> g.add(x > 0, x < 2)
5268 self.assert_exprs(*args) 5270 def convert_model(self, model): 5271 """Retrieve model
from a satisfiable goal
5272 >>> a, b =
Ints(
'a b')
5274 >>> g.add(
Or(a == 0, a == 1),
Or(b == 0, b == 1), a > b)
5278 [
Or(b == 0, b == 1),
Not(0 <= b)]
5280 [
Or(b == 0, b == 1),
Not(1 <= b)]
5296 _z3_assert(isinstance(model, ModelRef), "Z3 Model expected") 5297 return ModelRef(Z3_goal_convert_model(self.ctx.ref(), self.goal, model.model), self.ctx) 5300 return obj_to_string(self) 5303 """Return a textual representation of the s-expression representing the goal.
""" 5304 return Z3_goal_to_string(self.ctx.ref(), self.goal) 5307 """Return a textual representation of the goal
in DIMACS format.
""" 5308 return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal) 5310 def translate(self, target): 5311 """Copy goal `self` to context `target`.
5319 >>> g2 = g.translate(c2)
5330 _z3_assert(isinstance(target, Context), "target must be a context") 5331 return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target) 5334 return self.translate(self.ctx) 5336 def __deepcopy__(self): 5337 return self.translate(self.ctx) 5339 def simplify(self, *arguments, **keywords): 5340 """Return a new simplified goal.
5342 This method
is essentially invoking the simplify tactic.
5346 >>> g.add(x + 1 >= 2)
5349 >>> g2 = g.simplify()
5356 t = Tactic('simplify') 5357 return t.apply(self, *arguments, **keywords)[0] 5360 """Return goal `self`
as a single Z3 expression.
5375 return BoolVal(True, self.ctx) 5379 return And([ self.get(i) for i in range(len(self)) ], self.ctx) 5381 ######################################### 5385 ######################################### 5386 class AstVector(Z3PPObject): 5387 """A collection (vector) of ASTs.
""" 5389 def __init__(self, v=None, ctx=None): 5392 self.ctx = _get_ctx(ctx) 5393 self.vector = Z3_mk_ast_vector(self.ctx.ref()) 5396 assert ctx is not None 5398 Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector) 5400 def __deepcopy__(self, memo={}): 5401 return AstVector(self.vector, self.ctx) 5404 if self.vector is not None and self.ctx.ref() is not None: 5405 Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector) 5408 """Return the size of the vector `self`.
5413 >>> A.push(
Int(
'x'))
5414 >>> A.push(
Int(
'x'))
5418 return int(Z3_ast_vector_size(self.ctx.ref(), self.vector)) 5420 def __getitem__(self, i): 5421 """Return the AST at position `i`.
5424 >>> A.push(
Int(
'x') + 1)
5425 >>> A.push(
Int(
'y'))
5432 if isinstance(i, int): 5436 if i >= self.__len__(): 5438 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx) 5440 elif isinstance(i, slice): 5441 return [_to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, ii), self.ctx) for ii in range(*i.indices(self.__len__()))] 5444 def __setitem__(self, i, v): 5445 """Update AST at position `i`.
5448 >>> A.push(
Int(
'x') + 1)
5449 >>> A.push(
Int(
'y'))
5456 if i >= self.__len__(): 5458 Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast()) 5461 """Add `v`
in the end of the vector.
5466 >>> A.push(
Int(
'x'))
5470 Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast()) 5472 def resize(self, sz): 5473 """Resize the vector to `sz` elements.
5479 >>>
for i
in range(10): A[i] =
Int(
'x')
5483 Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz) 5485 def __contains__(self, item): 5486 """Return `
True`
if the vector contains `item`.
5508 def translate(self, other_ctx): 5509 """Copy vector `self` to context `other_ctx`.
5515 >>> B = A.translate(c2)
5519 return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx) 5522 return self.translate(self.ctx) 5524 def __deepcopy__(self): 5525 return self.translate(self.ctx) 5528 return obj_to_string(self) 5531 """Return a textual representation of the s-expression representing the vector.
""" 5532 return Z3_ast_vector_to_string(self.ctx.ref(), self.vector) 5534 ######################################### 5538 ######################################### 5540 """A mapping
from ASTs to ASTs.
""" 5542 def __init__(self, m=None, ctx=None): 5545 self.ctx = _get_ctx(ctx) 5546 self.map = Z3_mk_ast_map(self.ctx.ref()) 5549 assert ctx is not None 5551 Z3_ast_map_inc_ref(self.ctx.ref(), self.map) 5553 def __deepcopy__(self, memo={}): 5554 return AstMap(self.map, self.ctx) 5557 if self.map is not None and self.ctx.ref() is not None: 5558 Z3_ast_map_dec_ref(self.ctx.ref(), self.map) 5561 """Return the size of the map.
5571 return int(Z3_ast_map_size(self.ctx.ref(), self.map)) 5573 def __contains__(self, key): 5574 """Return `
True`
if the map contains key `key`.
5584 return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast()) 5586 def __getitem__(self, key): 5587 """Retrieve the value associated with key `key`.
5595 return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx) 5597 def __setitem__(self, k, v): 5598 """Add/Update key `k` with value `v`.
5611 Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast()) 5614 return Z3_ast_map_to_string(self.ctx.ref(), self.map) 5617 """Remove the entry associated with key `k`.
5628 Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast()) 5631 """Remove all entries
from the map.
5643 Z3_ast_map_reset(self.ctx.ref(), self.map) 5646 """Return an AstVector containing all keys
in the map.
5655 return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx) 5657 ######################################### 5661 ######################################### 5664 """Store the value of the interpretation of a function
in a particular point.
""" 5666 def __init__(self, entry, ctx): 5669 Z3_func_entry_inc_ref(self.ctx.ref(), self.entry) 5671 def __deepcopy__(self, memo={}): 5672 return FuncEntry(self.entry, self.ctx) 5675 if self.ctx.ref() is not None: 5676 Z3_func_entry_dec_ref(self.ctx.ref(), self.entry) 5679 """Return the number of arguments
in the given entry.
5683 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5688 >>> f_i.num_entries()
5690 >>> e = f_i.entry(0)
5694 return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry)) 5696 def arg_value(self, idx): 5697 """Return the value of argument `idx`.
5701 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5706 >>> f_i.num_entries()
5708 >>> e = f_i.entry(0)
5719 ...
except IndexError:
5720 ... print(
"index error")
5723 if idx >= self.num_args(): 5725 return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx) 5728 """Return the value of the function at point `self`.
5732 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5737 >>> f_i.num_entries()
5739 >>> e = f_i.entry(0)
5747 return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx) 5750 """Return entry `self`
as a Python list.
5753 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5758 >>> f_i.num_entries()
5760 >>> e = f_i.entry(0)
5764 args = [ self.arg_value(i) for i in range(self.num_args())] 5765 args.append(self.value()) 5769 return repr(self.as_list()) 5771 class FuncInterp(Z3PPObject): 5772 """Stores the interpretation of a function
in a Z3 model.
""" 5774 def __init__(self, f, ctx): 5777 if self.f is not None: 5778 Z3_func_interp_inc_ref(self.ctx.ref(), self.f) 5780 def __deepcopy__(self, memo={}): 5781 return FuncInterp(self.f, self.ctx) 5784 if self.f is not None and self.ctx.ref() is not None: 5785 Z3_func_interp_dec_ref(self.ctx.ref(), self.f) 5787 def else_value(self): 5789 Return the `
else` value
for a function interpretation.
5790 Return
None if Z3 did
not specify the `
else` value
for 5795 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5804 r = Z3_func_interp_get_else(self.ctx.ref(), self.f) 5806 return _to_expr_ref(r, self.ctx) 5810 def num_entries(self): 5811 """Return the number of entries/points
in the function interpretation `self`.
5815 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5824 return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f)) 5827 """Return the number of arguments
for each entry
in the function interpretation `self`.
5831 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5838 return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f)) 5840 def entry(self, idx): 5841 """Return an entry at position `idx < self.
num_entries()`
in the function interpretation `self`.
5845 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5856 if idx >= self.num_entries(): 5858 return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx) 5860 def translate(self, other_ctx): 5861 """Copy model
'self' to context
'other_ctx'.
5863 return ModelRef(Z3_model_translate(self.ctx.ref(), self.model, other_ctx.ref()), other_ctx) 5866 return self.translate(self.ctx) 5868 def __deepcopy__(self): 5869 return self.translate(self.ctx) 5872 """Return the function interpretation
as a Python list.
5875 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5884 r = [ self.entry(i).as_list() for i in range(self.num_entries())] 5885 r.append(self.else_value()) 5889 return obj_to_string(self) 5891 class ModelRef(Z3PPObject): 5892 """Model/Solution of a satisfiability problem (aka system of constraints).
""" 5894 def __init__(self, m, ctx): 5895 assert ctx is not None 5898 Z3_model_inc_ref(self.ctx.ref(), self.model) 5901 if self.ctx.ref() is not None: 5902 Z3_model_dec_ref(self.ctx.ref(), self.model) 5905 return obj_to_string(self) 5908 """Return a textual representation of the s-expression representing the model.
""" 5909 return Z3_model_to_string(self.ctx.ref(), self.model) 5911 def eval(self, t, model_completion=False): 5912 """Evaluate the expression `t`
in the model `self`. If `model_completion`
is enabled, then a default interpretation
is automatically added
for symbols that do
not have an interpretation
in the model `self`.
5916 >>> s.add(x > 0, x < 2)
5929 >>> m.eval(y, model_completion=
True)
5936 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r): 5937 return _to_expr_ref(r[0], self.ctx) 5938 raise Z3Exception("failed to evaluate expression in the model") 5940 def evaluate(self, t, model_completion=False): 5941 """Alias
for `eval`.
5945 >>> s.add(x > 0, x < 2)
5949 >>> m.evaluate(x + 1)
5951 >>> m.evaluate(x == 1)
5954 >>> m.evaluate(y + x)
5958 >>> m.evaluate(y, model_completion=
True)
5961 >>> m.evaluate(y + x)
5964 return self.eval(t, model_completion) 5967 """Return the number of constant
and function declarations
in the model `self`.
5972 >>> s.add(x > 0, f(x) != x)
5979 return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model)) 5981 def get_interp(self, decl): 5982 """Return the interpretation
for a given declaration
or constant.
5987 >>> s.add(x > 0, x < 2, f(x) == 0)
5997 _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected") 6001 if decl.arity() == 0: 6002 _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast) 6003 if _r.value is None: 6005 r = _to_expr_ref(_r, self.ctx) 6007 return self.get_interp(get_as_array_func(r)) 6011 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) 6015 def num_sorts(self): 6016 """Return the number of uninterpreted sorts that contain an interpretation
in the model `self`.
6019 >>> a, b =
Consts(
'a b', A)
6028 return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model)) 6030 def get_sort(self, idx): 6031 """Return the uninterpreted sort at position `idx` < self.
num_sorts().
6035 >>> a1, a2 =
Consts(
'a1 a2', A)
6036 >>> b1, b2 =
Consts(
'b1 b2', B)
6038 >>> s.add(a1 != a2, b1 != b2)
6049 if idx >= self.num_sorts(): 6051 return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx) 6054 """Return all uninterpreted sorts that have an interpretation
in the model `self`.
6058 >>> a1, a2 =
Consts(
'a1 a2', A)
6059 >>> b1, b2 =
Consts(
'b1 b2', B)
6061 >>> s.add(a1 != a2, b1 != b2)
6068 return [ self.get_sort(i) for i in range(self.num_sorts()) ] 6070 def get_universe(self, s): 6071 """Return the interpretation
for the uninterpreted sort `s`
in the model `self`.
6074 >>> a, b =
Consts(
'a b', A)
6080 >>> m.get_universe(A)
6084 _z3_assert(isinstance(s, SortRef), "Z3 sort expected") 6086 return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx) 6090 def __getitem__(self, idx): 6091 """If `idx`
is an integer, then the declaration at position `idx`
in the model `self`
is returned. If `idx`
is a declaration, then the actual interpretation
is returned.
6093 The elements can be retrieved using position
or the actual declaration.
6098 >>> s.add(x > 0, x < 2, f(x) == 0)
6112 >>>
for d
in m: print(
"%s -> %s" % (d, m[d]))
6117 if idx >= len(self): 6119 num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model) 6120 if (idx < num_consts): 6121 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx) 6123 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx) 6124 if isinstance(idx, FuncDeclRef): 6125 return self.get_interp(idx) 6127 return self.get_interp(idx.decl()) 6128 if isinstance(idx, SortRef): 6129 return self.get_universe(idx) 6131 _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected") 6135 """Return a list with all symbols that have an interpretation
in the model `self`.
6139 >>> s.add(x > 0, x < 2, f(x) == 0)
6147 for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)): 6148 r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx)) 6149 for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)): 6150 r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx)) 6153 def translate(self, target): 6154 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
6157 _z3_assert(isinstance(target, Context), "argument must be a Z3 context") 6158 model = Z3_model_translate(self.ctx.ref(), self.model, target.ref()) 6159 return Model(model, target) 6162 return self.translate(self.ctx) 6164 def __deepcopy__(self): 6165 return self.translate(self.ctx) 6167 def Model(ctx = None): 6169 return ModelRef(Z3_mk_model(ctx.ref()), ctx) 6172 """Return true
if n
is a Z3 expression of the form (_
as-array f).
""" 6173 return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast()) 6175 def get_as_array_func(n): 6176 """Return the function declaration f associated with a Z3 expression of the form (_
as-array f).
""" 6178 _z3_assert(is_as_array(n), "as-array Z3 expression expected.") 6179 return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx) 6181 ######################################### 6185 ######################################### 6187 """Statistics
for `Solver.check()`.
""" 6189 def __init__(self, stats, ctx): 6192 Z3_stats_inc_ref(self.ctx.ref(), self.stats) 6194 def __deepcopy__(self, memo={}): 6195 return Statistics(self.stats, self.ctx) 6198 if self.ctx.ref() is not None: 6199 Z3_stats_dec_ref(self.ctx.ref(), self.stats) 6205 out.write(u('<table border="1" cellpadding="2" cellspacing="0">')) 6208 out.write(u('<tr style="background-color:#CFCFCF">')) 6211 out.write(u('<tr>')) 6213 out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v))) 6214 out.write(u('</table>')) 6215 return out.getvalue() 6217 return Z3_stats_to_string(self.ctx.ref(), self.stats) 6220 """Return the number of statistical counters.
6223 >>> s =
Then(
'simplify',
'nlsat').solver()
6227 >>> st = s.statistics()
6231 return int(Z3_stats_size(self.ctx.ref(), self.stats)) 6233 def __getitem__(self, idx): 6234 """Return the value of statistical counter at position `idx`. The result
is a pair (key, value).
6237 >>> s =
Then(
'simplify',
'nlsat').solver()
6241 >>> st = s.statistics()
6245 (
'nlsat propagations', 2)
6249 if idx >= len(self): 6251 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 6252 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 6254 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 6255 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val) 6258 """Return the list of statistical counters.
6261 >>> s =
Then(
'simplify',
'nlsat').solver()
6265 >>> st = s.statistics()
6267 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))] 6269 def get_key_value(self, key): 6270 """Return the value of a particular statistical counter.
6273 >>> s =
Then(
'simplify',
'nlsat').solver()
6277 >>> st = s.statistics()
6278 >>> st.get_key_value(
'nlsat propagations')
6281 for idx in range(len(self)): 6282 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx): 6283 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 6284 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 6286 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 6287 raise Z3Exception("unknown key") 6289 def __getattr__(self, name): 6290 """Access the value of statistical using attributes.
6292 Remark: to access a counter containing blank spaces (e.g.,
'nlsat propagations'),
6293 we should use
'_' (e.g.,
'nlsat_propagations').
6296 >>> s =
Then(
'simplify',
'nlsat').solver()
6300 >>> st = s.statistics()
6301 >>> st.nlsat_propagations
6306 key = name.replace('_', ' ') 6308 return self.get_key_value(key) 6310 raise AttributeError 6312 ######################################### 6316 ######################################### 6317 class CheckSatResult: 6318 """Represents the result of a satisfiability check: sat, unsat, unknown.
6324 >>> isinstance(r, CheckSatResult)
6328 def __init__(self, r): 6331 def __deepcopy__(self, memo={}): 6332 return CheckSatResult(self.r) 6334 def __eq__(self, other): 6335 return isinstance(other, CheckSatResult) and self.r == other.r 6337 def __ne__(self, other): 6338 return not self.__eq__(other) 6342 if self.r == Z3_L_TRUE: 6344 elif self.r == Z3_L_FALSE: 6345 return "<b>unsat</b>" 6347 return "<b>unknown</b>" 6349 if self.r == Z3_L_TRUE: 6351 elif self.r == Z3_L_FALSE: 6356 sat = CheckSatResult(Z3_L_TRUE) 6357 unsat = CheckSatResult(Z3_L_FALSE) 6358 unknown = CheckSatResult(Z3_L_UNDEF) 6360 class Solver(Z3PPObject): 6361 """Solver API provides methods
for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.
""" 6363 def __init__(self, solver=None, ctx=None): 6364 assert solver is None or ctx is not None 6365 self.ctx = _get_ctx(ctx) 6366 self.backtrack_level = 4000000000 6369 self.solver = Z3_mk_solver(self.ctx.ref()) 6371 self.solver = solver 6372 Z3_solver_inc_ref(self.ctx.ref(), self.solver) 6375 if self.solver is not None and self.ctx.ref() is not None: 6376 Z3_solver_dec_ref(self.ctx.ref(), self.solver) 6378 def set(self, *args, **keys): 6379 """Set a configuration option. The method `
help()`
return a string containing all available options.
6383 >>> s.set(mbqi=
True)
6384 >>> s.set(
'MBQI',
True)
6385 >>> s.set(
':mbqi',
True)
6387 p = args2params(args, keys, self.ctx) 6388 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params) 6391 """Create a backtracking point.
6410 Z3_solver_push(self.ctx.ref(), self.solver) 6412 def pop(self, num=1): 6413 """Backtrack \c num backtracking points.
6432 Z3_solver_pop(self.ctx.ref(), self.solver, num) 6434 def num_scopes(self): 6435 """Return the current number of backtracking points.
6450 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver) 6453 """Remove all asserted constraints
and backtracking points created using `
push()`.
6464 Z3_solver_reset(self.ctx.ref(), self.solver) 6466 def assert_exprs(self, *args): 6467 """Assert constraints into the solver.
6471 >>> s.assert_exprs(x > 0, x < 2)
6475 args = _get_args(args) 6476 s = BoolSort(self.ctx) 6478 if isinstance(arg, Goal) or isinstance(arg, AstVector): 6480 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast()) 6483 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast()) 6485 def add(self, *args): 6486 """Assert constraints into the solver.
6490 >>> s.add(x > 0, x < 2)
6494 self.assert_exprs(*args) 6496 def __iadd__(self, fml): 6500 def append(self, *args): 6501 """Assert constraints into the solver.
6505 >>> s.append(x > 0, x < 2)
6509 self.assert_exprs(*args) 6511 def insert(self, *args): 6512 """Assert constraints into the solver.
6516 >>> s.insert(x > 0, x < 2)
6520 self.assert_exprs(*args) 6522 def assert_and_track(self, a, p): 6523 """Assert constraint `a`
and track it
in the unsat core using the Boolean constant `p`.
6525 If `p`
is a string, it will be automatically converted into a Boolean constant.
6530 >>> s.set(unsat_core=
True)
6531 >>> s.assert_and_track(x > 0,
'p1')
6532 >>> s.assert_and_track(x != 1,
'p2')
6533 >>> s.assert_and_track(x < 0, p3)
6534 >>> print(s.check())
6536 >>> c = s.unsat_core()
6546 if isinstance(p, str): 6547 p = Bool(p, self.ctx) 6548 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected") 6549 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected") 6550 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast()) 6552 def check(self, *assumptions): 6553 """Check whether the assertions
in the given solver plus the optional assumptions are consistent
or not.
6559 >>> s.add(x > 0, x < 2)
6562 >>> s.model().eval(x)
6568 >>> s.add(2**x == 4)
6572 assumptions = _get_args(assumptions) 6573 num = len(assumptions) 6574 _assumptions = (Ast * num)() 6575 for i in range(num): 6576 _assumptions[i] = assumptions[i].as_ast() 6577 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions) 6578 return CheckSatResult(r) 6581 """Return a model
for the last `
check()`.
6583 This function raises an exception
if 6584 a model
is not available (e.g., last `
check()` returned unsat).
6588 >>> s.add(a + 2 == 0)
6595 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx) 6597 raise Z3Exception("model is not available") 6599 def unsat_core(self): 6600 """Return a subset (
as an AST vector) of the assumptions provided to the last
check().
6602 These are the assumptions Z3 used
in the unsatisfiability proof.
6603 Assumptions are available
in Z3. They are used to extract unsatisfiable cores.
6604 They may be also used to
"retract" assumptions. Note that, assumptions are
not really
6605 "soft constraints", but they can be used to implement them.
6607 >>> p1, p2, p3 =
Bools(
'p1 p2 p3')
6608 >>> x, y =
Ints(
'x y')
6613 >>> s.add(
Implies(p3, y > -3))
6614 >>> s.check(p1, p2, p3)
6616 >>> core = s.unsat_core()
6629 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx) 6631 def consequences(self, assumptions, variables): 6632 """Determine fixed values
for the variables based on the solver state
and assumptions.
6634 >>> a, b, c, d =
Bools(
'a b c d')
6636 >>> s.consequences([a],[b,c,d])
6638 >>> s.consequences([
Not(c),d],[a,b,c,d])
6641 if isinstance(assumptions, list): 6642 _asms = AstVector(None, self.ctx) 6643 for a in assumptions: 6646 if isinstance(variables, list): 6647 _vars = AstVector(None, self.ctx) 6651 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected") 6652 _z3_assert(isinstance(variables, AstVector), "ast vector expected") 6653 consequences = AstVector(None, self.ctx) 6654 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector) 6655 sz = len(consequences) 6656 consequences = [ consequences[i] for i in range(sz) ] 6657 return CheckSatResult(r), consequences 6659 def from_file(self, filename): 6660 """Parse assertions
from a file
""" 6662 Z3_solver_from_file(self.ctx.ref(), self.solver, filename) 6663 except Z3Exception as e: 6664 _handle_parse_error(e, self.ctx) 6666 def from_string(self, s): 6667 """Parse assertions
from a string
""" 6669 Z3_solver_from_string(self.ctx.ref(), self.solver, s) 6670 except Z3Exception as e: 6671 _handle_parse_error(e, self.ctx) 6673 def cube(self, vars = None): 6675 The method takes an optional set of variables that restrict which
6676 variables may be used
as a starting point
for cubing.
6677 If vars
is not None, then the first case split
is based on a variable
in 6680 self.cube_vs = AstVector(None, self.ctx) 6681 if vars is not None: 6683 self.cube_vs.push(v) 6685 lvl = self.backtrack_level 6686 self.backtrack_level = 4000000000 6687 r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx) 6688 if (len(r) == 1 and is_false(r[0])): 6694 def cube_vars(self): 6695 """Access the set of variables that were touched by the most recently generated cube.
6696 This set of variables can be used
as a starting point
for additional cubes.
6697 The idea
is that variables that appear
in clauses that are reduced by the most recent
6698 cube are likely more useful to cube on.
""" 6702 """Return a proof
for the last `
check()`. Proof construction must be enabled.
""" 6703 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx) 6705 def assertions(self): 6706 """Return an AST vector containing all added constraints.
6717 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx) 6720 """Return an AST vector containing all currently inferred units.
6722 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx) 6724 def non_units(self): 6725 """Return an AST vector containing all atomic formulas
in solver state that are
not units.
6727 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx) 6729 def statistics(self): 6730 """Return statistics
for the last `
check()`.
6737 >>> st = s.statistics()
6738 >>> st.get_key_value(
'final checks')
6745 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx) 6747 def reason_unknown(self): 6748 """Return a string describing why the last `
check()` returned `unknown`.
6752 >>> s.add(2**x == 4)
6755 >>> s.reason_unknown()
6756 '(incomplete (theory arithmetic))' 6758 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver) 6761 """Display a string describing all available options.
""" 6762 print(Z3_solver_get_help(self.ctx.ref(), self.solver)) 6764 def param_descrs(self): 6765 """Return the parameter description set.
""" 6766 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx) 6769 """Return a formatted string with all added constraints.
""" 6770 return obj_to_string(self) 6772 def translate(self, target): 6773 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
6778 >>> s2 = s1.translate(c2)
6781 _z3_assert(isinstance(target, Context), "argument must be a Z3 context") 6782 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) 6783 return Solver(solver, target) 6786 return self.translate(self.ctx) 6788 def __deepcopy__(self): 6789 return self.translate(self.ctx) 6792 """Return a formatted string (
in Lisp-like format) with all added constraints. We say the string
is in s-expression format.
6800 return Z3_solver_to_string(self.ctx.ref(), self.solver) 6803 """return SMTLIB2 formatted benchmark
for solver
's assertions""" 6810 for i
in range(sz1):
6811 v[i] = es[i].as_ast()
6813 e = es[sz1].as_ast()
6819 """Create a solver customized for the given logic. 6821 The parameter `logic` is a string. It should be contains 6822 the name of a SMT-LIB logic. 6823 See http://www.smtlib.org/ for the name of all available logics. 6825 >>> s = SolverFor("QF_LIA") 6839 """Return a simple general purpose solver with limited amount of preprocessing. 6841 >>> s = SimpleSolver() 6857 """Fixedpoint API provides methods for solving with recursive predicates""" 6860 assert fixedpoint
is None or ctx
is not None 6863 if fixedpoint
is None:
6874 if self.
fixedpoint is not None and self.
ctx.ref()
is not None:
6878 """Set a configuration option. The method `help()` return a string containing all available options. 6884 """Display a string describing all available options.""" 6888 """Return the parameter description set.""" 6892 """Assert constraints as background axioms for the fixedpoint solver.""" 6893 args = _get_args(args)
6896 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
6906 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6914 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6918 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6922 """Assert rules defining recursive predicates to the fixedpoint solver. 6925 >>> s = Fixedpoint() 6926 >>> s.register_relation(a.decl()) 6927 >>> s.register_relation(b.decl()) 6940 body = _get_args(body)
6944 def rule(self, head, body = None, name = None):
6945 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 6949 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 6953 """Query the fixedpoint engine whether formula is derivable. 6954 You can also pass an tuple or list of recursive predicates. 6956 query = _get_args(query)
6958 if sz >= 1
and isinstance(query[0], FuncDeclRef):
6959 _decls = (FuncDecl * sz)()
6969 query =
And(query, self.
ctx)
6970 query = self.
abstract(query,
False)
6975 """Query the fixedpoint engine whether formula is derivable starting at the given query level. 6977 query = _get_args(query)
6979 if sz >= 1
and isinstance(query[0], FuncDecl):
6980 _z3_assert (
False,
"unsupported")
6986 query = self.
abstract(query,
False)
6987 r = Z3_fixedpoint_query_from_lvl (self.
ctx.ref(), self.
fixedpoint, query.as_ast(), lvl)
6991 """create a backtracking point for added rules, facts and assertions""" 6995 """restore to previously created backtracking point""" 7003 body = _get_args(body)
7008 """Retrieve answer from last query call.""" 7010 return _to_expr_ref(r, self.
ctx)
7013 """Retrieve a ground cex from last query call.""" 7014 r = Z3_fixedpoint_get_ground_sat_answer(self.
ctx.ref(), self.
fixedpoint)
7015 return _to_expr_ref(r, self.
ctx)
7018 """retrieve rules along the counterexample trace""" 7022 """retrieve rule names along the counterexample trace""" 7025 names = _symbol2py (self.
ctx, Z3_fixedpoint_get_rule_names_along_trace(self.
ctx.ref(), self.
fixedpoint))
7027 return names.split (
';')
7030 """Retrieve number of levels used for predicate in PDR engine""" 7034 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)""" 7036 return _to_expr_ref(r, self.
ctx)
7039 """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)""" 7043 """Register relation as recursive""" 7044 relations = _get_args(relations)
7049 """Control how relation is represented""" 7050 representations = _get_args(representations)
7051 representations = [
to_symbol(s)
for s
in representations]
7052 sz = len(representations)
7053 args = (Symbol * sz)()
7055 args[i] = representations[i]
7059 """Parse rules and queries from a string""" 7062 except Z3Exception
as e:
7063 _handle_parse_error(e, self.
ctx)
7066 """Parse rules and queries from a file""" 7069 except Z3Exception
as e:
7070 _handle_parse_error(e, self.
ctx)
7073 """retrieve rules that have been added to fixedpoint context""" 7077 """retrieve assertions that have been added to fixedpoint context""" 7081 """Return a formatted string with all added rules and constraints.""" 7085 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 7090 """Return a formatted string (in Lisp-like format) with all added constraints. 7091 We say the string is in s-expression format. 7092 Include also queries. 7094 args, len = _to_ast_array(queries)
7098 """Return statistics for the last `query()`. 7103 """Return a string describing why the last `query()` returned `unknown`. 7108 """Add variable or several variables. 7109 The added variable or variables will be bound in the rules 7112 vars = _get_args(vars)
7132 """Finite domain sort.""" 7135 """Return the size of the finite domain sort""" 7136 r = (ctypes.c_ulonglong * 1)()
7140 raise Z3Exception(
"Failed to retrieve finite domain sort size")
7143 """Create a named finite domain sort of a given size sz""" 7144 if not isinstance(name, Symbol):
7150 """Return True if `s` is a Z3 finite-domain sort. 7152 >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) 7154 >>> is_finite_domain_sort(IntSort()) 7157 return isinstance(s, FiniteDomainSortRef)
7161 """Finite-domain expressions.""" 7164 """Return the sort of the finite-domain expression `self`.""" 7168 """Return a Z3 floating point expression as a Python string.""" 7172 """Return `True` if `a` is a Z3 finite-domain expression. 7174 >>> s = FiniteDomainSort('S', 100) 7175 >>> b = Const('b', s) 7176 >>> is_finite_domain(b) 7178 >>> is_finite_domain(Int('x')) 7181 return isinstance(a, FiniteDomainRef)
7185 """Integer values.""" 7188 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. 7190 >>> s = FiniteDomainSort('S', 100) 7191 >>> v = FiniteDomainVal(3, s) 7200 """Return a Z3 finite-domain numeral as a Python string. 7202 >>> s = FiniteDomainSort('S', 100) 7203 >>> v = FiniteDomainVal(42, s) 7211 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. 7213 >>> s = FiniteDomainSort('S', 256) 7214 >>> FiniteDomainVal(255, s) 7216 >>> FiniteDomainVal('100', s) 7225 """Return `True` if `a` is a Z3 finite-domain value. 7227 >>> s = FiniteDomainSort('S', 100) 7228 >>> b = Const('b', s) 7229 >>> is_finite_domain_value(b) 7231 >>> b = FiniteDomainVal(10, s) 7234 >>> is_finite_domain_value(b) 7279 """Optimize API provides methods for solving using objective functions and weighted soft constraints""" 7290 if self.
optimize is not None and self.
ctx.ref()
is not None:
7294 """Set a configuration option. The method `help()` return a string containing all available options. 7300 """Display a string describing all available options.""" 7304 """Return the parameter description set.""" 7308 """Assert constraints as background axioms for the optimize solver.""" 7309 args = _get_args(args)
7312 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
7320 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr.""" 7328 """Add soft constraint with optional weight and optional identifier. 7329 If no weight is supplied, then the penalty for violating the soft constraint 7331 Soft constraints are grouped by identifiers. Soft constraints that are 7332 added without identifiers are grouped by default. 7335 weight =
"%d" % weight
7336 elif isinstance(weight, float):
7337 weight =
"%f" % weight
7338 if not isinstance(weight, str):
7339 raise Z3Exception(
"weight should be a string or an integer")
7347 """Add objective function to maximize.""" 7351 """Add objective function to minimize.""" 7355 """create a backtracking point for added rules, facts and assertions""" 7359 """restore to previously created backtracking point""" 7363 """Check satisfiability while optimizing objective functions.""" 7364 assumptions = _get_args(assumptions)
7365 num = len(assumptions)
7366 _assumptions = (Ast * num)()
7367 for i
in range(num):
7368 _assumptions[i] = assumptions[i].as_ast()
7372 """Return a string that describes why the last `check()` returned `unknown`.""" 7376 """Return a model for the last check().""" 7380 raise Z3Exception(
"model is not available")
7386 if not isinstance(obj, OptimizeObjective):
7387 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7391 if not isinstance(obj, OptimizeObjective):
7392 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7396 if not isinstance(obj, OptimizeObjective):
7397 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7398 return obj.lower_values()
7401 if not isinstance(obj, OptimizeObjective):
7402 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7403 return obj.upper_values()
7406 """Parse assertions and objectives from a file""" 7409 except Z3Exception
as e:
7410 _handle_parse_error(e, self.
ctx)
7413 """Parse assertions and objectives from a string""" 7416 except Z3Exception
as e:
7417 _handle_parse_error(e, self.
ctx)
7420 """Return an AST vector containing all added constraints.""" 7424 """returns set of objective functions""" 7428 """Return a formatted string with all added rules and constraints.""" 7432 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 7437 """Return statistics for the last check`. 7450 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters.""" 7461 if self.
ctx.ref()
is not None:
7465 """Return the number of subgoals in `self`. 7467 >>> a, b = Ints('a b') 7469 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7470 >>> t = Tactic('split-clause') 7474 >>> t = Then(Tactic('split-clause'), Tactic('split-clause')) 7477 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values')) 7484 """Return one of the subgoals stored in ApplyResult object `self`. 7486 >>> a, b = Ints('a b') 7488 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7489 >>> t = Tactic('split-clause') 7492 [a == 0, Or(b == 0, b == 1), a > b] 7494 [a == 1, Or(b == 0, b == 1), a > b] 7496 if idx >= len(self):
7501 return obj_to_string(self)
7504 """Return a textual representation of the s-expression representing the set of subgoals in `self`.""" 7509 """Return a Z3 expression consisting of all subgoals. 7514 >>> g.add(Or(x == 2, x == 3)) 7515 >>> r = Tactic('simplify')(g) 7517 [[Not(x <= 1), Or(x == 2, x == 3)]] 7519 And(Not(x <= 1), Or(x == 2, x == 3)) 7520 >>> r = Tactic('split-clause')(g) 7522 [[x > 1, x == 2], [x > 1, x == 3]] 7524 Or(And(x > 1, x == 2), And(x > 1, x == 3)) 7540 """Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver(). 7542 Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond(). 7547 if isinstance(tactic, TacticObj):
7551 _z3_assert(isinstance(tactic, str),
"tactic name expected")
7555 raise Z3Exception(
"unknown tactic '%s'" % tactic)
7562 if self.
tactic is not None and self.
ctx.ref()
is not None:
7566 """Create a solver using the tactic `self`. 7568 The solver supports the methods `push()` and `pop()`, but it 7569 will always solve each `check()` from scratch. 7571 >>> t = Then('simplify', 'nlsat') 7574 >>> s.add(x**2 == 2, x > 0) 7582 def apply(self, goal, *arguments, **keywords):
7583 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7585 >>> x, y = Ints('x y') 7586 >>> t = Tactic('solve-eqs') 7587 >>> t.apply(And(x == 0, y >= x + 1)) 7591 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expressions expected")
7592 goal = _to_goal(goal)
7593 if len(arguments) > 0
or len(keywords) > 0:
7600 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7602 >>> x, y = Ints('x y') 7603 >>> t = Tactic('solve-eqs') 7604 >>> t(And(x == 0, y >= x + 1)) 7607 return self.
apply(goal, *arguments, **keywords)
7610 """Display a string containing a description of the available options for the `self` tactic.""" 7614 """Return the parameter description set.""" 7618 if isinstance(a, BoolRef):
7619 goal =
Goal(ctx = a.ctx)
7625 def _to_tactic(t, ctx=None):
7626 if isinstance(t, Tactic):
7631 def _and_then(t1, t2, ctx=None):
7632 t1 = _to_tactic(t1, ctx)
7633 t2 = _to_tactic(t2, ctx)
7635 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7638 def _or_else(t1, t2, ctx=None):
7639 t1 = _to_tactic(t1, ctx)
7640 t2 = _to_tactic(t2, ctx)
7642 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7646 """Return a tactic that applies the tactics in `*ts` in sequence. 7648 >>> x, y = Ints('x y') 7649 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) 7650 >>> t(And(x == 0, y > x + 1)) 7652 >>> t(And(x == 0, y > x + 1)).as_expr() 7656 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7657 ctx = ks.get(
'ctx',
None)
7660 for i
in range(num - 1):
7661 r = _and_then(r, ts[i+1], ctx)
7665 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). 7667 >>> x, y = Ints('x y') 7668 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) 7669 >>> t(And(x == 0, y > x + 1)) 7671 >>> t(And(x == 0, y > x + 1)).as_expr() 7677 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). 7680 >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) 7681 >>> # Tactic split-clause fails if there is no clause in the given goal. 7684 >>> t(Or(x == 0, x == 1)) 7685 [[x == 0], [x == 1]] 7688 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7689 ctx = ks.get(
'ctx',
None)
7692 for i
in range(num - 1):
7693 r = _or_else(r, ts[i+1], ctx)
7697 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). 7700 >>> t = ParOr(Tactic('simplify'), Tactic('fail')) 7705 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7706 ctx = _get_ctx(ks.get(
'ctx',
None))
7707 ts = [ _to_tactic(t, ctx)
for t
in ts ]
7709 _args = (TacticObj * sz)()
7711 _args[i] = ts[i].tactic
7715 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. 7717 >>> x, y = Ints('x y') 7718 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) 7719 >>> t(And(Or(x == 1, x == 2), y == x + 1)) 7720 [[x == 1, y == 2], [x == 2, y == 3]] 7722 t1 = _to_tactic(t1, ctx)
7723 t2 = _to_tactic(t2, ctx)
7725 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7729 """Alias for ParThen(t1, t2, ctx).""" 7733 """Return a tactic that applies tactic `t` using the given configuration options. 7735 >>> x, y = Ints('x y') 7736 >>> t = With(Tactic('simplify'), som=True) 7737 >>> t((x + 1)*(y + 2) == 0) 7738 [[2*x + y + x*y == -2]] 7740 ctx = keys.pop(
'ctx',
None)
7741 t = _to_tactic(t, ctx)
7746 """Return a tactic that applies tactic `t` using the given configuration options. 7748 >>> x, y = Ints('x y') 7750 >>> p.set("som", True) 7751 >>> t = WithParams(Tactic('simplify'), p) 7752 >>> t((x + 1)*(y + 2) == 0) 7753 [[2*x + y + x*y == -2]] 7755 t = _to_tactic(t,
None)
7759 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. 7761 >>> x, y = Ints('x y') 7762 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) 7763 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) 7765 >>> for subgoal in r: print(subgoal) 7766 [x == 0, y == 0, x > y] 7767 [x == 0, y == 1, x > y] 7768 [x == 1, y == 0, x > y] 7769 [x == 1, y == 1, x > y] 7770 >>> t = Then(t, Tactic('propagate-values')) 7774 t = _to_tactic(t, ctx)
7778 """Return a tactic that applies `t` to a given goal for `ms` milliseconds. 7780 If `t` does not terminate in `ms` milliseconds, then it fails. 7782 t = _to_tactic(t, ctx)
7786 """Return a list of all available tactics in Z3. 7789 >>> l.count('simplify') == 1 7796 """Return a short description for the tactic named `name`. 7798 >>> d = tactic_description('simplify') 7804 """Display a (tabular) description of all available tactics in Z3.""" 7807 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7810 print(
'<tr style="background-color:#CFCFCF">')
7815 print(
'<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(
tactic_description(t), 40)))
7822 """Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used.""" 7826 if isinstance(probe, ProbeObj):
7828 elif isinstance(probe, float):
7830 elif _is_int(probe):
7832 elif isinstance(probe, bool):
7839 _z3_assert(isinstance(probe, str),
"probe name expected")
7843 raise Z3Exception(
"unknown probe '%s'" % probe)
7850 if self.
probe is not None and self.
ctx.ref()
is not None:
7854 """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`. 7856 >>> p = Probe('size') < 10 7867 """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`. 7869 >>> p = Probe('size') > 10 7880 """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`. 7882 >>> p = Probe('size') <= 2 7893 """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`. 7895 >>> p = Probe('size') >= 2 7906 """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`. 7908 >>> p = Probe('size') == 2 7919 """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`. 7921 >>> p = Probe('size') != 2 7933 """Evaluate the probe `self` in the given goal. 7935 >>> p = Probe('size') 7945 >>> p = Probe('num-consts') 7948 >>> p = Probe('is-propositional') 7951 >>> p = Probe('is-qflia') 7956 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expression expected")
7957 goal = _to_goal(goal)
7961 """Return `True` if `p` is a Z3 probe. 7963 >>> is_probe(Int('x')) 7965 >>> is_probe(Probe('memory')) 7968 return isinstance(p, Probe)
7970 def _to_probe(p, ctx=None):
7974 return Probe(p, ctx)
7977 """Return a list of all available probes in Z3. 7980 >>> l.count('memory') == 1 7987 """Return a short description for the probe named `name`. 7989 >>> d = probe_description('memory') 7995 """Display a (tabular) description of all available probes in Z3.""" 7998 print(
'<table border="1" cellpadding="2" cellspacing="0">')
8001 print(
'<tr style="background-color:#CFCFCF">')
8006 print(
'<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(
probe_description(p), 40)))
8012 def _probe_nary(f, args, ctx):
8014 _z3_assert(len(args) > 0,
"At least one argument expected")
8016 r = _to_probe(args[0], ctx)
8017 for i
in range(num - 1):
8018 r =
Probe(f(ctx.ref(), r.probe, _to_probe(args[i+1], ctx).probe), ctx)
8021 def _probe_and(args, ctx):
8022 return _probe_nary(Z3_probe_and, args, ctx)
8024 def _probe_or(args, ctx):
8025 return _probe_nary(Z3_probe_or, args, ctx)
8028 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 8030 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. 8032 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) 8033 >>> x, y = Ints('x y') 8039 >>> g.add(x == y + 1) 8041 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 8043 p = _to_probe(p, ctx)
8047 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 8049 >>> t = When(Probe('size') > 2, Tactic('simplify')) 8050 >>> x, y = Ints('x y') 8056 >>> g.add(x == y + 1) 8058 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 8060 p = _to_probe(p, ctx)
8061 t = _to_tactic(t, ctx)
8065 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. 8067 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt')) 8069 p = _to_probe(p, ctx)
8070 t1 = _to_tactic(t1, ctx)
8071 t2 = _to_tactic(t2, ctx)
8081 """Simplify the expression `a` using the given options. 8083 This function has many options. Use `help_simplify` to obtain the complete list. 8087 >>> simplify(x + 1 + y + x + 1) 8089 >>> simplify((x + 1)*(y + 1), som=True) 8091 >>> simplify(Distinct(x, y, 1), blast_distinct=True) 8092 And(Not(x == y), Not(x == 1), Not(y == 1)) 8093 >>> simplify(And(x == 0, y == 1), elim_and=True) 8094 Not(Or(Not(x == 0), Not(y == 1))) 8097 _z3_assert(
is_expr(a),
"Z3 expression expected")
8098 if len(arguments) > 0
or len(keywords) > 0:
8100 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
8102 return _to_expr_ref(
Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
8105 """Return a string describing all options available for Z3 `simplify` procedure.""" 8109 """Return the set of parameter descriptions for Z3 `simplify` procedure.""" 8113 """Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to. 8117 >>> substitute(x + 1, (x, y + 1)) 8119 >>> f = Function('f', IntSort(), IntSort()) 8120 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 8123 if isinstance(m, tuple):
8125 if isinstance(m1, list)
and all(isinstance(p, tuple)
for p
in m1):
8128 _z3_assert(
is_expr(t),
"Z3 expression expected")
8129 _z3_assert(all([isinstance(p, tuple)
and is_expr(p[0])
and is_expr(p[1])
and p[0].sort().
eq(p[1].sort())
for p
in m]),
"Z3 invalid substitution, expression pairs expected.")
8131 _from = (Ast * num)()
8133 for i
in range(num):
8134 _from[i] = m[i][0].as_ast()
8135 _to[i] = m[i][1].as_ast()
8136 return _to_expr_ref(
Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
8139 """Substitute the free variables in t with the expression in m. 8141 >>> v0 = Var(0, IntSort()) 8142 >>> v1 = Var(1, IntSort()) 8144 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 8145 >>> # replace v0 with x+1 and v1 with x 8146 >>> substitute_vars(f(v0, v1), x + 1, x) 8150 _z3_assert(
is_expr(t),
"Z3 expression expected")
8151 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
8154 for i
in range(num):
8155 _to[i] = m[i].as_ast()
8159 """Create the sum of the Z3 expressions. 8161 >>> a, b, c = Ints('a b c') 8166 >>> A = IntVector('a', 5) 8168 a__0 + a__1 + a__2 + a__3 + a__4 8170 args = _get_args(args)
8173 ctx = _ctx_from_ast_arg_list(args)
8175 return _reduce(
lambda a, b: a + b, args, 0)
8176 args = _coerce_expr_list(args, ctx)
8178 return _reduce(
lambda a, b: a + b, args, 0)
8180 _args, sz = _to_ast_array(args)
8185 """Create the product of the Z3 expressions. 8187 >>> a, b, c = Ints('a b c') 8188 >>> Product(a, b, c) 8190 >>> Product([a, b, c]) 8192 >>> A = IntVector('a', 5) 8194 a__0*a__1*a__2*a__3*a__4 8196 args = _get_args(args)
8199 ctx = _ctx_from_ast_arg_list(args)
8201 return _reduce(
lambda a, b: a * b, args, 1)
8202 args = _coerce_expr_list(args, ctx)
8204 return _reduce(
lambda a, b: a * b, args, 1)
8206 _args, sz = _to_ast_array(args)
8210 """Create an at-most Pseudo-Boolean k constraint. 8212 >>> a, b, c = Bools('a b c') 8213 >>> f = AtMost(a, b, c, 2) 8215 args = _get_args(args)
8217 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8218 ctx = _ctx_from_ast_arg_list(args)
8220 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8221 args1 = _coerce_expr_list(args[:-1], ctx)
8223 _args, sz = _to_ast_array(args1)
8227 """Create an at-most Pseudo-Boolean k constraint. 8229 >>> a, b, c = Bools('a b c') 8230 >>> f = AtLeast(a, b, c, 2) 8232 args = _get_args(args)
8234 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8235 ctx = _ctx_from_ast_arg_list(args)
8237 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8238 args1 = _coerce_expr_list(args[:-1], ctx)
8240 _args, sz = _to_ast_array(args1)
8244 def _pb_args_coeffs(args, default_ctx = None):
8245 args = _get_args_ast_list(args)
8247 return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
8248 args, coeffs = zip(*args)
8250 _z3_assert(len(args) > 0,
"Non empty list of arguments expected")
8251 ctx = _ctx_from_ast_arg_list(args)
8253 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8254 args = _coerce_expr_list(args, ctx)
8255 _args, sz = _to_ast_array(args)
8256 _coeffs = (ctypes.c_int * len(coeffs))()
8257 for i
in range(len(coeffs)):
8258 _z3_check_cint_overflow(coeffs[i],
"coefficient")
8259 _coeffs[i] = coeffs[i]
8260 return ctx, sz, _args, _coeffs
8263 """Create a Pseudo-Boolean inequality k constraint. 8265 >>> a, b, c = Bools('a b c') 8266 >>> f = PbLe(((a,1),(b,3),(c,2)), 3) 8268 _z3_check_cint_overflow(k,
"k")
8269 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8273 """Create a Pseudo-Boolean inequality k constraint. 8275 >>> a, b, c = Bools('a b c') 8276 >>> f = PbGe(((a,1),(b,3),(c,2)), 3) 8278 _z3_check_cint_overflow(k,
"k")
8279 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8283 """Create a Pseudo-Boolean inequality k constraint. 8285 >>> a, b, c = Bools('a b c') 8286 >>> f = PbEq(((a,1),(b,3),(c,2)), 3) 8288 _z3_check_cint_overflow(k,
"k")
8289 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8294 """Solve the constraints `*args`. 8296 This is a simple function for creating demonstrations. It creates a solver, 8297 configure it using the options in `keywords`, adds the constraints 8298 in `args`, and invokes check. 8301 >>> solve(a > 0, a < 2) 8307 if keywords.get(
'show',
False):
8311 print(
"no solution")
8313 print(
"failed to solve")
8322 """Solve the constraints `*args` using solver `s`. 8324 This is a simple function for creating demonstrations. It is similar to `solve`, 8325 but it uses the given solver `s`. 8326 It configures solver `s` using the options in `keywords`, adds the constraints 8327 in `args`, and invokes check. 8330 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8333 if keywords.get(
'show',
False):
8338 print(
"no solution")
8340 print(
"failed to solve")
8346 if keywords.get(
'show',
False):
8351 """Try to prove the given claim. 8353 This is a simple function for creating demonstrations. It tries to prove 8354 `claim` by showing the negation is unsatisfiable. 8356 >>> p, q = Bools('p q') 8357 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) 8361 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8365 if keywords.get(
'show',
False):
8371 print(
"failed to prove")
8374 print(
"counterexample")
8377 def _solve_html(*args, **keywords):
8378 """Version of function `solve` used in RiSE4Fun.""" 8382 if keywords.get(
'show',
False):
8383 print(
"<b>Problem:</b>")
8387 print(
"<b>no solution</b>")
8389 print(
"<b>failed to solve</b>")
8395 if keywords.get(
'show',
False):
8396 print(
"<b>Solution:</b>")
8399 def _solve_using_html(s, *args, **keywords):
8400 """Version of function `solve_using` used in RiSE4Fun.""" 8402 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8405 if keywords.get(
'show',
False):
8406 print(
"<b>Problem:</b>")
8410 print(
"<b>no solution</b>")
8412 print(
"<b>failed to solve</b>")
8418 if keywords.get(
'show',
False):
8419 print(
"<b>Solution:</b>")
8422 def _prove_html(claim, **keywords):
8423 """Version of function `prove` used in RiSE4Fun.""" 8425 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8429 if keywords.get(
'show',
False):
8433 print(
"<b>proved</b>")
8435 print(
"<b>failed to prove</b>")
8438 print(
"<b>counterexample</b>")
8441 def _dict2sarray(sorts, ctx):
8443 _names = (Symbol * sz)()
8444 _sorts = (Sort * sz) ()
8449 _z3_assert(isinstance(k, str),
"String expected")
8450 _z3_assert(
is_sort(v),
"Z3 sort expected")
8454 return sz, _names, _sorts
8456 def _dict2darray(decls, ctx):
8458 _names = (Symbol * sz)()
8459 _decls = (FuncDecl * sz) ()
8464 _z3_assert(isinstance(k, str),
"String expected")
8468 _decls[i] = v.decl().ast
8472 return sz, _names, _decls
8476 """Parse a string in SMT 2.0 format using the given sorts and decls. 8478 The arguments sorts and decls are Python dictionaries used to initialize 8479 the symbol table used for the SMT 2.0 parser. 8481 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') 8483 >>> x, y = Ints('x y') 8484 >>> f = Function('f', IntSort(), IntSort()) 8485 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) 8487 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) 8491 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 8492 dsz, dnames, ddecls = _dict2darray(decls, ctx) 8493 return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 8495 def parse_smt2_file(f, sorts={}, decls={}, ctx=None): 8496 """Parse a file
in SMT 2.0 format using the given sorts
and decls.
8501 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 8502 dsz, dnames, ddecls = _dict2darray(decls, ctx) 8503 return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 8506 ######################################### 8508 # Floating-Point Arithmetic 8510 ######################################### 8513 # Global default rounding mode 8514 _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO 8515 _dflt_fpsort_ebits = 11 8516 _dflt_fpsort_sbits = 53 8518 def get_default_rounding_mode(ctx=None): 8519 """Retrieves the
global default rounding mode.
""" 8520 global _dflt_rounding_mode 8521 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO: 8523 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE: 8525 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE: 8527 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: 8529 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: 8532 def set_default_rounding_mode(rm, ctx=None): 8533 global _dflt_rounding_mode 8534 if is_fprm_value(rm): 8535 _dflt_rounding_mode = rm.decl().kind() 8537 _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO or 8538 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE or 8539 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE or 8540 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN or 8541 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, 8542 "illegal rounding mode") 8543 _dflt_rounding_mode = rm 8545 def get_default_fp_sort(ctx=None): 8546 return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx) 8548 def set_default_fp_sort(ebits, sbits, ctx=None): 8549 global _dflt_fpsort_ebits 8550 global _dflt_fpsort_sbits 8551 _dflt_fpsort_ebits = ebits 8552 _dflt_fpsort_sbits = sbits 8554 def _dflt_rm(ctx=None): 8555 return get_default_rounding_mode(ctx) 8557 def _dflt_fps(ctx=None): 8558 return get_default_fp_sort(ctx) 8560 def _coerce_fp_expr_list(alist, ctx): 8561 first_fp_sort = None 8564 if first_fp_sort is None: 8565 first_fp_sort = a.sort() 8566 elif first_fp_sort == a.sort(): 8567 pass # OK, same as before 8569 # we saw at least 2 different float sorts; something will 8570 # throw a sort mismatch later, for now assume None. 8571 first_fp_sort = None 8575 for i in range(len(alist)): 8577 if (isinstance(a, str) and a.contains('2**(') and a.endswith(')')) or _is_int(a) or isinstance(a, float) or isinstance(a, bool): 8578 r.append(FPVal(a, None, first_fp_sort, ctx)) 8581 return _coerce_expr_list(r, ctx) 8586 class FPSortRef(SortRef): 8587 """Floating-point sort.
""" 8590 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint sort `self`.
8595 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast)) 8598 """Retrieves the number of bits reserved
for the significand
in the FloatingPoint sort `self`.
8603 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast)) 8605 def cast(self, val): 8606 """Try to cast `val`
as a floating-point expression.
8610 >>> b.cast(1.0).
sexpr()
8611 '(fp #b0 #x7f #b00000000000000000000000)' 8615 _z3_assert(self.ctx == val.ctx, "Context mismatch") 8618 return FPVal(val, None, self, self.ctx) 8621 def Float16(ctx=None): 8622 """Floating-point 16-bit (half) sort.
""" 8624 return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx) 8626 def FloatHalf(ctx=None): 8627 """Floating-point 16-bit (half) sort.
""" 8629 return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx) 8631 def Float32(ctx=None): 8632 """Floating-point 32-bit (single) sort.
""" 8634 return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx) 8636 def FloatSingle(ctx=None): 8637 """Floating-point 32-bit (single) sort.
""" 8639 return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx) 8641 def Float64(ctx=None): 8642 """Floating-point 64-bit (double) sort.
""" 8644 return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx) 8646 def FloatDouble(ctx=None): 8647 """Floating-point 64-bit (double) sort.
""" 8649 return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx) 8651 def Float128(ctx=None): 8652 """Floating-point 128-bit (quadruple) sort.
""" 8654 return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx) 8656 def FloatQuadruple(ctx=None): 8657 """Floating-point 128-bit (quadruple) sort.
""" 8659 return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx) 8661 class FPRMSortRef(SortRef): 8662 """"Floating-point rounding mode sort.""" 8666 """Return True if `s` is a Z3 floating-point sort.
8673 return isinstance(s, FPSortRef) 8675 def is_fprm_sort(s): 8676 """Return
True if `s`
is a Z3 floating-point rounding mode sort.
8683 return isinstance(s, FPRMSortRef) 8687 class FPRef(ExprRef): 8688 """Floating-point expressions.
""" 8691 """Return the sort of the floating-point expression `self`.
8696 >>> x.sort() ==
FPSort(8, 24)
8699 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 8702 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8707 return self.sort().ebits(); 8710 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8715 return self.sort().sbits(); 8717 def as_string(self): 8718 """Return a Z3 floating point expression
as a Python string.
""" 8719 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8721 def __le__(self, other): 8722 return fpLEQ(self, other, self.ctx) 8724 def __lt__(self, other): 8725 return fpLT(self, other, self.ctx) 8727 def __ge__(self, other): 8728 return fpGEQ(self, other, self.ctx) 8730 def __gt__(self, other): 8731 return fpGT(self, other, self.ctx) 8733 def __add__(self, other): 8734 """Create the Z3 expression `self + other`.
8743 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8744 return fpAdd(_dflt_rm(), a, b, self.ctx) 8746 def __radd__(self, other): 8747 """Create the Z3 expression `other + self`.
8753 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8754 return fpAdd(_dflt_rm(), a, b, self.ctx) 8756 def __sub__(self, other): 8757 """Create the Z3 expression `self - other`.
8766 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8767 return fpSub(_dflt_rm(), a, b, self.ctx) 8769 def __rsub__(self, other): 8770 """Create the Z3 expression `other - self`.
8776 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8777 return fpSub(_dflt_rm(), a, b, self.ctx) 8779 def __mul__(self, other): 8780 """Create the Z3 expression `self * other`.
8791 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8792 return fpMul(_dflt_rm(), a, b, self.ctx) 8794 def __rmul__(self, other): 8795 """Create the Z3 expression `other * self`.
8804 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8805 return fpMul(_dflt_rm(), a, b, self.ctx) 8808 """Create the Z3 expression `+self`.
""" 8812 """Create the Z3 expression `-self`.
8820 def __div__(self, other): 8821 """Create the Z3 expression `self / other`.
8832 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8833 return fpDiv(_dflt_rm(), a, b, self.ctx) 8835 def __rdiv__(self, other): 8836 """Create the Z3 expression `other / self`.
8845 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8846 return fpDiv(_dflt_rm(), a, b, self.ctx) 8848 if not sys.version < '3': 8849 def __truediv__(self, other): 8850 """Create the Z3 expression division `self / other`.
""" 8851 return self.__div__(other) 8853 def __rtruediv__(self, other): 8854 """Create the Z3 expression division `other / self`.
""" 8855 return self.__rdiv__(other) 8857 def __mod__(self, other): 8858 """Create the Z3 expression mod `self % other`.
""" 8859 return fpRem(self, other) 8861 def __rmod__(self, other): 8862 """Create the Z3 expression mod `other % self`.
""" 8863 return fpRem(other, self) 8865 class FPRMRef(ExprRef): 8866 """Floating-point rounding mode expressions
""" 8868 def as_string(self): 8869 """Return a Z3 floating point expression
as a Python string.
""" 8870 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8873 def RoundNearestTiesToEven(ctx=None): 8875 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8879 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8881 def RoundNearestTiesToAway(ctx=None): 8883 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8887 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8889 def RoundTowardPositive(ctx=None): 8891 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8895 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8897 def RoundTowardNegative(ctx=None): 8899 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8903 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8905 def RoundTowardZero(ctx=None): 8907 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8911 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8914 """Return `
True`
if `a`
is a Z3 floating-point rounding mode expression.
8923 return isinstance(a, FPRMRef) 8925 def is_fprm_value(a): 8926 """Return `
True`
if `a`
is a Z3 floating-point rounding mode numeral value.
""" 8927 return is_fprm(a) and _is_numeral(a.ctx, a.ast) 8931 class FPNumRef(FPRef): 8932 """The sign of the numeral.
8942 l = (ctypes.c_int)() 8943 if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False: 8944 raise Z3Exception("error retrieving the sign of a numeral.") 8947 """The sign of a floating-point numeral
as a bit-vector expression.
8949 Remark: NaN
's are invalid arguments. 8951 def sign_as_bv(self): 8952 return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx) 8954 """The significand of the numeral.
8960 def significand(self): 8961 return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast()) 8963 """The significand of the numeral
as a long.
8966 >>> x.significand_as_long()
8969 def significand_as_long(self): 8970 ptr = (ctypes.c_ulonglong * 1)() 8971 if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr): 8972 raise Z3Exception("error retrieving the significand of a numeral.") 8975 """The significand of the numeral
as a bit-vector expression.
8977 Remark: NaN are invalid arguments.
8979 def significand_as_bv(self): 8980 return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx) 8982 """The exponent of the numeral.
8988 def exponent(self, biased=True): 8989 return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased) 8991 """The exponent of the numeral
as a long.
8994 >>> x.exponent_as_long()
8997 def exponent_as_long(self, biased=True): 8998 ptr = (ctypes.c_longlong * 1)() 8999 if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased): 9000 raise Z3Exception("error retrieving the exponent of a numeral.") 9003 """The exponent of the numeral
as a bit-vector expression.
9005 Remark: NaNs are invalid arguments.
9007 def exponent_as_bv(self, biased=True): 9008 return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx) 9010 """Indicates whether the numeral
is a NaN.
""" 9012 return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast()) 9014 """Indicates whether the numeral
is +oo
or -oo.
""" 9016 return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast()) 9018 """Indicates whether the numeral
is +zero
or -zero.
""" 9020 return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast()) 9022 """Indicates whether the numeral
is normal.
""" 9024 return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast()) 9026 """Indicates whether the numeral
is subnormal.
""" 9027 def isSubnormal(self): 9028 return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast()) 9030 """Indicates whether the numeral
is positive.
""" 9031 def isPositive(self): 9032 return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast()) 9034 """Indicates whether the numeral
is negative.
""" 9035 def isNegative(self): 9036 return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast()) 9039 The string representation of the numeral.
9045 def as_string(self): 9046 s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast()) 9047 return ("FPVal(%s, %s)" % (s, self.sort())) 9050 """Return `
True`
if `a`
is a Z3 floating-point expression.
9060 return isinstance(a, FPRef) 9063 """Return `
True`
if `a`
is a Z3 floating-point numeral value.
9074 return is_fp(a) and _is_numeral(a.ctx, a.ast) 9076 def FPSort(ebits, sbits, ctx=None): 9077 """Return a Z3 floating-point sort of the given sizes. If `ctx=
None`, then the
global context
is used.
9079 >>> Single =
FPSort(8, 24)
9080 >>> Double =
FPSort(11, 53)
9083 >>> x =
Const(
'x', Single)
9088 return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx) 9090 def _to_float_str(val, exp=0): 9091 if isinstance(val, float): 9095 sone = math.copysign(1.0, val) 9100 elif val == float("+inf"): 9102 elif val == float("-inf"): 9105 v = val.as_integer_ratio() 9108 rvs = str(num) + '/' + str(den) 9109 res = rvs + 'p' + _to_int_str(exp) 9110 elif isinstance(val, bool): 9117 elif isinstance(val, str): 9118 inx = val.find('*(2**') 9121 elif val[-1] == ')': 9123 exp = str(int(val[inx+5:-1]) + int(exp)) 9125 _z3_assert(False, "String does not have floating-point numeral form.") 9127 _z3_assert(False, "Python value cannot be used to create floating-point numerals.") 9131 return res + 'p' + exp 9135 """Create a Z3 floating-point NaN term.
9138 >>> set_fpa_pretty(
True)
9141 >>> pb = get_fpa_pretty()
9142 >>> set_fpa_pretty(
False)
9145 >>> set_fpa_pretty(pb)
9147 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9148 return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx) 9150 def fpPlusInfinity(s): 9151 """Create a Z3 floating-point +oo term.
9154 >>> pb = get_fpa_pretty()
9155 >>> set_fpa_pretty(
True)
9158 >>> set_fpa_pretty(
False)
9161 >>> set_fpa_pretty(pb)
9163 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9164 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx) 9166 def fpMinusInfinity(s): 9167 """Create a Z3 floating-point -oo term.
""" 9168 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9169 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx) 9171 def fpInfinity(s, negative): 9172 """Create a Z3 floating-point +oo
or -oo term.
""" 9173 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9174 _z3_assert(isinstance(negative, bool), "expected Boolean flag") 9175 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx) 9178 """Create a Z3 floating-point +0.0 term.
""" 9179 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9180 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx) 9183 """Create a Z3 floating-point -0.0 term.
""" 9184 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9185 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx) 9187 def fpZero(s, negative): 9188 """Create a Z3 floating-point +0.0
or -0.0 term.
""" 9189 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9190 _z3_assert(isinstance(negative, bool), "expected Boolean flag") 9191 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx) 9193 def FPVal(sig, exp=None, fps=None, ctx=None): 9194 """Return a floating-point value of value `val`
and sort `fps`. If `ctx=
None`, then the
global context
is used.
9199 >>> print(
"0x%.8x" % v.exponent_as_long(
False))
9219 fps = _dflt_fps(ctx) 9220 _z3_assert(is_fp_sort(fps), "sort mismatch") 9223 val = _to_float_str(sig) 9224 if val == "NaN" or val == "nan": 9227 return fpMinusZero(fps) 9228 elif val == "0.0" or val == "+0.0": 9229 return fpPlusZero(fps) 9230 elif val == "+oo" or val == "+inf" or val == "+Inf": 9231 return fpPlusInfinity(fps) 9232 elif val == "-oo" or val == "-inf" or val == "-Inf": 9233 return fpMinusInfinity(fps) 9235 return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx) 9237 def FP(name, fpsort, ctx=None): 9238 """Return a floating-point constant named `name`.
9239 `fpsort`
is the floating-point sort.
9240 If `ctx=
None`, then the
global context
is used.
9250 >>> x2 =
FP(
'x', word)
9254 if isinstance(fpsort, FPSortRef) and ctx is None: 9258 return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx) 9260 def FPs(names, fpsort, ctx=None): 9261 """Return an array of floating-point constants.
9263 >>> x, y, z =
FPs(
'x y z',
FPSort(8, 24))
9274 if isinstance(names, str): 9275 names = names.split(" ") 9276 return [FP(name, fpsort, ctx) for name in names] 9278 def fpAbs(a, ctx=None): 9279 """Create a Z3 floating-point absolute value expression.
9283 >>> x =
FPVal(1.0, s)
9286 >>> y =
FPVal(-20.0, s)
9291 >>>
fpAbs(-1.25*(2**4))
9297 [a] = _coerce_fp_expr_list([a], ctx) 9298 return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx) 9300 def fpNeg(a, ctx=None): 9301 """Create a Z3 floating-point addition expression.
9312 [a] = _coerce_fp_expr_list([a], ctx) 9313 return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx) 9315 def _mk_fp_unary(f, rm, a, ctx): 9317 [a] = _coerce_fp_expr_list([a], ctx) 9319 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9320 _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression") 9321 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx) 9323 def _mk_fp_unary_norm(f, a, ctx): 9325 [a] = _coerce_fp_expr_list([a], ctx) 9327 _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression") 9328 return FPRef(f(ctx.ref(), a.as_ast()), ctx) 9330 def _mk_fp_unary_pred(f, a, ctx): 9332 [a] = _coerce_fp_expr_list([a], ctx) 9334 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9335 return BoolRef(f(ctx.ref(), a.as_ast()), ctx) 9337 def _mk_fp_bin(f, rm, a, b, ctx): 9339 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9341 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9342 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9343 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx) 9345 def _mk_fp_bin_norm(f, a, b, ctx): 9347 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9349 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression") 9350 return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 9352 def _mk_fp_bin_pred(f, a, b, ctx): 9354 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9356 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9357 return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 9359 def _mk_fp_tern(f, rm, a, b, c, ctx): 9361 [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx) 9363 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9364 _z3_assert(is_fp(a) or is_fp(b) or is_fp(c), "At least one of the arguments must be a Z3 floating-point expression") 9365 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx) 9367 def fpAdd(rm, a, b, ctx=None): 9368 """Create a Z3 floating-point addition expression.
9378 >>>
fpAdd(rm, x, y).sort()
9381 return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx) 9383 def fpSub(rm, a, b, ctx=None): 9384 """Create a Z3 floating-point subtraction expression.
9392 >>>
fpSub(rm, x, y).sort()
9395 return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx) 9397 def fpMul(rm, a, b, ctx=None): 9398 """Create a Z3 floating-point multiplication expression.
9406 >>>
fpMul(rm, x, y).sort()
9409 return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx) 9411 def fpDiv(rm, a, b, ctx=None): 9412 """Create a Z3 floating-point division expression.
9420 >>>
fpDiv(rm, x, y).sort()
9423 return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx) 9425 def fpRem(a, b, ctx=None): 9426 """Create a Z3 floating-point remainder expression.
9433 >>>
fpRem(x, y).sort()
9436 return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx) 9438 def fpMin(a, b, ctx=None): 9439 """Create a Z3 floating-point minimum expression.
9447 >>>
fpMin(x, y).sort()
9450 return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx) 9452 def fpMax(a, b, ctx=None): 9453 """Create a Z3 floating-point maximum expression.
9461 >>>
fpMax(x, y).sort()
9464 return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx) 9466 def fpFMA(rm, a, b, c, ctx=None): 9467 """Create a Z3 floating-point fused multiply-add expression.
9469 return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx) 9471 def fpSqrt(rm, a, ctx=None): 9472 """Create a Z3 floating-point square root expression.
9474 return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx) 9476 def fpRoundToIntegral(rm, a, ctx=None): 9477 """Create a Z3 floating-point roundToIntegral expression.
9479 return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx) 9481 def fpIsNaN(a, ctx=None): 9482 """Create a Z3 floating-point isNaN expression.
9490 return _mk_fp_unary_norm(Z3_mk_fpa_is_nan, a, ctx) 9492 def fpIsInf(a, ctx=None): 9493 """Create a Z3 floating-point isInfinite expression.
9500 return _mk_fp_unary_norm(Z3_mk_fpa_is_infinite, a, ctx) 9502 def fpIsZero(a, ctx=None): 9503 """Create a Z3 floating-point isZero expression.
9505 return _mk_fp_unary_norm(Z3_mk_fpa_is_zero, a, ctx) 9507 def fpIsNormal(a, ctx=None): 9508 """Create a Z3 floating-point isNormal expression.
9510 return _mk_fp_unary_norm(Z3_mk_fpa_is_normal, a, ctx) 9512 def fpIsSubnormal(a, ctx=None): 9513 """Create a Z3 floating-point isSubnormal expression.
9515 return _mk_fp_unary_norm(Z3_mk_fpa_is_subnormal, a, ctx) 9517 def fpIsNegative(a, ctx=None): 9518 """Create a Z3 floating-point isNegative expression.
9520 return _mk_fp_unary_norm(Z3_mk_fpa_is_negative, a, ctx) 9522 def fpIsPositive(a, ctx=None): 9523 """Create a Z3 floating-point isPositive expression.
9525 return _mk_fp_unary_norm(Z3_mk_fpa_is_positive, a, ctx) 9526 return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) 9528 def _check_fp_args(a, b): 9530 _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") 9532 def fpLT(a, b, ctx=None): 9533 """Create the Z3 floating-point expression `other < self`.
9541 return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx) 9543 def fpLEQ(a, b, ctx=None): 9544 """Create the Z3 floating-point expression `other <= self`.
9549 >>> (x <= y).sexpr()
9552 return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx) 9554 def fpGT(a, b, ctx=None): 9555 """Create the Z3 floating-point expression `other > self`.
9563 return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx) 9565 def fpGEQ(a, b, ctx=None): 9566 """Create the Z3 floating-point expression `other >= self`.
9571 >>> (x >= y).sexpr()
9574 return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx) 9576 def fpEQ(a, b, ctx=None): 9577 """Create the Z3 floating-point expression `
fpEQ(other, self)`.
9582 >>>
fpEQ(x, y).sexpr()
9585 return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx) 9587 def fpNEQ(a, b, ctx=None): 9588 """Create the Z3 floating-point expression `
Not(
fpEQ(other, self))`.
9593 >>> (x != y).sexpr()
9596 return Not(fpEQ(a, b, ctx)) 9598 def fpFP(sgn, exp, sig, ctx=None): 9599 """Create the Z3 floating-point value `
fpFP(sgn, sig, exp)`
from the three bit-vectors sgn, sig,
and exp.
9604 fpFP(1, 127, 4194304)
9605 >>> xv =
FPVal(-1.5, s)
9609 >>> slvr.add(
fpEQ(x, xv))
9612 >>> xv =
FPVal(+1.5, s)
9616 >>> slvr.add(
fpEQ(x, xv))
9620 _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch") 9621 _z3_assert(sgn.sort().size() == 1, "sort mismatch") 9623 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch") 9624 return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx) 9626 def fpToFP(a1, a2=None, a3=None, ctx=None): 9627 """Create a Z3 floating-point conversion expression
from other term sorts
9630 From a bit-vector term
in IEEE 754-2008 format:
9636 From a floating-point term with different precision:
9647 From a signed bit-vector term:
9653 if is_bv(a1) and is_fp_sort(a2): 9654 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx) 9655 elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3): 9656 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9657 elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3): 9658 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9659 elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3): 9660 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9662 raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.") 9664 def fpBVToFP(v, sort, ctx=None): 9665 """Create a Z3 floating-point conversion expression that represents the
9666 conversion
from a bit-vector term to a floating-point term.
9675 _z3_assert(is_bv(v), "First argument must be a Z3 floating-point rounding mode expression.") 9676 _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.") 9678 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx) 9680 def fpFPToFP(rm, v, sort, ctx=None): 9681 """Create a Z3 floating-point conversion expression that represents the
9682 conversion
from a floating-point term to a floating-point term of different precision.
9693 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9694 _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.") 9695 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9697 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9699 def fpRealToFP(rm, v, sort, ctx=None): 9700 """Create a Z3 floating-point conversion expression that represents the
9701 conversion
from a real term to a floating-point term.
9710 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9711 _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.") 9712 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9714 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9716 def fpSignedToFP(rm, v, sort, ctx=None): 9717 """Create a Z3 floating-point conversion expression that represents the
9718 conversion
from a signed bit-vector term (encoding an integer) to a floating-point term.
9727 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9728 _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") 9729 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9731 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9733 def fpUnsignedToFP(rm, v, sort, ctx=None): 9734 """Create a Z3 floating-point conversion expression that represents the
9735 conversion
from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9744 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9745 _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") 9746 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9748 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9750 def fpToFPUnsigned(rm, x, s, ctx=None): 9751 """Create a Z3 floating-point conversion expression,
from unsigned bit-vector to floating-point expression.
""" 9753 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9754 _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression") 9755 _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort") 9757 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx) 9759 def fpToSBV(rm, x, s, ctx=None): 9760 """Create a Z3 floating-point conversion expression,
from floating-point expression to signed bit-vector.
9774 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9775 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") 9776 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") 9778 return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9780 def fpToUBV(rm, x, s, ctx=None): 9781 """Create a Z3 floating-point conversion expression,
from floating-point expression to unsigned bit-vector.
9795 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9796 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") 9797 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") 9799 return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9801 def fpToReal(x, ctx=None): 9802 """Create a Z3 floating-point conversion expression,
from floating-point expression to real.
9816 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9818 return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx) 9820 def fpToIEEEBV(x, ctx=None): 9821 """\brief Conversion of a floating-point term into a bit-vector term
in IEEE 754-2008 format.
9823 The size of the resulting bit-vector
is automatically determined.
9825 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9826 knows only one NaN
and it will always produce the same bit-vector representation of
9841 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9843 return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx) 9847 ######################################### 9849 # Strings, Sequences and Regular expressions 9851 ######################################### 9853 class SeqSortRef(SortRef): 9854 """Sequence sort.
""" 9856 def is_string(self): 9857 """Determine
if sort
is a string
9865 return Z3_is_string_sort(self.ctx_ref(), self.ast) 9868 def StringSort(ctx=None): 9869 """Create a string sort
9875 return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx) 9879 """Create a sequence sort over elements provided
in the argument
9884 return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx) 9886 class SeqRef(ExprRef): 9887 """Sequence expression.
""" 9890 return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 9892 def __add__(self, other): 9893 return Concat(self, other) 9895 def __radd__(self, other): 9896 return Concat(other, self) 9898 def __getitem__(self, i): 9900 i = IntVal(i, self.ctx) 9901 return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) 9903 def is_string(self): 9904 return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast())) 9906 def is_string_value(self): 9907 return Z3_is_string(self.ctx_ref(), self.as_ast()) 9909 def as_string(self): 9910 """Return a string representation of sequence expression.
""" 9911 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 9914 def _coerce_seq(s, ctx=None): 9915 if isinstance(s, str): 9917 s = StringVal(s, ctx) 9919 raise Z3Exception("Non-expression passed as a sequence") 9921 raise Z3Exception("Non-sequence passed as a sequence") 9924 def _get_ctx2(a, b, ctx=None): 9934 """Return `
True`
if `a`
is a Z3 sequence expression.
9940 return isinstance(a, SeqRef) 9943 """Return `
True`
if `a`
is a Z3 string expression.
9947 return isinstance(a, SeqRef) and a.is_string() 9949 def is_string_value(a): 9950 """return 'True' if 'a' is a Z3 string constant expression.
9956 return isinstance(a, SeqRef) and a.is_string_value() 9959 def StringVal(s, ctx=None): 9960 """create a string expression
""" 9962 return SeqRef(Z3_mk_string(ctx.ref(), s), ctx) 9964 def String(name, ctx=None): 9965 """Return a string constant named `name`. If `ctx=
None`, then the
global context
is used.
9970 return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx) 9972 def SubString(s, offset, length): 9973 """Extract substring
or subsequence starting at offset
""" 9974 return Extract(s, offset, length) 9976 def SubSeq(s, offset, length): 9977 """Extract substring
or subsequence starting at offset
""" 9978 return Extract(s, offset, length) 9980 def Strings(names, ctx=None): 9981 """Return a tuple of String constants.
""" 9983 if isinstance(names, str): 9984 names = names.split(" ") 9985 return [String(name, ctx) for name in names] 9988 """Create the empty sequence of the given sort
10002 if isinstance(s, SeqSortRef): 10003 return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx) 10004 if isinstance(s, ReSortRef): 10005 return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx) 10006 raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty") 10009 """Create the regular expression that accepts the universal language
10017 if isinstance(s, ReSortRef): 10018 return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx) 10019 raise Z3Exception("Non-sequence, non-regular expression sort passed to Full") 10023 """Create a singleton sequence
""" 10024 return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx) 10026 def PrefixOf(a, b): 10027 """Check
if 'a' is a prefix of
'b' 10035 ctx = _get_ctx2(a, b) 10036 a = _coerce_seq(a, ctx) 10037 b = _coerce_seq(b, ctx) 10038 return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 10040 def SuffixOf(a, b): 10041 """Check
if 'a' is a suffix of
'b' 10049 ctx = _get_ctx2(a, b) 10050 a = _coerce_seq(a, ctx) 10051 b = _coerce_seq(b, ctx) 10052 return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 10054 def Contains(a, b): 10055 """Check
if 'a' contains
'b' 10062 >>> x, y, z =
Strings(
'x y z')
10067 ctx = _get_ctx2(a, b) 10068 a = _coerce_seq(a, ctx) 10069 b = _coerce_seq(b, ctx) 10070 return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 10073 def Replace(s, src, dst): 10074 """Replace the first occurrence of
'src' by
'dst' in 's' 10075 >>> r =
Replace(
"aaa",
"a",
"b")
10079 ctx = _get_ctx2(dst, s) 10080 if ctx is None and is_expr(src): 10082 src = _coerce_seq(src, ctx) 10083 dst = _coerce_seq(dst, ctx) 10084 s = _coerce_seq(s, ctx) 10085 return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx) 10087 def IndexOf(s, substr): 10088 return IndexOf(s, substr, IntVal(0)) 10090 def IndexOf(s, substr, offset): 10091 """Retrieve the index of substring within a string starting at a specified offset.
10098 if is_expr(offset): 10100 ctx = _get_ctx2(s, substr, ctx) 10101 s = _coerce_seq(s, ctx) 10102 substr = _coerce_seq(substr, ctx) 10103 if _is_int(offset): 10104 offset = IntVal(offset, ctx) 10105 return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx) 10108 """Obtain the length of a sequence
's' 10114 return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx) 10117 """Convert string expression to integer
10129 return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx) 10133 """Convert integer expression to string
""" 10136 return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx) 10139 def Re(s, ctx=None): 10140 """The regular expression that accepts sequence
's' 10145 s = _coerce_seq(s, ctx) 10146 return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx) 10151 ## Regular expressions 10153 class ReSortRef(SortRef): 10154 """Regular expression sort.
""" 10159 return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx) 10160 if s is None or isinstance(s, Context): 10162 return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), s.ctx) 10163 raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument") 10166 class ReRef(ExprRef): 10167 """Regular expressions.
""" 10169 def __add__(self, other): 10170 return Union(self, other) 10174 return isinstance(s, ReRef) 10178 """Create regular expression membership test
10187 s = _coerce_seq(s, re.ctx) 10188 return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx) 10191 """Create union of regular expressions.
10196 args = _get_args(args) 10199 _z3_assert(sz > 0, "At least one argument expected.") 10200 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 10205 for i in range(sz): 10206 v[i] = args[i].as_ast() 10207 return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx) 10210 """Create the regular expression accepting one
or more repetitions of argument.
10219 return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx) 10222 """Create the regular expression that optionally accepts the argument.
10231 return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx) 10233 def Complement(re): 10234 """Create the complement regular expression.
""" 10235 return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx) 10238 """Create the regular expression accepting zero
or more repetitions of argument.
10247 return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx) 10249 def Loop(re, lo, hi=0): 10250 """Create the regular expression accepting between a lower
and upper bound repetitions
10251 >>> re =
Loop(
Re(
"a"), 1, 3)
10259 return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)
Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o)
Return the parameter description set for the given optimize object.
Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i)
Return the name of the i probe.
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)
Return objectives on the optimization context. If the objective function is a max-sat objective it is...
def fpToIEEEBV(x, ctx=None)
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
def simplify(a, arguments, keywords)
Utils.
Z3_bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
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.
def FreshReal(prefix='b', ctx=None)
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form: ...
def update_rule(self, head, body, name)
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
def args2params(arguments, keywords, ctx=None)
def get_cover_delta(self, level, predicate)
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a bound variable.
def upper_values(self, obj)
def RatVal(a, b, ctx=None)
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
def __getitem__(self, idx)
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
def RealVector(prefix, sz, ctx=None)
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_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
Z3_bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
expr range(expr const &lo, expr const &hi)
def fpBVToFP(v, sort, ctx=None)
def FPs(names, fpsort, ctx=None)
def FPVal(sig, exp=None, fps=None, ctx=None)
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context...
def RealVarVector(n, ctx=None)
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
def substitute_vars(t, m)
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
def to_symbol(s, ctx=None)
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
def declare(self, name, args)
def assert_exprs(self, args)
def set_option(args, kws)
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
def IntVal(val, ctx=None)
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
def parse_smt2_string(s, sorts={}, decls={}, ctx=None)
def __init__(self, ctx=None)
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_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
def fpToFP(a1, a2=None, a3=None, ctx=None)
def assert_exprs(self, args)
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)
Return the name of the idx tactic.
def fpUnsignedToFP(rm, v, sort, ctx=None)
def lower_values(self, obj)
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f)
Convert a Z3_func_decl into Z3_ast. This is just type casting.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
def __deepcopy__(self, memo={})
def register_relation(self, relations)
def fpToUBV(rm, x, s, ctx=None)
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size)
Create a named finite domain sort.
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
def __deepcopy__(self, memo={})
def fpGEQ(a, b, ctx=None)
def PbEq(args, k, ctx=None)
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.
def rule(self, head, body=None, name=None)
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
def fpRem(a, b, ctx=None)
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
Assert a constraint to the fixedpoint context.
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d)
Backtrack one backtracking point.
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p)
Apply tactic t to the goal g using the parameter set p.
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
def is_finite_domain_sort(s)
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.
def z3_error_handler(c, e)
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
def BoolVector(prefix, sz, ctx=None)
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
def Array(name, dom, rng)
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
def If(a, b, c, ctx=None)
def BitVecVal(val, bv, ctx=None)
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_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.
def Cond(p, t1, t2, ctx=None)
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d)
Create a backtracking point.
def fpMax(a, b, ctx=None)
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
def get_rule_names_along_trace(self)
def __init__(self, fixedpoint=None, ctx=None)
def simplify_param_descrs()
def fpToFPUnsigned(rm, x, s, ctx=None)
def fpMul(rm, a, b, ctx=None)
def BitVec(name, bv, ctx=None)
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
def FiniteDomainSort(name, sz, ctx=None)
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
def FreshConst(sort, prefix='c')
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
def fpSignedToFP(rm, v, sort, ctx=None)
def fact(self, head, name=None)
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
def convert_model(self, model)
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
def __init__(self, args, kws)
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective.
def ParAndThen(t1, t2, ctx=None)
def Bools(names, ctx=None)
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. You can use Z3_get_ast_id intercha...
def RealVal(val, ctx=None)
def Extract(high, low, a)
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
def RealVar(idx, ctx=None)
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
def solve_using(s, args, keywords)
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context...
def set_predicate_representation(self, f, representations)
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1...
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query. ...
def RecFunction(name, sig)
Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s)
Convert a Z3_sort into Z3_ast. This is just type casting.
def add_soft(self, arg, weight="1", id=None)
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
void Z3_API Z3_enable_trace(Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
def __deepcopy__(self, memo={})
def Implies(a, b, ctx=None)
def __init__(self, tactic, ctx=None)
def __deepcopy__(self, memo={})
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
def apply(self, goal, arguments, keywords)
def solve(args, keywords)
def __init__(self, opt, value, is_max)
def check(self, assumptions)
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
def StringVal(s, ctx=None)
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
def __call__(self, goal, arguments, keywords)
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
def FiniteDomainVal(val, sort, ctx=None)
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
def FPSort(ebits, sbits, ctx=None)
def prove(claim, keywords)
def DeclareSort(name, ctx=None)
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
def Ints(names, ctx=None)
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
def is_finite_domain_value(a)
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
def FreshBool(prefix='b', ctx=None)
def probe_description(name, ctx=None)
def get_rules_along_trace(self)
def __deepcopy__(self, memo={})
def tactic_description(name, ctx=None)
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
def FP(name, fpsort, ctx=None)
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.
def fpToSBV(rm, x, s, ctx=None)
def fpDiv(rm, a, b, ctx=None)
def BitVecs(names, bv, ctx=None)
def translate(self, target)
def from_file(self, filename)
Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t *r)
Store the size of the sort in r. Return false if the call failed. That is, Z3_get_sort_kind(s) == Z3_...
def __init__(self, probe, ctx=None)
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
Query the PDR engine for the maximal levels properties are known about predicate. ...
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
def query_from_lvl(self, lvl, query)
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.
Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i)
Return the sort of the i-th parameter of the given function declaration.
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
def to_string(self, queries)
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
def Strings(names, ctx=None)
void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created. ...
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
def fpSub(rm, a, b, ctx=None)
def fpFP(sgn, exp, sig, ctx=None)
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
def parse_string(self, s)
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
def fpLEQ(a, b, ctx=None)
def get_ground_sat_answer(self)
def EnumSort(name, values, ctx=None)
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)
Return the set of asserted formulas on the optimization context.
def declare_var(self, vars)
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
def add_rule(self, head, body=None, name=None)
def __rmul__(self, other)
def RecAddDefinition(f, args, body)
def BoolVal(val, ctx=None)
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
def fpMin(a, b, ctx=None)
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
def FreshInt(prefix='x', ctx=None)
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target)
Translate/Copy the AST a from context source to context target. AST a must have been created using co...
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d)
Retrieve a string that describes the last status returned by Z3_optimize_check.
def BitVecSort(sz, ctx=None)
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
def IntVector(prefix, sz, ctx=None)
def fpAdd(rm, a, b, ctx=None)
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
def get_num_levels(self, predicate)
Z3_string Z3_API Z3_simplify_get_help(Z3_context c)
Return a string describing all available parameters.
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
def BV2Int(a, is_signed=False)
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)
Define the body of a recursive function.
def TryFor(t, ms, ctx=None)
def __init__(self, ast, ctx=None)
def __init__(self, result, ctx)
def abstract(self, fml, is_forall=True)
def set(self, args, keys)
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
def fpToReal(x, ctx=None)
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
def add_cover(self, level, predicate, property)
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
def Reals(names, ctx=None)
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
def fpFPToFP(rm, v, sort, ctx=None)
def fpNEQ(a, b, ctx=None)
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
def Repeat(t, max=4294967295, ctx=None)
Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective. The returned vector ...
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
def SolverFor(logic, ctx=None)
def ParThen(t1, t2, ctx=None)
void Z3_API Z3_fixedpoint_set_predicate_representation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f, unsigned num_relations, Z3_symbol const relation_kinds[])
Configure the predicate representation.
Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the probe with the given name.
def set(self, args, keys)
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
def fpRealToFP(rm, v, sort, ctx=None)
Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)
Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...
Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the tactic with the given name.
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
def check(self, assumptions)
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
def is_algebraic_value(a)
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
def __deepcopy__(self, memo={})
def String(name, ctx=None)
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.
Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the sort value associated with a sort parameter.
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
def SimpleSolver(ctx=None)
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.