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
64 return isinstance(v, (int, long))
67 return isinstance(v, int)
76 major = ctypes.c_uint(0)
77 minor = ctypes.c_uint(0)
78 build = ctypes.c_uint(0)
79 rev = ctypes.c_uint(0)
81 return "%s.%s.%s" % (major.value, minor.value, build.value)
84 major = ctypes.c_uint(0)
85 minor = ctypes.c_uint(0)
86 build = ctypes.c_uint(0)
87 rev = ctypes.c_uint(0)
89 return (major.value, minor.value, build.value, rev.value)
96 def _z3_assert(cond, msg):
98 raise Z3Exception(msg)
100 def _z3_check_cint_overflow(n, name):
101 _z3_assert(ctypes.c_int(n).value == n, name +
" is too large")
104 """Log interaction to a file. This function must be invoked immediately after init(). """ 108 """Append user-defined string to interaction log. """ 112 """Convert an integer or string into a Z3 symbol.""" 118 def _symbol2py(ctx, s):
119 """Convert a Z3 symbol back into a Python object. """ 130 if len(args) == 1
and (isinstance(args[0], tuple)
or isinstance(args[0], list)):
132 elif len(args) == 1
and (isinstance(args[0], set)
or isinstance(args[0], AstVector)):
133 return [arg
for arg
in args[0]]
140 def _get_args_ast_list(args):
142 if isinstance(args, set)
or isinstance(args, AstVector)
or isinstance(args, tuple):
143 return [arg
for arg
in args]
149 def _to_param_value(val):
150 if isinstance(val, bool):
164 """A Context manages all other Z3 objects, global configuration options, etc. 166 Z3Py uses a default global context. For most applications this is sufficient. 167 An application may use multiple Z3 contexts. Objects created in one context 168 cannot be used in another one. However, several objects may be "translated" from 169 one context to another. It is not safe to access Z3 objects from multiple threads. 170 The only exception is the method `interrupt()` that can be used to interrupt() a long 172 The initialization method receives global configuration options for the new context. 176 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
199 """Return a reference to the actual C pointer to the Z3 context.""" 203 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions. 205 This method can be invoked from a thread different from the one executing the 206 interruptible procedure. 214 """Return a reference to the global Z3 context. 217 >>> x.ctx == main_ctx() 222 >>> x2 = Real('x', c) 229 if _main_ctx
is None:
240 """Set Z3 global (or module) parameters. 242 >>> set_param(precision=10) 245 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
249 if not set_pp_option(k, v):
263 """Reset all global (or module) parameters. 268 """Alias for 'set_param' for backward compatibility. 273 """Return the value of a Z3 global (or module) parameter 275 >>> get_param('nlsat.reorder') 278 ptr = (ctypes.c_char_p * 1)()
280 r = z3core._to_pystr(ptr[0])
282 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
292 """Superclass for all Z3 objects that have support for pretty printing.""" 297 """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions.""" 304 if self.
ctx.ref()
is not None:
308 return _to_ast_ref(self.
ast, self.
ctx)
311 return obj_to_string(self)
314 return obj_to_string(self)
317 return self.
eq(other)
330 elif is_eq(self)
and self.num_args() == 2:
331 return self.arg(0).
eq(self.arg(1))
333 raise Z3Exception(
"Symbolic expressions cannot be cast to concrete Boolean values.")
336 """Return a string representing the AST node in s-expression notation. 339 >>> ((x + 1)*x).sexpr() 345 """Return a pointer to the corresponding C Z3_ast object.""" 349 """Return unique identifier for object. It can be used for hash-tables and maps.""" 353 """Return a reference to the C context where this AST node is stored.""" 354 return self.
ctx.ref()
357 """Return `True` if `self` and `other` are structurally identical. 364 >>> n1 = simplify(n1) 365 >>> n2 = simplify(n2) 370 _z3_assert(
is_ast(other),
"Z3 AST expected")
374 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 380 >>> # Nodes in different contexts can't be mixed. 381 >>> # However, we can translate nodes from one context to another. 382 >>> x.translate(c2) + y 386 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
393 """Return a hashcode for the `self`. 395 >>> n1 = simplify(Int('x') + 1) 396 >>> n2 = simplify(2 + Int('x') - 1) 397 >>> n1.hash() == n2.hash() 403 """Return `True` if `a` is an AST node. 407 >>> is_ast(IntVal(10)) 411 >>> is_ast(BoolSort()) 413 >>> is_ast(Function('f', IntSort(), IntSort())) 420 return isinstance(a, AstRef)
423 """Return `True` if `a` and `b` are structurally identical AST nodes. 433 >>> eq(simplify(x + 1), simplify(1 + x)) 440 def _ast_kind(ctx, a):
445 def _ctx_from_ast_arg_list(args, default_ctx=None):
453 _z3_assert(ctx == a.ctx,
"Context mismatch")
458 def _ctx_from_ast_args(*args):
459 return _ctx_from_ast_arg_list(args)
461 def _to_func_decl_array(args):
463 _args = (FuncDecl * sz)()
465 _args[i] = args[i].as_func_decl()
468 def _to_ast_array(args):
472 _args[i] = args[i].as_ast()
475 def _to_ref_array(ref, args):
479 _args[i] = args[i].as_ast()
482 def _to_ast_ref(a, ctx):
483 k = _ast_kind(ctx, a)
485 return _to_sort_ref(a, ctx)
486 elif k == Z3_FUNC_DECL_AST:
487 return _to_func_decl_ref(a, ctx)
489 return _to_expr_ref(a, ctx)
498 def _sort_kind(ctx, s):
502 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.""" 510 """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts. 513 >>> b.kind() == Z3_BOOL_SORT 515 >>> b.kind() == Z3_INT_SORT 517 >>> A = ArraySort(IntSort(), IntSort()) 518 >>> A.kind() == Z3_ARRAY_SORT 520 >>> A.kind() == Z3_INT_SORT 523 return _sort_kind(self.
ctx, self.
ast)
526 """Return `True` if `self` is a subsort of `other`. 528 >>> IntSort().subsort(RealSort()) 534 """Try to cast `val` as an element of sort `self`. 536 This method is used in Z3Py to convert Python objects such as integers, 537 floats, longs and strings into Z3 expressions. 540 >>> RealSort().cast(x) 544 _z3_assert(
is_expr(val),
"Z3 expression expected")
545 _z3_assert(self.
eq(val.sort()),
"Sort mismatch")
549 """Return the name (string) of sort `self`. 551 >>> BoolSort().name() 553 >>> ArraySort(IntSort(), IntSort()).name() 559 """Return `True` if `self` and `other` are the same Z3 sort. 562 >>> p.sort() == BoolSort() 564 >>> p.sort() == IntSort() 572 """Return `True` if `self` and `other` are not the same Z3 sort. 575 >>> p.sort() != BoolSort() 577 >>> p.sort() != IntSort() 584 return AstRef.__hash__(self)
587 """Return `True` if `s` is a Z3 sort. 589 >>> is_sort(IntSort()) 591 >>> is_sort(Int('x')) 593 >>> is_expr(Int('x')) 596 return isinstance(s, SortRef)
598 def _to_sort_ref(s, ctx):
600 _z3_assert(isinstance(s, Sort),
"Z3 Sort expected")
601 k = _sort_kind(ctx, s)
602 if k == Z3_BOOL_SORT:
604 elif k == Z3_INT_SORT
or k == Z3_REAL_SORT:
606 elif k == Z3_BV_SORT:
608 elif k == Z3_ARRAY_SORT:
610 elif k == Z3_DATATYPE_SORT:
612 elif k == Z3_FINITE_DOMAIN_SORT:
614 elif k == Z3_FLOATING_POINT_SORT:
616 elif k == Z3_ROUNDING_MODE_SORT:
618 elif k == Z3_RE_SORT:
620 elif k == Z3_SEQ_SORT:
625 return _to_sort_ref(
Z3_get_sort(ctx.ref(), a), ctx)
628 """Create a new uninterpreted sort named `name`. 630 If `ctx=None`, then the new sort is declared in the global Z3Py context. 632 >>> A = DeclareSort('A') 633 >>> a = Const('a', A) 634 >>> b = Const('b', A) 652 """Function declaration. Every constant and function have an associated declaration. 654 The declaration assigns a name, a sort (i.e., type), and for function 655 the sort (i.e., type) of each of its arguments. Note that, in Z3, 656 a constant is a function with 0 arguments. 668 """Return the name of the function declaration `self`. 670 >>> f = Function('f', IntSort(), IntSort()) 673 >>> isinstance(f.name(), str) 679 """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0. 681 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 688 """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`. 690 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 697 _z3_assert(i < self.
arity(),
"Index out of bounds")
701 """Return the sort of the range of a function declaration. For constants, this is the sort of the constant. 703 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 710 """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc. 713 >>> d = (x + 1).decl() 714 >>> d.kind() == Z3_OP_ADD 716 >>> d.kind() == Z3_OP_MUL 724 result = [
None for i
in range(n) ]
727 if k == Z3_PARAMETER_INT:
729 elif k == Z3_PARAMETER_DOUBLE:
731 elif k == Z3_PARAMETER_RATIONAL:
733 elif k == Z3_PARAMETER_SYMBOL:
735 elif k == Z3_PARAMETER_SORT:
737 elif k == Z3_PARAMETER_AST:
739 elif k == Z3_PARAMETER_FUNC_DECL:
746 """Create a Z3 application expression using the function `self`, and the given arguments. 748 The arguments must be Z3 expressions. This method assumes that 749 the sorts of the elements in `args` match the sorts of the 750 domain. Limited coercion is supported. For example, if 751 args[0] is a Python integer, and the function expects a Z3 752 integer, then the argument is automatically converted into a 755 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 763 args = _get_args(args)
766 _z3_assert(num == self.
arity(),
"Incorrect number of arguments to %s" % self)
767 _args = (Ast * num)()
772 tmp = self.
domain(i).cast(args[i])
774 _args[i] = tmp.as_ast()
778 """Return `True` if `a` is a Z3 function declaration. 780 >>> f = Function('f', IntSort(), IntSort()) 787 return isinstance(a, FuncDeclRef)
790 """Create a new Z3 uninterpreted function with the given sorts. 792 >>> f = Function('f', IntSort(), IntSort()) 798 _z3_assert(len(sig) > 0,
"At least two arguments expected")
802 _z3_assert(
is_sort(rng),
"Z3 sort expected")
803 dom = (Sort * arity)()
804 for i
in range(arity):
806 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
811 def _to_func_decl_ref(a, ctx):
815 """Create a new Z3 recursive with the given sorts.""" 818 _z3_assert(len(sig) > 0,
"At least two arguments expected")
822 _z3_assert(
is_sort(rng),
"Z3 sort expected")
823 dom = (Sort * arity)()
824 for i
in range(arity):
826 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
832 """Set the body of a recursive function. 833 Recursive definitions are only unfolded during search. 835 >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx)) 836 >>> n = Int('n', ctx) 837 >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1))) 840 >>> s = Solver(ctx=ctx) 841 >>> s.add(fac(n) < 3) 844 >>> s.model().eval(fac(5)) 850 args = _get_args(args)
854 _args[i] = args[i].ast
864 """Constraints, formulas and terms are expressions in Z3. 866 Expressions are ASTs. Every expression has a sort. 867 There are three main kinds of expressions: 868 function applications, quantifiers and bounded variables. 869 A constant is a function application with 0 arguments. 870 For quantifier free problems, all expressions are 871 function applications. 880 """Return the sort of expression `self`. 892 """Shorthand for `self.sort().kind()`. 894 >>> a = Array('a', IntSort(), IntSort()) 895 >>> a.sort_kind() == Z3_ARRAY_SORT 897 >>> a.sort_kind() == Z3_INT_SORT 900 return self.
sort().kind()
903 """Return a Z3 expression that represents the constraint `self == other`. 905 If `other` is `None`, then this method simply returns `False`. 916 a, b = _coerce_exprs(self, other)
921 return AstRef.__hash__(self)
924 """Return a Z3 expression that represents the constraint `self != other`. 926 If `other` is `None`, then this method simply returns `True`. 937 a, b = _coerce_exprs(self, other)
938 _args, sz = _to_ast_array((a, b))
945 """Return the Z3 function declaration associated with a Z3 application. 947 >>> f = Function('f', IntSort(), IntSort()) 956 _z3_assert(
is_app(self),
"Z3 application expected")
960 """Return the number of arguments of a Z3 application. 964 >>> (a + b).num_args() 966 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 972 _z3_assert(
is_app(self),
"Z3 application expected")
976 """Return argument `idx` of the application `self`. 978 This method assumes that `self` is a function application with at least `idx+1` arguments. 982 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 992 _z3_assert(
is_app(self),
"Z3 application expected")
993 _z3_assert(idx < self.
num_args(),
"Invalid argument index")
997 """Return a list containing the children of the given expression 1001 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 1011 def _to_expr_ref(a, ctx):
1012 if isinstance(a, Pattern):
1016 if k == Z3_QUANTIFIER_AST:
1019 if sk == Z3_BOOL_SORT:
1021 if sk == Z3_INT_SORT:
1022 if k == Z3_NUMERAL_AST:
1025 if sk == Z3_REAL_SORT:
1026 if k == Z3_NUMERAL_AST:
1028 if _is_algebraic(ctx, a):
1031 if sk == Z3_BV_SORT:
1032 if k == Z3_NUMERAL_AST:
1036 if sk == Z3_ARRAY_SORT:
1038 if sk == Z3_DATATYPE_SORT:
1040 if sk == Z3_FLOATING_POINT_SORT:
1041 if k == Z3_APP_AST
and _is_numeral(ctx, a):
1044 return FPRef(a, ctx)
1045 if sk == Z3_FINITE_DOMAIN_SORT:
1046 if k == Z3_NUMERAL_AST:
1050 if sk == Z3_ROUNDING_MODE_SORT:
1052 if sk == Z3_SEQ_SORT:
1054 if sk == Z3_RE_SORT:
1055 return ReRef(a, ctx)
1058 def _coerce_expr_merge(s, a):
1071 _z3_assert(s1.ctx == s.ctx,
"context mismatch")
1072 _z3_assert(
False,
"sort mismatch")
1076 def _coerce_exprs(a, b, ctx=None):
1078 a = _py2expr(a, ctx)
1079 b = _py2expr(b, ctx)
1081 s = _coerce_expr_merge(s, a)
1082 s = _coerce_expr_merge(s, b)
1088 def _reduce(f, l, a):
1094 def _coerce_expr_list(alist, ctx=None):
1101 alist = [ _py2expr(a, ctx)
for a
in alist ]
1102 s = _reduce(_coerce_expr_merge, alist,
None)
1103 return [ s.cast(a)
for a
in alist ]
1106 """Return `True` if `a` is a Z3 expression. 1113 >>> is_expr(IntSort()) 1117 >>> is_expr(IntVal(1)) 1120 >>> is_expr(ForAll(x, x >= 0)) 1122 >>> is_expr(FPVal(1.0)) 1125 return isinstance(a, ExprRef)
1128 """Return `True` if `a` is a Z3 function application. 1130 Note that, constants are function applications with 0 arguments. 1137 >>> is_app(IntSort()) 1141 >>> is_app(IntVal(1)) 1144 >>> is_app(ForAll(x, x >= 0)) 1147 if not isinstance(a, ExprRef):
1149 k = _ast_kind(a.ctx, a)
1150 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
1153 """Return `True` if `a` is Z3 constant/variable expression. 1162 >>> is_const(IntVal(1)) 1165 >>> is_const(ForAll(x, x >= 0)) 1168 return is_app(a)
and a.num_args() == 0
1171 """Return `True` if `a` is variable. 1173 Z3 uses de-Bruijn indices for representing bound variables in 1181 >>> f = Function('f', IntSort(), IntSort()) 1182 >>> # Z3 replaces x with bound variables when ForAll is executed. 1183 >>> q = ForAll(x, f(x) == x) 1189 >>> is_var(b.arg(1)) 1192 return is_expr(a)
and _ast_kind(a.ctx, a) == Z3_VAR_AST
1195 """Return the de-Bruijn index of the Z3 bounded variable `a`. 1203 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1204 >>> # Z3 replaces x and y with bound variables when ForAll is executed. 1205 >>> q = ForAll([x, y], f(x, y) == x + y) 1207 f(Var(1), Var(0)) == Var(1) + Var(0) 1211 >>> v1 = b.arg(0).arg(0) 1212 >>> v2 = b.arg(0).arg(1) 1217 >>> get_var_index(v1) 1219 >>> get_var_index(v2) 1223 _z3_assert(
is_var(a),
"Z3 bound variable expected")
1227 """Return `True` if `a` is an application of the given kind `k`. 1231 >>> is_app_of(n, Z3_OP_ADD) 1233 >>> is_app_of(n, Z3_OP_MUL) 1236 return is_app(a)
and a.decl().kind() == k
1238 def If(a, b, c, ctx=None):
1239 """Create a Z3 if-then-else expression. 1243 >>> max = If(x > y, x, y) 1249 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1250 return Cond(a, b, c, ctx)
1252 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1255 b, c = _coerce_exprs(b, c, ctx)
1257 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1258 return _to_expr_ref(
Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1261 """Create a Z3 distinct expression. 1268 >>> Distinct(x, y, z) 1270 >>> simplify(Distinct(x, y, z)) 1272 >>> simplify(Distinct(x, y, z), blast_distinct=True) 1273 And(Not(x == y), Not(x == z), Not(y == z)) 1275 args = _get_args(args)
1276 ctx = _ctx_from_ast_arg_list(args)
1278 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1279 args = _coerce_expr_list(args, ctx)
1280 _args, sz = _to_ast_array(args)
1283 def _mk_bin(f, a, b):
1286 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1287 args[0] = a.as_ast()
1288 args[1] = b.as_ast()
1289 return f(a.ctx.ref(), 2, args)
1292 """Create a constant of the given sort. 1294 >>> Const('x', IntSort()) 1298 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
1303 """Create a several constants of the given sort. 1305 `names` is a string containing the names of all constants to be created. 1306 Blank spaces separate the names of different constants. 1308 >>> x, y, z = Consts('x y z', IntSort()) 1312 if isinstance(names, str):
1313 names = names.split(
" ")
1314 return [
Const(name, sort)
for name
in names]
1317 """Create a fresh constant of a specified sort""" 1318 ctx = _get_ctx(sort.ctx)
1322 """Create a Z3 free variable. Free variables are used to create quantified formulas. 1324 >>> Var(0, IntSort()) 1326 >>> eq(Var(0, IntSort()), Var(0, BoolSort())) 1330 _z3_assert(
is_sort(s),
"Z3 sort expected")
1331 return _to_expr_ref(
Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1335 Create a real free variable. Free variables are used to create quantified formulas. 1336 They are also used to create polynomials. 1345 Create a list of Real free variables. 1346 The variables have ids: 0, 1, ..., n-1 1348 >>> x0, x1, x2, x3 = RealVarVector(4) 1363 """Try to cast `val` as a Boolean. 1365 >>> x = BoolSort().cast(True) 1375 if isinstance(val, bool):
1379 _z3_assert(
is_expr(val),
"True, False or Z3 Boolean expression expected. Received %s" % val)
1380 if not self.
eq(val.sort()):
1381 _z3_assert(self.
eq(val.sort()),
"Value cannot be converted into a Z3 Boolean value")
1385 return isinstance(other, ArithSortRef)
1395 """All Boolean expressions are instances of this class.""" 1403 """Create the Z3 expression `self * other`. 1409 return If(self, other, 0)
1413 """Return `True` if `a` is a Z3 Boolean expression. 1419 >>> is_bool(And(p, q)) 1427 return isinstance(a, BoolRef)
1430 """Return `True` if `a` is the Z3 true expression. 1435 >>> is_true(simplify(p == p)) 1440 >>> # True is a Python Boolean expression 1447 """Return `True` if `a` is the Z3 false expression. 1454 >>> is_false(BoolVal(False)) 1460 """Return `True` if `a` is a Z3 and expression. 1462 >>> p, q = Bools('p q') 1463 >>> is_and(And(p, q)) 1465 >>> is_and(Or(p, q)) 1471 """Return `True` if `a` is a Z3 or expression. 1473 >>> p, q = Bools('p q') 1476 >>> is_or(And(p, q)) 1482 """Return `True` if `a` is a Z3 implication expression. 1484 >>> p, q = Bools('p q') 1485 >>> is_implies(Implies(p, q)) 1487 >>> is_implies(And(p, q)) 1493 """Return `True` if `a` is a Z3 not expression. 1504 """Return `True` if `a` is a Z3 equality expression. 1506 >>> x, y = Ints('x y') 1513 """Return `True` if `a` is a Z3 distinct expression. 1515 >>> x, y, z = Ints('x y z') 1516 >>> is_distinct(x == y) 1518 >>> is_distinct(Distinct(x, y, z)) 1524 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. 1528 >>> p = Const('p', BoolSort()) 1531 >>> r = Function('r', IntSort(), IntSort(), BoolSort()) 1538 return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx) 1540 def BoolVal(val, ctx=None): 1541 """Return the Boolean value `
True`
or `
False`. If `ctx=
None`, then the
global context
is used.
1554 return BoolRef(Z3_mk_false(ctx.ref()), ctx) 1556 return BoolRef(Z3_mk_true(ctx.ref()), ctx) 1558 def Bool(name, ctx=None): 1559 """Return a Boolean constant named `name`. If `ctx=
None`, then the
global context
is used.
1567 return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx) 1569 def Bools(names, ctx=None): 1570 """Return a tuple of Boolean constants.
1572 `names`
is a single string containing all names separated by blank spaces.
1573 If `ctx=
None`, then the
global context
is used.
1575 >>> p, q, r =
Bools(
'p q r')
1576 >>>
And(p,
Or(q, r))
1580 if isinstance(names, str): 1581 names = names.split(" ") 1582 return [Bool(name, ctx) for name in names] 1584 def BoolVector(prefix, sz, ctx=None): 1585 """Return a list of Boolean constants of size `sz`.
1587 The constants are named using the given prefix.
1588 If `ctx=
None`, then the
global context
is used.
1594 And(p__0, p__1, p__2)
1596 return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ] 1598 def FreshBool(prefix='b', ctx=None): 1599 """Return a fresh Boolean constant
in the given context using the given prefix.
1601 If `ctx=
None`, then the
global context
is used.
1609 return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx) 1611 def Implies(a, b, ctx=None): 1612 """Create a Z3 implies expression.
1614 >>> p, q =
Bools(
'p q')
1620 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 1624 return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 1626 def Xor(a, b, ctx=None): 1627 """Create a Z3 Xor expression.
1629 >>> p, q =
Bools(
'p q')
1635 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 1639 return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 1641 def Not(a, ctx=None): 1642 """Create a Z3
not expression
or probe.
1650 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) 1652 # Not is also used to build probes 1653 return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx) 1657 return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx) 1665 def _has_probe(args): 1666 """Return `
True`
if one of the elements of the given collection
is a Z3 probe.
""" 1673 """Create a Z3
and-expression
or and-probe.
1675 >>> p, q, r =
Bools(
'p q r')
1680 And(p__0, p__1, p__2, p__3, p__4)
1684 last_arg = args[len(args)-1] 1685 if isinstance(last_arg, Context): 1686 ctx = args[len(args)-1] 1687 args = args[:len(args)-1] 1688 elif len(args) == 1 and isinstance(args[0], AstVector): 1690 args = [a for a in args[0]] 1693 args = _get_args(args) 1694 ctx_args = _ctx_from_ast_arg_list(args, ctx) 1696 _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") 1697 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") 1698 if _has_probe(args): 1699 return _probe_and(args, ctx) 1701 args = _coerce_expr_list(args, ctx) 1702 _args, sz = _to_ast_array(args) 1703 return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx) 1706 """Create a Z3
or-expression
or or-probe.
1708 >>> p, q, r =
Bools(
'p q r')
1713 Or(p__0, p__1, p__2, p__3, p__4)
1717 last_arg = args[len(args)-1] 1718 if isinstance(last_arg, Context): 1719 ctx = args[len(args)-1] 1720 args = args[:len(args)-1] 1723 args = _get_args(args) 1724 ctx_args = _ctx_from_ast_arg_list(args, ctx) 1726 _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") 1727 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") 1728 if _has_probe(args): 1729 return _probe_or(args, ctx) 1731 args = _coerce_expr_list(args, ctx) 1732 _args, sz = _to_ast_array(args) 1733 return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx) 1735 ######################################### 1739 ######################################### 1741 class PatternRef(ExprRef): 1742 """Patterns are hints
for quantifier instantiation.
1746 return Z3_pattern_to_ast(self.ctx_ref(), self.ast) 1749 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1752 """Return `
True`
if `a`
is a Z3 pattern (hint
for quantifier instantiation.
1756 >>> q =
ForAll(x, f(x) == 0, patterns = [ f(x) ])
1759 >>> q.num_patterns()
1766 return isinstance(a, PatternRef) 1768 def MultiPattern(*args): 1769 """Create a Z3 multi-pattern using the given expressions `*args`
1777 >>> q.num_patterns()
1785 _z3_assert(len(args) > 0, "At least one argument expected") 1786 _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected") 1788 args, sz = _to_ast_array(args) 1789 return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx) 1791 def _to_pattern(arg): 1795 return MultiPattern(arg) 1797 ######################################### 1801 ######################################### 1803 class QuantifierRef(BoolRef): 1804 """Universally
and Existentially quantified formulas.
""" 1810 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1813 """Return the Boolean sort
or sort of Lambda.
""" 1814 if self.is_lambda(): 1815 return _sort(self.ctx, self.as_ast()) 1816 return BoolSort(self.ctx) 1818 def is_forall(self): 1819 """Return `
True`
if `self`
is a universal quantifier.
1823 >>> q =
ForAll(x, f(x) == 0)
1826 >>> q =
Exists(x, f(x) != 0)
1830 return Z3_is_quantifier_forall(self.ctx_ref(), self.ast) 1832 def is_exists(self): 1833 """Return `
True`
if `self`
is an existential quantifier.
1837 >>> q =
ForAll(x, f(x) == 0)
1840 >>> q =
Exists(x, f(x) != 0)
1844 return Z3_is_quantifier_exists(self.ctx_ref(), self.ast) 1846 def is_lambda(self): 1847 """Return `
True`
if `self`
is a
lambda expression.
1854 >>> q =
Exists(x, f(x) != 0)
1858 return Z3_is_lambda(self.ctx_ref(), self.ast) 1861 """Return the weight annotation of `self`.
1865 >>> q =
ForAll(x, f(x) == 0)
1868 >>> q =
ForAll(x, f(x) == 0, weight=10)
1872 return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast)) 1874 def num_patterns(self): 1875 """Return the number of patterns (i.e., quantifier instantiation hints)
in `self`.
1880 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1881 >>> q.num_patterns()
1884 return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast)) 1886 def pattern(self, idx): 1887 """Return a pattern (i.e., quantifier instantiation hints)
in `self`.
1892 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1893 >>> q.num_patterns()
1901 _z3_assert(idx < self.num_patterns(), "Invalid pattern idx") 1902 return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1904 def num_no_patterns(self): 1905 """Return the number of no-patterns.
""" 1906 return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast) 1908 def no_pattern(self, idx): 1909 """Return a no-pattern.
""" 1911 _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx") 1912 return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1915 """Return the expression being quantified.
1919 >>> q =
ForAll(x, f(x) == 0)
1923 return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx) 1926 """Return the number of variables bounded by this quantifier.
1931 >>> q =
ForAll([x, y], f(x, y) >= x)
1935 return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast)) 1937 def var_name(self, idx): 1938 """Return a string representing a name used when displaying the quantifier.
1943 >>> q =
ForAll([x, y], f(x, y) >= x)
1950 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1951 return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx)) 1953 def var_sort(self, idx): 1954 """Return the sort of a bound variable.
1959 >>> q =
ForAll([x, y], f(x, y) >= x)
1966 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1967 return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx) 1970 """Return a list containing a single element self.
body()
1974 >>> q =
ForAll(x, f(x) == 0)
1978 return [ self.body() ] 1980 def is_quantifier(a): 1981 """Return `
True`
if `a`
is a Z3 quantifier.
1985 >>> q =
ForAll(x, f(x) == 0)
1991 return isinstance(a, QuantifierRef) 1993 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 1995 _z3_assert(is_bool(body) or is_app(vs) or (len(vs) > 0 and is_app(vs[0])), "Z3 expression expected") 1996 _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)") 1997 _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected") 1998 _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions") 2004 if not is_expr(body): 2005 body = BoolVal(body, ctx) 2009 _vs = (Ast * num_vars)() 2010 for i in range(num_vars): 2011 ## TODO: Check if is constant 2012 _vs[i] = vs[i].as_ast() 2013 patterns = [ _to_pattern(p) for p in patterns ] 2014 num_pats = len(patterns) 2015 _pats = (Pattern * num_pats)() 2016 for i in range(num_pats): 2017 _pats[i] = patterns[i].ast 2018 _no_pats, num_no_pats = _to_ast_array(no_patterns) 2019 qid = to_symbol(qid, ctx) 2020 skid = to_symbol(skid, ctx) 2021 return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid, 2024 num_no_pats, _no_pats, 2025 body.as_ast()), ctx) 2027 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 2028 """Create a Z3 forall formula.
2030 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
2035 >>>
ForAll([x, y], f(x, y) >= x)
2036 ForAll([x, y], f(x, y) >= x)
2037 >>>
ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2038 ForAll([x, y], f(x, y) >= x)
2039 >>>
ForAll([x, y], f(x, y) >= x, weight=10)
2040 ForAll([x, y], f(x, y) >= x)
2042 return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns) 2044 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 2045 """Create a Z3 exists formula.
2047 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
2053 >>> q =
Exists([x, y], f(x, y) >= x, skid=
"foo")
2055 Exists([x, y], f(x, y) >= x)
2058 >>> r =
Tactic(
'nnf')(q).as_expr()
2062 return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns) 2064 def Lambda(vs, body): 2065 """Create a Z3
lambda expression.
2069 >>> lo, hi, e, i =
Ints(
'lo hi e i')
2070 >>> mem1 =
Lambda([i],
If(
And(lo <= i, i <= hi), e, mem0[i]))
2078 _vs = (Ast * num_vars)() 2079 for i in range(num_vars): 2080 ## TODO: Check if is constant 2081 _vs[i] = vs[i].as_ast() 2082 return QuantifierRef(Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx) 2084 ######################################### 2088 ######################################### 2090 class ArithSortRef(SortRef): 2091 """Real
and Integer sorts.
""" 2094 """Return `
True`
if `self`
is of the sort Real.
2105 return self.kind() == Z3_REAL_SORT 2108 """Return `
True`
if `self`
is of the sort Integer.
2119 return self.kind() == Z3_INT_SORT 2121 def subsort(self, other): 2122 """Return `
True`
if `self`
is a subsort of `other`.
""" 2123 return self.is_int() and is_arith_sort(other) and other.is_real() 2125 def cast(self, val): 2126 """Try to cast `val`
as an Integer
or Real.
2141 _z3_assert(self.ctx == val.ctx, "Context mismatch") 2145 if val_s.is_int() and self.is_real(): 2147 if val_s.is_bool() and self.is_int(): 2148 return If(val, 1, 0) 2149 if val_s.is_bool() and self.is_real(): 2150 return ToReal(If(val, 1, 0)) 2152 _z3_assert(False, "Z3 Integer/Real expression expected" ) 2155 return IntVal(val, self.ctx) 2157 return RealVal(val, self.ctx) 2159 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self) 2161 def is_arith_sort(s): 2162 """Return `
True`
if s
is an arithmetical sort (type).
2170 >>> n =
Int(
'x') + 1
2174 return isinstance(s, ArithSortRef) 2176 class ArithRef(ExprRef): 2177 """Integer
and Real expressions.
""" 2180 """Return the sort (type) of the arithmetical expression `self`.
2187 return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 2190 """Return `
True`
if `self`
is an integer expression.
2201 return self.sort().is_int() 2204 """Return `
True`
if `self`
is an real expression.
2212 return self.sort().is_real() 2214 def __add__(self, other): 2215 """Create the Z3 expression `self + other`.
2224 a, b = _coerce_exprs(self, other) 2225 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx) 2227 def __radd__(self, other): 2228 """Create the Z3 expression `other + self`.
2234 a, b = _coerce_exprs(self, other) 2235 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx) 2237 def __mul__(self, other): 2238 """Create the Z3 expression `self * other`.
2247 if isinstance(other, BoolRef): 2248 return If(other, self, 0) 2249 a, b = _coerce_exprs(self, other) 2250 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx) 2252 def __rmul__(self, other): 2253 """Create the Z3 expression `other * self`.
2259 a, b = _coerce_exprs(self, other) 2260 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx) 2262 def __sub__(self, other): 2263 """Create the Z3 expression `self - other`.
2272 a, b = _coerce_exprs(self, other) 2273 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx) 2275 def __rsub__(self, other): 2276 """Create the Z3 expression `other - self`.
2282 a, b = _coerce_exprs(self, other) 2283 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx) 2285 def __pow__(self, other): 2286 """Create the Z3 expression `self**other` (**
is the power operator).
2296 a, b = _coerce_exprs(self, other) 2297 return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2299 def __rpow__(self, other): 2300 """Create the Z3 expression `other**self` (**
is the power operator).
2310 a, b = _coerce_exprs(self, other) 2311 return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2313 def __div__(self, other): 2314 """Create the Z3 expression `other/self`.
2333 a, b = _coerce_exprs(self, other) 2334 return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2336 def __truediv__(self, other): 2337 """Create the Z3 expression `other/self`.
""" 2338 return self.__div__(other) 2340 def __rdiv__(self, other): 2341 """Create the Z3 expression `other/self`.
2354 a, b = _coerce_exprs(self, other) 2355 return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2357 def __rtruediv__(self, other): 2358 """Create the Z3 expression `other/self`.
""" 2359 return self.__rdiv__(other) 2361 def __mod__(self, other): 2362 """Create the Z3 expression `other%self`.
2371 a, b = _coerce_exprs(self, other) 2373 _z3_assert(a.is_int(), "Z3 integer expression expected") 2374 return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2376 def __rmod__(self, other): 2377 """Create the Z3 expression `other%self`.
2383 a, b = _coerce_exprs(self, other) 2385 _z3_assert(a.is_int(), "Z3 integer expression expected") 2386 return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2389 """Return an expression representing `-self`.
2397 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx) 2408 def __le__(self, other): 2409 """Create the Z3 expression `other <= self`.
2411 >>> x, y =
Ints(
'x y')
2418 a, b = _coerce_exprs(self, other) 2419 return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2421 def __lt__(self, other): 2422 """Create the Z3 expression `other < self`.
2424 >>> x, y =
Ints(
'x y')
2431 a, b = _coerce_exprs(self, other) 2432 return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2434 def __gt__(self, other): 2435 """Create the Z3 expression `other > self`.
2437 >>> x, y =
Ints(
'x y')
2444 a, b = _coerce_exprs(self, other) 2445 return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2447 def __ge__(self, other): 2448 """Create the Z3 expression `other >= self`.
2450 >>> x, y =
Ints(
'x y')
2457 a, b = _coerce_exprs(self, other) 2458 return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2461 """Return `
True`
if `a`
is an arithmetical expression.
2478 return isinstance(a, ArithRef) 2481 """Return `
True`
if `a`
is an integer expression.
2496 return is_arith(a) and a.is_int() 2499 """Return `
True`
if `a`
is a real expression.
2514 return is_arith(a) and a.is_real() 2516 def _is_numeral(ctx, a): 2517 return Z3_is_numeral_ast(ctx.ref(), a) 2519 def _is_algebraic(ctx, a): 2520 return Z3_is_algebraic_number(ctx.ref(), a) 2522 def is_int_value(a): 2523 """Return `
True`
if `a`
is an integer value of sort Int.
2531 >>> n =
Int(
'x') + 1
2543 return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast()) 2545 def is_rational_value(a): 2546 """Return `
True`
if `a`
is rational value of sort Real.
2556 >>> n =
Real(
'x') + 1
2564 return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast()) 2566 def is_algebraic_value(a): 2567 """Return `
True`
if `a`
is an algebraic value of sort Real.
2577 return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast()) 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_ADD) 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_MUL) 2602 """Return `
True`
if `a`
is an expression of the form b - c.
2604 >>> x, y =
Ints(
'x y')
2610 return is_app_of(a, Z3_OP_SUB) 2613 """Return `
True`
if `a`
is an expression of the form b / c.
2615 >>> x, y =
Reals(
'x y')
2620 >>> x, y =
Ints(
'x y')
2626 return is_app_of(a, Z3_OP_DIV) 2629 """Return `
True`
if `a`
is an expression of the form b div c.
2631 >>> x, y =
Ints(
'x y')
2637 return is_app_of(a, Z3_OP_IDIV) 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_MOD) 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_LE) 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_LT) 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_GE) 2684 """Return `
True`
if `a`
is an expression of the form b > c.
2686 >>> x, y =
Ints(
'x y')
2692 return is_app_of(a, Z3_OP_GT) 2695 """Return `
True`
if `a`
is an expression of the form
IsInt(b).
2703 return is_app_of(a, Z3_OP_IS_INT) 2706 """Return `
True`
if `a`
is an expression of the form
ToReal(b).
2717 return is_app_of(a, Z3_OP_TO_REAL) 2720 """Return `
True`
if `a`
is an expression of the form
ToInt(b).
2731 return is_app_of(a, Z3_OP_TO_INT) 2733 class IntNumRef(ArithRef): 2734 """Integer values.
""" 2737 """Return a Z3 integer numeral
as a Python long (bignum) numeral.
2746 _z3_assert(self.is_int(), "Integer value expected") 2747 return int(self.as_string()) 2749 def as_string(self): 2750 """Return a Z3 integer numeral
as a Python string.
2755 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2757 class RatNumRef(ArithRef): 2758 """Rational values.
""" 2760 def numerator(self): 2761 """ Return the numerator of a Z3 rational numeral.
2773 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx) 2775 def denominator(self): 2776 """ Return the denominator of a Z3 rational numeral.
2784 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx) 2786 def numerator_as_long(self): 2787 """ Return the numerator
as a Python long.
2794 >>> v.numerator_as_long() + 1 == 10000000001
2797 return self.numerator().as_long() 2799 def denominator_as_long(self): 2800 """ Return the denominator
as a Python long.
2805 >>> v.denominator_as_long()
2808 return self.denominator().as_long() 2816 def is_int_value(self): 2817 return self.denominator().is_int() and self.denominator_as_long() == 1 2820 _z3_assert(self.is_int_value(), "Expected integer fraction") 2821 return self.numerator_as_long() 2823 def as_decimal(self, prec): 2824 """ Return a Z3 rational value
as a string
in decimal notation using at most `prec` decimal places.
2833 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2835 def as_string(self): 2836 """Return a Z3 rational numeral
as a Python string.
2842 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2844 def as_fraction(self): 2845 """Return a Z3 rational
as a Python Fraction object.
2851 return Fraction(self.numerator_as_long(), self.denominator_as_long()) 2853 class AlgebraicNumRef(ArithRef): 2854 """Algebraic irrational values.
""" 2856 def approx(self, precision=10): 2857 """Return a Z3 rational number that approximates the algebraic number `self`.
2858 The result `r`
is such that |r - self| <= 1/10^precision
2862 6838717160008073720548335/4835703278458516698824704
2866 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx) 2867 def as_decimal(self, prec): 2868 """Return a string representation of the algebraic number `self`
in decimal notation using `prec` decimal places
2871 >>> x.as_decimal(10)
2873 >>> x.as_decimal(20)
2874 '1.41421356237309504880?' 2876 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2878 def _py2expr(a, ctx=None): 2879 if isinstance(a, bool): 2880 return BoolVal(a, ctx) 2882 return IntVal(a, ctx) 2883 if isinstance(a, float): 2884 return RealVal(a, ctx) 2888 _z3_assert(False, "Python bool, int, long or float expected") 2890 def IntSort(ctx=None): 2891 """Return the integer sort
in the given context. If `ctx=
None`, then the
global context
is used.
2904 return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx) 2906 def RealSort(ctx=None): 2907 """Return the real sort
in the given context. If `ctx=
None`, then the
global context
is used.
2920 return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx) 2922 def _to_int_str(val): 2923 if isinstance(val, float): 2924 return str(int(val)) 2925 elif isinstance(val, bool): 2932 elif isinstance(val, str): 2935 _z3_assert(False, "Python value cannot be used as a Z3 integer") 2937 def IntVal(val, ctx=None): 2938 """Return a Z3 integer value. If `ctx=
None`, then the
global context
is used.
2946 return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx) 2948 def RealVal(val, ctx=None): 2949 """Return a Z3 real value.
2951 `val` may be a Python int, long, float
or string representing a number
in decimal
or rational notation.
2952 If `ctx=
None`, then the
global context
is used.
2964 return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx) 2966 def RatVal(a, b, ctx=None): 2967 """Return a Z3 rational a/b.
2969 If `ctx=
None`, then the
global context
is used.
2977 _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer") 2978 _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer") 2979 return simplify(RealVal(a, ctx)/RealVal(b, ctx)) 2981 def Q(a, b, ctx=None): 2982 """Return a Z3 rational a/b.
2984 If `ctx=
None`, then the
global context
is used.
2991 return simplify(RatVal(a, b)) 2993 def Int(name, ctx=None): 2994 """Return an integer constant named `name`. If `ctx=
None`, then the
global context
is used.
3003 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx) 3005 def Ints(names, ctx=None): 3006 """Return a tuple of Integer constants.
3008 >>> x, y, z =
Ints(
'x y z')
3013 if isinstance(names, str): 3014 names = names.split(" ") 3015 return [Int(name, ctx) for name in names] 3017 def IntVector(prefix, sz, ctx=None): 3018 """Return a list of integer constants of size `sz`.
3026 return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ] 3028 def FreshInt(prefix='x', ctx=None): 3029 """Return a fresh integer constant
in the given context using the given prefix.
3039 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx) 3041 def Real(name, ctx=None): 3042 """Return a real constant named `name`. If `ctx=
None`, then the
global context
is used.
3051 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx) 3053 def Reals(names, ctx=None): 3054 """Return a tuple of real constants.
3056 >>> x, y, z =
Reals(
'x y z')
3059 >>>
Sum(x, y, z).sort()
3063 if isinstance(names, str): 3064 names = names.split(" ") 3065 return [Real(name, ctx) for name in names] 3067 def RealVector(prefix, sz, ctx=None): 3068 """Return a list of real constants of size `sz`.
3078 return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ] 3080 def FreshReal(prefix='b', ctx=None): 3081 """Return a fresh real constant
in the given context using the given prefix.
3091 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx) 3094 """ Return the Z3 expression
ToReal(a).
3106 _z3_assert(a.is_int(), "Z3 integer expression expected.") 3108 return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx) 3111 """ Return the Z3 expression
ToInt(a).
3123 _z3_assert(a.is_real(), "Z3 real expression expected.") 3125 return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx) 3128 """ Return the Z3 predicate
IsInt(a).
3131 >>>
IsInt(x +
"1/2")
3135 >>>
solve(
IsInt(x +
"1/2"), x > 0, x < 1, x !=
"1/2")
3139 _z3_assert(a.is_real(), "Z3 real expression expected.") 3141 return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx) 3143 def Sqrt(a, ctx=None): 3144 """ Return a Z3 expression which represents the square root of a.
3155 def Cbrt(a, ctx=None): 3156 """ Return a Z3 expression which represents the cubic root of a.
3167 ######################################### 3171 ######################################### 3173 class BitVecSortRef(SortRef): 3174 """Bit-vector sort.
""" 3177 """Return the size (number of bits) of the bit-vector sort `self`.
3183 return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast)) 3185 def subsort(self, other): 3186 return is_bv_sort(other) and self.size() < other.size() 3188 def cast(self, val): 3189 """Try to cast `val`
as a Bit-Vector.
3194 >>> b.cast(10).
sexpr()
3199 _z3_assert(self.ctx == val.ctx, "Context mismatch") 3200 # Idea: use sign_extend if sort of val is a bitvector of smaller size 3203 return BitVecVal(val, self) 3206 """Return
True if `s`
is a Z3 bit-vector sort.
3213 return isinstance(s, BitVecSortRef) 3215 class BitVecRef(ExprRef): 3216 """Bit-vector expressions.
""" 3219 """Return the sort of the bit-vector expression `self`.
3227 return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 3230 """Return the number of bits of the bit-vector expression `self`.
3238 return self.sort().size() 3240 def __add__(self, other): 3241 """Create the Z3 expression `self + other`.
3250 a, b = _coerce_exprs(self, other) 3251 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3253 def __radd__(self, other): 3254 """Create the Z3 expression `other + self`.
3260 a, b = _coerce_exprs(self, other) 3261 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3263 def __mul__(self, other): 3264 """Create the Z3 expression `self * other`.
3273 a, b = _coerce_exprs(self, other) 3274 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3276 def __rmul__(self, other): 3277 """Create the Z3 expression `other * self`.
3283 a, b = _coerce_exprs(self, other) 3284 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3286 def __sub__(self, other): 3287 """Create the Z3 expression `self - other`.
3296 a, b = _coerce_exprs(self, other) 3297 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3299 def __rsub__(self, other): 3300 """Create the Z3 expression `other - self`.
3306 a, b = _coerce_exprs(self, other) 3307 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3309 def __or__(self, other): 3310 """Create the Z3 expression bitwise-
or `self | other`.
3319 a, b = _coerce_exprs(self, other) 3320 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3322 def __ror__(self, other): 3323 """Create the Z3 expression bitwise-
or `other | self`.
3329 a, b = _coerce_exprs(self, other) 3330 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3332 def __and__(self, other): 3333 """Create the Z3 expression bitwise-
and `self & other`.
3342 a, b = _coerce_exprs(self, other) 3343 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3345 def __rand__(self, other): 3346 """Create the Z3 expression bitwise-
or `other & self`.
3352 a, b = _coerce_exprs(self, other) 3353 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3355 def __xor__(self, other): 3356 """Create the Z3 expression bitwise-xor `self ^ other`.
3365 a, b = _coerce_exprs(self, other) 3366 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3368 def __rxor__(self, other): 3369 """Create the Z3 expression bitwise-xor `other ^ self`.
3375 a, b = _coerce_exprs(self, other) 3376 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3388 """Return an expression representing `-self`.
3396 return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx) 3398 def __invert__(self): 3399 """Create the Z3 expression bitwise-
not `~self`.
3407 return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx) 3409 def __div__(self, other): 3410 """Create the Z3 expression (signed) division `self / other`.
3412 Use the function
UDiv()
for unsigned division.
3425 a, b = _coerce_exprs(self, other) 3426 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3428 def __truediv__(self, other): 3429 """Create the Z3 expression (signed) division `self / other`.
""" 3430 return self.__div__(other) 3432 def __rdiv__(self, other): 3433 """Create the Z3 expression (signed) division `other / self`.
3435 Use the function
UDiv()
for unsigned division.
3440 >>> (10 / x).
sexpr()
3441 '(bvsdiv #x0000000a x)' 3443 '(bvudiv #x0000000a x)' 3445 a, b = _coerce_exprs(self, other) 3446 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3448 def __rtruediv__(self, other): 3449 """Create the Z3 expression (signed) division `other / self`.
""" 3450 return self.__rdiv__(other) 3452 def __mod__(self, other): 3453 """Create the Z3 expression (signed) mod `self % other`.
3455 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3470 a, b = _coerce_exprs(self, other) 3471 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3473 def __rmod__(self, other): 3474 """Create the Z3 expression (signed) mod `other % self`.
3476 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3481 >>> (10 % x).
sexpr()
3482 '(bvsmod #x0000000a x)' 3484 '(bvurem #x0000000a x)' 3486 '(bvsrem #x0000000a x)' 3488 a, b = _coerce_exprs(self, other) 3489 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3491 def __le__(self, other): 3492 """Create the Z3 expression (signed) `other <= self`.
3494 Use the function
ULE()
for unsigned less than
or equal to.
3499 >>> (x <= y).
sexpr()
3504 a, b = _coerce_exprs(self, other) 3505 return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3507 def __lt__(self, other): 3508 """Create the Z3 expression (signed) `other < self`.
3510 Use the function
ULT()
for unsigned less than.
3520 a, b = _coerce_exprs(self, other) 3521 return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3523 def __gt__(self, other): 3524 """Create the Z3 expression (signed) `other > self`.
3526 Use the function
UGT()
for unsigned greater than.
3536 a, b = _coerce_exprs(self, other) 3537 return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3539 def __ge__(self, other): 3540 """Create the Z3 expression (signed) `other >= self`.
3542 Use the function
UGE()
for unsigned greater than
or equal to.
3547 >>> (x >= y).
sexpr()
3552 a, b = _coerce_exprs(self, other) 3553 return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3555 def __rshift__(self, other): 3556 """Create the Z3 expression (arithmetical) right shift `self >> other`
3558 Use the function
LShR()
for the right logical shift
3563 >>> (x >> y).
sexpr()
3582 a, b = _coerce_exprs(self, other) 3583 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3585 def __lshift__(self, other): 3586 """Create the Z3 expression left shift `self << other`
3591 >>> (x << y).
sexpr()
3596 a, b = _coerce_exprs(self, other) 3597 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3599 def __rrshift__(self, other): 3600 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3602 Use the function
LShR()
for the right logical shift
3607 >>> (10 >> x).
sexpr()
3608 '(bvashr #x0000000a x)' 3610 a, b = _coerce_exprs(self, other) 3611 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3613 def __rlshift__(self, other): 3614 """Create the Z3 expression left shift `other << self`.
3616 Use the function
LShR()
for the right logical shift
3621 >>> (10 << x).
sexpr()
3622 '(bvshl #x0000000a x)' 3624 a, b = _coerce_exprs(self, other) 3625 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3627 class BitVecNumRef(BitVecRef): 3628 """Bit-vector values.
""" 3631 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral.
3636 >>> print(
"0x%.8x" % v.as_long())
3639 return int(self.as_string()) 3641 def as_signed_long(self): 3642 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral. The most significant bit
is assumed to be the sign.
3656 val = self.as_long() 3657 if val >= 2**(sz - 1): 3659 if val < -2**(sz - 1): 3663 def as_string(self): 3664 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 3667 """Return `
True`
if `a`
is a Z3 bit-vector expression.
3677 return isinstance(a, BitVecRef) 3680 """Return `
True`
if `a`
is a Z3 bit-vector numeral value.
3691 return is_bv(a) and _is_numeral(a.ctx, a.as_ast()) 3693 def BV2Int(a, is_signed=False): 3694 """Return the Z3 expression
BV2Int(a).
3702 >>> x >
BV2Int(b, is_signed=
False)
3704 >>> x >
BV2Int(b, is_signed=
True)
3710 _z3_assert(is_bv(a), "Z3 bit-vector expression expected") 3712 ## investigate problem with bv2int 3713 return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx) 3715 def Int2BV(a, num_bits): 3716 """Return the z3 expression
Int2BV(a, num_bits).
3717 It
is a bit-vector of width num_bits
and represents the
3718 modulo of a by 2^num_bits
3721 return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx) 3723 def BitVecSort(sz, ctx=None): 3724 """Return a Z3 bit-vector sort of the given size. If `ctx=
None`, then the
global context
is used.
3730 >>> x =
Const(
'x', Byte)
3735 return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx) 3737 def BitVecVal(val, bv, ctx=None): 3738 """Return a bit-vector value with the given number of bits. If `ctx=
None`, then the
global context
is used.
3743 >>> print(
"0x%.8x" % v.as_long())
3748 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx) 3751 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx) 3753 def BitVec(name, bv, ctx=None): 3754 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3755 If `ctx=
None`, then the
global context
is used.
3765 >>> x2 =
BitVec(
'x', word)
3769 if isinstance(bv, BitVecSortRef): 3773 bv = BitVecSort(bv, ctx) 3774 return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx) 3776 def BitVecs(names, bv, ctx=None): 3777 """Return a tuple of bit-vector constants of size bv.
3779 >>> x, y, z =
BitVecs(
'x y z', 16)
3792 if isinstance(names, str): 3793 names = names.split(" ") 3794 return [BitVec(name, bv, ctx) for name in names] 3797 """Create a Z3 bit-vector concatenation expression.
3807 args = _get_args(args) 3810 _z3_assert(sz >= 2, "At least two arguments expected.") 3817 if is_seq(args[0]) or isinstance(args[0], str): 3818 args = [_coerce_seq(s, ctx) for s in args] 3820 _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") 3823 v[i] = args[i].as_ast() 3824 return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) 3828 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 3831 v[i] = args[i].as_ast() 3832 return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx) 3835 _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") 3837 for i in range(sz - 1): 3838 r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx) 3841 def Extract(high, low, a): 3842 """Create a Z3 bit-vector extraction expression,
or create a string extraction expression.
3852 if isinstance(high, str): 3853 high = StringVal(high) 3856 offset, length = _coerce_exprs(low, a, s.ctx) 3857 return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) 3859 _z3_assert(low <= high, "First argument must be greater than or equal to second argument") 3860 _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers") 3861 _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression") 3862 return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx) 3864 def _check_bv_args(a, b): 3866 _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression") 3869 """Create the Z3 expression (unsigned) `other <= self`.
3871 Use the operator <=
for signed less than
or equal to.
3876 >>> (x <= y).sexpr()
3878 >>>
ULE(x, y).sexpr()
3881 _check_bv_args(a, b) 3882 a, b = _coerce_exprs(a, b) 3883 return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3886 """Create the Z3 expression (unsigned) `other < self`.
3888 Use the operator <
for signed less than.
3895 >>>
ULT(x, y).sexpr()
3898 _check_bv_args(a, b) 3899 a, b = _coerce_exprs(a, b) 3900 return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3903 """Create the Z3 expression (unsigned) `other >= self`.
3905 Use the operator >=
for signed greater than
or equal to.
3910 >>> (x >= y).sexpr()
3912 >>>
UGE(x, y).sexpr()
3915 _check_bv_args(a, b) 3916 a, b = _coerce_exprs(a, b) 3917 return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3920 """Create the Z3 expression (unsigned) `other > self`.
3922 Use the operator >
for signed greater than.
3929 >>>
UGT(x, y).sexpr()
3932 _check_bv_args(a, b) 3933 a, b = _coerce_exprs(a, b) 3934 return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3937 """Create the Z3 expression (unsigned) division `self / other`.
3939 Use the operator /
for signed division.
3945 >>>
UDiv(x, y).sort()
3949 >>>
UDiv(x, y).sexpr()
3952 _check_bv_args(a, b) 3953 a, b = _coerce_exprs(a, b) 3954 return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3957 """Create the Z3 expression (unsigned) remainder `self % other`.
3959 Use the operator %
for signed modulus,
and SRem()
for signed remainder.
3965 >>>
URem(x, y).sort()
3969 >>>
URem(x, y).sexpr()
3972 _check_bv_args(a, b) 3973 a, b = _coerce_exprs(a, b) 3974 return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3977 """Create the Z3 expression signed remainder.
3979 Use the operator %
for signed modulus,
and URem()
for unsigned remainder.
3985 >>>
SRem(x, y).sort()
3989 >>>
SRem(x, y).sexpr()
3992 _check_bv_args(a, b) 3993 a, b = _coerce_exprs(a, b) 3994 return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3997 """Create the Z3 expression logical right shift.
3999 Use the operator >>
for the arithmetical right shift.
4004 >>> (x >> y).sexpr()
4006 >>>
LShR(x, y).sexpr()
4023 _check_bv_args(a, b) 4024 a, b = _coerce_exprs(a, b) 4025 return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4027 def RotateLeft(a, b): 4028 """Return an expression representing `a` rotated to the left `b` times.
4038 _check_bv_args(a, b) 4039 a, b = _coerce_exprs(a, b) 4040 return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4042 def RotateRight(a, b): 4043 """Return an expression representing `a` rotated to the right `b` times.
4053 _check_bv_args(a, b) 4054 a, b = _coerce_exprs(a, b) 4055 return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4058 """Return a bit-vector expression with `n` extra sign-bits.
4078 >>> print(
"%.x" % v.as_long())
4082 _z3_assert(_is_int(n), "First argument must be an integer") 4083 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 4084 return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 4087 """Return a bit-vector expression with `n` extra zero-bits.
4109 _z3_assert(_is_int(n), "First argument must be an integer") 4110 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 4111 return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 4113 def RepeatBitVec(n, a): 4114 """Return an expression representing `n` copies of `a`.
4123 >>> print(
"%.x" % v0.as_long())
4128 >>> print(
"%.x" % v.as_long())
4132 _z3_assert(_is_int(n), "First argument must be an integer") 4133 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 4134 return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx) 4137 """Return the reduction-
and expression of `a`.
""" 4139 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 4140 return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) 4143 """Return the reduction-
or expression of `a`.
""" 4145 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 4146 return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) 4148 def BVAddNoOverflow(a, b, signed): 4149 """A predicate the determines that bit-vector addition does
not overflow
""" 4150 _check_bv_args(a, b) 4151 a, b = _coerce_exprs(a, b) 4152 return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4154 def BVAddNoUnderflow(a, b): 4155 """A predicate the determines that signed bit-vector addition does
not underflow
""" 4156 _check_bv_args(a, b) 4157 a, b = _coerce_exprs(a, b) 4158 return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4160 def BVSubNoOverflow(a, b): 4161 """A predicate the determines that bit-vector subtraction does
not overflow
""" 4162 _check_bv_args(a, b) 4163 a, b = _coerce_exprs(a, b) 4164 return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4167 def BVSubNoUnderflow(a, b, signed): 4168 """A predicate the determines that bit-vector subtraction does
not underflow
""" 4169 _check_bv_args(a, b) 4170 a, b = _coerce_exprs(a, b) 4171 return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4173 def BVSDivNoOverflow(a, b): 4174 """A predicate the determines that bit-vector signed division does
not overflow
""" 4175 _check_bv_args(a, b) 4176 a, b = _coerce_exprs(a, b) 4177 return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4179 def BVSNegNoOverflow(a): 4180 """A predicate the determines that bit-vector unary negation does
not overflow
""" 4182 _z3_assert(is_bv(a), "Argument should be a bit-vector") 4183 return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx) 4185 def BVMulNoOverflow(a, b, signed): 4186 """A predicate the determines that bit-vector multiplication does
not overflow
""" 4187 _check_bv_args(a, b) 4188 a, b = _coerce_exprs(a, b) 4189 return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4192 def BVMulNoUnderflow(a, b): 4193 """A predicate the determines that bit-vector signed multiplication does
not underflow
""" 4194 _check_bv_args(a, b) 4195 a, b = _coerce_exprs(a, b) 4196 return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4200 ######################################### 4204 ######################################### 4206 class ArraySortRef(SortRef): 4210 """Return the domain of the array sort `self`.
4216 return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx) 4219 """Return the range of the array sort `self`.
4225 return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx) 4227 class ArrayRef(ExprRef): 4228 """Array expressions.
""" 4231 """Return the array sort of the array expression `self`.
4237 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4246 return self.sort().domain() 4255 return self.sort().range() 4257 def __getitem__(self, arg): 4258 """Return the Z3 expression `self[arg]`.
4267 arg = self.domain().cast(arg) 4268 return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx) 4271 return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx) 4275 """Return `
True`
if `a`
is a Z3 array expression.
4285 return isinstance(a, ArrayRef) 4287 def is_const_array(a): 4288 """Return `
True`
if `a`
is a Z3 constant array.
4297 return is_app_of(a, Z3_OP_CONST_ARRAY) 4300 """Return `
True`
if `a`
is a Z3 constant array.
4309 return is_app_of(a, Z3_OP_CONST_ARRAY) 4312 """Return `
True`
if `a`
is a Z3 map array expression.
4324 return is_app_of(a, Z3_OP_ARRAY_MAP) 4327 """Return `
True`
if `a`
is a Z3 default array expression.
4332 return is_app_of(a, Z3_OP_ARRAY_DEFAULT) 4334 def get_map_func(a): 4335 """Return the function declaration associated with a Z3 map array expression.
4348 _z3_assert(is_map(a), "Z3 array map expression expected.") 4349 return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx) 4351 def ArraySort(*sig): 4352 """Return the Z3 array sort with the given domain
and range sorts.
4365 sig = _get_args(sig) 4367 _z3_assert(len(sig) > 1, "At least two arguments expected") 4368 arity = len(sig) - 1 4373 _z3_assert(is_sort(s), "Z3 sort expected") 4374 _z3_assert(s.ctx == r.ctx, "Context mismatch") 4377 return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx) 4378 dom = (Sort * arity)() 4379 for i in range(arity): 4381 return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx) 4383 def Array(name, dom, rng): 4384 """Return an array constant named `name` with the given domain
and range sorts.
4392 s = ArraySort(dom, rng) 4394 return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx) 4396 def Update(a, i, v): 4397 """Return a Z3 store array expression.
4400 >>> i, v =
Ints(
'i v')
4404 >>>
prove(s[i] == v)
4411 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4412 i = a.domain().cast(i) 4413 v = a.range().cast(v) 4415 return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx) 4418 """ Return a default value
for array expression.
4424 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4429 """Return a Z3 store array expression.
4432 >>> i, v =
Ints(
'i v')
4433 >>> s =
Store(a, i, v)
4436 >>>
prove(s[i] == v)
4442 return Update(a, i, v) 4445 """Return a Z3 select array expression.
4455 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4460 """Return a Z3 map array expression.
4465 >>> b =
Map(f, a1, a2)
4468 >>>
prove(b[0] == f(a1[0], a2[0]))
4471 args = _get_args(args) 4473 _z3_assert(len(args) > 0, "At least one Z3 array expression expected") 4474 _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration") 4475 _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected") 4476 _z3_assert(len(args) == f.arity(), "Number of arguments mismatch") 4477 _args, sz = _to_ast_array(args) 4479 return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx) 4482 """Return a Z3 constant array expression.
4496 _z3_assert(is_sort(dom), "Z3 sort expected") 4499 v = _py2expr(v, ctx) 4500 return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx) 4503 """Return extensionality index
for one-dimensional arrays.
4510 _z3_assert(is_array(a) and is_array(b), "arguments must be arrays") 4511 return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 4513 def SetHasSize(a, k): 4515 k = _py2expr(k, ctx) 4516 return _to_expr_ref(Z3_mk_set_has_size(ctx.ref(), a.as_ast(), k.as_ast()), ctx) 4519 """Return `
True`
if `a`
is a Z3 array select application.
4528 return is_app_of(a, Z3_OP_SELECT) 4531 """Return `
True`
if `a`
is a Z3 array store application.
4539 return is_app_of(a, Z3_OP_STORE) 4541 ######################################### 4545 ######################################### 4549 """ Create a set sort over element sort s
""" 4550 return ArraySort(s, BoolSort()) 4553 """Create the empty set
4558 return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx) 4561 """Create the full set
4566 return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx) 4568 def SetUnion(*args): 4569 """ Take the union of sets
4575 args = _get_args(args) 4576 ctx = _ctx_from_ast_arg_list(args) 4577 _args, sz = _to_ast_array(args) 4578 return ArrayRef(Z3_mk_set_union(ctx.ref(), sz, _args), ctx) 4580 def SetIntersect(*args): 4581 """ Take the union of sets
4587 args = _get_args(args) 4588 ctx = _ctx_from_ast_arg_list(args) 4589 _args, sz = _to_ast_array(args) 4590 return ArrayRef(Z3_mk_set_intersect(ctx.ref(), sz, _args), ctx) 4593 """ Add element e to set s
4598 ctx = _ctx_from_ast_arg_list([s,e]) 4599 e = _py2expr(e, ctx) 4600 return ArrayRef(Z3_mk_set_add(ctx.ref(), s.as_ast(), e.as_ast()), ctx) 4603 """ Remove element e to set s
4608 ctx = _ctx_from_ast_arg_list([s,e]) 4609 e = _py2expr(e, ctx) 4610 return ArrayRef(Z3_mk_set_del(ctx.ref(), s.as_ast(), e.as_ast()), ctx) 4612 def SetComplement(s): 4613 """ The complement of set s
4619 return ArrayRef(Z3_mk_set_complement(ctx.ref(), s.as_ast()), ctx) 4621 def SetDifference(a, b): 4622 """ The set difference of a
and b
4628 ctx = _ctx_from_ast_arg_list([a, b]) 4629 return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 4632 """ Check
if e
is a member of set s
4637 ctx = _ctx_from_ast_arg_list([s,e]) 4638 e = _py2expr(e, ctx) 4639 return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx) 4642 """ Check
if a
is a subset of b
4648 ctx = _ctx_from_ast_arg_list([a, b]) 4649 return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 4652 ######################################### 4656 ######################################### 4658 def _valid_accessor(acc): 4659 """Return `
True`
if acc
is pair of the form (String, Datatype
or Sort).
""" 4660 return isinstance(acc, tuple) and len(acc) == 2 and isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1])) 4663 """Helper
class for declaring Z3 datatypes.
4666 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4667 >>> List.declare(
'nil')
4668 >>> List = List.create()
4672 >>> List.cons(10, List.nil)
4674 >>> List.cons(10, List.nil).sort()
4676 >>> cons = List.cons
4680 >>> n = cons(1, cons(0, nil))
4682 cons(1, cons(0, nil))
4688 def __init__(self, name, ctx=None): 4689 self.ctx = _get_ctx(ctx) 4691 self.constructors = [] 4693 def __deepcopy__(self, memo={}): 4694 r = Datatype(self.name, self.ctx) 4695 r.constructors = copy.deepcopy(self.constructors) 4698 def declare_core(self, name, rec_name, *args): 4700 _z3_assert(isinstance(name, str), "String expected") 4701 _z3_assert(isinstance(rec_name, str), "String expected") 4702 _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)") 4703 self.constructors.append((name, rec_name, args)) 4705 def declare(self, name, *args): 4706 """Declare constructor named `name` with the given accessors `args`.
4707 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.
4709 In the following example `List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))`
4710 declares the constructor named `cons` that builds a new List using an integer
and a List.
4711 It also declares the accessors `car`
and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
4712 and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method
create() to create
4713 the actual datatype
in Z3.
4716 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4717 >>> List.declare(
'nil')
4718 >>> List = List.create()
4721 _z3_assert(isinstance(name, str), "String expected") 4722 _z3_assert(name != "", "Constructor name cannot be empty") 4723 return self.declare_core(name, "is-" + name, *args) 4726 return "Datatype(%s, %s)" % (self.name, self.constructors) 4729 """Create a Z3 datatype based on the constructors declared using the method `
declare()`.
4731 The function `
CreateDatatypes()` must be used to define mutually recursive datatypes.
4734 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4735 >>> List.declare(
'nil')
4736 >>> List = List.create()
4739 >>> List.cons(10, List.nil)
4742 return CreateDatatypes([self])[0] 4744 class ScopedConstructor: 4745 """Auxiliary object used to create Z3 datatypes.
""" 4746 def __init__(self, c, ctx): 4750 if self.ctx.ref() is not None: 4751 Z3_del_constructor(self.ctx.ref(), self.c) 4753 class ScopedConstructorList: 4754 """Auxiliary object used to create Z3 datatypes.
""" 4755 def __init__(self, c, ctx): 4759 if self.ctx.ref() is not None: 4760 Z3_del_constructor_list(self.ctx.ref(), self.c) 4762 def CreateDatatypes(*ds): 4763 """Create mutually recursive Z3 datatypes using 1
or more Datatype helper objects.
4765 In the following example we define a Tree-List using two mutually recursive datatypes.
4767 >>> TreeList =
Datatype(
'TreeList')
4770 >>> Tree.declare(
'leaf', (
'val',
IntSort()))
4772 >>> Tree.declare(
'node', (
'children', TreeList))
4773 >>> TreeList.declare(
'nil')
4774 >>> TreeList.declare(
'cons', (
'car', Tree), (
'cdr', TreeList))
4776 >>> Tree.val(Tree.leaf(10))
4778 >>>
simplify(Tree.val(Tree.leaf(10)))
4780 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4782 node(cons(leaf(10), cons(leaf(20), nil)))
4783 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4786 >>>
simplify(TreeList.car(Tree.children(n2)) == n1)
4791 _z3_assert(len(ds) > 0, "At least one Datatype must be specified") 4792 _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes") 4793 _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch") 4794 _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected") 4797 names = (Symbol * num)() 4798 out = (Sort * num)() 4799 clists = (ConstructorList * num)() 4801 for i in range(num): 4803 names[i] = to_symbol(d.name, ctx) 4804 num_cs = len(d.constructors) 4805 cs = (Constructor * num_cs)() 4806 for j in range(num_cs): 4807 c = d.constructors[j] 4808 cname = to_symbol(c[0], ctx) 4809 rname = to_symbol(c[1], ctx) 4812 fnames = (Symbol * num_fs)() 4813 sorts = (Sort * num_fs)() 4814 refs = (ctypes.c_uint * num_fs)() 4815 for k in range(num_fs): 4818 fnames[k] = to_symbol(fname, ctx) 4819 if isinstance(ftype, Datatype): 4821 _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected") 4823 refs[k] = ds.index(ftype) 4826 _z3_assert(is_sort(ftype), "Z3 sort expected") 4827 sorts[k] = ftype.ast 4829 cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs) 4830 to_delete.append(ScopedConstructor(cs[j], ctx)) 4831 clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs) 4832 to_delete.append(ScopedConstructorList(clists[i], ctx)) 4833 Z3_mk_datatypes(ctx.ref(), num, names, out, clists) 4835 ## Create a field for every constructor, recognizer and accessor 4836 for i in range(num): 4837 dref = DatatypeSortRef(out[i], ctx) 4838 num_cs = dref.num_constructors() 4839 for j in range(num_cs): 4840 cref = dref.constructor(j) 4841 cref_name = cref.name() 4842 cref_arity = cref.arity() 4843 if cref.arity() == 0: 4845 setattr(dref, cref_name, cref) 4846 rref = dref.recognizer(j) 4847 setattr(dref, "is_" + cref_name, rref) 4848 for k in range(cref_arity): 4849 aref = dref.accessor(j, k) 4850 setattr(dref, aref.name(), aref) 4852 return tuple(result) 4854 class DatatypeSortRef(SortRef): 4855 """Datatype sorts.
""" 4856 def num_constructors(self): 4857 """Return the number of constructors
in the given Z3 datatype.
4860 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4861 >>> List.declare(
'nil')
4862 >>> List = List.create()
4864 >>> List.num_constructors()
4867 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast)) 4869 def constructor(self, idx): 4870 """Return a constructor of the datatype `self`.
4873 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4874 >>> List.declare(
'nil')
4875 >>> List = List.create()
4877 >>> List.num_constructors()
4879 >>> List.constructor(0)
4881 >>> List.constructor(1)
4885 _z3_assert(idx < self.num_constructors(), "Invalid constructor index") 4886 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx) 4888 def recognizer(self, idx): 4889 """In Z3, each constructor has an associated recognizer predicate.
4891 If the constructor
is named `name`, then the recognizer `is_name`.
4894 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4895 >>> List.declare(
'nil')
4896 >>> List = List.create()
4898 >>> List.num_constructors()
4900 >>> List.recognizer(0)
4902 >>> List.recognizer(1)
4904 >>>
simplify(List.is_nil(List.cons(10, List.nil)))
4906 >>>
simplify(List.is_cons(List.cons(10, List.nil)))
4908 >>> l =
Const(
'l', List)
4913 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index") 4914 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx) 4916 def accessor(self, i, j): 4917 """In Z3, each constructor has 0
or more accessor. The number of accessors
is equal to the arity of the constructor.
4920 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4921 >>> List.declare(
'nil')
4922 >>> List = List.create()
4923 >>> List.num_constructors()
4925 >>> List.constructor(0)
4927 >>> num_accs = List.constructor(0).arity()
4930 >>> List.accessor(0, 0)
4932 >>> List.accessor(0, 1)
4934 >>> List.constructor(1)
4936 >>> num_accs = List.constructor(1).arity()
4941 _z3_assert(i < self.num_constructors(), "Invalid constructor index") 4942 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index") 4943 return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx) 4945 class DatatypeRef(ExprRef): 4946 """Datatype expressions.
""" 4948 """Return the datatype sort of the datatype expression `self`.
""" 4949 return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4951 def TupleSort(name, sorts, ctx = None): 4952 """Create a named tuple sort base on a set of underlying sorts
4956 tuple = Datatype(name, ctx) 4957 projects = [ ('project%d' % i, sorts[i]) for i in range(len(sorts)) ] 4958 tuple.declare(name, *projects) 4959 tuple = tuple.create() 4960 return tuple, tuple.constructor(0), [tuple.accessor(0, i) for i in range(len(sorts))] 4962 def DisjointSum(name, sorts, ctx=None): 4963 """Create a named tagged union sort base on a set of underlying sorts
4967 sum = Datatype(name, ctx) 4968 for i in range(len(sorts)): 4969 sum.declare("inject%d" % i, ("project%d" % i, sorts[i])) 4971 return sum, [(sum.constructor(i), sum.accessor(i, 0)) for i in range(len(sorts))] 4974 def EnumSort(name, values, ctx=None): 4975 """Return a new enumeration sort named `name` containing the given values.
4977 The result
is a pair (sort, list of constants).
4979 >>> Color, (red, green, blue) =
EnumSort(
'Color', [
'red',
'green',
'blue'])
4982 _z3_assert(isinstance(name, str), "Name must be a string") 4983 _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings") 4984 _z3_assert(len(values) > 0, "At least one value expected") 4987 _val_names = (Symbol * num)() 4988 for i in range(num): 4989 _val_names[i] = to_symbol(values[i]) 4990 _values = (FuncDecl * num)() 4991 _testers = (FuncDecl * num)() 4992 name = to_symbol(name) 4993 S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx) 4995 for i in range(num): 4996 V.append(FuncDeclRef(_values[i], ctx)) 4997 V = [a() for a in V] 5000 ######################################### 5004 ######################################### 5007 """Set of parameters used to configure Solvers, Tactics
and Simplifiers
in Z3.
5009 Consider using the function `args2params` to create instances of this object.
5011 def __init__(self, ctx=None, params=None): 5012 self.ctx = _get_ctx(ctx) 5014 self.params = Z3_mk_params(self.ctx.ref()) 5016 self.params = params 5017 Z3_params_inc_ref(self.ctx.ref(), self.params) 5019 def __deepcopy__(self, memo={}): 5020 return ParamsRef(self.ctx, self.params) 5023 if self.ctx.ref() is not None: 5024 Z3_params_dec_ref(self.ctx.ref(), self.params) 5026 def set(self, name, val): 5027 """Set parameter name with value val.
""" 5029 _z3_assert(isinstance(name, str), "parameter name must be a string") 5030 name_sym = to_symbol(name, self.ctx) 5031 if isinstance(val, bool): 5032 Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val) 5034 Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val) 5035 elif isinstance(val, float): 5036 Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val) 5037 elif isinstance(val, str): 5038 Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx)) 5041 _z3_assert(False, "invalid parameter value") 5044 return Z3_params_to_string(self.ctx.ref(), self.params) 5046 def validate(self, ds): 5047 _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected") 5048 Z3_params_validate(self.ctx.ref(), self.params, ds.descr) 5050 def args2params(arguments, keywords, ctx=None): 5051 """Convert python arguments into a Z3_params object.
5052 A
':' is added to the keywords,
and '_' is replaced with
'-' 5054 >>>
args2params([
'model',
True,
'relevancy', 2], {
'elim_and' :
True})
5055 (params model true relevancy 2 elim_and true)
5058 _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") 5072 class ParamDescrsRef: 5073 """Set of parameter descriptions
for Solvers, Tactics
and Simplifiers
in Z3.
5075 def __init__(self, descr, ctx=None): 5076 _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected") 5077 self.ctx = _get_ctx(ctx) 5079 Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr) 5081 def __deepcopy__(self, memo={}): 5082 return ParamsDescrsRef(self.descr, self.ctx) 5085 if self.ctx.ref() is not None: 5086 Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr) 5089 """Return the size of
in the parameter description `self`.
5091 return int(Z3_param_descrs_size(self.ctx.ref(), self.descr)) 5094 """Return the size of
in the parameter description `self`.
5098 def get_name(self, i): 5099 """Return the i-th parameter name
in the parameter description `self`.
5101 return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i)) 5103 def get_kind(self, n): 5104 """Return the kind of the parameter named `n`.
5106 return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 5108 def get_documentation(self, n): 5109 """Return the documentation string of the parameter named `n`.
5111 return Z3_param_descrs_get_documentation(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 5113 def __getitem__(self, arg): 5115 return self.get_name(arg) 5117 return self.get_kind(arg) 5120 return Z3_param_descrs_to_string(self.ctx.ref(), self.descr) 5122 ######################################### 5126 ######################################### 5128 class Goal(Z3PPObject): 5129 """Goal
is a collection of constraints we want to find a solution
or show to be unsatisfiable (infeasible).
5131 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
5132 A goal has a solution
if one of its subgoals has a solution.
5133 A goal
is unsatisfiable
if all subgoals are unsatisfiable.
5136 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None): 5138 _z3_assert(goal is None or ctx is not None, "If goal is different from None, then ctx must be also different from None") 5139 self.ctx = _get_ctx(ctx) 5141 if self.goal is None: 5142 self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs) 5143 Z3_goal_inc_ref(self.ctx.ref(), self.goal) 5145 def __deepcopy__(self, memo={}): 5146 return Goal(False, False, False, self.ctx, self.goal) 5149 if self.goal is not None and self.ctx.ref() is not None: 5150 Z3_goal_dec_ref(self.ctx.ref(), self.goal) 5153 """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
5155 >>> x, y =
Ints(
'x y')
5157 >>> g.add(x == 0, y >= x + 1)
5160 >>> r =
Then(
'simplify',
'solve-eqs')(g)
5167 return int(Z3_goal_depth(self.ctx.ref(), self.goal)) 5169 def inconsistent(self): 5170 """Return `
True`
if `self` contains the `
False` constraints.
5172 >>> x, y =
Ints(
'x y')
5174 >>> g.inconsistent()
5176 >>> g.add(x == 0, x == 1)
5179 >>> g.inconsistent()
5181 >>> g2 =
Tactic(
'propagate-values')(g)[0]
5182 >>> g2.inconsistent()
5185 return Z3_goal_inconsistent(self.ctx.ref(), self.goal) 5188 """Return the precision (under-approximation, over-approximation,
or precise) of the goal `self`.
5191 >>> g.prec() == Z3_GOAL_PRECISE
5193 >>> x, y =
Ints(
'x y')
5194 >>> g.add(x == y + 1)
5195 >>> g.prec() == Z3_GOAL_PRECISE
5197 >>> t =
With(
Tactic(
'add-bounds'), add_bound_lower=0, add_bound_upper=10)
5200 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
5201 >>> g2.prec() == Z3_GOAL_PRECISE
5203 >>> g2.prec() == Z3_GOAL_UNDER
5206 return Z3_goal_precision(self.ctx.ref(), self.goal) 5208 def precision(self): 5209 """Alias
for `
prec()`.
5212 >>> g.precision() == Z3_GOAL_PRECISE
5218 """Return the number of constraints
in the goal `self`.
5223 >>> x, y =
Ints(
'x y')
5224 >>> g.add(x == 0, y > x)
5228 return int(Z3_goal_size(self.ctx.ref(), self.goal)) 5231 """Return the number of constraints
in the goal `self`.
5236 >>> x, y =
Ints(
'x y')
5237 >>> g.add(x == 0, y > x)
5244 """Return a constraint
in the goal `self`.
5247 >>> x, y =
Ints(
'x y')
5248 >>> g.add(x == 0, y > x)
5254 return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx) 5256 def __getitem__(self, arg): 5257 """Return a constraint
in the goal `self`.
5260 >>> x, y =
Ints(
'x y')
5261 >>> g.add(x == 0, y > x)
5267 if arg >= len(self): 5269 return self.get(arg) 5271 def assert_exprs(self, *args): 5272 """Assert constraints into the goal.
5276 >>> g.assert_exprs(x > 0, x < 2)
5280 args = _get_args(args) 5281 s = BoolSort(self.ctx) 5284 Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast()) 5286 def append(self, *args): 5291 >>> g.append(x > 0, x < 2)
5295 self.assert_exprs(*args) 5297 def insert(self, *args): 5302 >>> g.insert(x > 0, x < 2)
5306 self.assert_exprs(*args) 5308 def add(self, *args): 5313 >>> g.add(x > 0, x < 2)
5317 self.assert_exprs(*args) 5319 def convert_model(self, model): 5320 """Retrieve model
from a satisfiable goal
5321 >>> a, b =
Ints(
'a b')
5323 >>> g.add(
Or(a == 0, a == 1),
Or(b == 0, b == 1), a > b)
5327 [
Or(b == 0, b == 1),
Not(0 <= b)]
5329 [
Or(b == 0, b == 1),
Not(1 <= b)]
5345 _z3_assert(isinstance(model, ModelRef), "Z3 Model expected") 5346 return ModelRef(Z3_goal_convert_model(self.ctx.ref(), self.goal, model.model), self.ctx) 5349 return obj_to_string(self) 5352 """Return a textual representation of the s-expression representing the goal.
""" 5353 return Z3_goal_to_string(self.ctx.ref(), self.goal) 5356 """Return a textual representation of the goal
in DIMACS format.
""" 5357 return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal) 5359 def translate(self, target): 5360 """Copy goal `self` to context `target`.
5368 >>> g2 = g.translate(c2)
5379 _z3_assert(isinstance(target, Context), "target must be a context") 5380 return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target) 5383 return self.translate(self.ctx) 5385 def __deepcopy__(self, memo={}): 5386 return self.translate(self.ctx) 5388 def simplify(self, *arguments, **keywords): 5389 """Return a new simplified goal.
5391 This method
is essentially invoking the simplify tactic.
5395 >>> g.add(x + 1 >= 2)
5398 >>> g2 = g.simplify()
5405 t = Tactic('simplify') 5406 return t.apply(self, *arguments, **keywords)[0] 5409 """Return goal `self`
as a single Z3 expression.
5424 return BoolVal(True, self.ctx) 5428 return And([ self.get(i) for i in range(len(self)) ], self.ctx) 5430 ######################################### 5434 ######################################### 5435 class AstVector(Z3PPObject): 5436 """A collection (vector) of ASTs.
""" 5438 def __init__(self, v=None, ctx=None): 5441 self.ctx = _get_ctx(ctx) 5442 self.vector = Z3_mk_ast_vector(self.ctx.ref()) 5445 assert ctx is not None 5447 Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector) 5449 def __deepcopy__(self, memo={}): 5450 return AstVector(self.vector, self.ctx) 5453 if self.vector is not None and self.ctx.ref() is not None: 5454 Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector) 5457 """Return the size of the vector `self`.
5462 >>> A.push(
Int(
'x'))
5463 >>> A.push(
Int(
'x'))
5467 return int(Z3_ast_vector_size(self.ctx.ref(), self.vector)) 5469 def __getitem__(self, i): 5470 """Return the AST at position `i`.
5473 >>> A.push(
Int(
'x') + 1)
5474 >>> A.push(
Int(
'y'))
5481 if isinstance(i, int): 5485 if i >= self.__len__(): 5487 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx) 5489 elif isinstance(i, slice): 5490 return [_to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, ii), self.ctx) for ii in range(*i.indices(self.__len__()))] 5493 def __setitem__(self, i, v): 5494 """Update AST at position `i`.
5497 >>> A.push(
Int(
'x') + 1)
5498 >>> A.push(
Int(
'y'))
5505 if i >= self.__len__(): 5507 Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast()) 5510 """Add `v`
in the end of the vector.
5515 >>> A.push(
Int(
'x'))
5519 Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast()) 5521 def resize(self, sz): 5522 """Resize the vector to `sz` elements.
5528 >>>
for i
in range(10): A[i] =
Int(
'x')
5532 Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz) 5534 def __contains__(self, item): 5535 """Return `
True`
if the vector contains `item`.
5557 def translate(self, other_ctx): 5558 """Copy vector `self` to context `other_ctx`.
5564 >>> B = A.translate(c2)
5568 return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx) 5571 return self.translate(self.ctx) 5573 def __deepcopy__(self, memo={}): 5574 return self.translate(self.ctx) 5577 return obj_to_string(self) 5580 """Return a textual representation of the s-expression representing the vector.
""" 5581 return Z3_ast_vector_to_string(self.ctx.ref(), self.vector) 5583 ######################################### 5587 ######################################### 5589 """A mapping
from ASTs to ASTs.
""" 5591 def __init__(self, m=None, ctx=None): 5594 self.ctx = _get_ctx(ctx) 5595 self.map = Z3_mk_ast_map(self.ctx.ref()) 5598 assert ctx is not None 5600 Z3_ast_map_inc_ref(self.ctx.ref(), self.map) 5602 def __deepcopy__(self, memo={}): 5603 return AstMap(self.map, self.ctx) 5606 if self.map is not None and self.ctx.ref() is not None: 5607 Z3_ast_map_dec_ref(self.ctx.ref(), self.map) 5610 """Return the size of the map.
5620 return int(Z3_ast_map_size(self.ctx.ref(), self.map)) 5622 def __contains__(self, key): 5623 """Return `
True`
if the map contains key `key`.
5633 return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast()) 5635 def __getitem__(self, key): 5636 """Retrieve the value associated with key `key`.
5644 return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx) 5646 def __setitem__(self, k, v): 5647 """Add/Update key `k` with value `v`.
5660 Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast()) 5663 return Z3_ast_map_to_string(self.ctx.ref(), self.map) 5666 """Remove the entry associated with key `k`.
5677 Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast()) 5680 """Remove all entries
from the map.
5692 Z3_ast_map_reset(self.ctx.ref(), self.map) 5695 """Return an AstVector containing all keys
in the map.
5704 return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx) 5706 ######################################### 5710 ######################################### 5713 """Store the value of the interpretation of a function
in a particular point.
""" 5715 def __init__(self, entry, ctx): 5718 Z3_func_entry_inc_ref(self.ctx.ref(), self.entry) 5720 def __deepcopy__(self, memo={}): 5721 return FuncEntry(self.entry, self.ctx) 5724 if self.ctx.ref() is not None: 5725 Z3_func_entry_dec_ref(self.ctx.ref(), self.entry) 5728 """Return the number of arguments
in the given entry.
5732 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5737 >>> f_i.num_entries()
5739 >>> e = f_i.entry(0)
5743 return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry)) 5745 def arg_value(self, idx): 5746 """Return the value of argument `idx`.
5750 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5755 >>> f_i.num_entries()
5757 >>> e = f_i.entry(0)
5768 ...
except IndexError:
5769 ... print(
"index error")
5772 if idx >= self.num_args(): 5774 return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx) 5777 """Return the value of the function at point `self`.
5781 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5786 >>> f_i.num_entries()
5788 >>> e = f_i.entry(0)
5796 return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx) 5799 """Return entry `self`
as a Python list.
5802 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5807 >>> f_i.num_entries()
5809 >>> e = f_i.entry(0)
5813 args = [ self.arg_value(i) for i in range(self.num_args())] 5814 args.append(self.value()) 5818 return repr(self.as_list()) 5820 class FuncInterp(Z3PPObject): 5821 """Stores the interpretation of a function
in a Z3 model.
""" 5823 def __init__(self, f, ctx): 5826 if self.f is not None: 5827 Z3_func_interp_inc_ref(self.ctx.ref(), self.f) 5829 def __deepcopy__(self, memo={}): 5830 return FuncInterp(self.f, self.ctx) 5833 if self.f is not None and self.ctx.ref() is not None: 5834 Z3_func_interp_dec_ref(self.ctx.ref(), self.f) 5836 def else_value(self): 5838 Return the `
else` value
for a function interpretation.
5839 Return
None if Z3 did
not specify the `
else` value
for 5844 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5853 r = Z3_func_interp_get_else(self.ctx.ref(), self.f) 5855 return _to_expr_ref(r, self.ctx) 5859 def num_entries(self): 5860 """Return the number of entries/points
in the function interpretation `self`.
5864 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5873 return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f)) 5876 """Return the number of arguments
for each entry
in the function interpretation `self`.
5880 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5887 return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f)) 5889 def entry(self, idx): 5890 """Return an entry at position `idx < self.
num_entries()`
in the function interpretation `self`.
5894 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5905 if idx >= self.num_entries(): 5907 return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx) 5909 def translate(self, other_ctx): 5910 """Copy model
'self' to context
'other_ctx'.
5912 return ModelRef(Z3_model_translate(self.ctx.ref(), self.model, other_ctx.ref()), other_ctx) 5915 return self.translate(self.ctx) 5917 def __deepcopy__(self, memo={}): 5918 return self.translate(self.ctx) 5921 """Return the function interpretation
as a Python list.
5924 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5933 r = [ self.entry(i).as_list() for i in range(self.num_entries())] 5934 r.append(self.else_value()) 5938 return obj_to_string(self) 5940 class ModelRef(Z3PPObject): 5941 """Model/Solution of a satisfiability problem (aka system of constraints).
""" 5943 def __init__(self, m, ctx): 5944 assert ctx is not None 5947 Z3_model_inc_ref(self.ctx.ref(), self.model) 5950 if self.ctx.ref() is not None: 5951 Z3_model_dec_ref(self.ctx.ref(), self.model) 5954 return obj_to_string(self) 5957 """Return a textual representation of the s-expression representing the model.
""" 5958 return Z3_model_to_string(self.ctx.ref(), self.model) 5960 def eval(self, t, model_completion=False): 5961 """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`.
5965 >>> s.add(x > 0, x < 2)
5978 >>> m.eval(y, model_completion=
True)
5985 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r): 5986 return _to_expr_ref(r[0], self.ctx) 5987 raise Z3Exception("failed to evaluate expression in the model") 5989 def evaluate(self, t, model_completion=False): 5990 """Alias
for `eval`.
5994 >>> s.add(x > 0, x < 2)
5998 >>> m.evaluate(x + 1)
6000 >>> m.evaluate(x == 1)
6003 >>> m.evaluate(y + x)
6007 >>> m.evaluate(y, model_completion=
True)
6010 >>> m.evaluate(y + x)
6013 return self.eval(t, model_completion) 6016 """Return the number of constant
and function declarations
in the model `self`.
6021 >>> s.add(x > 0, f(x) != x)
6028 return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model)) 6030 def get_interp(self, decl): 6031 """Return the interpretation
for a given declaration
or constant.
6036 >>> s.add(x > 0, x < 2, f(x) == 0)
6046 _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected") 6050 if decl.arity() == 0: 6051 _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast) 6052 if _r.value is None: 6054 r = _to_expr_ref(_r, self.ctx) 6056 return self.get_interp(get_as_array_func(r)) 6060 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) 6064 def num_sorts(self): 6065 """Return the number of uninterpreted sorts that contain an interpretation
in the model `self`.
6068 >>> a, b =
Consts(
'a b', A)
6077 return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model)) 6079 def get_sort(self, idx): 6080 """Return the uninterpreted sort at position `idx` < self.
num_sorts().
6084 >>> a1, a2 =
Consts(
'a1 a2', A)
6085 >>> b1, b2 =
Consts(
'b1 b2', B)
6087 >>> s.add(a1 != a2, b1 != b2)
6098 if idx >= self.num_sorts(): 6100 return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx) 6103 """Return all uninterpreted sorts that have an interpretation
in the model `self`.
6107 >>> a1, a2 =
Consts(
'a1 a2', A)
6108 >>> b1, b2 =
Consts(
'b1 b2', B)
6110 >>> s.add(a1 != a2, b1 != b2)
6117 return [ self.get_sort(i) for i in range(self.num_sorts()) ] 6119 def get_universe(self, s): 6120 """Return the interpretation
for the uninterpreted sort `s`
in the model `self`.
6123 >>> a, b =
Consts(
'a b', A)
6129 >>> m.get_universe(A)
6133 _z3_assert(isinstance(s, SortRef), "Z3 sort expected") 6135 return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx) 6139 def __getitem__(self, idx): 6140 """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.
6142 The elements can be retrieved using position
or the actual declaration.
6147 >>> s.add(x > 0, x < 2, f(x) == 0)
6161 >>>
for d
in m: print(
"%s -> %s" % (d, m[d]))
6166 if idx >= len(self): 6168 num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model) 6169 if (idx < num_consts): 6170 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx) 6172 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx) 6173 if isinstance(idx, FuncDeclRef): 6174 return self.get_interp(idx) 6176 return self.get_interp(idx.decl()) 6177 if isinstance(idx, SortRef): 6178 return self.get_universe(idx) 6180 _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected") 6184 """Return a list with all symbols that have an interpretation
in the model `self`.
6188 >>> s.add(x > 0, x < 2, f(x) == 0)
6196 for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)): 6197 r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx)) 6198 for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)): 6199 r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx)) 6202 def translate(self, target): 6203 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
6206 _z3_assert(isinstance(target, Context), "argument must be a Z3 context") 6207 model = Z3_model_translate(self.ctx.ref(), self.model, target.ref()) 6208 return Model(model, target) 6211 return self.translate(self.ctx) 6213 def __deepcopy__(self, memo={}): 6214 return self.translate(self.ctx) 6216 def Model(ctx = None): 6218 return ModelRef(Z3_mk_model(ctx.ref()), ctx) 6221 """Return true
if n
is a Z3 expression of the form (_
as-array f).
""" 6222 return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast()) 6224 def get_as_array_func(n): 6225 """Return the function declaration f associated with a Z3 expression of the form (_
as-array f).
""" 6227 _z3_assert(is_as_array(n), "as-array Z3 expression expected.") 6228 return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx) 6230 ######################################### 6234 ######################################### 6236 """Statistics
for `Solver.check()`.
""" 6238 def __init__(self, stats, ctx): 6241 Z3_stats_inc_ref(self.ctx.ref(), self.stats) 6243 def __deepcopy__(self, memo={}): 6244 return Statistics(self.stats, self.ctx) 6247 if self.ctx.ref() is not None: 6248 Z3_stats_dec_ref(self.ctx.ref(), self.stats) 6254 out.write(u('<table border="1" cellpadding="2" cellspacing="0">')) 6257 out.write(u('<tr style="background-color:#CFCFCF">')) 6260 out.write(u('<tr>')) 6262 out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v))) 6263 out.write(u('</table>')) 6264 return out.getvalue() 6266 return Z3_stats_to_string(self.ctx.ref(), self.stats) 6269 """Return the number of statistical counters.
6272 >>> s =
Then(
'simplify',
'nlsat').solver()
6276 >>> st = s.statistics()
6280 return int(Z3_stats_size(self.ctx.ref(), self.stats)) 6282 def __getitem__(self, idx): 6283 """Return the value of statistical counter at position `idx`. The result
is a pair (key, value).
6286 >>> s =
Then(
'simplify',
'nlsat').solver()
6290 >>> st = s.statistics()
6294 (
'nlsat propagations', 2)
6298 if idx >= len(self): 6300 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 6301 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 6303 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 6304 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val) 6307 """Return the list of statistical counters.
6310 >>> s =
Then(
'simplify',
'nlsat').solver()
6314 >>> st = s.statistics()
6316 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))] 6318 def get_key_value(self, key): 6319 """Return the value of a particular statistical counter.
6322 >>> s =
Then(
'simplify',
'nlsat').solver()
6326 >>> st = s.statistics()
6327 >>> st.get_key_value(
'nlsat propagations')
6330 for idx in range(len(self)): 6331 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx): 6332 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 6333 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 6335 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 6336 raise Z3Exception("unknown key") 6338 def __getattr__(self, name): 6339 """Access the value of statistical using attributes.
6341 Remark: to access a counter containing blank spaces (e.g.,
'nlsat propagations'),
6342 we should use
'_' (e.g.,
'nlsat_propagations').
6345 >>> s =
Then(
'simplify',
'nlsat').solver()
6349 >>> st = s.statistics()
6350 >>> st.nlsat_propagations
6355 key = name.replace('_', ' ') 6357 return self.get_key_value(key) 6359 raise AttributeError 6361 ######################################### 6365 ######################################### 6366 class CheckSatResult: 6367 """Represents the result of a satisfiability check: sat, unsat, unknown.
6373 >>> isinstance(r, CheckSatResult)
6377 def __init__(self, r): 6380 def __deepcopy__(self, memo={}): 6381 return CheckSatResult(self.r) 6383 def __eq__(self, other): 6384 return isinstance(other, CheckSatResult) and self.r == other.r 6386 def __ne__(self, other): 6387 return not self.__eq__(other) 6391 if self.r == Z3_L_TRUE: 6393 elif self.r == Z3_L_FALSE: 6394 return "<b>unsat</b>" 6396 return "<b>unknown</b>" 6398 if self.r == Z3_L_TRUE: 6400 elif self.r == Z3_L_FALSE: 6405 sat = CheckSatResult(Z3_L_TRUE) 6406 unsat = CheckSatResult(Z3_L_FALSE) 6407 unknown = CheckSatResult(Z3_L_UNDEF) 6409 class Solver(Z3PPObject): 6410 """Solver API provides methods
for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.
""" 6412 def __init__(self, solver=None, ctx=None): 6413 assert solver is None or ctx is not None 6414 self.ctx = _get_ctx(ctx) 6415 self.backtrack_level = 4000000000 6418 self.solver = Z3_mk_solver(self.ctx.ref()) 6420 self.solver = solver 6421 Z3_solver_inc_ref(self.ctx.ref(), self.solver) 6424 if self.solver is not None and self.ctx.ref() is not None: 6425 Z3_solver_dec_ref(self.ctx.ref(), self.solver) 6427 def set(self, *args, **keys): 6428 """Set a configuration option. The method `
help()`
return a string containing all available options.
6432 >>> s.set(mbqi=
True)
6433 >>> s.set(
'MBQI',
True)
6434 >>> s.set(
':mbqi',
True)
6436 p = args2params(args, keys, self.ctx) 6437 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params) 6440 """Create a backtracking point.
6459 Z3_solver_push(self.ctx.ref(), self.solver) 6461 def pop(self, num=1): 6462 """Backtrack \c num backtracking points.
6481 Z3_solver_pop(self.ctx.ref(), self.solver, num) 6483 def num_scopes(self): 6484 """Return the current number of backtracking points.
6499 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver) 6502 """Remove all asserted constraints
and backtracking points created using `
push()`.
6513 Z3_solver_reset(self.ctx.ref(), self.solver) 6515 def assert_exprs(self, *args): 6516 """Assert constraints into the solver.
6520 >>> s.assert_exprs(x > 0, x < 2)
6524 args = _get_args(args) 6525 s = BoolSort(self.ctx) 6527 if isinstance(arg, Goal) or isinstance(arg, AstVector): 6529 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast()) 6532 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast()) 6534 def add(self, *args): 6535 """Assert constraints into the solver.
6539 >>> s.add(x > 0, x < 2)
6543 self.assert_exprs(*args) 6545 def __iadd__(self, fml): 6549 def append(self, *args): 6550 """Assert constraints into the solver.
6554 >>> s.append(x > 0, x < 2)
6558 self.assert_exprs(*args) 6560 def insert(self, *args): 6561 """Assert constraints into the solver.
6565 >>> s.insert(x > 0, x < 2)
6569 self.assert_exprs(*args) 6571 def assert_and_track(self, a, p): 6572 """Assert constraint `a`
and track it
in the unsat core using the Boolean constant `p`.
6574 If `p`
is a string, it will be automatically converted into a Boolean constant.
6579 >>> s.set(unsat_core=
True)
6580 >>> s.assert_and_track(x > 0,
'p1')
6581 >>> s.assert_and_track(x != 1,
'p2')
6582 >>> s.assert_and_track(x < 0, p3)
6583 >>> print(s.check())
6585 >>> c = s.unsat_core()
6595 if isinstance(p, str): 6596 p = Bool(p, self.ctx) 6597 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected") 6598 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected") 6599 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast()) 6601 def check(self, *assumptions): 6602 """Check whether the assertions
in the given solver plus the optional assumptions are consistent
or not.
6608 >>> s.add(x > 0, x < 2)
6611 >>> s.model().eval(x)
6617 >>> s.add(2**x == 4)
6621 assumptions = _get_args(assumptions) 6622 num = len(assumptions) 6623 _assumptions = (Ast * num)() 6624 for i in range(num): 6625 _assumptions[i] = assumptions[i].as_ast() 6626 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions) 6627 return CheckSatResult(r) 6630 """Return a model
for the last `
check()`.
6632 This function raises an exception
if 6633 a model
is not available (e.g., last `
check()` returned unsat).
6637 >>> s.add(a + 2 == 0)
6644 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx) 6646 raise Z3Exception("model is not available") 6648 def unsat_core(self): 6649 """Return a subset (
as an AST vector) of the assumptions provided to the last
check().
6651 These are the assumptions Z3 used
in the unsatisfiability proof.
6652 Assumptions are available
in Z3. They are used to extract unsatisfiable cores.
6653 They may be also used to
"retract" assumptions. Note that, assumptions are
not really
6654 "soft constraints", but they can be used to implement them.
6656 >>> p1, p2, p3 =
Bools(
'p1 p2 p3')
6657 >>> x, y =
Ints(
'x y')
6662 >>> s.add(
Implies(p3, y > -3))
6663 >>> s.check(p1, p2, p3)
6665 >>> core = s.unsat_core()
6678 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx) 6680 def consequences(self, assumptions, variables): 6681 """Determine fixed values
for the variables based on the solver state
and assumptions.
6683 >>> a, b, c, d =
Bools(
'a b c d')
6685 >>> s.consequences([a],[b,c,d])
6687 >>> s.consequences([
Not(c),d],[a,b,c,d])
6690 if isinstance(assumptions, list): 6691 _asms = AstVector(None, self.ctx) 6692 for a in assumptions: 6695 if isinstance(variables, list): 6696 _vars = AstVector(None, self.ctx) 6700 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected") 6701 _z3_assert(isinstance(variables, AstVector), "ast vector expected") 6702 consequences = AstVector(None, self.ctx) 6703 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector) 6704 sz = len(consequences) 6705 consequences = [ consequences[i] for i in range(sz) ] 6706 return CheckSatResult(r), consequences 6708 def from_file(self, filename): 6709 """Parse assertions
from a file
""" 6710 Z3_solver_from_file(self.ctx.ref(), self.solver, filename) 6712 def from_string(self, s): 6713 """Parse assertions
from a string
""" 6714 Z3_solver_from_string(self.ctx.ref(), self.solver, s) 6716 def cube(self, vars = None): 6718 The method takes an optional set of variables that restrict which
6719 variables may be used
as a starting point
for cubing.
6720 If vars
is not None, then the first case split
is based on a variable
in 6723 self.cube_vs = AstVector(None, self.ctx) 6724 if vars is not None: 6726 self.cube_vs.push(v) 6728 lvl = self.backtrack_level 6729 self.backtrack_level = 4000000000 6730 r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx) 6731 if (len(r) == 1 and is_false(r[0])): 6737 def cube_vars(self): 6738 """Access the set of variables that were touched by the most recently generated cube.
6739 This set of variables can be used
as a starting point
for additional cubes.
6740 The idea
is that variables that appear
in clauses that are reduced by the most recent
6741 cube are likely more useful to cube on.
""" 6745 """Return a proof
for the last `
check()`. Proof construction must be enabled.
""" 6746 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx) 6748 def assertions(self): 6749 """Return an AST vector containing all added constraints.
6760 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx) 6763 """Return an AST vector containing all currently inferred units.
6765 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx) 6767 def non_units(self): 6768 """Return an AST vector containing all atomic formulas
in solver state that are
not units.
6770 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx) 6772 def trail_levels(self): 6773 """Return trail
and decision levels of the solver state after a
check() call.
6775 trail = self.trail() 6776 levels = (ctypes.c_uint * len(trail))() 6777 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels) 6778 return trail, levels 6781 """Return trail of the solver state after a
check() call.
6783 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx) 6785 def statistics(self): 6786 """Return statistics
for the last `
check()`.
6793 >>> st = s.statistics()
6794 >>> st.get_key_value(
'final checks')
6801 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx) 6803 def reason_unknown(self): 6804 """Return a string describing why the last `
check()` returned `unknown`.
6808 >>> s.add(2**x == 4)
6811 >>> s.reason_unknown()
6812 '(incomplete (theory arithmetic))' 6814 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver) 6817 """Display a string describing all available options.
""" 6818 print(Z3_solver_get_help(self.ctx.ref(), self.solver)) 6820 def param_descrs(self): 6821 """Return the parameter description set.
""" 6822 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx) 6825 """Return a formatted string with all added constraints.
""" 6826 return obj_to_string(self) 6828 def translate(self, target): 6829 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
6834 >>> s2 = s1.translate(c2)
6837 _z3_assert(isinstance(target, Context), "argument must be a Z3 context") 6838 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) 6839 return Solver(solver, target) 6842 return self.translate(self.ctx) 6844 def __deepcopy__(self, memo={}): 6845 return self.translate(self.ctx) 6848 """Return a formatted string (
in Lisp-like format) with all added constraints. We say the string
is in s-expression format.
6856 return Z3_solver_to_string(self.ctx.ref(), self.solver) 6859 """Return a textual representation of the solver
in DIMACS format.
""" 6860 return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver) 6863 """return SMTLIB2 formatted benchmark
for solver
's assertions""" 6870 for i
in range(sz1):
6871 v[i] = es[i].as_ast()
6873 e = es[sz1].as_ast()
6879 """Create a solver customized for the given logic. 6881 The parameter `logic` is a string. It should be contains 6882 the name of a SMT-LIB logic. 6883 See http://www.smtlib.org/ for the name of all available logics. 6885 >>> s = SolverFor("QF_LIA") 6899 """Return a simple general purpose solver with limited amount of preprocessing. 6901 >>> s = SimpleSolver() 6917 """Fixedpoint API provides methods for solving with recursive predicates""" 6920 assert fixedpoint
is None or ctx
is not None 6923 if fixedpoint
is None:
6934 if self.
fixedpoint is not None and self.
ctx.ref()
is not None:
6938 """Set a configuration option. The method `help()` return a string containing all available options. 6944 """Display a string describing all available options.""" 6948 """Return the parameter description set.""" 6952 """Assert constraints as background axioms for the fixedpoint solver.""" 6953 args = _get_args(args)
6956 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
6966 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6974 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6978 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6982 """Assert rules defining recursive predicates to the fixedpoint solver. 6985 >>> s = Fixedpoint() 6986 >>> s.register_relation(a.decl()) 6987 >>> s.register_relation(b.decl()) 7000 body = _get_args(body)
7004 def rule(self, head, body = None, name = None):
7005 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 7009 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 7013 """Query the fixedpoint engine whether formula is derivable. 7014 You can also pass an tuple or list of recursive predicates. 7016 query = _get_args(query)
7018 if sz >= 1
and isinstance(query[0], FuncDeclRef):
7019 _decls = (FuncDecl * sz)()
7029 query =
And(query, self.
ctx)
7030 query = self.
abstract(query,
False)
7035 """Query the fixedpoint engine whether formula is derivable starting at the given query level. 7037 query = _get_args(query)
7039 if sz >= 1
and isinstance(query[0], FuncDecl):
7040 _z3_assert (
False,
"unsupported")
7046 query = self.
abstract(query,
False)
7047 r = Z3_fixedpoint_query_from_lvl (self.
ctx.ref(), self.
fixedpoint, query.as_ast(), lvl)
7055 body = _get_args(body)
7060 """Retrieve answer from last query call.""" 7062 return _to_expr_ref(r, self.
ctx)
7065 """Retrieve a ground cex from last query call.""" 7066 r = Z3_fixedpoint_get_ground_sat_answer(self.
ctx.ref(), self.
fixedpoint)
7067 return _to_expr_ref(r, self.
ctx)
7070 """retrieve rules along the counterexample trace""" 7074 """retrieve rule names along the counterexample trace""" 7077 names = _symbol2py (self.
ctx, Z3_fixedpoint_get_rule_names_along_trace(self.
ctx.ref(), self.
fixedpoint))
7079 return names.split (
';')
7082 """Retrieve number of levels used for predicate in PDR engine""" 7086 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)""" 7088 return _to_expr_ref(r, self.
ctx)
7091 """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)""" 7095 """Register relation as recursive""" 7096 relations = _get_args(relations)
7101 """Control how relation is represented""" 7102 representations = _get_args(representations)
7103 representations = [
to_symbol(s)
for s
in representations]
7104 sz = len(representations)
7105 args = (Symbol * sz)()
7107 args[i] = representations[i]
7111 """Parse rules and queries from a string""" 7115 """Parse rules and queries from a file""" 7119 """retrieve rules that have been added to fixedpoint context""" 7123 """retrieve assertions that have been added to fixedpoint context""" 7127 """Return a formatted string with all added rules and constraints.""" 7131 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 7136 """Return a formatted string (in Lisp-like format) with all added constraints. 7137 We say the string is in s-expression format. 7138 Include also queries. 7140 args, len = _to_ast_array(queries)
7144 """Return statistics for the last `query()`. 7149 """Return a string describing why the last `query()` returned `unknown`. 7154 """Add variable or several variables. 7155 The added variable or variables will be bound in the rules 7158 vars = _get_args(vars)
7178 """Finite domain sort.""" 7181 """Return the size of the finite domain sort""" 7182 r = (ctypes.c_ulonglong * 1)()
7186 raise Z3Exception(
"Failed to retrieve finite domain sort size")
7189 """Create a named finite domain sort of a given size sz""" 7190 if not isinstance(name, Symbol):
7196 """Return True if `s` is a Z3 finite-domain sort. 7198 >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) 7200 >>> is_finite_domain_sort(IntSort()) 7203 return isinstance(s, FiniteDomainSortRef)
7207 """Finite-domain expressions.""" 7210 """Return the sort of the finite-domain expression `self`.""" 7214 """Return a Z3 floating point expression as a Python string.""" 7218 """Return `True` if `a` is a Z3 finite-domain expression. 7220 >>> s = FiniteDomainSort('S', 100) 7221 >>> b = Const('b', s) 7222 >>> is_finite_domain(b) 7224 >>> is_finite_domain(Int('x')) 7227 return isinstance(a, FiniteDomainRef)
7231 """Integer values.""" 7234 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. 7236 >>> s = FiniteDomainSort('S', 100) 7237 >>> v = FiniteDomainVal(3, s) 7246 """Return a Z3 finite-domain numeral as a Python string. 7248 >>> s = FiniteDomainSort('S', 100) 7249 >>> v = FiniteDomainVal(42, s) 7257 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. 7259 >>> s = FiniteDomainSort('S', 256) 7260 >>> FiniteDomainVal(255, s) 7262 >>> FiniteDomainVal('100', s) 7271 """Return `True` if `a` is a Z3 finite-domain value. 7273 >>> s = FiniteDomainSort('S', 100) 7274 >>> b = Const('b', s) 7275 >>> is_finite_domain_value(b) 7277 >>> b = FiniteDomainVal(10, s) 7280 >>> is_finite_domain_value(b) 7325 """Optimize API provides methods for solving using objective functions and weighted soft constraints""" 7336 if self.
optimize is not None and self.
ctx.ref()
is not None:
7340 """Set a configuration option. The method `help()` return a string containing all available options. 7346 """Display a string describing all available options.""" 7350 """Return the parameter description set.""" 7354 """Assert constraints as background axioms for the optimize solver.""" 7355 args = _get_args(args)
7358 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
7366 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr.""" 7374 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`. 7376 If `p` is a string, it will be automatically converted into a Boolean constant. 7381 >>> s.assert_and_track(x > 0, 'p1') 7382 >>> s.assert_and_track(x != 1, 'p2') 7383 >>> s.assert_and_track(x < 0, p3) 7384 >>> print(s.check()) 7386 >>> c = s.unsat_core() 7396 if isinstance(p, str):
7398 _z3_assert(isinstance(a, BoolRef),
"Boolean expression expected")
7399 _z3_assert(isinstance(p, BoolRef)
and is_const(p),
"Boolean expression expected")
7403 """Add soft constraint with optional weight and optional identifier. 7404 If no weight is supplied, then the penalty for violating the soft constraint 7406 Soft constraints are grouped by identifiers. Soft constraints that are 7407 added without identifiers are grouped by default. 7410 weight =
"%d" % weight
7411 elif isinstance(weight, float):
7412 weight =
"%f" % weight
7413 if not isinstance(weight, str):
7414 raise Z3Exception(
"weight should be a string or an integer")
7422 """Add objective function to maximize.""" 7426 """Add objective function to minimize.""" 7430 """create a backtracking point for added rules, facts and assertions""" 7434 """restore to previously created backtracking point""" 7438 """Check satisfiability while optimizing objective functions.""" 7439 assumptions = _get_args(assumptions)
7440 num = len(assumptions)
7441 _assumptions = (Ast * num)()
7442 for i
in range(num):
7443 _assumptions[i] = assumptions[i].as_ast()
7447 """Return a string that describes why the last `check()` returned `unknown`.""" 7451 """Return a model for the last check().""" 7455 raise Z3Exception(
"model is not available")
7461 if not isinstance(obj, OptimizeObjective):
7462 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7466 if not isinstance(obj, OptimizeObjective):
7467 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7471 if not isinstance(obj, OptimizeObjective):
7472 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7473 return obj.lower_values()
7476 if not isinstance(obj, OptimizeObjective):
7477 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7478 return obj.upper_values()
7481 """Parse assertions and objectives from a file""" 7485 """Parse assertions and objectives from a string""" 7489 """Return an AST vector containing all added constraints.""" 7493 """returns set of objective functions""" 7497 """Return a formatted string with all added rules and constraints.""" 7501 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 7506 """Return statistics for the last check`. 7519 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters.""" 7530 if self.
ctx.ref()
is not None:
7534 """Return the number of subgoals in `self`. 7536 >>> a, b = Ints('a b') 7538 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7539 >>> t = Tactic('split-clause') 7543 >>> t = Then(Tactic('split-clause'), Tactic('split-clause')) 7546 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values')) 7553 """Return one of the subgoals stored in ApplyResult object `self`. 7555 >>> a, b = Ints('a b') 7557 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7558 >>> t = Tactic('split-clause') 7561 [a == 0, Or(b == 0, b == 1), a > b] 7563 [a == 1, Or(b == 0, b == 1), a > b] 7565 if idx >= len(self):
7570 return obj_to_string(self)
7573 """Return a textual representation of the s-expression representing the set of subgoals in `self`.""" 7578 """Return a Z3 expression consisting of all subgoals. 7583 >>> g.add(Or(x == 2, x == 3)) 7584 >>> r = Tactic('simplify')(g) 7586 [[Not(x <= 1), Or(x == 2, x == 3)]] 7588 And(Not(x <= 1), Or(x == 2, x == 3)) 7589 >>> r = Tactic('split-clause')(g) 7591 [[x > 1, x == 2], [x > 1, x == 3]] 7593 Or(And(x > 1, x == 2), And(x > 1, x == 3)) 7609 """Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver(). 7611 Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond(). 7616 if isinstance(tactic, TacticObj):
7620 _z3_assert(isinstance(tactic, str),
"tactic name expected")
7624 raise Z3Exception(
"unknown tactic '%s'" % tactic)
7631 if self.
tactic is not None and self.
ctx.ref()
is not None:
7635 """Create a solver using the tactic `self`. 7637 The solver supports the methods `push()` and `pop()`, but it 7638 will always solve each `check()` from scratch. 7640 >>> t = Then('simplify', 'nlsat') 7643 >>> s.add(x**2 == 2, x > 0) 7651 def apply(self, goal, *arguments, **keywords):
7652 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7654 >>> x, y = Ints('x y') 7655 >>> t = Tactic('solve-eqs') 7656 >>> t.apply(And(x == 0, y >= x + 1)) 7660 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expressions expected")
7661 goal = _to_goal(goal)
7662 if len(arguments) > 0
or len(keywords) > 0:
7669 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7671 >>> x, y = Ints('x y') 7672 >>> t = Tactic('solve-eqs') 7673 >>> t(And(x == 0, y >= x + 1)) 7676 return self.
apply(goal, *arguments, **keywords)
7679 """Display a string containing a description of the available options for the `self` tactic.""" 7683 """Return the parameter description set.""" 7687 if isinstance(a, BoolRef):
7688 goal =
Goal(ctx = a.ctx)
7694 def _to_tactic(t, ctx=None):
7695 if isinstance(t, Tactic):
7700 def _and_then(t1, t2, ctx=None):
7701 t1 = _to_tactic(t1, ctx)
7702 t2 = _to_tactic(t2, ctx)
7704 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7707 def _or_else(t1, t2, ctx=None):
7708 t1 = _to_tactic(t1, ctx)
7709 t2 = _to_tactic(t2, ctx)
7711 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7715 """Return a tactic that applies the tactics in `*ts` in sequence. 7717 >>> x, y = Ints('x y') 7718 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) 7719 >>> t(And(x == 0, y > x + 1)) 7721 >>> t(And(x == 0, y > x + 1)).as_expr() 7725 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7726 ctx = ks.get(
'ctx',
None)
7729 for i
in range(num - 1):
7730 r = _and_then(r, ts[i+1], ctx)
7734 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). 7736 >>> x, y = Ints('x y') 7737 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) 7738 >>> t(And(x == 0, y > x + 1)) 7740 >>> t(And(x == 0, y > x + 1)).as_expr() 7746 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). 7749 >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) 7750 >>> # Tactic split-clause fails if there is no clause in the given goal. 7753 >>> t(Or(x == 0, x == 1)) 7754 [[x == 0], [x == 1]] 7757 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7758 ctx = ks.get(
'ctx',
None)
7761 for i
in range(num - 1):
7762 r = _or_else(r, ts[i+1], ctx)
7766 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). 7769 >>> t = ParOr(Tactic('simplify'), Tactic('fail')) 7774 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7775 ctx = _get_ctx(ks.get(
'ctx',
None))
7776 ts = [ _to_tactic(t, ctx)
for t
in ts ]
7778 _args = (TacticObj * sz)()
7780 _args[i] = ts[i].tactic
7784 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. 7786 >>> x, y = Ints('x y') 7787 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) 7788 >>> t(And(Or(x == 1, x == 2), y == x + 1)) 7789 [[x == 1, y == 2], [x == 2, y == 3]] 7791 t1 = _to_tactic(t1, ctx)
7792 t2 = _to_tactic(t2, ctx)
7794 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7798 """Alias for ParThen(t1, t2, ctx).""" 7802 """Return a tactic that applies tactic `t` using the given configuration options. 7804 >>> x, y = Ints('x y') 7805 >>> t = With(Tactic('simplify'), som=True) 7806 >>> t((x + 1)*(y + 2) == 0) 7807 [[2*x + y + x*y == -2]] 7809 ctx = keys.pop(
'ctx',
None)
7810 t = _to_tactic(t, ctx)
7815 """Return a tactic that applies tactic `t` using the given configuration options. 7817 >>> x, y = Ints('x y') 7819 >>> p.set("som", True) 7820 >>> t = WithParams(Tactic('simplify'), p) 7821 >>> t((x + 1)*(y + 2) == 0) 7822 [[2*x + y + x*y == -2]] 7824 t = _to_tactic(t,
None)
7828 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. 7830 >>> x, y = Ints('x y') 7831 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) 7832 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) 7834 >>> for subgoal in r: print(subgoal) 7835 [x == 0, y == 0, x > y] 7836 [x == 0, y == 1, x > y] 7837 [x == 1, y == 0, x > y] 7838 [x == 1, y == 1, x > y] 7839 >>> t = Then(t, Tactic('propagate-values')) 7843 t = _to_tactic(t, ctx)
7847 """Return a tactic that applies `t` to a given goal for `ms` milliseconds. 7849 If `t` does not terminate in `ms` milliseconds, then it fails. 7851 t = _to_tactic(t, ctx)
7855 """Return a list of all available tactics in Z3. 7858 >>> l.count('simplify') == 1 7865 """Return a short description for the tactic named `name`. 7867 >>> d = tactic_description('simplify') 7873 """Display a (tabular) description of all available tactics in Z3.""" 7876 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7879 print(
'<tr style="background-color:#CFCFCF">')
7884 print(
'<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(
tactic_description(t), 40)))
7891 """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.""" 7895 if isinstance(probe, ProbeObj):
7897 elif isinstance(probe, float):
7899 elif _is_int(probe):
7901 elif isinstance(probe, bool):
7908 _z3_assert(isinstance(probe, str),
"probe name expected")
7912 raise Z3Exception(
"unknown probe '%s'" % probe)
7919 if self.
probe is not None and self.
ctx.ref()
is not None:
7923 """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`. 7925 >>> p = Probe('size') < 10 7936 """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`. 7938 >>> p = Probe('size') > 10 7949 """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`. 7951 >>> p = Probe('size') <= 2 7962 """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`. 7964 >>> p = Probe('size') >= 2 7975 """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`. 7977 >>> p = Probe('size') == 2 7988 """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`. 7990 >>> p = Probe('size') != 2 8002 """Evaluate the probe `self` in the given goal. 8004 >>> p = Probe('size') 8014 >>> p = Probe('num-consts') 8017 >>> p = Probe('is-propositional') 8020 >>> p = Probe('is-qflia') 8025 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expression expected")
8026 goal = _to_goal(goal)
8030 """Return `True` if `p` is a Z3 probe. 8032 >>> is_probe(Int('x')) 8034 >>> is_probe(Probe('memory')) 8037 return isinstance(p, Probe)
8039 def _to_probe(p, ctx=None):
8043 return Probe(p, ctx)
8046 """Return a list of all available probes in Z3. 8049 >>> l.count('memory') == 1 8056 """Return a short description for the probe named `name`. 8058 >>> d = probe_description('memory') 8064 """Display a (tabular) description of all available probes in Z3.""" 8067 print(
'<table border="1" cellpadding="2" cellspacing="0">')
8070 print(
'<tr style="background-color:#CFCFCF">')
8075 print(
'<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(
probe_description(p), 40)))
8081 def _probe_nary(f, args, ctx):
8083 _z3_assert(len(args) > 0,
"At least one argument expected")
8085 r = _to_probe(args[0], ctx)
8086 for i
in range(num - 1):
8087 r =
Probe(f(ctx.ref(), r.probe, _to_probe(args[i+1], ctx).probe), ctx)
8090 def _probe_and(args, ctx):
8091 return _probe_nary(Z3_probe_and, args, ctx)
8093 def _probe_or(args, ctx):
8094 return _probe_nary(Z3_probe_or, args, ctx)
8097 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 8099 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. 8101 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) 8102 >>> x, y = Ints('x y') 8108 >>> g.add(x == y + 1) 8110 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 8112 p = _to_probe(p, ctx)
8116 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 8118 >>> t = When(Probe('size') > 2, Tactic('simplify')) 8119 >>> x, y = Ints('x y') 8125 >>> g.add(x == y + 1) 8127 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 8129 p = _to_probe(p, ctx)
8130 t = _to_tactic(t, ctx)
8134 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. 8136 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt')) 8138 p = _to_probe(p, ctx)
8139 t1 = _to_tactic(t1, ctx)
8140 t2 = _to_tactic(t2, ctx)
8150 """Simplify the expression `a` using the given options. 8152 This function has many options. Use `help_simplify` to obtain the complete list. 8156 >>> simplify(x + 1 + y + x + 1) 8158 >>> simplify((x + 1)*(y + 1), som=True) 8160 >>> simplify(Distinct(x, y, 1), blast_distinct=True) 8161 And(Not(x == y), Not(x == 1), Not(y == 1)) 8162 >>> simplify(And(x == 0, y == 1), elim_and=True) 8163 Not(Or(Not(x == 0), Not(y == 1))) 8166 _z3_assert(
is_expr(a),
"Z3 expression expected")
8167 if len(arguments) > 0
or len(keywords) > 0:
8169 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
8171 return _to_expr_ref(
Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
8174 """Return a string describing all options available for Z3 `simplify` procedure.""" 8178 """Return the set of parameter descriptions for Z3 `simplify` procedure.""" 8182 """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. 8186 >>> substitute(x + 1, (x, y + 1)) 8188 >>> f = Function('f', IntSort(), IntSort()) 8189 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 8192 if isinstance(m, tuple):
8194 if isinstance(m1, list)
and all(isinstance(p, tuple)
for p
in m1):
8197 _z3_assert(
is_expr(t),
"Z3 expression expected")
8198 _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.")
8200 _from = (Ast * num)()
8202 for i
in range(num):
8203 _from[i] = m[i][0].as_ast()
8204 _to[i] = m[i][1].as_ast()
8205 return _to_expr_ref(
Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
8208 """Substitute the free variables in t with the expression in m. 8210 >>> v0 = Var(0, IntSort()) 8211 >>> v1 = Var(1, IntSort()) 8213 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 8214 >>> # replace v0 with x+1 and v1 with x 8215 >>> substitute_vars(f(v0, v1), x + 1, x) 8219 _z3_assert(
is_expr(t),
"Z3 expression expected")
8220 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
8223 for i
in range(num):
8224 _to[i] = m[i].as_ast()
8228 """Create the sum of the Z3 expressions. 8230 >>> a, b, c = Ints('a b c') 8235 >>> A = IntVector('a', 5) 8237 a__0 + a__1 + a__2 + a__3 + a__4 8239 args = _get_args(args)
8242 ctx = _ctx_from_ast_arg_list(args)
8244 return _reduce(
lambda a, b: a + b, args, 0)
8245 args = _coerce_expr_list(args, ctx)
8247 return _reduce(
lambda a, b: a + b, args, 0)
8249 _args, sz = _to_ast_array(args)
8254 """Create the product of the Z3 expressions. 8256 >>> a, b, c = Ints('a b c') 8257 >>> Product(a, b, c) 8259 >>> Product([a, b, c]) 8261 >>> A = IntVector('a', 5) 8263 a__0*a__1*a__2*a__3*a__4 8265 args = _get_args(args)
8268 ctx = _ctx_from_ast_arg_list(args)
8270 return _reduce(
lambda a, b: a * b, args, 1)
8271 args = _coerce_expr_list(args, ctx)
8273 return _reduce(
lambda a, b: a * b, args, 1)
8275 _args, sz = _to_ast_array(args)
8279 """Create an at-most Pseudo-Boolean k constraint. 8281 >>> a, b, c = Bools('a b c') 8282 >>> f = AtMost(a, b, c, 2) 8284 args = _get_args(args)
8286 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8287 ctx = _ctx_from_ast_arg_list(args)
8289 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8290 args1 = _coerce_expr_list(args[:-1], ctx)
8292 _args, sz = _to_ast_array(args1)
8296 """Create an at-most Pseudo-Boolean k constraint. 8298 >>> a, b, c = Bools('a b c') 8299 >>> f = AtLeast(a, b, c, 2) 8301 args = _get_args(args)
8303 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8304 ctx = _ctx_from_ast_arg_list(args)
8306 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8307 args1 = _coerce_expr_list(args[:-1], ctx)
8309 _args, sz = _to_ast_array(args1)
8313 def _pb_args_coeffs(args, default_ctx = None):
8314 args = _get_args_ast_list(args)
8316 return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
8317 args, coeffs = zip(*args)
8319 _z3_assert(len(args) > 0,
"Non empty list of arguments expected")
8320 ctx = _ctx_from_ast_arg_list(args)
8322 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8323 args = _coerce_expr_list(args, ctx)
8324 _args, sz = _to_ast_array(args)
8325 _coeffs = (ctypes.c_int * len(coeffs))()
8326 for i
in range(len(coeffs)):
8327 _z3_check_cint_overflow(coeffs[i],
"coefficient")
8328 _coeffs[i] = coeffs[i]
8329 return ctx, sz, _args, _coeffs
8332 """Create a Pseudo-Boolean inequality k constraint. 8334 >>> a, b, c = Bools('a b c') 8335 >>> f = PbLe(((a,1),(b,3),(c,2)), 3) 8337 _z3_check_cint_overflow(k,
"k")
8338 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8342 """Create a Pseudo-Boolean inequality k constraint. 8344 >>> a, b, c = Bools('a b c') 8345 >>> f = PbGe(((a,1),(b,3),(c,2)), 3) 8347 _z3_check_cint_overflow(k,
"k")
8348 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8352 """Create a Pseudo-Boolean inequality k constraint. 8354 >>> a, b, c = Bools('a b c') 8355 >>> f = PbEq(((a,1),(b,3),(c,2)), 3) 8357 _z3_check_cint_overflow(k,
"k")
8358 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8363 """Solve the constraints `*args`. 8365 This is a simple function for creating demonstrations. It creates a solver, 8366 configure it using the options in `keywords`, adds the constraints 8367 in `args`, and invokes check. 8370 >>> solve(a > 0, a < 2) 8376 if keywords.get(
'show',
False):
8380 print(
"no solution")
8382 print(
"failed to solve")
8391 """Solve the constraints `*args` using solver `s`. 8393 This is a simple function for creating demonstrations. It is similar to `solve`, 8394 but it uses the given solver `s`. 8395 It configures solver `s` using the options in `keywords`, adds the constraints 8396 in `args`, and invokes check. 8399 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8402 if keywords.get(
'show',
False):
8407 print(
"no solution")
8409 print(
"failed to solve")
8415 if keywords.get(
'show',
False):
8420 """Try to prove the given claim. 8422 This is a simple function for creating demonstrations. It tries to prove 8423 `claim` by showing the negation is unsatisfiable. 8425 >>> p, q = Bools('p q') 8426 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) 8430 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8434 if keywords.get(
'show',
False):
8440 print(
"failed to prove")
8443 print(
"counterexample")
8446 def _solve_html(*args, **keywords):
8447 """Version of function `solve` used in RiSE4Fun.""" 8451 if keywords.get(
'show',
False):
8452 print(
"<b>Problem:</b>")
8456 print(
"<b>no solution</b>")
8458 print(
"<b>failed to solve</b>")
8464 if keywords.get(
'show',
False):
8465 print(
"<b>Solution:</b>")
8468 def _solve_using_html(s, *args, **keywords):
8469 """Version of function `solve_using` used in RiSE4Fun.""" 8471 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8474 if keywords.get(
'show',
False):
8475 print(
"<b>Problem:</b>")
8479 print(
"<b>no solution</b>")
8481 print(
"<b>failed to solve</b>")
8487 if keywords.get(
'show',
False):
8488 print(
"<b>Solution:</b>")
8491 def _prove_html(claim, **keywords):
8492 """Version of function `prove` used in RiSE4Fun.""" 8494 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8498 if keywords.get(
'show',
False):
8502 print(
"<b>proved</b>")
8504 print(
"<b>failed to prove</b>")
8507 print(
"<b>counterexample</b>")
8510 def _dict2sarray(sorts, ctx):
8512 _names = (Symbol * sz)()
8513 _sorts = (Sort * sz) ()
8518 _z3_assert(isinstance(k, str),
"String expected")
8519 _z3_assert(
is_sort(v),
"Z3 sort expected")
8523 return sz, _names, _sorts
8525 def _dict2darray(decls, ctx):
8527 _names = (Symbol * sz)()
8528 _decls = (FuncDecl * sz) ()
8533 _z3_assert(isinstance(k, str),
"String expected")
8537 _decls[i] = v.decl().ast
8541 return sz, _names, _decls
8545 """Parse a string in SMT 2.0 format using the given sorts and decls. 8547 The arguments sorts and decls are Python dictionaries used to initialize 8548 the symbol table used for the SMT 2.0 parser. 8550 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') 8552 >>> x, y = Ints('x y') 8553 >>> f = Function('f', IntSort(), IntSort()) 8554 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) 8556 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) 8560 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 8561 dsz, dnames, ddecls = _dict2darray(decls, ctx) 8562 return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 8564 def parse_smt2_file(f, sorts={}, decls={}, ctx=None): 8565 """Parse a file
in SMT 2.0 format using the given sorts
and decls.
8570 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 8571 dsz, dnames, ddecls = _dict2darray(decls, ctx) 8572 return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 8575 ######################################### 8577 # Floating-Point Arithmetic 8579 ######################################### 8582 # Global default rounding mode 8583 _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO 8584 _dflt_fpsort_ebits = 11 8585 _dflt_fpsort_sbits = 53 8587 def get_default_rounding_mode(ctx=None): 8588 """Retrieves the
global default rounding mode.
""" 8589 global _dflt_rounding_mode 8590 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO: 8592 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE: 8594 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE: 8596 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: 8598 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: 8601 def set_default_rounding_mode(rm, ctx=None): 8602 global _dflt_rounding_mode 8603 if is_fprm_value(rm): 8604 _dflt_rounding_mode = rm.decl().kind() 8606 _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO or 8607 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE or 8608 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE or 8609 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN or 8610 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, 8611 "illegal rounding mode") 8612 _dflt_rounding_mode = rm 8614 def get_default_fp_sort(ctx=None): 8615 return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx) 8617 def set_default_fp_sort(ebits, sbits, ctx=None): 8618 global _dflt_fpsort_ebits 8619 global _dflt_fpsort_sbits 8620 _dflt_fpsort_ebits = ebits 8621 _dflt_fpsort_sbits = sbits 8623 def _dflt_rm(ctx=None): 8624 return get_default_rounding_mode(ctx) 8626 def _dflt_fps(ctx=None): 8627 return get_default_fp_sort(ctx) 8629 def _coerce_fp_expr_list(alist, ctx): 8630 first_fp_sort = None 8633 if first_fp_sort is None: 8634 first_fp_sort = a.sort() 8635 elif first_fp_sort == a.sort(): 8636 pass # OK, same as before 8638 # we saw at least 2 different float sorts; something will 8639 # throw a sort mismatch later, for now assume None. 8640 first_fp_sort = None 8644 for i in range(len(alist)): 8646 if (isinstance(a, str) and a.contains('2**(') and a.endswith(')')) or _is_int(a) or isinstance(a, float) or isinstance(a, bool): 8647 r.append(FPVal(a, None, first_fp_sort, ctx)) 8650 return _coerce_expr_list(r, ctx) 8655 class FPSortRef(SortRef): 8656 """Floating-point sort.
""" 8659 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint sort `self`.
8664 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast)) 8667 """Retrieves the number of bits reserved
for the significand
in the FloatingPoint sort `self`.
8672 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast)) 8674 def cast(self, val): 8675 """Try to cast `val`
as a floating-point expression.
8679 >>> b.cast(1.0).
sexpr()
8680 '(fp #b0 #x7f #b00000000000000000000000)' 8684 _z3_assert(self.ctx == val.ctx, "Context mismatch") 8687 return FPVal(val, None, self, self.ctx) 8690 def Float16(ctx=None): 8691 """Floating-point 16-bit (half) sort.
""" 8693 return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx) 8695 def FloatHalf(ctx=None): 8696 """Floating-point 16-bit (half) sort.
""" 8698 return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx) 8700 def Float32(ctx=None): 8701 """Floating-point 32-bit (single) sort.
""" 8703 return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx) 8705 def FloatSingle(ctx=None): 8706 """Floating-point 32-bit (single) sort.
""" 8708 return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx) 8710 def Float64(ctx=None): 8711 """Floating-point 64-bit (double) sort.
""" 8713 return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx) 8715 def FloatDouble(ctx=None): 8716 """Floating-point 64-bit (double) sort.
""" 8718 return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx) 8720 def Float128(ctx=None): 8721 """Floating-point 128-bit (quadruple) sort.
""" 8723 return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx) 8725 def FloatQuadruple(ctx=None): 8726 """Floating-point 128-bit (quadruple) sort.
""" 8728 return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx) 8730 class FPRMSortRef(SortRef): 8731 """"Floating-point rounding mode sort.""" 8735 """Return True if `s` is a Z3 floating-point sort.
8742 return isinstance(s, FPSortRef) 8744 def is_fprm_sort(s): 8745 """Return
True if `s`
is a Z3 floating-point rounding mode sort.
8752 return isinstance(s, FPRMSortRef) 8756 class FPRef(ExprRef): 8757 """Floating-point expressions.
""" 8760 """Return the sort of the floating-point expression `self`.
8765 >>> x.sort() ==
FPSort(8, 24)
8768 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 8771 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8776 return self.sort().ebits(); 8779 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8784 return self.sort().sbits(); 8786 def as_string(self): 8787 """Return a Z3 floating point expression
as a Python string.
""" 8788 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8790 def __le__(self, other): 8791 return fpLEQ(self, other, self.ctx) 8793 def __lt__(self, other): 8794 return fpLT(self, other, self.ctx) 8796 def __ge__(self, other): 8797 return fpGEQ(self, other, self.ctx) 8799 def __gt__(self, other): 8800 return fpGT(self, other, self.ctx) 8802 def __add__(self, other): 8803 """Create the Z3 expression `self + other`.
8812 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8813 return fpAdd(_dflt_rm(), a, b, self.ctx) 8815 def __radd__(self, other): 8816 """Create the Z3 expression `other + self`.
8822 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8823 return fpAdd(_dflt_rm(), a, b, self.ctx) 8825 def __sub__(self, other): 8826 """Create the Z3 expression `self - other`.
8835 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8836 return fpSub(_dflt_rm(), a, b, self.ctx) 8838 def __rsub__(self, other): 8839 """Create the Z3 expression `other - self`.
8845 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8846 return fpSub(_dflt_rm(), a, b, self.ctx) 8848 def __mul__(self, other): 8849 """Create the Z3 expression `self * other`.
8860 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8861 return fpMul(_dflt_rm(), a, b, self.ctx) 8863 def __rmul__(self, other): 8864 """Create the Z3 expression `other * self`.
8873 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8874 return fpMul(_dflt_rm(), a, b, self.ctx) 8877 """Create the Z3 expression `+self`.
""" 8881 """Create the Z3 expression `-self`.
8889 def __div__(self, other): 8890 """Create the Z3 expression `self / other`.
8901 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8902 return fpDiv(_dflt_rm(), a, b, self.ctx) 8904 def __rdiv__(self, other): 8905 """Create the Z3 expression `other / self`.
8914 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8915 return fpDiv(_dflt_rm(), a, b, self.ctx) 8917 if not sys.version < '3': 8918 def __truediv__(self, other): 8919 """Create the Z3 expression division `self / other`.
""" 8920 return self.__div__(other) 8922 def __rtruediv__(self, other): 8923 """Create the Z3 expression division `other / self`.
""" 8924 return self.__rdiv__(other) 8926 def __mod__(self, other): 8927 """Create the Z3 expression mod `self % other`.
""" 8928 return fpRem(self, other) 8930 def __rmod__(self, other): 8931 """Create the Z3 expression mod `other % self`.
""" 8932 return fpRem(other, self) 8934 class FPRMRef(ExprRef): 8935 """Floating-point rounding mode expressions
""" 8937 def as_string(self): 8938 """Return a Z3 floating point expression
as a Python string.
""" 8939 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8942 def RoundNearestTiesToEven(ctx=None): 8944 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8948 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8950 def RoundNearestTiesToAway(ctx=None): 8952 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8956 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8958 def RoundTowardPositive(ctx=None): 8960 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8964 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8966 def RoundTowardNegative(ctx=None): 8968 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8972 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8974 def RoundTowardZero(ctx=None): 8976 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8980 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8983 """Return `
True`
if `a`
is a Z3 floating-point rounding mode expression.
8992 return isinstance(a, FPRMRef) 8994 def is_fprm_value(a): 8995 """Return `
True`
if `a`
is a Z3 floating-point rounding mode numeral value.
""" 8996 return is_fprm(a) and _is_numeral(a.ctx, a.ast) 9000 class FPNumRef(FPRef): 9001 """The sign of the numeral.
9011 l = (ctypes.c_int)() 9012 if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False: 9013 raise Z3Exception("error retrieving the sign of a numeral.") 9016 """The sign of a floating-point numeral
as a bit-vector expression.
9018 Remark: NaN
's are invalid arguments. 9020 def sign_as_bv(self): 9021 return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx) 9023 """The significand of the numeral.
9029 def significand(self): 9030 return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast()) 9032 """The significand of the numeral
as a long.
9035 >>> x.significand_as_long()
9038 def significand_as_long(self): 9039 ptr = (ctypes.c_ulonglong * 1)() 9040 if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr): 9041 raise Z3Exception("error retrieving the significand of a numeral.") 9044 """The significand of the numeral
as a bit-vector expression.
9046 Remark: NaN are invalid arguments.
9048 def significand_as_bv(self): 9049 return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx) 9051 """The exponent of the numeral.
9057 def exponent(self, biased=True): 9058 return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased) 9060 """The exponent of the numeral
as a long.
9063 >>> x.exponent_as_long()
9066 def exponent_as_long(self, biased=True): 9067 ptr = (ctypes.c_longlong * 1)() 9068 if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased): 9069 raise Z3Exception("error retrieving the exponent of a numeral.") 9072 """The exponent of the numeral
as a bit-vector expression.
9074 Remark: NaNs are invalid arguments.
9076 def exponent_as_bv(self, biased=True): 9077 return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx) 9079 """Indicates whether the numeral
is a NaN.
""" 9081 return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast()) 9083 """Indicates whether the numeral
is +oo
or -oo.
""" 9085 return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast()) 9087 """Indicates whether the numeral
is +zero
or -zero.
""" 9089 return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast()) 9091 """Indicates whether the numeral
is normal.
""" 9093 return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast()) 9095 """Indicates whether the numeral
is subnormal.
""" 9096 def isSubnormal(self): 9097 return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast()) 9099 """Indicates whether the numeral
is positive.
""" 9100 def isPositive(self): 9101 return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast()) 9103 """Indicates whether the numeral
is negative.
""" 9104 def isNegative(self): 9105 return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast()) 9108 The string representation of the numeral.
9114 def as_string(self): 9115 s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast()) 9116 return ("FPVal(%s, %s)" % (s, self.sort())) 9119 """Return `
True`
if `a`
is a Z3 floating-point expression.
9129 return isinstance(a, FPRef) 9132 """Return `
True`
if `a`
is a Z3 floating-point numeral value.
9143 return is_fp(a) and _is_numeral(a.ctx, a.ast) 9145 def FPSort(ebits, sbits, ctx=None): 9146 """Return a Z3 floating-point sort of the given sizes. If `ctx=
None`, then the
global context
is used.
9148 >>> Single =
FPSort(8, 24)
9149 >>> Double =
FPSort(11, 53)
9152 >>> x =
Const(
'x', Single)
9157 return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx) 9159 def _to_float_str(val, exp=0): 9160 if isinstance(val, float): 9164 sone = math.copysign(1.0, val) 9169 elif val == float("+inf"): 9171 elif val == float("-inf"): 9174 v = val.as_integer_ratio() 9177 rvs = str(num) + '/' + str(den) 9178 res = rvs + 'p' + _to_int_str(exp) 9179 elif isinstance(val, bool): 9186 elif isinstance(val, str): 9187 inx = val.find('*(2**') 9190 elif val[-1] == ')': 9192 exp = str(int(val[inx+5:-1]) + int(exp)) 9194 _z3_assert(False, "String does not have floating-point numeral form.") 9196 _z3_assert(False, "Python value cannot be used to create floating-point numerals.") 9200 return res + 'p' + exp 9204 """Create a Z3 floating-point NaN term.
9207 >>> set_fpa_pretty(
True)
9210 >>> pb = get_fpa_pretty()
9211 >>> set_fpa_pretty(
False)
9214 >>> set_fpa_pretty(pb)
9216 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9217 return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx) 9219 def fpPlusInfinity(s): 9220 """Create a Z3 floating-point +oo term.
9223 >>> pb = get_fpa_pretty()
9224 >>> set_fpa_pretty(
True)
9227 >>> set_fpa_pretty(
False)
9230 >>> set_fpa_pretty(pb)
9232 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9233 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx) 9235 def fpMinusInfinity(s): 9236 """Create a Z3 floating-point -oo term.
""" 9237 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9238 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx) 9240 def fpInfinity(s, negative): 9241 """Create a Z3 floating-point +oo
or -oo term.
""" 9242 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9243 _z3_assert(isinstance(negative, bool), "expected Boolean flag") 9244 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx) 9247 """Create a Z3 floating-point +0.0 term.
""" 9248 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9249 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx) 9252 """Create a Z3 floating-point -0.0 term.
""" 9253 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9254 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx) 9256 def fpZero(s, negative): 9257 """Create a Z3 floating-point +0.0
or -0.0 term.
""" 9258 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9259 _z3_assert(isinstance(negative, bool), "expected Boolean flag") 9260 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx) 9262 def FPVal(sig, exp=None, fps=None, ctx=None): 9263 """Return a floating-point value of value `val`
and sort `fps`. If `ctx=
None`, then the
global context
is used.
9268 >>> print(
"0x%.8x" % v.exponent_as_long(
False))
9288 fps = _dflt_fps(ctx) 9289 _z3_assert(is_fp_sort(fps), "sort mismatch") 9292 val = _to_float_str(sig) 9293 if val == "NaN" or val == "nan": 9296 return fpMinusZero(fps) 9297 elif val == "0.0" or val == "+0.0": 9298 return fpPlusZero(fps) 9299 elif val == "+oo" or val == "+inf" or val == "+Inf": 9300 return fpPlusInfinity(fps) 9301 elif val == "-oo" or val == "-inf" or val == "-Inf": 9302 return fpMinusInfinity(fps) 9304 return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx) 9306 def FP(name, fpsort, ctx=None): 9307 """Return a floating-point constant named `name`.
9308 `fpsort`
is the floating-point sort.
9309 If `ctx=
None`, then the
global context
is used.
9319 >>> x2 =
FP(
'x', word)
9323 if isinstance(fpsort, FPSortRef) and ctx is None: 9327 return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx) 9329 def FPs(names, fpsort, ctx=None): 9330 """Return an array of floating-point constants.
9332 >>> x, y, z =
FPs(
'x y z',
FPSort(8, 24))
9343 if isinstance(names, str): 9344 names = names.split(" ") 9345 return [FP(name, fpsort, ctx) for name in names] 9347 def fpAbs(a, ctx=None): 9348 """Create a Z3 floating-point absolute value expression.
9352 >>> x =
FPVal(1.0, s)
9355 >>> y =
FPVal(-20.0, s)
9360 >>>
fpAbs(-1.25*(2**4))
9366 [a] = _coerce_fp_expr_list([a], ctx) 9367 return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx) 9369 def fpNeg(a, ctx=None): 9370 """Create a Z3 floating-point addition expression.
9381 [a] = _coerce_fp_expr_list([a], ctx) 9382 return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx) 9384 def _mk_fp_unary(f, rm, a, ctx): 9386 [a] = _coerce_fp_expr_list([a], ctx) 9388 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9389 _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression") 9390 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx) 9392 def _mk_fp_unary_norm(f, a, ctx): 9394 [a] = _coerce_fp_expr_list([a], ctx) 9396 _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression") 9397 return FPRef(f(ctx.ref(), a.as_ast()), ctx) 9399 def _mk_fp_unary_pred(f, a, ctx): 9401 [a] = _coerce_fp_expr_list([a], ctx) 9403 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9404 return BoolRef(f(ctx.ref(), a.as_ast()), ctx) 9406 def _mk_fp_bin(f, rm, a, b, ctx): 9408 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9410 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9411 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9412 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx) 9414 def _mk_fp_bin_norm(f, a, b, ctx): 9416 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9418 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression") 9419 return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 9421 def _mk_fp_bin_pred(f, a, b, ctx): 9423 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9425 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9426 return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 9428 def _mk_fp_tern(f, rm, a, b, c, ctx): 9430 [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx) 9432 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9433 _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") 9434 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx) 9436 def fpAdd(rm, a, b, ctx=None): 9437 """Create a Z3 floating-point addition expression.
9447 >>>
fpAdd(rm, x, y).sort()
9450 return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx) 9452 def fpSub(rm, a, b, ctx=None): 9453 """Create a Z3 floating-point subtraction expression.
9461 >>>
fpSub(rm, x, y).sort()
9464 return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx) 9466 def fpMul(rm, a, b, ctx=None): 9467 """Create a Z3 floating-point multiplication expression.
9475 >>>
fpMul(rm, x, y).sort()
9478 return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx) 9480 def fpDiv(rm, a, b, ctx=None): 9481 """Create a Z3 floating-point division expression.
9489 >>>
fpDiv(rm, x, y).sort()
9492 return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx) 9494 def fpRem(a, b, ctx=None): 9495 """Create a Z3 floating-point remainder expression.
9502 >>>
fpRem(x, y).sort()
9505 return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx) 9507 def fpMin(a, b, ctx=None): 9508 """Create a Z3 floating-point minimum expression.
9516 >>>
fpMin(x, y).sort()
9519 return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx) 9521 def fpMax(a, b, ctx=None): 9522 """Create a Z3 floating-point maximum expression.
9530 >>>
fpMax(x, y).sort()
9533 return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx) 9535 def fpFMA(rm, a, b, c, ctx=None): 9536 """Create a Z3 floating-point fused multiply-add expression.
9538 return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx) 9540 def fpSqrt(rm, a, ctx=None): 9541 """Create a Z3 floating-point square root expression.
9543 return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx) 9545 def fpRoundToIntegral(rm, a, ctx=None): 9546 """Create a Z3 floating-point roundToIntegral expression.
9548 return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx) 9550 def fpIsNaN(a, ctx=None): 9551 """Create a Z3 floating-point isNaN expression.
9559 return _mk_fp_unary_norm(Z3_mk_fpa_is_nan, a, ctx) 9561 def fpIsInf(a, ctx=None): 9562 """Create a Z3 floating-point isInfinite expression.
9569 return _mk_fp_unary_norm(Z3_mk_fpa_is_infinite, a, ctx) 9571 def fpIsZero(a, ctx=None): 9572 """Create a Z3 floating-point isZero expression.
9574 return _mk_fp_unary_norm(Z3_mk_fpa_is_zero, a, ctx) 9576 def fpIsNormal(a, ctx=None): 9577 """Create a Z3 floating-point isNormal expression.
9579 return _mk_fp_unary_norm(Z3_mk_fpa_is_normal, a, ctx) 9581 def fpIsSubnormal(a, ctx=None): 9582 """Create a Z3 floating-point isSubnormal expression.
9584 return _mk_fp_unary_norm(Z3_mk_fpa_is_subnormal, a, ctx) 9586 def fpIsNegative(a, ctx=None): 9587 """Create a Z3 floating-point isNegative expression.
9589 return _mk_fp_unary_norm(Z3_mk_fpa_is_negative, a, ctx) 9591 def fpIsPositive(a, ctx=None): 9592 """Create a Z3 floating-point isPositive expression.
9594 return _mk_fp_unary_norm(Z3_mk_fpa_is_positive, a, ctx) 9595 return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) 9597 def _check_fp_args(a, b): 9599 _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") 9601 def fpLT(a, b, ctx=None): 9602 """Create the Z3 floating-point expression `other < self`.
9610 return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx) 9612 def fpLEQ(a, b, ctx=None): 9613 """Create the Z3 floating-point expression `other <= self`.
9618 >>> (x <= y).sexpr()
9621 return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx) 9623 def fpGT(a, b, ctx=None): 9624 """Create the Z3 floating-point expression `other > self`.
9632 return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx) 9634 def fpGEQ(a, b, ctx=None): 9635 """Create the Z3 floating-point expression `other >= self`.
9640 >>> (x >= y).sexpr()
9643 return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx) 9645 def fpEQ(a, b, ctx=None): 9646 """Create the Z3 floating-point expression `
fpEQ(other, self)`.
9651 >>>
fpEQ(x, y).sexpr()
9654 return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx) 9656 def fpNEQ(a, b, ctx=None): 9657 """Create the Z3 floating-point expression `
Not(
fpEQ(other, self))`.
9662 >>> (x != y).sexpr()
9665 return Not(fpEQ(a, b, ctx)) 9667 def fpFP(sgn, exp, sig, ctx=None): 9668 """Create the Z3 floating-point value `
fpFP(sgn, sig, exp)`
from the three bit-vectors sgn, sig,
and exp.
9673 fpFP(1, 127, 4194304)
9674 >>> xv =
FPVal(-1.5, s)
9678 >>> slvr.add(
fpEQ(x, xv))
9681 >>> xv =
FPVal(+1.5, s)
9685 >>> slvr.add(
fpEQ(x, xv))
9689 _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch") 9690 _z3_assert(sgn.sort().size() == 1, "sort mismatch") 9692 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch") 9693 return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx) 9695 def fpToFP(a1, a2=None, a3=None, ctx=None): 9696 """Create a Z3 floating-point conversion expression
from other term sorts
9699 From a bit-vector term
in IEEE 754-2008 format:
9705 From a floating-point term with different precision:
9716 From a signed bit-vector term:
9722 if is_bv(a1) and is_fp_sort(a2): 9723 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx) 9724 elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3): 9725 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9726 elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3): 9727 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9728 elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3): 9729 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9731 raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.") 9733 def fpBVToFP(v, sort, ctx=None): 9734 """Create a Z3 floating-point conversion expression that represents the
9735 conversion
from a bit-vector term to a floating-point term.
9744 _z3_assert(is_bv(v), "First argument must be a Z3 floating-point rounding mode expression.") 9745 _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.") 9747 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx) 9749 def fpFPToFP(rm, v, sort, ctx=None): 9750 """Create a Z3 floating-point conversion expression that represents the
9751 conversion
from a floating-point term to a floating-point term of different precision.
9762 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9763 _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.") 9764 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9766 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9768 def fpRealToFP(rm, v, sort, ctx=None): 9769 """Create a Z3 floating-point conversion expression that represents the
9770 conversion
from a real term to a floating-point term.
9779 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9780 _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.") 9781 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9783 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9785 def fpSignedToFP(rm, v, sort, ctx=None): 9786 """Create a Z3 floating-point conversion expression that represents the
9787 conversion
from a signed bit-vector term (encoding an integer) to a floating-point term.
9796 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9797 _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") 9798 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9800 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9802 def fpUnsignedToFP(rm, v, sort, ctx=None): 9803 """Create a Z3 floating-point conversion expression that represents the
9804 conversion
from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9813 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9814 _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") 9815 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9817 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9819 def fpToFPUnsigned(rm, x, s, ctx=None): 9820 """Create a Z3 floating-point conversion expression,
from unsigned bit-vector to floating-point expression.
""" 9822 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9823 _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression") 9824 _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort") 9826 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx) 9828 def fpToSBV(rm, x, s, ctx=None): 9829 """Create a Z3 floating-point conversion expression,
from floating-point expression to signed bit-vector.
9843 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9844 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") 9845 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") 9847 return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9849 def fpToUBV(rm, x, s, ctx=None): 9850 """Create a Z3 floating-point conversion expression,
from floating-point expression to unsigned bit-vector.
9864 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9865 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") 9866 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") 9868 return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9870 def fpToReal(x, ctx=None): 9871 """Create a Z3 floating-point conversion expression,
from floating-point expression to real.
9885 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9887 return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx) 9889 def fpToIEEEBV(x, ctx=None): 9890 """\brief Conversion of a floating-point term into a bit-vector term
in IEEE 754-2008 format.
9892 The size of the resulting bit-vector
is automatically determined.
9894 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9895 knows only one NaN
and it will always produce the same bit-vector representation of
9910 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9912 return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx) 9916 ######################################### 9918 # Strings, Sequences and Regular expressions 9920 ######################################### 9922 class SeqSortRef(SortRef): 9923 """Sequence sort.
""" 9925 def is_string(self): 9926 """Determine
if sort
is a string
9934 return Z3_is_string_sort(self.ctx_ref(), self.ast) 9937 return _to_sort_ref(Z3_get_seq_sort_basis(self.ctx_ref(), self.ast), self.ctx) 9940 def StringSort(ctx=None): 9941 """Create a string sort
9947 return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx) 9951 """Create a sequence sort over elements provided
in the argument
9956 return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx) 9958 class SeqRef(ExprRef): 9959 """Sequence expression.
""" 9962 return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 9964 def __add__(self, other): 9965 return Concat(self, other) 9967 def __radd__(self, other): 9968 return Concat(other, self) 9970 def __getitem__(self, i): 9972 i = IntVal(i, self.ctx) 9973 return SeqRef(Z3_mk_seq_nth(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) 9977 i = IntVal(i, self.ctx) 9978 return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) 9980 def is_string(self): 9981 return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast())) 9983 def is_string_value(self): 9984 return Z3_is_string(self.ctx_ref(), self.as_ast()) 9986 def as_string(self): 9987 """Return a string representation of sequence expression.
""" 9988 if self.is_string_value(): 9989 return Z3_get_string(self.ctx_ref(), self.as_ast()) 9990 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 9993 def _coerce_seq(s, ctx=None): 9994 if isinstance(s, str): 9996 s = StringVal(s, ctx) 9998 raise Z3Exception("Non-expression passed as a sequence") 10000 raise Z3Exception("Non-sequence passed as a sequence") 10003 def _get_ctx2(a, b, ctx=None): 10013 """Return `
True`
if `a`
is a Z3 sequence expression.
10019 return isinstance(a, SeqRef) 10022 """Return `
True`
if `a`
is a Z3 string expression.
10026 return isinstance(a, SeqRef) and a.is_string() 10028 def is_string_value(a): 10029 """return 'True' if 'a' is a Z3 string constant expression.
10035 return isinstance(a, SeqRef) and a.is_string_value() 10038 def StringVal(s, ctx=None): 10039 """create a string expression
""" 10040 ctx = _get_ctx(ctx) 10041 return SeqRef(Z3_mk_lstring(ctx.ref(), len(s), s), ctx) 10043 def String(name, ctx=None): 10044 """Return a string constant named `name`. If `ctx=
None`, then the
global context
is used.
10048 ctx = _get_ctx(ctx) 10049 return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx) 10051 def SubString(s, offset, length): 10052 """Extract substring
or subsequence starting at offset
""" 10053 return Extract(s, offset, length) 10055 def SubSeq(s, offset, length): 10056 """Extract substring
or subsequence starting at offset
""" 10057 return Extract(s, offset, length) 10059 def Strings(names, ctx=None): 10060 """Return a tuple of String constants.
""" 10061 ctx = _get_ctx(ctx) 10062 if isinstance(names, str): 10063 names = names.split(" ") 10064 return [String(name, ctx) for name in names] 10067 """Create the empty sequence of the given sort
10070 >>> print(e.eq(e2))
10079 if isinstance(s, SeqSortRef): 10080 return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx) 10081 if isinstance(s, ReSortRef): 10082 return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx) 10083 raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty") 10086 """Create the regular expression that accepts the universal language
10094 if isinstance(s, ReSortRef): 10095 return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx) 10096 raise Z3Exception("Non-sequence, non-regular expression sort passed to Full") 10100 """Create a singleton sequence
""" 10101 return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx) 10103 def PrefixOf(a, b): 10104 """Check
if 'a' is a prefix of
'b' 10112 ctx = _get_ctx2(a, b) 10113 a = _coerce_seq(a, ctx) 10114 b = _coerce_seq(b, ctx) 10115 return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 10117 def SuffixOf(a, b): 10118 """Check
if 'a' is a suffix of
'b' 10126 ctx = _get_ctx2(a, b) 10127 a = _coerce_seq(a, ctx) 10128 b = _coerce_seq(b, ctx) 10129 return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 10131 def Contains(a, b): 10132 """Check
if 'a' contains
'b' 10139 >>> x, y, z =
Strings(
'x y z')
10144 ctx = _get_ctx2(a, b) 10145 a = _coerce_seq(a, ctx) 10146 b = _coerce_seq(b, ctx) 10147 return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 10150 def Replace(s, src, dst): 10151 """Replace the first occurrence of
'src' by
'dst' in 's' 10152 >>> r =
Replace(
"aaa",
"a",
"b")
10156 ctx = _get_ctx2(dst, s) 10157 if ctx is None and is_expr(src): 10159 src = _coerce_seq(src, ctx) 10160 dst = _coerce_seq(dst, ctx) 10161 s = _coerce_seq(s, ctx) 10162 return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx) 10164 def IndexOf(s, substr): 10165 return IndexOf(s, substr, IntVal(0)) 10167 def IndexOf(s, substr, offset): 10168 """Retrieve the index of substring within a string starting at a specified offset.
10175 if is_expr(offset): 10177 ctx = _get_ctx2(s, substr, ctx) 10178 s = _coerce_seq(s, ctx) 10179 substr = _coerce_seq(substr, ctx) 10180 if _is_int(offset): 10181 offset = IntVal(offset, ctx) 10182 return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx) 10184 def LastIndexOf(s, substr): 10185 """Retrieve the last index of substring within a string
""" 10187 ctx = _get_ctx2(s, substr, ctx) 10188 s = _coerce_seq(s, ctx) 10189 substr = _coerce_seq(substr, ctx) 10190 return ArithRef(Z3_mk_seq_last_index(s.ctx_ref(), s.as_ast(), substr.as_ast()), s.ctx) 10194 """Obtain the length of a sequence
's' 10200 return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx) 10203 """Convert string expression to integer
10215 return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx) 10219 """Convert integer expression to string
""" 10222 return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx) 10225 def Re(s, ctx=None): 10226 """The regular expression that accepts sequence
's' 10231 s = _coerce_seq(s, ctx) 10232 return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx) 10237 ## Regular expressions 10239 class ReSortRef(SortRef): 10240 """Regular expression sort.
""" 10243 return _to_sort_ref(Z3_get_re_sort_basis(self.ctx_ref(), self.ast), self.ctx) 10247 return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx) 10248 if s is None or isinstance(s, Context): 10250 return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), s.ctx) 10251 raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument") 10254 class ReRef(ExprRef): 10255 """Regular expressions.
""" 10257 def __add__(self, other): 10258 return Union(self, other) 10261 return isinstance(s, ReRef) 10265 """Create regular expression membership test
10274 s = _coerce_seq(s, re.ctx) 10275 return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx) 10278 """Create union of regular expressions.
10283 args = _get_args(args) 10286 _z3_assert(sz > 0, "At least one argument expected.") 10287 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 10292 for i in range(sz): 10293 v[i] = args[i].as_ast() 10294 return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx) 10296 def Intersect(*args): 10297 """Create intersection of regular expressions.
10300 args = _get_args(args) 10303 _z3_assert(sz > 0, "At least one argument expected.") 10304 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 10309 for i in range(sz): 10310 v[i] = args[i].as_ast() 10311 return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx) 10314 """Create the regular expression accepting one
or more repetitions of argument.
10323 return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx) 10326 """Create the regular expression that optionally accepts the argument.
10335 return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx) 10337 def Complement(re): 10338 """Create the complement regular expression.
""" 10339 return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx) 10342 """Create the regular expression accepting zero
or more repetitions of argument.
10351 return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx) 10353 def Loop(re, lo, hi=0): 10354 """Create the regular expression accepting between a lower
and upper bound repetitions
10355 >>> re =
Loop(
Re(
"a"), 1, 3)
10363 return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx) 10365 def Range(lo, hi, ctx = None): 10366 """Create the range regular expression over two sequences of length 1
10367 >>> range =
Range(
"a",
"z")
10373 lo = _coerce_seq(lo, ctx) 10374 hi = _coerce_seq(hi, ctx) 10375 return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx) 10377 # Special Relations 10379 def PartialOrder(a, index): 10380 return FuncDeclRef(Z3_mk_partial_order(a.ctx_ref(), a.ast, index), a.ctx); 10382 def LinearOrder(a, index): 10383 return FuncDeclRef(Z3_mk_linear_order(a.ctx_ref(), a.ast, index), a.ctx); 10385 def TreeOrder(a, index): 10386 return FuncDeclRef(Z3_mk_tree_order(a.ctx_ref(), a.ast, index), a.ctx); 10388 def PiecewiseLinearOrder(a, index): 10389 return FuncDeclRef(Z3_mk_piecewise_linear_order(a.ctx_ref(), a.ast, index), a.ctx); 10391 def TransitiveClosure(f): 10392 """Given a binary relation R, such that the two arguments have the same sort
10393 create the transitive closure relation R+.
10394 The transitive closure R+
is a new relation.
10396 return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.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)
def TupleSort(name, sorts, ctx=None)
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...
def DisjointSum(name, sorts, ctx=None)
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.
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.
def Range(lo, hi, ctx=None)
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.
void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
Assert tracked hard constraint to the optimization context.
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
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.
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={})
Strings, Sequences and Regular expressions.
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 assert_and_track(self, a, p)
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.