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) 1654 def _has_probe(args): 1655 """Return `
True`
if one of the elements of the given collection
is a Z3 probe.
""" 1662 """Create a Z3
and-expression
or and-probe.
1664 >>> p, q, r =
Bools(
'p q r')
1669 And(p__0, p__1, p__2, p__3, p__4)
1673 last_arg = args[len(args)-1] 1674 if isinstance(last_arg, Context): 1675 ctx = args[len(args)-1] 1676 args = args[:len(args)-1] 1677 elif len(args) == 1 and isinstance(args[0], AstVector): 1679 args = [a for a in args[0]] 1682 args = _get_args(args) 1683 ctx_args = _ctx_from_ast_arg_list(args, ctx) 1685 _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") 1686 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") 1687 if _has_probe(args): 1688 return _probe_and(args, ctx) 1690 args = _coerce_expr_list(args, ctx) 1691 _args, sz = _to_ast_array(args) 1692 return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx) 1695 """Create a Z3
or-expression
or or-probe.
1697 >>> p, q, r =
Bools(
'p q r')
1702 Or(p__0, p__1, p__2, p__3, p__4)
1706 last_arg = args[len(args)-1] 1707 if isinstance(last_arg, Context): 1708 ctx = args[len(args)-1] 1709 args = args[:len(args)-1] 1712 args = _get_args(args) 1713 ctx_args = _ctx_from_ast_arg_list(args, ctx) 1715 _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") 1716 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") 1717 if _has_probe(args): 1718 return _probe_or(args, ctx) 1720 args = _coerce_expr_list(args, ctx) 1721 _args, sz = _to_ast_array(args) 1722 return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx) 1724 ######################################### 1728 ######################################### 1730 class PatternRef(ExprRef): 1731 """Patterns are hints
for quantifier instantiation.
1735 return Z3_pattern_to_ast(self.ctx_ref(), self.ast) 1738 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1741 """Return `
True`
if `a`
is a Z3 pattern (hint
for quantifier instantiation.
1745 >>> q =
ForAll(x, f(x) == 0, patterns = [ f(x) ])
1748 >>> q.num_patterns()
1755 return isinstance(a, PatternRef) 1757 def MultiPattern(*args): 1758 """Create a Z3 multi-pattern using the given expressions `*args`
1766 >>> q.num_patterns()
1774 _z3_assert(len(args) > 0, "At least one argument expected") 1775 _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected") 1777 args, sz = _to_ast_array(args) 1778 return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx) 1780 def _to_pattern(arg): 1784 return MultiPattern(arg) 1786 ######################################### 1790 ######################################### 1792 class QuantifierRef(BoolRef): 1793 """Universally
and Existentially quantified formulas.
""" 1799 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1802 """Return the Boolean sort
or sort of Lambda.
""" 1803 if self.is_lambda(): 1804 return _sort(self.ctx, self.as_ast()) 1805 return BoolSort(self.ctx) 1807 def is_forall(self): 1808 """Return `
True`
if `self`
is a universal quantifier.
1812 >>> q =
ForAll(x, f(x) == 0)
1815 >>> q =
Exists(x, f(x) != 0)
1819 return Z3_is_quantifier_forall(self.ctx_ref(), self.ast) 1821 def is_exists(self): 1822 """Return `
True`
if `self`
is an existential quantifier.
1826 >>> q =
ForAll(x, f(x) == 0)
1829 >>> q =
Exists(x, f(x) != 0)
1833 return Z3_is_quantifier_exists(self.ctx_ref(), self.ast) 1835 def is_lambda(self): 1836 """Return `
True`
if `self`
is a
lambda expression.
1843 >>> q =
Exists(x, f(x) != 0)
1847 return Z3_is_lambda(self.ctx_ref(), self.ast) 1850 """Return the weight annotation of `self`.
1854 >>> q =
ForAll(x, f(x) == 0)
1857 >>> q =
ForAll(x, f(x) == 0, weight=10)
1861 return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast)) 1863 def num_patterns(self): 1864 """Return the number of patterns (i.e., quantifier instantiation hints)
in `self`.
1869 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1870 >>> q.num_patterns()
1873 return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast)) 1875 def pattern(self, idx): 1876 """Return a pattern (i.e., quantifier instantiation hints)
in `self`.
1881 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1882 >>> q.num_patterns()
1890 _z3_assert(idx < self.num_patterns(), "Invalid pattern idx") 1891 return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1893 def num_no_patterns(self): 1894 """Return the number of no-patterns.
""" 1895 return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast) 1897 def no_pattern(self, idx): 1898 """Return a no-pattern.
""" 1900 _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx") 1901 return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1904 """Return the expression being quantified.
1908 >>> q =
ForAll(x, f(x) == 0)
1912 return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx) 1915 """Return the number of variables bounded by this quantifier.
1920 >>> q =
ForAll([x, y], f(x, y) >= x)
1924 return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast)) 1926 def var_name(self, idx): 1927 """Return a string representing a name used when displaying the quantifier.
1932 >>> q =
ForAll([x, y], f(x, y) >= x)
1939 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1940 return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx)) 1942 def var_sort(self, idx): 1943 """Return the sort of a bound variable.
1948 >>> q =
ForAll([x, y], f(x, y) >= x)
1955 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1956 return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx) 1959 """Return a list containing a single element self.
body()
1963 >>> q =
ForAll(x, f(x) == 0)
1967 return [ self.body() ] 1969 def is_quantifier(a): 1970 """Return `
True`
if `a`
is a Z3 quantifier.
1974 >>> q =
ForAll(x, f(x) == 0)
1980 return isinstance(a, QuantifierRef) 1982 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 1984 _z3_assert(is_bool(body) or is_app(vs) or (len(vs) > 0 and is_app(vs[0])), "Z3 expression expected") 1985 _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)") 1986 _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected") 1987 _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions") 1993 if not is_expr(body): 1994 body = BoolVal(body, ctx) 1998 _vs = (Ast * num_vars)() 1999 for i in range(num_vars): 2000 ## TODO: Check if is constant 2001 _vs[i] = vs[i].as_ast() 2002 patterns = [ _to_pattern(p) for p in patterns ] 2003 num_pats = len(patterns) 2004 _pats = (Pattern * num_pats)() 2005 for i in range(num_pats): 2006 _pats[i] = patterns[i].ast 2007 _no_pats, num_no_pats = _to_ast_array(no_patterns) 2008 qid = to_symbol(qid, ctx) 2009 skid = to_symbol(skid, ctx) 2010 return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid, 2013 num_no_pats, _no_pats, 2014 body.as_ast()), ctx) 2016 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 2017 """Create a Z3 forall formula.
2019 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
2024 >>>
ForAll([x, y], f(x, y) >= x)
2025 ForAll([x, y], f(x, y) >= x)
2026 >>>
ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2027 ForAll([x, y], f(x, y) >= x)
2028 >>>
ForAll([x, y], f(x, y) >= x, weight=10)
2029 ForAll([x, y], f(x, y) >= x)
2031 return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns) 2033 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 2034 """Create a Z3 exists formula.
2036 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
2042 >>> q =
Exists([x, y], f(x, y) >= x, skid=
"foo")
2044 Exists([x, y], f(x, y) >= x)
2047 >>> r =
Tactic(
'nnf')(q).as_expr()
2051 return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns) 2053 def Lambda(vs, body): 2054 """Create a Z3
lambda expression.
2058 >>> lo, hi, e, i =
Ints(
'lo hi e i')
2059 >>> mem1 =
Lambda([i],
If(
And(lo <= i, i <= hi), e, mem0[i]))
2067 _vs = (Ast * num_vars)() 2068 for i in range(num_vars): 2069 ## TODO: Check if is constant 2070 _vs[i] = vs[i].as_ast() 2071 return QuantifierRef(Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx) 2073 ######################################### 2077 ######################################### 2079 class ArithSortRef(SortRef): 2080 """Real
and Integer sorts.
""" 2083 """Return `
True`
if `self`
is of the sort Real.
2094 return self.kind() == Z3_REAL_SORT 2097 """Return `
True`
if `self`
is of the sort Integer.
2108 return self.kind() == Z3_INT_SORT 2110 def subsort(self, other): 2111 """Return `
True`
if `self`
is a subsort of `other`.
""" 2112 return self.is_int() and is_arith_sort(other) and other.is_real() 2114 def cast(self, val): 2115 """Try to cast `val`
as an Integer
or Real.
2130 _z3_assert(self.ctx == val.ctx, "Context mismatch") 2134 if val_s.is_int() and self.is_real(): 2136 if val_s.is_bool() and self.is_int(): 2137 return If(val, 1, 0) 2138 if val_s.is_bool() and self.is_real(): 2139 return ToReal(If(val, 1, 0)) 2141 _z3_assert(False, "Z3 Integer/Real expression expected" ) 2144 return IntVal(val, self.ctx) 2146 return RealVal(val, self.ctx) 2148 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self) 2150 def is_arith_sort(s): 2151 """Return `
True`
if s
is an arithmetical sort (type).
2159 >>> n =
Int(
'x') + 1
2163 return isinstance(s, ArithSortRef) 2165 class ArithRef(ExprRef): 2166 """Integer
and Real expressions.
""" 2169 """Return the sort (type) of the arithmetical expression `self`.
2176 return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 2179 """Return `
True`
if `self`
is an integer expression.
2190 return self.sort().is_int() 2193 """Return `
True`
if `self`
is an real expression.
2201 return self.sort().is_real() 2203 def __add__(self, other): 2204 """Create the Z3 expression `self + other`.
2213 a, b = _coerce_exprs(self, other) 2214 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx) 2216 def __radd__(self, other): 2217 """Create the Z3 expression `other + self`.
2223 a, b = _coerce_exprs(self, other) 2224 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx) 2226 def __mul__(self, other): 2227 """Create the Z3 expression `self * other`.
2236 if isinstance(other, BoolRef): 2237 return If(other, self, 0) 2238 a, b = _coerce_exprs(self, other) 2239 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx) 2241 def __rmul__(self, other): 2242 """Create the Z3 expression `other * self`.
2248 a, b = _coerce_exprs(self, other) 2249 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx) 2251 def __sub__(self, other): 2252 """Create the Z3 expression `self - other`.
2261 a, b = _coerce_exprs(self, other) 2262 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx) 2264 def __rsub__(self, other): 2265 """Create the Z3 expression `other - self`.
2271 a, b = _coerce_exprs(self, other) 2272 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx) 2274 def __pow__(self, other): 2275 """Create the Z3 expression `self**other` (**
is the power operator).
2285 a, b = _coerce_exprs(self, other) 2286 return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2288 def __rpow__(self, other): 2289 """Create the Z3 expression `other**self` (**
is the power operator).
2299 a, b = _coerce_exprs(self, other) 2300 return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2302 def __div__(self, other): 2303 """Create the Z3 expression `other/self`.
2322 a, b = _coerce_exprs(self, other) 2323 return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2325 def __truediv__(self, other): 2326 """Create the Z3 expression `other/self`.
""" 2327 return self.__div__(other) 2329 def __rdiv__(self, other): 2330 """Create the Z3 expression `other/self`.
2343 a, b = _coerce_exprs(self, other) 2344 return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2346 def __rtruediv__(self, other): 2347 """Create the Z3 expression `other/self`.
""" 2348 return self.__rdiv__(other) 2350 def __mod__(self, other): 2351 """Create the Z3 expression `other%self`.
2360 a, b = _coerce_exprs(self, other) 2362 _z3_assert(a.is_int(), "Z3 integer expression expected") 2363 return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2365 def __rmod__(self, other): 2366 """Create the Z3 expression `other%self`.
2372 a, b = _coerce_exprs(self, other) 2374 _z3_assert(a.is_int(), "Z3 integer expression expected") 2375 return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2378 """Return an expression representing `-self`.
2386 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx) 2397 def __le__(self, other): 2398 """Create the Z3 expression `other <= self`.
2400 >>> x, y =
Ints(
'x y')
2407 a, b = _coerce_exprs(self, other) 2408 return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2410 def __lt__(self, other): 2411 """Create the Z3 expression `other < self`.
2413 >>> x, y =
Ints(
'x y')
2420 a, b = _coerce_exprs(self, other) 2421 return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2423 def __gt__(self, other): 2424 """Create the Z3 expression `other > self`.
2426 >>> x, y =
Ints(
'x y')
2433 a, b = _coerce_exprs(self, other) 2434 return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2436 def __ge__(self, other): 2437 """Create the Z3 expression `other >= self`.
2439 >>> x, y =
Ints(
'x y')
2446 a, b = _coerce_exprs(self, other) 2447 return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2450 """Return `
True`
if `a`
is an arithmetical expression.
2467 return isinstance(a, ArithRef) 2470 """Return `
True`
if `a`
is an integer expression.
2485 return is_arith(a) and a.is_int() 2488 """Return `
True`
if `a`
is a real expression.
2503 return is_arith(a) and a.is_real() 2505 def _is_numeral(ctx, a): 2506 return Z3_is_numeral_ast(ctx.ref(), a) 2508 def _is_algebraic(ctx, a): 2509 return Z3_is_algebraic_number(ctx.ref(), a) 2511 def is_int_value(a): 2512 """Return `
True`
if `a`
is an integer value of sort Int.
2520 >>> n =
Int(
'x') + 1
2532 return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast()) 2534 def is_rational_value(a): 2535 """Return `
True`
if `a`
is rational value of sort Real.
2545 >>> n =
Real(
'x') + 1
2553 return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast()) 2555 def is_algebraic_value(a): 2556 """Return `
True`
if `a`
is an algebraic value of sort Real.
2566 return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast()) 2569 """Return `
True`
if `a`
is an expression of the form b + c.
2571 >>> x, y =
Ints(
'x y')
2577 return is_app_of(a, Z3_OP_ADD) 2580 """Return `
True`
if `a`
is an expression of the form b * c.
2582 >>> x, y =
Ints(
'x y')
2588 return is_app_of(a, Z3_OP_MUL) 2591 """Return `
True`
if `a`
is an expression of the form b - c.
2593 >>> x, y =
Ints(
'x y')
2599 return is_app_of(a, Z3_OP_SUB) 2602 """Return `
True`
if `a`
is an expression of the form b / c.
2604 >>> x, y =
Reals(
'x y')
2609 >>> x, y =
Ints(
'x y')
2615 return is_app_of(a, Z3_OP_DIV) 2618 """Return `
True`
if `a`
is an expression of the form b div c.
2620 >>> x, y =
Ints(
'x y')
2626 return is_app_of(a, Z3_OP_IDIV) 2629 """Return `
True`
if `a`
is an expression of the form b % c.
2631 >>> x, y =
Ints(
'x y')
2637 return is_app_of(a, Z3_OP_MOD) 2640 """Return `
True`
if `a`
is an expression of the form b <= c.
2642 >>> x, y =
Ints(
'x y')
2648 return is_app_of(a, Z3_OP_LE) 2651 """Return `
True`
if `a`
is an expression of the form b < c.
2653 >>> x, y =
Ints(
'x y')
2659 return is_app_of(a, Z3_OP_LT) 2662 """Return `
True`
if `a`
is an expression of the form b >= c.
2664 >>> x, y =
Ints(
'x y')
2670 return is_app_of(a, Z3_OP_GE) 2673 """Return `
True`
if `a`
is an expression of the form b > c.
2675 >>> x, y =
Ints(
'x y')
2681 return is_app_of(a, Z3_OP_GT) 2684 """Return `
True`
if `a`
is an expression of the form
IsInt(b).
2692 return is_app_of(a, Z3_OP_IS_INT) 2695 """Return `
True`
if `a`
is an expression of the form
ToReal(b).
2706 return is_app_of(a, Z3_OP_TO_REAL) 2709 """Return `
True`
if `a`
is an expression of the form
ToInt(b).
2720 return is_app_of(a, Z3_OP_TO_INT) 2722 class IntNumRef(ArithRef): 2723 """Integer values.
""" 2726 """Return a Z3 integer numeral
as a Python long (bignum) numeral.
2735 _z3_assert(self.is_int(), "Integer value expected") 2736 return int(self.as_string()) 2738 def as_string(self): 2739 """Return a Z3 integer numeral
as a Python string.
2744 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2746 class RatNumRef(ArithRef): 2747 """Rational values.
""" 2749 def numerator(self): 2750 """ Return the numerator of a Z3 rational numeral.
2762 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx) 2764 def denominator(self): 2765 """ Return the denominator of a Z3 rational numeral.
2773 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx) 2775 def numerator_as_long(self): 2776 """ Return the numerator
as a Python long.
2783 >>> v.numerator_as_long() + 1 == 10000000001
2786 return self.numerator().as_long() 2788 def denominator_as_long(self): 2789 """ Return the denominator
as a Python long.
2794 >>> v.denominator_as_long()
2797 return self.denominator().as_long() 2805 def is_int_value(self): 2806 return self.denominator().is_int() and self.denominator_as_long() == 1 2809 _z3_assert(self.is_int_value(), "Expected integer fraction") 2810 return self.numerator_as_long() 2812 def as_decimal(self, prec): 2813 """ Return a Z3 rational value
as a string
in decimal notation using at most `prec` decimal places.
2822 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2824 def as_string(self): 2825 """Return a Z3 rational numeral
as a Python string.
2831 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2833 def as_fraction(self): 2834 """Return a Z3 rational
as a Python Fraction object.
2840 return Fraction(self.numerator_as_long(), self.denominator_as_long()) 2842 class AlgebraicNumRef(ArithRef): 2843 """Algebraic irrational values.
""" 2845 def approx(self, precision=10): 2846 """Return a Z3 rational number that approximates the algebraic number `self`.
2847 The result `r`
is such that |r - self| <= 1/10^precision
2851 6838717160008073720548335/4835703278458516698824704
2855 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx) 2856 def as_decimal(self, prec): 2857 """Return a string representation of the algebraic number `self`
in decimal notation using `prec` decimal places
2860 >>> x.as_decimal(10)
2862 >>> x.as_decimal(20)
2863 '1.41421356237309504880?' 2865 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2867 def _py2expr(a, ctx=None): 2868 if isinstance(a, bool): 2869 return BoolVal(a, ctx) 2871 return IntVal(a, ctx) 2872 if isinstance(a, float): 2873 return RealVal(a, ctx) 2877 _z3_assert(False, "Python bool, int, long or float expected") 2879 def IntSort(ctx=None): 2880 """Return the integer sort
in the given context. If `ctx=
None`, then the
global context
is used.
2893 return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx) 2895 def RealSort(ctx=None): 2896 """Return the real sort
in the given context. If `ctx=
None`, then the
global context
is used.
2909 return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx) 2911 def _to_int_str(val): 2912 if isinstance(val, float): 2913 return str(int(val)) 2914 elif isinstance(val, bool): 2921 elif isinstance(val, str): 2924 _z3_assert(False, "Python value cannot be used as a Z3 integer") 2926 def IntVal(val, ctx=None): 2927 """Return a Z3 integer value. If `ctx=
None`, then the
global context
is used.
2935 return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx) 2937 def RealVal(val, ctx=None): 2938 """Return a Z3 real value.
2940 `val` may be a Python int, long, float
or string representing a number
in decimal
or rational notation.
2941 If `ctx=
None`, then the
global context
is used.
2953 return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx) 2955 def RatVal(a, b, ctx=None): 2956 """Return a Z3 rational a/b.
2958 If `ctx=
None`, then the
global context
is used.
2966 _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer") 2967 _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer") 2968 return simplify(RealVal(a, ctx)/RealVal(b, ctx)) 2970 def Q(a, b, ctx=None): 2971 """Return a Z3 rational a/b.
2973 If `ctx=
None`, then the
global context
is used.
2980 return simplify(RatVal(a, b)) 2982 def Int(name, ctx=None): 2983 """Return an integer constant named `name`. If `ctx=
None`, then the
global context
is used.
2992 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx) 2994 def Ints(names, ctx=None): 2995 """Return a tuple of Integer constants.
2997 >>> x, y, z =
Ints(
'x y z')
3002 if isinstance(names, str): 3003 names = names.split(" ") 3004 return [Int(name, ctx) for name in names] 3006 def IntVector(prefix, sz, ctx=None): 3007 """Return a list of integer constants of size `sz`.
3015 return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ] 3017 def FreshInt(prefix='x', ctx=None): 3018 """Return a fresh integer constant
in the given context using the given prefix.
3028 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx) 3030 def Real(name, ctx=None): 3031 """Return a real constant named `name`. If `ctx=
None`, then the
global context
is used.
3040 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx) 3042 def Reals(names, ctx=None): 3043 """Return a tuple of real constants.
3045 >>> x, y, z =
Reals(
'x y z')
3048 >>>
Sum(x, y, z).sort()
3052 if isinstance(names, str): 3053 names = names.split(" ") 3054 return [Real(name, ctx) for name in names] 3056 def RealVector(prefix, sz, ctx=None): 3057 """Return a list of real constants of size `sz`.
3067 return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ] 3069 def FreshReal(prefix='b', ctx=None): 3070 """Return a fresh real constant
in the given context using the given prefix.
3080 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx) 3083 """ Return the Z3 expression
ToReal(a).
3095 _z3_assert(a.is_int(), "Z3 integer expression expected.") 3097 return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx) 3100 """ Return the Z3 expression
ToInt(a).
3112 _z3_assert(a.is_real(), "Z3 real expression expected.") 3114 return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx) 3117 """ Return the Z3 predicate
IsInt(a).
3120 >>>
IsInt(x +
"1/2")
3124 >>>
solve(
IsInt(x +
"1/2"), x > 0, x < 1, x !=
"1/2")
3128 _z3_assert(a.is_real(), "Z3 real expression expected.") 3130 return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx) 3132 def Sqrt(a, ctx=None): 3133 """ Return a Z3 expression which represents the square root of a.
3144 def Cbrt(a, ctx=None): 3145 """ Return a Z3 expression which represents the cubic root of a.
3156 ######################################### 3160 ######################################### 3162 class BitVecSortRef(SortRef): 3163 """Bit-vector sort.
""" 3166 """Return the size (number of bits) of the bit-vector sort `self`.
3172 return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast)) 3174 def subsort(self, other): 3175 return is_bv_sort(other) and self.size() < other.size() 3177 def cast(self, val): 3178 """Try to cast `val`
as a Bit-Vector.
3183 >>> b.cast(10).
sexpr()
3188 _z3_assert(self.ctx == val.ctx, "Context mismatch") 3189 # Idea: use sign_extend if sort of val is a bitvector of smaller size 3192 return BitVecVal(val, self) 3195 """Return
True if `s`
is a Z3 bit-vector sort.
3202 return isinstance(s, BitVecSortRef) 3204 class BitVecRef(ExprRef): 3205 """Bit-vector expressions.
""" 3208 """Return the sort of the bit-vector expression `self`.
3216 return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 3219 """Return the number of bits of the bit-vector expression `self`.
3227 return self.sort().size() 3229 def __add__(self, other): 3230 """Create the Z3 expression `self + other`.
3239 a, b = _coerce_exprs(self, other) 3240 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3242 def __radd__(self, other): 3243 """Create the Z3 expression `other + self`.
3249 a, b = _coerce_exprs(self, other) 3250 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3252 def __mul__(self, other): 3253 """Create the Z3 expression `self * other`.
3262 a, b = _coerce_exprs(self, other) 3263 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3265 def __rmul__(self, other): 3266 """Create the Z3 expression `other * self`.
3272 a, b = _coerce_exprs(self, other) 3273 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3275 def __sub__(self, other): 3276 """Create the Z3 expression `self - other`.
3285 a, b = _coerce_exprs(self, other) 3286 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3288 def __rsub__(self, other): 3289 """Create the Z3 expression `other - self`.
3295 a, b = _coerce_exprs(self, other) 3296 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3298 def __or__(self, other): 3299 """Create the Z3 expression bitwise-
or `self | other`.
3308 a, b = _coerce_exprs(self, other) 3309 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3311 def __ror__(self, other): 3312 """Create the Z3 expression bitwise-
or `other | self`.
3318 a, b = _coerce_exprs(self, other) 3319 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3321 def __and__(self, other): 3322 """Create the Z3 expression bitwise-
and `self & other`.
3331 a, b = _coerce_exprs(self, other) 3332 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3334 def __rand__(self, other): 3335 """Create the Z3 expression bitwise-
or `other & self`.
3341 a, b = _coerce_exprs(self, other) 3342 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3344 def __xor__(self, other): 3345 """Create the Z3 expression bitwise-xor `self ^ other`.
3354 a, b = _coerce_exprs(self, other) 3355 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3357 def __rxor__(self, other): 3358 """Create the Z3 expression bitwise-xor `other ^ self`.
3364 a, b = _coerce_exprs(self, other) 3365 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3377 """Return an expression representing `-self`.
3385 return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx) 3387 def __invert__(self): 3388 """Create the Z3 expression bitwise-
not `~self`.
3396 return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx) 3398 def __div__(self, other): 3399 """Create the Z3 expression (signed) division `self / other`.
3401 Use the function
UDiv()
for unsigned division.
3414 a, b = _coerce_exprs(self, other) 3415 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3417 def __truediv__(self, other): 3418 """Create the Z3 expression (signed) division `self / other`.
""" 3419 return self.__div__(other) 3421 def __rdiv__(self, other): 3422 """Create the Z3 expression (signed) division `other / self`.
3424 Use the function
UDiv()
for unsigned division.
3429 >>> (10 / x).
sexpr()
3430 '(bvsdiv #x0000000a x)' 3432 '(bvudiv #x0000000a x)' 3434 a, b = _coerce_exprs(self, other) 3435 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3437 def __rtruediv__(self, other): 3438 """Create the Z3 expression (signed) division `other / self`.
""" 3439 return self.__rdiv__(other) 3441 def __mod__(self, other): 3442 """Create the Z3 expression (signed) mod `self % other`.
3444 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3459 a, b = _coerce_exprs(self, other) 3460 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3462 def __rmod__(self, other): 3463 """Create the Z3 expression (signed) mod `other % self`.
3465 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3470 >>> (10 % x).
sexpr()
3471 '(bvsmod #x0000000a x)' 3473 '(bvurem #x0000000a x)' 3475 '(bvsrem #x0000000a x)' 3477 a, b = _coerce_exprs(self, other) 3478 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3480 def __le__(self, other): 3481 """Create the Z3 expression (signed) `other <= self`.
3483 Use the function
ULE()
for unsigned less than
or equal to.
3488 >>> (x <= y).
sexpr()
3493 a, b = _coerce_exprs(self, other) 3494 return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3496 def __lt__(self, other): 3497 """Create the Z3 expression (signed) `other < self`.
3499 Use the function
ULT()
for unsigned less than.
3509 a, b = _coerce_exprs(self, other) 3510 return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3512 def __gt__(self, other): 3513 """Create the Z3 expression (signed) `other > self`.
3515 Use the function
UGT()
for unsigned greater than.
3525 a, b = _coerce_exprs(self, other) 3526 return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3528 def __ge__(self, other): 3529 """Create the Z3 expression (signed) `other >= self`.
3531 Use the function
UGE()
for unsigned greater than
or equal to.
3536 >>> (x >= y).
sexpr()
3541 a, b = _coerce_exprs(self, other) 3542 return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3544 def __rshift__(self, other): 3545 """Create the Z3 expression (arithmetical) right shift `self >> other`
3547 Use the function
LShR()
for the right logical shift
3552 >>> (x >> y).
sexpr()
3571 a, b = _coerce_exprs(self, other) 3572 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3574 def __lshift__(self, other): 3575 """Create the Z3 expression left shift `self << other`
3580 >>> (x << y).
sexpr()
3585 a, b = _coerce_exprs(self, other) 3586 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3588 def __rrshift__(self, other): 3589 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3591 Use the function
LShR()
for the right logical shift
3596 >>> (10 >> x).
sexpr()
3597 '(bvashr #x0000000a x)' 3599 a, b = _coerce_exprs(self, other) 3600 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3602 def __rlshift__(self, other): 3603 """Create the Z3 expression left shift `other << self`.
3605 Use the function
LShR()
for the right logical shift
3610 >>> (10 << x).
sexpr()
3611 '(bvshl #x0000000a x)' 3613 a, b = _coerce_exprs(self, other) 3614 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3616 class BitVecNumRef(BitVecRef): 3617 """Bit-vector values.
""" 3620 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral.
3625 >>> print(
"0x%.8x" % v.as_long())
3628 return int(self.as_string()) 3630 def as_signed_long(self): 3631 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral. The most significant bit
is assumed to be the sign.
3645 val = self.as_long() 3646 if val >= 2**(sz - 1): 3648 if val < -2**(sz - 1): 3652 def as_string(self): 3653 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 3656 """Return `
True`
if `a`
is a Z3 bit-vector expression.
3666 return isinstance(a, BitVecRef) 3669 """Return `
True`
if `a`
is a Z3 bit-vector numeral value.
3680 return is_bv(a) and _is_numeral(a.ctx, a.as_ast()) 3682 def BV2Int(a, is_signed=False): 3683 """Return the Z3 expression
BV2Int(a).
3691 >>> x >
BV2Int(b, is_signed=
False)
3693 >>> x >
BV2Int(b, is_signed=
True)
3699 _z3_assert(is_bv(a), "Z3 bit-vector expression expected") 3701 ## investigate problem with bv2int 3702 return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx) 3704 def Int2BV(a, num_bits): 3705 """Return the z3 expression
Int2BV(a, num_bits).
3706 It
is a bit-vector of width num_bits
and represents the
3707 modulo of a by 2^num_bits
3710 return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx) 3712 def BitVecSort(sz, ctx=None): 3713 """Return a Z3 bit-vector sort of the given size. If `ctx=
None`, then the
global context
is used.
3719 >>> x =
Const(
'x', Byte)
3724 return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx) 3726 def BitVecVal(val, bv, ctx=None): 3727 """Return a bit-vector value with the given number of bits. If `ctx=
None`, then the
global context
is used.
3732 >>> print(
"0x%.8x" % v.as_long())
3737 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx) 3740 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx) 3742 def BitVec(name, bv, ctx=None): 3743 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3744 If `ctx=
None`, then the
global context
is used.
3754 >>> x2 =
BitVec(
'x', word)
3758 if isinstance(bv, BitVecSortRef): 3762 bv = BitVecSort(bv, ctx) 3763 return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx) 3765 def BitVecs(names, bv, ctx=None): 3766 """Return a tuple of bit-vector constants of size bv.
3768 >>> x, y, z =
BitVecs(
'x y z', 16)
3781 if isinstance(names, str): 3782 names = names.split(" ") 3783 return [BitVec(name, bv, ctx) for name in names] 3786 """Create a Z3 bit-vector concatenation expression.
3796 args = _get_args(args) 3799 _z3_assert(sz >= 2, "At least two arguments expected.") 3806 if is_seq(args[0]) or isinstance(args[0], str): 3807 args = [_coerce_seq(s, ctx) for s in args] 3809 _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") 3812 v[i] = args[i].as_ast() 3813 return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) 3817 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 3820 v[i] = args[i].as_ast() 3821 return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx) 3824 _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") 3826 for i in range(sz - 1): 3827 r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx) 3830 def Extract(high, low, a): 3831 """Create a Z3 bit-vector extraction expression,
or create a string extraction expression.
3841 if isinstance(high, str): 3842 high = StringVal(high) 3845 offset, length = _coerce_exprs(low, a, s.ctx) 3846 return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) 3848 _z3_assert(low <= high, "First argument must be greater than or equal to second argument") 3849 _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers") 3850 _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression") 3851 return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx) 3853 def _check_bv_args(a, b): 3855 _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression") 3858 """Create the Z3 expression (unsigned) `other <= self`.
3860 Use the operator <=
for signed less than
or equal to.
3865 >>> (x <= y).sexpr()
3867 >>>
ULE(x, y).sexpr()
3870 _check_bv_args(a, b) 3871 a, b = _coerce_exprs(a, b) 3872 return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3875 """Create the Z3 expression (unsigned) `other < self`.
3877 Use the operator <
for signed less than.
3884 >>>
ULT(x, y).sexpr()
3887 _check_bv_args(a, b) 3888 a, b = _coerce_exprs(a, b) 3889 return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3892 """Create the Z3 expression (unsigned) `other >= self`.
3894 Use the operator >=
for signed greater than
or equal to.
3899 >>> (x >= y).sexpr()
3901 >>>
UGE(x, y).sexpr()
3904 _check_bv_args(a, b) 3905 a, b = _coerce_exprs(a, b) 3906 return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3909 """Create the Z3 expression (unsigned) `other > self`.
3911 Use the operator >
for signed greater than.
3918 >>>
UGT(x, y).sexpr()
3921 _check_bv_args(a, b) 3922 a, b = _coerce_exprs(a, b) 3923 return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3926 """Create the Z3 expression (unsigned) division `self / other`.
3928 Use the operator /
for signed division.
3934 >>>
UDiv(x, y).sort()
3938 >>>
UDiv(x, y).sexpr()
3941 _check_bv_args(a, b) 3942 a, b = _coerce_exprs(a, b) 3943 return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3946 """Create the Z3 expression (unsigned) remainder `self % other`.
3948 Use the operator %
for signed modulus,
and SRem()
for signed remainder.
3954 >>>
URem(x, y).sort()
3958 >>>
URem(x, y).sexpr()
3961 _check_bv_args(a, b) 3962 a, b = _coerce_exprs(a, b) 3963 return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3966 """Create the Z3 expression signed remainder.
3968 Use the operator %
for signed modulus,
and URem()
for unsigned remainder.
3974 >>>
SRem(x, y).sort()
3978 >>>
SRem(x, y).sexpr()
3981 _check_bv_args(a, b) 3982 a, b = _coerce_exprs(a, b) 3983 return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3986 """Create the Z3 expression logical right shift.
3988 Use the operator >>
for the arithmetical right shift.
3993 >>> (x >> y).sexpr()
3995 >>>
LShR(x, y).sexpr()
4012 _check_bv_args(a, b) 4013 a, b = _coerce_exprs(a, b) 4014 return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4016 def RotateLeft(a, b): 4017 """Return an expression representing `a` rotated to the left `b` times.
4027 _check_bv_args(a, b) 4028 a, b = _coerce_exprs(a, b) 4029 return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4031 def RotateRight(a, b): 4032 """Return an expression representing `a` rotated to the right `b` times.
4042 _check_bv_args(a, b) 4043 a, b = _coerce_exprs(a, b) 4044 return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4047 """Return a bit-vector expression with `n` extra sign-bits.
4067 >>> print(
"%.x" % v.as_long())
4071 _z3_assert(_is_int(n), "First argument must be an integer") 4072 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 4073 return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 4076 """Return a bit-vector expression with `n` extra zero-bits.
4098 _z3_assert(_is_int(n), "First argument must be an integer") 4099 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 4100 return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 4102 def RepeatBitVec(n, a): 4103 """Return an expression representing `n` copies of `a`.
4112 >>> print(
"%.x" % v0.as_long())
4117 >>> print(
"%.x" % v.as_long())
4121 _z3_assert(_is_int(n), "First argument must be an integer") 4122 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 4123 return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx) 4126 """Return the reduction-
and expression of `a`.
""" 4128 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 4129 return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) 4132 """Return the reduction-
or expression of `a`.
""" 4134 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 4135 return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) 4137 def BVAddNoOverflow(a, b, signed): 4138 """A predicate the determines that bit-vector addition does
not overflow
""" 4139 _check_bv_args(a, b) 4140 a, b = _coerce_exprs(a, b) 4141 return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4143 def BVAddNoUnderflow(a, b): 4144 """A predicate the determines that signed bit-vector addition does
not underflow
""" 4145 _check_bv_args(a, b) 4146 a, b = _coerce_exprs(a, b) 4147 return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4149 def BVSubNoOverflow(a, b): 4150 """A predicate the determines that bit-vector subtraction does
not overflow
""" 4151 _check_bv_args(a, b) 4152 a, b = _coerce_exprs(a, b) 4153 return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4156 def BVSubNoUnderflow(a, b, signed): 4157 """A predicate the determines that bit-vector subtraction does
not underflow
""" 4158 _check_bv_args(a, b) 4159 a, b = _coerce_exprs(a, b) 4160 return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4162 def BVSDivNoOverflow(a, b): 4163 """A predicate the determines that bit-vector signed division does
not overflow
""" 4164 _check_bv_args(a, b) 4165 a, b = _coerce_exprs(a, b) 4166 return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4168 def BVSNegNoOverflow(a): 4169 """A predicate the determines that bit-vector unary negation does
not overflow
""" 4171 _z3_assert(is_bv(a), "Argument should be a bit-vector") 4172 return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx) 4174 def BVMulNoOverflow(a, b, signed): 4175 """A predicate the determines that bit-vector multiplication does
not overflow
""" 4176 _check_bv_args(a, b) 4177 a, b = _coerce_exprs(a, b) 4178 return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4181 def BVMulNoUnderflow(a, b): 4182 """A predicate the determines that bit-vector signed multiplication does
not underflow
""" 4183 _check_bv_args(a, b) 4184 a, b = _coerce_exprs(a, b) 4185 return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4189 ######################################### 4193 ######################################### 4195 class ArraySortRef(SortRef): 4199 """Return the domain of the array sort `self`.
4205 return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx) 4208 """Return the range of the array sort `self`.
4214 return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx) 4216 class ArrayRef(ExprRef): 4217 """Array expressions.
""" 4220 """Return the array sort of the array expression `self`.
4226 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4235 return self.sort().domain() 4244 return self.sort().range() 4246 def __getitem__(self, arg): 4247 """Return the Z3 expression `self[arg]`.
4256 arg = self.domain().cast(arg) 4257 return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx) 4260 return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx) 4264 """Return `
True`
if `a`
is a Z3 array expression.
4274 return isinstance(a, ArrayRef) 4276 def is_const_array(a): 4277 """Return `
True`
if `a`
is a Z3 constant array.
4286 return is_app_of(a, Z3_OP_CONST_ARRAY) 4289 """Return `
True`
if `a`
is a Z3 constant array.
4298 return is_app_of(a, Z3_OP_CONST_ARRAY) 4301 """Return `
True`
if `a`
is a Z3 map array expression.
4313 return is_app_of(a, Z3_OP_ARRAY_MAP) 4316 """Return `
True`
if `a`
is a Z3 default array expression.
4321 return is_app_of(a, Z3_OP_ARRAY_DEFAULT) 4323 def get_map_func(a): 4324 """Return the function declaration associated with a Z3 map array expression.
4337 _z3_assert(is_map(a), "Z3 array map expression expected.") 4338 return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx) 4340 def ArraySort(*sig): 4341 """Return the Z3 array sort with the given domain
and range sorts.
4354 sig = _get_args(sig) 4356 _z3_assert(len(sig) > 1, "At least two arguments expected") 4357 arity = len(sig) - 1 4362 _z3_assert(is_sort(s), "Z3 sort expected") 4363 _z3_assert(s.ctx == r.ctx, "Context mismatch") 4366 return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx) 4367 dom = (Sort * arity)() 4368 for i in range(arity): 4370 return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx) 4372 def Array(name, dom, rng): 4373 """Return an array constant named `name` with the given domain
and range sorts.
4381 s = ArraySort(dom, rng) 4383 return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx) 4385 def Update(a, i, v): 4386 """Return a Z3 store array expression.
4389 >>> i, v =
Ints(
'i v')
4393 >>>
prove(s[i] == v)
4400 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4401 i = a.domain().cast(i) 4402 v = a.range().cast(v) 4404 return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx) 4407 """ Return a default value
for array expression.
4413 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4418 """Return a Z3 store array expression.
4421 >>> i, v =
Ints(
'i v')
4422 >>> s =
Store(a, i, v)
4425 >>>
prove(s[i] == v)
4431 return Update(a, i, v) 4434 """Return a Z3 select array expression.
4444 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4449 """Return a Z3 map array expression.
4454 >>> b =
Map(f, a1, a2)
4457 >>>
prove(b[0] == f(a1[0], a2[0]))
4460 args = _get_args(args) 4462 _z3_assert(len(args) > 0, "At least one Z3 array expression expected") 4463 _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration") 4464 _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected") 4465 _z3_assert(len(args) == f.arity(), "Number of arguments mismatch") 4466 _args, sz = _to_ast_array(args) 4468 return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx) 4471 """Return a Z3 constant array expression.
4485 _z3_assert(is_sort(dom), "Z3 sort expected") 4488 v = _py2expr(v, ctx) 4489 return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx) 4492 """Return extensionality index
for arrays.
4495 _z3_assert(is_array(a) and is_array(b)) 4496 return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast())); 4499 """Return `
True`
if `a`
is a Z3 array select application.
4508 return is_app_of(a, Z3_OP_SELECT) 4511 """Return `
True`
if `a`
is a Z3 array store application.
4519 return is_app_of(a, Z3_OP_STORE) 4521 ######################################### 4525 ######################################### 4529 """ Create a set sort over element sort s
""" 4530 return ArraySort(s, BoolSort()) 4533 """Create the empty set
4538 return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx) 4541 """Create the full set
4546 return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx) 4548 def SetUnion(*args): 4549 """ Take the union of sets
4555 args = _get_args(args) 4556 ctx = _ctx_from_ast_arg_list(args) 4557 _args, sz = _to_ast_array(args) 4558 return ArrayRef(Z3_mk_set_union(ctx.ref(), sz, _args), ctx) 4560 def SetIntersect(*args): 4561 """ Take the union of sets
4567 args = _get_args(args) 4568 ctx = _ctx_from_ast_arg_list(args) 4569 _args, sz = _to_ast_array(args) 4570 return ArrayRef(Z3_mk_set_intersect(ctx.ref(), sz, _args), ctx) 4573 """ Add element e to set s
4578 ctx = _ctx_from_ast_arg_list([s,e]) 4579 e = _py2expr(e, ctx) 4580 return ArrayRef(Z3_mk_set_add(ctx.ref(), s.as_ast(), e.as_ast()), ctx) 4583 """ Remove element e to set s
4588 ctx = _ctx_from_ast_arg_list([s,e]) 4589 e = _py2expr(e, ctx) 4590 return ArrayRef(Z3_mk_set_del(ctx.ref(), s.as_ast(), e.as_ast()), ctx) 4592 def SetComplement(s): 4593 """ The complement of set s
4599 return ArrayRef(Z3_mk_set_complement(ctx.ref(), s.as_ast()), ctx) 4601 def SetDifference(a, b): 4602 """ The set difference of a
and b
4608 ctx = _ctx_from_ast_arg_list([a, b]) 4609 return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 4612 """ Check
if e
is a member of set s
4617 ctx = _ctx_from_ast_arg_list([s,e]) 4618 e = _py2expr(e, ctx) 4619 return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx) 4622 """ Check
if a
is a subset of b
4628 ctx = _ctx_from_ast_arg_list([a, b]) 4629 return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 4632 ######################################### 4636 ######################################### 4638 def _valid_accessor(acc): 4639 """Return `
True`
if acc
is pair of the form (String, Datatype
or Sort).
""" 4640 return isinstance(acc, tuple) and len(acc) == 2 and isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1])) 4643 """Helper
class for declaring Z3 datatypes.
4646 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4647 >>> List.declare(
'nil')
4648 >>> List = List.create()
4652 >>> List.cons(10, List.nil)
4654 >>> List.cons(10, List.nil).sort()
4656 >>> cons = List.cons
4660 >>> n = cons(1, cons(0, nil))
4662 cons(1, cons(0, nil))
4668 def __init__(self, name, ctx=None): 4669 self.ctx = _get_ctx(ctx) 4671 self.constructors = [] 4673 def __deepcopy__(self, memo={}): 4674 r = Datatype(self.name, self.ctx) 4675 r.constructors = copy.deepcopy(self.constructors) 4678 def declare_core(self, name, rec_name, *args): 4680 _z3_assert(isinstance(name, str), "String expected") 4681 _z3_assert(isinstance(rec_name, str), "String expected") 4682 _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)") 4683 self.constructors.append((name, rec_name, args)) 4685 def declare(self, name, *args): 4686 """Declare constructor named `name` with the given accessors `args`.
4687 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.
4689 In the following example `List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))`
4690 declares the constructor named `cons` that builds a new List using an integer
and a List.
4691 It also declares the accessors `car`
and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
4692 and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method
create() to create
4693 the actual datatype
in Z3.
4696 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4697 >>> List.declare(
'nil')
4698 >>> List = List.create()
4701 _z3_assert(isinstance(name, str), "String expected") 4702 _z3_assert(name != "", "Constructor name cannot be empty") 4703 return self.declare_core(name, "is-" + name, *args) 4706 return "Datatype(%s, %s)" % (self.name, self.constructors) 4709 """Create a Z3 datatype based on the constructors declared using the method `
declare()`.
4711 The function `
CreateDatatypes()` must be used to define mutually recursive datatypes.
4714 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4715 >>> List.declare(
'nil')
4716 >>> List = List.create()
4719 >>> List.cons(10, List.nil)
4722 return CreateDatatypes([self])[0] 4724 class ScopedConstructor: 4725 """Auxiliary object used to create Z3 datatypes.
""" 4726 def __init__(self, c, ctx): 4730 if self.ctx.ref() is not None: 4731 Z3_del_constructor(self.ctx.ref(), self.c) 4733 class ScopedConstructorList: 4734 """Auxiliary object used to create Z3 datatypes.
""" 4735 def __init__(self, c, ctx): 4739 if self.ctx.ref() is not None: 4740 Z3_del_constructor_list(self.ctx.ref(), self.c) 4742 def CreateDatatypes(*ds): 4743 """Create mutually recursive Z3 datatypes using 1
or more Datatype helper objects.
4745 In the following example we define a Tree-List using two mutually recursive datatypes.
4747 >>> TreeList =
Datatype(
'TreeList')
4750 >>> Tree.declare(
'leaf', (
'val',
IntSort()))
4752 >>> Tree.declare(
'node', (
'children', TreeList))
4753 >>> TreeList.declare(
'nil')
4754 >>> TreeList.declare(
'cons', (
'car', Tree), (
'cdr', TreeList))
4756 >>> Tree.val(Tree.leaf(10))
4758 >>>
simplify(Tree.val(Tree.leaf(10)))
4760 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4762 node(cons(leaf(10), cons(leaf(20), nil)))
4763 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4766 >>>
simplify(TreeList.car(Tree.children(n2)) == n1)
4771 _z3_assert(len(ds) > 0, "At least one Datatype must be specified") 4772 _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes") 4773 _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch") 4774 _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected") 4777 names = (Symbol * num)() 4778 out = (Sort * num)() 4779 clists = (ConstructorList * num)() 4781 for i in range(num): 4783 names[i] = to_symbol(d.name, ctx) 4784 num_cs = len(d.constructors) 4785 cs = (Constructor * num_cs)() 4786 for j in range(num_cs): 4787 c = d.constructors[j] 4788 cname = to_symbol(c[0], ctx) 4789 rname = to_symbol(c[1], ctx) 4792 fnames = (Symbol * num_fs)() 4793 sorts = (Sort * num_fs)() 4794 refs = (ctypes.c_uint * num_fs)() 4795 for k in range(num_fs): 4798 fnames[k] = to_symbol(fname, ctx) 4799 if isinstance(ftype, Datatype): 4801 _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected") 4803 refs[k] = ds.index(ftype) 4806 _z3_assert(is_sort(ftype), "Z3 sort expected") 4807 sorts[k] = ftype.ast 4809 cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs) 4810 to_delete.append(ScopedConstructor(cs[j], ctx)) 4811 clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs) 4812 to_delete.append(ScopedConstructorList(clists[i], ctx)) 4813 Z3_mk_datatypes(ctx.ref(), num, names, out, clists) 4815 ## Create a field for every constructor, recognizer and accessor 4816 for i in range(num): 4817 dref = DatatypeSortRef(out[i], ctx) 4818 num_cs = dref.num_constructors() 4819 for j in range(num_cs): 4820 cref = dref.constructor(j) 4821 cref_name = cref.name() 4822 cref_arity = cref.arity() 4823 if cref.arity() == 0: 4825 setattr(dref, cref_name, cref) 4826 rref = dref.recognizer(j) 4827 setattr(dref, "is_" + cref_name, rref) 4828 for k in range(cref_arity): 4829 aref = dref.accessor(j, k) 4830 setattr(dref, aref.name(), aref) 4832 return tuple(result) 4834 class DatatypeSortRef(SortRef): 4835 """Datatype sorts.
""" 4836 def num_constructors(self): 4837 """Return the number of constructors
in the given Z3 datatype.
4840 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4841 >>> List.declare(
'nil')
4842 >>> List = List.create()
4844 >>> List.num_constructors()
4847 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast)) 4849 def constructor(self, idx): 4850 """Return a constructor of the datatype `self`.
4853 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4854 >>> List.declare(
'nil')
4855 >>> List = List.create()
4857 >>> List.num_constructors()
4859 >>> List.constructor(0)
4861 >>> List.constructor(1)
4865 _z3_assert(idx < self.num_constructors(), "Invalid constructor index") 4866 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx) 4868 def recognizer(self, idx): 4869 """In Z3, each constructor has an associated recognizer predicate.
4871 If the constructor
is named `name`, then the recognizer `is_name`.
4874 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4875 >>> List.declare(
'nil')
4876 >>> List = List.create()
4878 >>> List.num_constructors()
4880 >>> List.recognizer(0)
4882 >>> List.recognizer(1)
4884 >>>
simplify(List.is_nil(List.cons(10, List.nil)))
4886 >>>
simplify(List.is_cons(List.cons(10, List.nil)))
4888 >>> l =
Const(
'l', List)
4893 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index") 4894 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx) 4896 def accessor(self, i, j): 4897 """In Z3, each constructor has 0
or more accessor. The number of accessors
is equal to the arity of the constructor.
4900 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4901 >>> List.declare(
'nil')
4902 >>> List = List.create()
4903 >>> List.num_constructors()
4905 >>> List.constructor(0)
4907 >>> num_accs = List.constructor(0).arity()
4910 >>> List.accessor(0, 0)
4912 >>> List.accessor(0, 1)
4914 >>> List.constructor(1)
4916 >>> num_accs = List.constructor(1).arity()
4921 _z3_assert(i < self.num_constructors(), "Invalid constructor index") 4922 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index") 4923 return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx) 4925 class DatatypeRef(ExprRef): 4926 """Datatype expressions.
""" 4928 """Return the datatype sort of the datatype expression `self`.
""" 4929 return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4931 def EnumSort(name, values, ctx=None): 4932 """Return a new enumeration sort named `name` containing the given values.
4934 The result
is a pair (sort, list of constants).
4936 >>> Color, (red, green, blue) =
EnumSort(
'Color', [
'red',
'green',
'blue'])
4939 _z3_assert(isinstance(name, str), "Name must be a string") 4940 _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings") 4941 _z3_assert(len(values) > 0, "At least one value expected") 4944 _val_names = (Symbol * num)() 4945 for i in range(num): 4946 _val_names[i] = to_symbol(values[i]) 4947 _values = (FuncDecl * num)() 4948 _testers = (FuncDecl * num)() 4949 name = to_symbol(name) 4950 S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx) 4952 for i in range(num): 4953 V.append(FuncDeclRef(_values[i], ctx)) 4954 V = [a() for a in V] 4957 ######################################### 4961 ######################################### 4964 """Set of parameters used to configure Solvers, Tactics
and Simplifiers
in Z3.
4966 Consider using the function `args2params` to create instances of this object.
4968 def __init__(self, ctx=None, params=None): 4969 self.ctx = _get_ctx(ctx) 4971 self.params = Z3_mk_params(self.ctx.ref()) 4973 self.params = params 4974 Z3_params_inc_ref(self.ctx.ref(), self.params) 4976 def __deepcopy__(self, memo={}): 4977 return ParamsRef(self.ctx, self.params) 4980 if self.ctx.ref() is not None: 4981 Z3_params_dec_ref(self.ctx.ref(), self.params) 4983 def set(self, name, val): 4984 """Set parameter name with value val.
""" 4986 _z3_assert(isinstance(name, str), "parameter name must be a string") 4987 name_sym = to_symbol(name, self.ctx) 4988 if isinstance(val, bool): 4989 Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val) 4991 Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val) 4992 elif isinstance(val, float): 4993 Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val) 4994 elif isinstance(val, str): 4995 Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx)) 4998 _z3_assert(False, "invalid parameter value") 5001 return Z3_params_to_string(self.ctx.ref(), self.params) 5003 def validate(self, ds): 5004 _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected") 5005 Z3_params_validate(self.ctx.ref(), self.params, ds.descr) 5007 def args2params(arguments, keywords, ctx=None): 5008 """Convert python arguments into a Z3_params object.
5009 A
':' is added to the keywords,
and '_' is replaced with
'-' 5011 >>>
args2params([
'model',
True,
'relevancy', 2], {
'elim_and' :
True})
5012 (params model true relevancy 2 elim_and true)
5015 _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") 5029 class ParamDescrsRef: 5030 """Set of parameter descriptions
for Solvers, Tactics
and Simplifiers
in Z3.
5032 def __init__(self, descr, ctx=None): 5033 _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected") 5034 self.ctx = _get_ctx(ctx) 5036 Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr) 5038 def __deepcopy__(self, memo={}): 5039 return ParamsDescrsRef(self.descr, self.ctx) 5042 if self.ctx.ref() is not None: 5043 Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr) 5046 """Return the size of
in the parameter description `self`.
5048 return int(Z3_param_descrs_size(self.ctx.ref(), self.descr)) 5051 """Return the size of
in the parameter description `self`.
5055 def get_name(self, i): 5056 """Return the i-th parameter name
in the parameter description `self`.
5058 return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i)) 5060 def get_kind(self, n): 5061 """Return the kind of the parameter named `n`.
5063 return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 5065 def get_documentation(self, n): 5066 """Return the documentation string of the parameter named `n`.
5068 return Z3_param_descrs_get_documentation(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 5070 def __getitem__(self, arg): 5072 return self.get_name(arg) 5074 return self.get_kind(arg) 5077 return Z3_param_descrs_to_string(self.ctx.ref(), self.descr) 5079 ######################################### 5083 ######################################### 5085 class Goal(Z3PPObject): 5086 """Goal
is a collection of constraints we want to find a solution
or show to be unsatisfiable (infeasible).
5088 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
5089 A goal has a solution
if one of its subgoals has a solution.
5090 A goal
is unsatisfiable
if all subgoals are unsatisfiable.
5093 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None): 5095 _z3_assert(goal is None or ctx is not None, "If goal is different from None, then ctx must be also different from None") 5096 self.ctx = _get_ctx(ctx) 5098 if self.goal is None: 5099 self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs) 5100 Z3_goal_inc_ref(self.ctx.ref(), self.goal) 5102 def __deepcopy__(self, memo={}): 5103 return Goal(False, False, False, self.ctx, self.goal) 5106 if self.goal is not None and self.ctx.ref() is not None: 5107 Z3_goal_dec_ref(self.ctx.ref(), self.goal) 5110 """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
5112 >>> x, y =
Ints(
'x y')
5114 >>> g.add(x == 0, y >= x + 1)
5117 >>> r =
Then(
'simplify',
'solve-eqs')(g)
5124 return int(Z3_goal_depth(self.ctx.ref(), self.goal)) 5126 def inconsistent(self): 5127 """Return `
True`
if `self` contains the `
False` constraints.
5129 >>> x, y =
Ints(
'x y')
5131 >>> g.inconsistent()
5133 >>> g.add(x == 0, x == 1)
5136 >>> g.inconsistent()
5138 >>> g2 =
Tactic(
'propagate-values')(g)[0]
5139 >>> g2.inconsistent()
5142 return Z3_goal_inconsistent(self.ctx.ref(), self.goal) 5145 """Return the precision (under-approximation, over-approximation,
or precise) of the goal `self`.
5148 >>> g.prec() == Z3_GOAL_PRECISE
5150 >>> x, y =
Ints(
'x y')
5151 >>> g.add(x == y + 1)
5152 >>> g.prec() == Z3_GOAL_PRECISE
5154 >>> t =
With(
Tactic(
'add-bounds'), add_bound_lower=0, add_bound_upper=10)
5157 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
5158 >>> g2.prec() == Z3_GOAL_PRECISE
5160 >>> g2.prec() == Z3_GOAL_UNDER
5163 return Z3_goal_precision(self.ctx.ref(), self.goal) 5165 def precision(self): 5166 """Alias
for `
prec()`.
5169 >>> g.precision() == Z3_GOAL_PRECISE
5175 """Return the number of constraints
in the goal `self`.
5180 >>> x, y =
Ints(
'x y')
5181 >>> g.add(x == 0, y > x)
5185 return int(Z3_goal_size(self.ctx.ref(), self.goal)) 5188 """Return the number of constraints
in the goal `self`.
5193 >>> x, y =
Ints(
'x y')
5194 >>> g.add(x == 0, y > x)
5201 """Return a constraint
in the goal `self`.
5204 >>> x, y =
Ints(
'x y')
5205 >>> g.add(x == 0, y > x)
5211 return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx) 5213 def __getitem__(self, arg): 5214 """Return a constraint
in the goal `self`.
5217 >>> x, y =
Ints(
'x y')
5218 >>> g.add(x == 0, y > x)
5224 if arg >= len(self): 5226 return self.get(arg) 5228 def assert_exprs(self, *args): 5229 """Assert constraints into the goal.
5233 >>> g.assert_exprs(x > 0, x < 2)
5237 args = _get_args(args) 5238 s = BoolSort(self.ctx) 5241 Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast()) 5243 def append(self, *args): 5248 >>> g.append(x > 0, x < 2)
5252 self.assert_exprs(*args) 5254 def insert(self, *args): 5259 >>> g.insert(x > 0, x < 2)
5263 self.assert_exprs(*args) 5265 def add(self, *args): 5270 >>> g.add(x > 0, x < 2)
5274 self.assert_exprs(*args) 5276 def convert_model(self, model): 5277 """Retrieve model
from a satisfiable goal
5278 >>> a, b =
Ints(
'a b')
5280 >>> g.add(
Or(a == 0, a == 1),
Or(b == 0, b == 1), a > b)
5284 [
Or(b == 0, b == 1),
Not(0 <= b)]
5286 [
Or(b == 0, b == 1),
Not(1 <= b)]
5302 _z3_assert(isinstance(model, ModelRef), "Z3 Model expected") 5303 return ModelRef(Z3_goal_convert_model(self.ctx.ref(), self.goal, model.model), self.ctx) 5306 return obj_to_string(self) 5309 """Return a textual representation of the s-expression representing the goal.
""" 5310 return Z3_goal_to_string(self.ctx.ref(), self.goal) 5313 """Return a textual representation of the goal
in DIMACS format.
""" 5314 return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal) 5316 def translate(self, target): 5317 """Copy goal `self` to context `target`.
5325 >>> g2 = g.translate(c2)
5336 _z3_assert(isinstance(target, Context), "target must be a context") 5337 return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target) 5340 return self.translate(self.ctx) 5342 def __deepcopy__(self): 5343 return self.translate(self.ctx) 5345 def simplify(self, *arguments, **keywords): 5346 """Return a new simplified goal.
5348 This method
is essentially invoking the simplify tactic.
5352 >>> g.add(x + 1 >= 2)
5355 >>> g2 = g.simplify()
5362 t = Tactic('simplify') 5363 return t.apply(self, *arguments, **keywords)[0] 5366 """Return goal `self`
as a single Z3 expression.
5381 return BoolVal(True, self.ctx) 5385 return And([ self.get(i) for i in range(len(self)) ], self.ctx) 5387 ######################################### 5391 ######################################### 5392 class AstVector(Z3PPObject): 5393 """A collection (vector) of ASTs.
""" 5395 def __init__(self, v=None, ctx=None): 5398 self.ctx = _get_ctx(ctx) 5399 self.vector = Z3_mk_ast_vector(self.ctx.ref()) 5402 assert ctx is not None 5404 Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector) 5406 def __deepcopy__(self, memo={}): 5407 return AstVector(self.vector, self.ctx) 5410 if self.vector is not None and self.ctx.ref() is not None: 5411 Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector) 5414 """Return the size of the vector `self`.
5419 >>> A.push(
Int(
'x'))
5420 >>> A.push(
Int(
'x'))
5424 return int(Z3_ast_vector_size(self.ctx.ref(), self.vector)) 5426 def __getitem__(self, i): 5427 """Return the AST at position `i`.
5430 >>> A.push(
Int(
'x') + 1)
5431 >>> A.push(
Int(
'y'))
5438 if isinstance(i, int): 5442 if i >= self.__len__(): 5444 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx) 5446 elif isinstance(i, slice): 5447 return [_to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, ii), self.ctx) for ii in range(*i.indices(self.__len__()))] 5450 def __setitem__(self, i, v): 5451 """Update AST at position `i`.
5454 >>> A.push(
Int(
'x') + 1)
5455 >>> A.push(
Int(
'y'))
5462 if i >= self.__len__(): 5464 Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast()) 5467 """Add `v`
in the end of the vector.
5472 >>> A.push(
Int(
'x'))
5476 Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast()) 5478 def resize(self, sz): 5479 """Resize the vector to `sz` elements.
5485 >>>
for i
in range(10): A[i] =
Int(
'x')
5489 Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz) 5491 def __contains__(self, item): 5492 """Return `
True`
if the vector contains `item`.
5514 def translate(self, other_ctx): 5515 """Copy vector `self` to context `other_ctx`.
5521 >>> B = A.translate(c2)
5525 return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx) 5528 return self.translate(self.ctx) 5530 def __deepcopy__(self): 5531 return self.translate(self.ctx) 5534 return obj_to_string(self) 5537 """Return a textual representation of the s-expression representing the vector.
""" 5538 return Z3_ast_vector_to_string(self.ctx.ref(), self.vector) 5540 ######################################### 5544 ######################################### 5546 """A mapping
from ASTs to ASTs.
""" 5548 def __init__(self, m=None, ctx=None): 5551 self.ctx = _get_ctx(ctx) 5552 self.map = Z3_mk_ast_map(self.ctx.ref()) 5555 assert ctx is not None 5557 Z3_ast_map_inc_ref(self.ctx.ref(), self.map) 5559 def __deepcopy__(self, memo={}): 5560 return AstMap(self.map, self.ctx) 5563 if self.map is not None and self.ctx.ref() is not None: 5564 Z3_ast_map_dec_ref(self.ctx.ref(), self.map) 5567 """Return the size of the map.
5577 return int(Z3_ast_map_size(self.ctx.ref(), self.map)) 5579 def __contains__(self, key): 5580 """Return `
True`
if the map contains key `key`.
5590 return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast()) 5592 def __getitem__(self, key): 5593 """Retrieve the value associated with key `key`.
5601 return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx) 5603 def __setitem__(self, k, v): 5604 """Add/Update key `k` with value `v`.
5617 Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast()) 5620 return Z3_ast_map_to_string(self.ctx.ref(), self.map) 5623 """Remove the entry associated with key `k`.
5634 Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast()) 5637 """Remove all entries
from the map.
5649 Z3_ast_map_reset(self.ctx.ref(), self.map) 5652 """Return an AstVector containing all keys
in the map.
5661 return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx) 5663 ######################################### 5667 ######################################### 5670 """Store the value of the interpretation of a function
in a particular point.
""" 5672 def __init__(self, entry, ctx): 5675 Z3_func_entry_inc_ref(self.ctx.ref(), self.entry) 5677 def __deepcopy__(self, memo={}): 5678 return FuncEntry(self.entry, self.ctx) 5681 if self.ctx.ref() is not None: 5682 Z3_func_entry_dec_ref(self.ctx.ref(), self.entry) 5685 """Return the number of arguments
in the given entry.
5689 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5694 >>> f_i.num_entries()
5696 >>> e = f_i.entry(0)
5700 return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry)) 5702 def arg_value(self, idx): 5703 """Return the value of argument `idx`.
5707 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5712 >>> f_i.num_entries()
5714 >>> e = f_i.entry(0)
5725 ...
except IndexError:
5726 ... print(
"index error")
5729 if idx >= self.num_args(): 5731 return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx) 5734 """Return the value of the function at point `self`.
5738 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5743 >>> f_i.num_entries()
5745 >>> e = f_i.entry(0)
5753 return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx) 5756 """Return entry `self`
as a Python list.
5759 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5764 >>> f_i.num_entries()
5766 >>> e = f_i.entry(0)
5770 args = [ self.arg_value(i) for i in range(self.num_args())] 5771 args.append(self.value()) 5775 return repr(self.as_list()) 5777 class FuncInterp(Z3PPObject): 5778 """Stores the interpretation of a function
in a Z3 model.
""" 5780 def __init__(self, f, ctx): 5783 if self.f is not None: 5784 Z3_func_interp_inc_ref(self.ctx.ref(), self.f) 5786 def __deepcopy__(self, memo={}): 5787 return FuncInterp(self.f, self.ctx) 5790 if self.f is not None and self.ctx.ref() is not None: 5791 Z3_func_interp_dec_ref(self.ctx.ref(), self.f) 5793 def else_value(self): 5795 Return the `
else` value
for a function interpretation.
5796 Return
None if Z3 did
not specify the `
else` value
for 5801 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5810 r = Z3_func_interp_get_else(self.ctx.ref(), self.f) 5812 return _to_expr_ref(r, self.ctx) 5816 def num_entries(self): 5817 """Return the number of entries/points
in the function interpretation `self`.
5821 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5830 return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f)) 5833 """Return the number of arguments
for each entry
in the function interpretation `self`.
5837 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5844 return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f)) 5846 def entry(self, idx): 5847 """Return an entry at position `idx < self.
num_entries()`
in the function interpretation `self`.
5851 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5862 if idx >= self.num_entries(): 5864 return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx) 5866 def translate(self, other_ctx): 5867 """Copy model
'self' to context
'other_ctx'.
5869 return ModelRef(Z3_model_translate(self.ctx.ref(), self.model, other_ctx.ref()), other_ctx) 5872 return self.translate(self.ctx) 5874 def __deepcopy__(self): 5875 return self.translate(self.ctx) 5878 """Return the function interpretation
as a Python list.
5881 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5890 r = [ self.entry(i).as_list() for i in range(self.num_entries())] 5891 r.append(self.else_value()) 5895 return obj_to_string(self) 5897 class ModelRef(Z3PPObject): 5898 """Model/Solution of a satisfiability problem (aka system of constraints).
""" 5900 def __init__(self, m, ctx): 5901 assert ctx is not None 5904 Z3_model_inc_ref(self.ctx.ref(), self.model) 5907 if self.ctx.ref() is not None: 5908 Z3_model_dec_ref(self.ctx.ref(), self.model) 5911 return obj_to_string(self) 5914 """Return a textual representation of the s-expression representing the model.
""" 5915 return Z3_model_to_string(self.ctx.ref(), self.model) 5917 def eval(self, t, model_completion=False): 5918 """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`.
5922 >>> s.add(x > 0, x < 2)
5935 >>> m.eval(y, model_completion=
True)
5942 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r): 5943 return _to_expr_ref(r[0], self.ctx) 5944 raise Z3Exception("failed to evaluate expression in the model") 5946 def evaluate(self, t, model_completion=False): 5947 """Alias
for `eval`.
5951 >>> s.add(x > 0, x < 2)
5955 >>> m.evaluate(x + 1)
5957 >>> m.evaluate(x == 1)
5960 >>> m.evaluate(y + x)
5964 >>> m.evaluate(y, model_completion=
True)
5967 >>> m.evaluate(y + x)
5970 return self.eval(t, model_completion) 5973 """Return the number of constant
and function declarations
in the model `self`.
5978 >>> s.add(x > 0, f(x) != x)
5985 return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model)) 5987 def get_interp(self, decl): 5988 """Return the interpretation
for a given declaration
or constant.
5993 >>> s.add(x > 0, x < 2, f(x) == 0)
6003 _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected") 6007 if decl.arity() == 0: 6008 _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast) 6009 if _r.value is None: 6011 r = _to_expr_ref(_r, self.ctx) 6013 return self.get_interp(get_as_array_func(r)) 6017 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) 6021 def num_sorts(self): 6022 """Return the number of uninterpreted sorts that contain an interpretation
in the model `self`.
6025 >>> a, b =
Consts(
'a b', A)
6034 return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model)) 6036 def get_sort(self, idx): 6037 """Return the uninterpreted sort at position `idx` < self.
num_sorts().
6041 >>> a1, a2 =
Consts(
'a1 a2', A)
6042 >>> b1, b2 =
Consts(
'b1 b2', B)
6044 >>> s.add(a1 != a2, b1 != b2)
6055 if idx >= self.num_sorts(): 6057 return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx) 6060 """Return all uninterpreted sorts that have an interpretation
in the model `self`.
6064 >>> a1, a2 =
Consts(
'a1 a2', A)
6065 >>> b1, b2 =
Consts(
'b1 b2', B)
6067 >>> s.add(a1 != a2, b1 != b2)
6074 return [ self.get_sort(i) for i in range(self.num_sorts()) ] 6076 def get_universe(self, s): 6077 """Return the interpretation
for the uninterpreted sort `s`
in the model `self`.
6080 >>> a, b =
Consts(
'a b', A)
6086 >>> m.get_universe(A)
6090 _z3_assert(isinstance(s, SortRef), "Z3 sort expected") 6092 return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx) 6096 def __getitem__(self, idx): 6097 """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.
6099 The elements can be retrieved using position
or the actual declaration.
6104 >>> s.add(x > 0, x < 2, f(x) == 0)
6118 >>>
for d
in m: print(
"%s -> %s" % (d, m[d]))
6123 if idx >= len(self): 6125 num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model) 6126 if (idx < num_consts): 6127 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx) 6129 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx) 6130 if isinstance(idx, FuncDeclRef): 6131 return self.get_interp(idx) 6133 return self.get_interp(idx.decl()) 6134 if isinstance(idx, SortRef): 6135 return self.get_universe(idx) 6137 _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected") 6141 """Return a list with all symbols that have an interpretation
in the model `self`.
6145 >>> s.add(x > 0, x < 2, f(x) == 0)
6153 for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)): 6154 r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx)) 6155 for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)): 6156 r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx)) 6159 def translate(self, target): 6160 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
6163 _z3_assert(isinstance(target, Context), "argument must be a Z3 context") 6164 model = Z3_model_translate(self.ctx.ref(), self.model, target.ref()) 6165 return Model(model, target) 6168 return self.translate(self.ctx) 6170 def __deepcopy__(self): 6171 return self.translate(self.ctx) 6173 def Model(ctx = None): 6175 return ModelRef(Z3_mk_model(ctx.ref()), ctx) 6178 """Return true
if n
is a Z3 expression of the form (_
as-array f).
""" 6179 return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast()) 6181 def get_as_array_func(n): 6182 """Return the function declaration f associated with a Z3 expression of the form (_
as-array f).
""" 6184 _z3_assert(is_as_array(n), "as-array Z3 expression expected.") 6185 return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx) 6187 ######################################### 6191 ######################################### 6193 """Statistics
for `Solver.check()`.
""" 6195 def __init__(self, stats, ctx): 6198 Z3_stats_inc_ref(self.ctx.ref(), self.stats) 6200 def __deepcopy__(self, memo={}): 6201 return Statistics(self.stats, self.ctx) 6204 if self.ctx.ref() is not None: 6205 Z3_stats_dec_ref(self.ctx.ref(), self.stats) 6211 out.write(u('<table border="1" cellpadding="2" cellspacing="0">')) 6214 out.write(u('<tr style="background-color:#CFCFCF">')) 6217 out.write(u('<tr>')) 6219 out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v))) 6220 out.write(u('</table>')) 6221 return out.getvalue() 6223 return Z3_stats_to_string(self.ctx.ref(), self.stats) 6226 """Return the number of statistical counters.
6229 >>> s =
Then(
'simplify',
'nlsat').solver()
6233 >>> st = s.statistics()
6237 return int(Z3_stats_size(self.ctx.ref(), self.stats)) 6239 def __getitem__(self, idx): 6240 """Return the value of statistical counter at position `idx`. The result
is a pair (key, value).
6243 >>> s =
Then(
'simplify',
'nlsat').solver()
6247 >>> st = s.statistics()
6251 (
'nlsat propagations', 2)
6255 if idx >= len(self): 6257 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 6258 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 6260 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 6261 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val) 6264 """Return the list of statistical counters.
6267 >>> s =
Then(
'simplify',
'nlsat').solver()
6271 >>> st = s.statistics()
6273 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))] 6275 def get_key_value(self, key): 6276 """Return the value of a particular statistical counter.
6279 >>> s =
Then(
'simplify',
'nlsat').solver()
6283 >>> st = s.statistics()
6284 >>> st.get_key_value(
'nlsat propagations')
6287 for idx in range(len(self)): 6288 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx): 6289 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 6290 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 6292 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 6293 raise Z3Exception("unknown key") 6295 def __getattr__(self, name): 6296 """Access the value of statistical using attributes.
6298 Remark: to access a counter containing blank spaces (e.g.,
'nlsat propagations'),
6299 we should use
'_' (e.g.,
'nlsat_propagations').
6302 >>> s =
Then(
'simplify',
'nlsat').solver()
6306 >>> st = s.statistics()
6307 >>> st.nlsat_propagations
6312 key = name.replace('_', ' ') 6314 return self.get_key_value(key) 6316 raise AttributeError 6318 ######################################### 6322 ######################################### 6323 class CheckSatResult: 6324 """Represents the result of a satisfiability check: sat, unsat, unknown.
6330 >>> isinstance(r, CheckSatResult)
6334 def __init__(self, r): 6337 def __deepcopy__(self, memo={}): 6338 return CheckSatResult(self.r) 6340 def __eq__(self, other): 6341 return isinstance(other, CheckSatResult) and self.r == other.r 6343 def __ne__(self, other): 6344 return not self.__eq__(other) 6348 if self.r == Z3_L_TRUE: 6350 elif self.r == Z3_L_FALSE: 6351 return "<b>unsat</b>" 6353 return "<b>unknown</b>" 6355 if self.r == Z3_L_TRUE: 6357 elif self.r == Z3_L_FALSE: 6362 sat = CheckSatResult(Z3_L_TRUE) 6363 unsat = CheckSatResult(Z3_L_FALSE) 6364 unknown = CheckSatResult(Z3_L_UNDEF) 6366 class Solver(Z3PPObject): 6367 """Solver API provides methods
for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.
""" 6369 def __init__(self, solver=None, ctx=None): 6370 assert solver is None or ctx is not None 6371 self.ctx = _get_ctx(ctx) 6372 self.backtrack_level = 4000000000 6375 self.solver = Z3_mk_solver(self.ctx.ref()) 6377 self.solver = solver 6378 Z3_solver_inc_ref(self.ctx.ref(), self.solver) 6381 if self.solver is not None and self.ctx.ref() is not None: 6382 Z3_solver_dec_ref(self.ctx.ref(), self.solver) 6384 def set(self, *args, **keys): 6385 """Set a configuration option. The method `
help()`
return a string containing all available options.
6389 >>> s.set(mbqi=
True)
6390 >>> s.set(
'MBQI',
True)
6391 >>> s.set(
':mbqi',
True)
6393 p = args2params(args, keys, self.ctx) 6394 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params) 6397 """Create a backtracking point.
6416 Z3_solver_push(self.ctx.ref(), self.solver) 6418 def pop(self, num=1): 6419 """Backtrack \c num backtracking points.
6438 Z3_solver_pop(self.ctx.ref(), self.solver, num) 6440 def num_scopes(self): 6441 """Return the current number of backtracking points.
6456 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver) 6459 """Remove all asserted constraints
and backtracking points created using `
push()`.
6470 Z3_solver_reset(self.ctx.ref(), self.solver) 6472 def assert_exprs(self, *args): 6473 """Assert constraints into the solver.
6477 >>> s.assert_exprs(x > 0, x < 2)
6481 args = _get_args(args) 6482 s = BoolSort(self.ctx) 6484 if isinstance(arg, Goal) or isinstance(arg, AstVector): 6486 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast()) 6489 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast()) 6491 def add(self, *args): 6492 """Assert constraints into the solver.
6496 >>> s.add(x > 0, x < 2)
6500 self.assert_exprs(*args) 6502 def __iadd__(self, fml): 6506 def append(self, *args): 6507 """Assert constraints into the solver.
6511 >>> s.append(x > 0, x < 2)
6515 self.assert_exprs(*args) 6517 def insert(self, *args): 6518 """Assert constraints into the solver.
6522 >>> s.insert(x > 0, x < 2)
6526 self.assert_exprs(*args) 6528 def assert_and_track(self, a, p): 6529 """Assert constraint `a`
and track it
in the unsat core using the Boolean constant `p`.
6531 If `p`
is a string, it will be automatically converted into a Boolean constant.
6536 >>> s.set(unsat_core=
True)
6537 >>> s.assert_and_track(x > 0,
'p1')
6538 >>> s.assert_and_track(x != 1,
'p2')
6539 >>> s.assert_and_track(x < 0, p3)
6540 >>> print(s.check())
6542 >>> c = s.unsat_core()
6552 if isinstance(p, str): 6553 p = Bool(p, self.ctx) 6554 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected") 6555 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected") 6556 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast()) 6558 def check(self, *assumptions): 6559 """Check whether the assertions
in the given solver plus the optional assumptions are consistent
or not.
6565 >>> s.add(x > 0, x < 2)
6568 >>> s.model().eval(x)
6574 >>> s.add(2**x == 4)
6578 assumptions = _get_args(assumptions) 6579 num = len(assumptions) 6580 _assumptions = (Ast * num)() 6581 for i in range(num): 6582 _assumptions[i] = assumptions[i].as_ast() 6583 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions) 6584 return CheckSatResult(r) 6587 """Return a model
for the last `
check()`.
6589 This function raises an exception
if 6590 a model
is not available (e.g., last `
check()` returned unsat).
6594 >>> s.add(a + 2 == 0)
6601 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx) 6603 raise Z3Exception("model is not available") 6605 def unsat_core(self): 6606 """Return a subset (
as an AST vector) of the assumptions provided to the last
check().
6608 These are the assumptions Z3 used
in the unsatisfiability proof.
6609 Assumptions are available
in Z3. They are used to extract unsatisfiable cores.
6610 They may be also used to
"retract" assumptions. Note that, assumptions are
not really
6611 "soft constraints", but they can be used to implement them.
6613 >>> p1, p2, p3 =
Bools(
'p1 p2 p3')
6614 >>> x, y =
Ints(
'x y')
6619 >>> s.add(
Implies(p3, y > -3))
6620 >>> s.check(p1, p2, p3)
6622 >>> core = s.unsat_core()
6635 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx) 6637 def consequences(self, assumptions, variables): 6638 """Determine fixed values
for the variables based on the solver state
and assumptions.
6640 >>> a, b, c, d =
Bools(
'a b c d')
6642 >>> s.consequences([a],[b,c,d])
6644 >>> s.consequences([
Not(c),d],[a,b,c,d])
6647 if isinstance(assumptions, list): 6648 _asms = AstVector(None, self.ctx) 6649 for a in assumptions: 6652 if isinstance(variables, list): 6653 _vars = AstVector(None, self.ctx) 6657 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected") 6658 _z3_assert(isinstance(variables, AstVector), "ast vector expected") 6659 consequences = AstVector(None, self.ctx) 6660 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector) 6661 sz = len(consequences) 6662 consequences = [ consequences[i] for i in range(sz) ] 6663 return CheckSatResult(r), consequences 6665 def from_file(self, filename): 6666 """Parse assertions
from a file
""" 6668 Z3_solver_from_file(self.ctx.ref(), self.solver, filename) 6669 except Z3Exception as e: 6670 _handle_parse_error(e, self.ctx) 6672 def from_string(self, s): 6673 """Parse assertions
from a string
""" 6675 Z3_solver_from_string(self.ctx.ref(), self.solver, s) 6676 except Z3Exception as e: 6677 _handle_parse_error(e, self.ctx) 6679 def cube(self, vars = None): 6681 The method takes an optional set of variables that restrict which
6682 variables may be used
as a starting point
for cubing.
6683 If vars
is not None, then the first case split
is based on a variable
in 6686 self.cube_vs = AstVector(None, self.ctx) 6687 if vars is not None: 6689 self.cube_vs.push(v) 6691 lvl = self.backtrack_level 6692 self.backtrack_level = 4000000000 6693 r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx) 6694 if (len(r) == 1 and is_false(r[0])): 6700 def cube_vars(self): 6701 """Access the set of variables that were touched by the most recently generated cube.
6702 This set of variables can be used
as a starting point
for additional cubes.
6703 The idea
is that variables that appear
in clauses that are reduced by the most recent
6704 cube are likely more useful to cube on.
""" 6708 """Return a proof
for the last `
check()`. Proof construction must be enabled.
""" 6709 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx) 6711 def assertions(self): 6712 """Return an AST vector containing all added constraints.
6723 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx) 6726 """Return an AST vector containing all currently inferred units.
6728 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx) 6730 def non_units(self): 6731 """Return an AST vector containing all atomic formulas
in solver state that are
not units.
6733 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx) 6735 def statistics(self): 6736 """Return statistics
for the last `
check()`.
6743 >>> st = s.statistics()
6744 >>> st.get_key_value(
'final checks')
6751 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx) 6753 def reason_unknown(self): 6754 """Return a string describing why the last `
check()` returned `unknown`.
6758 >>> s.add(2**x == 4)
6761 >>> s.reason_unknown()
6762 '(incomplete (theory arithmetic))' 6764 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver) 6767 """Display a string describing all available options.
""" 6768 print(Z3_solver_get_help(self.ctx.ref(), self.solver)) 6770 def param_descrs(self): 6771 """Return the parameter description set.
""" 6772 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx) 6775 """Return a formatted string with all added constraints.
""" 6776 return obj_to_string(self) 6778 def translate(self, target): 6779 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
6784 >>> s2 = s1.translate(c2)
6787 _z3_assert(isinstance(target, Context), "argument must be a Z3 context") 6788 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) 6789 return Solver(solver, target) 6792 return self.translate(self.ctx) 6794 def __deepcopy__(self): 6795 return self.translate(self.ctx) 6798 """Return a formatted string (
in Lisp-like format) with all added constraints. We say the string
is in s-expression format.
6806 return Z3_solver_to_string(self.ctx.ref(), self.solver) 6809 """return SMTLIB2 formatted benchmark
for solver
's assertions""" 6816 for i
in range(sz1):
6817 v[i] = es[i].as_ast()
6819 e = es[sz1].as_ast()
6825 """Create a solver customized for the given logic. 6827 The parameter `logic` is a string. It should be contains 6828 the name of a SMT-LIB logic. 6829 See http://www.smtlib.org/ for the name of all available logics. 6831 >>> s = SolverFor("QF_LIA") 6845 """Return a simple general purpose solver with limited amount of preprocessing. 6847 >>> s = SimpleSolver() 6863 """Fixedpoint API provides methods for solving with recursive predicates""" 6866 assert fixedpoint
is None or ctx
is not None 6869 if fixedpoint
is None:
6880 if self.
fixedpoint is not None and self.
ctx.ref()
is not None:
6884 """Set a configuration option. The method `help()` return a string containing all available options. 6890 """Display a string describing all available options.""" 6894 """Return the parameter description set.""" 6898 """Assert constraints as background axioms for the fixedpoint solver.""" 6899 args = _get_args(args)
6902 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
6912 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6920 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6924 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6928 """Assert rules defining recursive predicates to the fixedpoint solver. 6931 >>> s = Fixedpoint() 6932 >>> s.register_relation(a.decl()) 6933 >>> s.register_relation(b.decl()) 6946 body = _get_args(body)
6950 def rule(self, head, body = None, name = None):
6951 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 6955 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 6959 """Query the fixedpoint engine whether formula is derivable. 6960 You can also pass an tuple or list of recursive predicates. 6962 query = _get_args(query)
6964 if sz >= 1
and isinstance(query[0], FuncDeclRef):
6965 _decls = (FuncDecl * sz)()
6975 query =
And(query, self.
ctx)
6976 query = self.
abstract(query,
False)
6981 """Query the fixedpoint engine whether formula is derivable starting at the given query level. 6983 query = _get_args(query)
6985 if sz >= 1
and isinstance(query[0], FuncDecl):
6986 _z3_assert (
False,
"unsupported")
6992 query = self.
abstract(query,
False)
6993 r = Z3_fixedpoint_query_from_lvl (self.
ctx.ref(), self.
fixedpoint, query.as_ast(), lvl)
6997 """create a backtracking point for added rules, facts and assertions""" 7001 """restore to previously created backtracking point""" 7009 body = _get_args(body)
7014 """Retrieve answer from last query call.""" 7016 return _to_expr_ref(r, self.
ctx)
7019 """Retrieve a ground cex from last query call.""" 7020 r = Z3_fixedpoint_get_ground_sat_answer(self.
ctx.ref(), self.
fixedpoint)
7021 return _to_expr_ref(r, self.
ctx)
7024 """retrieve rules along the counterexample trace""" 7028 """retrieve rule names along the counterexample trace""" 7031 names = _symbol2py (self.
ctx, Z3_fixedpoint_get_rule_names_along_trace(self.
ctx.ref(), self.
fixedpoint))
7033 return names.split (
';')
7036 """Retrieve number of levels used for predicate in PDR engine""" 7040 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)""" 7042 return _to_expr_ref(r, self.
ctx)
7045 """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)""" 7049 """Register relation as recursive""" 7050 relations = _get_args(relations)
7055 """Control how relation is represented""" 7056 representations = _get_args(representations)
7057 representations = [
to_symbol(s)
for s
in representations]
7058 sz = len(representations)
7059 args = (Symbol * sz)()
7061 args[i] = representations[i]
7065 """Parse rules and queries from a string""" 7068 except Z3Exception
as e:
7069 _handle_parse_error(e, self.
ctx)
7072 """Parse rules and queries from a file""" 7075 except Z3Exception
as e:
7076 _handle_parse_error(e, self.
ctx)
7079 """retrieve rules that have been added to fixedpoint context""" 7083 """retrieve assertions that have been added to fixedpoint context""" 7087 """Return a formatted string with all added rules and constraints.""" 7091 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 7096 """Return a formatted string (in Lisp-like format) with all added constraints. 7097 We say the string is in s-expression format. 7098 Include also queries. 7100 args, len = _to_ast_array(queries)
7104 """Return statistics for the last `query()`. 7109 """Return a string describing why the last `query()` returned `unknown`. 7114 """Add variable or several variables. 7115 The added variable or variables will be bound in the rules 7118 vars = _get_args(vars)
7138 """Finite domain sort.""" 7141 """Return the size of the finite domain sort""" 7142 r = (ctypes.c_ulonglong * 1)()
7146 raise Z3Exception(
"Failed to retrieve finite domain sort size")
7149 """Create a named finite domain sort of a given size sz""" 7150 if not isinstance(name, Symbol):
7156 """Return True if `s` is a Z3 finite-domain sort. 7158 >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) 7160 >>> is_finite_domain_sort(IntSort()) 7163 return isinstance(s, FiniteDomainSortRef)
7167 """Finite-domain expressions.""" 7170 """Return the sort of the finite-domain expression `self`.""" 7174 """Return a Z3 floating point expression as a Python string.""" 7178 """Return `True` if `a` is a Z3 finite-domain expression. 7180 >>> s = FiniteDomainSort('S', 100) 7181 >>> b = Const('b', s) 7182 >>> is_finite_domain(b) 7184 >>> is_finite_domain(Int('x')) 7187 return isinstance(a, FiniteDomainRef)
7191 """Integer values.""" 7194 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. 7196 >>> s = FiniteDomainSort('S', 100) 7197 >>> v = FiniteDomainVal(3, s) 7206 """Return a Z3 finite-domain numeral as a Python string. 7208 >>> s = FiniteDomainSort('S', 100) 7209 >>> v = FiniteDomainVal(42, s) 7217 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. 7219 >>> s = FiniteDomainSort('S', 256) 7220 >>> FiniteDomainVal(255, s) 7222 >>> FiniteDomainVal('100', s) 7231 """Return `True` if `a` is a Z3 finite-domain value. 7233 >>> s = FiniteDomainSort('S', 100) 7234 >>> b = Const('b', s) 7235 >>> is_finite_domain_value(b) 7237 >>> b = FiniteDomainVal(10, s) 7240 >>> is_finite_domain_value(b) 7285 """Optimize API provides methods for solving using objective functions and weighted soft constraints""" 7296 if self.
optimize is not None and self.
ctx.ref()
is not None:
7300 """Set a configuration option. The method `help()` return a string containing all available options. 7306 """Display a string describing all available options.""" 7310 """Return the parameter description set.""" 7314 """Assert constraints as background axioms for the optimize solver.""" 7315 args = _get_args(args)
7318 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
7326 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr.""" 7334 """Add soft constraint with optional weight and optional identifier. 7335 If no weight is supplied, then the penalty for violating the soft constraint 7337 Soft constraints are grouped by identifiers. Soft constraints that are 7338 added without identifiers are grouped by default. 7341 weight =
"%d" % weight
7342 elif isinstance(weight, float):
7343 weight =
"%f" % weight
7344 if not isinstance(weight, str):
7345 raise Z3Exception(
"weight should be a string or an integer")
7353 """Add objective function to maximize.""" 7357 """Add objective function to minimize.""" 7361 """create a backtracking point for added rules, facts and assertions""" 7365 """restore to previously created backtracking point""" 7369 """Check satisfiability while optimizing objective functions.""" 7370 assumptions = _get_args(assumptions)
7371 num = len(assumptions)
7372 _assumptions = (Ast * num)()
7373 for i
in range(num):
7374 _assumptions[i] = assumptions[i].as_ast()
7378 """Return a string that describes why the last `check()` returned `unknown`.""" 7382 """Return a model for the last check().""" 7386 raise Z3Exception(
"model is not available")
7392 if not isinstance(obj, OptimizeObjective):
7393 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7397 if not isinstance(obj, OptimizeObjective):
7398 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7402 if not isinstance(obj, OptimizeObjective):
7403 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7404 return obj.lower_values()
7407 if not isinstance(obj, OptimizeObjective):
7408 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7409 return obj.upper_values()
7412 """Parse assertions and objectives from a file""" 7415 except Z3Exception
as e:
7416 _handle_parse_error(e, self.
ctx)
7419 """Parse assertions and objectives from a string""" 7422 except Z3Exception
as e:
7423 _handle_parse_error(e, self.
ctx)
7426 """Return an AST vector containing all added constraints.""" 7430 """returns set of objective functions""" 7434 """Return a formatted string with all added rules and constraints.""" 7438 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 7443 """Return statistics for the last check`. 7456 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters.""" 7467 if self.
ctx.ref()
is not None:
7471 """Return the number of subgoals in `self`. 7473 >>> a, b = Ints('a b') 7475 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7476 >>> t = Tactic('split-clause') 7480 >>> t = Then(Tactic('split-clause'), Tactic('split-clause')) 7483 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values')) 7490 """Return one of the subgoals stored in ApplyResult object `self`. 7492 >>> a, b = Ints('a b') 7494 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7495 >>> t = Tactic('split-clause') 7498 [a == 0, Or(b == 0, b == 1), a > b] 7500 [a == 1, Or(b == 0, b == 1), a > b] 7502 if idx >= len(self):
7507 return obj_to_string(self)
7510 """Return a textual representation of the s-expression representing the set of subgoals in `self`.""" 7515 """Return a Z3 expression consisting of all subgoals. 7520 >>> g.add(Or(x == 2, x == 3)) 7521 >>> r = Tactic('simplify')(g) 7523 [[Not(x <= 1), Or(x == 2, x == 3)]] 7525 And(Not(x <= 1), Or(x == 2, x == 3)) 7526 >>> r = Tactic('split-clause')(g) 7528 [[x > 1, x == 2], [x > 1, x == 3]] 7530 Or(And(x > 1, x == 2), And(x > 1, x == 3)) 7546 """Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver(). 7548 Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond(). 7553 if isinstance(tactic, TacticObj):
7557 _z3_assert(isinstance(tactic, str),
"tactic name expected")
7561 raise Z3Exception(
"unknown tactic '%s'" % tactic)
7568 if self.
tactic is not None and self.
ctx.ref()
is not None:
7572 """Create a solver using the tactic `self`. 7574 The solver supports the methods `push()` and `pop()`, but it 7575 will always solve each `check()` from scratch. 7577 >>> t = Then('simplify', 'nlsat') 7580 >>> s.add(x**2 == 2, x > 0) 7588 def apply(self, goal, *arguments, **keywords):
7589 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7591 >>> x, y = Ints('x y') 7592 >>> t = Tactic('solve-eqs') 7593 >>> t.apply(And(x == 0, y >= x + 1)) 7597 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expressions expected")
7598 goal = _to_goal(goal)
7599 if len(arguments) > 0
or len(keywords) > 0:
7606 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7608 >>> x, y = Ints('x y') 7609 >>> t = Tactic('solve-eqs') 7610 >>> t(And(x == 0, y >= x + 1)) 7613 return self.
apply(goal, *arguments, **keywords)
7616 """Display a string containing a description of the available options for the `self` tactic.""" 7620 """Return the parameter description set.""" 7624 if isinstance(a, BoolRef):
7625 goal =
Goal(ctx = a.ctx)
7631 def _to_tactic(t, ctx=None):
7632 if isinstance(t, Tactic):
7637 def _and_then(t1, t2, ctx=None):
7638 t1 = _to_tactic(t1, ctx)
7639 t2 = _to_tactic(t2, ctx)
7641 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7644 def _or_else(t1, t2, ctx=None):
7645 t1 = _to_tactic(t1, ctx)
7646 t2 = _to_tactic(t2, ctx)
7648 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7652 """Return a tactic that applies the tactics in `*ts` in sequence. 7654 >>> x, y = Ints('x y') 7655 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) 7656 >>> t(And(x == 0, y > x + 1)) 7658 >>> t(And(x == 0, y > x + 1)).as_expr() 7662 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7663 ctx = ks.get(
'ctx',
None)
7666 for i
in range(num - 1):
7667 r = _and_then(r, ts[i+1], ctx)
7671 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). 7673 >>> x, y = Ints('x y') 7674 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) 7675 >>> t(And(x == 0, y > x + 1)) 7677 >>> t(And(x == 0, y > x + 1)).as_expr() 7683 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). 7686 >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) 7687 >>> # Tactic split-clause fails if there is no clause in the given goal. 7690 >>> t(Or(x == 0, x == 1)) 7691 [[x == 0], [x == 1]] 7694 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7695 ctx = ks.get(
'ctx',
None)
7698 for i
in range(num - 1):
7699 r = _or_else(r, ts[i+1], ctx)
7703 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). 7706 >>> t = ParOr(Tactic('simplify'), Tactic('fail')) 7711 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7712 ctx = _get_ctx(ks.get(
'ctx',
None))
7713 ts = [ _to_tactic(t, ctx)
for t
in ts ]
7715 _args = (TacticObj * sz)()
7717 _args[i] = ts[i].tactic
7721 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. 7723 >>> x, y = Ints('x y') 7724 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) 7725 >>> t(And(Or(x == 1, x == 2), y == x + 1)) 7726 [[x == 1, y == 2], [x == 2, y == 3]] 7728 t1 = _to_tactic(t1, ctx)
7729 t2 = _to_tactic(t2, ctx)
7731 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7735 """Alias for ParThen(t1, t2, ctx).""" 7739 """Return a tactic that applies tactic `t` using the given configuration options. 7741 >>> x, y = Ints('x y') 7742 >>> t = With(Tactic('simplify'), som=True) 7743 >>> t((x + 1)*(y + 2) == 0) 7744 [[2*x + y + x*y == -2]] 7746 ctx = keys.pop(
'ctx',
None)
7747 t = _to_tactic(t, ctx)
7752 """Return a tactic that applies tactic `t` using the given configuration options. 7754 >>> x, y = Ints('x y') 7756 >>> p.set("som", True) 7757 >>> t = WithParams(Tactic('simplify'), p) 7758 >>> t((x + 1)*(y + 2) == 0) 7759 [[2*x + y + x*y == -2]] 7761 t = _to_tactic(t,
None)
7765 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. 7767 >>> x, y = Ints('x y') 7768 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) 7769 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) 7771 >>> for subgoal in r: print(subgoal) 7772 [x == 0, y == 0, x > y] 7773 [x == 0, y == 1, x > y] 7774 [x == 1, y == 0, x > y] 7775 [x == 1, y == 1, x > y] 7776 >>> t = Then(t, Tactic('propagate-values')) 7780 t = _to_tactic(t, ctx)
7784 """Return a tactic that applies `t` to a given goal for `ms` milliseconds. 7786 If `t` does not terminate in `ms` milliseconds, then it fails. 7788 t = _to_tactic(t, ctx)
7792 """Return a list of all available tactics in Z3. 7795 >>> l.count('simplify') == 1 7802 """Return a short description for the tactic named `name`. 7804 >>> d = tactic_description('simplify') 7810 """Display a (tabular) description of all available tactics in Z3.""" 7813 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7816 print(
'<tr style="background-color:#CFCFCF">')
7821 print(
'<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(
tactic_description(t), 40)))
7828 """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.""" 7832 if isinstance(probe, ProbeObj):
7834 elif isinstance(probe, float):
7836 elif _is_int(probe):
7838 elif isinstance(probe, bool):
7845 _z3_assert(isinstance(probe, str),
"probe name expected")
7849 raise Z3Exception(
"unknown probe '%s'" % probe)
7856 if self.
probe is not None and self.
ctx.ref()
is not None:
7860 """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`. 7862 >>> p = Probe('size') < 10 7873 """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`. 7875 >>> p = Probe('size') > 10 7886 """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`. 7888 >>> p = Probe('size') <= 2 7899 """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`. 7901 >>> p = Probe('size') >= 2 7912 """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`. 7914 >>> p = Probe('size') == 2 7925 """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`. 7927 >>> p = Probe('size') != 2 7939 """Evaluate the probe `self` in the given goal. 7941 >>> p = Probe('size') 7951 >>> p = Probe('num-consts') 7954 >>> p = Probe('is-propositional') 7957 >>> p = Probe('is-qflia') 7962 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expression expected")
7963 goal = _to_goal(goal)
7967 """Return `True` if `p` is a Z3 probe. 7969 >>> is_probe(Int('x')) 7971 >>> is_probe(Probe('memory')) 7974 return isinstance(p, Probe)
7976 def _to_probe(p, ctx=None):
7980 return Probe(p, ctx)
7983 """Return a list of all available probes in Z3. 7986 >>> l.count('memory') == 1 7993 """Return a short description for the probe named `name`. 7995 >>> d = probe_description('memory') 8001 """Display a (tabular) description of all available probes in Z3.""" 8004 print(
'<table border="1" cellpadding="2" cellspacing="0">')
8007 print(
'<tr style="background-color:#CFCFCF">')
8012 print(
'<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(
probe_description(p), 40)))
8018 def _probe_nary(f, args, ctx):
8020 _z3_assert(len(args) > 0,
"At least one argument expected")
8022 r = _to_probe(args[0], ctx)
8023 for i
in range(num - 1):
8024 r =
Probe(f(ctx.ref(), r.probe, _to_probe(args[i+1], ctx).probe), ctx)
8027 def _probe_and(args, ctx):
8028 return _probe_nary(Z3_probe_and, args, ctx)
8030 def _probe_or(args, ctx):
8031 return _probe_nary(Z3_probe_or, args, ctx)
8034 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 8036 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. 8038 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) 8039 >>> x, y = Ints('x y') 8045 >>> g.add(x == y + 1) 8047 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 8049 p = _to_probe(p, ctx)
8053 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 8055 >>> t = When(Probe('size') > 2, Tactic('simplify')) 8056 >>> x, y = Ints('x y') 8062 >>> g.add(x == y + 1) 8064 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 8066 p = _to_probe(p, ctx)
8067 t = _to_tactic(t, ctx)
8071 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. 8073 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt')) 8075 p = _to_probe(p, ctx)
8076 t1 = _to_tactic(t1, ctx)
8077 t2 = _to_tactic(t2, ctx)
8087 """Simplify the expression `a` using the given options. 8089 This function has many options. Use `help_simplify` to obtain the complete list. 8093 >>> simplify(x + 1 + y + x + 1) 8095 >>> simplify((x + 1)*(y + 1), som=True) 8097 >>> simplify(Distinct(x, y, 1), blast_distinct=True) 8098 And(Not(x == y), Not(x == 1), Not(y == 1)) 8099 >>> simplify(And(x == 0, y == 1), elim_and=True) 8100 Not(Or(Not(x == 0), Not(y == 1))) 8103 _z3_assert(
is_expr(a),
"Z3 expression expected")
8104 if len(arguments) > 0
or len(keywords) > 0:
8106 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
8108 return _to_expr_ref(
Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
8111 """Return a string describing all options available for Z3 `simplify` procedure.""" 8115 """Return the set of parameter descriptions for Z3 `simplify` procedure.""" 8119 """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. 8123 >>> substitute(x + 1, (x, y + 1)) 8125 >>> f = Function('f', IntSort(), IntSort()) 8126 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 8129 if isinstance(m, tuple):
8131 if isinstance(m1, list)
and all(isinstance(p, tuple)
for p
in m1):
8134 _z3_assert(
is_expr(t),
"Z3 expression expected")
8135 _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.")
8137 _from = (Ast * num)()
8139 for i
in range(num):
8140 _from[i] = m[i][0].as_ast()
8141 _to[i] = m[i][1].as_ast()
8142 return _to_expr_ref(
Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
8145 """Substitute the free variables in t with the expression in m. 8147 >>> v0 = Var(0, IntSort()) 8148 >>> v1 = Var(1, IntSort()) 8150 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 8151 >>> # replace v0 with x+1 and v1 with x 8152 >>> substitute_vars(f(v0, v1), x + 1, x) 8156 _z3_assert(
is_expr(t),
"Z3 expression expected")
8157 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
8160 for i
in range(num):
8161 _to[i] = m[i].as_ast()
8165 """Create the sum of the Z3 expressions. 8167 >>> a, b, c = Ints('a b c') 8172 >>> A = IntVector('a', 5) 8174 a__0 + a__1 + a__2 + a__3 + a__4 8176 args = _get_args(args)
8179 ctx = _ctx_from_ast_arg_list(args)
8181 return _reduce(
lambda a, b: a + b, args, 0)
8182 args = _coerce_expr_list(args, ctx)
8184 return _reduce(
lambda a, b: a + b, args, 0)
8186 _args, sz = _to_ast_array(args)
8191 """Create the product of the Z3 expressions. 8193 >>> a, b, c = Ints('a b c') 8194 >>> Product(a, b, c) 8196 >>> Product([a, b, c]) 8198 >>> A = IntVector('a', 5) 8200 a__0*a__1*a__2*a__3*a__4 8202 args = _get_args(args)
8205 ctx = _ctx_from_ast_arg_list(args)
8207 return _reduce(
lambda a, b: a * b, args, 1)
8208 args = _coerce_expr_list(args, ctx)
8210 return _reduce(
lambda a, b: a * b, args, 1)
8212 _args, sz = _to_ast_array(args)
8216 """Create an at-most Pseudo-Boolean k constraint. 8218 >>> a, b, c = Bools('a b c') 8219 >>> f = AtMost(a, b, c, 2) 8221 args = _get_args(args)
8223 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8224 ctx = _ctx_from_ast_arg_list(args)
8226 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8227 args1 = _coerce_expr_list(args[:-1], ctx)
8229 _args, sz = _to_ast_array(args1)
8233 """Create an at-most Pseudo-Boolean k constraint. 8235 >>> a, b, c = Bools('a b c') 8236 >>> f = AtLeast(a, b, c, 2) 8238 args = _get_args(args)
8240 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8241 ctx = _ctx_from_ast_arg_list(args)
8243 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8244 args1 = _coerce_expr_list(args[:-1], ctx)
8246 _args, sz = _to_ast_array(args1)
8250 def _pb_args_coeffs(args, default_ctx = None):
8251 args = _get_args_ast_list(args)
8253 return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
8254 args, coeffs = zip(*args)
8256 _z3_assert(len(args) > 0,
"Non empty list of arguments expected")
8257 ctx = _ctx_from_ast_arg_list(args)
8259 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8260 args = _coerce_expr_list(args, ctx)
8261 _args, sz = _to_ast_array(args)
8262 _coeffs = (ctypes.c_int * len(coeffs))()
8263 for i
in range(len(coeffs)):
8264 _z3_check_cint_overflow(coeffs[i],
"coefficient")
8265 _coeffs[i] = coeffs[i]
8266 return ctx, sz, _args, _coeffs
8269 """Create a Pseudo-Boolean inequality k constraint. 8271 >>> a, b, c = Bools('a b c') 8272 >>> f = PbLe(((a,1),(b,3),(c,2)), 3) 8274 _z3_check_cint_overflow(k,
"k")
8275 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8279 """Create a Pseudo-Boolean inequality k constraint. 8281 >>> a, b, c = Bools('a b c') 8282 >>> f = PbGe(((a,1),(b,3),(c,2)), 3) 8284 _z3_check_cint_overflow(k,
"k")
8285 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8289 """Create a Pseudo-Boolean inequality k constraint. 8291 >>> a, b, c = Bools('a b c') 8292 >>> f = PbEq(((a,1),(b,3),(c,2)), 3) 8294 _z3_check_cint_overflow(k,
"k")
8295 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8300 """Solve the constraints `*args`. 8302 This is a simple function for creating demonstrations. It creates a solver, 8303 configure it using the options in `keywords`, adds the constraints 8304 in `args`, and invokes check. 8307 >>> solve(a > 0, a < 2) 8313 if keywords.get(
'show',
False):
8317 print(
"no solution")
8319 print(
"failed to solve")
8328 """Solve the constraints `*args` using solver `s`. 8330 This is a simple function for creating demonstrations. It is similar to `solve`, 8331 but it uses the given solver `s`. 8332 It configures solver `s` using the options in `keywords`, adds the constraints 8333 in `args`, and invokes check. 8336 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8339 if keywords.get(
'show',
False):
8344 print(
"no solution")
8346 print(
"failed to solve")
8352 if keywords.get(
'show',
False):
8357 """Try to prove the given claim. 8359 This is a simple function for creating demonstrations. It tries to prove 8360 `claim` by showing the negation is unsatisfiable. 8362 >>> p, q = Bools('p q') 8363 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) 8367 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8371 if keywords.get(
'show',
False):
8377 print(
"failed to prove")
8380 print(
"counterexample")
8383 def _solve_html(*args, **keywords):
8384 """Version of function `solve` used in RiSE4Fun.""" 8388 if keywords.get(
'show',
False):
8389 print(
"<b>Problem:</b>")
8393 print(
"<b>no solution</b>")
8395 print(
"<b>failed to solve</b>")
8401 if keywords.get(
'show',
False):
8402 print(
"<b>Solution:</b>")
8405 def _solve_using_html(s, *args, **keywords):
8406 """Version of function `solve_using` used in RiSE4Fun.""" 8408 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8411 if keywords.get(
'show',
False):
8412 print(
"<b>Problem:</b>")
8416 print(
"<b>no solution</b>")
8418 print(
"<b>failed to solve</b>")
8424 if keywords.get(
'show',
False):
8425 print(
"<b>Solution:</b>")
8428 def _prove_html(claim, **keywords):
8429 """Version of function `prove` used in RiSE4Fun.""" 8431 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8435 if keywords.get(
'show',
False):
8439 print(
"<b>proved</b>")
8441 print(
"<b>failed to prove</b>")
8444 print(
"<b>counterexample</b>")
8447 def _dict2sarray(sorts, ctx):
8449 _names = (Symbol * sz)()
8450 _sorts = (Sort * sz) ()
8455 _z3_assert(isinstance(k, str),
"String expected")
8456 _z3_assert(
is_sort(v),
"Z3 sort expected")
8460 return sz, _names, _sorts
8462 def _dict2darray(decls, ctx):
8464 _names = (Symbol * sz)()
8465 _decls = (FuncDecl * sz) ()
8470 _z3_assert(isinstance(k, str),
"String expected")
8474 _decls[i] = v.decl().ast
8478 return sz, _names, _decls
8482 """Parse a string in SMT 2.0 format using the given sorts and decls. 8484 The arguments sorts and decls are Python dictionaries used to initialize 8485 the symbol table used for the SMT 2.0 parser. 8487 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') 8489 >>> x, y = Ints('x y') 8490 >>> f = Function('f', IntSort(), IntSort()) 8491 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) 8493 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) 8497 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 8498 dsz, dnames, ddecls = _dict2darray(decls, ctx) 8499 return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 8501 def parse_smt2_file(f, sorts={}, decls={}, ctx=None): 8502 """Parse a file
in SMT 2.0 format using the given sorts
and decls.
8507 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 8508 dsz, dnames, ddecls = _dict2darray(decls, ctx) 8509 return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 8512 ######################################### 8514 # Floating-Point Arithmetic 8516 ######################################### 8519 # Global default rounding mode 8520 _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO 8521 _dflt_fpsort_ebits = 11 8522 _dflt_fpsort_sbits = 53 8524 def get_default_rounding_mode(ctx=None): 8525 """Retrieves the
global default rounding mode.
""" 8526 global _dflt_rounding_mode 8527 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO: 8529 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE: 8531 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE: 8533 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: 8535 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: 8538 def set_default_rounding_mode(rm, ctx=None): 8539 global _dflt_rounding_mode 8540 if is_fprm_value(rm): 8541 _dflt_rounding_mode = rm.decl().kind() 8543 _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO or 8544 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE or 8545 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE or 8546 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN or 8547 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, 8548 "illegal rounding mode") 8549 _dflt_rounding_mode = rm 8551 def get_default_fp_sort(ctx=None): 8552 return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx) 8554 def set_default_fp_sort(ebits, sbits, ctx=None): 8555 global _dflt_fpsort_ebits 8556 global _dflt_fpsort_sbits 8557 _dflt_fpsort_ebits = ebits 8558 _dflt_fpsort_sbits = sbits 8560 def _dflt_rm(ctx=None): 8561 return get_default_rounding_mode(ctx) 8563 def _dflt_fps(ctx=None): 8564 return get_default_fp_sort(ctx) 8566 def _coerce_fp_expr_list(alist, ctx): 8567 first_fp_sort = None 8570 if first_fp_sort is None: 8571 first_fp_sort = a.sort() 8572 elif first_fp_sort == a.sort(): 8573 pass # OK, same as before 8575 # we saw at least 2 different float sorts; something will 8576 # throw a sort mismatch later, for now assume None. 8577 first_fp_sort = None 8581 for i in range(len(alist)): 8583 if (isinstance(a, str) and a.contains('2**(') and a.endswith(')')) or _is_int(a) or isinstance(a, float) or isinstance(a, bool): 8584 r.append(FPVal(a, None, first_fp_sort, ctx)) 8587 return _coerce_expr_list(r, ctx) 8592 class FPSortRef(SortRef): 8593 """Floating-point sort.
""" 8596 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint sort `self`.
8601 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast)) 8604 """Retrieves the number of bits reserved
for the significand
in the FloatingPoint sort `self`.
8609 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast)) 8611 def cast(self, val): 8612 """Try to cast `val`
as a floating-point expression.
8616 >>> b.cast(1.0).
sexpr()
8617 '(fp #b0 #x7f #b00000000000000000000000)' 8621 _z3_assert(self.ctx == val.ctx, "Context mismatch") 8624 return FPVal(val, None, self, self.ctx) 8627 def Float16(ctx=None): 8628 """Floating-point 16-bit (half) sort.
""" 8630 return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx) 8632 def FloatHalf(ctx=None): 8633 """Floating-point 16-bit (half) sort.
""" 8635 return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx) 8637 def Float32(ctx=None): 8638 """Floating-point 32-bit (single) sort.
""" 8640 return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx) 8642 def FloatSingle(ctx=None): 8643 """Floating-point 32-bit (single) sort.
""" 8645 return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx) 8647 def Float64(ctx=None): 8648 """Floating-point 64-bit (double) sort.
""" 8650 return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx) 8652 def FloatDouble(ctx=None): 8653 """Floating-point 64-bit (double) sort.
""" 8655 return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx) 8657 def Float128(ctx=None): 8658 """Floating-point 128-bit (quadruple) sort.
""" 8660 return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx) 8662 def FloatQuadruple(ctx=None): 8663 """Floating-point 128-bit (quadruple) sort.
""" 8665 return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx) 8667 class FPRMSortRef(SortRef): 8668 """"Floating-point rounding mode sort.""" 8672 """Return True if `s` is a Z3 floating-point sort.
8679 return isinstance(s, FPSortRef) 8681 def is_fprm_sort(s): 8682 """Return
True if `s`
is a Z3 floating-point rounding mode sort.
8689 return isinstance(s, FPRMSortRef) 8693 class FPRef(ExprRef): 8694 """Floating-point expressions.
""" 8697 """Return the sort of the floating-point expression `self`.
8702 >>> x.sort() ==
FPSort(8, 24)
8705 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 8708 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8713 return self.sort().ebits(); 8716 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8721 return self.sort().sbits(); 8723 def as_string(self): 8724 """Return a Z3 floating point expression
as a Python string.
""" 8725 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8727 def __le__(self, other): 8728 return fpLEQ(self, other, self.ctx) 8730 def __lt__(self, other): 8731 return fpLT(self, other, self.ctx) 8733 def __ge__(self, other): 8734 return fpGEQ(self, other, self.ctx) 8736 def __gt__(self, other): 8737 return fpGT(self, other, self.ctx) 8739 def __add__(self, other): 8740 """Create the Z3 expression `self + other`.
8749 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8750 return fpAdd(_dflt_rm(), a, b, self.ctx) 8752 def __radd__(self, other): 8753 """Create the Z3 expression `other + self`.
8759 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8760 return fpAdd(_dflt_rm(), a, b, self.ctx) 8762 def __sub__(self, other): 8763 """Create the Z3 expression `self - other`.
8772 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8773 return fpSub(_dflt_rm(), a, b, self.ctx) 8775 def __rsub__(self, other): 8776 """Create the Z3 expression `other - self`.
8782 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8783 return fpSub(_dflt_rm(), a, b, self.ctx) 8785 def __mul__(self, other): 8786 """Create the Z3 expression `self * other`.
8797 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8798 return fpMul(_dflt_rm(), a, b, self.ctx) 8800 def __rmul__(self, other): 8801 """Create the Z3 expression `other * self`.
8810 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8811 return fpMul(_dflt_rm(), a, b, self.ctx) 8814 """Create the Z3 expression `+self`.
""" 8818 """Create the Z3 expression `-self`.
8826 def __div__(self, other): 8827 """Create the Z3 expression `self / other`.
8838 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8839 return fpDiv(_dflt_rm(), a, b, self.ctx) 8841 def __rdiv__(self, other): 8842 """Create the Z3 expression `other / self`.
8851 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8852 return fpDiv(_dflt_rm(), a, b, self.ctx) 8854 if not sys.version < '3': 8855 def __truediv__(self, other): 8856 """Create the Z3 expression division `self / other`.
""" 8857 return self.__div__(other) 8859 def __rtruediv__(self, other): 8860 """Create the Z3 expression division `other / self`.
""" 8861 return self.__rdiv__(other) 8863 def __mod__(self, other): 8864 """Create the Z3 expression mod `self % other`.
""" 8865 return fpRem(self, other) 8867 def __rmod__(self, other): 8868 """Create the Z3 expression mod `other % self`.
""" 8869 return fpRem(other, self) 8871 class FPRMRef(ExprRef): 8872 """Floating-point rounding mode expressions
""" 8874 def as_string(self): 8875 """Return a Z3 floating point expression
as a Python string.
""" 8876 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8879 def RoundNearestTiesToEven(ctx=None): 8881 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8885 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8887 def RoundNearestTiesToAway(ctx=None): 8889 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8893 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8895 def RoundTowardPositive(ctx=None): 8897 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8901 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8903 def RoundTowardNegative(ctx=None): 8905 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8909 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8911 def RoundTowardZero(ctx=None): 8913 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8917 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8920 """Return `
True`
if `a`
is a Z3 floating-point rounding mode expression.
8929 return isinstance(a, FPRMRef) 8931 def is_fprm_value(a): 8932 """Return `
True`
if `a`
is a Z3 floating-point rounding mode numeral value.
""" 8933 return is_fprm(a) and _is_numeral(a.ctx, a.ast) 8937 class FPNumRef(FPRef): 8938 """The sign of the numeral.
8948 l = (ctypes.c_int)() 8949 if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False: 8950 raise Z3Exception("error retrieving the sign of a numeral.") 8953 """The sign of a floating-point numeral
as a bit-vector expression.
8955 Remark: NaN
's are invalid arguments. 8957 def sign_as_bv(self): 8958 return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx) 8960 """The significand of the numeral.
8966 def significand(self): 8967 return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast()) 8969 """The significand of the numeral
as a long.
8972 >>> x.significand_as_long()
8975 def significand_as_long(self): 8976 ptr = (ctypes.c_ulonglong * 1)() 8977 if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr): 8978 raise Z3Exception("error retrieving the significand of a numeral.") 8981 """The significand of the numeral
as a bit-vector expression.
8983 Remark: NaN are invalid arguments.
8985 def significand_as_bv(self): 8986 return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx) 8988 """The exponent of the numeral.
8994 def exponent(self, biased=True): 8995 return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased) 8997 """The exponent of the numeral
as a long.
9000 >>> x.exponent_as_long()
9003 def exponent_as_long(self, biased=True): 9004 ptr = (ctypes.c_longlong * 1)() 9005 if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased): 9006 raise Z3Exception("error retrieving the exponent of a numeral.") 9009 """The exponent of the numeral
as a bit-vector expression.
9011 Remark: NaNs are invalid arguments.
9013 def exponent_as_bv(self, biased=True): 9014 return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx) 9016 """Indicates whether the numeral
is a NaN.
""" 9018 return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast()) 9020 """Indicates whether the numeral
is +oo
or -oo.
""" 9022 return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast()) 9024 """Indicates whether the numeral
is +zero
or -zero.
""" 9026 return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast()) 9028 """Indicates whether the numeral
is normal.
""" 9030 return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast()) 9032 """Indicates whether the numeral
is subnormal.
""" 9033 def isSubnormal(self): 9034 return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast()) 9036 """Indicates whether the numeral
is positive.
""" 9037 def isPositive(self): 9038 return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast()) 9040 """Indicates whether the numeral
is negative.
""" 9041 def isNegative(self): 9042 return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast()) 9045 The string representation of the numeral.
9051 def as_string(self): 9052 s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast()) 9053 return ("FPVal(%s, %s)" % (s, self.sort())) 9056 """Return `
True`
if `a`
is a Z3 floating-point expression.
9066 return isinstance(a, FPRef) 9069 """Return `
True`
if `a`
is a Z3 floating-point numeral value.
9080 return is_fp(a) and _is_numeral(a.ctx, a.ast) 9082 def FPSort(ebits, sbits, ctx=None): 9083 """Return a Z3 floating-point sort of the given sizes. If `ctx=
None`, then the
global context
is used.
9085 >>> Single =
FPSort(8, 24)
9086 >>> Double =
FPSort(11, 53)
9089 >>> x =
Const(
'x', Single)
9094 return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx) 9096 def _to_float_str(val, exp=0): 9097 if isinstance(val, float): 9101 sone = math.copysign(1.0, val) 9106 elif val == float("+inf"): 9108 elif val == float("-inf"): 9111 v = val.as_integer_ratio() 9114 rvs = str(num) + '/' + str(den) 9115 res = rvs + 'p' + _to_int_str(exp) 9116 elif isinstance(val, bool): 9123 elif isinstance(val, str): 9124 inx = val.find('*(2**') 9127 elif val[-1] == ')': 9129 exp = str(int(val[inx+5:-1]) + int(exp)) 9131 _z3_assert(False, "String does not have floating-point numeral form.") 9133 _z3_assert(False, "Python value cannot be used to create floating-point numerals.") 9137 return res + 'p' + exp 9141 """Create a Z3 floating-point NaN term.
9144 >>> set_fpa_pretty(
True)
9147 >>> pb = get_fpa_pretty()
9148 >>> set_fpa_pretty(
False)
9151 >>> set_fpa_pretty(pb)
9153 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9154 return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx) 9156 def fpPlusInfinity(s): 9157 """Create a Z3 floating-point +oo term.
9160 >>> pb = get_fpa_pretty()
9161 >>> set_fpa_pretty(
True)
9164 >>> set_fpa_pretty(
False)
9167 >>> set_fpa_pretty(pb)
9169 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9170 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx) 9172 def fpMinusInfinity(s): 9173 """Create a Z3 floating-point -oo term.
""" 9174 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9175 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx) 9177 def fpInfinity(s, negative): 9178 """Create a Z3 floating-point +oo
or -oo term.
""" 9179 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9180 _z3_assert(isinstance(negative, bool), "expected Boolean flag") 9181 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx) 9184 """Create a Z3 floating-point +0.0 term.
""" 9185 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9186 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx) 9189 """Create a Z3 floating-point -0.0 term.
""" 9190 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9191 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx) 9193 def fpZero(s, negative): 9194 """Create a Z3 floating-point +0.0
or -0.0 term.
""" 9195 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9196 _z3_assert(isinstance(negative, bool), "expected Boolean flag") 9197 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx) 9199 def FPVal(sig, exp=None, fps=None, ctx=None): 9200 """Return a floating-point value of value `val`
and sort `fps`. If `ctx=
None`, then the
global context
is used.
9205 >>> print(
"0x%.8x" % v.exponent_as_long(
False))
9225 fps = _dflt_fps(ctx) 9226 _z3_assert(is_fp_sort(fps), "sort mismatch") 9229 val = _to_float_str(sig) 9230 if val == "NaN" or val == "nan": 9233 return fpMinusZero(fps) 9234 elif val == "0.0" or val == "+0.0": 9235 return fpPlusZero(fps) 9236 elif val == "+oo" or val == "+inf" or val == "+Inf": 9237 return fpPlusInfinity(fps) 9238 elif val == "-oo" or val == "-inf" or val == "-Inf": 9239 return fpMinusInfinity(fps) 9241 return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx) 9243 def FP(name, fpsort, ctx=None): 9244 """Return a floating-point constant named `name`.
9245 `fpsort`
is the floating-point sort.
9246 If `ctx=
None`, then the
global context
is used.
9256 >>> x2 =
FP(
'x', word)
9260 if isinstance(fpsort, FPSortRef) and ctx is None: 9264 return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx) 9266 def FPs(names, fpsort, ctx=None): 9267 """Return an array of floating-point constants.
9269 >>> x, y, z =
FPs(
'x y z',
FPSort(8, 24))
9280 if isinstance(names, str): 9281 names = names.split(" ") 9282 return [FP(name, fpsort, ctx) for name in names] 9284 def fpAbs(a, ctx=None): 9285 """Create a Z3 floating-point absolute value expression.
9289 >>> x =
FPVal(1.0, s)
9292 >>> y =
FPVal(-20.0, s)
9297 >>>
fpAbs(-1.25*(2**4))
9303 [a] = _coerce_fp_expr_list([a], ctx) 9304 return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx) 9306 def fpNeg(a, ctx=None): 9307 """Create a Z3 floating-point addition expression.
9318 [a] = _coerce_fp_expr_list([a], ctx) 9319 return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx) 9321 def _mk_fp_unary(f, rm, a, ctx): 9323 [a] = _coerce_fp_expr_list([a], ctx) 9325 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9326 _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression") 9327 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx) 9329 def _mk_fp_unary_norm(f, a, ctx): 9331 [a] = _coerce_fp_expr_list([a], ctx) 9333 _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression") 9334 return FPRef(f(ctx.ref(), a.as_ast()), ctx) 9336 def _mk_fp_unary_pred(f, a, ctx): 9338 [a] = _coerce_fp_expr_list([a], ctx) 9340 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9341 return BoolRef(f(ctx.ref(), a.as_ast()), ctx) 9343 def _mk_fp_bin(f, rm, a, b, ctx): 9345 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9347 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9348 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9349 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx) 9351 def _mk_fp_bin_norm(f, a, b, ctx): 9353 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9355 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression") 9356 return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 9358 def _mk_fp_bin_pred(f, a, b, ctx): 9360 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9362 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9363 return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 9365 def _mk_fp_tern(f, rm, a, b, c, ctx): 9367 [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx) 9369 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9370 _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") 9371 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx) 9373 def fpAdd(rm, a, b, ctx=None): 9374 """Create a Z3 floating-point addition expression.
9384 >>>
fpAdd(rm, x, y).sort()
9387 return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx) 9389 def fpSub(rm, a, b, ctx=None): 9390 """Create a Z3 floating-point subtraction expression.
9398 >>>
fpSub(rm, x, y).sort()
9401 return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx) 9403 def fpMul(rm, a, b, ctx=None): 9404 """Create a Z3 floating-point multiplication expression.
9412 >>>
fpMul(rm, x, y).sort()
9415 return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx) 9417 def fpDiv(rm, a, b, ctx=None): 9418 """Create a Z3 floating-point division expression.
9426 >>>
fpDiv(rm, x, y).sort()
9429 return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx) 9431 def fpRem(a, b, ctx=None): 9432 """Create a Z3 floating-point remainder expression.
9439 >>>
fpRem(x, y).sort()
9442 return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx) 9444 def fpMin(a, b, ctx=None): 9445 """Create a Z3 floating-point minimum expression.
9453 >>>
fpMin(x, y).sort()
9456 return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx) 9458 def fpMax(a, b, ctx=None): 9459 """Create a Z3 floating-point maximum expression.
9467 >>>
fpMax(x, y).sort()
9470 return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx) 9472 def fpFMA(rm, a, b, c, ctx=None): 9473 """Create a Z3 floating-point fused multiply-add expression.
9475 return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx) 9477 def fpSqrt(rm, a, ctx=None): 9478 """Create a Z3 floating-point square root expression.
9480 return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx) 9482 def fpRoundToIntegral(rm, a, ctx=None): 9483 """Create a Z3 floating-point roundToIntegral expression.
9485 return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx) 9487 def fpIsNaN(a, ctx=None): 9488 """Create a Z3 floating-point isNaN expression.
9496 return _mk_fp_unary_norm(Z3_mk_fpa_is_nan, a, ctx) 9498 def fpIsInf(a, ctx=None): 9499 """Create a Z3 floating-point isInfinite expression.
9506 return _mk_fp_unary_norm(Z3_mk_fpa_is_infinite, a, ctx) 9508 def fpIsZero(a, ctx=None): 9509 """Create a Z3 floating-point isZero expression.
9511 return _mk_fp_unary_norm(Z3_mk_fpa_is_zero, a, ctx) 9513 def fpIsNormal(a, ctx=None): 9514 """Create a Z3 floating-point isNormal expression.
9516 return _mk_fp_unary_norm(Z3_mk_fpa_is_normal, a, ctx) 9518 def fpIsSubnormal(a, ctx=None): 9519 """Create a Z3 floating-point isSubnormal expression.
9521 return _mk_fp_unary_norm(Z3_mk_fpa_is_subnormal, a, ctx) 9523 def fpIsNegative(a, ctx=None): 9524 """Create a Z3 floating-point isNegative expression.
9526 return _mk_fp_unary_norm(Z3_mk_fpa_is_negative, a, ctx) 9528 def fpIsPositive(a, ctx=None): 9529 """Create a Z3 floating-point isPositive expression.
9531 return _mk_fp_unary_norm(Z3_mk_fpa_is_positive, a, ctx) 9532 return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) 9534 def _check_fp_args(a, b): 9536 _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") 9538 def fpLT(a, b, ctx=None): 9539 """Create the Z3 floating-point expression `other < self`.
9547 return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx) 9549 def fpLEQ(a, b, ctx=None): 9550 """Create the Z3 floating-point expression `other <= self`.
9555 >>> (x <= y).sexpr()
9558 return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx) 9560 def fpGT(a, b, ctx=None): 9561 """Create the Z3 floating-point expression `other > self`.
9569 return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx) 9571 def fpGEQ(a, b, ctx=None): 9572 """Create the Z3 floating-point expression `other >= self`.
9577 >>> (x >= y).sexpr()
9580 return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx) 9582 def fpEQ(a, b, ctx=None): 9583 """Create the Z3 floating-point expression `
fpEQ(other, self)`.
9588 >>>
fpEQ(x, y).sexpr()
9591 return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx) 9593 def fpNEQ(a, b, ctx=None): 9594 """Create the Z3 floating-point expression `
Not(
fpEQ(other, self))`.
9599 >>> (x != y).sexpr()
9602 return Not(fpEQ(a, b, ctx)) 9604 def fpFP(sgn, exp, sig, ctx=None): 9605 """Create the Z3 floating-point value `
fpFP(sgn, sig, exp)`
from the three bit-vectors sgn, sig,
and exp.
9610 fpFP(1, 127, 4194304)
9611 >>> xv =
FPVal(-1.5, s)
9615 >>> slvr.add(
fpEQ(x, xv))
9618 >>> xv =
FPVal(+1.5, s)
9622 >>> slvr.add(
fpEQ(x, xv))
9626 _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch") 9627 _z3_assert(sgn.sort().size() == 1, "sort mismatch") 9629 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch") 9630 return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx) 9632 def fpToFP(a1, a2=None, a3=None, ctx=None): 9633 """Create a Z3 floating-point conversion expression
from other term sorts
9636 From a bit-vector term
in IEEE 754-2008 format:
9642 From a floating-point term with different precision:
9653 From a signed bit-vector term:
9659 if is_bv(a1) and is_fp_sort(a2): 9660 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx) 9661 elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3): 9662 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9663 elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3): 9664 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9665 elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3): 9666 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9668 raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.") 9670 def fpBVToFP(v, sort, ctx=None): 9671 """Create a Z3 floating-point conversion expression that represents the
9672 conversion
from a bit-vector term to a floating-point term.
9681 _z3_assert(is_bv(v), "First argument must be a Z3 floating-point rounding mode expression.") 9682 _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.") 9684 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx) 9686 def fpFPToFP(rm, v, sort, ctx=None): 9687 """Create a Z3 floating-point conversion expression that represents the
9688 conversion
from a floating-point term to a floating-point term of different precision.
9699 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9700 _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.") 9701 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9703 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9705 def fpRealToFP(rm, v, sort, ctx=None): 9706 """Create a Z3 floating-point conversion expression that represents the
9707 conversion
from a real term to a floating-point term.
9716 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9717 _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.") 9718 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9720 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9722 def fpSignedToFP(rm, v, sort, ctx=None): 9723 """Create a Z3 floating-point conversion expression that represents the
9724 conversion
from a signed bit-vector term (encoding an integer) to a floating-point term.
9733 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9734 _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") 9735 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9737 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9739 def fpUnsignedToFP(rm, v, sort, ctx=None): 9740 """Create a Z3 floating-point conversion expression that represents the
9741 conversion
from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9750 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9751 _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") 9752 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9754 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9756 def fpToFPUnsigned(rm, x, s, ctx=None): 9757 """Create a Z3 floating-point conversion expression,
from unsigned bit-vector to floating-point expression.
""" 9759 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9760 _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression") 9761 _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort") 9763 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx) 9765 def fpToSBV(rm, x, s, ctx=None): 9766 """Create a Z3 floating-point conversion expression,
from floating-point expression to signed bit-vector.
9780 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9781 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") 9782 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") 9784 return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9786 def fpToUBV(rm, x, s, ctx=None): 9787 """Create a Z3 floating-point conversion expression,
from floating-point expression to unsigned bit-vector.
9801 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9802 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") 9803 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") 9805 return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9807 def fpToReal(x, ctx=None): 9808 """Create a Z3 floating-point conversion expression,
from floating-point expression to real.
9822 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9824 return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx) 9826 def fpToIEEEBV(x, ctx=None): 9827 """\brief Conversion of a floating-point term into a bit-vector term
in IEEE 754-2008 format.
9829 The size of the resulting bit-vector
is automatically determined.
9831 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9832 knows only one NaN
and it will always produce the same bit-vector representation of
9847 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9849 return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx) 9853 ######################################### 9855 # Strings, Sequences and Regular expressions 9857 ######################################### 9859 class SeqSortRef(SortRef): 9860 """Sequence sort.
""" 9862 def is_string(self): 9863 """Determine
if sort
is a string
9871 return Z3_is_string_sort(self.ctx_ref(), self.ast) 9874 def StringSort(ctx=None): 9875 """Create a string sort
9881 return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx) 9885 """Create a sequence sort over elements provided
in the argument
9890 return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx) 9892 class SeqRef(ExprRef): 9893 """Sequence expression.
""" 9896 return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 9898 def __add__(self, other): 9899 return Concat(self, other) 9901 def __radd__(self, other): 9902 return Concat(other, self) 9904 def __getitem__(self, i): 9906 i = IntVal(i, self.ctx) 9907 return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) 9909 def is_string(self): 9910 return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast())) 9912 def is_string_value(self): 9913 return Z3_is_string(self.ctx_ref(), self.as_ast()) 9915 def as_string(self): 9916 """Return a string representation of sequence expression.
""" 9917 if self.is_string_value(): 9918 return Z3_get_string(self.ctx_ref(), self.as_ast()) 9919 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 9922 def _coerce_seq(s, ctx=None): 9923 if isinstance(s, str): 9925 s = StringVal(s, ctx) 9927 raise Z3Exception("Non-expression passed as a sequence") 9929 raise Z3Exception("Non-sequence passed as a sequence") 9932 def _get_ctx2(a, b, ctx=None): 9942 """Return `
True`
if `a`
is a Z3 sequence expression.
9948 return isinstance(a, SeqRef) 9951 """Return `
True`
if `a`
is a Z3 string expression.
9955 return isinstance(a, SeqRef) and a.is_string() 9957 def is_string_value(a): 9958 """return 'True' if 'a' is a Z3 string constant expression.
9964 return isinstance(a, SeqRef) and a.is_string_value() 9967 def StringVal(s, ctx=None): 9968 """create a string expression
""" 9970 return SeqRef(Z3_mk_string(ctx.ref(), s), ctx) 9972 def String(name, ctx=None): 9973 """Return a string constant named `name`. If `ctx=
None`, then the
global context
is used.
9978 return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx) 9980 def SubString(s, offset, length): 9981 """Extract substring
or subsequence starting at offset
""" 9982 return Extract(s, offset, length) 9984 def SubSeq(s, offset, length): 9985 """Extract substring
or subsequence starting at offset
""" 9986 return Extract(s, offset, length) 9988 def Strings(names, ctx=None): 9989 """Return a tuple of String constants.
""" 9991 if isinstance(names, str): 9992 names = names.split(" ") 9993 return [String(name, ctx) for name in names] 9996 """Create the empty sequence of the given sort
10008 if isinstance(s, SeqSortRef): 10009 return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx) 10010 if isinstance(s, ReSortRef): 10011 return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx) 10012 raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty") 10015 """Create the regular expression that accepts the universal language
10023 if isinstance(s, ReSortRef): 10024 return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx) 10025 raise Z3Exception("Non-sequence, non-regular expression sort passed to Full") 10029 """Create a singleton sequence
""" 10030 return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx) 10032 def PrefixOf(a, b): 10033 """Check
if 'a' is a prefix of
'b' 10041 ctx = _get_ctx2(a, b) 10042 a = _coerce_seq(a, ctx) 10043 b = _coerce_seq(b, ctx) 10044 return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 10046 def SuffixOf(a, b): 10047 """Check
if 'a' is a suffix of
'b' 10055 ctx = _get_ctx2(a, b) 10056 a = _coerce_seq(a, ctx) 10057 b = _coerce_seq(b, ctx) 10058 return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 10060 def Contains(a, b): 10061 """Check
if 'a' contains
'b' 10068 >>> x, y, z =
Strings(
'x y z')
10073 ctx = _get_ctx2(a, b) 10074 a = _coerce_seq(a, ctx) 10075 b = _coerce_seq(b, ctx) 10076 return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 10079 def Replace(s, src, dst): 10080 """Replace the first occurrence of
'src' by
'dst' in 's' 10081 >>> r =
Replace(
"aaa",
"a",
"b")
10085 ctx = _get_ctx2(dst, s) 10086 if ctx is None and is_expr(src): 10088 src = _coerce_seq(src, ctx) 10089 dst = _coerce_seq(dst, ctx) 10090 s = _coerce_seq(s, ctx) 10091 return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx) 10093 def IndexOf(s, substr): 10094 return IndexOf(s, substr, IntVal(0)) 10096 def IndexOf(s, substr, offset): 10097 """Retrieve the index of substring within a string starting at a specified offset.
10104 if is_expr(offset): 10106 ctx = _get_ctx2(s, substr, ctx) 10107 s = _coerce_seq(s, ctx) 10108 substr = _coerce_seq(substr, ctx) 10109 if _is_int(offset): 10110 offset = IntVal(offset, ctx) 10111 return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx) 10114 """Obtain the length of a sequence
's' 10120 return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx) 10123 """Convert string expression to integer
10135 return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx) 10139 """Convert integer expression to string
""" 10142 return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx) 10145 def Re(s, ctx=None): 10146 """The regular expression that accepts sequence
's' 10151 s = _coerce_seq(s, ctx) 10152 return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx) 10157 ## Regular expressions 10159 class ReSortRef(SortRef): 10160 """Regular expression sort.
""" 10165 return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx) 10166 if s is None or isinstance(s, Context): 10168 return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), s.ctx) 10169 raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument") 10172 class ReRef(ExprRef): 10173 """Regular expressions.
""" 10175 def __add__(self, other): 10176 return Union(self, other) 10180 return isinstance(s, ReRef) 10184 """Create regular expression membership test
10193 s = _coerce_seq(s, re.ctx) 10194 return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx) 10197 """Create union of regular expressions.
10202 args = _get_args(args) 10205 _z3_assert(sz > 0, "At least one argument expected.") 10206 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 10211 for i in range(sz): 10212 v[i] = args[i].as_ast() 10213 return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx) 10216 """Create the regular expression accepting one
or more repetitions of argument.
10225 return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx) 10228 """Create the regular expression that optionally accepts the argument.
10237 return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx) 10239 def Complement(re): 10240 """Create the complement regular expression.
""" 10241 return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx) 10244 """Create the regular expression accepting zero
or more repetitions of argument.
10253 return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx) 10255 def Loop(re, lo, hi=0): 10256 """Create the regular expression accepting between a lower
and upper bound repetitions
10257 >>> re =
Loop(
Re(
"a"), 1, 3)
10265 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.
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_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.
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
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.
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)
bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
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.