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. """ 119 if len(args) == 1
and (isinstance(args[0], tuple)
or isinstance(args[0], list)):
121 elif len(args) == 1
and (isinstance(args[0], set)
or isinstance(args[0], AstVector)):
122 return [arg
for arg
in args[0]]
128 def _to_param_value(val):
129 if isinstance(val, bool):
143 """A Context manages all other Z3 objects, global configuration options, etc. 145 Z3Py uses a default global context. For most applications this is sufficient. 146 An application may use multiple Z3 contexts. Objects created in one context 147 cannot be used in another one. However, several objects may be "translated" from 148 one context to another. It is not safe to access Z3 objects from multiple threads. 149 The only exception is the method `interrupt()` that can be used to interrupt() a long 151 The initialization method receives global configuration options for the new context. 155 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
178 """Return a reference to the actual C pointer to the Z3 context.""" 182 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions. 184 This method can be invoked from a thread different from the one executing the 185 interruptable procedure. 193 """Return a reference to the global Z3 context. 196 >>> x.ctx == main_ctx() 201 >>> x2 = Real('x', c) 208 if _main_ctx
is None:
219 """Set Z3 global (or module) parameters. 221 >>> set_param(precision=10) 224 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
228 if not set_pp_option(k, v):
242 """Reset all global (or module) parameters. 247 """Alias for 'set_param' for backward compatibility. 252 """Return the value of a Z3 global (or module) parameter 254 >>> get_param('nlsat.reorder') 257 ptr = (ctypes.c_char_p * 1)()
259 r = z3core._to_pystr(ptr[0])
261 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
271 """Superclass for all Z3 objects that have support for pretty printing.""" 276 """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions.""" 283 if self.
ctx.ref()
is not None:
287 return _to_ast_ref(self.
ast, self.
ctx)
290 return obj_to_string(self)
293 return obj_to_string(self)
296 return self.
eq(other)
309 elif is_eq(self)
and self.num_args() == 2:
310 return self.arg(0).
eq(self.arg(1))
312 raise Z3Exception(
"Symbolic expressions cannot be cast to concrete Boolean values.")
315 """Return a string representing the AST node in s-expression notation. 318 >>> ((x + 1)*x).sexpr() 324 """Return a pointer to the corresponding C Z3_ast object.""" 328 """Return unique identifier for object. It can be used for hash-tables and maps.""" 332 """Return a reference to the C context where this AST node is stored.""" 333 return self.
ctx.ref()
336 """Return `True` if `self` and `other` are structurally identical. 343 >>> n1 = simplify(n1) 344 >>> n2 = simplify(n2) 349 _z3_assert(
is_ast(other),
"Z3 AST expected")
353 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 359 >>> # Nodes in different contexts can't be mixed. 360 >>> # However, we can translate nodes from one context to another. 361 >>> x.translate(c2) + y 365 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
369 """Return a hashcode for the `self`. 371 >>> n1 = simplify(Int('x') + 1) 372 >>> n2 = simplify(2 + Int('x') - 1) 373 >>> n1.hash() == n2.hash() 379 """Return `True` if `a` is an AST node. 383 >>> is_ast(IntVal(10)) 387 >>> is_ast(BoolSort()) 389 >>> is_ast(Function('f', IntSort(), IntSort())) 396 return isinstance(a, AstRef)
399 """Return `True` if `a` and `b` are structurally identical AST nodes. 409 >>> eq(simplify(x + 1), simplify(1 + x)) 416 def _ast_kind(ctx, a):
421 def _ctx_from_ast_arg_list(args, default_ctx=None):
429 _z3_assert(ctx == a.ctx,
"Context mismatch")
434 def _ctx_from_ast_args(*args):
435 return _ctx_from_ast_arg_list(args)
437 def _to_func_decl_array(args):
439 _args = (FuncDecl * sz)()
441 _args[i] = args[i].as_func_decl()
444 def _to_ast_array(args):
448 _args[i] = args[i].as_ast()
451 def _to_ref_array(ref, args):
455 _args[i] = args[i].as_ast()
458 def _to_ast_ref(a, ctx):
459 k = _ast_kind(ctx, a)
461 return _to_sort_ref(a, ctx)
462 elif k == Z3_FUNC_DECL_AST:
463 return _to_func_decl_ref(a, ctx)
465 return _to_expr_ref(a, ctx)
473 def _sort_kind(ctx, s):
477 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.""" 485 """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts. 488 >>> b.kind() == Z3_BOOL_SORT 490 >>> b.kind() == Z3_INT_SORT 492 >>> A = ArraySort(IntSort(), IntSort()) 493 >>> A.kind() == Z3_ARRAY_SORT 495 >>> A.kind() == Z3_INT_SORT 498 return _sort_kind(self.
ctx, self.
ast)
501 """Return `True` if `self` is a subsort of `other`. 503 >>> IntSort().subsort(RealSort()) 509 """Try to cast `val` as an element of sort `self`. 511 This method is used in Z3Py to convert Python objects such as integers, 512 floats, longs and strings into Z3 expressions. 515 >>> RealSort().cast(x) 519 _z3_assert(
is_expr(val),
"Z3 expression expected")
520 _z3_assert(self.
eq(val.sort()),
"Sort mismatch")
524 """Return the name (string) of sort `self`. 526 >>> BoolSort().name() 528 >>> ArraySort(IntSort(), IntSort()).name() 534 """Return `True` if `self` and `other` are the same Z3 sort. 537 >>> p.sort() == BoolSort() 539 >>> p.sort() == IntSort() 547 """Return `True` if `self` and `other` are not the same Z3 sort. 550 >>> p.sort() != BoolSort() 552 >>> p.sort() != IntSort() 559 return AstRef.__hash__(self)
562 """Return `True` if `s` is a Z3 sort. 564 >>> is_sort(IntSort()) 566 >>> is_sort(Int('x')) 568 >>> is_expr(Int('x')) 571 return isinstance(s, SortRef)
573 def _to_sort_ref(s, ctx):
575 _z3_assert(isinstance(s, Sort),
"Z3 Sort expected")
576 k = _sort_kind(ctx, s)
577 if k == Z3_BOOL_SORT:
579 elif k == Z3_INT_SORT
or k == Z3_REAL_SORT:
581 elif k == Z3_BV_SORT:
583 elif k == Z3_ARRAY_SORT:
585 elif k == Z3_DATATYPE_SORT:
587 elif k == Z3_FINITE_DOMAIN_SORT:
589 elif k == Z3_FLOATING_POINT_SORT:
591 elif k == Z3_ROUNDING_MODE_SORT:
596 return _to_sort_ref(
Z3_get_sort(ctx.ref(), a), ctx)
599 """Create a new uninterpred sort named `name`. 601 If `ctx=None`, then the new sort is declared in the global Z3Py context. 603 >>> A = DeclareSort('A') 604 >>> a = Const('a', A) 605 >>> b = Const('b', A) 623 """Function declaration. Every constant and function have an associated declaration. 625 The declaration assigns a name, a sort (i.e., type), and for function 626 the sort (i.e., type) of each of its arguments. Note that, in Z3, 627 a constant is a function with 0 arguments. 639 """Return the name of the function declaration `self`. 641 >>> f = Function('f', IntSort(), IntSort()) 644 >>> isinstance(f.name(), str) 650 """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0. 652 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 659 """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`. 661 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 668 _z3_assert(i < self.
arity(),
"Index out of bounds")
672 """Return the sort of the range of a function declaration. For constants, this is the sort of the constant. 674 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 681 """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc. 684 >>> d = (x + 1).decl() 685 >>> d.kind() == Z3_OP_ADD 687 >>> d.kind() == Z3_OP_MUL 695 result = [
None for i
in range(n) ]
698 if k == Z3_PARAMETER_INT:
700 elif k == Z3_PARAMETER_DOUBLE:
702 elif k == Z3_PARAMETER_RATIONAL:
704 elif k == Z3_PARAMETER_SYMBOL:
706 elif k == Z3_PARAMETER_SORT:
708 elif k == Z3_PARAMETER_AST:
710 elif k == Z3_PARAMETER_FUNC_DECL:
717 """Create a Z3 application expression using the function `self`, and the given arguments. 719 The arguments must be Z3 expressions. This method assumes that 720 the sorts of the elements in `args` match the sorts of the 721 domain. Limited coersion is supported. For example, if 722 args[0] is a Python integer, and the function expects a Z3 723 integer, then the argument is automatically converted into a 726 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 734 args = _get_args(args)
737 _z3_assert(num == self.
arity(),
"Incorrect number of arguments to %s" % self)
738 _args = (Ast * num)()
743 tmp = self.
domain(i).cast(args[i])
745 _args[i] = tmp.as_ast()
749 """Return `True` if `a` is a Z3 function declaration. 751 >>> f = Function('f', IntSort(), IntSort()) 758 return isinstance(a, FuncDeclRef)
761 """Create a new Z3 uninterpreted function with the given sorts. 763 >>> f = Function('f', IntSort(), IntSort()) 769 _z3_assert(len(sig) > 0,
"At least two arguments expected")
773 _z3_assert(
is_sort(rng),
"Z3 sort expected")
774 dom = (Sort * arity)()
775 for i
in range(arity):
777 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
782 def _to_func_decl_ref(a, ctx):
792 """Constraints, formulas and terms are expressions in Z3. 794 Expressions are ASTs. Every expression has a sort. 795 There are three main kinds of expressions: 796 function applications, quantifiers and bounded variables. 797 A constant is a function application with 0 arguments. 798 For quantifier free problems, all expressions are 799 function applications. 808 """Return the sort of expression `self`. 820 """Shorthand for `self.sort().kind()`. 822 >>> a = Array('a', IntSort(), IntSort()) 823 >>> a.sort_kind() == Z3_ARRAY_SORT 825 >>> a.sort_kind() == Z3_INT_SORT 828 return self.
sort().kind()
831 """Return a Z3 expression that represents the constraint `self == other`. 833 If `other` is `None`, then this method simply returns `False`. 844 a, b = _coerce_exprs(self, other)
849 return AstRef.__hash__(self)
852 """Return a Z3 expression that represents the constraint `self != other`. 854 If `other` is `None`, then this method simply returns `True`. 865 a, b = _coerce_exprs(self, other)
866 _args, sz = _to_ast_array((a, b))
873 """Return the Z3 function declaration associated with a Z3 application. 875 >>> f = Function('f', IntSort(), IntSort()) 884 _z3_assert(
is_app(self),
"Z3 application expected")
888 """Return the number of arguments of a Z3 application. 892 >>> (a + b).num_args() 894 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 900 _z3_assert(
is_app(self),
"Z3 application expected")
904 """Return argument `idx` of the application `self`. 906 This method assumes that `self` is a function application with at least `idx+1` arguments. 910 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 920 _z3_assert(
is_app(self),
"Z3 application expected")
921 _z3_assert(idx < self.
num_args(),
"Invalid argument index")
925 """Return a list containing the children of the given expression 929 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 939 def _to_expr_ref(a, ctx):
940 if isinstance(a, Pattern):
944 if k == Z3_QUANTIFIER_AST:
947 if sk == Z3_BOOL_SORT:
949 if sk == Z3_INT_SORT:
950 if k == Z3_NUMERAL_AST:
953 if sk == Z3_REAL_SORT:
954 if k == Z3_NUMERAL_AST:
956 if _is_algebraic(ctx, a):
960 if k == Z3_NUMERAL_AST:
964 if sk == Z3_ARRAY_SORT:
966 if sk == Z3_DATATYPE_SORT:
968 if sk == Z3_FLOATING_POINT_SORT:
969 if k == Z3_APP_AST
and _is_numeral(ctx, a):
973 if sk == Z3_FINITE_DOMAIN_SORT:
974 if k == Z3_NUMERAL_AST:
978 if sk == Z3_ROUNDING_MODE_SORT:
980 if sk == Z3_SEQ_SORT:
986 def _coerce_expr_merge(s, a):
999 _z3_assert(s1.ctx == s.ctx,
"context mismatch")
1000 _z3_assert(
False,
"sort mismatch")
1004 def _coerce_exprs(a, b, ctx=None):
1006 a = _py2expr(a, ctx)
1007 b = _py2expr(b, ctx)
1009 s = _coerce_expr_merge(s, a)
1010 s = _coerce_expr_merge(s, b)
1016 def _reduce(f, l, a):
1022 def _coerce_expr_list(alist, ctx=None):
1029 alist = [ _py2expr(a, ctx)
for a
in alist ]
1030 s = _reduce(_coerce_expr_merge, alist,
None)
1031 return [ s.cast(a)
for a
in alist ]
1034 """Return `True` if `a` is a Z3 expression. 1041 >>> is_expr(IntSort()) 1045 >>> is_expr(IntVal(1)) 1048 >>> is_expr(ForAll(x, x >= 0)) 1050 >>> is_expr(FPVal(1.0)) 1053 return isinstance(a, ExprRef)
1056 """Return `True` if `a` is a Z3 function application. 1058 Note that, constants are function applications with 0 arguments. 1065 >>> is_app(IntSort()) 1069 >>> is_app(IntVal(1)) 1072 >>> is_app(ForAll(x, x >= 0)) 1075 if not isinstance(a, ExprRef):
1077 k = _ast_kind(a.ctx, a)
1078 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
1081 """Return `True` if `a` is Z3 constant/variable expression. 1090 >>> is_const(IntVal(1)) 1093 >>> is_const(ForAll(x, x >= 0)) 1096 return is_app(a)
and a.num_args() == 0
1099 """Return `True` if `a` is variable. 1101 Z3 uses de-Bruijn indices for representing bound variables in 1109 >>> f = Function('f', IntSort(), IntSort()) 1110 >>> # Z3 replaces x with bound variables when ForAll is executed. 1111 >>> q = ForAll(x, f(x) == x) 1117 >>> is_var(b.arg(1)) 1120 return is_expr(a)
and _ast_kind(a.ctx, a) == Z3_VAR_AST
1123 """Return the de-Bruijn index of the Z3 bounded variable `a`. 1131 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1132 >>> # Z3 replaces x and y with bound variables when ForAll is executed. 1133 >>> q = ForAll([x, y], f(x, y) == x + y) 1135 f(Var(1), Var(0)) == Var(1) + Var(0) 1139 >>> v1 = b.arg(0).arg(0) 1140 >>> v2 = b.arg(0).arg(1) 1145 >>> get_var_index(v1) 1147 >>> get_var_index(v2) 1151 _z3_assert(
is_var(a),
"Z3 bound variable expected")
1155 """Return `True` if `a` is an application of the given kind `k`. 1159 >>> is_app_of(n, Z3_OP_ADD) 1161 >>> is_app_of(n, Z3_OP_MUL) 1164 return is_app(a)
and a.decl().kind() == k
1166 def If(a, b, c, ctx=None):
1167 """Create a Z3 if-then-else expression. 1171 >>> max = If(x > y, x, y) 1177 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1178 return Cond(a, b, c, ctx)
1180 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1183 b, c = _coerce_exprs(b, c, ctx)
1185 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1186 return _to_expr_ref(
Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1189 """Create a Z3 distinct expression. 1196 >>> Distinct(x, y, z) 1198 >>> simplify(Distinct(x, y, z)) 1200 >>> simplify(Distinct(x, y, z), blast_distinct=True) 1201 And(Not(x == y), Not(x == z), Not(y == z)) 1203 args = _get_args(args)
1204 ctx = _ctx_from_ast_arg_list(args)
1206 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1207 args = _coerce_expr_list(args, ctx)
1208 _args, sz = _to_ast_array(args)
1211 def _mk_bin(f, a, b):
1214 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1215 args[0] = a.as_ast()
1216 args[1] = b.as_ast()
1217 return f(a.ctx.ref(), 2, args)
1220 """Create a constant of the given sort. 1222 >>> Const('x', IntSort()) 1226 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
1231 """Create a several constants of the given sort. 1233 `names` is a string containing the names of all constants to be created. 1234 Blank spaces separate the names of different constants. 1236 >>> x, y, z = Consts('x y z', IntSort()) 1240 if isinstance(names, str):
1241 names = names.split(
" ")
1242 return [
Const(name, sort)
for name
in names]
1245 """Create a Z3 free variable. Free variables are used to create quantified formulas. 1247 >>> Var(0, IntSort()) 1249 >>> eq(Var(0, IntSort()), Var(0, BoolSort())) 1253 _z3_assert(
is_sort(s),
"Z3 sort expected")
1254 return _to_expr_ref(
Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1258 Create a real free variable. Free variables are used to create quantified formulas. 1259 They are also used to create polynomials. 1268 Create a list of Real free variables. 1269 The variables have ids: 0, 1, ..., n-1 1271 >>> x0, x1, x2, x3 = RealVarVector(4) 1286 """Try to cast `val` as a Boolean. 1288 >>> x = BoolSort().cast(True) 1298 if isinstance(val, bool):
1302 _z3_assert(
is_expr(val),
"True, False or Z3 Boolean expression expected. Received %s" % val)
1303 if not self.
eq(val.sort()):
1304 _z3_assert(self.
eq(val.sort()),
"Value cannot be converted into a Z3 Boolean value")
1308 return isinstance(other, ArithSortRef)
1318 """All Boolean expressions are instances of this class.""" 1326 """Create the Z3 expression `self * other`. 1332 return If(self, other, 0)
1336 """Return `True` if `a` is a Z3 Boolean expression. 1342 >>> is_bool(And(p, q)) 1350 return isinstance(a, BoolRef)
1353 """Return `True` if `a` is the Z3 true expression. 1358 >>> is_true(simplify(p == p)) 1363 >>> # True is a Python Boolean expression 1370 """Return `True` if `a` is the Z3 false expression. 1377 >>> is_false(BoolVal(False)) 1383 """Return `True` if `a` is a Z3 and expression. 1385 >>> p, q = Bools('p q') 1386 >>> is_and(And(p, q)) 1388 >>> is_and(Or(p, q)) 1394 """Return `True` if `a` is a Z3 or expression. 1396 >>> p, q = Bools('p q') 1399 >>> is_or(And(p, q)) 1405 """Return `True` if `a` is a Z3 not expression. 1416 """Return `True` if `a` is a Z3 equality expression. 1418 >>> x, y = Ints('x y') 1425 """Return `True` if `a` is a Z3 distinct expression. 1427 >>> x, y, z = Ints('x y z') 1428 >>> is_distinct(x == y) 1430 >>> is_distinct(Distinct(x, y, z)) 1436 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. 1440 >>> p = Const('p', BoolSort()) 1443 >>> r = Function('r', IntSort(), IntSort(), BoolSort()) 1450 return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx) 1452 def BoolVal(val, ctx=None): 1453 """Return the Boolean value `
True`
or `
False`. If `ctx=
None`, then the
global context
is used.
1466 return BoolRef(Z3_mk_false(ctx.ref()), ctx) 1468 return BoolRef(Z3_mk_true(ctx.ref()), ctx) 1470 def Bool(name, ctx=None): 1471 """Return a Boolean constant named `name`. If `ctx=
None`, then the
global context
is used.
1479 return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx) 1481 def Bools(names, ctx=None): 1482 """Return a tuple of Boolean constants.
1484 `names`
is a single string containing all names separated by blank spaces.
1485 If `ctx=
None`, then the
global context
is used.
1487 >>> p, q, r =
Bools(
'p q r')
1488 >>>
And(p,
Or(q, r))
1492 if isinstance(names, str): 1493 names = names.split(" ") 1494 return [Bool(name, ctx) for name in names] 1496 def BoolVector(prefix, sz, ctx=None): 1497 """Return a list of Boolean constants of size `sz`.
1499 The constants are named using the given prefix.
1500 If `ctx=
None`, then the
global context
is used.
1506 And(p__0, p__1, p__2)
1508 return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ] 1510 def FreshBool(prefix='b', ctx=None): 1511 """Return a fresh Boolean constant
in the given context using the given prefix.
1513 If `ctx=
None`, then the
global context
is used.
1521 return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx) 1523 def Implies(a, b, ctx=None): 1524 """Create a Z3 implies expression.
1526 >>> p, q =
Bools(
'p q')
1532 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 1536 return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 1538 def Xor(a, b, ctx=None): 1539 """Create a Z3 Xor expression.
1541 >>> p, q =
Bools(
'p q')
1547 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 1551 return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 1553 def Not(a, ctx=None): 1554 """Create a Z3
not expression
or probe.
1562 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) 1564 # Not is also used to build probes 1565 return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx) 1569 return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx) 1571 def _has_probe(args): 1572 """Return `
True`
if one of the elements of the given collection
is a Z3 probe.
""" 1579 """Create a Z3
and-expression
or and-probe.
1581 >>> p, q, r =
Bools(
'p q r')
1586 And(p__0, p__1, p__2, p__3, p__4)
1590 last_arg = args[len(args)-1] 1591 if isinstance(last_arg, Context): 1592 ctx = args[len(args)-1] 1593 args = args[:len(args)-1] 1594 elif len(args) == 1 and isinstance(args[0], AstVector): 1596 args = [a for a in args[0]] 1599 args = _get_args(args) 1600 ctx_args = _ctx_from_ast_arg_list(args, ctx) 1602 _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") 1603 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") 1604 if _has_probe(args): 1605 return _probe_and(args, ctx) 1607 args = _coerce_expr_list(args, ctx) 1608 _args, sz = _to_ast_array(args) 1609 return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx) 1612 """Create a Z3
or-expression
or or-probe.
1614 >>> p, q, r =
Bools(
'p q r')
1619 Or(p__0, p__1, p__2, p__3, p__4)
1623 last_arg = args[len(args)-1] 1624 if isinstance(last_arg, Context): 1625 ctx = args[len(args)-1] 1626 args = args[:len(args)-1] 1629 args = _get_args(args) 1630 ctx_args = _ctx_from_ast_arg_list(args, ctx) 1632 _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch") 1633 _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe") 1634 if _has_probe(args): 1635 return _probe_or(args, ctx) 1637 args = _coerce_expr_list(args, ctx) 1638 _args, sz = _to_ast_array(args) 1639 return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx) 1641 ######################################### 1645 ######################################### 1647 class PatternRef(ExprRef): 1648 """Patterns are hints
for quantifier instantiation.
1650 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1653 return Z3_pattern_to_ast(self.ctx_ref(), self.ast) 1656 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1659 """Return `
True`
if `a`
is a Z3 pattern (hint
for quantifier instantiation.
1661 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1665 >>> q =
ForAll(x, f(x) == 0, patterns = [ f(x) ])
1668 >>> q.num_patterns()
1675 return isinstance(a, PatternRef) 1677 def MultiPattern(*args): 1678 """Create a Z3 multi-pattern using the given expressions `*args`
1680 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1688 >>> q.num_patterns()
1696 _z3_assert(len(args) > 0, "At least one argument expected") 1697 _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected") 1699 args, sz = _to_ast_array(args) 1700 return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx) 1702 def _to_pattern(arg): 1706 return MultiPattern(arg) 1708 ######################################### 1712 ######################################### 1714 class QuantifierRef(BoolRef): 1715 """Universally
and Existentially quantified formulas.
""" 1721 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1724 """Return the Boolean sort.
""" 1725 return BoolSort(self.ctx) 1727 def is_forall(self): 1728 """Return `
True`
if `self`
is a universal quantifier.
1732 >>> q =
ForAll(x, f(x) == 0)
1735 >>> q =
Exists(x, f(x) != 0)
1739 return Z3_is_quantifier_forall(self.ctx_ref(), self.ast) 1742 """Return the weight annotation of `self`.
1746 >>> q =
ForAll(x, f(x) == 0)
1749 >>> q =
ForAll(x, f(x) == 0, weight=10)
1753 return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast)) 1755 def num_patterns(self): 1756 """Return the number of patterns (i.e., quantifier instantiation hints)
in `self`.
1761 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1762 >>> q.num_patterns()
1765 return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast)) 1767 def pattern(self, idx): 1768 """Return a pattern (i.e., quantifier instantiation hints)
in `self`.
1773 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1774 >>> q.num_patterns()
1782 _z3_assert(idx < self.num_patterns(), "Invalid pattern idx") 1783 return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1785 def num_no_patterns(self): 1786 """Return the number of no-patterns.
""" 1787 return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast) 1789 def no_pattern(self, idx): 1790 """Return a no-pattern.
""" 1792 _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx") 1793 return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1796 """Return the expression being quantified.
1800 >>> q =
ForAll(x, f(x) == 0)
1804 return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx) 1807 """Return the number of variables bounded by this quantifier.
1812 >>> q =
ForAll([x, y], f(x, y) >= x)
1816 return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast)) 1818 def var_name(self, idx): 1819 """Return a string representing a name used when displaying the quantifier.
1824 >>> q =
ForAll([x, y], f(x, y) >= x)
1831 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1832 return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx)) 1834 def var_sort(self, idx): 1835 """Return the sort of a bound variable.
1840 >>> q =
ForAll([x, y], f(x, y) >= x)
1847 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1848 return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx) 1851 """Return a list containing a single element self.
body()
1855 >>> q =
ForAll(x, f(x) == 0)
1859 return [ self.body() ] 1861 def is_quantifier(a): 1862 """Return `
True`
if `a`
is a Z3 quantifier.
1866 >>> q =
ForAll(x, f(x) == 0)
1872 return isinstance(a, QuantifierRef) 1874 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 1876 _z3_assert(is_bool(body), "Z3 expression expected") 1877 _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)") 1878 _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected") 1879 _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions") 1886 _vs = (Ast * num_vars)() 1887 for i in range(num_vars): 1888 ## TODO: Check if is constant 1889 _vs[i] = vs[i].as_ast() 1890 patterns = [ _to_pattern(p) for p in patterns ] 1891 num_pats = len(patterns) 1892 _pats = (Pattern * num_pats)() 1893 for i in range(num_pats): 1894 _pats[i] = patterns[i].ast 1895 _no_pats, num_no_pats = _to_ast_array(no_patterns) 1896 qid = to_symbol(qid, ctx) 1897 skid = to_symbol(skid, ctx) 1898 return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid, 1901 num_no_pats, _no_pats, 1902 body.as_ast()), ctx) 1904 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 1905 """Create a Z3 forall formula.
1907 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
1909 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1914 >>>
ForAll([x, y], f(x, y) >= x)
1915 ForAll([x, y], f(x, y) >= x)
1916 >>>
ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
1917 ForAll([x, y], f(x, y) >= x)
1918 >>>
ForAll([x, y], f(x, y) >= x, weight=10)
1919 ForAll([x, y], f(x, y) >= x)
1921 return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns) 1923 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 1924 """Create a Z3 exists formula.
1926 The parameters `weight`, `qif`, `skid`, `patterns`
and `no_patterns` are optional annotations.
1928 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1933 >>> q =
Exists([x, y], f(x, y) >= x, skid=
"foo")
1935 Exists([x, y], f(x, y) >= x)
1938 >>> r =
Tactic(
'nnf')(q).as_expr()
1942 return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns) 1944 ######################################### 1948 ######################################### 1950 class ArithSortRef(SortRef): 1951 """Real
and Integer sorts.
""" 1954 """Return `
True`
if `self`
is of the sort Real.
1965 return self.kind() == Z3_REAL_SORT 1968 """Return `
True`
if `self`
is of the sort Integer.
1979 return self.kind() == Z3_INT_SORT 1981 def subsort(self, other): 1982 """Return `
True`
if `self`
is a subsort of `other`.
""" 1983 return self.is_int() and is_arith_sort(other) and other.is_real() 1985 def cast(self, val): 1986 """Try to cast `val`
as an Integer
or Real.
2001 _z3_assert(self.ctx == val.ctx, "Context mismatch") 2005 if val_s.is_int() and self.is_real(): 2007 if val_s.is_bool() and self.is_int(): 2008 return If(val, 1, 0) 2009 if val_s.is_bool() and self.is_real(): 2010 return ToReal(If(val, 1, 0)) 2012 _z3_assert(False, "Z3 Integer/Real expression expected" ) 2015 return IntVal(val, self.ctx) 2017 return RealVal(val, self.ctx) 2019 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self) 2021 def is_arith_sort(s): 2022 """Return `
True`
if s
is an arithmetical sort (type).
2030 >>> n =
Int(
'x') + 1
2034 return isinstance(s, ArithSortRef) 2036 class ArithRef(ExprRef): 2037 """Integer
and Real expressions.
""" 2040 """Return the sort (type) of the arithmetical expression `self`.
2047 return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 2050 """Return `
True`
if `self`
is an integer expression.
2061 return self.sort().is_int() 2064 """Return `
True`
if `self`
is an real expression.
2072 return self.sort().is_real() 2074 def __add__(self, other): 2075 """Create the Z3 expression `self + other`.
2084 a, b = _coerce_exprs(self, other) 2085 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx) 2087 def __radd__(self, other): 2088 """Create the Z3 expression `other + self`.
2094 a, b = _coerce_exprs(self, other) 2095 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx) 2097 def __mul__(self, other): 2098 """Create the Z3 expression `self * other`.
2107 a, b = _coerce_exprs(self, other) 2108 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx) 2110 def __rmul__(self, other): 2111 """Create the Z3 expression `other * self`.
2117 a, b = _coerce_exprs(self, other) 2118 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx) 2120 def __sub__(self, other): 2121 """Create the Z3 expression `self - other`.
2130 a, b = _coerce_exprs(self, other) 2131 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx) 2133 def __rsub__(self, other): 2134 """Create the Z3 expression `other - self`.
2140 a, b = _coerce_exprs(self, other) 2141 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx) 2143 def __pow__(self, other): 2144 """Create the Z3 expression `self**other` (**
is the power operator).
2154 a, b = _coerce_exprs(self, other) 2155 return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2157 def __rpow__(self, other): 2158 """Create the Z3 expression `other**self` (**
is the power operator).
2168 a, b = _coerce_exprs(self, other) 2169 return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2171 def __div__(self, other): 2172 """Create the Z3 expression `other/self`.
2191 a, b = _coerce_exprs(self, other) 2192 return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2194 def __truediv__(self, other): 2195 """Create the Z3 expression `other/self`.
""" 2196 return self.__div__(other) 2198 def __rdiv__(self, other): 2199 """Create the Z3 expression `other/self`.
2212 a, b = _coerce_exprs(self, other) 2213 return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2215 def __rtruediv__(self, other): 2216 """Create the Z3 expression `other/self`.
""" 2217 return self.__rdiv__(other) 2219 def __mod__(self, other): 2220 """Create the Z3 expression `other%self`.
2229 a, b = _coerce_exprs(self, other) 2231 _z3_assert(a.is_int(), "Z3 integer expression expected") 2232 return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2234 def __rmod__(self, other): 2235 """Create the Z3 expression `other%self`.
2241 a, b = _coerce_exprs(self, other) 2243 _z3_assert(a.is_int(), "Z3 integer expression expected") 2244 return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2247 """Return an expression representing `-self`.
2255 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx) 2266 def __le__(self, other): 2267 """Create the Z3 expression `other <= self`.
2269 >>> x, y =
Ints(
'x y')
2276 a, b = _coerce_exprs(self, other) 2277 return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2279 def __lt__(self, other): 2280 """Create the Z3 expression `other < self`.
2282 >>> x, y =
Ints(
'x y')
2289 a, b = _coerce_exprs(self, other) 2290 return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2292 def __gt__(self, other): 2293 """Create the Z3 expression `other > self`.
2295 >>> x, y =
Ints(
'x y')
2302 a, b = _coerce_exprs(self, other) 2303 return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2305 def __ge__(self, other): 2306 """Create the Z3 expression `other >= self`.
2308 >>> x, y =
Ints(
'x y')
2315 a, b = _coerce_exprs(self, other) 2316 return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2319 """Return `
True`
if `a`
is an arithmetical expression.
2336 return isinstance(a, ArithRef) 2339 """Return `
True`
if `a`
is an integer expression.
2354 return is_arith(a) and a.is_int() 2357 """Return `
True`
if `a`
is a real expression.
2372 return is_arith(a) and a.is_real() 2374 def _is_numeral(ctx, a): 2375 return Z3_is_numeral_ast(ctx.ref(), a) 2377 def _is_algebraic(ctx, a): 2378 return Z3_is_algebraic_number(ctx.ref(), a) 2380 def is_int_value(a): 2381 """Return `
True`
if `a`
is an integer value of sort Int.
2389 >>> n =
Int(
'x') + 1
2401 return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast()) 2403 def is_rational_value(a): 2404 """Return `
True`
if `a`
is rational value of sort Real.
2414 >>> n =
Real(
'x') + 1
2422 return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast()) 2424 def is_algebraic_value(a): 2425 """Return `
True`
if `a`
is an algerbraic value of sort Real.
2435 return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast()) 2438 """Return `
True`
if `a`
is an expression of the form b + c.
2440 >>> x, y =
Ints(
'x y')
2446 return is_app_of(a, Z3_OP_ADD) 2449 """Return `
True`
if `a`
is an expression of the form b * c.
2451 >>> x, y =
Ints(
'x y')
2457 return is_app_of(a, Z3_OP_MUL) 2460 """Return `
True`
if `a`
is an expression of the form b - c.
2462 >>> x, y =
Ints(
'x y')
2468 return is_app_of(a, Z3_OP_SUB) 2471 """Return `
True`
if `a`
is an expression of the form b / c.
2473 >>> x, y =
Reals(
'x y')
2478 >>> x, y =
Ints(
'x y')
2484 return is_app_of(a, Z3_OP_DIV) 2487 """Return `
True`
if `a`
is an expression of the form b div c.
2489 >>> x, y =
Ints(
'x y')
2495 return is_app_of(a, Z3_OP_IDIV) 2498 """Return `
True`
if `a`
is an expression of the form b % c.
2500 >>> x, y =
Ints(
'x y')
2506 return is_app_of(a, Z3_OP_MOD) 2509 """Return `
True`
if `a`
is an expression of the form b <= c.
2511 >>> x, y =
Ints(
'x y')
2517 return is_app_of(a, Z3_OP_LE) 2520 """Return `
True`
if `a`
is an expression of the form b < c.
2522 >>> x, y =
Ints(
'x y')
2528 return is_app_of(a, Z3_OP_LT) 2531 """Return `
True`
if `a`
is an expression of the form b >= c.
2533 >>> x, y =
Ints(
'x y')
2539 return is_app_of(a, Z3_OP_GE) 2542 """Return `
True`
if `a`
is an expression of the form b > c.
2544 >>> x, y =
Ints(
'x y')
2550 return is_app_of(a, Z3_OP_GT) 2553 """Return `
True`
if `a`
is an expression of the form
IsInt(b).
2561 return is_app_of(a, Z3_OP_IS_INT) 2564 """Return `
True`
if `a`
is an expression of the form
ToReal(b).
2575 return is_app_of(a, Z3_OP_TO_REAL) 2578 """Return `
True`
if `a`
is an expression of the form
ToInt(b).
2589 return is_app_of(a, Z3_OP_TO_INT) 2591 class IntNumRef(ArithRef): 2592 """Integer values.
""" 2595 """Return a Z3 integer numeral
as a Python long (bignum) numeral.
2604 _z3_assert(self.is_int(), "Integer value expected") 2605 return int(self.as_string()) 2607 def as_string(self): 2608 """Return a Z3 integer numeral
as a Python string.
2613 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2615 class RatNumRef(ArithRef): 2616 """Rational values.
""" 2618 def numerator(self): 2619 """ Return the numerator of a Z3 rational numeral.
2631 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx) 2633 def denominator(self): 2634 """ Return the denominator of a Z3 rational numeral.
2642 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx) 2644 def numerator_as_long(self): 2645 """ Return the numerator
as a Python long.
2652 >>> v.numerator_as_long() + 1 == 10000000001
2655 return self.numerator().as_long() 2657 def denominator_as_long(self): 2658 """ Return the denominator
as a Python long.
2663 >>> v.denominator_as_long()
2666 return self.denominator().as_long() 2674 def is_int_value(self): 2675 return self.denominator().is_int() and self.denominator_as_long() == 1 2678 _z3_assert(self.is_int(), "Expected integer fraction") 2679 return self.numerator_as_long() 2681 def as_decimal(self, prec): 2682 """ Return a Z3 rational value
as a string
in decimal notation using at most `prec` decimal places.
2691 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2693 def as_string(self): 2694 """Return a Z3 rational numeral
as a Python string.
2700 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2702 def as_fraction(self): 2703 """Return a Z3 rational
as a Python Fraction object.
2709 return Fraction(self.numerator_as_long(), self.denominator_as_long()) 2711 class AlgebraicNumRef(ArithRef): 2712 """Algebraic irrational values.
""" 2714 def approx(self, precision=10): 2715 """Return a Z3 rational number that approximates the algebraic number `self`.
2716 The result `r`
is such that |r - self| <= 1/10^precision
2720 6838717160008073720548335/4835703278458516698824704
2724 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx) 2725 def as_decimal(self, prec): 2726 """Return a string representation of the algebraic number `self`
in decimal notation using `prec` decimal places
2729 >>> x.as_decimal(10)
2731 >>> x.as_decimal(20)
2732 '1.41421356237309504880?' 2734 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2736 def _py2expr(a, ctx=None): 2737 if isinstance(a, bool): 2738 return BoolVal(a, ctx) 2740 return IntVal(a, ctx) 2741 if isinstance(a, float): 2742 return RealVal(a, ctx) 2744 _z3_assert(False, "Python bool, int, long or float expected") 2746 def IntSort(ctx=None): 2747 """Return the integer sort
in the given context. If `ctx=
None`, then the
global context
is used.
2760 return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx) 2762 def RealSort(ctx=None): 2763 """Return the real sort
in the given context. If `ctx=
None`, then the
global context
is used.
2776 return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx) 2778 def _to_int_str(val): 2779 if isinstance(val, float): 2780 return str(int(val)) 2781 elif isinstance(val, bool): 2788 elif isinstance(val, str): 2791 _z3_assert(False, "Python value cannot be used as a Z3 integer") 2793 def IntVal(val, ctx=None): 2794 """Return a Z3 integer value. If `ctx=
None`, then the
global context
is used.
2802 return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx) 2804 def RealVal(val, ctx=None): 2805 """Return a Z3 real value.
2807 `val` may be a Python int, long, float
or string representing a number
in decimal
or rational notation.
2808 If `ctx=
None`, then the
global context
is used.
2820 return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx) 2822 def RatVal(a, b, ctx=None): 2823 """Return a Z3 rational a/b.
2825 If `ctx=
None`, then the
global context
is used.
2833 _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer") 2834 _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer") 2835 return simplify(RealVal(a, ctx)/RealVal(b, ctx)) 2837 def Q(a, b, ctx=None): 2838 """Return a Z3 rational a/b.
2840 If `ctx=
None`, then the
global context
is used.
2847 return simplify(RatVal(a, b)) 2849 def Int(name, ctx=None): 2850 """Return an integer constant named `name`. If `ctx=
None`, then the
global context
is used.
2859 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx) 2861 def Ints(names, ctx=None): 2862 """Return a tuple of Integer constants.
2864 >>> x, y, z =
Ints(
'x y z')
2869 if isinstance(names, str): 2870 names = names.split(" ") 2871 return [Int(name, ctx) for name in names] 2873 def IntVector(prefix, sz, ctx=None): 2874 """Return a list of integer constants of size `sz`.
2882 return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ] 2884 def FreshInt(prefix='x', ctx=None): 2885 """Return a fresh integer constant
in the given context using the given prefix.
2895 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx) 2897 def Real(name, ctx=None): 2898 """Return a real constant named `name`. If `ctx=
None`, then the
global context
is used.
2907 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx) 2909 def Reals(names, ctx=None): 2910 """Return a tuple of real constants.
2912 >>> x, y, z =
Reals(
'x y z')
2915 >>>
Sum(x, y, z).sort()
2919 if isinstance(names, str): 2920 names = names.split(" ") 2921 return [Real(name, ctx) for name in names] 2923 def RealVector(prefix, sz, ctx=None): 2924 """Return a list of real constants of size `sz`.
2934 return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ] 2936 def FreshReal(prefix='b', ctx=None): 2937 """Return a fresh real constant
in the given context using the given prefix.
2947 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx) 2950 """ Return the Z3 expression
ToReal(a).
2962 _z3_assert(a.is_int(), "Z3 integer expression expected.") 2964 return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx) 2967 """ Return the Z3 expression
ToInt(a).
2979 _z3_assert(a.is_real(), "Z3 real expression expected.") 2981 return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx) 2984 """ Return the Z3 predicate
IsInt(a).
2987 >>>
IsInt(x +
"1/2")
2991 >>>
solve(
IsInt(x +
"1/2"), x > 0, x < 1, x !=
"1/2")
2995 _z3_assert(a.is_real(), "Z3 real expression expected.") 2997 return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx) 2999 def Sqrt(a, ctx=None): 3000 """ Return a Z3 expression which represents the square root of a.
3011 def Cbrt(a, ctx=None): 3012 """ Return a Z3 expression which represents the cubic root of a.
3023 ######################################### 3027 ######################################### 3029 class BitVecSortRef(SortRef): 3030 """Bit-vector sort.
""" 3033 """Return the size (number of bits) of the bit-vector sort `self`.
3039 return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast)) 3041 def subsort(self, other): 3042 return is_bv_sort(other) and self.size() < other.size() 3044 def cast(self, val): 3045 """Try to cast `val`
as a Bit-Vector.
3050 >>> b.cast(10).
sexpr()
3055 _z3_assert(self.ctx == val.ctx, "Context mismatch") 3056 # Idea: use sign_extend if sort of val is a bitvector of smaller size 3059 return BitVecVal(val, self) 3062 """Return
True if `s`
is a Z3 bit-vector sort.
3069 return isinstance(s, BitVecSortRef) 3071 class BitVecRef(ExprRef): 3072 """Bit-vector expressions.
""" 3075 """Return the sort of the bit-vector expression `self`.
3083 return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 3086 """Return the number of bits of the bit-vector expression `self`.
3094 return self.sort().size() 3096 def __add__(self, other): 3097 """Create the Z3 expression `self + other`.
3106 a, b = _coerce_exprs(self, other) 3107 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3109 def __radd__(self, other): 3110 """Create the Z3 expression `other + self`.
3116 a, b = _coerce_exprs(self, other) 3117 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3119 def __mul__(self, other): 3120 """Create the Z3 expression `self * other`.
3129 a, b = _coerce_exprs(self, other) 3130 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3132 def __rmul__(self, other): 3133 """Create the Z3 expression `other * self`.
3139 a, b = _coerce_exprs(self, other) 3140 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3142 def __sub__(self, other): 3143 """Create the Z3 expression `self - other`.
3152 a, b = _coerce_exprs(self, other) 3153 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3155 def __rsub__(self, other): 3156 """Create the Z3 expression `other - self`.
3162 a, b = _coerce_exprs(self, other) 3163 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3165 def __or__(self, other): 3166 """Create the Z3 expression bitwise-
or `self | other`.
3175 a, b = _coerce_exprs(self, other) 3176 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3178 def __ror__(self, other): 3179 """Create the Z3 expression bitwise-
or `other | self`.
3185 a, b = _coerce_exprs(self, other) 3186 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3188 def __and__(self, other): 3189 """Create the Z3 expression bitwise-
and `self & other`.
3198 a, b = _coerce_exprs(self, other) 3199 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3201 def __rand__(self, other): 3202 """Create the Z3 expression bitwise-
or `other & self`.
3208 a, b = _coerce_exprs(self, other) 3209 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3211 def __xor__(self, other): 3212 """Create the Z3 expression bitwise-xor `self ^ other`.
3221 a, b = _coerce_exprs(self, other) 3222 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3224 def __rxor__(self, other): 3225 """Create the Z3 expression bitwise-xor `other ^ self`.
3231 a, b = _coerce_exprs(self, other) 3232 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3244 """Return an expression representing `-self`.
3252 return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx) 3254 def __invert__(self): 3255 """Create the Z3 expression bitwise-
not `~self`.
3263 return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx) 3265 def __div__(self, other): 3266 """Create the Z3 expression (signed) division `self / other`.
3268 Use the function
UDiv()
for unsigned division.
3281 a, b = _coerce_exprs(self, other) 3282 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3284 def __truediv__(self, other): 3285 """Create the Z3 expression (signed) division `self / other`.
""" 3286 return self.__div__(other) 3288 def __rdiv__(self, other): 3289 """Create the Z3 expression (signed) division `other / self`.
3291 Use the function
UDiv()
for unsigned division.
3296 >>> (10 / x).
sexpr()
3297 '(bvsdiv #x0000000a x)' 3299 '(bvudiv #x0000000a x)' 3301 a, b = _coerce_exprs(self, other) 3302 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3304 def __rtruediv__(self, other): 3305 """Create the Z3 expression (signed) division `other / self`.
""" 3306 return self.__rdiv__(other) 3308 def __mod__(self, other): 3309 """Create the Z3 expression (signed) mod `self % other`.
3311 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3326 a, b = _coerce_exprs(self, other) 3327 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3329 def __rmod__(self, other): 3330 """Create the Z3 expression (signed) mod `other % self`.
3332 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3337 >>> (10 % x).
sexpr()
3338 '(bvsmod #x0000000a x)' 3340 '(bvurem #x0000000a x)' 3342 '(bvsrem #x0000000a x)' 3344 a, b = _coerce_exprs(self, other) 3345 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3347 def __le__(self, other): 3348 """Create the Z3 expression (signed) `other <= self`.
3350 Use the function
ULE()
for unsigned less than
or equal to.
3355 >>> (x <= y).
sexpr()
3360 a, b = _coerce_exprs(self, other) 3361 return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3363 def __lt__(self, other): 3364 """Create the Z3 expression (signed) `other < self`.
3366 Use the function
ULT()
for unsigned less than.
3376 a, b = _coerce_exprs(self, other) 3377 return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3379 def __gt__(self, other): 3380 """Create the Z3 expression (signed) `other > self`.
3382 Use the function
UGT()
for unsigned greater than.
3392 a, b = _coerce_exprs(self, other) 3393 return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3395 def __ge__(self, other): 3396 """Create the Z3 expression (signed) `other >= self`.
3398 Use the function
UGE()
for unsigned greater than
or equal to.
3403 >>> (x >= y).
sexpr()
3408 a, b = _coerce_exprs(self, other) 3409 return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3411 def __rshift__(self, other): 3412 """Create the Z3 expression (arithmetical) right shift `self >> other`
3414 Use the function
LShR()
for the right logical shift
3419 >>> (x >> y).
sexpr()
3438 a, b = _coerce_exprs(self, other) 3439 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3441 def __lshift__(self, other): 3442 """Create the Z3 expression left shift `self << other`
3447 >>> (x << y).
sexpr()
3452 a, b = _coerce_exprs(self, other) 3453 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3455 def __rrshift__(self, other): 3456 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3458 Use the function
LShR()
for the right logical shift
3463 >>> (10 >> x).
sexpr()
3464 '(bvashr #x0000000a x)' 3466 a, b = _coerce_exprs(self, other) 3467 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3469 def __rlshift__(self, other): 3470 """Create the Z3 expression left shift `other << self`.
3472 Use the function
LShR()
for the right logical shift
3477 >>> (10 << x).
sexpr()
3478 '(bvshl #x0000000a x)' 3480 a, b = _coerce_exprs(self, other) 3481 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3483 class BitVecNumRef(BitVecRef): 3484 """Bit-vector values.
""" 3487 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral.
3492 >>> print(
"0x%.8x" % v.as_long())
3495 return int(self.as_string()) 3497 def as_signed_long(self): 3498 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral. The most significant bit
is assumed to be the sign.
3512 val = self.as_long() 3513 if val >= 2**(sz - 1): 3515 if val < -2**(sz - 1): 3519 def as_string(self): 3520 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 3523 """Return `
True`
if `a`
is a Z3 bit-vector expression.
3533 return isinstance(a, BitVecRef) 3536 """Return `
True`
if `a`
is a Z3 bit-vector numeral value.
3547 return is_bv(a) and _is_numeral(a.ctx, a.as_ast()) 3549 def BV2Int(a, is_signed=False): 3550 """Return the Z3 expression
BV2Int(a).
3558 >>> x >
BV2Int(b, is_signed=
False)
3560 >>> x >
BV2Int(b, is_signed=
True)
3566 _z3_assert(is_bv(a), "Z3 bit-vector expression expected") 3568 ## investigate problem with bv2int 3569 return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx) 3571 def BitVecSort(sz, ctx=None): 3572 """Return a Z3 bit-vector sort of the given size. If `ctx=
None`, then the
global context
is used.
3578 >>> x =
Const(
'x', Byte)
3583 return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx) 3585 def BitVecVal(val, bv, ctx=None): 3586 """Return a bit-vector value with the given number of bits. If `ctx=
None`, then the
global context
is used.
3591 >>> print(
"0x%.8x" % v.as_long())
3596 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx) 3599 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx) 3601 def BitVec(name, bv, ctx=None): 3602 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3603 If `ctx=
None`, then the
global context
is used.
3613 >>> x2 =
BitVec(
'x', word)
3617 if isinstance(bv, BitVecSortRef): 3621 bv = BitVecSort(bv, ctx) 3622 return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx) 3624 def BitVecs(names, bv, ctx=None): 3625 """Return a tuple of bit-vector constants of size bv.
3627 >>> x, y, z =
BitVecs(
'x y z', 16)
3640 if isinstance(names, str): 3641 names = names.split(" ") 3642 return [BitVec(name, bv, ctx) for name in names] 3645 """Create a Z3 bit-vector concatenation expression.
3655 args = _get_args(args) 3658 _z3_assert(sz >= 2, "At least two arguments expected.") 3665 if is_seq(args[0]) or isinstance(args[0], str): 3666 args = [_coerce_seq(s, ctx) for s in args] 3668 _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") 3671 v[i] = args[i].as_ast() 3672 return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) 3676 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 3679 v[i] = args[i].as_ast() 3680 return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx) 3683 _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") 3685 for i in range(sz - 1): 3686 r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx) 3689 def Extract(high, low, a): 3690 """Create a Z3 bit-vector extraction expression,
or create a string extraction expression.
3700 if isinstance(high, str): 3701 high = StringVal(high) 3704 offset, length = _coerce_exprs(low, a, s.ctx) 3705 return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) 3707 _z3_assert(low <= high, "First argument must be greater than or equal to second argument") 3708 _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers") 3709 _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression") 3710 return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx) 3712 def _check_bv_args(a, b): 3714 _z3_assert(is_bv(a) or is_bv(b), "At least one of the arguments must be a Z3 bit-vector expression") 3717 """Create the Z3 expression (unsigned) `other <= self`.
3719 Use the operator <=
for signed less than
or equal to.
3724 >>> (x <= y).sexpr()
3726 >>>
ULE(x, y).sexpr()
3729 _check_bv_args(a, b) 3730 a, b = _coerce_exprs(a, b) 3731 return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3734 """Create the Z3 expression (unsigned) `other < self`.
3736 Use the operator <
for signed less than.
3743 >>>
ULT(x, y).sexpr()
3746 _check_bv_args(a, b) 3747 a, b = _coerce_exprs(a, b) 3748 return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3751 """Create the Z3 expression (unsigned) `other >= self`.
3753 Use the operator >=
for signed greater than
or equal to.
3758 >>> (x >= y).sexpr()
3760 >>>
UGE(x, y).sexpr()
3763 _check_bv_args(a, b) 3764 a, b = _coerce_exprs(a, b) 3765 return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3768 """Create the Z3 expression (unsigned) `other > self`.
3770 Use the operator >
for signed greater than.
3777 >>>
UGT(x, y).sexpr()
3780 _check_bv_args(a, b) 3781 a, b = _coerce_exprs(a, b) 3782 return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3785 """Create the Z3 expression (unsigned) division `self / other`.
3787 Use the operator /
for signed division.
3793 >>>
UDiv(x, y).sort()
3797 >>>
UDiv(x, y).sexpr()
3800 _check_bv_args(a, b) 3801 a, b = _coerce_exprs(a, b) 3802 return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3805 """Create the Z3 expression (unsigned) remainder `self % other`.
3807 Use the operator %
for signed modulus,
and SRem()
for signed remainder.
3813 >>>
URem(x, y).sort()
3817 >>>
URem(x, y).sexpr()
3820 _check_bv_args(a, b) 3821 a, b = _coerce_exprs(a, b) 3822 return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3825 """Create the Z3 expression signed remainder.
3827 Use the operator %
for signed modulus,
and URem()
for unsigned remainder.
3833 >>>
SRem(x, y).sort()
3837 >>>
SRem(x, y).sexpr()
3840 _check_bv_args(a, b) 3841 a, b = _coerce_exprs(a, b) 3842 return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3845 """Create the Z3 expression logical right shift.
3847 Use the operator >>
for the arithmetical right shift.
3852 >>> (x >> y).sexpr()
3854 >>>
LShR(x, y).sexpr()
3871 _check_bv_args(a, b) 3872 a, b = _coerce_exprs(a, b) 3873 return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3875 def RotateLeft(a, b): 3876 """Return an expression representing `a` rotated to the left `b` times.
3886 _check_bv_args(a, b) 3887 a, b = _coerce_exprs(a, b) 3888 return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3890 def RotateRight(a, b): 3891 """Return an expression representing `a` rotated to the right `b` times.
3901 _check_bv_args(a, b) 3902 a, b = _coerce_exprs(a, b) 3903 return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3906 """Return a bit-vector expression with `n` extra sign-bits.
3926 >>> print(
"%.x" % v.as_long())
3930 _z3_assert(_is_int(n), "First argument must be an integer") 3931 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 3932 return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 3935 """Return a bit-vector expression with `n` extra zero-bits.
3957 _z3_assert(_is_int(n), "First argument must be an integer") 3958 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 3959 return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 3961 def RepeatBitVec(n, a): 3962 """Return an expression representing `n` copies of `a`.
3971 >>> print(
"%.x" % v0.as_long())
3976 >>> print(
"%.x" % v.as_long())
3980 _z3_assert(_is_int(n), "First argument must be an integer") 3981 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 3982 return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx) 3985 """Return the reduction-
and expression of `a`.
""" 3987 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 3988 return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) 3991 """Return the reduction-
or expression of `a`.
""" 3993 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 3994 return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) 3996 def BVAddNoOverflow(a, b, signed): 3997 """A predicate the determines that bit-vector addition does
not overflow
""" 3998 _check_bv_args(a, b) 3999 a, b = _coerce_exprs(a, b) 4000 return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4002 def BVAddNoUnderflow(a, b): 4003 """A predicate the determines that signed bit-vector addition does
not underflow
""" 4004 _check_bv_args(a, b) 4005 a, b = _coerce_exprs(a, b) 4006 return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4008 def BVSubNoOverflow(a, b): 4009 """A predicate the determines that bit-vector subtraction does
not overflow
""" 4010 _check_bv_args(a, b) 4011 a, b = _coerce_exprs(a, b) 4012 return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4015 def BVSubNoUnderflow(a, b, signed): 4016 """A predicate the determines that bit-vector subtraction does
not underflow
""" 4017 _check_bv_args(a, b) 4018 a, b = _coerce_exprs(a, b) 4019 return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4021 def BVSDivNoOverflow(a, b): 4022 """A predicate the determines that bit-vector signed division does
not overflow
""" 4023 _check_bv_args(a, b) 4024 a, b = _coerce_exprs(a, b) 4025 return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4027 def BVSNegNoOverflow(a): 4028 """A predicate the determines that bit-vector unary negation does
not overflow
""" 4030 _z3_assert(is_bv(a), "Argument should be a bit-vector") 4031 return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx) 4033 def BVMulNoOverflow(a, b, signed): 4034 """A predicate the determines that bit-vector multiplication does
not overflow
""" 4035 _check_bv_args(a, b) 4036 a, b = _coerce_exprs(a, b) 4037 return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx) 4040 def BVMulNoUnderflow(a, b): 4041 """A predicate the determines that bit-vector signed multiplication does
not underflow
""" 4042 _check_bv_args(a, b) 4043 a, b = _coerce_exprs(a, b) 4044 return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 4048 ######################################### 4052 ######################################### 4054 class ArraySortRef(SortRef): 4058 """Return the domain of the array sort `self`.
4064 return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx) 4067 """Return the range of the array sort `self`.
4073 return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx) 4075 class ArrayRef(ExprRef): 4076 """Array expressions.
""" 4079 """Return the array sort of the array expression `self`.
4085 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4094 return self.sort().domain() 4103 return self.sort().range() 4105 def __getitem__(self, arg): 4106 """Return the Z3 expression `self[arg]`.
4115 arg = self.domain().cast(arg) 4116 return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx) 4119 return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx) 4123 """Return `
True`
if `a`
is a Z3 array expression.
4133 return isinstance(a, ArrayRef) 4135 def is_const_array(a): 4136 """Return `
True`
if `a`
is a Z3 constant array.
4145 return is_app_of(a, Z3_OP_CONST_ARRAY) 4148 """Return `
True`
if `a`
is a Z3 constant array.
4157 return is_app_of(a, Z3_OP_CONST_ARRAY) 4160 """Return `
True`
if `a`
is a Z3 map array expression.
4172 return is_app_of(a, Z3_OP_ARRAY_MAP) 4175 """Return `
True`
if `a`
is a Z3 default array expression.
4180 return is_app_of(a, Z3_OP_ARRAY_DEFAULT) 4182 def get_map_func(a): 4183 """Return the function declaration associated with a Z3 map array expression.
4196 _z3_assert(is_map(a), "Z3 array map expression expected.") 4197 return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx) 4199 def ArraySort(d, r): 4200 """Return the Z3 array sort with the given domain
and range sorts.
4214 _z3_assert(is_sort(d), "Z3 sort expected") 4215 _z3_assert(is_sort(r), "Z3 sort expected") 4216 _z3_assert(d.ctx == r.ctx, "Context mismatch") 4218 return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx) 4220 def Array(name, dom, rng): 4221 """Return an array constant named `name` with the given domain
and range sorts.
4229 s = ArraySort(dom, rng) 4231 return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx) 4233 def Update(a, i, v): 4234 """Return a Z3 store array expression.
4237 >>> i, v =
Ints(
'i v')
4241 >>>
prove(s[i] == v)
4248 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4249 i = a.domain().cast(i) 4250 v = a.range().cast(v) 4252 return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx) 4255 """ Return a default value
for array expression.
4261 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4266 """Return a Z3 store array expression.
4269 >>> i, v =
Ints(
'i v')
4270 >>> s =
Store(a, i, v)
4273 >>>
prove(s[i] == v)
4279 return Update(a, i, v) 4282 """Return a Z3 select array expression.
4292 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4297 """Return a Z3 map array expression.
4302 >>> b =
Map(f, a1, a2)
4305 >>>
prove(b[0] == f(a1[0], a2[0]))
4308 args = _get_args(args) 4310 _z3_assert(len(args) > 0, "At least one Z3 array expression expected") 4311 _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration") 4312 _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected") 4313 _z3_assert(len(args) == f.arity(), "Number of arguments mismatch") 4314 _args, sz = _to_ast_array(args) 4316 return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx) 4319 """Return a Z3 constant array expression.
4333 _z3_assert(is_sort(dom), "Z3 sort expected") 4336 v = _py2expr(v, ctx) 4337 return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx) 4340 """Return extensionality index
for arrays.
4343 _z3_assert(is_array(a) and is_array(b)) 4344 return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast())); 4347 """Return `
True`
if `a`
is a Z3 array select application.
4356 return is_app_of(a, Z3_OP_SELECT) 4359 """Return `
True`
if `a`
is a Z3 array store application.
4367 return is_app_of(a, Z3_OP_STORE) 4369 ######################################### 4373 ######################################### 4375 def _valid_accessor(acc): 4376 """Return `
True`
if acc
is pair of the form (String, Datatype
or Sort).
""" 4377 return isinstance(acc, tuple) and len(acc) == 2 and isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1])) 4380 """Helper
class for declaring Z3 datatypes.
4383 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4384 >>> List.declare(
'nil')
4385 >>> List = List.create()
4389 >>> List.cons(10, List.nil)
4391 >>> List.cons(10, List.nil).sort()
4393 >>> cons = List.cons
4397 >>> n = cons(1, cons(0, nil))
4399 cons(1, cons(0, nil))
4405 def __init__(self, name, ctx=None): 4406 self.ctx = _get_ctx(ctx) 4408 self.constructors = [] 4410 def __deepcopy__(self, memo={}): 4411 r = Datatype(self.name, self.ctx) 4412 r.constructors = copy.deepcopy(self.constructors) 4415 def declare_core(self, name, rec_name, *args): 4417 _z3_assert(isinstance(name, str), "String expected") 4418 _z3_assert(isinstance(rec_name, str), "String expected") 4419 _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)") 4420 self.constructors.append((name, rec_name, args)) 4422 def declare(self, name, *args): 4423 """Declare constructor named `name` with the given accessors `args`.
4424 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.
4426 In the followin example `List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))`
4427 declares the constructor named `cons` that builds a new List using an integer
and a List.
4428 It also declares the accessors `car`
and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
4429 and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method
create() to create
4430 the actual datatype
in Z3.
4433 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4434 >>> List.declare(
'nil')
4435 >>> List = List.create()
4438 _z3_assert(isinstance(name, str), "String expected") 4439 _z3_assert(name != "", "Constructor name cannot be empty") 4440 return self.declare_core(name, "is_" + name, *args) 4443 return "Datatype(%s, %s)" % (self.name, self.constructors) 4446 """Create a Z3 datatype based on the constructors declared using the mehtod `
declare()`.
4448 The function `
CreateDatatypes()` must be used to define mutually recursive datatypes.
4451 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4452 >>> List.declare(
'nil')
4453 >>> List = List.create()
4456 >>> List.cons(10, List.nil)
4459 return CreateDatatypes([self])[0] 4461 class ScopedConstructor: 4462 """Auxiliary object used to create Z3 datatypes.
""" 4463 def __init__(self, c, ctx): 4467 if self.ctx.ref() is not None: 4468 Z3_del_constructor(self.ctx.ref(), self.c) 4470 class ScopedConstructorList: 4471 """Auxiliary object used to create Z3 datatypes.
""" 4472 def __init__(self, c, ctx): 4476 if self.ctx.ref() is not None: 4477 Z3_del_constructor_list(self.ctx.ref(), self.c) 4479 def CreateDatatypes(*ds): 4480 """Create mutually recursive Z3 datatypes using 1
or more Datatype helper objects.
4482 In the following example we define a Tree-List using two mutually recursive datatypes.
4484 >>> TreeList =
Datatype(
'TreeList')
4487 >>> Tree.declare(
'leaf', (
'val',
IntSort()))
4489 >>> Tree.declare(
'node', (
'children', TreeList))
4490 >>> TreeList.declare(
'nil')
4491 >>> TreeList.declare(
'cons', (
'car', Tree), (
'cdr', TreeList))
4493 >>> Tree.val(Tree.leaf(10))
4495 >>>
simplify(Tree.val(Tree.leaf(10)))
4497 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4499 node(cons(leaf(10), cons(leaf(20), nil)))
4500 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4503 >>>
simplify(TreeList.car(Tree.children(n2)) == n1)
4508 _z3_assert(len(ds) > 0, "At least one Datatype must be specified") 4509 _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes") 4510 _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch") 4511 _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected") 4514 names = (Symbol * num)() 4515 out = (Sort * num)() 4516 clists = (ConstructorList * num)() 4518 for i in range(num): 4520 names[i] = to_symbol(d.name, ctx) 4521 num_cs = len(d.constructors) 4522 cs = (Constructor * num_cs)() 4523 for j in range(num_cs): 4524 c = d.constructors[j] 4525 cname = to_symbol(c[0], ctx) 4526 rname = to_symbol(c[1], ctx) 4529 fnames = (Symbol * num_fs)() 4530 sorts = (Sort * num_fs)() 4531 refs = (ctypes.c_uint * num_fs)() 4532 for k in range(num_fs): 4535 fnames[k] = to_symbol(fname, ctx) 4536 if isinstance(ftype, Datatype): 4538 _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected") 4540 refs[k] = ds.index(ftype) 4543 _z3_assert(is_sort(ftype), "Z3 sort expected") 4544 sorts[k] = ftype.ast 4546 cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs) 4547 to_delete.append(ScopedConstructor(cs[j], ctx)) 4548 clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs) 4549 to_delete.append(ScopedConstructorList(clists[i], ctx)) 4550 Z3_mk_datatypes(ctx.ref(), num, names, out, clists) 4552 ## Create a field for every constructor, recognizer and accessor 4553 for i in range(num): 4554 dref = DatatypeSortRef(out[i], ctx) 4555 num_cs = dref.num_constructors() 4556 for j in range(num_cs): 4557 cref = dref.constructor(j) 4558 cref_name = cref.name() 4559 cref_arity = cref.arity() 4560 if cref.arity() == 0: 4562 setattr(dref, cref_name, cref) 4563 rref = dref.recognizer(j) 4564 setattr(dref, rref.name(), rref) 4565 for k in range(cref_arity): 4566 aref = dref.accessor(j, k) 4567 setattr(dref, aref.name(), aref) 4569 return tuple(result) 4571 class DatatypeSortRef(SortRef): 4572 """Datatype sorts.
""" 4573 def num_constructors(self): 4574 """Return the number of constructors
in the given Z3 datatype.
4577 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4578 >>> List.declare(
'nil')
4579 >>> List = List.create()
4581 >>> List.num_constructors()
4584 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast)) 4586 def constructor(self, idx): 4587 """Return a constructor of the datatype `self`.
4590 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4591 >>> List.declare(
'nil')
4592 >>> List = List.create()
4594 >>> List.num_constructors()
4596 >>> List.constructor(0)
4598 >>> List.constructor(1)
4602 _z3_assert(idx < self.num_constructors(), "Invalid constructor index") 4603 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx) 4605 def recognizer(self, idx): 4606 """In Z3, each constructor has an associated recognizer predicate.
4608 If the constructor
is named `name`, then the recognizer `is_name`.
4611 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4612 >>> List.declare(
'nil')
4613 >>> List = List.create()
4615 >>> List.num_constructors()
4617 >>> List.recognizer(0)
4619 >>> List.recognizer(1)
4621 >>>
simplify(List.is_nil(List.cons(10, List.nil)))
4623 >>>
simplify(List.is_cons(List.cons(10, List.nil)))
4625 >>> l =
Const(
'l', List)
4630 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index") 4631 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx) 4633 def accessor(self, i, j): 4634 """In Z3, each constructor has 0
or more accessor. The number of accessors
is equal to the arity of the constructor.
4637 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4638 >>> List.declare(
'nil')
4639 >>> List = List.create()
4640 >>> List.num_constructors()
4642 >>> List.constructor(0)
4644 >>> num_accs = List.constructor(0).arity()
4647 >>> List.accessor(0, 0)
4649 >>> List.accessor(0, 1)
4651 >>> List.constructor(1)
4653 >>> num_accs = List.constructor(1).arity()
4658 _z3_assert(i < self.num_constructors(), "Invalid constructor index") 4659 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index") 4660 return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx) 4662 class DatatypeRef(ExprRef): 4663 """Datatype expressions.
""" 4665 """Return the datatype sort of the datatype expression `self`.
""" 4666 return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4668 def EnumSort(name, values, ctx=None): 4669 """Return a new enumeration sort named `name` containing the given values.
4671 The result
is a pair (sort, list of constants).
4673 >>> Color, (red, green, blue) =
EnumSort(
'Color', [
'red',
'green',
'blue'])
4676 _z3_assert(isinstance(name, str), "Name must be a string") 4677 _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings") 4678 _z3_assert(len(values) > 0, "At least one value expected") 4681 _val_names = (Symbol * num)() 4682 for i in range(num): 4683 _val_names[i] = to_symbol(values[i]) 4684 _values = (FuncDecl * num)() 4685 _testers = (FuncDecl * num)() 4686 name = to_symbol(name) 4687 S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx) 4689 for i in range(num): 4690 V.append(FuncDeclRef(_values[i], ctx)) 4691 V = [a() for a in V] 4694 ######################################### 4698 ######################################### 4701 """Set of parameters used to configure Solvers, Tactics
and Simplifiers
in Z3.
4703 Consider using the function `args2params` to create instances of this object.
4705 def __init__(self, ctx=None, params=None): 4706 self.ctx = _get_ctx(ctx) 4708 self.params = Z3_mk_params(self.ctx.ref()) 4710 self.params = params 4711 Z3_params_inc_ref(self.ctx.ref(), self.params) 4713 def __deepcopy__(self, memo={}): 4714 return ParamsRef(self.ctx, self.params) 4717 if self.ctx.ref() is not None: 4718 Z3_params_dec_ref(self.ctx.ref(), self.params) 4720 def set(self, name, val): 4721 """Set parameter name with value val.
""" 4723 _z3_assert(isinstance(name, str), "parameter name must be a string") 4724 name_sym = to_symbol(name, self.ctx) 4725 if isinstance(val, bool): 4726 Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val) 4728 Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val) 4729 elif isinstance(val, float): 4730 Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val) 4731 elif isinstance(val, str): 4732 Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx)) 4735 _z3_assert(False, "invalid parameter value") 4738 return Z3_params_to_string(self.ctx.ref(), self.params) 4740 def validate(self, ds): 4741 _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected") 4742 Z3_params_validate(self.ctx.ref(), self.params, ds.descr) 4744 def args2params(arguments, keywords, ctx=None): 4745 """Convert python arguments into a Z3_params object.
4746 A
':' is added to the keywords,
and '_' is replaced with
'-' 4748 >>>
args2params([
'model',
True,
'relevancy', 2], {
'elim_and' :
True})
4749 (params model true relevancy 2 elim_and true)
4752 _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") 4766 class ParamDescrsRef: 4767 """Set of parameter descriptions
for Solvers, Tactics
and Simplifiers
in Z3.
4769 def __init__(self, descr, ctx=None): 4770 _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected") 4771 self.ctx = _get_ctx(ctx) 4773 Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr) 4775 def __deepcopy__(self, memo={}): 4776 return ParamsDescrsRef(self.descr, self.ctx) 4779 if self.ctx.ref() is not None: 4780 Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr) 4783 """Return the size of
in the parameter description `self`.
4785 return int(Z3_param_descrs_size(self.ctx.ref(), self.descr)) 4788 """Return the size of
in the parameter description `self`.
4792 def get_name(self, i): 4793 """Return the i-th parameter name
in the parameter description `self`.
4795 return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i)) 4797 def get_kind(self, n): 4798 """Return the kind of the parameter named `n`.
4800 return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 4802 def get_documentation(self, n): 4803 """Return the documentation string of the parameter named `n`.
4805 return Z3_param_descrs_get_documentation(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 4807 def __getitem__(self, arg): 4809 return self.get_name(arg) 4811 return self.get_kind(arg) 4814 return Z3_param_descrs_to_string(self.ctx.ref(), self.descr) 4816 ######################################### 4820 ######################################### 4822 class Goal(Z3PPObject): 4823 """Goal
is a collection of constraints we want to find a solution
or show to be unsatisfiable (infeasible).
4825 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
4826 A goal has a solution
if one of its subgoals has a solution.
4827 A goal
is unsatisfiable
if all subgoals are unsatisfiable.
4830 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None): 4832 _z3_assert(goal is None or ctx is not None, "If goal is different from None, then ctx must be also different from None") 4833 self.ctx = _get_ctx(ctx) 4835 if self.goal is None: 4836 self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs) 4837 Z3_goal_inc_ref(self.ctx.ref(), self.goal) 4839 def __deepcopy__(self, memo={}): 4840 return Goal(False, False, False, self.ctx, self.goal) 4843 if self.goal is not None and self.ctx.ref() is not None: 4844 Z3_goal_dec_ref(self.ctx.ref(), self.goal) 4847 """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
4849 >>> x, y =
Ints(
'x y')
4851 >>> g.add(x == 0, y >= x + 1)
4854 >>> r =
Then(
'simplify',
'solve-eqs')(g)
4861 return int(Z3_goal_depth(self.ctx.ref(), self.goal)) 4863 def inconsistent(self): 4864 """Return `
True`
if `self` contains the `
False` constraints.
4866 >>> x, y =
Ints(
'x y')
4868 >>> g.inconsistent()
4870 >>> g.add(x == 0, x == 1)
4873 >>> g.inconsistent()
4875 >>> g2 =
Tactic(
'propagate-values')(g)[0]
4876 >>> g2.inconsistent()
4879 return Z3_goal_inconsistent(self.ctx.ref(), self.goal) 4882 """Return the precision (under-approximation, over-approximation,
or precise) of the goal `self`.
4885 >>> g.prec() == Z3_GOAL_PRECISE
4887 >>> x, y =
Ints(
'x y')
4888 >>> g.add(x == y + 1)
4889 >>> g.prec() == Z3_GOAL_PRECISE
4891 >>> t =
With(
Tactic(
'add-bounds'), add_bound_lower=0, add_bound_upper=10)
4894 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
4895 >>> g2.prec() == Z3_GOAL_PRECISE
4897 >>> g2.prec() == Z3_GOAL_UNDER
4900 return Z3_goal_precision(self.ctx.ref(), self.goal) 4902 def precision(self): 4903 """Alias
for `
prec()`.
4906 >>> g.precision() == Z3_GOAL_PRECISE
4912 """Return the number of constraints
in the goal `self`.
4917 >>> x, y =
Ints(
'x y')
4918 >>> g.add(x == 0, y > x)
4922 return int(Z3_goal_size(self.ctx.ref(), self.goal)) 4925 """Return the number of constraints
in the goal `self`.
4930 >>> x, y =
Ints(
'x y')
4931 >>> g.add(x == 0, y > x)
4938 """Return a constraint
in the goal `self`.
4941 >>> x, y =
Ints(
'x y')
4942 >>> g.add(x == 0, y > x)
4948 return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx) 4950 def __getitem__(self, arg): 4951 """Return a constraint
in the goal `self`.
4954 >>> x, y =
Ints(
'x y')
4955 >>> g.add(x == 0, y > x)
4961 if arg >= len(self): 4963 return self.get(arg) 4965 def assert_exprs(self, *args): 4966 """Assert constraints into the goal.
4970 >>> g.assert_exprs(x > 0, x < 2)
4974 args = _get_args(args) 4975 s = BoolSort(self.ctx) 4978 Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast()) 4980 def append(self, *args): 4985 >>> g.append(x > 0, x < 2)
4989 self.assert_exprs(*args) 4991 def insert(self, *args): 4996 >>> g.insert(x > 0, x < 2)
5000 self.assert_exprs(*args) 5002 def add(self, *args): 5007 >>> g.add(x > 0, x < 2)
5011 self.assert_exprs(*args) 5014 return obj_to_string(self) 5017 """Return a textual representation of the s-expression representing the goal.
""" 5018 return Z3_goal_to_string(self.ctx.ref(), self.goal) 5020 def translate(self, target): 5021 """Copy goal `self` to context `target`.
5029 >>> g2 = g.translate(c2)
5040 _z3_assert(isinstance(target, Context), "target must be a context") 5041 return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target) 5043 def simplify(self, *arguments, **keywords): 5044 """Return a new simplified goal.
5046 This method
is essentially invoking the simplify tactic.
5050 >>> g.add(x + 1 >= 2)
5053 >>> g2 = g.simplify()
5060 t = Tactic('simplify') 5061 return t.apply(self, *arguments, **keywords)[0] 5064 """Return goal `self`
as a single Z3 expression.
5079 return BoolVal(True, self.ctx) 5083 return And([ self.get(i) for i in range(len(self)) ], self.ctx) 5085 ######################################### 5089 ######################################### 5090 class AstVector(Z3PPObject): 5091 """A collection (vector) of ASTs.
""" 5093 def __init__(self, v=None, ctx=None): 5096 self.ctx = _get_ctx(ctx) 5097 self.vector = Z3_mk_ast_vector(self.ctx.ref()) 5100 assert ctx is not None 5102 Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector) 5104 def __deepcopy__(self, memo={}): 5105 return AstVector(self.vector, self.ctx) 5108 if self.vector is not None and self.ctx.ref() is not None: 5109 Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector) 5112 """Return the size of the vector `self`.
5117 >>> A.push(
Int(
'x'))
5118 >>> A.push(
Int(
'x'))
5122 return int(Z3_ast_vector_size(self.ctx.ref(), self.vector)) 5124 def __getitem__(self, i): 5125 """Return the AST at position `i`.
5128 >>> A.push(
Int(
'x') + 1)
5129 >>> A.push(
Int(
'y'))
5135 if i >= self.__len__(): 5137 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx) 5139 def __setitem__(self, i, v): 5140 """Update AST at position `i`.
5143 >>> A.push(
Int(
'x') + 1)
5144 >>> A.push(
Int(
'y'))
5151 if i >= self.__len__(): 5153 Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast()) 5156 """Add `v`
in the end of the vector.
5161 >>> A.push(
Int(
'x'))
5165 Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast()) 5167 def resize(self, sz): 5168 """Resize the vector to `sz` elements.
5174 >>>
for i
in range(10): A[i] =
Int(
'x')
5178 Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz) 5180 def __contains__(self, item): 5181 """Return `
True`
if the vector contains `item`.
5203 def translate(self, other_ctx): 5204 """Copy vector `self` to context `other_ctx`.
5210 >>> B = A.translate(c2)
5214 return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx) 5217 return obj_to_string(self) 5220 """Return a textual representation of the s-expression representing the vector.
""" 5221 return Z3_ast_vector_to_string(self.ctx.ref(), self.vector) 5223 ######################################### 5227 ######################################### 5229 """A mapping
from ASTs to ASTs.
""" 5231 def __init__(self, m=None, ctx=None): 5234 self.ctx = _get_ctx(ctx) 5235 self.map = Z3_mk_ast_map(self.ctx.ref()) 5238 assert ctx is not None 5240 Z3_ast_map_inc_ref(self.ctx.ref(), self.map) 5242 def __deepcopy__(self, memo={}): 5243 return AstMap(self.map, self.ctx) 5246 if self.map is not None and self.ctx.ref() is not None: 5247 Z3_ast_map_dec_ref(self.ctx.ref(), self.map) 5250 """Return the size of the map.
5260 return int(Z3_ast_map_size(self.ctx.ref(), self.map)) 5262 def __contains__(self, key): 5263 """Return `
True`
if the map contains key `key`.
5273 return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast()) 5275 def __getitem__(self, key): 5276 """Retrieve the value associated with key `key`.
5284 return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx) 5286 def __setitem__(self, k, v): 5287 """Add/Update key `k` with value `v`.
5300 Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast()) 5303 return Z3_ast_map_to_string(self.ctx.ref(), self.map) 5306 """Remove the entry associated with key `k`.
5317 Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast()) 5320 """Remove all entries
from the map.
5332 Z3_ast_map_reset(self.ctx.ref(), self.map) 5335 """Return an AstVector containing all keys
in the map.
5344 return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx) 5346 ######################################### 5350 ######################################### 5353 """Store the value of the interpretation of a function
in a particular point.
""" 5355 def __init__(self, entry, ctx): 5358 Z3_func_entry_inc_ref(self.ctx.ref(), self.entry) 5360 def __deepcopy__(self, memo={}): 5361 return FuncEntry(self.entry, self.ctx) 5364 if self.ctx.ref() is not None: 5365 Z3_func_entry_dec_ref(self.ctx.ref(), self.entry) 5368 """Return the number of arguments
in the given entry.
5372 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5377 >>> f_i.num_entries()
5379 >>> e = f_i.entry(0)
5383 return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry)) 5385 def arg_value(self, idx): 5386 """Return the value of argument `idx`.
5390 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5395 >>> f_i.num_entries()
5397 >>> e = f_i.entry(0)
5408 ...
except IndexError:
5409 ... print(
"index error")
5412 if idx >= self.num_args(): 5414 return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx) 5417 """Return the value of the function at point `self`.
5421 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5426 >>> f_i.num_entries()
5428 >>> e = f_i.entry(0)
5436 return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx) 5439 """Return entry `self`
as a Python list.
5442 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
5447 >>> f_i.num_entries()
5449 >>> e = f_i.entry(0)
5453 args = [ self.arg_value(i) for i in range(self.num_args())] 5454 args.append(self.value()) 5458 return repr(self.as_list()) 5460 class FuncInterp(Z3PPObject): 5461 """Stores the interpretation of a function
in a Z3 model.
""" 5463 def __init__(self, f, ctx): 5466 if self.f is not None: 5467 Z3_func_interp_inc_ref(self.ctx.ref(), self.f) 5469 def __deepcopy__(self, memo={}): 5470 return FuncInterp(self.f, self.ctx) 5473 if self.f is not None and self.ctx.ref() is not None: 5474 Z3_func_interp_dec_ref(self.ctx.ref(), self.f) 5476 def else_value(self): 5478 Return the `
else` value
for a function interpretation.
5479 Return
None if Z3 did
not specify the `
else` value
for 5484 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5489 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5493 r = Z3_func_interp_get_else(self.ctx.ref(), self.f) 5495 return _to_expr_ref(r, self.ctx) 5499 def num_entries(self): 5500 """Return the number of entries/points
in the function interpretation `self`.
5504 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5509 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5513 return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f)) 5516 """Return the number of arguments
for each entry
in the function interpretation `self`.
5520 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5527 return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f)) 5529 def entry(self, idx): 5530 """Return an entry at position `idx < self.
num_entries()`
in the function interpretation `self`.
5534 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5539 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5549 if idx >= self.num_entries(): 5551 return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx) 5554 """Return the function interpretation
as a Python list.
5557 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5562 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5564 [[0, 1], [1, 1], [2, 0], 1]
5566 r = [ self.entry(i).as_list() for i in range(self.num_entries())] 5567 r.append(self.else_value()) 5571 return obj_to_string(self) 5573 class ModelRef(Z3PPObject): 5574 """Model/Solution of a satisfiability problem (aka system of constraints).
""" 5576 def __init__(self, m, ctx): 5577 assert ctx is not None 5580 Z3_model_inc_ref(self.ctx.ref(), self.model) 5582 def __deepcopy__(self, memo={}): 5583 return ModelRef(self.m, self.ctx) 5586 if self.ctx.ref() is not None: 5587 Z3_model_dec_ref(self.ctx.ref(), self.model) 5590 return obj_to_string(self) 5593 """Return a textual representation of the s-expression representing the model.
""" 5594 return Z3_model_to_string(self.ctx.ref(), self.model) 5596 def eval(self, t, model_completion=False): 5597 """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`.
5601 >>> s.add(x > 0, x < 2)
5614 >>> m.eval(y, model_completion=
True)
5621 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r): 5622 return _to_expr_ref(r[0], self.ctx) 5623 raise Z3Exception("failed to evaluate expression in the model") 5625 def evaluate(self, t, model_completion=False): 5626 """Alias
for `eval`.
5630 >>> s.add(x > 0, x < 2)
5634 >>> m.evaluate(x + 1)
5636 >>> m.evaluate(x == 1)
5639 >>> m.evaluate(y + x)
5643 >>> m.evaluate(y, model_completion=
True)
5646 >>> m.evaluate(y + x)
5649 return self.eval(t, model_completion) 5652 """Return the number of constant
and function declarations
in the model `self`.
5657 >>> s.add(x > 0, f(x) != x)
5664 return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model)) 5666 def get_interp(self, decl): 5667 """Return the interpretation
for a given declaration
or constant.
5672 >>> s.add(x > 0, x < 2, f(x) == 0)
5682 _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected") 5686 if decl.arity() == 0: 5687 _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast) 5688 if _r.value is None: 5690 r = _to_expr_ref(_r, self.ctx) 5692 return self.get_interp(get_as_array_func(r)) 5696 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) 5700 def num_sorts(self): 5701 """Return the number of unintepreted sorts that contain an interpretation
in the model `self`.
5704 >>> a, b =
Consts(
'a b', A)
5713 return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model)) 5715 def get_sort(self, idx): 5716 """Return the unintepreted sort at position `idx` < self.
num_sorts().
5720 >>> a1, a2 =
Consts(
'a1 a2', A)
5721 >>> b1, b2 =
Consts(
'b1 b2', B)
5723 >>> s.add(a1 != a2, b1 != b2)
5734 if idx >= self.num_sorts(): 5736 return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx) 5739 """Return all uninterpreted sorts that have an interpretation
in the model `self`.
5743 >>> a1, a2 =
Consts(
'a1 a2', A)
5744 >>> b1, b2 =
Consts(
'b1 b2', B)
5746 >>> s.add(a1 != a2, b1 != b2)
5753 return [ self.get_sort(i) for i in range(self.num_sorts()) ] 5755 def get_universe(self, s): 5756 """Return the intepretation
for the uninterpreted sort `s`
in the model `self`.
5759 >>> a, b =
Consts(
'a b', A)
5765 >>> m.get_universe(A)
5769 _z3_assert(isinstance(s, SortRef), "Z3 sort expected") 5771 return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx) 5775 def __getitem__(self, idx): 5776 """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 interpreation
is returned.
5778 The elements can be retrieved using position
or the actual declaration.
5783 >>> s.add(x > 0, x < 2, f(x) == 0)
5797 >>>
for d
in m: print(
"%s -> %s" % (d, m[d]))
5799 f -> [1 -> 0,
else -> 0]
5802 if idx >= len(self): 5804 num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model) 5805 if (idx < num_consts): 5806 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx) 5808 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx) 5809 if isinstance(idx, FuncDeclRef): 5810 return self.get_interp(idx) 5812 return self.get_interp(idx.decl()) 5813 if isinstance(idx, SortRef): 5814 return self.get_universe(idx) 5816 _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected") 5820 """Return a list with all symbols that have an interpreation
in the model `self`.
5824 >>> s.add(x > 0, x < 2, f(x) == 0)
5832 for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)): 5833 r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx)) 5834 for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)): 5835 r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx)) 5839 """Return true
if n
is a Z3 expression of the form (_
as-array f).
""" 5840 return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast()) 5842 def get_as_array_func(n): 5843 """Return the function declaration f associated with a Z3 expression of the form (_
as-array f).
""" 5845 _z3_assert(is_as_array(n), "as-array Z3 expression expected.") 5846 return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx) 5848 ######################################### 5852 ######################################### 5854 """Statistics
for `Solver.check()`.
""" 5856 def __init__(self, stats, ctx): 5859 Z3_stats_inc_ref(self.ctx.ref(), self.stats) 5861 def __deepcopy__(self, memo={}): 5862 return Statistics(self.stats, self.ctx) 5865 if self.ctx.ref() is not None: 5866 Z3_stats_dec_ref(self.ctx.ref(), self.stats) 5872 out.write(u('<table border="1" cellpadding="2" cellspacing="0">')) 5875 out.write(u('<tr style="background-color:#CFCFCF">')) 5878 out.write(u('<tr>')) 5880 out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v))) 5881 out.write(u('</table>')) 5882 return out.getvalue() 5884 return Z3_stats_to_string(self.ctx.ref(), self.stats) 5887 """Return the number of statistical counters.
5890 >>> s =
Then(
'simplify',
'nlsat').solver()
5894 >>> st = s.statistics()
5898 return int(Z3_stats_size(self.ctx.ref(), self.stats)) 5900 def __getitem__(self, idx): 5901 """Return the value of statistical counter at position `idx`. The result
is a pair (key, value).
5904 >>> s =
Then(
'simplify',
'nlsat').solver()
5908 >>> st = s.statistics()
5912 (
'nlsat propagations', 2)
5916 if idx >= len(self): 5918 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 5919 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 5921 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 5922 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val) 5925 """Return the list of statistical counters.
5928 >>> s =
Then(
'simplify',
'nlsat').solver()
5932 >>> st = s.statistics()
5934 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))] 5936 def get_key_value(self, key): 5937 """Return the value of a particular statistical counter.
5940 >>> s =
Then(
'simplify',
'nlsat').solver()
5944 >>> st = s.statistics()
5945 >>> st.get_key_value(
'nlsat propagations')
5948 for idx in range(len(self)): 5949 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx): 5950 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 5951 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 5953 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 5954 raise Z3Exception("unknown key") 5956 def __getattr__(self, name): 5957 """Access the value of statistical using attributes.
5959 Remark: to access a counter containing blank spaces (e.g.,
'nlsat propagations'),
5960 we should use
'_' (e.g.,
'nlsat_propagations').
5963 >>> s =
Then(
'simplify',
'nlsat').solver()
5967 >>> st = s.statistics()
5968 >>> st.nlsat_propagations
5973 key = name.replace('_', ' ') 5975 return self.get_key_value(key) 5977 raise AttributeError 5979 ######################################### 5983 ######################################### 5984 class CheckSatResult: 5985 """Represents the result of a satisfiability check: sat, unsat, unknown.
5991 >>> isinstance(r, CheckSatResult)
5995 def __init__(self, r): 5998 def __deepcopy__(self, memo={}): 5999 return CheckSatResult(self.r) 6001 def __eq__(self, other): 6002 return isinstance(other, CheckSatResult) and self.r == other.r 6004 def __ne__(self, other): 6005 return not self.__eq__(other) 6009 if self.r == Z3_L_TRUE: 6011 elif self.r == Z3_L_FALSE: 6012 return "<b>unsat</b>" 6014 return "<b>unknown</b>" 6016 if self.r == Z3_L_TRUE: 6018 elif self.r == Z3_L_FALSE: 6023 sat = CheckSatResult(Z3_L_TRUE) 6024 unsat = CheckSatResult(Z3_L_FALSE) 6025 unknown = CheckSatResult(Z3_L_UNDEF) 6027 class Solver(Z3PPObject): 6028 """Solver API provides methods
for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.
""" 6030 def __init__(self, solver=None, ctx=None): 6031 assert solver is None or ctx is not None 6032 self.ctx = _get_ctx(ctx) 6035 self.solver = Z3_mk_solver(self.ctx.ref()) 6037 self.solver = solver 6038 Z3_solver_inc_ref(self.ctx.ref(), self.solver) 6040 def __deepcopy__(self, memo={}): 6041 return Solver(self.solver, self.ctx) 6044 if self.solver is not None and self.ctx.ref() is not None: 6045 Z3_solver_dec_ref(self.ctx.ref(), self.solver) 6047 def set(self, *args, **keys): 6048 """Set a configuration option. The method `
help()`
return a string containing all available options.
6052 >>> s.set(mbqi=
True)
6053 >>> s.set(
'MBQI',
True)
6054 >>> s.set(
':mbqi',
True)
6056 p = args2params(args, keys, self.ctx) 6057 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params) 6060 """Create a backtracking point.
6079 Z3_solver_push(self.ctx.ref(), self.solver) 6081 def pop(self, num=1): 6082 """Backtrack \c num backtracking points.
6101 Z3_solver_pop(self.ctx.ref(), self.solver, num) 6103 def num_scopes(self): 6104 """Return the current number of backtracking points.
6119 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver) 6122 """Remove all asserted constraints
and backtracking points created using `
push()`.
6133 Z3_solver_reset(self.ctx.ref(), self.solver) 6135 def assert_exprs(self, *args): 6136 """Assert constraints into the solver.
6140 >>> s.assert_exprs(x > 0, x < 2)
6144 args = _get_args(args) 6145 s = BoolSort(self.ctx) 6147 if isinstance(arg, Goal) or isinstance(arg, AstVector): 6149 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast()) 6152 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast()) 6154 def add(self, *args): 6155 """Assert constraints into the solver.
6159 >>> s.add(x > 0, x < 2)
6163 self.assert_exprs(*args) 6165 def __iadd__(self, fml): 6169 def append(self, *args): 6170 """Assert constraints into the solver.
6174 >>> s.append(x > 0, x < 2)
6178 self.assert_exprs(*args) 6180 def insert(self, *args): 6181 """Assert constraints into the solver.
6185 >>> s.insert(x > 0, x < 2)
6189 self.assert_exprs(*args) 6191 def assert_and_track(self, a, p): 6192 """Assert constraint `a`
and track it
in the unsat core using the Boolean constant `p`.
6194 If `p`
is a string, it will be automatically converted into a Boolean constant.
6199 >>> s.set(unsat_core=
True)
6200 >>> s.assert_and_track(x > 0,
'p1')
6201 >>> s.assert_and_track(x != 1,
'p2')
6202 >>> s.assert_and_track(x < 0, p3)
6203 >>> print(s.check())
6205 >>> c = s.unsat_core()
6215 if isinstance(p, str): 6216 p = Bool(p, self.ctx) 6217 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected") 6218 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected") 6219 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast()) 6221 def check(self, *assumptions): 6222 """Check whether the assertions
in the given solver plus the optional assumptions are consistent
or not.
6228 >>> s.add(x > 0, x < 2)
6237 >>> s.add(2**x == 4)
6241 assumptions = _get_args(assumptions) 6242 num = len(assumptions) 6243 _assumptions = (Ast * num)() 6244 for i in range(num): 6245 _assumptions[i] = assumptions[i].as_ast() 6246 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions) 6247 return CheckSatResult(r) 6250 """Return a model
for the last `
check()`.
6252 This function raises an exception
if 6253 a model
is not available (e.g., last `
check()` returned unsat).
6257 >>> s.add(a + 2 == 0)
6264 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx) 6266 raise Z3Exception("model is not available") 6268 def unsat_core(self): 6269 """Return a subset (
as an AST vector) of the assumptions provided to the last
check().
6271 These are the assumptions Z3 used
in the unsatisfiability proof.
6272 Assumptions are available
in Z3. They are used to extract unsatisfiable cores.
6273 They may be also used to
"retract" assumptions. Note that, assumptions are
not really
6274 "soft constraints", but they can be used to implement them.
6276 >>> p1, p2, p3 =
Bools(
'p1 p2 p3')
6277 >>> x, y =
Ints(
'x y')
6282 >>> s.add(
Implies(p3, y > -3))
6283 >>> s.check(p1, p2, p3)
6285 >>> core = s.unsat_core()
6298 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx) 6300 def consequences(self, assumptions, variables): 6301 """Determine fixed values
for the variables based on the solver state
and assumptions.
6303 >>> a, b, c, d =
Bools(
'a b c d')
6305 >>> s.consequences([a],[b,c,d])
6307 >>> s.consequences([
Not(c),d],[a,b,c,d])
6310 if isinstance(assumptions, list): 6311 _asms = AstVector(None, self.ctx) 6312 for a in assumptions: 6315 if isinstance(variables, list): 6316 _vars = AstVector(None, self.ctx) 6320 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected") 6321 _z3_assert(isinstance(variables, AstVector), "ast vector expected") 6322 consequences = AstVector(None, self.ctx) 6323 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector) 6324 sz = len(consequences) 6325 consequences = [ consequences[i] for i in range(sz) ] 6326 return CheckSatResult(r), consequences 6328 def from_file(self, filename): 6329 """Parse assertions
from a file
""" 6331 Z3_solver_from_file(self.ctx.ref(), self.solver, filename) 6332 except Z3Exception as e: 6333 _handle_parse_error(e, self.ctx) 6335 def from_string(self, s): 6336 """Parse assertions
from a string
""" 6338 Z3_solver_from_string(self.ctx.ref(), self.solver, s) 6339 except Z3Exception as e: 6340 _handle_parse_error(e, self.ctx) 6343 """Return a proof
for the last `
check()`. Proof construction must be enabled.
""" 6344 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx) 6346 def assertions(self): 6347 """Return an AST vector containing all added constraints.
6358 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx) 6360 def statistics(self): 6361 """Return statistics
for the last `
check()`.
6368 >>> st = s.statistics()
6369 >>> st.get_key_value(
'final checks')
6376 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx) 6378 def reason_unknown(self): 6379 """Return a string describing why the last `
check()` returned `unknown`.
6383 >>> s.add(2**x == 4)
6386 >>> s.reason_unknown()
6387 '(incomplete (theory arithmetic))' 6389 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver) 6392 """Display a string describing all available options.
""" 6393 print(Z3_solver_get_help(self.ctx.ref(), self.solver)) 6395 def param_descrs(self): 6396 """Return the parameter description set.
""" 6397 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx) 6400 """Return a formatted string with all added constraints.
""" 6401 return obj_to_string(self) 6403 def translate(self, target): 6404 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
6409 >>> s2 = s1.translate(c2)
6412 _z3_assert(isinstance(target, Context), "argument must be a Z3 context") 6413 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) 6414 return Solver(solver, target) 6417 """Return a formatted string (
in Lisp-like format) with all added constraints. We say the string
is in s-expression format.
6425 return Z3_solver_to_string(self.ctx.ref(), self.solver) 6428 """return SMTLIB2 formatted benchmark
for solver
's assertions""" 6435 for i
in range(sz1):
6436 v[i] = es[i].as_ast()
6438 e = es[sz1].as_ast()
6444 """Create a solver customized for the given logic. 6446 The parameter `logic` is a string. It should be contains 6447 the name of a SMT-LIB logic. 6448 See http://www.smtlib.org/ for the name of all available logics. 6450 >>> s = SolverFor("QF_LIA") 6464 """Return a simple general purpose solver with limited amount of preprocessing. 6466 >>> s = SimpleSolver() 6482 """Fixedpoint API provides methods for solving with recursive predicates""" 6485 assert fixedpoint
is None or ctx
is not None 6488 if fixedpoint
is None:
6499 if self.
fixedpoint is not None and self.
ctx.ref()
is not None:
6503 """Set a configuration option. The method `help()` return a string containing all available options. 6509 """Display a string describing all available options.""" 6513 """Return the parameter description set.""" 6517 """Assert constraints as background axioms for the fixedpoint solver.""" 6518 args = _get_args(args)
6521 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
6531 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6539 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6543 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6547 """Assert rules defining recursive predicates to the fixedpoint solver. 6550 >>> s = Fixedpoint() 6551 >>> s.register_relation(a.decl()) 6552 >>> s.register_relation(b.decl()) 6565 body = _get_args(body)
6569 def rule(self, head, body = None, name = None):
6570 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 6574 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 6578 """Query the fixedpoint engine whether formula is derivable. 6579 You can also pass an tuple or list of recursive predicates. 6581 query = _get_args(query)
6583 if sz >= 1
and isinstance(query[0], FuncDeclRef):
6584 _decls = (FuncDecl * sz)()
6594 query =
And(query, self.
ctx)
6595 query = self.
abstract(query,
False)
6600 """Query the fixedpoint engine whether formula is derivable starting at the given query level. 6602 query = _get_args(query)
6604 if sz >= 1
and isinstance(query[0], FuncDecl):
6605 _z3_assert (
False,
"unsupported")
6611 query = self.
abstract(query,
False)
6612 r = Z3_fixedpoint_query_from_lvl (self.
ctx.ref(), self.
fixedpoint, query.as_ast(), lvl)
6616 """create a backtracking point for added rules, facts and assertions""" 6620 """restore to previously created backtracking point""" 6628 body = _get_args(body)
6633 """Retrieve answer from last query call.""" 6635 return _to_expr_ref(r, self.
ctx)
6638 """Retrieve a ground cex from last query call.""" 6639 r = Z3_fixedpoint_get_ground_sat_answer(self.
ctx.ref(), self.
fixedpoint)
6640 return _to_expr_ref(r, self.
ctx)
6643 """retrieve rules along the counterexample trace""" 6647 """retrieve rule names along the counterexample trace""" 6650 names = _symbol2py (self.
ctx, Z3_fixedpoint_get_rule_names_along_trace(self.
ctx.ref(), self.
fixedpoint))
6652 return names.split (
';')
6655 """Retrieve number of levels used for predicate in PDR engine""" 6659 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)""" 6661 return _to_expr_ref(r, self.
ctx)
6664 """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)""" 6668 """Register relation as recursive""" 6669 relations = _get_args(relations)
6674 """Control how relation is represented""" 6675 representations = _get_args(representations)
6676 representations = [
to_symbol(s)
for s
in representations]
6677 sz = len(representations)
6678 args = (Symbol * sz)()
6680 args[i] = representations[i]
6684 """Parse rules and queries from a string""" 6687 except Z3Exception
as e:
6688 _handle_parse_error(e, self.
ctx)
6691 """Parse rules and queries from a file""" 6694 except Z3Exception
as e:
6695 _handle_parse_error(e, self.
ctx)
6698 """retrieve rules that have been added to fixedpoint context""" 6702 """retrieve assertions that have been added to fixedpoint context""" 6706 """Return a formatted string with all added rules and constraints.""" 6710 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 6715 """Return a formatted string (in Lisp-like format) with all added constraints. 6716 We say the string is in s-expression format. 6717 Include also queries. 6719 args, len = _to_ast_array(queries)
6723 """Return statistics for the last `query()`. 6728 """Return a string describing why the last `query()` returned `unknown`. 6733 """Add variable or several variables. 6734 The added variable or variables will be bound in the rules 6737 vars = _get_args(vars)
6757 """Finite domain sort.""" 6760 """Return the size of the finite domain sort""" 6761 r = (ctype.c_ulonglong * 1)()
6765 raise Z3Exception(
"Failed to retrieve finite domain sort size")
6768 """Create a named finite domain sort of a given size sz""" 6769 if not isinstance(name, Symbol):
6775 """Return True if `s` is a Z3 finite-domain sort. 6777 >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) 6779 >>> is_finite_domain_sort(IntSort()) 6782 return isinstance(s, FiniteDomainSortRef)
6786 """Finite-domain expressions.""" 6789 """Return the sort of the finite-domain expression `self`.""" 6793 """Return a Z3 floating point expression as a Python string.""" 6797 """Return `True` if `a` is a Z3 finite-domain expression. 6799 >>> s = FiniteDomainSort('S', 100) 6800 >>> b = Const('b', s) 6801 >>> is_finite_domain(b) 6803 >>> is_finite_domain(Int('x')) 6806 return isinstance(a, FiniteDomainRef)
6810 """Integer values.""" 6813 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. 6815 >>> s = FiniteDomainSort('S', 100) 6816 >>> v = FiniteDomainVal(3, s) 6825 """Return a Z3 finite-domain numeral as a Python string. 6827 >>> s = FiniteDomainSort('S', 100) 6828 >>> v = FiniteDomainVal(42, s) 6836 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. 6838 >>> s = FiniteDomainSort('S', 256) 6839 >>> FiniteDomainVal(255, s) 6841 >>> FiniteDomainVal('100', s) 6850 """Return `True` if `a` is a Z3 finite-domain value. 6852 >>> s = FiniteDomainSort('S', 100) 6853 >>> b = Const('b', s) 6854 >>> is_finite_domain_value(b) 6856 >>> b = FiniteDomainVal(10, s) 6859 >>> is_finite_domain_value(b) 6904 """Optimize API provides methods for solving using objective functions and weighted soft constraints""" 6915 if self.
optimize is not None and self.
ctx.ref()
is not None:
6919 """Set a configuration option. The method `help()` return a string containing all available options. 6925 """Display a string describing all available options.""" 6929 """Return the parameter description set.""" 6933 """Assert constraints as background axioms for the optimize solver.""" 6934 args = _get_args(args)
6936 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
6943 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr.""" 6951 """Add soft constraint with optional weight and optional identifier. 6952 If no weight is supplied, then the penalty for violating the soft constraint 6954 Soft constraints are grouped by identifiers. Soft constraints that are 6955 added without identifiers are grouped by default. 6958 weight =
"%d" % weight
6959 elif isinstance(weight, float):
6960 weight =
"%f" % weight
6961 if not isinstance(weight, str):
6962 raise Z3Exception(
"weight should be a string or an integer")
6970 """Add objective function to maximize.""" 6974 """Add objective function to minimize.""" 6978 """create a backtracking point for added rules, facts and assertions""" 6982 """restore to previously created backtracking point""" 6986 """Check satisfiability while optimizing objective functions.""" 6990 """Return a string that describes why the last `check()` returned `unknown`.""" 6994 """Return a model for the last check().""" 6998 raise Z3Exception(
"model is not available")
7001 if not isinstance(obj, OptimizeObjective):
7002 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7006 if not isinstance(obj, OptimizeObjective):
7007 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7011 if not isinstance(obj, OptimizeObjective):
7012 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7013 return obj.lower_values()
7016 if not isinstance(obj, OptimizeObjective):
7017 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7018 return obj.upper_values()
7021 """Parse assertions and objectives from a file""" 7024 except Z3Exception
as e:
7025 _handle_parse_error(e, self.
ctx)
7028 """Parse assertions and objectives from a string""" 7031 except Z3Exception
as e:
7032 _handle_parse_error(e, self.
ctx)
7035 """Return an AST vector containing all added constraints.""" 7039 """returns set of objective functions""" 7043 """Return a formatted string with all added rules and constraints.""" 7047 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 7052 """Return statistics for the last check`. 7065 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters.""" 7076 if self.
ctx.ref()
is not None:
7080 """Return the number of subgoals in `self`. 7082 >>> a, b = Ints('a b') 7084 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7085 >>> t = Tactic('split-clause') 7089 >>> t = Then(Tactic('split-clause'), Tactic('split-clause')) 7092 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values')) 7099 """Return one of the subgoals stored in ApplyResult object `self`. 7101 >>> a, b = Ints('a b') 7103 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7104 >>> t = Tactic('split-clause') 7107 [a == 0, Or(b == 0, b == 1), a > b] 7109 [a == 1, Or(b == 0, b == 1), a > b] 7111 if idx >= len(self):
7116 return obj_to_string(self)
7119 """Return a textual representation of the s-expression representing the set of subgoals in `self`.""" 7123 """Convert a model for a subgoal into a model for the original goal. 7125 >>> a, b = Ints('a b') 7127 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 7128 >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs')) 7131 [Or(b == 0, b == 1), Not(0 <= b)] 7133 [Or(b == 0, b == 1), Not(1 <= b)] 7134 >>> # Remark: the subgoal r[0] is unsatisfiable 7135 >>> # Creating a solver for solving the second subgoal 7142 >>> # Model s.model() does not assign a value to `a` 7143 >>> # It is a model for subgoal `r[1]`, but not for goal `g` 7144 >>> # The method convert_model creates a model for `g` from a model for `r[1]`. 7145 >>> r.convert_model(s.model(), 1) 7149 _z3_assert(idx < len(self),
"index out of bounds")
7150 _z3_assert(isinstance(model, ModelRef),
"Z3 Model expected")
7154 """Return a Z3 expression consisting of all subgoals. 7159 >>> g.add(Or(x == 2, x == 3)) 7160 >>> r = Tactic('simplify')(g) 7162 [[Not(x <= 1), Or(x == 2, x == 3)]] 7164 And(Not(x <= 1), Or(x == 2, x == 3)) 7165 >>> r = Tactic('split-clause')(g) 7167 [[x > 1, x == 2], [x > 1, x == 3]] 7169 Or(And(x > 1, x == 2), And(x > 1, x == 3)) 7185 """Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver(). 7187 Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond(). 7192 if isinstance(tactic, TacticObj):
7196 _z3_assert(isinstance(tactic, str),
"tactic name expected")
7200 raise Z3Exception(
"unknown tactic '%s'" % tactic)
7207 if self.
tactic is not None and self.
ctx.ref()
is not None:
7211 """Create a solver using the tactic `self`. 7213 The solver supports the methods `push()` and `pop()`, but it 7214 will always solve each `check()` from scratch. 7216 >>> t = Then('simplify', 'nlsat') 7219 >>> s.add(x**2 == 2, x > 0) 7227 def apply(self, goal, *arguments, **keywords):
7228 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7230 >>> x, y = Ints('x y') 7231 >>> t = Tactic('solve-eqs') 7232 >>> t.apply(And(x == 0, y >= x + 1)) 7236 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expressions expected")
7237 goal = _to_goal(goal)
7238 if len(arguments) > 0
or len(keywords) > 0:
7245 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7247 >>> x, y = Ints('x y') 7248 >>> t = Tactic('solve-eqs') 7249 >>> t(And(x == 0, y >= x + 1)) 7252 return self.
apply(goal, *arguments, **keywords)
7255 """Display a string containing a description of the available options for the `self` tactic.""" 7259 """Return the parameter description set.""" 7263 if isinstance(a, BoolRef):
7264 goal =
Goal(ctx = a.ctx)
7270 def _to_tactic(t, ctx=None):
7271 if isinstance(t, Tactic):
7276 def _and_then(t1, t2, ctx=None):
7277 t1 = _to_tactic(t1, ctx)
7278 t2 = _to_tactic(t2, ctx)
7280 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7283 def _or_else(t1, t2, ctx=None):
7284 t1 = _to_tactic(t1, ctx)
7285 t2 = _to_tactic(t2, ctx)
7287 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7291 """Return a tactic that applies the tactics in `*ts` in sequence. 7293 >>> x, y = Ints('x y') 7294 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) 7295 >>> t(And(x == 0, y > x + 1)) 7297 >>> t(And(x == 0, y > x + 1)).as_expr() 7301 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7302 ctx = ks.get(
'ctx',
None)
7305 for i
in range(num - 1):
7306 r = _and_then(r, ts[i+1], ctx)
7310 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). 7312 >>> x, y = Ints('x y') 7313 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) 7314 >>> t(And(x == 0, y > x + 1)) 7316 >>> t(And(x == 0, y > x + 1)).as_expr() 7322 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). 7325 >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) 7326 >>> # Tactic split-clause fails if there is no clause in the given goal. 7329 >>> t(Or(x == 0, x == 1)) 7330 [[x == 0], [x == 1]] 7333 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7334 ctx = ks.get(
'ctx',
None)
7337 for i
in range(num - 1):
7338 r = _or_else(r, ts[i+1], ctx)
7342 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). 7345 >>> t = ParOr(Tactic('simplify'), Tactic('fail')) 7350 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7351 ctx = _get_ctx(ks.get(
'ctx',
None))
7352 ts = [ _to_tactic(t, ctx)
for t
in ts ]
7354 _args = (TacticObj * sz)()
7356 _args[i] = ts[i].tactic
7360 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. 7362 >>> x, y = Ints('x y') 7363 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) 7364 >>> t(And(Or(x == 1, x == 2), y == x + 1)) 7365 [[x == 1, y == 2], [x == 2, y == 3]] 7367 t1 = _to_tactic(t1, ctx)
7368 t2 = _to_tactic(t2, ctx)
7370 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7374 """Alias for ParThen(t1, t2, ctx).""" 7378 """Return a tactic that applies tactic `t` using the given configuration options. 7380 >>> x, y = Ints('x y') 7381 >>> t = With(Tactic('simplify'), som=True) 7382 >>> t((x + 1)*(y + 2) == 0) 7383 [[2*x + y + x*y == -2]] 7385 ctx = keys.pop(
'ctx',
None)
7386 t = _to_tactic(t, ctx)
7391 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. 7393 >>> x, y = Ints('x y') 7394 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) 7395 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) 7397 >>> for subgoal in r: print(subgoal) 7398 [x == 0, y == 0, x > y] 7399 [x == 0, y == 1, x > y] 7400 [x == 1, y == 0, x > y] 7401 [x == 1, y == 1, x > y] 7402 >>> t = Then(t, Tactic('propagate-values')) 7406 t = _to_tactic(t, ctx)
7410 """Return a tactic that applies `t` to a given goal for `ms` milliseconds. 7412 If `t` does not terminate in `ms` milliseconds, then it fails. 7414 t = _to_tactic(t, ctx)
7418 """Return a list of all available tactics in Z3. 7421 >>> l.count('simplify') == 1 7428 """Return a short description for the tactic named `name`. 7430 >>> d = tactic_description('simplify') 7436 """Display a (tabular) description of all available tactics in Z3.""" 7439 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7442 print(
'<tr style="background-color:#CFCFCF">')
7447 print(
'<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(
tactic_description(t), 40)))
7454 """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.""" 7458 if isinstance(probe, ProbeObj):
7460 elif isinstance(probe, float):
7462 elif _is_int(probe):
7464 elif isinstance(probe, bool):
7471 _z3_assert(isinstance(probe, str),
"probe name expected")
7475 raise Z3Exception(
"unknown probe '%s'" % probe)
7482 if self.
probe is not None and self.
ctx.ref()
is not None:
7486 """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`. 7488 >>> p = Probe('size') < 10 7499 """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`. 7501 >>> p = Probe('size') > 10 7512 """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`. 7514 >>> p = Probe('size') <= 2 7525 """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`. 7527 >>> p = Probe('size') >= 2 7538 """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`. 7540 >>> p = Probe('size') == 2 7551 """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`. 7553 >>> p = Probe('size') != 2 7565 """Evaluate the probe `self` in the given goal. 7567 >>> p = Probe('size') 7577 >>> p = Probe('num-consts') 7580 >>> p = Probe('is-propositional') 7583 >>> p = Probe('is-qflia') 7588 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expression expected")
7589 goal = _to_goal(goal)
7593 """Return `True` if `p` is a Z3 probe. 7595 >>> is_probe(Int('x')) 7597 >>> is_probe(Probe('memory')) 7600 return isinstance(p, Probe)
7602 def _to_probe(p, ctx=None):
7606 return Probe(p, ctx)
7609 """Return a list of all available probes in Z3. 7612 >>> l.count('memory') == 1 7619 """Return a short description for the probe named `name`. 7621 >>> d = probe_description('memory') 7627 """Display a (tabular) description of all available probes in Z3.""" 7630 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7633 print(
'<tr style="background-color:#CFCFCF">')
7638 print(
'<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(
probe_description(p), 40)))
7644 def _probe_nary(f, args, ctx):
7646 _z3_assert(len(args) > 0,
"At least one argument expected")
7648 r = _to_probe(args[0], ctx)
7649 for i
in range(num - 1):
7650 r =
Probe(f(ctx.ref(), r.probe, _to_probe(args[i+1], ctx).probe), ctx)
7653 def _probe_and(args, ctx):
7654 return _probe_nary(Z3_probe_and, args, ctx)
7656 def _probe_or(args, ctx):
7657 return _probe_nary(Z3_probe_or, args, ctx)
7660 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 7662 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. 7664 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) 7665 >>> x, y = Ints('x y') 7671 >>> g.add(x == y + 1) 7673 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 7675 p = _to_probe(p, ctx)
7679 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 7681 >>> t = When(Probe('size') > 2, Tactic('simplify')) 7682 >>> x, y = Ints('x y') 7688 >>> g.add(x == y + 1) 7690 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 7692 p = _to_probe(p, ctx)
7693 t = _to_tactic(t, ctx)
7697 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. 7699 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt')) 7701 p = _to_probe(p, ctx)
7702 t1 = _to_tactic(t1, ctx)
7703 t2 = _to_tactic(t2, ctx)
7713 """Simplify the expression `a` using the given options. 7715 This function has many options. Use `help_simplify` to obtain the complete list. 7719 >>> simplify(x + 1 + y + x + 1) 7721 >>> simplify((x + 1)*(y + 1), som=True) 7723 >>> simplify(Distinct(x, y, 1), blast_distinct=True) 7724 And(Not(x == y), Not(x == 1), Not(y == 1)) 7725 >>> simplify(And(x == 0, y == 1), elim_and=True) 7726 Not(Or(Not(x == 0), Not(y == 1))) 7729 _z3_assert(
is_expr(a),
"Z3 expression expected")
7730 if len(arguments) > 0
or len(keywords) > 0:
7732 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
7734 return _to_expr_ref(
Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
7737 """Return a string describing all options available for Z3 `simplify` procedure.""" 7741 """Return the set of parameter descriptions for Z3 `simplify` procedure.""" 7745 """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. 7749 >>> substitute(x + 1, (x, y + 1)) 7751 >>> f = Function('f', IntSort(), IntSort()) 7752 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 7755 if isinstance(m, tuple):
7757 if isinstance(m1, list):
7760 _z3_assert(
is_expr(t),
"Z3 expression expected")
7761 _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.")
7763 _from = (Ast * num)()
7765 for i
in range(num):
7766 _from[i] = m[i][0].as_ast()
7767 _to[i] = m[i][1].as_ast()
7768 return _to_expr_ref(
Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
7771 """Substitute the free variables in t with the expression in m. 7773 >>> v0 = Var(0, IntSort()) 7774 >>> v1 = Var(1, IntSort()) 7776 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 7777 >>> # replace v0 with x+1 and v1 with x 7778 >>> substitute_vars(f(v0, v1), x + 1, x) 7782 _z3_assert(
is_expr(t),
"Z3 expression expected")
7783 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
7786 for i
in range(num):
7787 _to[i] = m[i].as_ast()
7791 """Create the sum of the Z3 expressions. 7793 >>> a, b, c = Ints('a b c') 7798 >>> A = IntVector('a', 5) 7800 a__0 + a__1 + a__2 + a__3 + a__4 7802 args = _get_args(args)
7805 ctx = _ctx_from_ast_arg_list(args)
7807 return _reduce(
lambda a, b: a + b, args, 0)
7808 args = _coerce_expr_list(args, ctx)
7810 return _reduce(
lambda a, b: a + b, args, 0)
7812 _args, sz = _to_ast_array(args)
7817 """Create the product of the Z3 expressions. 7819 >>> a, b, c = Ints('a b c') 7820 >>> Product(a, b, c) 7822 >>> Product([a, b, c]) 7824 >>> A = IntVector('a', 5) 7826 a__0*a__1*a__2*a__3*a__4 7828 args = _get_args(args)
7831 ctx = _ctx_from_ast_arg_list(args)
7833 return _reduce(
lambda a, b: a * b, args, 1)
7834 args = _coerce_expr_list(args, ctx)
7836 return _reduce(
lambda a, b: a * b, args, 1)
7838 _args, sz = _to_ast_array(args)
7842 """Create an at-most Pseudo-Boolean k constraint. 7844 >>> a, b, c = Bools('a b c') 7845 >>> f = AtMost(a, b, c, 2) 7847 args = _get_args(args)
7849 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
7850 ctx = _ctx_from_ast_arg_list(args)
7852 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
7853 args1 = _coerce_expr_list(args[:-1], ctx)
7855 _args, sz = _to_ast_array(args1)
7859 """Create an at-most Pseudo-Boolean k constraint. 7861 >>> a, b, c = Bools('a b c') 7862 >>> f = AtLeast(a, b, c, 2) 7864 args = _get_args(args)
7866 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
7867 ctx = _ctx_from_ast_arg_list(args)
7869 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
7870 args1 = _coerce_expr_list(args[:-1], ctx)
7872 _args, sz = _to_ast_array(args1)
7876 def _pb_args_coeffs(args):
7877 args = _get_args(args)
7878 args, coeffs = zip(*args)
7880 _z3_assert(len(args) > 0,
"Non empty list of arguments expected")
7881 ctx = _ctx_from_ast_arg_list(args)
7883 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
7884 args = _coerce_expr_list(args, ctx)
7885 _args, sz = _to_ast_array(args)
7886 _coeffs = (ctypes.c_int * len(coeffs))()
7887 for i
in range(len(coeffs)):
7888 _coeffs[i] = coeffs[i]
7889 return ctx, sz, _args, _coeffs
7892 """Create a Pseudo-Boolean inequality k constraint. 7894 >>> a, b, c = Bools('a b c') 7895 >>> f = PbLe(((a,1),(b,3),(c,2)), 3) 7897 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
7901 """Create a Pseudo-Boolean inequality k constraint. 7903 >>> a, b, c = Bools('a b c') 7904 >>> f = PbGe(((a,1),(b,3),(c,2)), 3) 7906 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
7910 """Create a Pseudo-Boolean inequality k constraint. 7912 >>> a, b, c = Bools('a b c') 7913 >>> f = PbEq(((a,1),(b,3),(c,2)), 3) 7915 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
7920 """Solve the constraints `*args`. 7922 This is a simple function for creating demonstrations. It creates a solver, 7923 configure it using the options in `keywords`, adds the constraints 7924 in `args`, and invokes check. 7927 >>> solve(a > 0, a < 2) 7933 if keywords.get(
'show',
False):
7937 print(
"no solution")
7939 print(
"failed to solve")
7948 """Solve the constraints `*args` using solver `s`. 7950 This is a simple function for creating demonstrations. It is similar to `solve`, 7951 but it uses the given solver `s`. 7952 It configures solver `s` using the options in `keywords`, adds the constraints 7953 in `args`, and invokes check. 7956 _z3_assert(isinstance(s, Solver),
"Solver object expected")
7959 if keywords.get(
'show',
False):
7964 print(
"no solution")
7966 print(
"failed to solve")
7972 if keywords.get(
'show',
False):
7977 """Try to prove the given claim. 7979 This is a simple function for creating demonstrations. It tries to prove 7980 `claim` by showing the negation is unsatisfiable. 7982 >>> p, q = Bools('p q') 7983 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) 7987 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
7991 if keywords.get(
'show',
False):
7997 print(
"failed to prove")
8000 print(
"counterexample")
8003 def _solve_html(*args, **keywords):
8004 """Version of funcion `solve` used in RiSE4Fun.""" 8008 if keywords.get(
'show',
False):
8009 print(
"<b>Problem:</b>")
8013 print(
"<b>no solution</b>")
8015 print(
"<b>failed to solve</b>")
8021 if keywords.get(
'show',
False):
8022 print(
"<b>Solution:</b>")
8025 def _solve_using_html(s, *args, **keywords):
8026 """Version of funcion `solve_using` used in RiSE4Fun.""" 8028 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8031 if keywords.get(
'show',
False):
8032 print(
"<b>Problem:</b>")
8036 print(
"<b>no solution</b>")
8038 print(
"<b>failed to solve</b>")
8044 if keywords.get(
'show',
False):
8045 print(
"<b>Solution:</b>")
8048 def _prove_html(claim, **keywords):
8049 """Version of funcion `prove` used in RiSE4Fun.""" 8051 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8055 if keywords.get(
'show',
False):
8059 print(
"<b>proved</b>")
8061 print(
"<b>failed to prove</b>")
8064 print(
"<b>counterexample</b>")
8067 def _dict2sarray(sorts, ctx):
8069 _names = (Symbol * sz)()
8070 _sorts = (Sort * sz) ()
8075 _z3_assert(isinstance(k, str),
"String expected")
8076 _z3_assert(
is_sort(v),
"Z3 sort expected")
8080 return sz, _names, _sorts
8082 def _dict2darray(decls, ctx):
8084 _names = (Symbol * sz)()
8085 _decls = (FuncDecl * sz) ()
8090 _z3_assert(isinstance(k, str),
"String expected")
8094 _decls[i] = v.decl().ast
8098 return sz, _names, _decls
8100 def _handle_parse_error(ex, ctx):
8103 raise Z3Exception(msg)
8107 """Parse a string in SMT 2.0 format using the given sorts and decls. 8109 The arguments sorts and decls are Python dictionaries used to initialize 8110 the symbol table used for the SMT 2.0 parser. 8112 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') 8114 >>> x, y = Ints('x y') 8115 >>> f = Function('f', IntSort(), IntSort()) 8116 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) 8118 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) 8122 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 8123 dsz, dnames, ddecls = _dict2darray(decls, ctx) 8125 return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 8126 except Z3Exception as e: 8127 _handle_parse_error(e, ctx) 8129 def parse_smt2_file(f, sorts={}, decls={}, ctx=None): 8130 """Parse a file
in SMT 2.0 format using the given sorts
and decls.
8135 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 8136 dsz, dnames, ddecls = _dict2darray(decls, ctx) 8138 return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 8139 except Z3Exception as e: 8140 _handle_parse_error(e, ctx) 8142 def Interpolant(a,ctx=None): 8143 """Create an interpolation operator.
8145 The argument
is an interpolation pattern (see tree_interpolant).
8151 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) 8154 return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx) 8156 def tree_interpolant(pat,p=None,ctx=None): 8157 """Compute interpolant
for a tree of formulas.
8159 The input
is an interpolation pattern over a set of formulas C.
8160 The pattern pat
is a formula combining the formulas
in C using
8161 logical conjunction
and the
"interp" operator (see Interp). This
8162 interp operator
is logically the identity operator. It marks the
8163 sub-formulas of the pattern
for which interpolants should be
8164 computed. The interpolant
is a map sigma
from marked subformulas
8165 to formulas, such that,
for each marked subformula phi of pat
8166 (where phi sigma
is phi with sigma(psi) substituted
for each
8167 subformula psi of phi such that psi
in dom(sigma)):
8169 1) phi sigma implies sigma(phi),
and 8171 2) sigma(phi)
is in the common uninterpreted vocabulary between
8172 the formulas of C occurring
in phi
and those
not occurring
in 8175 and moreover pat sigma implies false. In the simplest case
8176 an interpolant
for the pattern
"(and (interp A) B)" maps A
8177 to an interpolant
for A /\ B.
8179 The
return value
is a vector of formulas representing sigma. This
8180 vector contains sigma(phi)
for each marked subformula of pat,
in 8181 pre-order traversal. This means that subformulas of phi occur before phi
8182 in the vector. Also, subformulas that occur multiply
in pat will
8183 occur multiply
in the result vector.
8185 If pat
is satisfiable, raises an object of
class ModelRef 8186 that represents a model of pat.
8188 If neither a proof of unsatisfiability nor a model
is obtained
8189 (
for example, because of a timeout,
or because models are disabled)
8190 then
None is returned.
8192 If parameters p are supplied, these are used
in creating the
8193 solver that determines satisfiability.
8198 [
Not(x >= 0),
Not(y <= 2)]
8205 (define-fun x () Int
8209 ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx)) 8210 ptr = (AstVectorObj * 1)() 8211 mptr = (Model * 1)() 8214 res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr) 8215 if res == Z3_L_FALSE: 8216 return AstVector(ptr[0],ctx) 8218 raise ModelRef(mptr[0], ctx) 8221 def binary_interpolant(a,b,p=None,ctx=None): 8222 """Compute an interpolant
for a binary conjunction.
8224 If a & b
is unsatisfiable, returns an interpolant
for a & b.
8225 This
is a formula phi such that
8228 2) b implies
not phi
8229 3) All the uninterpreted symbols of phi occur
in both a
and b.
8231 If a & b
is satisfiable, raises an object of
class ModelRef 8232 that represents a model of a &b.
8234 If neither a proof of unsatisfiability nor a model
is obtained
8235 (
for example, because of a timeout,
or because models are disabled)
8236 then
None is returned.
8238 If parameters p are supplied, these are used
in creating the
8239 solver that determines satisfiability.
8245 f = And(Interpolant(a),b) 8246 ti = tree_interpolant(f,p,ctx) 8247 return ti[0] if ti is not None else None 8249 def sequence_interpolant(v,p=None,ctx=None): 8250 """Compute interpolant
for a sequence of formulas.
8252 If len(v) == N,
and if the conjunction of the formulas
in v
is 8253 unsatisfiable, the interpolant
is a sequence of formulas w
8254 such that len(w) = N-1
and v[0] implies w[0]
and for i
in 0..N-1:
8256 1) w[i] & v[i+1] implies w[i+1] (
or false
if i+1 = N)
8257 2) All uninterpreted symbols
in w[i] occur
in both v[0]..v[i]
8260 Requires len(v) >= 1.
8262 If a & b
is satisfiable, raises an object of
class ModelRef 8263 that represents a model of a & b.
8265 If neither a proof of unsatisfiability nor a model
is obtained
8266 (
for example, because of a timeout,
or because models are disabled)
8267 then
None is returned.
8269 If parameters p are supplied, these are used
in creating the
8270 solver that determines satisfiability.
8275 [
Not(x >= 0),
Not(y >= 0)]
8278 for i in range(1,len(v)): 8279 f = And(Interpolant(f),v[i]) 8280 return tree_interpolant(f,p,ctx) 8283 ######################################### 8285 # Floating-Point Arithmetic 8287 ######################################### 8290 # Global default rounding mode 8291 _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO 8292 _dflt_fpsort_ebits = 11 8293 _dflt_fpsort_sbits = 53 8295 def get_default_rounding_mode(ctx=None): 8296 """Retrieves the
global default rounding mode.
""" 8297 global _dflt_rounding_mode 8298 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO: 8300 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE: 8302 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE: 8304 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: 8306 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: 8309 def set_default_rounding_mode(rm, ctx=None): 8310 global _dflt_rounding_mode 8311 if is_fprm_value(rm): 8312 _dflt_rounding_mode = rm.decl().kind() 8314 _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO or 8315 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE or 8316 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE or 8317 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN or 8318 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, 8319 "illegal rounding mode") 8320 _dflt_rounding_mode = rm 8322 def get_default_fp_sort(ctx=None): 8323 return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx) 8325 def set_default_fp_sort(ebits, sbits, ctx=None): 8326 global _dflt_fpsort_ebits 8327 global _dflt_fpsort_sbits 8328 _dflt_fpsort_ebits = ebits 8329 _dflt_fpsort_sbits = sbits 8331 def _dflt_rm(ctx=None): 8332 return get_default_rounding_mode(ctx) 8334 def _dflt_fps(ctx=None): 8335 return get_default_fp_sort(ctx) 8337 def _coerce_fp_expr_list(alist, ctx): 8338 first_fp_sort = None 8341 if first_fp_sort is None: 8342 first_fp_sort = a.sort() 8343 elif first_fp_sort == a.sort(): 8344 pass # OK, same as before 8346 # we saw at least 2 different float sorts; something will 8347 # throw a sort mismatch later, for now assume None. 8348 first_fp_sort = None 8352 for i in range(len(alist)): 8354 if (isinstance(a, str) and a.contains('2**(') and a.endswith(')')) or _is_int(a) or isinstance(a, float) or isinstance(a, bool): 8355 r.append(FPVal(a, None, first_fp_sort, ctx)) 8358 return _coerce_expr_list(r, ctx) 8363 class FPSortRef(SortRef): 8364 """Floating-point sort.
""" 8367 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint sort `self`.
8372 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast)) 8375 """Retrieves the number of bits reserved
for the significand
in the FloatingPoint sort `self`.
8380 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast)) 8382 def cast(self, val): 8383 """Try to cast `val`
as a floating-point expression.
8387 >>> b.cast(1.0).
sexpr()
8388 '(fp #b0 #x7f #b00000000000000000000000)' 8392 _z3_assert(self.ctx == val.ctx, "Context mismatch") 8395 return FPVal(val, None, self, self.ctx) 8398 def Float16(ctx=None): 8399 """Floating-point 16-bit (half) sort.
""" 8401 return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx) 8403 def FloatHalf(ctx=None): 8404 """Floating-point 16-bit (half) sort.
""" 8406 return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx) 8408 def Float32(ctx=None): 8409 """Floating-point 32-bit (single) sort.
""" 8411 return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx) 8413 def FloatSingle(ctx=None): 8414 """Floating-point 32-bit (single) sort.
""" 8416 return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx) 8418 def Float64(ctx=None): 8419 """Floating-point 64-bit (double) sort.
""" 8421 return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx) 8423 def FloatDouble(ctx=None): 8424 """Floating-point 64-bit (double) sort.
""" 8426 return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx) 8428 def Float128(ctx=None): 8429 """Floating-point 128-bit (quadruple) sort.
""" 8431 return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx) 8433 def FloatQuadruple(ctx=None): 8434 """Floating-point 128-bit (quadruple) sort.
""" 8436 return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx) 8438 class FPRMSortRef(SortRef): 8439 """"Floating-point rounding mode sort.""" 8443 """Return True if `s` is a Z3 floating-point sort.
8450 return isinstance(s, FPSortRef) 8452 def is_fprm_sort(s): 8453 """Return
True if `s`
is a Z3 floating-point rounding mode sort.
8460 return isinstance(s, FPRMSortRef) 8464 class FPRef(ExprRef): 8465 """Floating-point expressions.
""" 8468 """Return the sort of the floating-point expression `self`.
8473 >>> x.sort() ==
FPSort(8, 24)
8476 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 8479 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8484 return self.sort().ebits(); 8487 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8492 return self.sort().sbits(); 8494 def as_string(self): 8495 """Return a Z3 floating point expression
as a Python string.
""" 8496 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8498 def __le__(self, other): 8499 return fpLEQ(self, other, self.ctx) 8501 def __lt__(self, other): 8502 return fpLT(self, other, self.ctx) 8504 def __ge__(self, other): 8505 return fpGEQ(self, other, self.ctx) 8507 def __gt__(self, other): 8508 return fpGT(self, other, self.ctx) 8510 def __add__(self, other): 8511 """Create the Z3 expression `self + other`.
8520 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8521 return fpAdd(_dflt_rm(), a, b, self.ctx) 8523 def __radd__(self, other): 8524 """Create the Z3 expression `other + self`.
8530 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8531 return fpAdd(_dflt_rm(), a, b, self.ctx) 8533 def __sub__(self, other): 8534 """Create the Z3 expression `self - other`.
8543 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8544 return fpSub(_dflt_rm(), a, b, self.ctx) 8546 def __rsub__(self, other): 8547 """Create the Z3 expression `other - self`.
8553 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8554 return fpSub(_dflt_rm(), a, b, self.ctx) 8556 def __mul__(self, other): 8557 """Create the Z3 expression `self * other`.
8568 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8569 return fpMul(_dflt_rm(), a, b, self.ctx) 8571 def __rmul__(self, other): 8572 """Create the Z3 expression `other * self`.
8581 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8582 return fpMul(_dflt_rm(), a, b, self.ctx) 8585 """Create the Z3 expression `+self`.
""" 8589 """Create the Z3 expression `-self`.
8597 def __div__(self, other): 8598 """Create the Z3 expression `self / other`.
8609 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8610 return fpDiv(_dflt_rm(), a, b, self.ctx) 8612 def __rdiv__(self, other): 8613 """Create the Z3 expression `other / self`.
8622 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8623 return fpDiv(_dflt_rm(), a, b, self.ctx) 8625 if not sys.version < '3': 8626 def __truediv__(self, other): 8627 """Create the Z3 expression division `self / other`.
""" 8628 return self.__div__(other) 8630 def __rtruediv__(self, other): 8631 """Create the Z3 expression division `other / self`.
""" 8632 return self.__rdiv__(other) 8634 def __mod__(self, other): 8635 """Create the Z3 expression mod `self % other`.
""" 8636 return fpRem(self, other) 8638 def __rmod__(self, other): 8639 """Create the Z3 expression mod `other % self`.
""" 8640 return fpRem(other, self) 8642 class FPRMRef(ExprRef): 8643 """Floating-point rounding mode expressions
""" 8645 def as_string(self): 8646 """Return a Z3 floating point expression
as a Python string.
""" 8647 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8650 def RoundNearestTiesToEven(ctx=None): 8652 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8656 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8658 def RoundNearestTiesToAway(ctx=None): 8660 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8664 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8666 def RoundTowardPositive(ctx=None): 8668 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8672 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8674 def RoundTowardNegative(ctx=None): 8676 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8680 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8682 def RoundTowardZero(ctx=None): 8684 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8688 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8691 """Return `
True`
if `a`
is a Z3 floating-point rounding mode expression.
8700 return isinstance(a, FPRMRef) 8702 def is_fprm_value(a): 8703 """Return `
True`
if `a`
is a Z3 floating-point rounding mode numeral value.
""" 8704 return is_fprm(a) and _is_numeral(a.ctx, a.ast) 8708 class FPNumRef(FPRef): 8709 """The sign of the numeral.
8719 l = (ctypes.c_int)() 8720 if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False: 8721 raise Z3Exception("error retrieving the sign of a numeral.") 8724 """The sign of a floating-point numeral
as a bit-vector expression.
8726 Remark: NaN
's are invalid arguments. 8728 def sign_as_bv(self): 8729 return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx) 8731 """The significand of the numeral.
8737 def significand(self): 8738 return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast()) 8740 """The significand of the numeral
as a long.
8743 >>> x.significand_as_long()
8746 def significand_as_long(self): 8747 return Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast()) 8749 """The significand of the numeral
as a bit-vector expression.
8751 Remark: NaN are invalid arguments.
8753 def significand_as_bv(self): 8754 return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx) 8756 """The exponent of the numeral.
8762 def exponent(self, biased=True): 8763 return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased) 8765 """The exponent of the numeral
as a long.
8768 >>> x.exponent_as_long()
8771 def exponent_as_long(self, biased=True): 8772 ptr = (ctypes.c_longlong * 1)() 8773 if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased): 8774 raise Z3Exception("error retrieving the exponent of a numeral.") 8777 """The exponent of the numeral
as a bit-vector expression.
8779 Remark: NaNs are invalid arguments.
8781 def exponent_as_bv(self, biased=True): 8782 return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx) 8784 """Indicates whether the numeral
is a NaN.
""" 8786 return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast()) 8788 """Indicates whether the numeral
is +oo
or -oo.
""" 8790 return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast()) 8792 """Indicates whether the numeral
is +zero
or -zero.
""" 8794 return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast()) 8796 """Indicates whether the numeral
is normal.
""" 8798 return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast()) 8800 """Indicates whether the numeral
is subnormal.
""" 8801 def isSubnormal(self): 8802 return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast()) 8804 """Indicates whether the numeral
is postitive.
""" 8805 def isPositive(self): 8806 return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast()) 8808 """Indicates whether the numeral
is negative.
""" 8809 def isNegative(self): 8810 return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast()) 8813 The string representation of the numeral.
8819 def as_string(self): 8820 s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast()) 8821 return ("FPVal(%s, %s)" % (s, self.sort())) 8824 """Return `
True`
if `a`
is a Z3 floating-point expression.
8834 return isinstance(a, FPRef) 8837 """Return `
True`
if `a`
is a Z3 floating-point numeral value.
8848 return is_fp(a) and _is_numeral(a.ctx, a.ast) 8850 def FPSort(ebits, sbits, ctx=None): 8851 """Return a Z3 floating-point sort of the given sizes. If `ctx=
None`, then the
global context
is used.
8853 >>> Single =
FPSort(8, 24)
8854 >>> Double =
FPSort(11, 53)
8857 >>> x =
Const(
'x', Single)
8862 return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx) 8864 def _to_float_str(val, exp=0): 8865 if isinstance(val, float): 8869 sone = math.copysign(1.0, val) 8874 elif val == float("+inf"): 8876 elif val == float("-inf"): 8879 v = val.as_integer_ratio() 8882 rvs = str(num) + '/' + str(den) 8883 res = rvs + 'p' + _to_int_str(exp) 8884 elif isinstance(val, bool): 8891 elif isinstance(val, str): 8892 inx = val.find('*(2**') 8895 elif val[-1] == ')': 8897 exp = str(int(val[inx+5:-1]) + int(exp)) 8899 _z3_assert(False, "String does not have floating-point numeral form.") 8901 _z3_assert(False, "Python value cannot be used to create floating-point numerals.") 8905 return res + 'p' + exp 8909 """Create a Z3 floating-point NaN term.
8912 >>> set_fpa_pretty(
True)
8915 >>> pb = get_fpa_pretty()
8916 >>> set_fpa_pretty(
False)
8919 >>> set_fpa_pretty(pb)
8921 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8922 return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx) 8924 def fpPlusInfinity(s): 8925 """Create a Z3 floating-point +oo term.
8928 >>> pb = get_fpa_pretty()
8929 >>> set_fpa_pretty(
True)
8932 >>> set_fpa_pretty(
False)
8935 >>> set_fpa_pretty(pb)
8937 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8938 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx) 8940 def fpMinusInfinity(s): 8941 """Create a Z3 floating-point -oo term.
""" 8942 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8943 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx) 8945 def fpInfinity(s, negative): 8946 """Create a Z3 floating-point +oo
or -oo term.
""" 8947 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8948 _z3_assert(isinstance(negative, bool), "expected Boolean flag") 8949 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx) 8952 """Create a Z3 floating-point +0.0 term.
""" 8953 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8954 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx) 8957 """Create a Z3 floating-point -0.0 term.
""" 8958 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8959 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx) 8961 def fpZero(s, negative): 8962 """Create a Z3 floating-point +0.0
or -0.0 term.
""" 8963 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8964 _z3_assert(isinstance(negative, bool), "expected Boolean flag") 8965 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx) 8967 def FPVal(sig, exp=None, fps=None, ctx=None): 8968 """Return a floating-point value of value `val`
and sort `fps`. If `ctx=
None`, then the
global context
is used.
8973 >>> print(
"0x%.8x" % v.exponent_as_long(
False))
8993 fps = _dflt_fps(ctx) 8994 _z3_assert(is_fp_sort(fps), "sort mismatch") 8997 val = _to_float_str(sig) 8998 if val == "NaN" or val == "nan": 9001 return fpMinusZero(fps) 9002 elif val == "0.0" or val == "+0.0": 9003 return fpPlusZero(fps) 9004 elif val == "+oo" or val == "+inf" or val == "+Inf": 9005 return fpPlusInfinity(fps) 9006 elif val == "-oo" or val == "-inf" or val == "-Inf": 9007 return fpMinusInfinity(fps) 9009 return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx) 9011 def FP(name, fpsort, ctx=None): 9012 """Return a floating-point constant named `name`.
9013 `fpsort`
is the floating-point sort.
9014 If `ctx=
None`, then the
global context
is used.
9024 >>> x2 =
FP(
'x', word)
9028 if isinstance(fpsort, FPSortRef) and ctx is None: 9032 return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx) 9034 def FPs(names, fpsort, ctx=None): 9035 """Return an array of floating-point constants.
9037 >>> x, y, z =
FPs(
'x y z',
FPSort(8, 24))
9048 if isinstance(names, str): 9049 names = names.split(" ") 9050 return [FP(name, fpsort, ctx) for name in names] 9052 def fpAbs(a, ctx=None): 9053 """Create a Z3 floating-point absolute value expression.
9057 >>> x =
FPVal(1.0, s)
9060 >>> y =
FPVal(-20.0, s)
9065 >>>
fpAbs(-1.25*(2**4))
9071 [a] = _coerce_fp_expr_list([a], ctx) 9072 return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx) 9074 def fpNeg(a, ctx=None): 9075 """Create a Z3 floating-point addition expression.
9086 [a] = _coerce_fp_expr_list([a], ctx) 9087 return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx) 9089 def _mk_fp_unary(f, rm, a, ctx): 9091 [a] = _coerce_fp_expr_list([a], ctx) 9093 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9094 _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression") 9095 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx) 9097 def _mk_fp_unary_norm(f, a, ctx): 9099 [a] = _coerce_fp_expr_list([a], ctx) 9101 _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression") 9102 return FPRef(f(ctx.ref(), a.as_ast()), ctx) 9104 def _mk_fp_unary_pred(f, a, ctx): 9106 [a] = _coerce_fp_expr_list([a], ctx) 9108 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9109 return BoolRef(f(ctx.ref(), a.as_ast()), ctx) 9111 def _mk_fp_bin(f, rm, a, b, ctx): 9113 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9115 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9116 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9117 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx) 9119 def _mk_fp_bin_norm(f, a, b, ctx): 9121 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9123 _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression") 9124 return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 9126 def _mk_fp_bin_pred(f, a, b, ctx): 9128 [a, b] = _coerce_fp_expr_list([a, b], ctx) 9130 _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression") 9131 return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 9133 def _mk_fp_tern(f, rm, a, b, c, ctx): 9135 [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx) 9137 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9138 _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") 9139 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx) 9141 def fpAdd(rm, a, b, ctx=None): 9142 """Create a Z3 floating-point addition expression.
9152 >>>
fpAdd(rm, x, y).sort()
9155 return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx) 9157 def fpSub(rm, a, b, ctx=None): 9158 """Create a Z3 floating-point subtraction expression.
9166 >>>
fpSub(rm, x, y).sort()
9169 return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx) 9171 def fpMul(rm, a, b, ctx=None): 9172 """Create a Z3 floating-point multiplication expression.
9180 >>>
fpMul(rm, x, y).sort()
9183 return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx) 9185 def fpDiv(rm, a, b, ctx=None): 9186 """Create a Z3 floating-point divison expression.
9194 >>>
fpDiv(rm, x, y).sort()
9197 return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx) 9199 def fpRem(a, b, ctx=None): 9200 """Create a Z3 floating-point remainder expression.
9207 >>>
fpRem(x, y).sort()
9210 return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx) 9212 def fpMin(a, b, ctx=None): 9213 """Create a Z3 floating-point minimium expression.
9221 >>>
fpMin(x, y).sort()
9224 return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx) 9226 def fpMax(a, b, ctx=None): 9227 """Create a Z3 floating-point maximum expression.
9235 >>>
fpMax(x, y).sort()
9238 return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx) 9240 def fpFMA(rm, a, b, c, ctx=None): 9241 """Create a Z3 floating-point fused multiply-add expression.
9243 return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx) 9245 def fpSqrt(rm, a, ctx=None): 9246 """Create a Z3 floating-point square root expression.
9248 return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx) 9250 def fpRoundToIntegral(rm, a, ctx=None): 9251 """Create a Z3 floating-point roundToIntegral expression.
9253 return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx) 9255 def fpIsNaN(a, ctx=None): 9256 """Create a Z3 floating-point isNaN expression.
9264 return _mk_fp_unary_norm(Z3_mk_fpa_is_nan, a, ctx) 9266 def fpIsInf(a, ctx=None): 9267 """Create a Z3 floating-point isInfinite expression.
9274 return _mk_fp_unary_norm(Z3_mk_fpa_is_infinite, a, ctx) 9276 def fpIsZero(a, ctx=None): 9277 """Create a Z3 floating-point isZero expression.
9279 return _mk_fp_unary_norm(Z3_mk_fpa_is_zero, a, ctx) 9281 def fpIsNormal(a, ctx=None): 9282 """Create a Z3 floating-point isNormal expression.
9284 return _mk_fp_unary_norm(Z3_mk_fpa_is_normal, a, ctx) 9286 def fpIsSubnormal(a, ctx=None): 9287 """Create a Z3 floating-point isSubnormal expression.
9289 return _mk_fp_unary_norm(Z3_mk_fpa_is_subnormal, a, ctx) 9291 def fpIsNegative(a, ctx=None): 9292 """Create a Z3 floating-point isNegative expression.
9294 return _mk_fp_unary_norm(Z3_mk_fpa_is_negative, a, ctx) 9296 def fpIsPositive(a, ctx=None): 9297 """Create a Z3 floating-point isPositive expression.
9299 return _mk_fp_unary_norm(Z3_mk_fpa_is_positive, a, ctx) 9300 return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) 9302 def _check_fp_args(a, b): 9304 _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") 9306 def fpLT(a, b, ctx=None): 9307 """Create the Z3 floating-point expression `other < self`.
9315 return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx) 9317 def fpLEQ(a, b, ctx=None): 9318 """Create the Z3 floating-point expression `other <= self`.
9323 >>> (x <= y).sexpr()
9326 return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx) 9328 def fpGT(a, b, ctx=None): 9329 """Create the Z3 floating-point expression `other > self`.
9337 return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx) 9339 def fpGEQ(a, b, ctx=None): 9340 """Create the Z3 floating-point expression `other >= self`.
9345 >>> (x >= y).sexpr()
9348 return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx) 9350 def fpEQ(a, b, ctx=None): 9351 """Create the Z3 floating-point expression `
fpEQ(other, self)`.
9356 >>>
fpEQ(x, y).sexpr()
9359 return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx) 9361 def fpNEQ(a, b, ctx=None): 9362 """Create the Z3 floating-point expression `
Not(
fpEQ(other, self))`.
9367 >>> (x != y).sexpr()
9370 return Not(fpEQ(a, b, ctx)) 9372 def fpFP(sgn, exp, sig, ctx=None): 9373 """Create the Z3 floating-point value `
fpFP(sgn, sig, exp)`
from the three bit-vectors sgn, sig,
and exp.
9378 fpFP(1, 127, 4194304)
9379 >>> xv =
FPVal(-1.5, s)
9383 >>> slvr.add(
fpEQ(x, xv))
9386 >>> xv =
FPVal(+1.5, s)
9390 >>> slvr.add(
fpEQ(x, xv))
9394 _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch") 9395 _z3_assert(sgn.sort().size() == 1, "sort mismatch") 9397 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch") 9398 return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx) 9400 def fpToFP(a1, a2=None, a3=None, ctx=None): 9401 """Create a Z3 floating-point conversion expression
from other term sorts
9404 From a bit-vector term
in IEEE 754-2008 format:
9410 From a floating-point term with different precision:
9421 From a signed bit-vector term:
9427 if is_bv(a1) and is_fp_sort(a2): 9428 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx) 9429 elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3): 9430 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9431 elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3): 9432 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9433 elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3): 9434 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9436 raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.") 9438 def fpBVToFP(v, sort, ctx=None): 9439 """Create a Z3 floating-point conversion expression that represents the
9440 conversion
from a bit-vector term to a floating-point term.
9449 _z3_assert(is_bv(v), "First argument must be a Z3 floating-point rounding mode expression.") 9450 _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.") 9452 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx) 9454 def fpFPToFP(rm, v, sort, ctx=None): 9455 """Create a Z3 floating-point conversion expression that represents the
9456 conversion
from a floating-point term to a floating-point term of different precision.
9467 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9468 _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.") 9469 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9471 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9473 def fpRealToFP(rm, v, sort, ctx=None): 9474 """Create a Z3 floating-point conversion expression that represents the
9475 conversion
from a real term to a floating-point term.
9484 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9485 _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.") 9486 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9488 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9490 def fpSignedToFP(rm, v, sort, ctx=None): 9491 """Create a Z3 floating-point conversion expression that represents the
9492 conversion
from a signed bit-vector term (encoding an integer) to a floating-point term.
9501 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9502 _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") 9503 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9505 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9507 def fpUnsignedToFP(rm, v, sort, ctx=None): 9508 """Create a Z3 floating-point conversion expression that represents the
9509 conversion
from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9518 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") 9519 _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") 9520 _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") 9522 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9524 def fpToFPUnsigned(rm, x, s, ctx=None): 9525 """Create a Z3 floating-point conversion expression,
from unsigned bit-vector to floating-point expression.
""" 9527 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9528 _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression") 9529 _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort") 9531 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx) 9533 def fpToSBV(rm, x, s, ctx=None): 9534 """Create a Z3 floating-point conversion expression,
from floating-point expression to signed bit-vector.
9548 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9549 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") 9550 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") 9552 return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9554 def fpToUBV(rm, x, s, ctx=None): 9555 """Create a Z3 floating-point conversion expression,
from floating-point expression to unsigned bit-vector.
9569 _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression") 9570 _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression") 9571 _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort") 9573 return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9575 def fpToReal(x, ctx=None): 9576 """Create a Z3 floating-point conversion expression,
from floating-point expression to real.
9590 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9592 return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx) 9594 def fpToIEEEBV(x, ctx=None): 9595 """\brief Conversion of a floating-point term into a bit-vector term
in IEEE 754-2008 format.
9597 The size of the resulting bit-vector
is automatically determined.
9599 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9600 knows only one NaN
and it will always produce the same bit-vector represenatation of
9615 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9617 return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx) 9621 ######################################### 9623 # Strings, Sequences and Regular expressions 9625 ######################################### 9627 class SeqSortRef(SortRef): 9628 """Sequence sort.
""" 9630 def is_string(self): 9631 """Determine
if sort
is a string
9639 return Z3_is_string_sort(self.ctx_ref(), self.ast) 9642 def StringSort(ctx=None): 9643 """Create a string sort
9649 return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx) 9653 """Create a sequence sort over elements provided
in the argument
9658 return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx) 9660 class SeqRef(ExprRef): 9661 """Sequence expression.
""" 9664 return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 9666 def __add__(self, other): 9667 return Concat(self, other) 9669 def __radd__(self, other): 9670 return Concat(other, self) 9672 def __getitem__(self, i): 9674 i = IntVal(i, self.ctx) 9675 return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) 9677 def is_string(self): 9678 return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast())) 9680 def is_string_value(self): 9681 return Z3_is_string(self.ctx_ref(), self.as_ast()) 9683 def as_string(self): 9684 """Return a string representation of sequence expression.
""" 9685 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 9688 def _coerce_seq(s, ctx=None): 9689 if isinstance(s, str): 9691 s = StringVal(s, ctx) 9693 raise Z3Exception("Non-expression passed as a sequence") 9695 raise Z3Exception("Non-sequence passed as a sequence") 9698 def _get_ctx2(a, b, ctx=None): 9708 """Return `
True`
if `a`
is a Z3 sequence expression.
9714 return isinstance(a, SeqRef) 9717 """Return `
True`
if `a`
is a Z3 string expression.
9721 return isinstance(a, SeqRef) and a.is_string() 9723 def is_string_value(a): 9724 """return 'True' if 'a' is a Z3 string constant expression.
9730 return isinstance(a, SeqRef) and a.is_string_value() 9733 def StringVal(s, ctx=None): 9734 """create a string expression
""" 9736 return SeqRef(Z3_mk_string(ctx.ref(), s), ctx) 9738 def String(name, ctx=None): 9739 """Return a string constant named `name`. If `ctx=
None`, then the
global context
is used.
9744 return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx) 9746 def Strings(names, ctx=None): 9747 """Return a tuple of String constants.
""" 9749 if isinstance(names, str): 9750 names = names.split(" ") 9751 return [String(name, ctx) for name in names] 9754 """Create the empty sequence of the given sort
9768 if isinstance(s, SeqSortRef): 9769 return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx) 9770 if isinstance(s, ReSortRef): 9771 return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx) 9772 raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty") 9775 """Create the regular expression that accepts the universal langauge
9783 if isinstance(s, ReSortRef): 9784 return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx) 9785 raise Z3Exception("Non-sequence, non-regular expression sort passed to Full") 9789 """Create a singleton sequence
""" 9790 return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx) 9793 """Check
if 'a' is a prefix of
'b' 9801 ctx = _get_ctx2(a, b) 9802 a = _coerce_seq(a, ctx) 9803 b = _coerce_seq(b, ctx) 9804 return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 9807 """Check
if 'a' is a suffix of
'b' 9815 ctx = _get_ctx2(a, b) 9816 a = _coerce_seq(a, ctx) 9817 b = _coerce_seq(b, ctx) 9818 return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 9821 """Check
if 'a' contains
'b' 9828 >>> x, y, z =
Strings(
'x y z')
9833 ctx = _get_ctx2(a, b) 9834 a = _coerce_seq(a, ctx) 9835 b = _coerce_seq(b, ctx) 9836 return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 9839 def Replace(s, src, dst): 9840 """Replace the first occurrence of
'src' by
'dst' in 's' 9841 >>> r =
Replace(
"aaa",
"a",
"b")
9845 ctx = _get_ctx2(dst, s) 9846 if ctx is None and is_expr(src): 9848 src = _coerce_seq(src, ctx) 9849 dst = _coerce_seq(dst, ctx) 9850 s = _coerce_seq(s, ctx) 9851 return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx) 9853 def IndexOf(s, substr): 9854 return IndexOf(s, substr, IntVal(0)) 9856 def IndexOf(s, substr, offset): 9857 """Retrieve the index of substring within a string starting at a specified offset.
9866 ctx = _get_ctx2(s, substr, ctx) 9867 s = _coerce_seq(s, ctx) 9868 substr = _coerce_seq(substr, ctx) 9870 offset = IntVal(offset, ctx) 9871 return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx) 9874 """Obtain the length of a sequence
's' 9880 return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx) 9883 """Convert string expression to integer
9895 return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx) 9899 """Convert integer expression to string
""" 9902 return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx) 9905 def Re(s, ctx=None): 9906 """The regular expression that accepts sequence
's' 9911 s = _coerce_seq(s, ctx) 9912 return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx) 9917 ## Regular expressions 9919 class ReSortRef(SortRef): 9920 """Regular expression sort.
""" 9925 return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx) 9926 if s is None or isinstance(s, Context): 9928 return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), s.ctx) 9929 raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument") 9932 class ReRef(ExprRef): 9933 """Regular expressions.
""" 9935 def __add__(self, other): 9936 return Union(self, other) 9940 return isinstance(s, ReRef) 9944 """Create regular expression membership test
9953 s = _coerce_seq(s, re.ctx) 9954 return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx) 9957 """Create union of regular expressions.
9962 args = _get_args(args) 9965 _z3_assert(sz > 0, "At least one argument expected.") 9966 _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") 9972 v[i] = args[i].as_ast() 9973 return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx) 9976 """Create the regular expression accepting one
or more repetitions of argument.
9985 return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx) 9988 """Create the regular expression that optionally accepts the argument.
9997 return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx) 10000 """Create the complement regular expression.
""" 10001 return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx) 10004 """Create the regular expression accepting zero
or more repetitions of argument.
10013 return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx) 10015 def Loop(re, lo, hi=0): 10016 """Create the regular expression accepting between a lower
and upper bound repetitions
10017 >>> re =
Loop(
Re(
"a"), 1, 3)
10025 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_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)
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-Brujin 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 expresson 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)
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, __uint64 size)
Create a named finite domain sort.
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)
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 expresson 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_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, __uint64 *r)
Store the size of the sort in r. Return Z3_FALSE if the call failed. That is, Z3_get_sort_kind(s) == ...
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)