10 """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. 12 Several online tutorials for Z3Py are available at: 13 http://rise4fun.com/Z3Py/tutorial/guide 15 Please send feedback, comments and/or corrections on the Issue tracker for https://github.com/Z3prover/z3.git. Your comments are very valuable. 36 ... x = BitVec('x', 32) 38 ... # the expression x + y is type incorrect 40 ... except Z3Exception as ex: 41 ... print("failed: %s" % ex) 46 from .z3types
import *
47 from .z3consts
import *
48 from .z3printer
import *
49 from fractions
import Fraction
57 return isinstance(v, (int, long))
60 return isinstance(v, int)
69 major = ctypes.c_uint(0)
70 minor = ctypes.c_uint(0)
71 build = ctypes.c_uint(0)
72 rev = ctypes.c_uint(0)
74 return "%s.%s.%s" % (major.value, minor.value, build.value)
77 major = ctypes.c_uint(0)
78 minor = ctypes.c_uint(0)
79 build = ctypes.c_uint(0)
80 rev = ctypes.c_uint(0)
82 return (major.value, minor.value, build.value, rev.value)
89 def _z3_assert(cond, msg):
91 raise Z3Exception(msg)
94 """Log interaction to a file. This function must be invoked immediately after init(). """ 98 """Append user-defined string to interaction log. """ 102 """Convert an integer or string into a Z3 symbol.""" 108 def _symbol2py(ctx, s):
109 """Convert a Z3 symbol back into a Python object. """ 120 if len(args) == 1
and (isinstance(args[0], tuple)
or isinstance(args[0], list)):
122 elif len(args) == 1
and (isinstance(args[0], set)
or isinstance(args[0], AstVector)):
123 return [arg
for arg
in args[0]]
130 def _get_args_ast_list(args):
132 if isinstance(args, set)
or isinstance(args, AstVector)
or isinstance(args, tuple):
133 return [arg
for arg
in args]
139 def _to_param_value(val):
140 if isinstance(val, bool):
154 """A Context manages all other Z3 objects, global configuration options, etc. 156 Z3Py uses a default global context. For most applications this is sufficient. 157 An application may use multiple Z3 contexts. Objects created in one context 158 cannot be used in another one. However, several objects may be "translated" from 159 one context to another. It is not safe to access Z3 objects from multiple threads. 160 The only exception is the method `interrupt()` that can be used to interrupt() a long 162 The initialization method receives global configuration options for the new context. 166 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
189 """Return a reference to the actual C pointer to the Z3 context.""" 193 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions. 195 This method can be invoked from a thread different from the one executing the 196 interruptible procedure. 204 """Return a reference to the global Z3 context. 207 >>> x.ctx == main_ctx() 212 >>> x2 = Real('x', c) 219 if _main_ctx
is None:
230 """Set Z3 global (or module) parameters. 232 >>> set_param(precision=10) 235 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
239 if not set_pp_option(k, v):
253 """Reset all global (or module) parameters. 258 """Alias for 'set_param' for backward compatibility. 263 """Return the value of a Z3 global (or module) parameter 265 >>> get_param('nlsat.reorder') 268 ptr = (ctypes.c_char_p * 1)()
270 r = z3core._to_pystr(ptr[0])
272 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
282 """Superclass for all Z3 objects that have support for pretty printing.""" 287 """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions.""" 294 if self.
ctx.ref()
is not None:
298 return _to_ast_ref(self.
ast, self.
ctx)
301 return obj_to_string(self)
304 return obj_to_string(self)
307 return self.
eq(other)
320 elif is_eq(self)
and self.num_args() == 2:
321 return self.arg(0).
eq(self.arg(1))
323 raise Z3Exception(
"Symbolic expressions cannot be cast to concrete Boolean values.")
326 """Return a string representing the AST node in s-expression notation. 329 >>> ((x + 1)*x).sexpr() 335 """Return a pointer to the corresponding C Z3_ast object.""" 339 """Return unique identifier for object. It can be used for hash-tables and maps.""" 343 """Return a reference to the C context where this AST node is stored.""" 344 return self.
ctx.ref()
347 """Return `True` if `self` and `other` are structurally identical. 354 >>> n1 = simplify(n1) 355 >>> n2 = simplify(n2) 360 _z3_assert(
is_ast(other),
"Z3 AST expected")
364 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 370 >>> # Nodes in different contexts can't be mixed. 371 >>> # However, we can translate nodes from one context to another. 372 >>> x.translate(c2) + y 376 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
383 """Return a hashcode for the `self`. 385 >>> n1 = simplify(Int('x') + 1) 386 >>> n2 = simplify(2 + Int('x') - 1) 387 >>> n1.hash() == n2.hash() 393 """Return `True` if `a` is an AST node. 397 >>> is_ast(IntVal(10)) 401 >>> is_ast(BoolSort()) 403 >>> is_ast(Function('f', IntSort(), IntSort())) 410 return isinstance(a, AstRef)
413 """Return `True` if `a` and `b` are structurally identical AST nodes. 423 >>> eq(simplify(x + 1), simplify(1 + x)) 430 def _ast_kind(ctx, a):
435 def _ctx_from_ast_arg_list(args, default_ctx=None):
443 _z3_assert(ctx == a.ctx,
"Context mismatch")
448 def _ctx_from_ast_args(*args):
449 return _ctx_from_ast_arg_list(args)
451 def _to_func_decl_array(args):
453 _args = (FuncDecl * sz)()
455 _args[i] = args[i].as_func_decl()
458 def _to_ast_array(args):
462 _args[i] = args[i].as_ast()
465 def _to_ref_array(ref, args):
469 _args[i] = args[i].as_ast()
472 def _to_ast_ref(a, ctx):
473 k = _ast_kind(ctx, a)
475 return _to_sort_ref(a, ctx)
476 elif k == Z3_FUNC_DECL_AST:
477 return _to_func_decl_ref(a, ctx)
479 return _to_expr_ref(a, ctx)
487 def _sort_kind(ctx, s):
491 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.""" 499 """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts. 502 >>> b.kind() == Z3_BOOL_SORT 504 >>> b.kind() == Z3_INT_SORT 506 >>> A = ArraySort(IntSort(), IntSort()) 507 >>> A.kind() == Z3_ARRAY_SORT 509 >>> A.kind() == Z3_INT_SORT 512 return _sort_kind(self.
ctx, self.
ast)
515 """Return `True` if `self` is a subsort of `other`. 517 >>> IntSort().subsort(RealSort()) 523 """Try to cast `val` as an element of sort `self`. 525 This method is used in Z3Py to convert Python objects such as integers, 526 floats, longs and strings into Z3 expressions. 529 >>> RealSort().cast(x) 533 _z3_assert(
is_expr(val),
"Z3 expression expected")
534 _z3_assert(self.
eq(val.sort()),
"Sort mismatch")
538 """Return the name (string) of sort `self`. 540 >>> BoolSort().name() 542 >>> ArraySort(IntSort(), IntSort()).name() 548 """Return `True` if `self` and `other` are the same Z3 sort. 551 >>> p.sort() == BoolSort() 553 >>> p.sort() == IntSort() 561 """Return `True` if `self` and `other` are not the same Z3 sort. 564 >>> p.sort() != BoolSort() 566 >>> p.sort() != IntSort() 573 return AstRef.__hash__(self)
576 """Return `True` if `s` is a Z3 sort. 578 >>> is_sort(IntSort()) 580 >>> is_sort(Int('x')) 582 >>> is_expr(Int('x')) 585 return isinstance(s, SortRef)
587 def _to_sort_ref(s, ctx):
589 _z3_assert(isinstance(s, Sort),
"Z3 Sort expected")
590 k = _sort_kind(ctx, s)
591 if k == Z3_BOOL_SORT:
593 elif k == Z3_INT_SORT
or k == Z3_REAL_SORT:
595 elif k == Z3_BV_SORT:
597 elif k == Z3_ARRAY_SORT:
599 elif k == Z3_DATATYPE_SORT:
601 elif k == Z3_FINITE_DOMAIN_SORT:
603 elif k == Z3_FLOATING_POINT_SORT:
605 elif k == Z3_ROUNDING_MODE_SORT:
610 return _to_sort_ref(
Z3_get_sort(ctx.ref(), a), ctx)
613 """Create a new uninterpreted sort named `name`. 615 If `ctx=None`, then the new sort is declared in the global Z3Py context. 617 >>> A = DeclareSort('A') 618 >>> a = Const('a', A) 619 >>> b = Const('b', A) 637 """Function declaration. Every constant and function have an associated declaration. 639 The declaration assigns a name, a sort (i.e., type), and for function 640 the sort (i.e., type) of each of its arguments. Note that, in Z3, 641 a constant is a function with 0 arguments. 653 """Return the name of the function declaration `self`. 655 >>> f = Function('f', IntSort(), IntSort()) 658 >>> isinstance(f.name(), str) 664 """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0. 666 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 673 """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`. 675 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 682 _z3_assert(i < self.
arity(),
"Index out of bounds")
686 """Return the sort of the range of a function declaration. For constants, this is the sort of the constant. 688 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 695 """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc. 698 >>> d = (x + 1).decl() 699 >>> d.kind() == Z3_OP_ADD 701 >>> d.kind() == Z3_OP_MUL 709 result = [
None for i
in range(n) ]
712 if k == Z3_PARAMETER_INT:
714 elif k == Z3_PARAMETER_DOUBLE:
716 elif k == Z3_PARAMETER_RATIONAL:
718 elif k == Z3_PARAMETER_SYMBOL:
720 elif k == Z3_PARAMETER_SORT:
722 elif k == Z3_PARAMETER_AST:
724 elif k == Z3_PARAMETER_FUNC_DECL:
731 """Create a Z3 application expression using the function `self`, and the given arguments. 733 The arguments must be Z3 expressions. This method assumes that 734 the sorts of the elements in `args` match the sorts of the 735 domain. Limited coercion is supported. For example, if 736 args[0] is a Python integer, and the function expects a Z3 737 integer, then the argument is automatically converted into a 740 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 748 args = _get_args(args)
751 _z3_assert(num == self.
arity(),
"Incorrect number of arguments to %s" % self)
752 _args = (Ast * num)()
757 tmp = self.
domain(i).cast(args[i])
759 _args[i] = tmp.as_ast()
763 """Return `True` if `a` is a Z3 function declaration. 765 >>> f = Function('f', IntSort(), IntSort()) 772 return isinstance(a, FuncDeclRef)
775 """Create a new Z3 uninterpreted function with the given sorts. 777 >>> f = Function('f', IntSort(), IntSort()) 783 _z3_assert(len(sig) > 0,
"At least two arguments expected")
787 _z3_assert(
is_sort(rng),
"Z3 sort expected")
788 dom = (Sort * arity)()
789 for i
in range(arity):
791 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
796 def _to_func_decl_ref(a, ctx):
806 """Constraints, formulas and terms are expressions in Z3. 808 Expressions are ASTs. Every expression has a sort. 809 There are three main kinds of expressions: 810 function applications, quantifiers and bounded variables. 811 A constant is a function application with 0 arguments. 812 For quantifier free problems, all expressions are 813 function applications. 822 """Return the sort of expression `self`. 834 """Shorthand for `self.sort().kind()`. 836 >>> a = Array('a', IntSort(), IntSort()) 837 >>> a.sort_kind() == Z3_ARRAY_SORT 839 >>> a.sort_kind() == Z3_INT_SORT 842 return self.
sort().kind()
845 """Return a Z3 expression that represents the constraint `self == other`. 847 If `other` is `None`, then this method simply returns `False`. 858 a, b = _coerce_exprs(self, other)
863 return AstRef.__hash__(self)
866 """Return a Z3 expression that represents the constraint `self != other`. 868 If `other` is `None`, then this method simply returns `True`. 879 a, b = _coerce_exprs(self, other)
880 _args, sz = _to_ast_array((a, b))
887 """Return the Z3 function declaration associated with a Z3 application. 889 >>> f = Function('f', IntSort(), IntSort()) 898 _z3_assert(
is_app(self),
"Z3 application expected")
902 """Return the number of arguments of a Z3 application. 906 >>> (a + b).num_args() 908 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 914 _z3_assert(
is_app(self),
"Z3 application expected")
918 """Return argument `idx` of the application `self`. 920 This method assumes that `self` is a function application with at least `idx+1` arguments. 924 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 934 _z3_assert(
is_app(self),
"Z3 application expected")
935 _z3_assert(idx < self.
num_args(),
"Invalid argument index")
939 """Return a list containing the children of the given expression 943 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 953 def _to_expr_ref(a, ctx):
954 if isinstance(a, Pattern):
958 if k == Z3_QUANTIFIER_AST:
961 if sk == Z3_BOOL_SORT:
963 if sk == Z3_INT_SORT:
964 if k == Z3_NUMERAL_AST:
967 if sk == Z3_REAL_SORT:
968 if k == Z3_NUMERAL_AST:
970 if _is_algebraic(ctx, a):
974 if k == Z3_NUMERAL_AST:
978 if sk == Z3_ARRAY_SORT:
980 if sk == Z3_DATATYPE_SORT:
982 if sk == Z3_FLOATING_POINT_SORT:
983 if k == Z3_APP_AST
and _is_numeral(ctx, a):
987 if sk == Z3_FINITE_DOMAIN_SORT:
988 if k == Z3_NUMERAL_AST:
992 if sk == Z3_ROUNDING_MODE_SORT:
994 if sk == Z3_SEQ_SORT:
1000 def _coerce_expr_merge(s, a):
1013 _z3_assert(s1.ctx == s.ctx,
"context mismatch")
1014 _z3_assert(
False,
"sort mismatch")
1018 def _coerce_exprs(a, b, ctx=None):
1020 a = _py2expr(a, ctx)
1021 b = _py2expr(b, ctx)
1023 s = _coerce_expr_merge(s, a)
1024 s = _coerce_expr_merge(s, b)
1030 def _reduce(f, l, a):
1036 def _coerce_expr_list(alist, ctx=None):
1043 alist = [ _py2expr(a, ctx)
for a
in alist ]
1044 s = _reduce(_coerce_expr_merge, alist,
None)
1045 return [ s.cast(a)
for a
in alist ]
1048 """Return `True` if `a` is a Z3 expression. 1055 >>> is_expr(IntSort()) 1059 >>> is_expr(IntVal(1)) 1062 >>> is_expr(ForAll(x, x >= 0)) 1064 >>> is_expr(FPVal(1.0)) 1067 return isinstance(a, ExprRef)
1070 """Return `True` if `a` is a Z3 function application. 1072 Note that, constants are function applications with 0 arguments. 1079 >>> is_app(IntSort()) 1083 >>> is_app(IntVal(1)) 1086 >>> is_app(ForAll(x, x >= 0)) 1089 if not isinstance(a, ExprRef):
1091 k = _ast_kind(a.ctx, a)
1092 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
1095 """Return `True` if `a` is Z3 constant/variable expression. 1104 >>> is_const(IntVal(1)) 1107 >>> is_const(ForAll(x, x >= 0)) 1110 return is_app(a)
and a.num_args() == 0
1113 """Return `True` if `a` is variable. 1115 Z3 uses de-Bruijn indices for representing bound variables in 1123 >>> f = Function('f', IntSort(), IntSort()) 1124 >>> # Z3 replaces x with bound variables when ForAll is executed. 1125 >>> q = ForAll(x, f(x) == x) 1131 >>> is_var(b.arg(1)) 1134 return is_expr(a)
and _ast_kind(a.ctx, a) == Z3_VAR_AST
1137 """Return the de-Bruijn index of the Z3 bounded variable `a`. 1145 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1146 >>> # Z3 replaces x and y with bound variables when ForAll is executed. 1147 >>> q = ForAll([x, y], f(x, y) == x + y) 1149 f(Var(1), Var(0)) == Var(1) + Var(0) 1153 >>> v1 = b.arg(0).arg(0) 1154 >>> v2 = b.arg(0).arg(1) 1159 >>> get_var_index(v1) 1161 >>> get_var_index(v2) 1165 _z3_assert(
is_var(a),
"Z3 bound variable expected")
1169 """Return `True` if `a` is an application of the given kind `k`. 1173 >>> is_app_of(n, Z3_OP_ADD) 1175 >>> is_app_of(n, Z3_OP_MUL) 1178 return is_app(a)
and a.decl().kind() == k
1180 def If(a, b, c, ctx=None):
1181 """Create a Z3 if-then-else expression. 1185 >>> max = If(x > y, x, y) 1191 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1192 return Cond(a, b, c, ctx)
1194 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1197 b, c = _coerce_exprs(b, c, ctx)
1199 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1200 return _to_expr_ref(
Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1203 """Create a Z3 distinct expression. 1210 >>> Distinct(x, y, z) 1212 >>> simplify(Distinct(x, y, z)) 1214 >>> simplify(Distinct(x, y, z), blast_distinct=True) 1215 And(Not(x == y), Not(x == z), Not(y == z)) 1217 args = _get_args(args)
1218 ctx = _ctx_from_ast_arg_list(args)
1220 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1221 args = _coerce_expr_list(args, ctx)
1222 _args, sz = _to_ast_array(args)
1225 def _mk_bin(f, a, b):
1228 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1229 args[0] = a.as_ast()
1230 args[1] = b.as_ast()
1231 return f(a.ctx.ref(), 2, args)
1234 """Create a constant of the given sort. 1236 >>> Const('x', IntSort()) 1240 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
1245 """Create a several constants of the given sort. 1247 `names` is a string containing the names of all constants to be created. 1248 Blank spaces separate the names of different constants. 1250 >>> x, y, z = Consts('x y z', IntSort()) 1254 if isinstance(names, str):
1255 names = names.split(
" ")
1256 return [
Const(name, sort)
for name
in names]
1259 """Create a Z3 free variable. Free variables are used to create quantified formulas. 1261 >>> Var(0, IntSort()) 1263 >>> eq(Var(0, IntSort()), Var(0, BoolSort())) 1267 _z3_assert(
is_sort(s),
"Z3 sort expected")
1268 return _to_expr_ref(
Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1272 Create a real free variable. Free variables are used to create quantified formulas. 1273 They are also used to create polynomials. 1282 Create a list of Real free variables. 1283 The variables have ids: 0, 1, ..., n-1 1285 >>> x0, x1, x2, x3 = RealVarVector(4) 1300 """Try to cast `val` as a Boolean. 1302 >>> x = BoolSort().cast(True) 1312 if isinstance(val, bool):
1316 _z3_assert(
is_expr(val),
"True, False or Z3 Boolean expression expected. Received %s" % val)
1317 if not self.
eq(val.sort()):
1318 _z3_assert(self.
eq(val.sort()),
"Value cannot be converted into a Z3 Boolean value")
1322 return isinstance(other, ArithSortRef)
1332 """All Boolean expressions are instances of this class.""" 1340 """Create the Z3 expression `self * other`. 1346 return If(self, other, 0)
1350 """Return `True` if `a` is a Z3 Boolean expression. 1356 >>> is_bool(And(p, q)) 1364 return isinstance(a, BoolRef)
1367 """Return `True` if `a` is the Z3 true expression. 1372 >>> is_true(simplify(p == p)) 1377 >>> # True is a Python Boolean expression 1384 """Return `True` if `a` is the Z3 false expression. 1391 >>> is_false(BoolVal(False)) 1397 """Return `True` if `a` is a Z3 and expression. 1399 >>> p, q = Bools('p q') 1400 >>> is_and(And(p, q)) 1402 >>> is_and(Or(p, q)) 1408 """Return `True` if `a` is a Z3 or expression. 1410 >>> p, q = Bools('p q') 1413 >>> is_or(And(p, q)) 1419 """Return `True` if `a` is a Z3 not expression. 1430 """Return `True` if `a` is a Z3 equality expression. 1432 >>> x, y = Ints('x y') 1439 """Return `True` if `a` is a Z3 distinct expression. 1441 >>> x, y, z = Ints('x y z') 1442 >>> is_distinct(x == y) 1444 >>> is_distinct(Distinct(x, y, z)) 1450 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. 1454 >>> p = Const('p', BoolSort()) 1457 >>> r = Function('r', IntSort(), IntSort(), BoolSort()) 1464 return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx) 1466 def BoolVal(val, ctx=None): 1467 """Return the Boolean value `
True`
or `
False`. If `ctx=
None`, then the
global context
is used.
1480 return BoolRef(Z3_mk_false(ctx.ref()), ctx) 1482 return BoolRef(Z3_mk_true(ctx.ref()), ctx) 1484 def Bool(name, ctx=None): 1485 """Return a Boolean constant named `name`. If `ctx=
None`, then the
global context
is used.
1493 return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx) 1495 def Bools(names, ctx=None): 1496 """Return a tuple of Boolean constants.
1498 `names`
is a single string containing all names separated by blank spaces.
1499 If `ctx=
None`, then the
global context
is used.
1501 >>> p, q, r =
Bools(
'p q r')
1502 >>>
And(p,
Or(q, r))
1506 if isinstance(names, str): 1507 names = names.split(" ") 1508 return [Bool(name, ctx) for name in names] 1510 def BoolVector(prefix, sz, ctx=None): 1511 """Return a list of Boolean constants of size `sz`.
1513 The constants are named using the given prefix.
1514 If `ctx=
None`, then the
global context
is used.
1520 And(p__0, p__1, p__2)
1522 return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ] 1524 def FreshBool(prefix='b', ctx=None): 1525 """Return a fresh Boolean constant
in the given context using the given prefix.
1527 If `ctx=
None`, then the
global context
is used.
1535 return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx) 1537 def Implies(a, b, ctx=None): 1538 """Create a Z3 implies expression.
1540 >>> p, q =
Bools(
'p q')
1546 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 1550 return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 1552 def Xor(a, b, ctx=None): 1553 """Create a Z3 Xor expression.
1555 >>> p, q =
Bools(
'p q')
1561 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 1565 return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 1567 def Not(a, ctx=None): 1568 """Create a Z3
not expression
or probe.
1576 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) 1578 # Not is also used to build probes 1579 return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx) 1583 return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx) 1585 def _has_probe(args): 1586 """Return `
True`
if one of the elements of the given collection
is a Z3 probe.
""" 1593 """Create a Z3
and-expression
or and-probe.
1595 >>> p, q, r =
Bools(
'p q r')
1600 And(p__0, p__1, p__2, p__3, p__4)
1604 last_arg = args[len(args)-1] 1605 if isinstance(last_arg, Context): 1606 ctx = args[len(args)-1] 1607 args = args[:len(args)-1] 1608 elif len(args) == 1 and isinstance(args[0], AstVector): 1610 args = [a for a in args[0]] 1613 args = _get_args(args) 1614 ctx_args = _ctx_from_ast_arg_list(args, ctx) 1616 _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") 1617 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") 1618 if _has_probe(args): 1619 return _probe_and(args, ctx) 1621 args = _coerce_expr_list(args, ctx) 1622 _args, sz = _to_ast_array(args) 1623 return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx) 1626 """Create a Z3
or-expression
or or-probe.
1628 >>> p, q, r =
Bools(
'p q r')
1633 Or(p__0, p__1, p__2, p__3, p__4)
1637 last_arg = args[len(args)-1] 1638 if isinstance(last_arg, Context): 1639 ctx = args[len(args)-1] 1640 args = args[:len(args)-1] 1643 args = _get_args(args) 1644 ctx_args = _ctx_from_ast_arg_list(args, ctx) 1646 _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") 1647 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") 1648 if _has_probe(args): 1649 return _probe_or(args, ctx) 1651 args = _coerce_expr_list(args, ctx) 1652 _args, sz = _to_ast_array(args) 1653 return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx) 1655 ######################################### 1659 ######################################### 1661 class PatternRef(ExprRef): 1662 """Patterns are hints
for quantifier instantiation.
1664 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1667 return Z3_pattern_to_ast(self.ctx_ref(), self.ast) 1670 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1673 """Return `
True`
if `a`
is a Z3 pattern (hint
for quantifier instantiation.
1675 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1679 >>> q =
ForAll(x, f(x) == 0, patterns = [ f(x) ])
1682 >>> q.num_patterns()
1689 return isinstance(a, PatternRef) 1691 def MultiPattern(*args): 1692 """Create a Z3 multi-pattern using the given expressions `*args`
1694 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1702 >>> q.num_patterns()
1710 _z3_assert(len(args) > 0, "At least one argument expected") 1711 _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected") 1713 args, sz = _to_ast_array(args) 1714 return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx) 1716 def _to_pattern(arg): 1720 return MultiPattern(arg) 1722 ######################################### 1726 ######################################### 1728 class QuantifierRef(BoolRef): 1729 """Universally
and Existentially quantified formulas.
""" 1735 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1738 """Return the Boolean sort.
""" 1739 return BoolSort(self.ctx) 1741 def is_forall(self): 1742 """Return `
True`
if `self`
is a universal quantifier.
1746 >>> q =
ForAll(x, f(x) == 0)
1749 >>> q =
Exists(x, f(x) != 0)
1753 return Z3_is_quantifier_forall(self.ctx_ref(), self.ast) 1756 """Return the weight annotation of `self`.
1760 >>> q =
ForAll(x, f(x) == 0)
1763 >>> q =
ForAll(x, f(x) == 0, weight=10)
1767 return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast)) 1769 def num_patterns(self): 1770 """Return the number of patterns (i.e., quantifier instantiation hints)
in `self`.
1775 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1776 >>> q.num_patterns()
1779 return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast)) 1781 def pattern(self, idx): 1782 """Return a pattern (i.e., quantifier instantiation hints)
in `self`.
1787 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1788 >>> q.num_patterns()
1796 _z3_assert(idx < self.num_patterns(), "Invalid pattern idx") 1797 return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1799 def num_no_patterns(self): 1800 """Return the number of no-patterns.
""" 1801 return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast) 1803 def no_pattern(self, idx): 1804 """Return a no-pattern.
""" 1806 _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx") 1807 return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1810 """Return the expression being quantified.
1814 >>> q =
ForAll(x, f(x) == 0)
1818 return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx) 1821 """Return the number of variables bounded by this quantifier.
1826 >>> q =
ForAll([x, y], f(x, y) >= x)
1830 return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast)) 1832 def var_name(self, idx): 1833 """Return a string representing a name used when displaying the quantifier.
1838 >>> q =
ForAll([x, y], f(x, y) >= x)
1845 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1846 return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx)) 1848 def var_sort(self, idx): 1849 """Return the sort of a bound variable.
1854 >>> q =
ForAll([x, y], f(x, y) >= x)
1861 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1862 return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx) 1865 """Return a list containing a single element self.
body()
1869 >>> q =
ForAll(x, f(x) == 0)
1873 return [ self.body() ] 1875 def is_quantifier(a): 1876 """Return `
True`
if `a`
is a Z3 quantifier.
1880 >>> q =
ForAll(x, f(x) == 0)
1886 return isinstance(a, QuantifierRef) 1888 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 1890 _z3_assert(is_bool(body), "Z3 expression expected") 1891 _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)") 1892 _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected") 1893 _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions") 1900 _vs = (Ast * num_vars)() 1901 for i in range(num_vars): 1902 ## TODO: Check if is constant 1903 _vs[i] = vs[i].as_ast() 1904 patterns = [ _to_pattern(p) for p in patterns ] 1905 num_pats = len(patterns) 1906 _pats = (Pattern * num_pats)() 1907 for i in range(num_pats): 1908 _pats[i] = patterns[i].ast 1909 _no_pats, num_no_pats = _to_ast_array(no_patterns) 1910 qid = to_symbol(qid, ctx) 1911 skid = to_symbol(skid, ctx) 1912 return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid, 1915 num_no_pats, _no_pats, 1916 body.as_ast()), ctx) 1918 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 1919 """Create a Z3 forall formula.
1921 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
1923 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1928 >>>
ForAll([x, y], f(x, y) >= x)
1929 ForAll([x, y], f(x, y) >= x)
1930 >>>
ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
1931 ForAll([x, y], f(x, y) >= x)
1932 >>>
ForAll([x, y], f(x, y) >= x, weight=10)
1933 ForAll([x, y], f(x, y) >= x)
1935 return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns) 1937 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 1938 """Create a Z3 exists formula.
1940 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
1942 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1947 >>> q =
Exists([x, y], f(x, y) >= x, skid=
"foo")
1949 Exists([x, y], f(x, y) >= x)
1952 >>> r =
Tactic(
'nnf')(q).as_expr()
1956 return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns) 1958 ######################################### 1962 ######################################### 1964 class ArithSortRef(SortRef): 1965 """Real
and Integer sorts.
""" 1968 """Return `
True`
if `self`
is of the sort Real.
1979 return self.kind() == Z3_REAL_SORT 1982 """Return `
True`
if `self`
is of the sort Integer.
1993 return self.kind() == Z3_INT_SORT 1995 def subsort(self, other): 1996 """Return `
True`
if `self`
is a subsort of `other`.
""" 1997 return self.is_int() and is_arith_sort(other) and other.is_real() 1999 def cast(self, val): 2000 """Try to cast `val`
as an Integer
or Real.
2015 _z3_assert(self.ctx == val.ctx, "Context mismatch") 2019 if val_s.is_int() and self.is_real(): 2021 if val_s.is_bool() and self.is_int(): 2022 return If(val, 1, 0) 2023 if val_s.is_bool() and self.is_real(): 2024 return ToReal(If(val, 1, 0)) 2026 _z3_assert(False, "Z3 Integer/Real expression expected" ) 2029 return IntVal(val, self.ctx) 2031 return RealVal(val, self.ctx) 2033 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self) 2035 def is_arith_sort(s): 2036 """Return `
True`
if s
is an arithmetical sort (type).
2044 >>> n =
Int(
'x') + 1
2048 return isinstance(s, ArithSortRef) 2050 class ArithRef(ExprRef): 2051 """Integer
and Real expressions.
""" 2054 """Return the sort (type) of the arithmetical expression `self`.
2061 return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 2064 """Return `
True`
if `self`
is an integer expression.
2075 return self.sort().is_int() 2078 """Return `
True`
if `self`
is an real expression.
2086 return self.sort().is_real() 2088 def __add__(self, other): 2089 """Create the Z3 expression `self + other`.
2098 a, b = _coerce_exprs(self, other) 2099 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx) 2101 def __radd__(self, other): 2102 """Create the Z3 expression `other + self`.
2108 a, b = _coerce_exprs(self, other) 2109 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx) 2111 def __mul__(self, other): 2112 """Create the Z3 expression `self * other`.
2121 a, b = _coerce_exprs(self, other) 2122 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx) 2124 def __rmul__(self, other): 2125 """Create the Z3 expression `other * self`.
2131 a, b = _coerce_exprs(self, other) 2132 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx) 2134 def __sub__(self, other): 2135 """Create the Z3 expression `self - other`.
2144 a, b = _coerce_exprs(self, other) 2145 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx) 2147 def __rsub__(self, other): 2148 """Create the Z3 expression `other - self`.
2154 a, b = _coerce_exprs(self, other) 2155 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx) 2157 def __pow__(self, other): 2158 """Create the Z3 expression `self**other` (**
is the power operator).
2168 a, b = _coerce_exprs(self, other) 2169 return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2171 def __rpow__(self, other): 2172 """Create the Z3 expression `other**self` (**
is the power operator).
2182 a, b = _coerce_exprs(self, other) 2183 return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2185 def __div__(self, other): 2186 """Create the Z3 expression `other/self`.
2205 a, b = _coerce_exprs(self, other) 2206 return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2208 def __truediv__(self, other): 2209 """Create the Z3 expression `other/self`.
""" 2210 return self.__div__(other) 2212 def __rdiv__(self, other): 2213 """Create the Z3 expression `other/self`.
2226 a, b = _coerce_exprs(self, other) 2227 return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2229 def __rtruediv__(self, other): 2230 """Create the Z3 expression `other/self`.
""" 2231 return self.__rdiv__(other) 2233 def __mod__(self, other): 2234 """Create the Z3 expression `other%self`.
2243 a, b = _coerce_exprs(self, other) 2245 _z3_assert(a.is_int(), "Z3 integer expression expected") 2246 return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2248 def __rmod__(self, other): 2249 """Create the Z3 expression `other%self`.
2255 a, b = _coerce_exprs(self, other) 2257 _z3_assert(a.is_int(), "Z3 integer expression expected") 2258 return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2261 """Return an expression representing `-self`.
2269 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx) 2280 def __le__(self, other): 2281 """Create the Z3 expression `other <= self`.
2283 >>> x, y =
Ints(
'x y')
2290 a, b = _coerce_exprs(self, other) 2291 return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2293 def __lt__(self, other): 2294 """Create the Z3 expression `other < self`.
2296 >>> x, y =
Ints(
'x y')
2303 a, b = _coerce_exprs(self, other) 2304 return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2306 def __gt__(self, other): 2307 """Create the Z3 expression `other > self`.
2309 >>> x, y =
Ints(
'x y')
2316 a, b = _coerce_exprs(self, other) 2317 return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2319 def __ge__(self, other): 2320 """Create the Z3 expression `other >= self`.
2322 >>> x, y =
Ints(
'x y')
2329 a, b = _coerce_exprs(self, other) 2330 return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2333 """Return `
True`
if `a`
is an arithmetical expression.
2350 return isinstance(a, ArithRef) 2353 """Return `
True`
if `a`
is an integer expression.
2368 return is_arith(a) and a.is_int() 2371 """Return `
True`
if `a`
is a real expression.
2386 return is_arith(a) and a.is_real() 2388 def _is_numeral(ctx, a): 2389 return Z3_is_numeral_ast(ctx.ref(), a) 2391 def _is_algebraic(ctx, a): 2392 return Z3_is_algebraic_number(ctx.ref(), a) 2394 def is_int_value(a): 2395 """Return `
True`
if `a`
is an integer value of sort Int.
2403 >>> n =
Int(
'x') + 1
2415 return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast()) 2417 def is_rational_value(a): 2418 """Return `
True`
if `a`
is rational value of sort Real.
2428 >>> n =
Real(
'x') + 1
2436 return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast()) 2438 def is_algebraic_value(a): 2439 """Return `
True`
if `a`
is an algebraic value of sort Real.
2449 return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast()) 2452 """Return `
True`
if `a`
is an expression of the form b + c.
2454 >>> x, y =
Ints(
'x y')
2460 return is_app_of(a, Z3_OP_ADD) 2463 """Return `
True`
if `a`
is an expression of the form b * c.
2465 >>> x, y =
Ints(
'x y')
2471 return is_app_of(a, Z3_OP_MUL) 2474 """Return `
True`
if `a`
is an expression of the form b - c.
2476 >>> x, y =
Ints(
'x y')
2482 return is_app_of(a, Z3_OP_SUB) 2485 """Return `
True`
if `a`
is an expression of the form b / c.
2487 >>> x, y =
Reals(
'x y')
2492 >>> x, y =
Ints(
'x y')
2498 return is_app_of(a, Z3_OP_DIV) 2501 """Return `
True`
if `a`
is an expression of the form b div c.
2503 >>> x, y =
Ints(
'x y')
2509 return is_app_of(a, Z3_OP_IDIV) 2512 """Return `
True`
if `a`
is an expression of the form b % c.
2514 >>> x, y =
Ints(
'x y')
2520 return is_app_of(a, Z3_OP_MOD) 2523 """Return `
True`
if `a`
is an expression of the form b <= c.
2525 >>> x, y =
Ints(
'x y')
2531 return is_app_of(a, Z3_OP_LE) 2534 """Return `
True`
if `a`
is an expression of the form b < c.
2536 >>> x, y =
Ints(
'x y')
2542 return is_app_of(a, Z3_OP_LT) 2545 """Return `
True`
if `a`
is an expression of the form b >= c.
2547 >>> x, y =
Ints(
'x y')
2553 return is_app_of(a, Z3_OP_GE) 2556 """Return `
True`
if `a`
is an expression of the form b > c.
2558 >>> x, y =
Ints(
'x y')
2564 return is_app_of(a, Z3_OP_GT) 2567 """Return `
True`
if `a`
is an expression of the form
IsInt(b).
2575 return is_app_of(a, Z3_OP_IS_INT) 2578 """Return `
True`
if `a`
is an expression of the form
ToReal(b).
2589 return is_app_of(a, Z3_OP_TO_REAL) 2592 """Return `
True`
if `a`
is an expression of the form
ToInt(b).
2603 return is_app_of(a, Z3_OP_TO_INT) 2605 class IntNumRef(ArithRef): 2606 """Integer values.
""" 2609 """Return a Z3 integer numeral
as a Python long (bignum) numeral.
2618 _z3_assert(self.is_int(), "Integer value expected") 2619 return int(self.as_string()) 2621 def as_string(self): 2622 """Return a Z3 integer numeral
as a Python string.
2627 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2629 class RatNumRef(ArithRef): 2630 """Rational values.
""" 2632 def numerator(self): 2633 """ Return the numerator of a Z3 rational numeral.
2645 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx) 2647 def denominator(self): 2648 """ Return the denominator of a Z3 rational numeral.
2656 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx) 2658 def numerator_as_long(self): 2659 """ Return the numerator
as a Python long.
2666 >>> v.numerator_as_long() + 1 == 10000000001
2669 return self.numerator().as_long() 2671 def denominator_as_long(self): 2672 """ Return the denominator
as a Python long.
2677 >>> v.denominator_as_long()
2680 return self.denominator().as_long() 2688 def is_int_value(self): 2689 return self.denominator().is_int() and self.denominator_as_long() == 1 2692 _z3_assert(self.is_int(), "Expected integer fraction") 2693 return self.numerator_as_long() 2695 def as_decimal(self, prec): 2696 """ Return a Z3 rational value
as a string
in decimal notation using at most `prec` decimal places.
2705 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2707 def as_string(self): 2708 """Return a Z3 rational numeral
as a Python string.
2714 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2716 def as_fraction(self): 2717 """Return a Z3 rational
as a Python Fraction object.
2723 return Fraction(self.numerator_as_long(), self.denominator_as_long()) 2725 class AlgebraicNumRef(ArithRef): 2726 """Algebraic irrational values.
""" 2728 def approx(self, precision=10): 2729 """Return a Z3 rational number that approximates the algebraic number `self`.
2730 The result `r`
is such that |r - self| <= 1/10^precision
2734 6838717160008073720548335/4835703278458516698824704
2738 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx) 2739 def as_decimal(self, prec): 2740 """Return a string representation of the algebraic number `self`
in decimal notation using `prec` decimal places
2743 >>> x.as_decimal(10)
2745 >>> x.as_decimal(20)
2746 '1.41421356237309504880?' 2748 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2750 def _py2expr(a, ctx=None): 2751 if isinstance(a, bool): 2752 return BoolVal(a, ctx) 2754 return IntVal(a, ctx) 2755 if isinstance(a, float): 2756 return RealVal(a, ctx) 2758 _z3_assert(False, "Python bool, int, long or float expected") 2760 def IntSort(ctx=None): 2761 """Return the integer sort
in the given context. If `ctx=
None`, then the
global context
is used.
2774 return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx) 2776 def RealSort(ctx=None): 2777 """Return the real sort
in the given context. If `ctx=
None`, then the
global context
is used.
2790 return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx) 2792 def _to_int_str(val): 2793 if isinstance(val, float): 2794 return str(int(val)) 2795 elif isinstance(val, bool): 2802 elif isinstance(val, str): 2805 _z3_assert(False, "Python value cannot be used as a Z3 integer") 2807 def IntVal(val, ctx=None): 2808 """Return a Z3 integer value. If `ctx=
None`, then the
global context
is used.
2816 return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx) 2818 def RealVal(val, ctx=None): 2819 """Return a Z3 real value.
2821 `val` may be a Python int, long, float
or string representing a number
in decimal
or rational notation.
2822 If `ctx=
None`, then the
global context
is used.
2834 return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx) 2836 def RatVal(a, b, ctx=None): 2837 """Return a Z3 rational a/b.
2839 If `ctx=
None`, then the
global context
is used.
2847 _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer") 2848 _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer") 2849 return simplify(RealVal(a, ctx)/RealVal(b, ctx)) 2851 def Q(a, b, ctx=None): 2852 """Return a Z3 rational a/b.
2854 If `ctx=
None`, then the
global context
is used.
2861 return simplify(RatVal(a, b)) 2863 def Int(name, ctx=None): 2864 """Return an integer constant named `name`. If `ctx=
None`, then the
global context
is used.
2873 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx) 2875 def Ints(names, ctx=None): 2876 """Return a tuple of Integer constants.
2878 >>> x, y, z =
Ints(
'x y z')
2883 if isinstance(names, str): 2884 names = names.split(" ") 2885 return [Int(name, ctx) for name in names] 2887 def IntVector(prefix, sz, ctx=None): 2888 """Return a list of integer constants of size `sz`.
2896 return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ] 2898 def FreshInt(prefix='x', ctx=None): 2899 """Return a fresh integer constant
in the given context using the given prefix.
2909 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx) 2911 def Real(name, ctx=None): 2912 """Return a real constant named `name`. If `ctx=
None`, then the
global context
is used.
2921 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx) 2923 def Reals(names, ctx=None): 2924 """Return a tuple of real constants.
2926 >>> x, y, z =
Reals(
'x y z')
2929 >>>
Sum(x, y, z).sort()
2933 if isinstance(names, str): 2934 names = names.split(" ") 2935 return [Real(name, ctx) for name in names] 2937 def RealVector(prefix, sz, ctx=None): 2938 """Return a list of real constants of size `sz`.
2948 return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ] 2950 def FreshReal(prefix='b', ctx=None): 2951 """Return a fresh real constant
in the given context using the given prefix.
2961 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx) 2964 """ Return the Z3 expression
ToReal(a).
2976 _z3_assert(a.is_int(), "Z3 integer expression expected.") 2978 return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx) 2981 """ Return the Z3 expression
ToInt(a).
2993 _z3_assert(a.is_real(), "Z3 real expression expected.") 2995 return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx) 2998 """ Return the Z3 predicate
IsInt(a).
3001 >>>
IsInt(x +
"1/2")
3005 >>>
solve(
IsInt(x +
"1/2"), x > 0, x < 1, x !=
"1/2")
3009 _z3_assert(a.is_real(), "Z3 real expression expected.") 3011 return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx) 3013 def Sqrt(a, ctx=None): 3014 """ Return a Z3 expression which represents the square root of a.
3025 def Cbrt(a, ctx=None): 3026 """ Return a Z3 expression which represents the cubic root of a.
3037 ######################################### 3041 ######################################### 3043 class BitVecSortRef(SortRef): 3044 """Bit-vector sort.
""" 3047 """Return the size (number of bits) of the bit-vector sort `self`.
3053 return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast)) 3055 def subsort(self, other): 3056 return is_bv_sort(other) and self.size() < other.size() 3058 def cast(self, val): 3059 """Try to cast `val`
as a Bit-Vector.
3064 >>> b.cast(10).
sexpr()
3069 _z3_assert(self.ctx == val.ctx, "Context mismatch") 3070 # Idea: use sign_extend if sort of val is a bitvector of smaller size 3073 return BitVecVal(val, self) 3076 """Return
True if `s`
is a Z3 bit-vector sort.
3083 return isinstance(s, BitVecSortRef) 3085 class BitVecRef(ExprRef): 3086 """Bit-vector expressions.
""" 3089 """Return the sort of the bit-vector expression `self`.
3097 return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 3100 """Return the number of bits of the bit-vector expression `self`.
3108 return self.sort().size() 3110 def __add__(self, other): 3111 """Create the Z3 expression `self + other`.
3120 a, b = _coerce_exprs(self, other) 3121 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3123 def __radd__(self, other): 3124 """Create the Z3 expression `other + self`.
3130 a, b = _coerce_exprs(self, other) 3131 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3133 def __mul__(self, other): 3134 """Create the Z3 expression `self * other`.
3143 a, b = _coerce_exprs(self, other) 3144 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3146 def __rmul__(self, other): 3147 """Create the Z3 expression `other * self`.
3153 a, b = _coerce_exprs(self, other) 3154 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3156 def __sub__(self, other): 3157 """Create the Z3 expression `self - other`.
3166 a, b = _coerce_exprs(self, other) 3167 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3169 def __rsub__(self, other): 3170 """Create the Z3 expression `other - self`.
3176 a, b = _coerce_exprs(self, other) 3177 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3179 def __or__(self, other): 3180 """Create the Z3 expression bitwise-
or `self | other`.
3189 a, b = _coerce_exprs(self, other) 3190 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3192 def __ror__(self, other): 3193 """Create the Z3 expression bitwise-
or `other | self`.
3199 a, b = _coerce_exprs(self, other) 3200 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3202 def __and__(self, other): 3203 """Create the Z3 expression bitwise-
and `self & other`.
3212 a, b = _coerce_exprs(self, other) 3213 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3215 def __rand__(self, other): 3216 """Create the Z3 expression bitwise-
or `other & self`.
3222 a, b = _coerce_exprs(self, other) 3223 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3225 def __xor__(self, other): 3226 """Create the Z3 expression bitwise-xor `self ^ other`.
3235 a, b = _coerce_exprs(self, other) 3236 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3238 def __rxor__(self, other): 3239 """Create the Z3 expression bitwise-xor `other ^ self`.
3245 a, b = _coerce_exprs(self, other) 3246 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3258 """Return an expression representing `-self`.
3266 return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx) 3268 def __invert__(self): 3269 """Create the Z3 expression bitwise-
not `~self`.
3277 return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx) 3279 def __div__(self, other): 3280 """Create the Z3 expression (signed) division `self / other`.
3282 Use the function
UDiv()
for unsigned division.
3295 a, b = _coerce_exprs(self, other) 3296 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3298 def __truediv__(self, other): 3299 """Create the Z3 expression (signed) division `self / other`.
""" 3300 return self.__div__(other) 3302 def __rdiv__(self, other): 3303 """Create the Z3 expression (signed) division `other / self`.
3305 Use the function
UDiv()
for unsigned division.
3310 >>> (10 / x).
sexpr()
3311 '(bvsdiv #x0000000a x)' 3313 '(bvudiv #x0000000a x)' 3315 a, b = _coerce_exprs(self, other) 3316 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3318 def __rtruediv__(self, other): 3319 """Create the Z3 expression (signed) division `other / self`.
""" 3320 return self.__rdiv__(other) 3322 def __mod__(self, other): 3323 """Create the Z3 expression (signed) mod `self % other`.
3325 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3340 a, b = _coerce_exprs(self, other) 3341 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3343 def __rmod__(self, other): 3344 """Create the Z3 expression (signed) mod `other % self`.
3346 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3351 >>> (10 % x).
sexpr()
3352 '(bvsmod #x0000000a x)' 3354 '(bvurem #x0000000a x)' 3356 '(bvsrem #x0000000a x)' 3358 a, b = _coerce_exprs(self, other) 3359 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3361 def __le__(self, other): 3362 """Create the Z3 expression (signed) `other <= self`.
3364 Use the function
ULE()
for unsigned less than
or equal to.
3369 >>> (x <= y).
sexpr()
3374 a, b = _coerce_exprs(self, other) 3375 return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3377 def __lt__(self, other): 3378 """Create the Z3 expression (signed) `other < self`.
3380 Use the function
ULT()
for unsigned less than.
3390 a, b = _coerce_exprs(self, other) 3391 return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3393 def __gt__(self, other): 3394 """Create the Z3 expression (signed) `other > self`.
3396 Use the function
UGT()
for unsigned greater than.
3406 a, b = _coerce_exprs(self, other) 3407 return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3409 def __ge__(self, other): 3410 """Create the Z3 expression (signed) `other >= self`.
3412 Use the function
UGE()
for unsigned greater than
or equal to.
3417 >>> (x >= y).
sexpr()
3422 a, b = _coerce_exprs(self, other) 3423 return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3425 def __rshift__(self, other): 3426 """Create the Z3 expression (arithmetical) right shift `self >> other`
3428 Use the function
LShR()
for the right logical shift
3433 >>> (x >> y).
sexpr()
3452 a, b = _coerce_exprs(self, other) 3453 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3455 def __lshift__(self, other): 3456 """Create the Z3 expression left shift `self << other`
3461 >>> (x << y).
sexpr()
3466 a, b = _coerce_exprs(self, other) 3467 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3469 def __rrshift__(self, other): 3470 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3472 Use the function
LShR()
for the right logical shift
3477 >>> (10 >> x).
sexpr()
3478 '(bvashr #x0000000a x)' 3480 a, b = _coerce_exprs(self, other) 3481 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3483 def __rlshift__(self, other): 3484 """Create the Z3 expression left shift `other << self`.
3486 Use the function
LShR()
for the right logical shift
3491 >>> (10 << x).
sexpr()
3492 '(bvshl #x0000000a x)' 3494 a, b = _coerce_exprs(self, other) 3495 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3497 class BitVecNumRef(BitVecRef): 3498 """Bit-vector values.
""" 3501 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral.
3506 >>> print(
"0x%.8x" % v.as_long())
3509 return int(self.as_string()) 3511 def as_signed_long(self): 3512 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral. The most significant bit
is assumed to be the sign.
3526 val = self.as_long() 3527 if val >= 2**(sz - 1): 3529 if val < -2**(sz - 1): 3533 def as_string(self): 3534 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 3537 """Return `
True`
if `a`
is a Z3 bit-vector expression.
3547 return isinstance(a, BitVecRef) 3550 """Return `
True`
if `a`
is a Z3 bit-vector numeral value.
3561 return is_bv(a) and _is_numeral(a.ctx, a.as_ast()) 3563 def BV2Int(a, is_signed=False): 3564 """Return the Z3 expression
BV2Int(a).
3572 >>> x >
BV2Int(b, is_signed=
False)
3574 >>> x >
BV2Int(b, is_signed=
True)
3580 _z3_assert(is_bv(a), "Z3 bit-vector expression expected") 3582 ## investigate problem with bv2int 3583 return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx) 3585 def Int2BV(a, num_bits): 3586 """Return the z3 expression
Int2BV(a, num_bits).
3587 It
is a bit-vector of width num_bits
and represents the
3588 modulo of a by 2^num_bits
3591 return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx) 3593 def BitVecSort(sz, ctx=None): 3594 """Return a Z3 bit-vector sort of the given size. If `ctx=
None`, then the
global context
is used.
3600 >>> x =
Const(
'x', Byte)
3605 return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx) 3607 def BitVecVal(val, bv, ctx=None): 3608 """Return a bit-vector value with the given number of bits. If `ctx=
None`, then the
global context
is used.
3613 >>> print(
"0x%.8x" % v.as_long())
3618 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx) 3621 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx) 3623 def BitVec(name, bv, ctx=None): 3624 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3625 If `ctx=
None`, then the
global context
is used.
3635 >>> x2 =
BitVec(
'x', word)
3639 if isinstance(bv, BitVecSortRef): 3643 bv = BitVecSort(bv, ctx) 3644 return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx) 3646 def BitVecs(names, bv, ctx=None): 3647 """Return a tuple of bit-vector constants of size bv.
3649 >>> x, y, z =
BitVecs(
'x y z', 16)
3662 if isinstance(names, str): 3663 names = names.split(" ") 3664 return [BitVec(name, bv, ctx) for name in names] 3667 """Create a Z3 bit-vector concatenation expression.
3677 args = _get_args(args) 3680 _z3_assert(sz >= 2, "At least two arguments expected.") 3687 if is_seq(args[0]) or isinstance(args[0], str): 3688 args = [_coerce_seq(s, ctx) for s in args] 3690 _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") 3693 v[i] = args[i].as_ast() 3694 return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) 3698 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 3701 v[i] = args[i].as_ast() 3702 return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx) 3705 _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") 3707 for i in range(sz - 1): 3708 r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx) 3711 def Extract(high, low, a): 3712 """Create a Z3 bit-vector extraction expression,
or create a string extraction expression.
3722 if isinstance(high, str): 3723 high = StringVal(high) 3726 offset, length = _coerce_exprs(low, a, s.ctx) 3727 return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) 3729 _z3_assert(low <= high, "First argument must be greater than or equal to second argument") 3730 _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers") 3731 _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression") 3732 return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx) 3734 def _check_bv_args(a, b): 3736 _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression") 3739 """Create the Z3 expression (unsigned) `other <= self`.
3741 Use the operator <=
for signed less than
or equal to.
3746 >>> (x <= y).sexpr()
3748 >>>
ULE(x, y).sexpr()
3751 _check_bv_args(a, b) 3752 a, b = _coerce_exprs(a, b) 3753 return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3756 """Create the Z3 expression (unsigned) `other < self`.
3758 Use the operator <
for signed less than.
3765 >>>
ULT(x, y).sexpr()
3768 _check_bv_args(a, b) 3769 a, b = _coerce_exprs(a, b) 3770 return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3773 """Create the Z3 expression (unsigned) `other >= self`.
3775 Use the operator >=
for signed greater than
or equal to.
3780 >>> (x >= y).sexpr()
3782 >>>
UGE(x, y).sexpr()
3785 _check_bv_args(a, b) 3786 a, b = _coerce_exprs(a, b) 3787 return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3790 """Create the Z3 expression (unsigned) `other > self`.
3792 Use the operator >
for signed greater than.
3799 >>>
UGT(x, y).sexpr()
3802 _check_bv_args(a, b) 3803 a, b = _coerce_exprs(a, b) 3804 return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3807 """Create the Z3 expression (unsigned) division `self / other`.
3809 Use the operator /
for signed division.
3815 >>>
UDiv(x, y).sort()
3819 >>>
UDiv(x, y).sexpr()
3822 _check_bv_args(a, b) 3823 a, b = _coerce_exprs(a, b) 3824 return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3827 """Create the Z3 expression (unsigned) remainder `self % other`.
3829 Use the operator %
for signed modulus,
and SRem()
for signed remainder.
3835 >>>
URem(x, y).sort()
3839 >>>
URem(x, y).sexpr()
3842 _check_bv_args(a, b) 3843 a, b = _coerce_exprs(a, b) 3844 return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3847 """Create the Z3 expression signed remainder.
3849 Use the operator %
for signed modulus,
and URem()
for unsigned remainder.
3855 >>>
SRem(x, y).sort()
3859 >>>
SRem(x, y).sexpr()
3862 _check_bv_args(a, b) 3863 a, b = _coerce_exprs(a, b) 3864 return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3867 """Create the Z3 expression logical right shift.
3869 Use the operator >>
for the arithmetical right shift.
3874 >>> (x >> y).sexpr()
3876 >>>
LShR(x, y).sexpr()
3893 _check_bv_args(a, b) 3894 a, b = _coerce_exprs(a, b) 3895 return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3897 def RotateLeft(a, b): 3898 """Return an expression representing `a` rotated to the left `b` times.
3908 _check_bv_args(a, b) 3909 a, b = _coerce_exprs(a, b) 3910 return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3912 def RotateRight(a, b): 3913 """Return an expression representing `a` rotated to the right `b` times.
3923 _check_bv_args(a, b) 3924 a, b = _coerce_exprs(a, b) 3925 return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3928 """Return a bit-vector expression with `n` extra sign-bits.
3948 >>> print(
"%.x" % v.as_long())
3952 _z3_assert(_is_int(n), "First argument must be an integer") 3953 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 3954 return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 3957 """Return a bit-vector expression with `n` extra zero-bits.
3979 _z3_assert(_is_int(n), "First argument must be an integer") 3980 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 3981 return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 3983 def RepeatBitVec(n, a): 3984 """Return an expression representing `n` copies of `a`.
3993 >>> print(
"%.x" % v0.as_long())
3998 >>> print(
"%.x" % v.as_long())
4002 _z3_assert(_is_int(n), "First argument must be an integer") 4003 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 4004 return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx) 4007 """Return the reduction-
and expression of `a`.
""" 4009 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 4010 return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) 4013 """Return the reduction-
or expression of `a`.
""" 4015 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 4016 return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) 4018 def BVAddNoOverflow(a, b, signed): 4019 """A predicate the determines that bit-vector addition does
not overflow
""" 4020 _check_bv_args(a, b) 4021 a, b = _coerce_exprs(a, b) 4022 return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4024 def BVAddNoUnderflow(a, b): 4025 """A predicate the determines that signed bit-vector addition does
not underflow
""" 4026 _check_bv_args(a, b) 4027 a, b = _coerce_exprs(a, b) 4028 return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4030 def BVSubNoOverflow(a, b): 4031 """A predicate the determines that bit-vector subtraction does
not overflow
""" 4032 _check_bv_args(a, b) 4033 a, b = _coerce_exprs(a, b) 4034 return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4037 def BVSubNoUnderflow(a, b, signed): 4038 """A predicate the determines that bit-vector subtraction does
not underflow
""" 4039 _check_bv_args(a, b) 4040 a, b = _coerce_exprs(a, b) 4041 return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4043 def BVSDivNoOverflow(a, b): 4044 """A predicate the determines that bit-vector signed division does
not overflow
""" 4045 _check_bv_args(a, b) 4046 a, b = _coerce_exprs(a, b) 4047 return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4049 def BVSNegNoOverflow(a): 4050 """A predicate the determines that bit-vector unary negation does
not overflow
""" 4052 _z3_assert(is_bv(a), "Argument should be a bit-vector") 4053 return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx) 4055 def BVMulNoOverflow(a, b, signed): 4056 """A predicate the determines that bit-vector multiplication does
not overflow
""" 4057 _check_bv_args(a, b) 4058 a, b = _coerce_exprs(a, b) 4059 return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4062 def BVMulNoUnderflow(a, b): 4063 """A predicate the determines that bit-vector signed multiplication does
not underflow
""" 4064 _check_bv_args(a, b) 4065 a, b = _coerce_exprs(a, b) 4066 return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4070 ######################################### 4074 ######################################### 4076 class ArraySortRef(SortRef): 4080 """Return the domain of the array sort `self`.
4086 return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx) 4089 """Return the range of the array sort `self`.
4095 return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx) 4097 class ArrayRef(ExprRef): 4098 """Array expressions.
""" 4101 """Return the array sort of the array expression `self`.
4107 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4116 return self.sort().domain() 4125 return self.sort().range() 4127 def __getitem__(self, arg): 4128 """Return the Z3 expression `self[arg]`.
4137 arg = self.domain().cast(arg) 4138 return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx) 4141 return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx) 4145 """Return `
True`
if `a`
is a Z3 array expression.
4155 return isinstance(a, ArrayRef) 4157 def is_const_array(a): 4158 """Return `
True`
if `a`
is a Z3 constant array.
4167 return is_app_of(a, Z3_OP_CONST_ARRAY) 4170 """Return `
True`
if `a`
is a Z3 constant array.
4179 return is_app_of(a, Z3_OP_CONST_ARRAY) 4182 """Return `
True`
if `a`
is a Z3 map array expression.
4194 return is_app_of(a, Z3_OP_ARRAY_MAP) 4197 """Return `
True`
if `a`
is a Z3 default array expression.
4202 return is_app_of(a, Z3_OP_ARRAY_DEFAULT) 4204 def get_map_func(a): 4205 """Return the function declaration associated with a Z3 map array expression.
4218 _z3_assert(is_map(a), "Z3 array map expression expected.") 4219 return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx) 4221 def ArraySort(d, r): 4222 """Return the Z3 array sort with the given domain
and range sorts.
4236 _z3_assert(is_sort(d), "Z3 sort expected") 4237 _z3_assert(is_sort(r), "Z3 sort expected") 4238 _z3_assert(d.ctx == r.ctx, "Context mismatch") 4240 return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx) 4242 def Array(name, dom, rng): 4243 """Return an array constant named `name` with the given domain
and range sorts.
4251 s = ArraySort(dom, rng) 4253 return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx) 4255 def Update(a, i, v): 4256 """Return a Z3 store array expression.
4259 >>> i, v =
Ints(
'i v')
4263 >>>
prove(s[i] == v)
4270 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4271 i = a.domain().cast(i) 4272 v = a.range().cast(v) 4274 return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx) 4277 """ Return a default value
for array expression.
4283 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4288 """Return a Z3 store array expression.
4291 >>> i, v =
Ints(
'i v')
4292 >>> s =
Store(a, i, v)
4295 >>>
prove(s[i] == v)
4301 return Update(a, i, v) 4304 """Return a Z3 select array expression.
4314 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4319 """Return a Z3 map array expression.
4324 >>> b =
Map(f, a1, a2)
4327 >>>
prove(b[0] == f(a1[0], a2[0]))
4330 args = _get_args(args) 4332 _z3_assert(len(args) > 0, "At least one Z3 array expression expected") 4333 _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration") 4334 _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected") 4335 _z3_assert(len(args) == f.arity(), "Number of arguments mismatch") 4336 _args, sz = _to_ast_array(args) 4338 return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx) 4341 """Return a Z3 constant array expression.
4355 _z3_assert(is_sort(dom), "Z3 sort expected") 4358 v = _py2expr(v, ctx) 4359 return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx) 4362 """Return extensionality index
for arrays.
4365 _z3_assert(is_array(a) and is_array(b)) 4366 return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast())); 4369 """Return `
True`
if `a`
is a Z3 array select application.
4378 return is_app_of(a, Z3_OP_SELECT) 4381 """Return `
True`
if `a`
is a Z3 array store application.
4389 return is_app_of(a, Z3_OP_STORE) 4391 ######################################### 4395 ######################################### 4397 def _valid_accessor(acc): 4398 """Return `
True`
if acc
is pair of the form (String, Datatype
or Sort).
""" 4399 return isinstance(acc, tuple) and len(acc) == 2 and isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1])) 4402 """Helper
class for declaring Z3 datatypes.
4405 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4406 >>> List.declare(
'nil')
4407 >>> List = List.create()
4411 >>> List.cons(10, List.nil)
4413 >>> List.cons(10, List.nil).sort()
4415 >>> cons = List.cons
4419 >>> n = cons(1, cons(0, nil))
4421 cons(1, cons(0, nil))
4427 def __init__(self, name, ctx=None): 4428 self.ctx = _get_ctx(ctx) 4430 self.constructors = [] 4432 def __deepcopy__(self, memo={}): 4433 r = Datatype(self.name, self.ctx) 4434 r.constructors = copy.deepcopy(self.constructors) 4437 def declare_core(self, name, rec_name, *args): 4439 _z3_assert(isinstance(name, str), "String expected") 4440 _z3_assert(isinstance(rec_name, str), "String expected") 4441 _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)") 4442 self.constructors.append((name, rec_name, args)) 4444 def declare(self, name, *args): 4445 """Declare constructor named `name` with the given accessors `args`.
4446 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.
4448 In the following example `List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))`
4449 declares the constructor named `cons` that builds a new List using an integer
and a List.
4450 It also declares the accessors `car`
and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
4451 and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method
create() to create
4452 the actual datatype
in Z3.
4455 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4456 >>> List.declare(
'nil')
4457 >>> List = List.create()
4460 _z3_assert(isinstance(name, str), "String expected") 4461 _z3_assert(name != "", "Constructor name cannot be empty") 4462 return self.declare_core(name, "is-" + name, *args) 4465 return "Datatype(%s, %s)" % (self.name, self.constructors) 4468 """Create a Z3 datatype based on the constructors declared using the method `
declare()`.
4470 The function `
CreateDatatypes()` must be used to define mutually recursive datatypes.
4473 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4474 >>> List.declare(
'nil')
4475 >>> List = List.create()
4478 >>> List.cons(10, List.nil)
4481 return CreateDatatypes([self])[0] 4483 class ScopedConstructor: 4484 """Auxiliary object used to create Z3 datatypes.
""" 4485 def __init__(self, c, ctx): 4489 if self.ctx.ref() is not None: 4490 Z3_del_constructor(self.ctx.ref(), self.c) 4492 class ScopedConstructorList: 4493 """Auxiliary object used to create Z3 datatypes.
""" 4494 def __init__(self, c, ctx): 4498 if self.ctx.ref() is not None: 4499 Z3_del_constructor_list(self.ctx.ref(), self.c) 4501 def CreateDatatypes(*ds): 4502 """Create mutually recursive Z3 datatypes using 1
or more Datatype helper objects.
4504 In the following example we define a Tree-List using two mutually recursive datatypes.
4506 >>> TreeList =
Datatype(
'TreeList')
4509 >>> Tree.declare(
'leaf', (
'val',
IntSort()))
4511 >>> Tree.declare(
'node', (
'children', TreeList))
4512 >>> TreeList.declare(
'nil')
4513 >>> TreeList.declare(
'cons', (
'car', Tree), (
'cdr', TreeList))
4515 >>> Tree.val(Tree.leaf(10))
4517 >>>
simplify(Tree.val(Tree.leaf(10)))
4519 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4521 node(cons(leaf(10), cons(leaf(20), nil)))
4522 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4525 >>>
simplify(TreeList.car(Tree.children(n2)) == n1)
4530 _z3_assert(len(ds) > 0, "At least one Datatype must be specified") 4531 _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes") 4532 _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch") 4533 _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected") 4536 names = (Symbol * num)() 4537 out = (Sort * num)() 4538 clists = (ConstructorList * num)() 4540 for i in range(num): 4542 names[i] = to_symbol(d.name, ctx) 4543 num_cs = len(d.constructors) 4544 cs = (Constructor * num_cs)() 4545 for j in range(num_cs): 4546 c = d.constructors[j] 4547 cname = to_symbol(c[0], ctx) 4548 rname = to_symbol(c[1], ctx) 4551 fnames = (Symbol * num_fs)() 4552 sorts = (Sort * num_fs)() 4553 refs = (ctypes.c_uint * num_fs)() 4554 for k in range(num_fs): 4557 fnames[k] = to_symbol(fname, ctx) 4558 if isinstance(ftype, Datatype): 4560 _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected") 4562 refs[k] = ds.index(ftype) 4565 _z3_assert(is_sort(ftype), "Z3 sort expected") 4566 sorts[k] = ftype.ast 4568 cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs) 4569 to_delete.append(ScopedConstructor(cs[j], ctx)) 4570 clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs) 4571 to_delete.append(ScopedConstructorList(clists[i], ctx)) 4572 Z3_mk_datatypes(ctx.ref(), num, names, out, clists) 4574 ## Create a field for every constructor, recognizer and accessor 4575 for i in range(num): 4576 dref = DatatypeSortRef(out[i], ctx) 4577 num_cs = dref.num_constructors() 4578 for j in range(num_cs): 4579 cref = dref.constructor(j) 4580 cref_name = cref.name() 4581 cref_arity = cref.arity() 4582 if cref.arity() == 0: 4584 setattr(dref, cref_name, cref) 4585 rref = dref.recognizer(j) 4586 setattr(dref, "is_" + cref_name, rref) 4587 for k in range(cref_arity): 4588 aref = dref.accessor(j, k) 4589 setattr(dref, aref.name(), aref) 4591 return tuple(result) 4593 class DatatypeSortRef(SortRef): 4594 """Datatype sorts.
""" 4595 def num_constructors(self): 4596 """Return the number of constructors
in the given Z3 datatype.
4599 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4600 >>> List.declare(
'nil')
4601 >>> List = List.create()
4603 >>> List.num_constructors()
4606 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast)) 4608 def constructor(self, idx): 4609 """Return a constructor of the datatype `self`.
4612 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4613 >>> List.declare(
'nil')
4614 >>> List = List.create()
4616 >>> List.num_constructors()
4618 >>> List.constructor(0)
4620 >>> List.constructor(1)
4624 _z3_assert(idx < self.num_constructors(), "Invalid constructor index") 4625 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx) 4627 def recognizer(self, idx): 4628 """In Z3, each constructor has an associated recognizer predicate.
4630 If the constructor
is named `name`, then the recognizer `is_name`.
4633 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4634 >>> List.declare(
'nil')
4635 >>> List = List.create()
4637 >>> List.num_constructors()
4639 >>> List.recognizer(0)
4641 >>> List.recognizer(1)
4643 >>>
simplify(List.is_nil(List.cons(10, List.nil)))
4645 >>>
simplify(List.is_cons(List.cons(10, List.nil)))
4647 >>> l =
Const(
'l', List)
4652 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index") 4653 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx) 4655 def accessor(self, i, j): 4656 """In Z3, each constructor has 0
or more accessor. The number of accessors
is equal to the arity of the constructor.
4659 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4660 >>> List.declare(
'nil')
4661 >>> List = List.create()
4662 >>> List.num_constructors()
4664 >>> List.constructor(0)
4666 >>> num_accs = List.constructor(0).arity()
4669 >>> List.accessor(0, 0)
4671 >>> List.accessor(0, 1)
4673 >>> List.constructor(1)
4675 >>> num_accs = List.constructor(1).arity()
4680 _z3_assert(i < self.num_constructors(), "Invalid constructor index") 4681 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index") 4682 return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx) 4684 class DatatypeRef(ExprRef): 4685 """Datatype expressions.
""" 4687 """Return the datatype sort of the datatype expression `self`.
""" 4688 return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4690 def EnumSort(name, values, ctx=None): 4691 """Return a new enumeration sort named `name` containing the given values.
4693 The result
is a pair (sort, list of constants).
4695 >>> Color, (red, green, blue) =
EnumSort(
'Color', [
'red',
'green',
'blue'])
4698 _z3_assert(isinstance(name, str), "Name must be a string") 4699 _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings") 4700 _z3_assert(len(values) > 0, "At least one value expected") 4703 _val_names = (Symbol * num)() 4704 for i in range(num): 4705 _val_names[i] = to_symbol(values[i]) 4706 _values = (FuncDecl * num)() 4707 _testers = (FuncDecl * num)() 4708 name = to_symbol(name) 4709 S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx) 4711 for i in range(num): 4712 V.append(FuncDeclRef(_values[i], ctx)) 4713 V = [a() for a in V] 4716 ######################################### 4720 ######################################### 4723 """Set of parameters used to configure Solvers, Tactics
and Simplifiers
in Z3.
4725 Consider using the function `args2params` to create instances of this object.
4727 def __init__(self, ctx=None, params=None): 4728 self.ctx = _get_ctx(ctx) 4730 self.params = Z3_mk_params(self.ctx.ref()) 4732 self.params = params 4733 Z3_params_inc_ref(self.ctx.ref(), self.params) 4735 def __deepcopy__(self, memo={}): 4736 return ParamsRef(self.ctx, self.params) 4739 if self.ctx.ref() is not None: 4740 Z3_params_dec_ref(self.ctx.ref(), self.params) 4742 def set(self, name, val): 4743 """Set parameter name with value val.
""" 4745 _z3_assert(isinstance(name, str), "parameter name must be a string") 4746 name_sym = to_symbol(name, self.ctx) 4747 if isinstance(val, bool): 4748 Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val) 4750 Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val) 4751 elif isinstance(val, float): 4752 Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val) 4753 elif isinstance(val, str): 4754 Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx)) 4757 _z3_assert(False, "invalid parameter value") 4760 return Z3_params_to_string(self.ctx.ref(), self.params) 4762 def validate(self, ds): 4763 _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected") 4764 Z3_params_validate(self.ctx.ref(), self.params, ds.descr) 4766 def args2params(arguments, keywords, ctx=None): 4767 """Convert python arguments into a Z3_params object.
4768 A
':' is added to the keywords,
and '_' is replaced with
'-' 4770 >>>
args2params([
'model',
True,
'relevancy', 2], {
'elim_and' :
True})
4771 (params model true relevancy 2 elim_and true)
4774 _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") 4788 class ParamDescrsRef: 4789 """Set of parameter descriptions
for Solvers, Tactics
and Simplifiers
in Z3.
4791 def __init__(self, descr, ctx=None): 4792 _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected") 4793 self.ctx = _get_ctx(ctx) 4795 Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr) 4797 def __deepcopy__(self, memo={}): 4798 return ParamsDescrsRef(self.descr, self.ctx) 4801 if self.ctx.ref() is not None: 4802 Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr) 4805 """Return the size of
in the parameter description `self`.
4807 return int(Z3_param_descrs_size(self.ctx.ref(), self.descr)) 4810 """Return the size of
in the parameter description `self`.
4814 def get_name(self, i): 4815 """Return the i-th parameter name
in the parameter description `self`.
4817 return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i)) 4819 def get_kind(self, n): 4820 """Return the kind of the parameter named `n`.
4822 return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 4824 def get_documentation(self, n): 4825 """Return the documentation string of the parameter named `n`.
4827 return Z3_param_descrs_get_documentation(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 4829 def __getitem__(self, arg): 4831 return self.get_name(arg) 4833 return self.get_kind(arg) 4836 return Z3_param_descrs_to_string(self.ctx.ref(), self.descr) 4838 ######################################### 4842 ######################################### 4844 class Goal(Z3PPObject): 4845 """Goal
is a collection of constraints we want to find a solution
or show to be unsatisfiable (infeasible).
4847 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
4848 A goal has a solution
if one of its subgoals has a solution.
4849 A goal
is unsatisfiable
if all subgoals are unsatisfiable.
4852 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None): 4854 _z3_assert(goal is None or ctx is not None, "If goal is different from None, then ctx must be also different from None") 4855 self.ctx = _get_ctx(ctx) 4857 if self.goal is None: 4858 self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs) 4859 Z3_goal_inc_ref(self.ctx.ref(), self.goal) 4861 def __deepcopy__(self, memo={}): 4862 return Goal(False, False, False, self.ctx, self.goal) 4865 if self.goal is not None and self.ctx.ref() is not None: 4866 Z3_goal_dec_ref(self.ctx.ref(), self.goal) 4869 """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
4871 >>> x, y =
Ints(
'x y')
4873 >>> g.add(x == 0, y >= x + 1)
4876 >>> r =
Then(
'simplify',
'solve-eqs')(g)
4883 return int(Z3_goal_depth(self.ctx.ref(), self.goal)) 4885 def inconsistent(self): 4886 """Return `
True`
if `self` contains the `
False` constraints.
4888 >>> x, y =
Ints(
'x y')
4890 >>> g.inconsistent()
4892 >>> g.add(x == 0, x == 1)
4895 >>> g.inconsistent()
4897 >>> g2 =
Tactic(
'propagate-values')(g)[0]
4898 >>> g2.inconsistent()
4901 return Z3_goal_inconsistent(self.ctx.ref(), self.goal) 4904 """Return the precision (under-approximation, over-approximation,
or precise) of the goal `self`.
4907 >>> g.prec() == Z3_GOAL_PRECISE
4909 >>> x, y =
Ints(
'x y')
4910 >>> g.add(x == y + 1)
4911 >>> g.prec() == Z3_GOAL_PRECISE
4913 >>> t =
With(
Tactic(
'add-bounds'), add_bound_lower=0, add_bound_upper=10)
4916 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
4917 >>> g2.prec() == Z3_GOAL_PRECISE
4919 >>> g2.prec() == Z3_GOAL_UNDER
4922 return Z3_goal_precision(self.ctx.ref(), self.goal) 4924 def precision(self): 4925 """Alias
for `
prec()`.
4928 >>> g.precision() == Z3_GOAL_PRECISE
4934 """Return the number of constraints
in the goal `self`.
4939 >>> x, y =
Ints(
'x y')
4940 >>> g.add(x == 0, y > x)
4944 return int(Z3_goal_size(self.ctx.ref(), self.goal)) 4947 """Return the number of constraints
in the goal `self`.
4952 >>> x, y =
Ints(
'x y')
4953 >>> g.add(x == 0, y > x)
4960 """Return a constraint
in the goal `self`.
4963 >>> x, y =
Ints(
'x y')
4964 >>> g.add(x == 0, y > x)
4970 return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx) 4972 def __getitem__(self, arg): 4973 """Return a constraint
in the goal `self`.
4976 >>> x, y =
Ints(
'x y')
4977 >>> g.add(x == 0, y > x)
4983 if arg >= len(self): 4985 return self.get(arg) 4987 def assert_exprs(self, *args): 4988 """Assert constraints into the goal.
4992 >>> g.assert_exprs(x > 0, x < 2)
4996 args = _get_args(args) 4997 s = BoolSort(self.ctx) 5000 Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast()) 5002 def append(self, *args): 5007 >>> g.append(x > 0, x < 2)
5011 self.assert_exprs(*args) 5013 def insert(self, *args): 5018 >>> g.insert(x > 0, x < 2)
5022 self.assert_exprs(*args) 5024 def add(self, *args): 5029 >>> g.add(x > 0, x < 2)
5033 self.assert_exprs(*args) 5036 return obj_to_string(self) 5039 """Return a textual representation of the s-expression representing the goal.
""" 5040 return Z3_goal_to_string(self.ctx.ref(), self.goal) 5042 def translate(self, target): 5043 """Copy goal `self` to context `target`.
5051 >>> g2 = g.translate(c2)
5062 _z3_assert(isinstance(target, Context), "target must be a context") 5063 return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target) 5066 return self.translate(self.ctx) 5068 def __deepcopy__(self): 5069 return self.translate(self.ctx) 5071 def simplify(self, *arguments, **keywords): 5072 """Return a new simplified goal.
5074 This method
is essentially invoking the simplify tactic.
5078 >>> g.add(x + 1 >= 2)
5081 >>> g2 = g.simplify()
5088 t = Tactic('simplify') 5089 return t.apply(self, *arguments, **keywords)[0] 5092 """Return goal `self`
as a single Z3 expression.
5107 return BoolVal(True, self.ctx) 5111 return And([ self.get(i) for i in range(len(self)) ], self.ctx) 5113 ######################################### 5117 ######################################### 5118 class AstVector(Z3PPObject): 5119 """A collection (vector) of ASTs.
""" 5121 def __init__(self, v=None, ctx=None): 5124 self.ctx = _get_ctx(ctx) 5125 self.vector = Z3_mk_ast_vector(self.ctx.ref()) 5128 assert ctx is not None 5130 Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector) 5132 def __deepcopy__(self, memo={}): 5133 return AstVector(self.vector, self.ctx) 5136 if self.vector is not None and self.ctx.ref() is not None: 5137 Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector) 5140 """Return the size of the vector `self`.
5145 >>> A.push(
Int(
'x'))
5146 >>> A.push(
Int(
'x'))
5150 return int(Z3_ast_vector_size(self.ctx.ref(), self.vector)) 5152 def __getitem__(self, i): 5153 """Return the AST at position `i`.
5156 >>> A.push(
Int(
'x') + 1)
5157 >>> A.push(
Int(
'y'))
5164 if isinstance(i, int): 5168 if i >= self.__len__(): 5170 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx) 5172 elif isinstance(i, slice): 5173 return [_to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, ii), self.ctx) for ii in range(*i.indices(self.__len__()))] 5176 def __setitem__(self, i, v): 5177 """Update AST at position `i`.
5180 >>> A.push(
Int(
'x') + 1)
5181 >>> A.push(
Int(
'y'))
5188 if i >= self.__len__(): 5190 Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast()) 5193 """Add `v`
in the end of the vector.
5198 >>> A.push(
Int(
'x'))
5202 Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast()) 5204 def resize(self, sz): 5205 """Resize the vector to `sz` elements.
5211 >>>
for i
in range(10): A[i] =
Int(
'x')
5215 Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz) 5217 def __contains__(self, item): 5218 """Return `
True`
if the vector contains `item`.
5240 def translate(self, other_ctx): 5241 """Copy vector `self` to context `other_ctx`.
5247 >>> B = A.translate(c2)
5251 return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx) 5254 return self.translate(self.ctx) 5256 def __deepcopy__(self): 5257 return self.translate(self.ctx) 5260 return obj_to_string(self) 5263 """Return a textual representation of the s-expression representing the vector.
""" 5264 return Z3_ast_vector_to_string(self.ctx.ref(), self.vector) 5266 ######################################### 5270 ######################################### 5272 """A mapping
from ASTs to ASTs.
""" 5274 def __init__(self, m=None, ctx=None): 5277 self.ctx = _get_ctx(ctx) 5278 self.map = Z3_mk_ast_map(self.ctx.ref()) 5281 assert ctx is not None 5283 Z3_ast_map_inc_ref(self.ctx.ref(), self.map) 5285 def __deepcopy__(self, memo={}): 5286 return AstMap(self.map, self.ctx) 5289 if self.map is not None and self.ctx.ref() is not None: 5290 Z3_ast_map_dec_ref(self.ctx.ref(), self.map) 5293 """Return the size of the map.
5303 return int(Z3_ast_map_size(self.ctx.ref(), self.map)) 5305 def __contains__(self, key): 5306 """Return `
True`
if the map contains key `key`.
5316 return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast()) 5318 def __getitem__(self, key): 5319 """Retrieve the value associated with key `key`.
5327 return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx) 5329 def __setitem__(self, k, v): 5330 """Add/Update key `k` with value `v`.
5343 Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast()) 5346 return Z3_ast_map_to_string(self.ctx.ref(), self.map) 5349 """Remove the entry associated with key `k`.
5360 Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast()) 5363 """Remove all entries
from the map.
5375 Z3_ast_map_reset(self.ctx.ref(), self.map) 5378 """Return an AstVector containing all keys
in the map.
5387 return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx) 5389 ######################################### 5393 ######################################### 5396 """Store the value of the interpretation of a function
in a particular point.
""" 5398 def __init__(self, entry, ctx): 5401 Z3_func_entry_inc_ref(self.ctx.ref(), self.entry) 5403 def __deepcopy__(self, memo={}): 5404 return FuncEntry(self.entry, self.ctx) 5407 if self.ctx.ref() is not None: 5408 Z3_func_entry_dec_ref(self.ctx.ref(), self.entry) 5411 """Return the number of arguments
in the given entry.
5415 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5420 >>> f_i.num_entries()
5422 >>> e = f_i.entry(0)
5426 return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry)) 5428 def arg_value(self, idx): 5429 """Return the value of argument `idx`.
5433 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5438 >>> f_i.num_entries()
5440 >>> e = f_i.entry(0)
5451 ...
except IndexError:
5452 ... print(
"index error")
5455 if idx >= self.num_args(): 5457 return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx) 5460 """Return the value of the function at point `self`.
5464 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5469 >>> f_i.num_entries()
5471 >>> e = f_i.entry(0)
5479 return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx) 5482 """Return entry `self`
as a Python list.
5485 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5490 >>> f_i.num_entries()
5492 >>> e = f_i.entry(0)
5496 args = [ self.arg_value(i) for i in range(self.num_args())] 5497 args.append(self.value()) 5501 return repr(self.as_list()) 5503 class FuncInterp(Z3PPObject): 5504 """Stores the interpretation of a function
in a Z3 model.
""" 5506 def __init__(self, f, ctx): 5509 if self.f is not None: 5510 Z3_func_interp_inc_ref(self.ctx.ref(), self.f) 5512 def __deepcopy__(self, memo={}): 5513 return FuncInterp(self.f, self.ctx) 5516 if self.f is not None and self.ctx.ref() is not None: 5517 Z3_func_interp_dec_ref(self.ctx.ref(), self.f) 5519 def else_value(self): 5521 Return the `
else` value
for a function interpretation.
5522 Return
None if Z3 did
not specify the `
else` value
for 5527 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5532 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5536 r = Z3_func_interp_get_else(self.ctx.ref(), self.f) 5538 return _to_expr_ref(r, self.ctx) 5542 def num_entries(self): 5543 """Return the number of entries/points
in the function interpretation `self`.
5547 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5552 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5556 return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f)) 5559 """Return the number of arguments
for each entry
in the function interpretation `self`.
5563 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5570 return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f)) 5572 def entry(self, idx): 5573 """Return an entry at position `idx < self.
num_entries()`
in the function interpretation `self`.
5577 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5582 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5592 if idx >= self.num_entries(): 5594 return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx) 5596 def translate(self, other_ctx): 5597 """Copy model
'self' to context
'other_ctx'.
5599 return ModelRef(Z3_model_translate(self.ctx.ref(), self.model, other_ctx.ref()), other_ctx) 5602 return self.translate(self.ctx) 5604 def __deepcopy__(self): 5605 return self.translate(self.ctx) 5608 """Return the function interpretation
as a Python list.
5611 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5616 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5618 [[0, 1], [1, 1], [2, 0], 1]
5620 r = [ self.entry(i).as_list() for i in range(self.num_entries())] 5621 r.append(self.else_value()) 5625 return obj_to_string(self) 5627 class ModelRef(Z3PPObject): 5628 """Model/Solution of a satisfiability problem (aka system of constraints).
""" 5630 def __init__(self, m, ctx): 5631 assert ctx is not None 5634 Z3_model_inc_ref(self.ctx.ref(), self.model) 5637 if self.ctx.ref() is not None: 5638 Z3_model_dec_ref(self.ctx.ref(), self.model) 5641 return obj_to_string(self) 5644 """Return a textual representation of the s-expression representing the model.
""" 5645 return Z3_model_to_string(self.ctx.ref(), self.model) 5647 def eval(self, t, model_completion=False): 5648 """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`.
5652 >>> s.add(x > 0, x < 2)
5665 >>> m.eval(y, model_completion=
True)
5672 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r): 5673 return _to_expr_ref(r[0], self.ctx) 5674 raise Z3Exception("failed to evaluate expression in the model") 5676 def evaluate(self, t, model_completion=False): 5677 """Alias
for `eval`.
5681 >>> s.add(x > 0, x < 2)
5685 >>> m.evaluate(x + 1)
5687 >>> m.evaluate(x == 1)
5690 >>> m.evaluate(y + x)
5694 >>> m.evaluate(y, model_completion=
True)
5697 >>> m.evaluate(y + x)
5700 return self.eval(t, model_completion) 5703 """Return the number of constant
and function declarations
in the model `self`.
5708 >>> s.add(x > 0, f(x) != x)
5715 return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model)) 5717 def get_interp(self, decl): 5718 """Return the interpretation
for a given declaration
or constant.
5723 >>> s.add(x > 0, x < 2, f(x) == 0)
5733 _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected") 5737 if decl.arity() == 0: 5738 _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast) 5739 if _r.value is None: 5741 r = _to_expr_ref(_r, self.ctx) 5743 return self.get_interp(get_as_array_func(r)) 5747 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) 5751 def num_sorts(self): 5752 """Return the number of uninterpreted sorts that contain an interpretation
in the model `self`.
5755 >>> a, b =
Consts(
'a b', A)
5764 return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model)) 5766 def get_sort(self, idx): 5767 """Return the uninterpreted sort at position `idx` < self.
num_sorts().
5771 >>> a1, a2 =
Consts(
'a1 a2', A)
5772 >>> b1, b2 =
Consts(
'b1 b2', B)
5774 >>> s.add(a1 != a2, b1 != b2)
5785 if idx >= self.num_sorts(): 5787 return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx) 5790 """Return all uninterpreted sorts that have an interpretation
in the model `self`.
5794 >>> a1, a2 =
Consts(
'a1 a2', A)
5795 >>> b1, b2 =
Consts(
'b1 b2', B)
5797 >>> s.add(a1 != a2, b1 != b2)
5804 return [ self.get_sort(i) for i in range(self.num_sorts()) ] 5806 def get_universe(self, s): 5807 """Return the interpretation
for the uninterpreted sort `s`
in the model `self`.
5810 >>> a, b =
Consts(
'a b', A)
5816 >>> m.get_universe(A)
5820 _z3_assert(isinstance(s, SortRef), "Z3 sort expected") 5822 return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx) 5826 def __getitem__(self, idx): 5827 """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.
5829 The elements can be retrieved using position
or the actual declaration.
5834 >>> s.add(x > 0, x < 2, f(x) == 0)
5848 >>>
for d
in m: print(
"%s -> %s" % (d, m[d]))
5850 f -> [1 -> 0,
else -> 0]
5853 if idx >= len(self): 5855 num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model) 5856 if (idx < num_consts): 5857 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx) 5859 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx) 5860 if isinstance(idx, FuncDeclRef): 5861 return self.get_interp(idx) 5863 return self.get_interp(idx.decl()) 5864 if isinstance(idx, SortRef): 5865 return self.get_universe(idx) 5867 _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected") 5871 """Return a list with all symbols that have an interpretation
in the model `self`.
5875 >>> s.add(x > 0, x < 2, f(x) == 0)
5883 for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)): 5884 r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx)) 5885 for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)): 5886 r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx)) 5889 def translate(self, target): 5890 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
5893 _z3_assert(isinstance(target, Context), "argument must be a Z3 context") 5894 model = Z3_model_translate(self.ctx.ref(), self.model, target.ref()) 5895 return Model(model, target) 5898 return self.translate(self.ctx) 5900 def __deepcopy__(self): 5901 return self.translate(self.ctx) 5904 """Return true
if n
is a Z3 expression of the form (_
as-array f).
""" 5905 return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast()) 5907 def get_as_array_func(n): 5908 """Return the function declaration f associated with a Z3 expression of the form (_
as-array f).
""" 5910 _z3_assert(is_as_array(n), "as-array Z3 expression expected.") 5911 return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx) 5913 ######################################### 5917 ######################################### 5919 """Statistics
for `Solver.check()`.
""" 5921 def __init__(self, stats, ctx): 5924 Z3_stats_inc_ref(self.ctx.ref(), self.stats) 5926 def __deepcopy__(self, memo={}): 5927 return Statistics(self.stats, self.ctx) 5930 if self.ctx.ref() is not None: 5931 Z3_stats_dec_ref(self.ctx.ref(), self.stats) 5937 out.write(u('<table border="1" cellpadding="2" cellspacing="0">')) 5940 out.write(u('<tr style="background-color:#CFCFCF">')) 5943 out.write(u('<tr>')) 5945 out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v))) 5946 out.write(u('</table>')) 5947 return out.getvalue() 5949 return Z3_stats_to_string(self.ctx.ref(), self.stats) 5952 """Return the number of statistical counters.
5955 >>> s =
Then(
'simplify',
'nlsat').solver()
5959 >>> st = s.statistics()
5963 return int(Z3_stats_size(self.ctx.ref(), self.stats)) 5965 def __getitem__(self, idx): 5966 """Return the value of statistical counter at position `idx`. The result
is a pair (key, value).
5969 >>> s =
Then(
'simplify',
'nlsat').solver()
5973 >>> st = s.statistics()
5977 (
'nlsat propagations', 2)
5981 if idx >= len(self): 5983 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 5984 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 5986 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 5987 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val) 5990 """Return the list of statistical counters.
5993 >>> s =
Then(
'simplify',
'nlsat').solver()
5997 >>> st = s.statistics()
5999 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))] 6001 def get_key_value(self, key): 6002 """Return the value of a particular statistical counter.
6005 >>> s =
Then(
'simplify',
'nlsat').solver()
6009 >>> st = s.statistics()
6010 >>> st.get_key_value(
'nlsat propagations')
6013 for idx in range(len(self)): 6014 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx): 6015 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 6016 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 6018 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 6019 raise Z3Exception("unknown key") 6021 def __getattr__(self, name): 6022 """Access the value of statistical using attributes.
6024 Remark: to access a counter containing blank spaces (e.g.,
'nlsat propagations'),
6025 we should use
'_' (e.g.,
'nlsat_propagations').
6028 >>> s =
Then(
'simplify',
'nlsat').solver()
6032 >>> st = s.statistics()
6033 >>> st.nlsat_propagations
6038 key = name.replace('_', ' ') 6040 return self.get_key_value(key) 6042 raise AttributeError 6044 ######################################### 6048 ######################################### 6049 class CheckSatResult: 6050 """Represents the result of a satisfiability check: sat, unsat, unknown.
6056 >>> isinstance(r, CheckSatResult)
6060 def __init__(self, r): 6063 def __deepcopy__(self, memo={}): 6064 return CheckSatResult(self.r) 6066 def __eq__(self, other): 6067 return isinstance(other, CheckSatResult) and self.r == other.r 6069 def __ne__(self, other): 6070 return not self.__eq__(other) 6074 if self.r == Z3_L_TRUE: 6076 elif self.r == Z3_L_FALSE: 6077 return "<b>unsat</b>" 6079 return "<b>unknown</b>" 6081 if self.r == Z3_L_TRUE: 6083 elif self.r == Z3_L_FALSE: 6088 sat = CheckSatResult(Z3_L_TRUE) 6089 unsat = CheckSatResult(Z3_L_FALSE) 6090 unknown = CheckSatResult(Z3_L_UNDEF) 6092 class Solver(Z3PPObject): 6093 """Solver API provides methods
for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.
""" 6095 def __init__(self, solver=None, ctx=None): 6096 assert solver is None or ctx is not None 6097 self.ctx = _get_ctx(ctx) 6100 self.solver = Z3_mk_solver(self.ctx.ref()) 6102 self.solver = solver 6103 Z3_solver_inc_ref(self.ctx.ref(), self.solver) 6106 if self.solver is not None and self.ctx.ref() is not None: 6107 Z3_solver_dec_ref(self.ctx.ref(), self.solver) 6109 def set(self, *args, **keys): 6110 """Set a configuration option. The method `
help()`
return a string containing all available options.
6114 >>> s.set(mbqi=
True)
6115 >>> s.set(
'MBQI',
True)
6116 >>> s.set(
':mbqi',
True)
6118 p = args2params(args, keys, self.ctx) 6119 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params) 6122 """Create a backtracking point.
6141 Z3_solver_push(self.ctx.ref(), self.solver) 6143 def pop(self, num=1): 6144 """Backtrack \c num backtracking points.
6163 Z3_solver_pop(self.ctx.ref(), self.solver, num) 6165 def num_scopes(self): 6166 """Return the current number of backtracking points.
6181 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver) 6184 """Remove all asserted constraints
and backtracking points created using `
push()`.
6195 Z3_solver_reset(self.ctx.ref(), self.solver) 6197 def assert_exprs(self, *args): 6198 """Assert constraints into the solver.
6202 >>> s.assert_exprs(x > 0, x < 2)
6206 args = _get_args(args) 6207 s = BoolSort(self.ctx) 6209 if isinstance(arg, Goal) or isinstance(arg, AstVector): 6211 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast()) 6214 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast()) 6216 def add(self, *args): 6217 """Assert constraints into the solver.
6221 >>> s.add(x > 0, x < 2)
6225 self.assert_exprs(*args) 6227 def __iadd__(self, fml): 6231 def append(self, *args): 6232 """Assert constraints into the solver.
6236 >>> s.append(x > 0, x < 2)
6240 self.assert_exprs(*args) 6242 def insert(self, *args): 6243 """Assert constraints into the solver.
6247 >>> s.insert(x > 0, x < 2)
6251 self.assert_exprs(*args) 6253 def assert_and_track(self, a, p): 6254 """Assert constraint `a`
and track it
in the unsat core using the Boolean constant `p`.
6256 If `p`
is a string, it will be automatically converted into a Boolean constant.
6261 >>> s.set(unsat_core=
True)
6262 >>> s.assert_and_track(x > 0,
'p1')
6263 >>> s.assert_and_track(x != 1,
'p2')
6264 >>> s.assert_and_track(x < 0, p3)
6265 >>> print(s.check())
6267 >>> c = s.unsat_core()
6277 if isinstance(p, str): 6278 p = Bool(p, self.ctx) 6279 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected") 6280 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected") 6281 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast()) 6283 def check(self, *assumptions): 6284 """Check whether the assertions
in the given solver plus the optional assumptions are consistent
or not.
6290 >>> s.add(x > 0, x < 2)
6299 >>> s.add(2**x == 4)
6303 assumptions = _get_args(assumptions) 6304 num = len(assumptions) 6305 _assumptions = (Ast * num)() 6306 for i in range(num): 6307 _assumptions[i] = assumptions[i].as_ast() 6308 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions) 6309 return CheckSatResult(r) 6312 """Return a model
for the last `
check()`.
6314 This function raises an exception
if 6315 a model
is not available (e.g., last `
check()` returned unsat).
6319 >>> s.add(a + 2 == 0)
6326 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx) 6328 raise Z3Exception("model is not available") 6330 def unsat_core(self): 6331 """Return a subset (
as an AST vector) of the assumptions provided to the last
check().
6333 These are the assumptions Z3 used
in the unsatisfiability proof.
6334 Assumptions are available
in Z3. They are used to extract unsatisfiable cores.
6335 They may be also used to
"retract" assumptions. Note that, assumptions are
not really
6336 "soft constraints", but they can be used to implement them.
6338 >>> p1, p2, p3 =
Bools(
'p1 p2 p3')
6339 >>> x, y =
Ints(
'x y')
6344 >>> s.add(
Implies(p3, y > -3))
6345 >>> s.check(p1, p2, p3)
6347 >>> core = s.unsat_core()
6360 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx) 6362 def consequences(self, assumptions, variables): 6363 """Determine fixed values
for the variables based on the solver state
and assumptions.
6365 >>> a, b, c, d =
Bools(
'a b c d')
6367 >>> s.consequences([a],[b,c,d])
6369 >>> s.consequences([
Not(c),d],[a,b,c,d])
6372 if isinstance(assumptions, list): 6373 _asms = AstVector(None, self.ctx) 6374 for a in assumptions: 6377 if isinstance(variables, list): 6378 _vars = AstVector(None, self.ctx) 6382 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected") 6383 _z3_assert(isinstance(variables, AstVector), "ast vector expected") 6384 consequences = AstVector(None, self.ctx) 6385 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector) 6386 sz = len(consequences) 6387 consequences = [ consequences[i] for i in range(sz) ] 6388 return CheckSatResult(r), consequences 6390 def from_file(self, filename): 6391 """Parse assertions
from a file
""" 6393 Z3_solver_from_file(self.ctx.ref(), self.solver, filename) 6394 except Z3Exception as e: 6395 _handle_parse_error(e, self.ctx) 6397 def from_string(self, s): 6398 """Parse assertions
from a string
""" 6400 Z3_solver_from_string(self.ctx.ref(), self.solver, s) 6401 except Z3Exception as e: 6402 _handle_parse_error(e, self.ctx) 6405 """Return a proof
for the last `
check()`. Proof construction must be enabled.
""" 6406 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx) 6408 def assertions(self): 6409 """Return an AST vector containing all added constraints.
6420 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx) 6422 def statistics(self): 6423 """Return statistics
for the last `
check()`.
6430 >>> st = s.statistics()
6431 >>> st.get_key_value(
'final checks')
6438 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx) 6440 def reason_unknown(self): 6441 """Return a string describing why the last `
check()` returned `unknown`.
6445 >>> s.add(2**x == 4)
6448 >>> s.reason_unknown()
6449 '(incomplete (theory arithmetic))' 6451 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver) 6454 """Display a string describing all available options.
""" 6455 print(Z3_solver_get_help(self.ctx.ref(), self.solver)) 6457 def param_descrs(self): 6458 """Return the parameter description set.
""" 6459 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx) 6462 """Return a formatted string with all added constraints.
""" 6463 return obj_to_string(self) 6465 def translate(self, target): 6466 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
6471 >>> s2 = s1.translate(c2)
6474 _z3_assert(isinstance(target, Context), "argument must be a Z3 context") 6475 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) 6476 return Solver(solver, target) 6479 return self.translate(self.ctx) 6481 def __deepcopy__(self): 6482 return self.translate(self.ctx) 6485 """Return a formatted string (
in Lisp-like format) with all added constraints. We say the string
is in s-expression format.
6493 return Z3_solver_to_string(self.ctx.ref(), self.solver) 6496 """return SMTLIB2 formatted benchmark
for solver
's assertions""" 6503 for i
in range(sz1):
6504 v[i] = es[i].as_ast()
6506 e = es[sz1].as_ast()
6512 """Create a solver customized for the given logic. 6514 The parameter `logic` is a string. It should be contains 6515 the name of a SMT-LIB logic. 6516 See http://www.smtlib.org/ for the name of all available logics. 6518 >>> s = SolverFor("QF_LIA") 6532 """Return a simple general purpose solver with limited amount of preprocessing. 6534 >>> s = SimpleSolver() 6550 """Fixedpoint API provides methods for solving with recursive predicates""" 6553 assert fixedpoint
is None or ctx
is not None 6556 if fixedpoint
is None:
6567 if self.
fixedpoint is not None and self.
ctx.ref()
is not None:
6571 """Set a configuration option. The method `help()` return a string containing all available options. 6577 """Display a string describing all available options.""" 6581 """Return the parameter description set.""" 6585 """Assert constraints as background axioms for the fixedpoint solver.""" 6586 args = _get_args(args)
6589 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
6599 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6607 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6611 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6615 """Assert rules defining recursive predicates to the fixedpoint solver. 6618 >>> s = Fixedpoint() 6619 >>> s.register_relation(a.decl()) 6620 >>> s.register_relation(b.decl()) 6633 body = _get_args(body)
6637 def rule(self, head, body = None, name = None):
6638 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 6642 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 6646 """Query the fixedpoint engine whether formula is derivable. 6647 You can also pass an tuple or list of recursive predicates. 6649 query = _get_args(query)
6651 if sz >= 1
and isinstance(query[0], FuncDeclRef):
6652 _decls = (FuncDecl * sz)()
6662 query =
And(query, self.
ctx)
6663 query = self.
abstract(query,
False)
6668 """Query the fixedpoint engine whether formula is derivable starting at the given query level. 6670 query = _get_args(query)
6672 if sz >= 1
and isinstance(query[0], FuncDecl):
6673 _z3_assert (
False,
"unsupported")
6679 query = self.
abstract(query,
False)
6680 r = Z3_fixedpoint_query_from_lvl (self.
ctx.ref(), self.
fixedpoint, query.as_ast(), lvl)
6684 """create a backtracking point for added rules, facts and assertions""" 6688 """restore to previously created backtracking point""" 6696 body = _get_args(body)
6701 """Retrieve answer from last query call.""" 6703 return _to_expr_ref(r, self.
ctx)
6706 """Retrieve a ground cex from last query call.""" 6707 r = Z3_fixedpoint_get_ground_sat_answer(self.
ctx.ref(), self.
fixedpoint)
6708 return _to_expr_ref(r, self.
ctx)
6711 """retrieve rules along the counterexample trace""" 6715 """retrieve rule names along the counterexample trace""" 6718 names = _symbol2py (self.
ctx, Z3_fixedpoint_get_rule_names_along_trace(self.
ctx.ref(), self.
fixedpoint))
6720 return names.split (
';')
6723 """Retrieve number of levels used for predicate in PDR engine""" 6727 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)""" 6729 return _to_expr_ref(r, self.
ctx)
6732 """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)""" 6736 """Register relation as recursive""" 6737 relations = _get_args(relations)
6742 """Control how relation is represented""" 6743 representations = _get_args(representations)
6744 representations = [
to_symbol(s)
for s
in representations]
6745 sz = len(representations)
6746 args = (Symbol * sz)()
6748 args[i] = representations[i]
6752 """Parse rules and queries from a string""" 6755 except Z3Exception
as e:
6756 _handle_parse_error(e, self.
ctx)
6759 """Parse rules and queries from a file""" 6762 except Z3Exception
as e:
6763 _handle_parse_error(e, self.
ctx)
6766 """retrieve rules that have been added to fixedpoint context""" 6770 """retrieve assertions that have been added to fixedpoint context""" 6774 """Return a formatted string with all added rules and constraints.""" 6778 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 6783 """Return a formatted string (in Lisp-like format) with all added constraints. 6784 We say the string is in s-expression format. 6785 Include also queries. 6787 args, len = _to_ast_array(queries)
6791 """Return statistics for the last `query()`. 6796 """Return a string describing why the last `query()` returned `unknown`. 6801 """Add variable or several variables. 6802 The added variable or variables will be bound in the rules 6805 vars = _get_args(vars)
6825 """Finite domain sort.""" 6828 """Return the size of the finite domain sort""" 6829 r = (ctypes.c_ulonglong * 1)()
6833 raise Z3Exception(
"Failed to retrieve finite domain sort size")
6836 """Create a named finite domain sort of a given size sz""" 6837 if not isinstance(name, Symbol):
6843 """Return True if `s` is a Z3 finite-domain sort. 6845 >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) 6847 >>> is_finite_domain_sort(IntSort()) 6850 return isinstance(s, FiniteDomainSortRef)
6854 """Finite-domain expressions.""" 6857 """Return the sort of the finite-domain expression `self`.""" 6861 """Return a Z3 floating point expression as a Python string.""" 6865 """Return `True` if `a` is a Z3 finite-domain expression. 6867 >>> s = FiniteDomainSort('S', 100) 6868 >>> b = Const('b', s) 6869 >>> is_finite_domain(b) 6871 >>> is_finite_domain(Int('x')) 6874 return isinstance(a, FiniteDomainRef)
6878 """Integer values.""" 6881 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. 6883 >>> s = FiniteDomainSort('S', 100) 6884 >>> v = FiniteDomainVal(3, s) 6893 """Return a Z3 finite-domain numeral as a Python string. 6895 >>> s = FiniteDomainSort('S', 100) 6896 >>> v = FiniteDomainVal(42, s) 6904 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. 6906 >>> s = FiniteDomainSort('S', 256) 6907 >>> FiniteDomainVal(255, s) 6909 >>> FiniteDomainVal('100', s) 6918 """Return `True` if `a` is a Z3 finite-domain value. 6920 >>> s = FiniteDomainSort('S', 100) 6921 >>> b = Const('b', s) 6922 >>> is_finite_domain_value(b) 6924 >>> b = FiniteDomainVal(10, s) 6927 >>> is_finite_domain_value(b) 6972 """Optimize API provides methods for solving using objective functions and weighted soft constraints""" 6983 if self.
optimize is not None and self.
ctx.ref()
is not None:
6987 """Set a configuration option. The method `help()` return a string containing all available options. 6993 """Display a string describing all available options.""" 6997 """Return the parameter description set.""" 7001 """Assert constraints as background axioms for the optimize solver.""" 7002 args = _get_args(args)
7004 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
7011 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr.""" 7019 """Add soft constraint with optional weight and optional identifier. 7020 If no weight is supplied, then the penalty for violating the soft constraint 7022 Soft constraints are grouped by identifiers. Soft constraints that are 7023 added without identifiers are grouped by default. 7026 weight =
"%d" % weight
7027 elif isinstance(weight, float):
7028 weight =
"%f" % weight
7029 if not isinstance(weight, str):
7030 raise Z3Exception(
"weight should be a string or an integer")
7038 """Add objective function to maximize.""" 7042 """Add objective function to minimize.""" 7046 """create a backtracking point for added rules, facts and assertions""" 7050 """restore to previously created backtracking point""" 7054 """Check satisfiability while optimizing objective functions.""" 7058 """Return a string that describes why the last `check()` returned `unknown`.""" 7062 """Return a model for the last check().""" 7066 raise Z3Exception(
"model is not available")
7069 if not isinstance(obj, OptimizeObjective):
7070 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7074 if not isinstance(obj, OptimizeObjective):
7075 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7079 if not isinstance(obj, OptimizeObjective):
7080 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7081 return obj.lower_values()
7084 if not isinstance(obj, OptimizeObjective):
7085 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7086 return obj.upper_values()
7089 """Parse assertions and objectives from a file""" 7092 except Z3Exception
as e:
7093 _handle_parse_error(e, self.
ctx)
7096 """Parse assertions and objectives from a string""" 7099 except Z3Exception
as e:
7100 _handle_parse_error(e, self.
ctx)
7103 """Return an AST vector containing all added constraints.""" 7107 """returns set of objective functions""" 7111 """Return a formatted string with all added rules and constraints.""" 7115 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 7120 """Return statistics for the last check`. 7133 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters.""" 7144 if self.
ctx.ref()
is not None:
7148 """Return the number of subgoals in `self`. 7150 >>> a, b = Ints('a b') 7152 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7153 >>> t = Tactic('split-clause') 7157 >>> t = Then(Tactic('split-clause'), Tactic('split-clause')) 7160 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values')) 7167 """Return one of the subgoals stored in ApplyResult object `self`. 7169 >>> a, b = Ints('a b') 7171 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7172 >>> t = Tactic('split-clause') 7175 [a == 0, Or(b == 0, b == 1), a > b] 7177 [a == 1, Or(b == 0, b == 1), a > b] 7179 if idx >= len(self):
7184 return obj_to_string(self)
7187 """Return a textual representation of the s-expression representing the set of subgoals in `self`.""" 7191 """Convert a model for a subgoal into a model for the original goal. 7193 >>> a, b = Ints('a b') 7195 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7196 >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs')) 7199 [Or(b == 0, b == 1), Not(0 <= b)] 7201 [Or(b == 0, b == 1), Not(1 <= b)] 7202 >>> # Remark: the subgoal r[0] is unsatisfiable 7203 >>> # Creating a solver for solving the second subgoal 7210 >>> # Model s.model() does not assign a value to `a` 7211 >>> # It is a model for subgoal `r[1]`, but not for goal `g` 7212 >>> # The method convert_model creates a model for `g` from a model for `r[1]`. 7213 >>> r.convert_model(s.model(), 1) 7217 _z3_assert(idx < len(self),
"index out of bounds")
7218 _z3_assert(isinstance(model, ModelRef),
"Z3 Model expected")
7222 """Return a Z3 expression consisting of all subgoals. 7227 >>> g.add(Or(x == 2, x == 3)) 7228 >>> r = Tactic('simplify')(g) 7230 [[Not(x <= 1), Or(x == 2, x == 3)]] 7232 And(Not(x <= 1), Or(x == 2, x == 3)) 7233 >>> r = Tactic('split-clause')(g) 7235 [[x > 1, x == 2], [x > 1, x == 3]] 7237 Or(And(x > 1, x == 2), And(x > 1, x == 3)) 7253 """Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver(). 7255 Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond(). 7260 if isinstance(tactic, TacticObj):
7264 _z3_assert(isinstance(tactic, str),
"tactic name expected")
7268 raise Z3Exception(
"unknown tactic '%s'" % tactic)
7275 if self.
tactic is not None and self.
ctx.ref()
is not None:
7279 """Create a solver using the tactic `self`. 7281 The solver supports the methods `push()` and `pop()`, but it 7282 will always solve each `check()` from scratch. 7284 >>> t = Then('simplify', 'nlsat') 7287 >>> s.add(x**2 == 2, x > 0) 7295 def apply(self, goal, *arguments, **keywords):
7296 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7298 >>> x, y = Ints('x y') 7299 >>> t = Tactic('solve-eqs') 7300 >>> t.apply(And(x == 0, y >= x + 1)) 7304 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expressions expected")
7305 goal = _to_goal(goal)
7306 if len(arguments) > 0
or len(keywords) > 0:
7313 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7315 >>> x, y = Ints('x y') 7316 >>> t = Tactic('solve-eqs') 7317 >>> t(And(x == 0, y >= x + 1)) 7320 return self.
apply(goal, *arguments, **keywords)
7323 """Display a string containing a description of the available options for the `self` tactic.""" 7327 """Return the parameter description set.""" 7331 if isinstance(a, BoolRef):
7332 goal =
Goal(ctx = a.ctx)
7338 def _to_tactic(t, ctx=None):
7339 if isinstance(t, Tactic):
7344 def _and_then(t1, t2, ctx=None):
7345 t1 = _to_tactic(t1, ctx)
7346 t2 = _to_tactic(t2, ctx)
7348 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7351 def _or_else(t1, t2, ctx=None):
7352 t1 = _to_tactic(t1, ctx)
7353 t2 = _to_tactic(t2, ctx)
7355 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7359 """Return a tactic that applies the tactics in `*ts` in sequence. 7361 >>> x, y = Ints('x y') 7362 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) 7363 >>> t(And(x == 0, y > x + 1)) 7365 >>> t(And(x == 0, y > x + 1)).as_expr() 7369 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7370 ctx = ks.get(
'ctx',
None)
7373 for i
in range(num - 1):
7374 r = _and_then(r, ts[i+1], ctx)
7378 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). 7380 >>> x, y = Ints('x y') 7381 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) 7382 >>> t(And(x == 0, y > x + 1)) 7384 >>> t(And(x == 0, y > x + 1)).as_expr() 7390 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). 7393 >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) 7394 >>> # Tactic split-clause fails if there is no clause in the given goal. 7397 >>> t(Or(x == 0, x == 1)) 7398 [[x == 0], [x == 1]] 7401 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7402 ctx = ks.get(
'ctx',
None)
7405 for i
in range(num - 1):
7406 r = _or_else(r, ts[i+1], ctx)
7410 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). 7413 >>> t = ParOr(Tactic('simplify'), Tactic('fail')) 7418 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7419 ctx = _get_ctx(ks.get(
'ctx',
None))
7420 ts = [ _to_tactic(t, ctx)
for t
in ts ]
7422 _args = (TacticObj * sz)()
7424 _args[i] = ts[i].tactic
7428 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. 7430 >>> x, y = Ints('x y') 7431 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) 7432 >>> t(And(Or(x == 1, x == 2), y == x + 1)) 7433 [[x == 1, y == 2], [x == 2, y == 3]] 7435 t1 = _to_tactic(t1, ctx)
7436 t2 = _to_tactic(t2, ctx)
7438 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7442 """Alias for ParThen(t1, t2, ctx).""" 7446 """Return a tactic that applies tactic `t` using the given configuration options. 7448 >>> x, y = Ints('x y') 7449 >>> t = With(Tactic('simplify'), som=True) 7450 >>> t((x + 1)*(y + 2) == 0) 7451 [[2*x + y + x*y == -2]] 7453 ctx = keys.pop(
'ctx',
None)
7454 t = _to_tactic(t, ctx)
7459 """Return a tactic that applies tactic `t` using the given configuration options. 7461 >>> x, y = Ints('x y') 7463 >>> p.set("som", True) 7464 >>> t = WithParams(Tactic('simplify'), p) 7465 >>> t((x + 1)*(y + 2) == 0) 7466 [[2*x + y + x*y == -2]] 7468 t = _to_tactic(t,
None)
7472 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. 7474 >>> x, y = Ints('x y') 7475 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) 7476 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) 7478 >>> for subgoal in r: print(subgoal) 7479 [x == 0, y == 0, x > y] 7480 [x == 0, y == 1, x > y] 7481 [x == 1, y == 0, x > y] 7482 [x == 1, y == 1, x > y] 7483 >>> t = Then(t, Tactic('propagate-values')) 7487 t = _to_tactic(t, ctx)
7491 """Return a tactic that applies `t` to a given goal for `ms` milliseconds. 7493 If `t` does not terminate in `ms` milliseconds, then it fails. 7495 t = _to_tactic(t, ctx)
7499 """Return a list of all available tactics in Z3. 7502 >>> l.count('simplify') == 1 7509 """Return a short description for the tactic named `name`. 7511 >>> d = tactic_description('simplify') 7517 """Display a (tabular) description of all available tactics in Z3.""" 7520 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7523 print(
'<tr style="background-color:#CFCFCF">')
7528 print(
'<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(
tactic_description(t), 40)))
7535 """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.""" 7539 if isinstance(probe, ProbeObj):
7541 elif isinstance(probe, float):
7543 elif _is_int(probe):
7545 elif isinstance(probe, bool):
7552 _z3_assert(isinstance(probe, str),
"probe name expected")
7556 raise Z3Exception(
"unknown probe '%s'" % probe)
7563 if self.
probe is not None and self.
ctx.ref()
is not None:
7567 """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`. 7569 >>> p = Probe('size') < 10 7580 """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`. 7582 >>> p = Probe('size') > 10 7593 """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`. 7595 >>> p = Probe('size') <= 2 7606 """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`. 7608 >>> p = Probe('size') >= 2 7619 """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`. 7621 >>> p = Probe('size') == 2 7632 """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`. 7634 >>> p = Probe('size') != 2 7646 """Evaluate the probe `self` in the given goal. 7648 >>> p = Probe('size') 7658 >>> p = Probe('num-consts') 7661 >>> p = Probe('is-propositional') 7664 >>> p = Probe('is-qflia') 7669 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expression expected")
7670 goal = _to_goal(goal)
7674 """Return `True` if `p` is a Z3 probe. 7676 >>> is_probe(Int('x')) 7678 >>> is_probe(Probe('memory')) 7681 return isinstance(p, Probe)
7683 def _to_probe(p, ctx=None):
7687 return Probe(p, ctx)
7690 """Return a list of all available probes in Z3. 7693 >>> l.count('memory') == 1 7700 """Return a short description for the probe named `name`. 7702 >>> d = probe_description('memory') 7708 """Display a (tabular) description of all available probes in Z3.""" 7711 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7714 print(
'<tr style="background-color:#CFCFCF">')
7719 print(
'<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(
probe_description(p), 40)))
7725 def _probe_nary(f, args, ctx):
7727 _z3_assert(len(args) > 0,
"At least one argument expected")
7729 r = _to_probe(args[0], ctx)
7730 for i
in range(num - 1):
7731 r =
Probe(f(ctx.ref(), r.probe, _to_probe(args[i+1], ctx).probe), ctx)
7734 def _probe_and(args, ctx):
7735 return _probe_nary(Z3_probe_and, args, ctx)
7737 def _probe_or(args, ctx):
7738 return _probe_nary(Z3_probe_or, args, ctx)
7741 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 7743 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. 7745 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) 7746 >>> x, y = Ints('x y') 7752 >>> g.add(x == y + 1) 7754 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 7756 p = _to_probe(p, ctx)
7760 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 7762 >>> t = When(Probe('size') > 2, Tactic('simplify')) 7763 >>> x, y = Ints('x y') 7769 >>> g.add(x == y + 1) 7771 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 7773 p = _to_probe(p, ctx)
7774 t = _to_tactic(t, ctx)
7778 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. 7780 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt')) 7782 p = _to_probe(p, ctx)
7783 t1 = _to_tactic(t1, ctx)
7784 t2 = _to_tactic(t2, ctx)
7794 """Simplify the expression `a` using the given options. 7796 This function has many options. Use `help_simplify` to obtain the complete list. 7800 >>> simplify(x + 1 + y + x + 1) 7802 >>> simplify((x + 1)*(y + 1), som=True) 7804 >>> simplify(Distinct(x, y, 1), blast_distinct=True) 7805 And(Not(x == y), Not(x == 1), Not(y == 1)) 7806 >>> simplify(And(x == 0, y == 1), elim_and=True) 7807 Not(Or(Not(x == 0), Not(y == 1))) 7810 _z3_assert(
is_expr(a),
"Z3 expression expected")
7811 if len(arguments) > 0
or len(keywords) > 0:
7813 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
7815 return _to_expr_ref(
Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
7818 """Return a string describing all options available for Z3 `simplify` procedure.""" 7822 """Return the set of parameter descriptions for Z3 `simplify` procedure.""" 7826 """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. 7830 >>> substitute(x + 1, (x, y + 1)) 7832 >>> f = Function('f', IntSort(), IntSort()) 7833 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 7836 if isinstance(m, tuple):
7838 if isinstance(m1, list):
7841 _z3_assert(
is_expr(t),
"Z3 expression expected")
7842 _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.")
7844 _from = (Ast * num)()
7846 for i
in range(num):
7847 _from[i] = m[i][0].as_ast()
7848 _to[i] = m[i][1].as_ast()
7849 return _to_expr_ref(
Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
7852 """Substitute the free variables in t with the expression in m. 7854 >>> v0 = Var(0, IntSort()) 7855 >>> v1 = Var(1, IntSort()) 7857 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 7858 >>> # replace v0 with x+1 and v1 with x 7859 >>> substitute_vars(f(v0, v1), x + 1, x) 7863 _z3_assert(
is_expr(t),
"Z3 expression expected")
7864 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
7867 for i
in range(num):
7868 _to[i] = m[i].as_ast()
7872 """Create the sum of the Z3 expressions. 7874 >>> a, b, c = Ints('a b c') 7879 >>> A = IntVector('a', 5) 7881 a__0 + a__1 + a__2 + a__3 + a__4 7883 args = _get_args(args)
7886 ctx = _ctx_from_ast_arg_list(args)
7888 return _reduce(
lambda a, b: a + b, args, 0)
7889 args = _coerce_expr_list(args, ctx)
7891 return _reduce(
lambda a, b: a + b, args, 0)
7893 _args, sz = _to_ast_array(args)
7898 """Create the product of the Z3 expressions. 7900 >>> a, b, c = Ints('a b c') 7901 >>> Product(a, b, c) 7903 >>> Product([a, b, c]) 7905 >>> A = IntVector('a', 5) 7907 a__0*a__1*a__2*a__3*a__4 7909 args = _get_args(args)
7912 ctx = _ctx_from_ast_arg_list(args)
7914 return _reduce(
lambda a, b: a * b, args, 1)
7915 args = _coerce_expr_list(args, ctx)
7917 return _reduce(
lambda a, b: a * b, args, 1)
7919 _args, sz = _to_ast_array(args)
7923 """Create an at-most Pseudo-Boolean k constraint. 7925 >>> a, b, c = Bools('a b c') 7926 >>> f = AtMost(a, b, c, 2) 7928 args = _get_args(args)
7930 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
7931 ctx = _ctx_from_ast_arg_list(args)
7933 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
7934 args1 = _coerce_expr_list(args[:-1], ctx)
7936 _args, sz = _to_ast_array(args1)
7940 """Create an at-most Pseudo-Boolean k constraint. 7942 >>> a, b, c = Bools('a b c') 7943 >>> f = AtLeast(a, b, c, 2) 7945 args = _get_args(args)
7947 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
7948 ctx = _ctx_from_ast_arg_list(args)
7950 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
7951 args1 = _coerce_expr_list(args[:-1], ctx)
7953 _args, sz = _to_ast_array(args1)
7957 def _pb_args_coeffs(args, default_ctx = None):
7958 args = _get_args_ast_list(args)
7960 return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
7961 args, coeffs = zip(*args)
7963 _z3_assert(len(args) > 0,
"Non empty list of arguments expected")
7964 ctx = _ctx_from_ast_arg_list(args)
7966 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
7967 args = _coerce_expr_list(args, ctx)
7968 _args, sz = _to_ast_array(args)
7969 _coeffs = (ctypes.c_int * len(coeffs))()
7970 for i
in range(len(coeffs)):
7971 _coeffs[i] = coeffs[i]
7972 return ctx, sz, _args, _coeffs
7975 """Create a Pseudo-Boolean inequality k constraint. 7977 >>> a, b, c = Bools('a b c') 7978 >>> f = PbLe(((a,1),(b,3),(c,2)), 3) 7980 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
7984 """Create a Pseudo-Boolean inequality k constraint. 7986 >>> a, b, c = Bools('a b c') 7987 >>> f = PbGe(((a,1),(b,3),(c,2)), 3) 7989 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
7993 """Create a Pseudo-Boolean inequality k constraint. 7995 >>> a, b, c = Bools('a b c') 7996 >>> f = PbEq(((a,1),(b,3),(c,2)), 3) 7998 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8003 """Solve the constraints `*args`. 8005 This is a simple function for creating demonstrations. It creates a solver, 8006 configure it using the options in `keywords`, adds the constraints 8007 in `args`, and invokes check. 8010 >>> solve(a > 0, a < 2) 8016 if keywords.get(
'show',
False):
8020 print(
"no solution")
8022 print(
"failed to solve")
8031 """Solve the constraints `*args` using solver `s`. 8033 This is a simple function for creating demonstrations. It is similar to `solve`, 8034 but it uses the given solver `s`. 8035 It configures solver `s` using the options in `keywords`, adds the constraints 8036 in `args`, and invokes check. 8039 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8042 if keywords.get(
'show',
False):
8047 print(
"no solution")
8049 print(
"failed to solve")
8055 if keywords.get(
'show',
False):
8060 """Try to prove the given claim. 8062 This is a simple function for creating demonstrations. It tries to prove 8063 `claim` by showing the negation is unsatisfiable. 8065 >>> p, q = Bools('p q') 8066 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) 8070 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8074 if keywords.get(
'show',
False):
8080 print(
"failed to prove")
8083 print(
"counterexample")
8086 def _solve_html(*args, **keywords):
8087 """Version of funcion `solve` used in RiSE4Fun.""" 8091 if keywords.get(
'show',
False):
8092 print(
"<b>Problem:</b>")
8096 print(
"<b>no solution</b>")
8098 print(
"<b>failed to solve</b>")
8104 if keywords.get(
'show',
False):
8105 print(
"<b>Solution:</b>")
8108 def _solve_using_html(s, *args, **keywords):
8109 """Version of funcion `solve_using` used in RiSE4Fun.""" 8111 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8114 if keywords.get(
'show',
False):
8115 print(
"<b>Problem:</b>")
8119 print(
"<b>no solution</b>")
8121 print(
"<b>failed to solve</b>")
8127 if keywords.get(
'show',
False):
8128 print(
"<b>Solution:</b>")
8131 def _prove_html(claim, **keywords):
8132 """Version of funcion `prove` used in RiSE4Fun.""" 8134 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8138 if keywords.get(
'show',
False):
8142 print(
"<b>proved</b>")
8144 print(
"<b>failed to prove</b>")
8147 print(
"<b>counterexample</b>")
8150 def _dict2sarray(sorts, ctx):
8152 _names = (Symbol * sz)()
8153 _sorts = (Sort * sz) ()
8158 _z3_assert(isinstance(k, str),
"String expected")
8159 _z3_assert(
is_sort(v),
"Z3 sort expected")
8163 return sz, _names, _sorts
8165 def _dict2darray(decls, ctx):
8167 _names = (Symbol * sz)()
8168 _decls = (FuncDecl * sz) ()
8173 _z3_assert(isinstance(k, str),
"String expected")
8177 _decls[i] = v.decl().ast
8181 return sz, _names, _decls
8183 def _handle_parse_error(ex, ctx):
8186 raise Z3Exception(msg)
8190 """Parse a string in SMT 2.0 format using the given sorts and decls. 8192 The arguments sorts and decls are Python dictionaries used to initialize 8193 the symbol table used for the SMT 2.0 parser. 8195 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') 8197 >>> x, y = Ints('x y') 8198 >>> f = Function('f', IntSort(), IntSort()) 8199 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) 8201 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) 8205 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 8206 dsz, dnames, ddecls = _dict2darray(decls, ctx) 8208 return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 8209 except Z3Exception as e: 8210 _handle_parse_error(e, ctx) 8212 def parse_smt2_file(f, sorts={}, decls={}, ctx=None): 8213 """Parse a file
in SMT 2.0 format using the given sorts
and decls.
8218 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 8219 dsz, dnames, ddecls = _dict2darray(decls, ctx) 8221 return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 8222 except Z3Exception as e: 8223 _handle_parse_error(e, ctx) 8225 def Interpolant(a,ctx=None): 8226 """Create an interpolation operator.
8228 The argument
is an interpolation pattern (see tree_interpolant).
8234 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) 8237 return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx) 8239 def tree_interpolant(pat,p=None,ctx=None): 8240 """Compute interpolant
for a tree of formulas.
8242 The input
is an interpolation pattern over a set of formulas C.
8243 The pattern pat
is a formula combining the formulas
in C using
8244 logical conjunction
and the
"interp" operator (see Interp). This
8245 interp operator
is logically the identity operator. It marks the
8246 sub-formulas of the pattern
for which interpolants should be
8247 computed. The interpolant
is a map sigma
from marked subformulas
8248 to formulas, such that,
for each marked subformula phi of pat
8249 (where phi sigma
is phi with sigma(psi) substituted
for each
8250 subformula psi of phi such that psi
in dom(sigma)):
8252 1) phi sigma implies sigma(phi),
and 8254 2) sigma(phi)
is in the common uninterpreted vocabulary between
8255 the formulas of C occurring
in phi
and those
not occurring
in 8258 and moreover pat sigma implies false. In the simplest case
8259 an interpolant
for the pattern
"(and (interp A) B)" maps A
8260 to an interpolant
for A /\ B.
8262 The
return value
is a vector of formulas representing sigma. This
8263 vector contains sigma(phi)
for each marked subformula of pat,
in 8264 pre-order traversal. This means that subformulas of phi occur before phi
8265 in the vector. Also, subformulas that occur multiply
in pat will
8266 occur multiply
in the result vector.
8268 If pat
is satisfiable, raises an object of
class ModelRef 8269 that represents a model of pat.
8271 If neither a proof of unsatisfiability nor a model
is obtained
8272 (
for example, because of a timeout,
or because models are disabled)
8273 then
None is returned.
8275 If parameters p are supplied, these are used
in creating the
8276 solver that determines satisfiability.
8281 [
Not(x >= 0),
Not(y <= 2)]
8288 (define-fun x () Int
8292 ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx)) 8293 ptr = (AstVectorObj * 1)() 8294 mptr = (Model * 1)() 8297 res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr) 8298 if res == Z3_L_FALSE: 8299 return AstVector(ptr[0],ctx) 8301 raise ModelRef(mptr[0], ctx) 8304 def binary_interpolant(a,b,p=None,ctx=None): 8305 """Compute an interpolant
for a binary conjunction.
8307 If a & b
is unsatisfiable, returns an interpolant
for a & b.
8308 This
is a formula phi such that
8311 2) b implies
not phi
8312 3) All the uninterpreted symbols of phi occur
in both a
and b.
8314 If a & b
is satisfiable, raises an object of
class ModelRef 8315 that represents a model of a &b.
8317 If neither a proof of unsatisfiability nor a model
is obtained
8318 (
for example, because of a timeout,
or because models are disabled)
8319 then
None is returned.
8321 If parameters p are supplied, these are used
in creating the
8322 solver that determines satisfiability.
8328 f = And(Interpolant(a),b) 8329 ti = tree_interpolant(f,p,ctx) 8330 return ti[0] if ti is not None else None 8332 def sequence_interpolant(v,p=None,ctx=None): 8333 """Compute interpolant
for a sequence of formulas.
8335 If len(v) == N,
and if the conjunction of the formulas
in v
is 8336 unsatisfiable, the interpolant
is a sequence of formulas w
8337 such that len(w) = N-1
and v[0] implies w[0]
and for i
in 0..N-1:
8339 1) w[i] & v[i+1] implies w[i+1] (
or false
if i+1 = N)
8340 2) All uninterpreted symbols
in w[i] occur
in both v[0]..v[i]
8343 Requires len(v) >= 1.
8345 If a & b
is satisfiable, raises an object of
class ModelRef 8346 that represents a model of a & b.
8348 If neither a proof of unsatisfiability nor a model
is obtained
8349 (
for example, because of a timeout,
or because models are disabled)
8350 then
None is returned.
8352 If parameters p are supplied, these are used
in creating the
8353 solver that determines satisfiability.
8358 [
Not(x >= 0),
Not(y >= 0)]
8361 for i in range(1,len(v)): 8362 f = And(Interpolant(f),v[i]) 8363 return tree_interpolant(f,p,ctx) 8366 ######################################### 8368 # Floating-Point Arithmetic 8370 ######################################### 8373 # Global default rounding mode 8374 _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO 8375 _dflt_fpsort_ebits = 11 8376 _dflt_fpsort_sbits = 53 8378 def get_default_rounding_mode(ctx=None): 8379 """Retrieves the
global default rounding mode.
""" 8380 global _dflt_rounding_mode 8381 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO: 8383 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE: 8385 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE: 8387 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: 8389 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: 8392 def set_default_rounding_mode(rm, ctx=None): 8393 global _dflt_rounding_mode 8394 if is_fprm_value(rm): 8395 _dflt_rounding_mode = rm.decl().kind() 8397 _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO or 8398 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE or 8399 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE or 8400 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN or 8401 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, 8402 "illegal rounding mode") 8403 _dflt_rounding_mode = rm 8405 def get_default_fp_sort(ctx=None): 8406 return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx) 8408 def set_default_fp_sort(ebits, sbits, ctx=None): 8409 global _dflt_fpsort_ebits 8410 global _dflt_fpsort_sbits 8411 _dflt_fpsort_ebits = ebits 8412 _dflt_fpsort_sbits = sbits 8414 def _dflt_rm(ctx=None): 8415 return get_default_rounding_mode(ctx) 8417 def _dflt_fps(ctx=None): 8418 return get_default_fp_sort(ctx) 8420 def _coerce_fp_expr_list(alist, ctx): 8421 first_fp_sort = None 8424 if first_fp_sort is None: 8425 first_fp_sort = a.sort() 8426 elif first_fp_sort == a.sort(): 8427 pass # OK, same as before 8429 # we saw at least 2 different float sorts; something will 8430 # throw a sort mismatch later, for now assume None. 8431 first_fp_sort = None 8435 for i in range(len(alist)): 8437 if (isinstance(a, str) and a.contains('2**(') and a.endswith(')')) or _is_int(a) or isinstance(a, float) or isinstance(a, bool): 8438 r.append(FPVal(a, None, first_fp_sort, ctx)) 8441 return _coerce_expr_list(r, ctx) 8446 class FPSortRef(SortRef): 8447 """Floating-point sort.
""" 8450 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint sort `self`.
8455 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast)) 8458 """Retrieves the number of bits reserved
for the significand
in the FloatingPoint sort `self`.
8463 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast)) 8465 def cast(self, val): 8466 """Try to cast `val`
as a floating-point expression.
8470 >>> b.cast(1.0).
sexpr()
8471 '(fp #b0 #x7f #b00000000000000000000000)' 8475 _z3_assert(self.ctx == val.ctx, "Context mismatch") 8478 return FPVal(val, None, self, self.ctx) 8481 def Float16(ctx=None): 8482 """Floating-point 16-bit (half) sort.
""" 8484 return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx) 8486 def FloatHalf(ctx=None): 8487 """Floating-point 16-bit (half) sort.
""" 8489 return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx) 8491 def Float32(ctx=None): 8492 """Floating-point 32-bit (single) sort.
""" 8494 return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx) 8496 def FloatSingle(ctx=None): 8497 """Floating-point 32-bit (single) sort.
""" 8499 return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx) 8501 def Float64(ctx=None): 8502 """Floating-point 64-bit (double) sort.
""" 8504 return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx) 8506 def FloatDouble(ctx=None): 8507 """Floating-point 64-bit (double) sort.
""" 8509 return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx) 8511 def Float128(ctx=None): 8512 """Floating-point 128-bit (quadruple) sort.
""" 8514 return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx) 8516 def FloatQuadruple(ctx=None): 8517 """Floating-point 128-bit (quadruple) sort.
""" 8519 return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx) 8521 class FPRMSortRef(SortRef): 8522 """"Floating-point rounding mode sort.""" 8526 """Return True if `s` is a Z3 floating-point sort.
8533 return isinstance(s, FPSortRef) 8535 def is_fprm_sort(s): 8536 """Return
True if `s`
is a Z3 floating-point rounding mode sort.
8543 return isinstance(s, FPRMSortRef) 8547 class FPRef(ExprRef): 8548 """Floating-point expressions.
""" 8551 """Return the sort of the floating-point expression `self`.
8556 >>> x.sort() ==
FPSort(8, 24)
8559 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 8562 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8567 return self.sort().ebits(); 8570 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8575 return self.sort().sbits(); 8577 def as_string(self): 8578 """Return a Z3 floating point expression
as a Python string.
""" 8579 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8581 def __le__(self, other): 8582 return fpLEQ(self, other, self.ctx) 8584 def __lt__(self, other): 8585 return fpLT(self, other, self.ctx) 8587 def __ge__(self, other): 8588 return fpGEQ(self, other, self.ctx) 8590 def __gt__(self, other): 8591 return fpGT(self, other, self.ctx) 8593 def __add__(self, other): 8594 """Create the Z3 expression `self + other`.
8603 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8604 return fpAdd(_dflt_rm(), a, b, self.ctx) 8606 def __radd__(self, other): 8607 """Create the Z3 expression `other + self`.
8613 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8614 return fpAdd(_dflt_rm(), a, b, self.ctx) 8616 def __sub__(self, other): 8617 """Create the Z3 expression `self - other`.
8626 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8627 return fpSub(_dflt_rm(), a, b, self.ctx) 8629 def __rsub__(self, other): 8630 """Create the Z3 expression `other - self`.
8636 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8637 return fpSub(_dflt_rm(), a, b, self.ctx) 8639 def __mul__(self, other): 8640 """Create the Z3 expression `self * other`.
8651 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8652 return fpMul(_dflt_rm(), a, b, self.ctx) 8654 def __rmul__(self, other): 8655 """Create the Z3 expression `other * self`.
8664 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8665 return fpMul(_dflt_rm(), a, b, self.ctx) 8668 """Create the Z3 expression `+self`.
""" 8672 """Create the Z3 expression `-self`.
8680 def __div__(self, other): 8681 """Create the Z3 expression `self / other`.
8692 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8693 return fpDiv(_dflt_rm(), a, b, self.ctx) 8695 def __rdiv__(self, other): 8696 """Create the Z3 expression `other / self`.
8705 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8706 return fpDiv(_dflt_rm(), a, b, self.ctx) 8708 if not sys.version < '3': 8709 def __truediv__(self, other): 8710 """Create the Z3 expression division `self / other`.
""" 8711 return self.__div__(other) 8713 def __rtruediv__(self, other): 8714 """Create the Z3 expression division `other / self`.
""" 8715 return self.__rdiv__(other) 8717 def __mod__(self, other): 8718 """Create the Z3 expression mod `self % other`.
""" 8719 return fpRem(self, other) 8721 def __rmod__(self, other): 8722 """Create the Z3 expression mod `other % self`.
""" 8723 return fpRem(other, self) 8725 class FPRMRef(ExprRef): 8726 """Floating-point rounding mode expressions
""" 8728 def as_string(self): 8729 """Return a Z3 floating point expression
as a Python string.
""" 8730 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8733 def RoundNearestTiesToEven(ctx=None): 8735 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8739 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8741 def RoundNearestTiesToAway(ctx=None): 8743 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8747 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8749 def RoundTowardPositive(ctx=None): 8751 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8755 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8757 def RoundTowardNegative(ctx=None): 8759 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8763 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8765 def RoundTowardZero(ctx=None): 8767 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8771 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8774 """Return `
True`
if `a`
is a Z3 floating-point rounding mode expression.
8783 return isinstance(a, FPRMRef) 8785 def is_fprm_value(a): 8786 """Return `
True`
if `a`
is a Z3 floating-point rounding mode numeral value.
""" 8787 return is_fprm(a) and _is_numeral(a.ctx, a.ast) 8791 class FPNumRef(FPRef): 8792 """The sign of the numeral.
8802 l = (ctypes.c_int)() 8803 if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False: 8804 raise Z3Exception("error retrieving the sign of a numeral.") 8807 """The sign of a floating-point numeral
as a bit-vector expression.
8809 Remark: NaN
's are invalid arguments. 8811 def sign_as_bv(self): 8812 return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx) 8814 """The significand of the numeral.
8820 def significand(self): 8821 return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast()) 8823 """The significand of the numeral
as a long.
8826 >>> x.significand_as_long()
8829 def significand_as_long(self): 8830 return Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast()) 8832 """The significand of the numeral
as a bit-vector expression.
8834 Remark: NaN are invalid arguments.
8836 def significand_as_bv(self): 8837 return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx) 8839 """The exponent of the numeral.
8845 def exponent(self, biased=True): 8846 return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased) 8848 """The exponent of the numeral
as a long.
8851 >>> x.exponent_as_long()
8854 def exponent_as_long(self, biased=True): 8855 ptr = (ctypes.c_longlong * 1)() 8856 if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased): 8857 raise Z3Exception("error retrieving the exponent of a numeral.") 8860 """The exponent of the numeral
as a bit-vector expression.
8862 Remark: NaNs are invalid arguments.
8864 def exponent_as_bv(self, biased=True): 8865 return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx) 8867 """Indicates whether the numeral
is a NaN.
""" 8869 return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast()) 8871 """Indicates whether the numeral
is +oo
or -oo.
""" 8873 return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast()) 8875 """Indicates whether the numeral
is +zero
or -zero.
""" 8877 return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast()) 8879 """Indicates whether the numeral
is normal.
""" 8881 return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast()) 8883 """Indicates whether the numeral
is subnormal.
""" 8884 def isSubnormal(self): 8885 return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast()) 8887 """Indicates whether the numeral
is positive.
""" 8888 def isPositive(self): 8889 return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast()) 8891 """Indicates whether the numeral
is negative.
""" 8892 def isNegative(self): 8893 return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast()) 8896 The string representation of the numeral.
8902 def as_string(self): 8903 s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast()) 8904 return ("FPVal(%s, %s)" % (s, self.sort())) 8907 """Return `
True`
if `a`
is a Z3 floating-point expression.
8917 return isinstance(a, FPRef) 8920 """Return `
True`
if `a`
is a Z3 floating-point numeral value.
8931 return is_fp(a) and _is_numeral(a.ctx, a.ast) 8933 def FPSort(ebits, sbits, ctx=None): 8934 """Return a Z3 floating-point sort of the given sizes. If `ctx=
None`, then the
global context
is used.
8936 >>> Single =
FPSort(8, 24)
8937 >>> Double =
FPSort(11, 53)
8940 >>> x =
Const(
'x', Single)
8945 return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx) 8947 def _to_float_str(val, exp=0): 8948 if isinstance(val, float): 8952 sone = math.copysign(1.0, val) 8957 elif val == float("+inf"): 8959 elif val == float("-inf"): 8962 v = val.as_integer_ratio() 8965 rvs = str(num) + '/' + str(den) 8966 res = rvs + 'p' + _to_int_str(exp) 8967 elif isinstance(val, bool): 8974 elif isinstance(val, str): 8975 inx = val.find('*(2**') 8978 elif val[-1] == ')': 8980 exp = str(int(val[inx+5:-1]) + int(exp)) 8982 _z3_assert(False, "String does not have floating-point numeral form.") 8984 _z3_assert(False, "Python value cannot be used to create floating-point numerals.") 8988 return res + 'p' + exp 8992 """Create a Z3 floating-point NaN term.
8995 >>> set_fpa_pretty(
True)
8998 >>> pb = get_fpa_pretty()
8999 >>> set_fpa_pretty(
False)
9002 >>> set_fpa_pretty(pb)
9004 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9005 return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx) 9007 def fpPlusInfinity(s): 9008 """Create a Z3 floating-point +oo term.
9011 >>> pb = get_fpa_pretty()
9012 >>> set_fpa_pretty(
True)
9015 >>> set_fpa_pretty(
False)
9018 >>> set_fpa_pretty(pb)
9020 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9021 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx) 9023 def fpMinusInfinity(s): 9024 """Create a Z3 floating-point -oo term.
""" 9025 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9026 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx) 9028 def fpInfinity(s, negative): 9029 """Create a Z3 floating-point +oo
or -oo term.
""" 9030 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9031 _z3_assert(isinstance(negative, bool), "expected Boolean flag") 9032 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx) 9035 """Create a Z3 floating-point +0.0 term.
""" 9036 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9037 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx) 9040 """Create a Z3 floating-point -0.0 term.
""" 9041 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9042 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx) 9044 def fpZero(s, negative): 9045 """Create a Z3 floating-point +0.0
or -0.0 term.
""" 9046 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 9047 _z3_assert(isinstance(negative, bool), "expected Boolean flag") 9048 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx) 9050 def FPVal(sig, exp=None, fps=None, ctx=None): 9051 """Return a floating-point value of value `val`
and sort `fps`. If `ctx=
None`, then the
global context
is used.
9056 >>> print(
"0x%.8x" % v.exponent_as_long(
False))
9076 fps = _dflt_fps(ctx) 9077 _z3_assert(is_fp_sort(fps), "sort mismatch") 9080 val = _to_float_str(sig) 9081 if val == "NaN" or val == "nan": 9084 return fpMinusZero(fps) 9085 elif val == "0.0" or val == "+0.0": 9086 return fpPlusZero(fps) 9087 elif val == "+oo" or val == "+inf" or val == "+Inf": 9088 return fpPlusInfinity(fps) 9089 elif val == "-oo" or val == "-inf" or val == "-Inf": 9090 return fpMinusInfinity(fps) 9092 return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx) 9094 def FP(name, fpsort, ctx=None): 9095 """Return a floating-point constant named `name`.
9096 `fpsort`
is the floating-point sort.
9097 If `ctx=
None`, then the
global context
is used.
9107 >>> x2 =
FP(
'x', word)
9111 if isinstance(fpsort, FPSortRef) and ctx is None: 9115 return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx) 9117 def FPs(names, fpsort, ctx=None): 9118 """Return an array of floating-point constants.
9120 >>> x, y, z =
FPs(
'x y z',
FPSort(8, 24))
9131 if isinstance(names, str): 9132 names = names.split(" ") 9133 return [FP(name, fpsort, ctx) for name in names] 9135 def fpAbs(a, ctx=None): 9136 """Create a Z3 floating-point absolute value expression.
9140 >>> x =
FPVal(1.0, s)
9143 >>> y =
FPVal(-20.0, s)
9148 >>>
fpAbs(-1.25*(2**4))
9154 [a] = _coerce_fp_expr_list([a], ctx) 9155 return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx) 9157 def fpNeg(a, ctx=None): 9158 """Create a Z3 floating-point addition expression.
9169 [a] = _coerce_fp_expr_list([a], ctx) 9170 return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx) 9172 def _mk_fp_unary(f, rm, a, ctx): 9174 [a] = _coerce_fp_expr_list([a], ctx) 9176 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9177 _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression") 9178 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx) 9180 def _mk_fp_unary_norm(f, a, ctx): 9182 [a] = _coerce_fp_expr_list([a], ctx) 9184 _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression") 9185 return FPRef(f(ctx.ref(), a.as_ast()), ctx) 9187 def _mk_fp_unary_pred(f, a, ctx): 9189 [a] = _coerce_fp_expr_list([a], ctx) 9191 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9192 return BoolRef(f(ctx.ref(), a.as_ast()), ctx) 9194 def _mk_fp_bin(f, rm, a, b, ctx): 9196 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9198 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9199 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9200 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx) 9202 def _mk_fp_bin_norm(f, a, b, ctx): 9204 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9206 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression") 9207 return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 9209 def _mk_fp_bin_pred(f, a, b, ctx): 9211 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9213 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9214 return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 9216 def _mk_fp_tern(f, rm, a, b, c, ctx): 9218 [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx) 9220 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9221 _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") 9222 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx) 9224 def fpAdd(rm, a, b, ctx=None): 9225 """Create a Z3 floating-point addition expression.
9235 >>>
fpAdd(rm, x, y).sort()
9238 return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx) 9240 def fpSub(rm, a, b, ctx=None): 9241 """Create a Z3 floating-point subtraction expression.
9249 >>>
fpSub(rm, x, y).sort()
9252 return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx) 9254 def fpMul(rm, a, b, ctx=None): 9255 """Create a Z3 floating-point multiplication expression.
9263 >>>
fpMul(rm, x, y).sort()
9266 return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx) 9268 def fpDiv(rm, a, b, ctx=None): 9269 """Create a Z3 floating-point division expression.
9277 >>>
fpDiv(rm, x, y).sort()
9280 return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx) 9282 def fpRem(a, b, ctx=None): 9283 """Create a Z3 floating-point remainder expression.
9290 >>>
fpRem(x, y).sort()
9293 return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx) 9295 def fpMin(a, b, ctx=None): 9296 """Create a Z3 floating-point minimum expression.
9304 >>>
fpMin(x, y).sort()
9307 return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx) 9309 def fpMax(a, b, ctx=None): 9310 """Create a Z3 floating-point maximum expression.
9318 >>>
fpMax(x, y).sort()
9321 return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx) 9323 def fpFMA(rm, a, b, c, ctx=None): 9324 """Create a Z3 floating-point fused multiply-add expression.
9326 return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx) 9328 def fpSqrt(rm, a, ctx=None): 9329 """Create a Z3 floating-point square root expression.
9331 return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx) 9333 def fpRoundToIntegral(rm, a, ctx=None): 9334 """Create a Z3 floating-point roundToIntegral expression.
9336 return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx) 9338 def fpIsNaN(a, ctx=None): 9339 """Create a Z3 floating-point isNaN expression.
9347 return _mk_fp_unary_norm(Z3_mk_fpa_is_nan, a, ctx) 9349 def fpIsInf(a, ctx=None): 9350 """Create a Z3 floating-point isInfinite expression.
9357 return _mk_fp_unary_norm(Z3_mk_fpa_is_infinite, a, ctx) 9359 def fpIsZero(a, ctx=None): 9360 """Create a Z3 floating-point isZero expression.
9362 return _mk_fp_unary_norm(Z3_mk_fpa_is_zero, a, ctx) 9364 def fpIsNormal(a, ctx=None): 9365 """Create a Z3 floating-point isNormal expression.
9367 return _mk_fp_unary_norm(Z3_mk_fpa_is_normal, a, ctx) 9369 def fpIsSubnormal(a, ctx=None): 9370 """Create a Z3 floating-point isSubnormal expression.
9372 return _mk_fp_unary_norm(Z3_mk_fpa_is_subnormal, a, ctx) 9374 def fpIsNegative(a, ctx=None): 9375 """Create a Z3 floating-point isNegative expression.
9377 return _mk_fp_unary_norm(Z3_mk_fpa_is_negative, a, ctx) 9379 def fpIsPositive(a, ctx=None): 9380 """Create a Z3 floating-point isPositive expression.
9382 return _mk_fp_unary_norm(Z3_mk_fpa_is_positive, a, ctx) 9383 return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) 9385 def _check_fp_args(a, b): 9387 _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") 9389 def fpLT(a, b, ctx=None): 9390 """Create the Z3 floating-point expression `other < self`.
9398 return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx) 9400 def fpLEQ(a, b, ctx=None): 9401 """Create the Z3 floating-point expression `other <= self`.
9406 >>> (x <= y).sexpr()
9409 return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx) 9411 def fpGT(a, b, ctx=None): 9412 """Create the Z3 floating-point expression `other > self`.
9420 return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx) 9422 def fpGEQ(a, b, ctx=None): 9423 """Create the Z3 floating-point expression `other >= self`.
9428 >>> (x >= y).sexpr()
9431 return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx) 9433 def fpEQ(a, b, ctx=None): 9434 """Create the Z3 floating-point expression `
fpEQ(other, self)`.
9439 >>>
fpEQ(x, y).sexpr()
9442 return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx) 9444 def fpNEQ(a, b, ctx=None): 9445 """Create the Z3 floating-point expression `
Not(
fpEQ(other, self))`.
9450 >>> (x != y).sexpr()
9453 return Not(fpEQ(a, b, ctx)) 9455 def fpFP(sgn, exp, sig, ctx=None): 9456 """Create the Z3 floating-point value `
fpFP(sgn, sig, exp)`
from the three bit-vectors sgn, sig,
and exp.
9461 fpFP(1, 127, 4194304)
9462 >>> xv =
FPVal(-1.5, s)
9466 >>> slvr.add(
fpEQ(x, xv))
9469 >>> xv =
FPVal(+1.5, s)
9473 >>> slvr.add(
fpEQ(x, xv))
9477 _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch") 9478 _z3_assert(sgn.sort().size() == 1, "sort mismatch") 9480 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch") 9481 return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx) 9483 def fpToFP(a1, a2=None, a3=None, ctx=None): 9484 """Create a Z3 floating-point conversion expression
from other term sorts
9487 From a bit-vector term
in IEEE 754-2008 format:
9493 From a floating-point term with different precision:
9504 From a signed bit-vector term:
9510 if is_bv(a1) and is_fp_sort(a2): 9511 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx) 9512 elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3): 9513 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9514 elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3): 9515 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9516 elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3): 9517 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9519 raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.") 9521 def fpBVToFP(v, sort, ctx=None): 9522 """Create a Z3 floating-point conversion expression that represents the
9523 conversion
from a bit-vector term to a floating-point term.
9532 _z3_assert(is_bv(v), "First argument must be a Z3 floating-point rounding mode expression.") 9533 _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.") 9535 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx) 9537 def fpFPToFP(rm, v, sort, ctx=None): 9538 """Create a Z3 floating-point conversion expression that represents the
9539 conversion
from a floating-point term to a floating-point term of different precision.
9550 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9551 _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.") 9552 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9554 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9556 def fpRealToFP(rm, v, sort, ctx=None): 9557 """Create a Z3 floating-point conversion expression that represents the
9558 conversion
from a real term to a floating-point term.
9567 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9568 _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.") 9569 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9571 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9573 def fpSignedToFP(rm, v, sort, ctx=None): 9574 """Create a Z3 floating-point conversion expression that represents the
9575 conversion
from a signed bit-vector term (encoding an integer) to a floating-point term.
9584 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9585 _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") 9586 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9588 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9590 def fpUnsignedToFP(rm, v, sort, ctx=None): 9591 """Create a Z3 floating-point conversion expression that represents the
9592 conversion
from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9601 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9602 _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") 9603 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9605 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9607 def fpToFPUnsigned(rm, x, s, ctx=None): 9608 """Create a Z3 floating-point conversion expression,
from unsigned bit-vector to floating-point expression.
""" 9610 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9611 _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression") 9612 _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort") 9614 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx) 9616 def fpToSBV(rm, x, s, ctx=None): 9617 """Create a Z3 floating-point conversion expression,
from floating-point expression to signed bit-vector.
9631 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9632 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") 9633 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") 9635 return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9637 def fpToUBV(rm, x, s, ctx=None): 9638 """Create a Z3 floating-point conversion expression,
from floating-point expression to unsigned bit-vector.
9652 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9653 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") 9654 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") 9656 return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9658 def fpToReal(x, ctx=None): 9659 """Create a Z3 floating-point conversion expression,
from floating-point expression to real.
9673 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9675 return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx) 9677 def fpToIEEEBV(x, ctx=None): 9678 """\brief Conversion of a floating-point term into a bit-vector term
in IEEE 754-2008 format.
9680 The size of the resulting bit-vector
is automatically determined.
9682 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9683 knows only one NaN
and it will always produce the same bit-vector representation of
9698 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9700 return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx) 9704 ######################################### 9706 # Strings, Sequences and Regular expressions 9708 ######################################### 9710 class SeqSortRef(SortRef): 9711 """Sequence sort.
""" 9713 def is_string(self): 9714 """Determine
if sort
is a string
9722 return Z3_is_string_sort(self.ctx_ref(), self.ast) 9725 def StringSort(ctx=None): 9726 """Create a string sort
9732 return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx) 9736 """Create a sequence sort over elements provided
in the argument
9741 return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx) 9743 class SeqRef(ExprRef): 9744 """Sequence expression.
""" 9747 return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 9749 def __add__(self, other): 9750 return Concat(self, other) 9752 def __radd__(self, other): 9753 return Concat(other, self) 9755 def __getitem__(self, i): 9757 i = IntVal(i, self.ctx) 9758 return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) 9760 def is_string(self): 9761 return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast())) 9763 def is_string_value(self): 9764 return Z3_is_string(self.ctx_ref(), self.as_ast()) 9766 def as_string(self): 9767 """Return a string representation of sequence expression.
""" 9768 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 9771 def _coerce_seq(s, ctx=None): 9772 if isinstance(s, str): 9774 s = StringVal(s, ctx) 9776 raise Z3Exception("Non-expression passed as a sequence") 9778 raise Z3Exception("Non-sequence passed as a sequence") 9781 def _get_ctx2(a, b, ctx=None): 9791 """Return `
True`
if `a`
is a Z3 sequence expression.
9797 return isinstance(a, SeqRef) 9800 """Return `
True`
if `a`
is a Z3 string expression.
9804 return isinstance(a, SeqRef) and a.is_string() 9806 def is_string_value(a): 9807 """return 'True' if 'a' is a Z3 string constant expression.
9813 return isinstance(a, SeqRef) and a.is_string_value() 9816 def StringVal(s, ctx=None): 9817 """create a string expression
""" 9819 return SeqRef(Z3_mk_string(ctx.ref(), s), ctx) 9821 def String(name, ctx=None): 9822 """Return a string constant named `name`. If `ctx=
None`, then the
global context
is used.
9827 return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx) 9829 def SubString(s, offset, length): 9830 """Extract substring
or subsequence starting at offset
""" 9831 return Extract(s, offset, length) 9833 def SubSeq(s, offset, length): 9834 """Extract substring
or subsequence starting at offset
""" 9835 return Extract(s, offset, length) 9837 def Strings(names, ctx=None): 9838 """Return a tuple of String constants.
""" 9840 if isinstance(names, str): 9841 names = names.split(" ") 9842 return [String(name, ctx) for name in names] 9845 """Create the empty sequence of the given sort
9859 if isinstance(s, SeqSortRef): 9860 return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx) 9861 if isinstance(s, ReSortRef): 9862 return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx) 9863 raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty") 9866 """Create the regular expression that accepts the universal language
9874 if isinstance(s, ReSortRef): 9875 return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx) 9876 raise Z3Exception("Non-sequence, non-regular expression sort passed to Full") 9880 """Create a singleton sequence
""" 9881 return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx) 9884 """Check
if 'a' is a prefix of
'b' 9892 ctx = _get_ctx2(a, b) 9893 a = _coerce_seq(a, ctx) 9894 b = _coerce_seq(b, ctx) 9895 return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 9898 """Check
if 'a' is a suffix of
'b' 9906 ctx = _get_ctx2(a, b) 9907 a = _coerce_seq(a, ctx) 9908 b = _coerce_seq(b, ctx) 9909 return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 9912 """Check
if 'a' contains
'b' 9919 >>> x, y, z =
Strings(
'x y z')
9924 ctx = _get_ctx2(a, b) 9925 a = _coerce_seq(a, ctx) 9926 b = _coerce_seq(b, ctx) 9927 return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 9930 def Replace(s, src, dst): 9931 """Replace the first occurrence of
'src' by
'dst' in 's' 9932 >>> r =
Replace(
"aaa",
"a",
"b")
9936 ctx = _get_ctx2(dst, s) 9937 if ctx is None and is_expr(src): 9939 src = _coerce_seq(src, ctx) 9940 dst = _coerce_seq(dst, ctx) 9941 s = _coerce_seq(s, ctx) 9942 return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx) 9944 def IndexOf(s, substr): 9945 return IndexOf(s, substr, IntVal(0)) 9947 def IndexOf(s, substr, offset): 9948 """Retrieve the index of substring within a string starting at a specified offset.
9957 ctx = _get_ctx2(s, substr, ctx) 9958 s = _coerce_seq(s, ctx) 9959 substr = _coerce_seq(substr, ctx) 9961 offset = IntVal(offset, ctx) 9962 return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx) 9965 """Obtain the length of a sequence
's' 9971 return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx) 9974 """Convert string expression to integer
9986 return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx) 9990 """Convert integer expression to string
""" 9993 return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx) 9996 def Re(s, ctx=None): 9997 """The regular expression that accepts sequence
's' 10002 s = _coerce_seq(s, ctx) 10003 return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx) 10008 ## Regular expressions 10010 class ReSortRef(SortRef): 10011 """Regular expression sort.
""" 10016 return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx) 10017 if s is None or isinstance(s, Context): 10019 return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), s.ctx) 10020 raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument") 10023 class ReRef(ExprRef): 10024 """Regular expressions.
""" 10026 def __add__(self, other): 10027 return Union(self, other) 10031 return isinstance(s, ReRef) 10035 """Create regular expression membership test
10044 s = _coerce_seq(s, re.ctx) 10045 return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx) 10048 """Create union of regular expressions.
10053 args = _get_args(args) 10056 _z3_assert(sz > 0, "At least one argument expected.") 10057 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 10062 for i in range(sz): 10063 v[i] = args[i].as_ast() 10064 return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx) 10067 """Create the regular expression accepting one
or more repetitions of argument.
10076 return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx) 10079 """Create the regular expression that optionally accepts the argument.
10088 return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx) 10090 def Complement(re): 10091 """Create the complement regular expression.
""" 10092 return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx) 10095 """Create the regular expression accepting zero
or more repetitions of argument.
10104 return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx) 10106 def Loop(re, lo, hi=0): 10107 """Create the regular expression accepting between a lower
and upper bound repetitions
10108 >>> re =
Loop(
Re(
"a"), 1, 3)
10116 return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)
Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o)
Return the parameter description set for the given optimize object.
Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i)
Return the name of the i probe.
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)
Return objectives on the optimization context. If the objective function is a max-sat objective it is...
def fpToIEEEBV(x, ctx=None)
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
def simplify(a, arguments, keywords)
Utils.
Z3_bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
def FreshReal(prefix='b', ctx=None)
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form: ...
def update_rule(self, head, body, name)
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
def args2params(arguments, keywords, ctx=None)
def get_cover_delta(self, level, predicate)
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a bound variable.
def upper_values(self, obj)
def RatVal(a, b, ctx=None)
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
def __getitem__(self, idx)
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
def RealVector(prefix, sz, ctx=None)
void Z3_API Z3_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
Z3_bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
expr range(expr const &lo, expr const &hi)
def fpBVToFP(v, sort, ctx=None)
Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o)
Check consistency and produce optimal values.
def FPs(names, fpsort, ctx=None)
def FPVal(sig, exp=None, fps=None, ctx=None)
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context...
def RealVarVector(n, ctx=None)
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
def substitute_vars(t, m)
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
def to_symbol(s, ctx=None)
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
def declare(self, name, args)
def assert_exprs(self, args)
def set_option(args, kws)
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
def IntVal(val, ctx=None)
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
def parse_smt2_string(s, sorts={}, decls={}, ctx=None)
def __init__(self, ctx=None)
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
def fpToFP(a1, a2=None, a3=None, ctx=None)
def assert_exprs(self, args)
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)
Return the name of the idx tactic.
def fpUnsignedToFP(rm, v, sort, ctx=None)
def lower_values(self, obj)
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f)
Convert a Z3_func_decl into Z3_ast. This is just type casting.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
def __deepcopy__(self, memo={})
def register_relation(self, relations)
def fpToUBV(rm, x, s, ctx=None)
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size)
Create a named finite domain sort.
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
def __deepcopy__(self, memo={})
def fpGEQ(a, b, ctx=None)
def PbEq(args, k, ctx=None)
Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
def rule(self, head, body=None, name=None)
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
def fpRem(a, b, ctx=None)
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
Assert a constraint to the fixedpoint context.
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d)
Backtrack one backtracking point.
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p)
Apply tactic t to the goal g using the parameter set p.
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
def is_finite_domain_sort(s)
def z3_error_handler(c, e)
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
def BoolVector(prefix, sz, ctx=None)
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
def Array(name, dom, rng)
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
def If(a, b, c, ctx=None)
def BitVecVal(val, bv, ctx=None)
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
def Cond(p, t1, t2, ctx=None)
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d)
Create a backtracking point.
def fpMax(a, b, ctx=None)
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
def get_rule_names_along_trace(self)
def __init__(self, fixedpoint=None, ctx=None)
def simplify_param_descrs()
def fpToFPUnsigned(rm, x, s, ctx=None)
def fpMul(rm, a, b, ctx=None)
def BitVec(name, bv, ctx=None)
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
def FiniteDomainSort(name, sz, ctx=None)
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
def binary_interpolant(a, b, p=None, ctx=None)
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.
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. ...
Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s)
Convert a Z3_sort into Z3_ast. This is just type casting.
def add_soft(self, arg, weight="1", id=None)
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
void Z3_API Z3_enable_trace(Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
def __deepcopy__(self, memo={})
def Implies(a, b, ctx=None)
def __init__(self, tactic, ctx=None)
def __deepcopy__(self, memo={})
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
def apply(self, goal, arguments, keywords)
def solve(args, keywords)
def __init__(self, opt, value, is_max)
def check(self, assumptions)
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
def StringVal(s, ctx=None)
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
def __call__(self, goal, arguments, keywords)
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
def FiniteDomainVal(val, sort, ctx=None)
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
def FPSort(ebits, sbits, ctx=None)
def prove(claim, keywords)
def DeclareSort(name, ctx=None)
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
def Ints(names, ctx=None)
def Interpolant(a, ctx=None)
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
def is_finite_domain_value(a)
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
def FreshBool(prefix='b', ctx=None)
def probe_description(name, ctx=None)
def get_rules_along_trace(self)
def __deepcopy__(self, memo={})
def tactic_description(name, ctx=None)
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
def FP(name, fpsort, ctx=None)
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.
def fpToSBV(rm, x, s, ctx=None)
def fpDiv(rm, a, b, ctx=None)
def BitVecs(names, bv, ctx=None)
def translate(self, target)
def from_file(self, filename)
Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t *r)
Store the size of the sort in r. Return Z3_FALSE if the call failed. That is, Z3_get_sort_kind(s) == ...
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 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.
def TryFor(t, ms, ctx=None)
def sequence_interpolant(v, p=None, ctx=None)
Z3_string Z3_API Z3_get_parser_error(Z3_context c)
Retrieve that last error message information generated from parsing.
def __init__(self, ast, ctx=None)
def convert_model(self, model, idx=0)
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_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.
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_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.
def tree_interpolant(pat, p=None, ctx=None)
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)