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 to leonardo@microsoft.com. 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
56 return isinstance(v, (int, long))
59 return isinstance(v, int)
68 major = ctypes.c_uint(0)
69 minor = ctypes.c_uint(0)
70 build = ctypes.c_uint(0)
71 rev = ctypes.c_uint(0)
73 return "%s.%s.%s" % (major.value, minor.value, build.value)
76 major = ctypes.c_uint(0)
77 minor = ctypes.c_uint(0)
78 build = ctypes.c_uint(0)
79 rev = ctypes.c_uint(0)
81 return (major.value, minor.value, build.value, rev.value)
88 def _z3_assert(cond, msg):
90 raise Z3Exception(msg)
93 """Log interaction to a file. This function must be invoked immediately after init(). """ 97 """Append user-defined string to interaction log. """ 101 """Convert an integer or string into a Z3 symbol.""" 107 def _symbol2py(ctx, s):
108 """Convert a Z3 symbol back into a Python object. """ 109 if Z3_get_symbol_kind(ctx.ref(), s) == Z3_INT_SYMBOL:
110 return "k!%s" % Z3_get_symbol_int(ctx.ref(), s)
112 return Z3_get_symbol_string(ctx.ref(), s)
114 _error_handler_fptr = ctypes.CFUNCTYPE(
None, ctypes.c_void_p, ctypes.c_uint)
120 if len(args) == 1
and (isinstance(args[0], tuple)
or isinstance(args[0], list)):
122 elif len(args) == 1
and isinstance(args[0], set):
123 return [arg
for arg
in args[0]]
129 def _Z3python_error_handler_core(c, e):
134 _Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)
136 def _to_param_value(val):
137 if isinstance(val, bool):
146 """A Context manages all other Z3 objects, global configuration options, etc. 148 Z3Py uses a default global context. For most applications this is sufficient. 149 An application may use multiple Z3 contexts. Objects created in one context 150 cannot be used in another one. However, several objects may be "translated" from 151 one context to another. It is not safe to access Z3 objects from multiple threads. 152 The only exception is the method `interrupt()` that can be used to interrupt() a long 154 The initialization method receives global configuration options for the new context. 158 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
173 lib().Z3_set_error_handler.restype =
None 174 lib().Z3_set_error_handler.argtypes = [ContextObj, _error_handler_fptr]
183 """Return a reference to the actual C pointer to the Z3 context.""" 187 """Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions. 189 This method can be invoked from a thread different from the one executing the 190 interruptable procedure. 198 """Return a reference to the global Z3 context. 201 >>> x.ctx == main_ctx() 206 >>> x2 = Real('x', c) 213 if _main_ctx
is None:
224 """Set Z3 global (or module) parameters. 226 >>> set_param(precision=10) 229 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
233 if not set_pp_option(k, v):
247 """Reset all global (or module) parameters. 252 """Alias for 'set_param' for backward compatibility. 257 """Return the value of a Z3 global (or module) parameter 259 >>> get_param('nlsat.reorder') 262 ptr = (ctypes.c_char_p * 1)()
264 r = z3core._to_pystr(ptr[0])
266 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
276 """Superclass for all Z3 objects that have support for pretty printing.""" 281 """AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions.""" 288 if self.
ctx.ref()
is not None:
292 return obj_to_string(self)
295 return obj_to_string(self)
298 return self.
eq(other)
311 elif is_eq(self)
and self.num_args() == 2:
312 return self.arg(0).
eq(self.arg(1))
314 raise Z3Exception(
"Symbolic expressions cannot be cast to concrete Boolean values.")
317 """Return an string representing the AST node in s-expression notation. 320 >>> ((x + 1)*x).sexpr() 326 """Return a pointer to the corresponding C Z3_ast object.""" 330 """Return unique identifier for object. It can be used for hash-tables and maps.""" 334 """Return a reference to the C context where this AST node is stored.""" 335 return self.
ctx.ref()
338 """Return `True` if `self` and `other` are structurally identical. 345 >>> n1 = simplify(n1) 346 >>> n2 = simplify(n2) 351 _z3_assert(
is_ast(other),
"Z3 AST expected")
352 return Z3_is_eq_ast(self.
ctx_ref(), self.
as_ast(), other.as_ast())
355 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 361 >>> # Nodes in different contexts can't be mixed. 362 >>> # However, we can translate nodes from one context to another. 363 >>> x.translate(c2) + y 367 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
371 """Return a hashcode for the `self`. 373 >>> n1 = simplify(Int('x') + 1) 374 >>> n2 = simplify(2 + Int('x') - 1) 375 >>> n1.hash() == n2.hash() 381 """Return `True` if `a` is an AST node. 385 >>> is_ast(IntVal(10)) 389 >>> is_ast(BoolSort()) 391 >>> is_ast(Function('f', IntSort(), IntSort())) 398 return isinstance(a, AstRef)
401 """Return `True` if `a` and `b` are structurally identical AST nodes. 411 >>> eq(simplify(x + 1), simplify(1 + x)) 418 def _ast_kind(ctx, a):
421 return Z3_get_ast_kind(ctx.ref(), a)
423 def _ctx_from_ast_arg_list(args, default_ctx=None):
431 _z3_assert(ctx == a.ctx,
"Context mismatch")
436 def _ctx_from_ast_args(*args):
437 return _ctx_from_ast_arg_list(args)
439 def _to_func_decl_array(args):
441 _args = (FuncDecl * sz)()
443 _args[i] = args[i].as_func_decl()
446 def _to_ast_array(args):
450 _args[i] = args[i].as_ast()
453 def _to_ref_array(ref, args):
457 _args[i] = args[i].as_ast()
460 def _to_ast_ref(a, ctx):
461 k = _ast_kind(ctx, a)
463 return _to_sort_ref(a, ctx)
464 elif k == Z3_FUNC_DECL_AST:
465 return _to_func_decl_ref(a, ctx)
467 return _to_expr_ref(a, ctx)
475 def _sort_kind(ctx, s):
476 return Z3_get_sort_kind(ctx.ref(), s)
479 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.""" 481 return Z3_sort_to_ast(self.
ctx_ref(), self.
ast)
487 """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts. 490 >>> b.kind() == Z3_BOOL_SORT 492 >>> b.kind() == Z3_INT_SORT 494 >>> A = ArraySort(IntSort(), IntSort()) 495 >>> A.kind() == Z3_ARRAY_SORT 497 >>> A.kind() == Z3_INT_SORT 500 return _sort_kind(self.
ctx, self.
ast)
503 """Return `True` if `self` is a subsort of `other`. 505 >>> IntSort().subsort(RealSort()) 511 """Try to cast `val` as an element of sort `self`. 513 This method is used in Z3Py to convert Python objects such as integers, 514 floats, longs and strings into Z3 expressions. 517 >>> RealSort().cast(x) 521 _z3_assert(
is_expr(val),
"Z3 expression expected")
522 _z3_assert(self.
eq(val.sort()),
"Sort mismatch")
526 """Return the name (string) of sort `self`. 528 >>> BoolSort().name() 530 >>> ArraySort(IntSort(), IntSort()).name() 533 return _symbol2py(self.
ctx, Z3_get_sort_name(self.
ctx_ref(), self.
ast))
536 """Return `True` if `self` and `other` are the same Z3 sort. 539 >>> p.sort() == BoolSort() 541 >>> p.sort() == IntSort() 546 return Z3_is_eq_sort(self.
ctx_ref(), self.
ast, other.ast)
549 """Return `True` if `self` and `other` are not the same Z3 sort. 552 >>> p.sort() != BoolSort() 554 >>> p.sort() != IntSort() 557 return not Z3_is_eq_sort(self.
ctx_ref(), self.
ast, other.ast)
561 return AstRef.__hash__(self)
564 """Return `True` if `s` is a Z3 sort. 566 >>> is_sort(IntSort()) 568 >>> is_sort(Int('x')) 570 >>> is_expr(Int('x')) 573 return isinstance(s, SortRef)
575 def _to_sort_ref(s, ctx):
577 _z3_assert(isinstance(s, Sort),
"Z3 Sort expected")
578 k = _sort_kind(ctx, s)
579 if k == Z3_BOOL_SORT:
581 elif k == Z3_INT_SORT
or k == Z3_REAL_SORT:
583 elif k == Z3_BV_SORT:
585 elif k == Z3_ARRAY_SORT:
587 elif k == Z3_DATATYPE_SORT:
589 elif k == Z3_FINITE_DOMAIN_SORT:
591 elif k == Z3_FLOATING_POINT_SORT:
593 elif k == Z3_ROUNDING_MODE_SORT:
598 return _to_sort_ref(Z3_get_sort(ctx.ref(), a), ctx)
601 """Create a new uninterpred sort named `name`. 603 If `ctx=None`, then the new sort is declared in the global Z3Py context. 605 >>> A = DeclareSort('A') 606 >>> a = Const('a', A) 607 >>> b = Const('b', A) 625 """Function declaration. Every constant and function have an associated declaration. 627 The declaration assigns a name, a sort (i.e., type), and for function 628 the sort (i.e., type) of each of its arguments. Note that, in Z3, 629 a constant is a function with 0 arguments. 632 return Z3_func_decl_to_ast(self.
ctx_ref(), self.
ast)
641 """Return the name of the function declaration `self`. 643 >>> f = Function('f', IntSort(), IntSort()) 646 >>> isinstance(f.name(), str) 649 return _symbol2py(self.
ctx, Z3_get_decl_name(self.
ctx_ref(), self.
ast))
652 """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0. 654 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 658 return int(Z3_get_arity(self.
ctx_ref(), self.
ast))
661 """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`. 663 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 670 _z3_assert(i < self.
arity(),
"Index out of bounds")
671 return _to_sort_ref(Z3_get_domain(self.
ctx_ref(), self.
ast, i), self.
ctx)
674 """Return the sort of the range of a function declaration. For constants, this is the sort of the constant. 676 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 680 return _to_sort_ref(Z3_get_range(self.
ctx_ref(), self.
ast), self.
ctx)
683 """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc. 686 >>> d = (x + 1).decl() 687 >>> d.kind() == Z3_OP_ADD 689 >>> d.kind() == Z3_OP_MUL 692 return Z3_get_decl_kind(self.
ctx_ref(), self.
ast)
695 """Create a Z3 application expression using the function `self`, and the given arguments. 697 The arguments must be Z3 expressions. This method assumes that 698 the sorts of the elements in `args` match the sorts of the 699 domain. Limited coersion is supported. For example, if 700 args[0] is a Python integer, and the function expects a Z3 701 integer, then the argument is automatically converted into a 704 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 712 args = _get_args(args)
715 _z3_assert(num == self.
arity(),
"Incorrect number of arguments to %s" % self)
716 _args = (Ast * num)()
721 tmp = self.
domain(i).cast(args[i])
723 _args[i] = tmp.as_ast()
727 """Return `True` if `a` is a Z3 function declaration. 729 >>> f = Function('f', IntSort(), IntSort()) 736 return isinstance(a, FuncDeclRef)
739 """Create a new Z3 uninterpreted function with the given sorts. 741 >>> f = Function('f', IntSort(), IntSort()) 747 _z3_assert(len(sig) > 0,
"At least two arguments expected")
751 _z3_assert(
is_sort(rng),
"Z3 sort expected")
752 dom = (Sort * arity)()
753 for i
in range(arity):
755 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
760 def _to_func_decl_ref(a, ctx):
770 """Constraints, formulas and terms are expressions in Z3. 772 Expressions are ASTs. Every expression has a sort. 773 There are three main kinds of expressions: 774 function applications, quantifiers and bounded variables. 775 A constant is a function application with 0 arguments. 776 For quantifier free problems, all expressions are 777 function applications. 786 """Return the sort of expression `self`. 798 """Shorthand for `self.sort().kind()`. 800 >>> a = Array('a', IntSort(), IntSort()) 801 >>> a.sort_kind() == Z3_ARRAY_SORT 803 >>> a.sort_kind() == Z3_INT_SORT 806 return self.
sort().kind()
809 """Return a Z3 expression that represents the constraint `self == other`. 811 If `other` is `None`, then this method simply returns `False`. 822 a, b = _coerce_exprs(self, other)
827 return AstRef.__hash__(self)
830 """Return a Z3 expression that represents the constraint `self != other`. 832 If `other` is `None`, then this method simply returns `True`. 843 a, b = _coerce_exprs(self, other)
844 _args, sz = _to_ast_array((a, b))
848 """Return the Z3 function declaration associated with a Z3 application. 850 >>> f = Function('f', IntSort(), IntSort()) 859 _z3_assert(
is_app(self),
"Z3 application expected")
863 """Return the number of arguments of a Z3 application. 867 >>> (a + b).num_args() 869 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 875 _z3_assert(
is_app(self),
"Z3 application expected")
876 return int(Z3_get_app_num_args(self.
ctx_ref(), self.
as_ast()))
879 """Return argument `idx` of the application `self`. 881 This method assumes that `self` is a function application with at least `idx+1` arguments. 885 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 895 _z3_assert(
is_app(self),
"Z3 application expected")
896 _z3_assert(idx < self.
num_args(),
"Invalid argument index")
897 return _to_expr_ref(Z3_get_app_arg(self.
ctx_ref(), self.
as_ast(), idx), self.
ctx)
900 """Return a list containing the children of the given expression 904 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 910 return [self.
arg(i)
for i
in range(self.
num_args())]
914 def _to_expr_ref(a, ctx):
915 if isinstance(a, Pattern):
918 k = Z3_get_ast_kind(ctx_ref, a)
919 if k == Z3_QUANTIFIER_AST:
921 sk = Z3_get_sort_kind(ctx_ref, Z3_get_sort(ctx_ref, a))
922 if sk == Z3_BOOL_SORT:
924 if sk == Z3_INT_SORT:
925 if k == Z3_NUMERAL_AST:
928 if sk == Z3_REAL_SORT:
929 if k == Z3_NUMERAL_AST:
931 if _is_algebraic(ctx, a):
935 if k == Z3_NUMERAL_AST:
939 if sk == Z3_ARRAY_SORT:
941 if sk == Z3_DATATYPE_SORT:
943 if sk == Z3_FLOATING_POINT_SORT:
944 if k == Z3_APP_AST
and _is_numeral(ctx, a):
948 if sk == Z3_FINITE_DOMAIN_SORT:
949 if k == Z3_NUMERAL_AST:
953 if sk == Z3_ROUNDING_MODE_SORT:
955 if sk == Z3_SEQ_SORT:
961 def _coerce_expr_merge(s, a):
974 _z3_assert(s1.ctx == s.ctx,
"context mismatch")
975 _z3_assert(
False,
"sort mismatch")
979 def _coerce_exprs(a, b, ctx=None):
984 s = _coerce_expr_merge(s, a)
985 s = _coerce_expr_merge(s, b)
990 def _reduce(f, l, a):
996 def _coerce_expr_list(alist, ctx=None):
1003 alist = [ _py2expr(a, ctx)
for a
in alist ]
1004 s = _reduce(_coerce_expr_merge, alist,
None)
1005 return [ s.cast(a)
for a
in alist ]
1008 """Return `True` if `a` is a Z3 expression. 1015 >>> is_expr(IntSort()) 1019 >>> is_expr(IntVal(1)) 1022 >>> is_expr(ForAll(x, x >= 0)) 1024 >>> is_expr(FPVal(1.0)) 1027 return isinstance(a, ExprRef)
1030 """Return `True` if `a` is a Z3 function application. 1032 Note that, constants are function applications with 0 arguments. 1039 >>> is_app(IntSort()) 1043 >>> is_app(IntVal(1)) 1046 >>> is_app(ForAll(x, x >= 0)) 1049 if not isinstance(a, ExprRef):
1051 k = _ast_kind(a.ctx, a)
1052 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
1055 """Return `True` if `a` is Z3 constant/variable expression. 1064 >>> is_const(IntVal(1)) 1067 >>> is_const(ForAll(x, x >= 0)) 1070 return is_app(a)
and a.num_args() == 0
1073 """Return `True` if `a` is variable. 1075 Z3 uses de-Bruijn indices for representing bound variables in 1083 >>> f = Function('f', IntSort(), IntSort()) 1084 >>> # Z3 replaces x with bound variables when ForAll is executed. 1085 >>> q = ForAll(x, f(x) == x) 1091 >>> is_var(b.arg(1)) 1094 return is_expr(a)
and _ast_kind(a.ctx, a) == Z3_VAR_AST
1097 """Return the de-Bruijn index of the Z3 bounded variable `a`. 1105 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1106 >>> # Z3 replaces x and y with bound variables when ForAll is executed. 1107 >>> q = ForAll([x, y], f(x, y) == x + y) 1109 f(Var(1), Var(0)) == Var(1) + Var(0) 1113 >>> v1 = b.arg(0).arg(0) 1114 >>> v2 = b.arg(0).arg(1) 1119 >>> get_var_index(v1) 1121 >>> get_var_index(v2) 1125 _z3_assert(
is_var(a),
"Z3 bound variable expected")
1129 """Return `True` if `a` is an application of the given kind `k`. 1133 >>> is_app_of(n, Z3_OP_ADD) 1135 >>> is_app_of(n, Z3_OP_MUL) 1138 return is_app(a)
and a.decl().kind() == k
1140 def If(a, b, c, ctx=None):
1141 """Create a Z3 if-then-else expression. 1145 >>> max = If(x > y, x, y) 1151 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1152 return Cond(a, b, c, ctx)
1154 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1157 b, c = _coerce_exprs(b, c, ctx)
1159 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1160 return _to_expr_ref(
Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
1163 """Create a Z3 distinct expression. 1170 >>> Distinct(x, y, z) 1172 >>> simplify(Distinct(x, y, z)) 1174 >>> simplify(Distinct(x, y, z), blast_distinct=True) 1175 And(Not(x == y), Not(x == z), Not(y == z)) 1177 args = _get_args(args)
1178 ctx = _ctx_from_ast_arg_list(args)
1180 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1181 args = _coerce_expr_list(args, ctx)
1182 _args, sz = _to_ast_array(args)
1185 def _mk_bin(f, a, b):
1188 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1189 args[0] = a.as_ast()
1190 args[1] = b.as_ast()
1191 return f(a.ctx.ref(), 2, args)
1194 """Create a constant of the given sort. 1196 >>> Const('x', IntSort()) 1200 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
1205 """Create a several constants of the given sort. 1207 `names` is a string containing the names of all constants to be created. 1208 Blank spaces separate the names of different constants. 1210 >>> x, y, z = Consts('x y z', IntSort()) 1214 if isinstance(names, str):
1215 names = names.split(
" ")
1216 return [
Const(name, sort)
for name
in names]
1219 """Create a Z3 free variable. Free variables are used to create quantified formulas. 1221 >>> Var(0, IntSort()) 1223 >>> eq(Var(0, IntSort()), Var(0, BoolSort())) 1227 _z3_assert(
is_sort(s),
"Z3 sort expected")
1228 return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
1232 Create a real free variable. Free variables are used to create quantified formulas. 1233 They are also used to create polynomials. 1242 Create a list of Real free variables. 1243 The variables have ids: 0, 1, ..., n-1 1245 >>> x0, x1, x2, x3 = RealVarVector(4) 1249 return [
RealVar(i, ctx)
for i
in range(n) ]
1260 """Try to cast `val` as a Boolean. 1262 >>> x = BoolSort().cast(True) 1272 if isinstance(val, bool):
1275 _z3_assert(
is_expr(val),
"True, False or Z3 Boolean expression expected")
1276 _z3_assert(self.
eq(val.sort()),
"Value cannot be converted into a Z3 Boolean value")
1280 return isinstance(other, ArithSortRef)
1290 """All Boolean expressions are instances of this class.""" 1298 """Create the Z3 expression `self * other`. 1304 return If(self, other, 0)
1308 """Return `True` if `a` is a Z3 Boolean expression. 1314 >>> is_bool(And(p, q)) 1322 return isinstance(a, BoolRef)
1325 """Return `True` if `a` is the Z3 true expression. 1330 >>> is_true(simplify(p == p)) 1335 >>> # True is a Python Boolean expression 1342 """Return `True` if `a` is the Z3 false expression. 1349 >>> is_false(BoolVal(False)) 1355 """Return `True` if `a` is a Z3 and expression. 1357 >>> p, q = Bools('p q') 1358 >>> is_and(And(p, q)) 1360 >>> is_and(Or(p, q)) 1366 """Return `True` if `a` is a Z3 or expression. 1368 >>> p, q = Bools('p q') 1371 >>> is_or(And(p, q)) 1377 """Return `True` if `a` is a Z3 not expression. 1388 """Return `True` if `a` is a Z3 equality expression. 1390 >>> x, y = Ints('x y') 1397 """Return `True` if `a` is a Z3 distinct expression. 1399 >>> x, y, z = Ints('x y z') 1400 >>> is_distinct(x == y) 1402 >>> is_distinct(Distinct(x, y, z)) 1408 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. 1412 >>> p = Const('p', BoolSort()) 1415 >>> r = Function('r', IntSort(), IntSort(), BoolSort()) 1418 >>> is_bool(r(0, 1)) 1425 """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used. 1429 >>> is_true(BoolVal(True)) 1433 >>> is_false(BoolVal(False)) 1443 """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used. 1454 """Return a tuple of Boolean constants. 1456 `names` is a single string containing all names separated by blank spaces. 1457 If `ctx=None`, then the global context is used. 1459 >>> p, q, r = Bools('p q r') 1460 >>> And(p, Or(q, r)) 1464 if isinstance(names, str):
1465 names = names.split(
" ")
1466 return [
Bool(name, ctx)
for name
in names]
1469 """Return a list of Boolean constants of size `sz`. 1471 The constants are named using the given prefix. 1472 If `ctx=None`, then the global context is used. 1474 >>> P = BoolVector('p', 3) 1478 And(p__0, p__1, p__2) 1480 return [
Bool(
'%s__%s' % (prefix, i))
for i
in range(sz) ]
1483 """Return a fresh Boolean constant in the given context using the given prefix. 1485 If `ctx=None`, then the global context is used. 1487 >>> b1 = FreshBool() 1488 >>> b2 = FreshBool() 1496 """Create a Z3 implies expression. 1498 >>> p, q = Bools('p q') 1501 >>> simplify(Implies(p, q)) 1504 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1511 """Create a Z3 Xor expression. 1513 >>> p, q = Bools('p q') 1516 >>> simplify(Xor(p, q)) 1519 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1526 """Create a Z3 not expression or probe. 1531 >>> simplify(Not(Not(p))) 1534 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1543 def _has_probe(args):
1544 """Return `True` if one of the elements of the given collection is a Z3 probe.""" 1551 """Create a Z3 and-expression or and-probe. 1553 >>> p, q, r = Bools('p q r') 1556 >>> P = BoolVector('p', 5) 1558 And(p__0, p__1, p__2, p__3, p__4) 1562 last_arg = args[len(args)-1]
1563 if isinstance(last_arg, Context):
1564 ctx = args[len(args)-1]
1565 args = args[:len(args)-1]
1566 elif len(args) == 1
and isinstance(args[0], AstVector):
1568 args = [a
for a
in args[0]]
1571 args = _get_args(args)
1572 ctx_args = _ctx_from_ast_arg_list(args, ctx)
1574 _z3_assert(ctx_args
is None or ctx_args == ctx,
"context mismatch")
1575 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1576 if _has_probe(args):
1577 return _probe_and(args, ctx)
1579 args = _coerce_expr_list(args, ctx)
1580 _args, sz = _to_ast_array(args)
1584 """Create a Z3 or-expression or or-probe. 1586 >>> p, q, r = Bools('p q r') 1589 >>> P = BoolVector('p', 5) 1591 Or(p__0, p__1, p__2, p__3, p__4) 1595 last_arg = args[len(args)-1]
1596 if isinstance(last_arg, Context):
1597 ctx = args[len(args)-1]
1598 args = args[:len(args)-1]
1601 args = _get_args(args)
1602 ctx_args = _ctx_from_ast_arg_list(args, ctx)
1604 _z3_assert(ctx_args
is None or ctx_args == ctx,
"context mismatch")
1605 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1606 if _has_probe(args):
1607 return _probe_or(args, ctx)
1609 args = _coerce_expr_list(args, ctx)
1610 _args, sz = _to_ast_array(args)
1620 """Patterns are hints for quantifier instantiation. 1622 See http://rise4fun.com/Z3Py/tutorial/advanced for more details. 1631 """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. 1633 See http://rise4fun.com/Z3Py/tutorial/advanced for more details. 1635 >>> f = Function('f', IntSort(), IntSort()) 1637 >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ]) 1639 ForAll(x, f(x) == 0) 1640 >>> q.num_patterns() 1642 >>> is_pattern(q.pattern(0)) 1647 return isinstance(a, PatternRef)
1650 """Create a Z3 multi-pattern using the given expressions `*args` 1652 See http://rise4fun.com/Z3Py/tutorial/advanced for more details. 1654 >>> f = Function('f', IntSort(), IntSort()) 1655 >>> g = Function('g', IntSort(), IntSort()) 1657 >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ]) 1659 ForAll(x, f(x) != g(x)) 1660 >>> q.num_patterns() 1662 >>> is_pattern(q.pattern(0)) 1665 MultiPattern(f(Var(0)), g(Var(0))) 1668 _z3_assert(len(args) > 0,
"At least one argument expected")
1669 _z3_assert(all([
is_expr(a)
for a
in args ]),
"Z3 expressions expected")
1671 args, sz = _to_ast_array(args)
1672 return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
1674 def _to_pattern(arg):
1687 """Universally and Existentially quantified formulas.""" 1696 """Return the Boolean sort.""" 1700 """Return `True` if `self` is a universal quantifier. 1702 >>> f = Function('f', IntSort(), IntSort()) 1704 >>> q = ForAll(x, f(x) == 0) 1707 >>> q = Exists(x, f(x) != 0) 1714 """Return the weight annotation of `self`. 1716 >>> f = Function('f', IntSort(), IntSort()) 1718 >>> q = ForAll(x, f(x) == 0) 1721 >>> q = ForAll(x, f(x) == 0, weight=10) 1728 """Return the number of patterns (i.e., quantifier instantiation hints) in `self`. 1730 >>> f = Function('f', IntSort(), IntSort()) 1731 >>> g = Function('g', IntSort(), IntSort()) 1733 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ]) 1734 >>> q.num_patterns() 1740 """Return a pattern (i.e., quantifier instantiation hints) in `self`. 1742 >>> f = Function('f', IntSort(), IntSort()) 1743 >>> g = Function('g', IntSort(), IntSort()) 1745 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ]) 1746 >>> q.num_patterns() 1754 _z3_assert(idx < self.
num_patterns(),
"Invalid pattern idx")
1758 """Return the number of no-patterns.""" 1762 """Return a no-pattern.""" 1768 """Return the expression being quantified. 1770 >>> f = Function('f', IntSort(), IntSort()) 1772 >>> q = ForAll(x, f(x) == 0) 1779 """Return the number of variables bounded by this quantifier. 1781 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1784 >>> q = ForAll([x, y], f(x, y) >= x) 1791 """Return a string representing a name used when displaying the quantifier. 1793 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1796 >>> q = ForAll([x, y], f(x, y) >= x) 1803 _z3_assert(idx < self.
num_vars(),
"Invalid variable idx")
1807 """Return the sort of a bound variable. 1809 >>> f = Function('f', IntSort(), RealSort(), IntSort()) 1812 >>> q = ForAll([x, y], f(x, y) >= x) 1819 _z3_assert(idx < self.
num_vars(),
"Invalid variable idx")
1823 """Return a list containing a single element self.body() 1825 >>> f = Function('f', IntSort(), IntSort()) 1827 >>> q = ForAll(x, f(x) == 0) 1831 return [ self.
body() ]
1834 """Return `True` if `a` is a Z3 quantifier. 1836 >>> f = Function('f', IntSort(), IntSort()) 1838 >>> q = ForAll(x, f(x) == 0) 1839 >>> is_quantifier(q) 1841 >>> is_quantifier(f(x)) 1844 return isinstance(a, QuantifierRef)
1846 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1848 _z3_assert(
is_bool(body),
"Z3 expression expected")
1849 _z3_assert(
is_const(vs)
or (len(vs) > 0
and all([
is_const(v)
for v
in vs])),
"Invalid bounded variable(s)")
1850 _z3_assert(all([
is_pattern(a)
or is_expr(a)
for a
in patterns]),
"Z3 patterns expected")
1851 _z3_assert(all([
is_expr(p)
for p
in no_patterns]),
"no patterns are Z3 expressions")
1858 _vs = (Ast * num_vars)()
1859 for i
in range(num_vars):
1861 _vs[i] = vs[i].as_ast()
1862 patterns = [ _to_pattern(p)
for p
in patterns ]
1863 num_pats = len(patterns)
1864 _pats = (Pattern * num_pats)()
1865 for i
in range(num_pats):
1866 _pats[i] = patterns[i].ast
1867 _no_pats, num_no_pats = _to_ast_array(no_patterns)
1870 return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid,
1873 num_no_pats, _no_pats,
1874 body.as_ast()), ctx)
1876 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1877 """Create a Z3 forall formula. 1879 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. 1881 See http://rise4fun.com/Z3Py/tutorial/advanced for more details. 1883 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1886 >>> ForAll([x, y], f(x, y) >= x) 1887 ForAll([x, y], f(x, y) >= x) 1888 >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ]) 1889 ForAll([x, y], f(x, y) >= x) 1890 >>> ForAll([x, y], f(x, y) >= x, weight=10) 1891 ForAll([x, y], f(x, y) >= x) 1893 return _mk_quantifier(
True, vs, body, weight, qid, skid, patterns, no_patterns)
1895 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
1896 """Create a Z3 exists formula. 1898 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. 1900 See http://rise4fun.com/Z3Py/tutorial/advanced for more details. 1902 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1905 >>> q = Exists([x, y], f(x, y) >= x, skid="foo") 1907 Exists([x, y], f(x, y) >= x) 1908 >>> is_quantifier(q) 1910 >>> r = Tactic('nnf')(q).as_expr() 1911 >>> is_quantifier(r) 1914 return _mk_quantifier(
False, vs, body, weight, qid, skid, patterns, no_patterns)
1923 """Real and Integer sorts.""" 1926 """Return `True` if `self` is of the sort Real. 1931 >>> (x + 1).is_real() 1937 return self.
kind() == Z3_REAL_SORT
1940 """Return `True` if `self` is of the sort Integer. 1945 >>> (x + 1).is_int() 1951 return self.
kind() == Z3_INT_SORT
1954 """Return `True` if `self` is a subsort of `other`.""" 1958 """Try to cast `val` as an Integer or Real. 1960 >>> IntSort().cast(10) 1962 >>> is_int(IntSort().cast(10)) 1966 >>> RealSort().cast(10) 1968 >>> is_real(RealSort().cast(10)) 1973 _z3_assert(self.
ctx == val.ctx,
"Context mismatch")
1977 if val_s.is_int()
and self.
is_real():
1979 if val_s.is_bool()
and self.
is_int():
1980 return If(val, 1, 0)
1981 if val_s.is_bool()
and self.
is_real():
1984 _z3_assert(
False,
"Z3 Integer/Real expression expected" )
1991 _z3_assert(
False,
"int, long, float, string (numeral), or Z3 Integer/Real expression expected")
1994 """Return `True` if s is an arithmetical sort (type). 1996 >>> is_arith_sort(IntSort()) 1998 >>> is_arith_sort(RealSort()) 2000 >>> is_arith_sort(BoolSort()) 2002 >>> n = Int('x') + 1 2003 >>> is_arith_sort(n.sort()) 2006 return isinstance(s, ArithSortRef)
2009 """Integer and Real expressions.""" 2012 """Return the sort (type) of the arithmetical expression `self`. 2016 >>> (Real('x') + 1).sort() 2022 """Return `True` if `self` is an integer expression. 2027 >>> (x + 1).is_int() 2030 >>> (x + y).is_int() 2036 """Return `True` if `self` is an real expression. 2041 >>> (x + 1).is_real() 2047 """Create the Z3 expression `self + other`. 2056 a, b = _coerce_exprs(self, other)
2057 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.
ctx)
2060 """Create the Z3 expression `other + self`. 2066 a, b = _coerce_exprs(self, other)
2067 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.
ctx)
2070 """Create the Z3 expression `self * other`. 2079 a, b = _coerce_exprs(self, other)
2080 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.
ctx)
2083 """Create the Z3 expression `other * self`. 2089 a, b = _coerce_exprs(self, other)
2090 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.
ctx)
2093 """Create the Z3 expression `self - other`. 2102 a, b = _coerce_exprs(self, other)
2103 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.
ctx)
2106 """Create the Z3 expression `other - self`. 2112 a, b = _coerce_exprs(self, other)
2113 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.
ctx)
2116 """Create the Z3 expression `self**other` (** is the power operator). 2123 >>> simplify(IntVal(2)**8) 2126 a, b = _coerce_exprs(self, other)
2130 """Create the Z3 expression `other**self` (** is the power operator). 2137 >>> simplify(2**IntVal(8)) 2140 a, b = _coerce_exprs(self, other)
2144 """Create the Z3 expression `other/self`. 2163 a, b = _coerce_exprs(self, other)
2167 """Create the Z3 expression `other/self`.""" 2171 """Create the Z3 expression `other/self`. 2184 a, b = _coerce_exprs(self, other)
2188 """Create the Z3 expression `other/self`.""" 2192 """Create the Z3 expression `other%self`. 2198 >>> simplify(IntVal(10) % IntVal(3)) 2201 a, b = _coerce_exprs(self, other)
2203 _z3_assert(a.is_int(),
"Z3 integer expression expected")
2207 """Create the Z3 expression `other%self`. 2213 a, b = _coerce_exprs(self, other)
2215 _z3_assert(a.is_int(),
"Z3 integer expression expected")
2219 """Return an expression representing `-self`. 2239 """Create the Z3 expression `other <= self`. 2241 >>> x, y = Ints('x y') 2248 a, b = _coerce_exprs(self, other)
2252 """Create the Z3 expression `other < self`. 2254 >>> x, y = Ints('x y') 2261 a, b = _coerce_exprs(self, other)
2265 """Create the Z3 expression `other > self`. 2267 >>> x, y = Ints('x y') 2274 a, b = _coerce_exprs(self, other)
2278 """Create the Z3 expression `other >= self`. 2280 >>> x, y = Ints('x y') 2287 a, b = _coerce_exprs(self, other)
2291 """Return `True` if `a` is an arithmetical expression. 2300 >>> is_arith(IntVal(1)) 2308 return isinstance(a, ArithRef)
2311 """Return `True` if `a` is an integer expression. 2318 >>> is_int(IntVal(1)) 2329 """Return `True` if `a` is a real expression. 2341 >>> is_real(RealVal(1)) 2346 def _is_numeral(ctx, a):
2347 return Z3_is_numeral_ast(ctx.ref(), a)
2349 def _is_algebraic(ctx, a):
2350 return Z3_is_algebraic_number(ctx.ref(), a)
2353 """Return `True` if `a` is an integer value of sort Int. 2355 >>> is_int_value(IntVal(1)) 2359 >>> is_int_value(Int('x')) 2361 >>> n = Int('x') + 1 2366 >>> is_int_value(n.arg(1)) 2368 >>> is_int_value(RealVal("1/3")) 2370 >>> is_int_value(RealVal(1)) 2373 return is_arith(a)
and a.is_int()
and _is_numeral(a.ctx, a.as_ast())
2376 """Return `True` if `a` is rational value of sort Real. 2378 >>> is_rational_value(RealVal(1)) 2380 >>> is_rational_value(RealVal("3/5")) 2382 >>> is_rational_value(IntVal(1)) 2384 >>> is_rational_value(1) 2386 >>> n = Real('x') + 1 2389 >>> is_rational_value(n.arg(1)) 2391 >>> is_rational_value(Real('x')) 2394 return is_arith(a)
and a.is_real()
and _is_numeral(a.ctx, a.as_ast())
2397 """Return `True` if `a` is an algerbraic value of sort Real. 2399 >>> is_algebraic_value(RealVal("3/5")) 2401 >>> n = simplify(Sqrt(2)) 2404 >>> is_algebraic_value(n) 2407 return is_arith(a)
and a.is_real()
and _is_algebraic(a.ctx, a.as_ast())
2410 """Return `True` if `a` is an expression of the form b + c. 2412 >>> x, y = Ints('x y') 2421 """Return `True` if `a` is an expression of the form b * c. 2423 >>> x, y = Ints('x y') 2432 """Return `True` if `a` is an expression of the form b - c. 2434 >>> x, y = Ints('x y') 2443 """Return `True` if `a` is an expression of the form b / c. 2445 >>> x, y = Reals('x y') 2450 >>> x, y = Ints('x y') 2459 """Return `True` if `a` is an expression of the form b div c. 2461 >>> x, y = Ints('x y') 2470 """Return `True` if `a` is an expression of the form b % c. 2472 >>> x, y = Ints('x y') 2481 """Return `True` if `a` is an expression of the form b <= c. 2483 >>> x, y = Ints('x y') 2492 """Return `True` if `a` is an expression of the form b < c. 2494 >>> x, y = Ints('x y') 2503 """Return `True` if `a` is an expression of the form b >= c. 2505 >>> x, y = Ints('x y') 2514 """Return `True` if `a` is an expression of the form b > c. 2516 >>> x, y = Ints('x y') 2525 """Return `True` if `a` is an expression of the form IsInt(b). 2528 >>> is_is_int(IsInt(x)) 2536 """Return `True` if `a` is an expression of the form ToReal(b). 2550 """Return `True` if `a` is an expression of the form ToInt(b). 2564 """Integer values.""" 2567 """Return a Z3 integer numeral as a Python long (bignum) numeral. 2576 _z3_assert(self.
is_int(),
"Integer value expected")
2580 """Return a Z3 integer numeral as a Python string. 2588 """Rational values.""" 2591 """ Return the numerator of a Z3 rational numeral. 2593 >>> is_rational_value(RealVal("3/5")) 2595 >>> n = RealVal("3/5") 2598 >>> is_rational_value(Q(3,5)) 2600 >>> Q(3,5).numerator() 2606 """ Return the denominator of a Z3 rational numeral. 2608 >>> is_rational_value(Q(3,5)) 2617 """ Return the numerator as a Python long. 2619 >>> v = RealVal(10000000000) 2624 >>> v.numerator_as_long() + 1 == 10000000001 2630 """ Return the denominator as a Python long. 2632 >>> v = RealVal("1/3") 2635 >>> v.denominator_as_long() 2641 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places. 2643 >>> v = RealVal("1/5") 2646 >>> v = RealVal("1/3") 2653 """Return a Z3 rational numeral as a Python string. 2662 """Return a Z3 rational as a Python Fraction object. 2664 >>> v = RealVal("1/5") 2671 """Algebraic irrational values.""" 2674 """Return a Z3 rational number that approximates the algebraic number `self`. 2675 The result `r` is such that |r - self| <= 1/10^precision 2677 >>> x = simplify(Sqrt(2)) 2679 6838717160008073720548335/4835703278458516698824704 2685 """Return a string representation of the algebraic number `self` in decimal notation using `prec` decimal places 2687 >>> x = simplify(Sqrt(2)) 2688 >>> x.as_decimal(10) 2690 >>> x.as_decimal(20) 2691 '1.41421356237309504880?' 2695 def _py2expr(a, ctx=None):
2696 if isinstance(a, bool):
2700 if isinstance(a, float):
2703 _z3_assert(
False,
"Python bool, int, long or float expected")
2706 """Return the integer sort in the given context. If `ctx=None`, then the global context is used. 2710 >>> x = Const('x', IntSort()) 2713 >>> x.sort() == IntSort() 2715 >>> x.sort() == BoolSort() 2722 """Return the real sort in the given context. If `ctx=None`, then the global context is used. 2726 >>> x = Const('x', RealSort()) 2731 >>> x.sort() == RealSort() 2737 def _to_int_str(val):
2738 if isinstance(val, float):
2739 return str(int(val))
2740 elif isinstance(val, bool):
2747 elif isinstance(val, str):
2750 _z3_assert(
False,
"Python value cannot be used as a Z3 integer")
2753 """Return a Z3 integer value. If `ctx=None`, then the global context is used. 2761 return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val),
IntSort(ctx).ast), ctx)
2764 """Return a Z3 real value. 2766 `val` may be a Python int, long, float or string representing a number in decimal or rational notation. 2767 If `ctx=None`, then the global context is used. 2771 >>> RealVal(1).sort() 2782 """Return a Z3 rational a/b. 2784 If `ctx=None`, then the global context is used. 2788 >>> RatVal(3,5).sort() 2792 _z3_assert(_is_int(a)
or isinstance(a, str),
"First argument cannot be converted into an integer")
2793 _z3_assert(_is_int(b)
or isinstance(b, str),
"Second argument cannot be converted into an integer")
2796 def Q(a, b, ctx=None):
2797 """Return a Z3 rational a/b. 2799 If `ctx=None`, then the global context is used. 2809 """Return an integer constant named `name`. If `ctx=None`, then the global context is used. 2821 """Return a tuple of Integer constants. 2823 >>> x, y, z = Ints('x y z') 2828 if isinstance(names, str):
2829 names = names.split(
" ")
2830 return [
Int(name, ctx)
for name
in names]
2833 """Return a list of integer constants of size `sz`. 2835 >>> X = IntVector('x', 3) 2841 return [
Int(
'%s__%s' % (prefix, i))
for i
in range(sz) ]
2844 """Return a fresh integer constant in the given context using the given prefix. 2857 """Return a real constant named `name`. If `ctx=None`, then the global context is used. 2869 """Return a tuple of real constants. 2871 >>> x, y, z = Reals('x y z') 2874 >>> Sum(x, y, z).sort() 2878 if isinstance(names, str):
2879 names = names.split(
" ")
2880 return [
Real(name, ctx)
for name
in names]
2883 """Return a list of real constants of size `sz`. 2885 >>> X = RealVector('x', 3) 2893 return [
Real(
'%s__%s' % (prefix, i))
for i
in range(sz) ]
2896 """Return a fresh real constant in the given context using the given prefix. 2909 """ Return the Z3 expression ToReal(a). 2921 _z3_assert(a.is_int(),
"Z3 integer expression expected.")
2926 """ Return the Z3 expression ToInt(a). 2938 _z3_assert(a.is_real(),
"Z3 real expression expected.")
2943 """ Return the Z3 predicate IsInt(a). 2946 >>> IsInt(x + "1/2") 2948 >>> solve(IsInt(x + "1/2"), x > 0, x < 1) 2950 >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2") 2954 _z3_assert(a.is_real(),
"Z3 real expression expected.")
2959 """ Return a Z3 expression which represents the square root of a. 2971 """ Return a Z3 expression which represents the cubic root of a. 2989 """Bit-vector sort.""" 2992 """Return the size (number of bits) of the bit-vector sort `self`. 2994 >>> b = BitVecSort(32) 2998 return int(Z3_get_bv_sort_size(self.
ctx_ref(), self.
ast))
3004 """Try to cast `val` as a Bit-Vector. 3006 >>> b = BitVecSort(32) 3009 >>> b.cast(10).sexpr() 3014 _z3_assert(self.
ctx == val.ctx,
"Context mismatch")
3021 """Return True if `s` is a Z3 bit-vector sort. 3023 >>> is_bv_sort(BitVecSort(32)) 3025 >>> is_bv_sort(IntSort()) 3028 return isinstance(s, BitVecSortRef)
3031 """Bit-vector expressions.""" 3034 """Return the sort of the bit-vector expression `self`. 3036 >>> x = BitVec('x', 32) 3039 >>> x.sort() == BitVecSort(32) 3045 """Return the number of bits of the bit-vector expression `self`. 3047 >>> x = BitVec('x', 32) 3050 >>> Concat(x, x).size() 3056 """Create the Z3 expression `self + other`. 3058 >>> x = BitVec('x', 32) 3059 >>> y = BitVec('y', 32) 3065 a, b = _coerce_exprs(self, other)
3069 """Create the Z3 expression `other + self`. 3071 >>> x = BitVec('x', 32) 3075 a, b = _coerce_exprs(self, other)
3079 """Create the Z3 expression `self * other`. 3081 >>> x = BitVec('x', 32) 3082 >>> y = BitVec('y', 32) 3088 a, b = _coerce_exprs(self, other)
3092 """Create the Z3 expression `other * self`. 3094 >>> x = BitVec('x', 32) 3098 a, b = _coerce_exprs(self, other)
3102 """Create the Z3 expression `self - other`. 3104 >>> x = BitVec('x', 32) 3105 >>> y = BitVec('y', 32) 3111 a, b = _coerce_exprs(self, other)
3115 """Create the Z3 expression `other - self`. 3117 >>> x = BitVec('x', 32) 3121 a, b = _coerce_exprs(self, other)
3125 """Create the Z3 expression bitwise-or `self | other`. 3127 >>> x = BitVec('x', 32) 3128 >>> y = BitVec('y', 32) 3134 a, b = _coerce_exprs(self, other)
3138 """Create the Z3 expression bitwise-or `other | self`. 3140 >>> x = BitVec('x', 32) 3144 a, b = _coerce_exprs(self, other)
3148 """Create the Z3 expression bitwise-and `self & other`. 3150 >>> x = BitVec('x', 32) 3151 >>> y = BitVec('y', 32) 3157 a, b = _coerce_exprs(self, other)
3161 """Create the Z3 expression bitwise-or `other & self`. 3163 >>> x = BitVec('x', 32) 3167 a, b = _coerce_exprs(self, other)
3171 """Create the Z3 expression bitwise-xor `self ^ other`. 3173 >>> x = BitVec('x', 32) 3174 >>> y = BitVec('y', 32) 3180 a, b = _coerce_exprs(self, other)
3184 """Create the Z3 expression bitwise-xor `other ^ self`. 3186 >>> x = BitVec('x', 32) 3190 a, b = _coerce_exprs(self, other)
3196 >>> x = BitVec('x', 32) 3203 """Return an expression representing `-self`. 3205 >>> x = BitVec('x', 32) 3214 """Create the Z3 expression bitwise-not `~self`. 3216 >>> x = BitVec('x', 32) 3225 """Create the Z3 expression (signed) division `self / other`. 3227 Use the function UDiv() for unsigned division. 3229 >>> x = BitVec('x', 32) 3230 >>> y = BitVec('y', 32) 3237 >>> UDiv(x, y).sexpr() 3240 a, b = _coerce_exprs(self, other)
3244 """Create the Z3 expression (signed) division `self / other`.""" 3248 """Create the Z3 expression (signed) division `other / self`. 3250 Use the function UDiv() for unsigned division. 3252 >>> x = BitVec('x', 32) 3255 >>> (10 / x).sexpr() 3256 '(bvsdiv #x0000000a x)' 3257 >>> UDiv(10, x).sexpr() 3258 '(bvudiv #x0000000a x)' 3260 a, b = _coerce_exprs(self, other)
3264 """Create the Z3 expression (signed) division `other / self`.""" 3268 """Create the Z3 expression (signed) mod `self % other`. 3270 Use the function URem() for unsigned remainder, and SRem() for signed remainder. 3272 >>> x = BitVec('x', 32) 3273 >>> y = BitVec('y', 32) 3280 >>> URem(x, y).sexpr() 3282 >>> SRem(x, y).sexpr() 3285 a, b = _coerce_exprs(self, other)
3289 """Create the Z3 expression (signed) mod `other % self`. 3291 Use the function URem() for unsigned remainder, and SRem() for signed remainder. 3293 >>> x = BitVec('x', 32) 3296 >>> (10 % x).sexpr() 3297 '(bvsmod #x0000000a x)' 3298 >>> URem(10, x).sexpr() 3299 '(bvurem #x0000000a x)' 3300 >>> SRem(10, x).sexpr() 3301 '(bvsrem #x0000000a x)' 3303 a, b = _coerce_exprs(self, other)
3307 """Create the Z3 expression (signed) `other <= self`. 3309 Use the function ULE() for unsigned less than or equal to. 3311 >>> x, y = BitVecs('x y', 32) 3314 >>> (x <= y).sexpr() 3316 >>> ULE(x, y).sexpr() 3319 a, b = _coerce_exprs(self, other)
3323 """Create the Z3 expression (signed) `other < self`. 3325 Use the function ULT() for unsigned less than. 3327 >>> x, y = BitVecs('x y', 32) 3332 >>> ULT(x, y).sexpr() 3335 a, b = _coerce_exprs(self, other)
3339 """Create the Z3 expression (signed) `other > self`. 3341 Use the function UGT() for unsigned greater than. 3343 >>> x, y = BitVecs('x y', 32) 3348 >>> UGT(x, y).sexpr() 3351 a, b = _coerce_exprs(self, other)
3355 """Create the Z3 expression (signed) `other >= self`. 3357 Use the function UGE() for unsigned greater than or equal to. 3359 >>> x, y = BitVecs('x y', 32) 3362 >>> (x >= y).sexpr() 3364 >>> UGE(x, y).sexpr() 3367 a, b = _coerce_exprs(self, other)
3371 """Create the Z3 expression (arithmetical) right shift `self >> other` 3373 Use the function LShR() for the right logical shift 3375 >>> x, y = BitVecs('x y', 32) 3378 >>> (x >> y).sexpr() 3380 >>> LShR(x, y).sexpr() 3384 >>> BitVecVal(4, 3).as_signed_long() 3386 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() 3388 >>> simplify(BitVecVal(4, 3) >> 1) 3390 >>> simplify(LShR(BitVecVal(4, 3), 1)) 3392 >>> simplify(BitVecVal(2, 3) >> 1) 3394 >>> simplify(LShR(BitVecVal(2, 3), 1)) 3397 a, b = _coerce_exprs(self, other)
3401 """Create the Z3 expression left shift `self << other` 3403 >>> x, y = BitVecs('x y', 32) 3406 >>> (x << y).sexpr() 3408 >>> simplify(BitVecVal(2, 3) << 1) 3411 a, b = _coerce_exprs(self, other)
3415 """Create the Z3 expression (arithmetical) right shift `other` >> `self`. 3417 Use the function LShR() for the right logical shift 3419 >>> x = BitVec('x', 32) 3422 >>> (10 >> x).sexpr() 3423 '(bvashr #x0000000a x)' 3425 a, b = _coerce_exprs(self, other)
3429 """Create the Z3 expression left shift `other << self`. 3431 Use the function LShR() for the right logical shift 3433 >>> x = BitVec('x', 32) 3436 >>> (10 << x).sexpr() 3437 '(bvshl #x0000000a x)' 3439 a, b = _coerce_exprs(self, other)
3443 """Bit-vector values.""" 3446 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. 3448 >>> v = BitVecVal(0xbadc0de, 32) 3451 >>> print("0x%.8x" % v.as_long()) 3457 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign. 3459 >>> BitVecVal(4, 3).as_signed_long() 3461 >>> BitVecVal(7, 3).as_signed_long() 3463 >>> BitVecVal(3, 3).as_signed_long() 3465 >>> BitVecVal(2**32 - 1, 32).as_signed_long() 3467 >>> BitVecVal(2**64 - 1, 64).as_signed_long() 3472 if val >= 2**(sz - 1):
3474 if val < -2**(sz - 1):
3482 """Return `True` if `a` is a Z3 bit-vector expression. 3484 >>> b = BitVec('b', 32) 3492 return isinstance(a, BitVecRef)
3495 """Return `True` if `a` is a Z3 bit-vector numeral value. 3497 >>> b = BitVec('b', 32) 3500 >>> b = BitVecVal(10, 32) 3506 return is_bv(a)
and _is_numeral(a.ctx, a.as_ast())
3509 """Return the Z3 expression BV2Int(a). 3511 >>> b = BitVec('b', 3) 3512 >>> BV2Int(b).sort() 3517 >>> x > BV2Int(b, is_signed=False) 3519 >>> x > BV2Int(b, is_signed=True) 3520 x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) 3521 >>> solve(x > BV2Int(b), b == 1, x < 3) 3525 _z3_assert(
is_bv(a),
"Z3 bit-vector expression expected")
3531 """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. 3533 >>> Byte = BitVecSort(8) 3534 >>> Word = BitVecSort(16) 3537 >>> x = Const('x', Byte) 3538 >>> eq(x, BitVec('x', 8)) 3545 """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used. 3547 >>> v = BitVecVal(10, 32) 3550 >>> print("0x%.8x" % v.as_long()) 3555 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
3561 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort. 3562 If `ctx=None`, then the global context is used. 3564 >>> x = BitVec('x', 16) 3571 >>> word = BitVecSort(16) 3572 >>> x2 = BitVec('x', word) 3576 if isinstance(bv, BitVecSortRef):
3584 """Return a tuple of bit-vector constants of size bv. 3586 >>> x, y, z = BitVecs('x y z', 16) 3593 >>> Product(x, y, z) 3595 >>> simplify(Product(x, y, z)) 3599 if isinstance(names, str):
3600 names = names.split(
" ")
3601 return [
BitVec(name, bv, ctx)
for name
in names]
3604 """Create a Z3 bit-vector concatenation expression. 3606 >>> v = BitVecVal(1, 4) 3607 >>> Concat(v, v+1, v) 3608 Concat(Concat(1, 1 + 1), 1) 3609 >>> simplify(Concat(v, v+1, v)) 3611 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long()) 3614 args = _get_args(args)
3617 _z3_assert(sz >= 2,
"At least two arguments expected.")
3624 if is_seq(args[0])
or isinstance(args[0], str):
3625 args = [_coerce_seq(s, ctx)
for s
in args]
3627 _z3_assert(all([
is_seq(a)
for a
in args]),
"All arguments must be sequence expressions.")
3630 v[i] = args[i].as_ast()
3631 return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
3635 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
3638 v[i] = args[i].as_ast()
3639 return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
3642 _z3_assert(all([
is_bv(a)
for a
in args]),
"All arguments must be Z3 bit-vector expressions.")
3644 for i
in range(sz - 1):
3649 """Create a Z3 bit-vector extraction expression, or create a string extraction expression. 3651 >>> x = BitVec('x', 8) 3652 >>> Extract(6, 2, x) 3654 >>> Extract(6, 2, x).sort() 3656 >>> simplify(Extract(StringVal("abcd"),2,1)) 3659 if isinstance(high, str):
3663 offset = _py2expr(low, high.ctx)
3664 length = _py2expr(a, high.ctx)
3667 _z3_assert(
is_int(offset)
and is_int(length),
"Second and third arguments must be integers")
3668 return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
3670 _z3_assert(low <= high,
"First argument must be greater than or equal to second argument")
3671 _z3_assert(_is_int(high)
and high >= 0
and _is_int(low)
and low >= 0,
"First and second arguments must be non negative integers")
3672 _z3_assert(
is_bv(a),
"Third argument must be a Z3 Bitvector expression")
3675 def _check_bv_args(a, b):
3677 _z3_assert(
is_bv(a)
or is_bv(b),
"At least one of the arguments must be a Z3 bit-vector expression")
3680 """Create the Z3 expression (unsigned) `other <= self`. 3682 Use the operator <= for signed less than or equal to. 3684 >>> x, y = BitVecs('x y', 32) 3687 >>> (x <= y).sexpr() 3689 >>> ULE(x, y).sexpr() 3692 _check_bv_args(a, b)
3693 a, b = _coerce_exprs(a, b)
3697 """Create the Z3 expression (unsigned) `other < self`. 3699 Use the operator < for signed less than. 3701 >>> x, y = BitVecs('x y', 32) 3706 >>> ULT(x, y).sexpr() 3709 _check_bv_args(a, b)
3710 a, b = _coerce_exprs(a, b)
3714 """Create the Z3 expression (unsigned) `other >= self`. 3716 Use the operator >= for signed greater than or equal to. 3718 >>> x, y = BitVecs('x y', 32) 3721 >>> (x >= y).sexpr() 3723 >>> UGE(x, y).sexpr() 3726 _check_bv_args(a, b)
3727 a, b = _coerce_exprs(a, b)
3731 """Create the Z3 expression (unsigned) `other > self`. 3733 Use the operator > for signed greater than. 3735 >>> x, y = BitVecs('x y', 32) 3740 >>> UGT(x, y).sexpr() 3743 _check_bv_args(a, b)
3744 a, b = _coerce_exprs(a, b)
3748 """Create the Z3 expression (unsigned) division `self / other`. 3750 Use the operator / for signed division. 3752 >>> x = BitVec('x', 32) 3753 >>> y = BitVec('y', 32) 3756 >>> UDiv(x, y).sort() 3760 >>> UDiv(x, y).sexpr() 3763 _check_bv_args(a, b)
3764 a, b = _coerce_exprs(a, b)
3768 """Create the Z3 expression (unsigned) remainder `self % other`. 3770 Use the operator % for signed modulus, and SRem() for signed remainder. 3772 >>> x = BitVec('x', 32) 3773 >>> y = BitVec('y', 32) 3776 >>> URem(x, y).sort() 3780 >>> URem(x, y).sexpr() 3783 _check_bv_args(a, b)
3784 a, b = _coerce_exprs(a, b)
3788 """Create the Z3 expression signed remainder. 3790 Use the operator % for signed modulus, and URem() for unsigned remainder. 3792 >>> x = BitVec('x', 32) 3793 >>> y = BitVec('y', 32) 3796 >>> SRem(x, y).sort() 3800 >>> SRem(x, y).sexpr() 3803 _check_bv_args(a, b)
3804 a, b = _coerce_exprs(a, b)
3808 """Create the Z3 expression logical right shift. 3810 Use the operator >> for the arithmetical right shift. 3812 >>> x, y = BitVecs('x y', 32) 3815 >>> (x >> y).sexpr() 3817 >>> LShR(x, y).sexpr() 3821 >>> BitVecVal(4, 3).as_signed_long() 3823 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() 3825 >>> simplify(BitVecVal(4, 3) >> 1) 3827 >>> simplify(LShR(BitVecVal(4, 3), 1)) 3829 >>> simplify(BitVecVal(2, 3) >> 1) 3831 >>> simplify(LShR(BitVecVal(2, 3), 1)) 3834 _check_bv_args(a, b)
3835 a, b = _coerce_exprs(a, b)
3839 """Return an expression representing `a` rotated to the left `b` times. 3841 >>> a, b = BitVecs('a b', 16) 3842 >>> RotateLeft(a, b) 3844 >>> simplify(RotateLeft(a, 0)) 3846 >>> simplify(RotateLeft(a, 16)) 3849 _check_bv_args(a, b)
3850 a, b = _coerce_exprs(a, b)
3854 """Return an expression representing `a` rotated to the right `b` times. 3856 >>> a, b = BitVecs('a b', 16) 3857 >>> RotateRight(a, b) 3859 >>> simplify(RotateRight(a, 0)) 3861 >>> simplify(RotateRight(a, 16)) 3864 _check_bv_args(a, b)
3865 a, b = _coerce_exprs(a, b)
3869 """Return a bit-vector expression with `n` extra sign-bits. 3871 >>> x = BitVec('x', 16) 3872 >>> n = SignExt(8, x) 3879 >>> v0 = BitVecVal(2, 2) 3884 >>> v = simplify(SignExt(6, v0)) 3889 >>> print("%.x" % v.as_long()) 3893 _z3_assert(_is_int(n),
"First argument must be an integer")
3894 _z3_assert(
is_bv(a),
"Second argument must be a Z3 Bitvector expression")
3898 """Return a bit-vector expression with `n` extra zero-bits. 3900 >>> x = BitVec('x', 16) 3901 >>> n = ZeroExt(8, x) 3908 >>> v0 = BitVecVal(2, 2) 3913 >>> v = simplify(ZeroExt(6, v0)) 3920 _z3_assert(_is_int(n),
"First argument must be an integer")
3921 _z3_assert(
is_bv(a),
"Second argument must be a Z3 Bitvector expression")
3925 """Return an expression representing `n` copies of `a`. 3927 >>> x = BitVec('x', 8) 3928 >>> n = RepeatBitVec(4, x) 3933 >>> v0 = BitVecVal(10, 4) 3934 >>> print("%.x" % v0.as_long()) 3936 >>> v = simplify(RepeatBitVec(4, v0)) 3939 >>> print("%.x" % v.as_long()) 3943 _z3_assert(_is_int(n),
"First argument must be an integer")
3944 _z3_assert(
is_bv(a),
"Second argument must be a Z3 Bitvector expression")
3948 """Return the reduction-and expression of `a`.""" 3950 _z3_assert(
is_bv(a),
"First argument must be a Z3 Bitvector expression")
3954 """Return the reduction-or expression of `a`.""" 3956 _z3_assert(
is_bv(a),
"First argument must be a Z3 Bitvector expression")
3969 """Return the domain of the array sort `self`. 3971 >>> A = ArraySort(IntSort(), BoolSort()) 3975 return _to_sort_ref(Z3_get_array_sort_domain(self.
ctx_ref(), self.
ast), self.
ctx)
3978 """Return the range of the array sort `self`. 3980 >>> A = ArraySort(IntSort(), BoolSort()) 3984 return _to_sort_ref(Z3_get_array_sort_range(self.
ctx_ref(), self.
ast), self.
ctx)
3987 """Array expressions. """ 3990 """Return the array sort of the array expression `self`. 3992 >>> a = Array('a', IntSort(), BoolSort()) 3999 """Shorthand for `self.sort().domain()`. 4001 >>> a = Array('a', IntSort(), BoolSort()) 4008 """Shorthand for `self.sort().range()`. 4010 >>> a = Array('a', IntSort(), BoolSort()) 4017 """Return the Z3 expression `self[arg]`. 4019 >>> a = Array('a', IntSort(), BoolSort()) 4026 arg = self.
domain().cast(arg)
4034 """Return `True` if `a` is a Z3 array expression. 4036 >>> a = Array('a', IntSort(), IntSort()) 4039 >>> is_array(Store(a, 0, 1)) 4044 return isinstance(a, ArrayRef)
4047 """Return `True` if `a` is a Z3 constant array. 4049 >>> a = K(IntSort(), 10) 4050 >>> is_const_array(a) 4052 >>> a = Array('a', IntSort(), IntSort()) 4053 >>> is_const_array(a) 4059 """Return `True` if `a` is a Z3 constant array. 4061 >>> a = K(IntSort(), 10) 4064 >>> a = Array('a', IntSort(), IntSort()) 4071 """Return `True` if `a` is a Z3 map array expression. 4073 >>> f = Function('f', IntSort(), IntSort()) 4074 >>> b = Array('b', IntSort(), IntSort()) 4086 """Return `True` if `a` is a Z3 default array expression. 4087 >>> d = Default(K(IntSort(), 10)) 4091 return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
4094 """Return the function declaration associated with a Z3 map array expression. 4096 >>> f = Function('f', IntSort(), IntSort()) 4097 >>> b = Array('b', IntSort(), IntSort()) 4099 >>> eq(f, get_map_func(a)) 4103 >>> get_map_func(a)(0) 4107 _z3_assert(
is_map(a),
"Z3 array map expression expected.")
4111 """Return the Z3 array sort with the given domain and range sorts. 4113 >>> A = ArraySort(IntSort(), BoolSort()) 4120 >>> AA = ArraySort(IntSort(), A) 4122 Array(Int, Array(Int, Bool)) 4125 _z3_assert(
is_sort(d),
"Z3 sort expected")
4126 _z3_assert(
is_sort(r),
"Z3 sort expected")
4127 _z3_assert(d.ctx == r.ctx,
"Context mismatch")
4132 """Return an array constant named `name` with the given domain and range sorts. 4134 >>> a = Array('a', IntSort(), IntSort()) 4145 """Return a Z3 store array expression. 4147 >>> a = Array('a', IntSort(), IntSort()) 4148 >>> i, v = Ints('i v') 4149 >>> s = Update(a, i, v) 4152 >>> prove(s[i] == v) 4155 >>> prove(Implies(i != j, s[j] == a[j])) 4159 _z3_assert(
is_array(a),
"First argument must be a Z3 array expression")
4160 i = a.domain().cast(i)
4161 v = a.range().cast(v)
4163 return _to_expr_ref(
Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
4166 """ Return a default value for array expression. 4167 >>> b = K(IntSort(), 1) 4168 >>> prove(Default(b) == 1) 4172 _z3_assert(
is_array(a),
"First argument must be a Z3 array expression")
4177 """Return a Z3 store array expression. 4179 >>> a = Array('a', IntSort(), IntSort()) 4180 >>> i, v = Ints('i v') 4181 >>> s = Store(a, i, v) 4184 >>> prove(s[i] == v) 4187 >>> prove(Implies(i != j, s[j] == a[j])) 4193 """Return a Z3 select array expression. 4195 >>> a = Array('a', IntSort(), IntSort()) 4199 >>> eq(Select(a, i), a[i]) 4203 _z3_assert(
is_array(a),
"First argument must be a Z3 array expression")
4208 """Return a Z3 map array expression. 4210 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 4211 >>> a1 = Array('a1', IntSort(), IntSort()) 4212 >>> a2 = Array('a2', IntSort(), IntSort()) 4213 >>> b = Map(f, a1, a2) 4216 >>> prove(b[0] == f(a1[0], a2[0])) 4219 args = _get_args(args)
4221 _z3_assert(len(args) > 0,
"At least one Z3 array expression expected")
4222 _z3_assert(
is_func_decl(f),
"First argument must be a Z3 function declaration")
4223 _z3_assert(all([
is_array(a)
for a
in args]),
"Z3 array expected expected")
4224 _z3_assert(len(args) == f.arity(),
"Number of arguments mismatch")
4225 _args, sz = _to_ast_array(args)
4230 """Return a Z3 constant array expression. 4232 >>> a = K(IntSort(), 10) 4244 _z3_assert(
is_sort(dom),
"Z3 sort expected")
4247 v = _py2expr(v, ctx)
4251 """Return extensionality index for arrays. 4255 return _to_expr_ref(
Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()));
4258 """Return `True` if `a` is a Z3 array select application. 4260 >>> a = Array('a', IntSort(), IntSort()) 4270 """Return `True` if `a` is a Z3 array store application. 4272 >>> a = Array('a', IntSort(), IntSort()) 4275 >>> is_store(Store(a, 0, 1)) 4286 def _valid_accessor(acc):
4287 """Return `True` if acc is pair of the form (String, Datatype or Sort). """ 4288 return isinstance(acc, tuple)
and len(acc) == 2
and isinstance(acc[0], str)
and (isinstance(acc[1], Datatype)
or is_sort(acc[1]))
4291 """Helper class for declaring Z3 datatypes. 4293 >>> List = Datatype('List') 4294 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4295 >>> List.declare('nil') 4296 >>> List = List.create() 4297 >>> # List is now a Z3 declaration 4300 >>> List.cons(10, List.nil) 4302 >>> List.cons(10, List.nil).sort() 4304 >>> cons = List.cons 4308 >>> n = cons(1, cons(0, nil)) 4310 cons(1, cons(0, nil)) 4311 >>> simplify(cdr(n)) 4313 >>> simplify(car(n)) 4323 _z3_assert(isinstance(name, str),
"String expected")
4324 _z3_assert(isinstance(rec_name, str),
"String expected")
4325 _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)")
4329 """Declare constructor named `name` with the given accessors `args`. 4330 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. 4332 In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))` 4333 declares the constructor named `cons` that builds a new List using an integer and a List. 4334 It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell, 4335 and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create 4336 the actual datatype in Z3. 4338 >>> List = Datatype('List') 4339 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4340 >>> List.declare('nil') 4341 >>> List = List.create() 4344 _z3_assert(isinstance(name, str),
"String expected")
4345 _z3_assert(name !=
"",
"Constructor name cannot be empty")
4352 """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`. 4354 The function `CreateDatatypes()` must be used to define mutually recursive datatypes. 4356 >>> List = Datatype('List') 4357 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4358 >>> List.declare('nil') 4359 >>> List = List.create() 4362 >>> List.cons(10, List.nil) 4368 """Auxiliary object used to create Z3 datatypes.""" 4373 if self.
ctx.ref()
is not None:
4377 """Auxiliary object used to create Z3 datatypes.""" 4382 if self.
ctx.ref()
is not None:
4386 """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects. 4388 In the following example we define a Tree-List using two mutually recursive datatypes. 4390 >>> TreeList = Datatype('TreeList') 4391 >>> Tree = Datatype('Tree') 4392 >>> # Tree has two constructors: leaf and node 4393 >>> Tree.declare('leaf', ('val', IntSort())) 4394 >>> # a node contains a list of trees 4395 >>> Tree.declare('node', ('children', TreeList)) 4396 >>> TreeList.declare('nil') 4397 >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList)) 4398 >>> Tree, TreeList = CreateDatatypes(Tree, TreeList) 4399 >>> Tree.val(Tree.leaf(10)) 4401 >>> simplify(Tree.val(Tree.leaf(10))) 4403 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil))) 4405 node(cons(leaf(10), cons(leaf(20), nil))) 4406 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil)) 4407 >>> simplify(n2 == n1) 4409 >>> simplify(TreeList.car(Tree.children(n2)) == n1) 4414 _z3_assert(len(ds) > 0,
"At least one Datatype must be specified")
4415 _z3_assert(all([isinstance(d, Datatype)
for d
in ds]),
"Arguments must be Datatypes")
4416 _z3_assert(all([d.ctx == ds[0].ctx
for d
in ds]),
"Context mismatch")
4417 _z3_assert(all([d.constructors != []
for d
in ds]),
"Non-empty Datatypes expected")
4420 names = (Symbol * num)()
4421 out = (Sort * num)()
4422 clists = (ConstructorList * num)()
4424 for i
in range(num):
4427 num_cs = len(d.constructors)
4428 cs = (Constructor * num_cs)()
4429 for j
in range(num_cs):
4430 c = d.constructors[j]
4435 fnames = (Symbol * num_fs)()
4436 sorts = (Sort * num_fs)()
4437 refs = (ctypes.c_uint * num_fs)()
4438 for k
in range(num_fs):
4442 if isinstance(ftype, Datatype):
4444 _z3_assert(ds.count(ftype) == 1,
"One and only one occurrence of each datatype is expected")
4446 refs[k] = ds.index(ftype)
4449 _z3_assert(
is_sort(ftype),
"Z3 sort expected")
4450 sorts[k] = ftype.ast
4459 for i
in range(num):
4461 num_cs = dref.num_constructors()
4462 for j
in range(num_cs):
4463 cref = dref.constructor(j)
4464 cref_name = cref.name()
4465 cref_arity = cref.arity()
4466 if cref.arity() == 0:
4468 setattr(dref, cref_name, cref)
4469 rref = dref.recognizer(j)
4470 setattr(dref, rref.name(), rref)
4471 for k
in range(cref_arity):
4472 aref = dref.accessor(j, k)
4473 setattr(dref, aref.name(), aref)
4475 return tuple(result)
4478 """Datatype sorts.""" 4480 """Return the number of constructors in the given Z3 datatype. 4482 >>> List = Datatype('List') 4483 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4484 >>> List.declare('nil') 4485 >>> List = List.create() 4486 >>> # List is now a Z3 declaration 4487 >>> List.num_constructors() 4490 return int(Z3_get_datatype_sort_num_constructors(self.
ctx_ref(), self.
ast))
4493 """Return a constructor of the datatype `self`. 4495 >>> List = Datatype('List') 4496 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4497 >>> List.declare('nil') 4498 >>> List = List.create() 4499 >>> # List is now a Z3 declaration 4500 >>> List.num_constructors() 4502 >>> List.constructor(0) 4504 >>> List.constructor(1) 4512 """In Z3, each constructor has an associated recognizer predicate. 4514 If the constructor is named `name`, then the recognizer `is_name`. 4516 >>> List = Datatype('List') 4517 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4518 >>> List.declare('nil') 4519 >>> List = List.create() 4520 >>> # List is now a Z3 declaration 4521 >>> List.num_constructors() 4523 >>> List.recognizer(0) 4525 >>> List.recognizer(1) 4527 >>> simplify(List.is_nil(List.cons(10, List.nil))) 4529 >>> simplify(List.is_cons(List.cons(10, List.nil))) 4531 >>> l = Const('l', List) 4532 >>> simplify(List.is_cons(l)) 4540 """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor. 4542 >>> List = Datatype('List') 4543 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4544 >>> List.declare('nil') 4545 >>> List = List.create() 4546 >>> List.num_constructors() 4548 >>> List.constructor(0) 4550 >>> num_accs = List.constructor(0).arity() 4553 >>> List.accessor(0, 0) 4555 >>> List.accessor(0, 1) 4557 >>> List.constructor(1) 4559 >>> num_accs = List.constructor(1).arity() 4565 _z3_assert(j < self.
constructor(i).arity(),
"Invalid accessor index")
4569 """Datatype expressions.""" 4571 """Return the datatype sort of the datatype expression `self`.""" 4575 """Return a new enumeration sort named `name` containing the given values. 4577 The result is a pair (sort, list of constants). 4579 >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue']) 4582 _z3_assert(isinstance(name, str),
"Name must be a string")
4583 _z3_assert(all([isinstance(v, str)
for v
in values]),
"Eumeration sort values must be strings")
4584 _z3_assert(len(values) > 0,
"At least one value expected")
4587 _val_names = (Symbol * num)()
4588 for i
in range(num):
4590 _values = (FuncDecl * num)()
4591 _testers = (FuncDecl * num)()
4595 for i
in range(num):
4597 V = [a()
for a
in V]
4607 """Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3. 4609 Consider using the function `args2params` to create instances of this object. 4617 if self.
ctx.ref()
is not None:
4621 """Set parameter name with value val.""" 4623 _z3_assert(isinstance(name, str),
"parameter name must be a string")
4625 if isinstance(val, bool):
4629 elif isinstance(val, float):
4631 elif isinstance(val, str):
4635 _z3_assert(
False,
"invalid parameter value")
4641 _z3_assert(isinstance(ds, ParamDescrsRef),
"parameter description set expected")
4645 """Convert python arguments into a Z3_params object. 4646 A ':' is added to the keywords, and '_' is replaced with '-' 4648 >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) 4649 (params model true relevancy 2 elim_and true) 4652 _z3_assert(len(arguments) % 2 == 0,
"Argument list must have an even number of elements.")
4667 """Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3. 4670 _z3_assert(isinstance(descr, ParamDescrs),
"parameter description object expected")
4676 if self.
ctx.ref()
is not None:
4680 """Return the size of in the parameter description `self`. 4685 """Return the size of in the parameter description `self`. 4690 """Return the i-th parameter name in the parameter description `self`. 4695 """Return the kind of the parameter named `n`. 4700 """Return the documentation string of the parameter named `n`. 4720 """Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible). 4722 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals. 4723 A goal has a solution if one of its subgoals has a solution. 4724 A goal is unsatisfiable if all subgoals are unsatisfiable. 4727 def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
4729 _z3_assert(goal
is None or ctx
is not None,
"If goal is different from None, then ctx must be also different from None")
4732 if self.
goal is None:
4737 if self.
goal is not None and self.
ctx.ref()
is not None:
4741 """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`. 4743 >>> x, y = Ints('x y') 4745 >>> g.add(x == 0, y >= x + 1) 4748 >>> r = Then('simplify', 'solve-eqs')(g) 4749 >>> # r has 1 subgoal 4758 """Return `True` if `self` contains the `False` constraints. 4760 >>> x, y = Ints('x y') 4762 >>> g.inconsistent() 4764 >>> g.add(x == 0, x == 1) 4767 >>> g.inconsistent() 4769 >>> g2 = Tactic('propagate-values')(g)[0] 4770 >>> g2.inconsistent() 4776 """Return the precision (under-approximation, over-approximation, or precise) of the goal `self`. 4779 >>> g.prec() == Z3_GOAL_PRECISE 4781 >>> x, y = Ints('x y') 4782 >>> g.add(x == y + 1) 4783 >>> g.prec() == Z3_GOAL_PRECISE 4785 >>> t = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10) 4788 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0] 4789 >>> g2.prec() == Z3_GOAL_PRECISE 4791 >>> g2.prec() == Z3_GOAL_UNDER 4797 """Alias for `prec()`. 4800 >>> g.precision() == Z3_GOAL_PRECISE 4806 """Return the number of constraints in the goal `self`. 4811 >>> x, y = Ints('x y') 4812 >>> g.add(x == 0, y > x) 4819 """Return the number of constraints in the goal `self`. 4824 >>> x, y = Ints('x y') 4825 >>> g.add(x == 0, y > x) 4832 """Return a constraint in the goal `self`. 4835 >>> x, y = Ints('x y') 4836 >>> g.add(x == 0, y > x) 4845 """Return a constraint in the goal `self`. 4848 >>> x, y = Ints('x y') 4849 >>> g.add(x == 0, y > x) 4855 if arg >= len(self):
4857 return self.
get(arg)
4860 """Assert constraints into the goal. 4864 >>> g.assert_exprs(x > 0, x < 2) 4868 args = _get_args(args)
4879 >>> g.append(x > 0, x < 2) 4890 >>> g.insert(x > 0, x < 2) 4901 >>> g.add(x > 0, x < 2) 4908 return obj_to_string(self)
4911 """Return a textual representation of the s-expression representing the goal.""" 4915 """Copy goal `self` to context `target`. 4923 >>> g2 = g.translate(c2) 4926 >>> g.ctx == main_ctx() 4930 >>> g2.ctx == main_ctx() 4934 _z3_assert(isinstance(target, Context),
"target must be a context")
4938 """Return a new simplified goal. 4940 This method is essentially invoking the simplify tactic. 4944 >>> g.add(x + 1 >= 2) 4947 >>> g2 = g.simplify() 4950 >>> # g was not modified 4955 return t.apply(self, *arguments, **keywords)[0]
4958 """Return goal `self` as a single Z3 expression. 4977 return And([ self.
get(i)
for i
in range(len(self)) ], self.
ctx)
4985 """A collection (vector) of ASTs.""" 4991 self.
vector = Z3_mk_ast_vector(self.
ctx.ref())
4994 assert ctx
is not None 4996 Z3_ast_vector_inc_ref(self.
ctx.ref(), self.
vector)
4999 if self.
vector is not None and self.
ctx.ref()
is not None:
5000 Z3_ast_vector_dec_ref(self.
ctx.ref(), self.
vector)
5003 """Return the size of the vector `self`. 5008 >>> A.push(Int('x')) 5009 >>> A.push(Int('x')) 5013 return int(Z3_ast_vector_size(self.
ctx.ref(), self.
vector))
5016 """Return the AST at position `i`. 5019 >>> A.push(Int('x') + 1) 5020 >>> A.push(Int('y')) 5028 return _to_ast_ref(Z3_ast_vector_get(self.
ctx.ref(), self.
vector, i), self.
ctx)
5031 """Update AST at position `i`. 5034 >>> A.push(Int('x') + 1) 5035 >>> A.push(Int('y')) 5044 Z3_ast_vector_set(self.
ctx.ref(), self.
vector, i, v.as_ast())
5047 """Add `v` in the end of the vector. 5052 >>> A.push(Int('x')) 5056 Z3_ast_vector_push(self.
ctx.ref(), self.
vector, v.as_ast())
5059 """Resize the vector to `sz` elements. 5065 >>> for i in range(10): A[i] = Int('x') 5069 Z3_ast_vector_resize(self.
ctx.ref(), self.
vector, sz)
5072 """Return `True` if the vector contains `item`. 5095 """Copy vector `self` to context `other_ctx`. 5101 >>> B = A.translate(c2) 5105 return AstVector(Z3_ast_vector_translate(self.
ctx.ref(), self.
vector, other_ctx.ref()), other_ctx)
5108 return obj_to_string(self)
5111 """Return a textual representation of the s-expression representing the vector.""" 5112 return Z3_ast_vector_to_string(self.
ctx.ref(), self.
vector)
5120 """A mapping from ASTs to ASTs.""" 5126 self.
map = Z3_mk_ast_map(self.
ctx.ref())
5129 assert ctx
is not None 5131 Z3_ast_map_inc_ref(self.
ctx.ref(), self.
map)
5134 if self.
map is not None and self.
ctx.ref()
is not None:
5135 Z3_ast_map_dec_ref(self.
ctx.ref(), self.
map)
5138 """Return the size of the map. 5144 >>> M[x] = IntVal(1) 5148 return int(Z3_ast_map_size(self.
ctx.ref(), self.
map))
5151 """Return `True` if the map contains key `key`. 5161 return Z3_ast_map_contains(self.
ctx.ref(), self.
map, key.as_ast())
5164 """Retrieve the value associated with key `key`. 5172 return _to_ast_ref(Z3_ast_map_find(self.
ctx.ref(), self.
map, key.as_ast()), self.
ctx)
5175 """Add/Update key `k` with value `v`. 5184 >>> M[x] = IntVal(1) 5188 Z3_ast_map_insert(self.
ctx.ref(), self.
map, k.as_ast(), v.as_ast())
5191 return Z3_ast_map_to_string(self.
ctx.ref(), self.
map)
5194 """Remove the entry associated with key `k`. 5205 Z3_ast_map_erase(self.
ctx.ref(), self.
map, k.as_ast())
5208 """Remove all entries from the map. 5213 >>> M[x+x] = IntVal(1) 5220 Z3_ast_map_reset(self.
ctx.ref(), self.
map)
5223 """Return an AstVector containing all keys in the map. 5228 >>> M[x+x] = IntVal(1) 5241 """Store the value of the interpretation of a function in a particular point.""" 5249 if self.
ctx.ref()
is not None:
5253 """Return the number of arguments in the given entry. 5255 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5257 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5262 >>> f_i.num_entries() 5264 >>> e = f_i.entry(0) 5271 """Return the value of argument `idx`. 5273 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5275 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5280 >>> f_i.num_entries() 5282 >>> e = f_i.entry(0) 5293 ... except IndexError: 5294 ... print("index error") 5302 """Return the value of the function at point `self`. 5304 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5306 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5311 >>> f_i.num_entries() 5313 >>> e = f_i.entry(0) 5324 """Return entry `self` as a Python list. 5325 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5327 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5332 >>> f_i.num_entries() 5334 >>> e = f_i.entry(0) 5339 args.append(self.
value())
5346 """Stores the interpretation of a function in a Z3 model.""" 5351 if self.
f is not None:
5355 if self.
f is not None and self.
ctx.ref()
is not None:
5360 Return the `else` value for a function interpretation. 5361 Return None if Z3 did not specify the `else` value for 5364 >>> f = Function('f', IntSort(), IntSort()) 5366 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5371 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5372 >>> m[f].else_value() 5377 return _to_expr_ref(r, self.
ctx)
5382 """Return the number of entries/points in the function interpretation `self`. 5384 >>> f = Function('f', IntSort(), IntSort()) 5386 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5391 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5392 >>> m[f].num_entries() 5398 """Return the number of arguments for each entry in the function interpretation `self`. 5400 >>> f = Function('f', IntSort(), IntSort()) 5402 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5412 """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`. 5414 >>> f = Function('f', IntSort(), IntSort()) 5416 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5421 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5422 >>> m[f].num_entries() 5436 """Return the function interpretation as a Python list. 5437 >>> f = Function('f', IntSort(), IntSort()) 5439 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5444 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5446 [[0, 1], [1, 1], [2, 0], 1] 5453 return obj_to_string(self)
5456 """Model/Solution of a satisfiability problem (aka system of constraints).""" 5459 assert ctx
is not None 5465 if self.
ctx.ref()
is not None:
5469 return obj_to_string(self)
5472 """Return a textual representation of the s-expression representing the model.""" 5475 def eval(self, t, model_completion=False):
5476 """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`. 5480 >>> s.add(x > 0, x < 2) 5493 >>> m.eval(y, model_completion=True) 5495 >>> # Now, m contains an interpretation for y 5501 return _to_expr_ref(r[0], self.
ctx)
5502 raise Z3Exception(
"failed to evaluate expression in the model")
5505 """Alias for `eval`. 5509 >>> s.add(x > 0, x < 2) 5513 >>> m.evaluate(x + 1) 5515 >>> m.evaluate(x == 1) 5518 >>> m.evaluate(y + x) 5522 >>> m.evaluate(y, model_completion=True) 5524 >>> # Now, m contains an interpretation for y 5525 >>> m.evaluate(y + x) 5528 return self.
eval(t, model_completion)
5531 """Return the number of constant and function declarations in the model `self`. 5533 >>> f = Function('f', IntSort(), IntSort()) 5536 >>> s.add(x > 0, f(x) != x) 5546 """Return the interpretation for a given declaration or constant. 5548 >>> f = Function('f', IntSort(), IntSort()) 5551 >>> s.add(x > 0, x < 2, f(x) == 0) 5561 _z3_assert(isinstance(decl, FuncDeclRef)
or is_const(decl),
"Z3 declaration expected")
5565 if decl.arity() == 0:
5567 if _r.value
is None:
5569 r = _to_expr_ref(_r, self.
ctx)
5580 """Return the number of unintepreted sorts that contain an interpretation in the model `self`. 5582 >>> A = DeclareSort('A') 5583 >>> a, b = Consts('a b', A) 5595 """Return the unintepreted sort at position `idx` < self.num_sorts(). 5597 >>> A = DeclareSort('A') 5598 >>> B = DeclareSort('B') 5599 >>> a1, a2 = Consts('a1 a2', A) 5600 >>> b1, b2 = Consts('b1 b2', B) 5602 >>> s.add(a1 != a2, b1 != b2) 5618 """Return all uninterpreted sorts that have an interpretation in the model `self`. 5620 >>> A = DeclareSort('A') 5621 >>> B = DeclareSort('B') 5622 >>> a1, a2 = Consts('a1 a2', A) 5623 >>> b1, b2 = Consts('b1 b2', B) 5625 >>> s.add(a1 != a2, b1 != b2) 5635 """Return the intepretation for the uninterpreted sort `s` in the model `self`. 5637 >>> A = DeclareSort('A') 5638 >>> a, b = Consts('a b', A) 5644 >>> m.get_universe(A) 5648 _z3_assert(isinstance(s, SortRef),
"Z3 sort expected")
5655 """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. 5657 The elements can be retrieved using position or the actual declaration. 5659 >>> f = Function('f', IntSort(), IntSort()) 5662 >>> s.add(x > 0, x < 2, f(x) == 0) 5676 >>> for d in m: print("%s -> %s" % (d, m[d])) 5678 f -> [1 -> 0, else -> 0] 5681 if idx >= len(self):
5684 if (idx < num_consts):
5688 if isinstance(idx, FuncDeclRef):
5692 if isinstance(idx, SortRef):
5695 _z3_assert(
False,
"Integer, Z3 declaration, or Z3 constant expected")
5699 """Return a list with all symbols that have an interpreation in the model `self`. 5700 >>> f = Function('f', IntSort(), IntSort()) 5703 >>> s.add(x > 0, x < 2, f(x) == 0) 5718 """Return true if n is a Z3 expression of the form (_ as-array f).""" 5719 return isinstance(n, ExprRef)
and Z3_is_as_array(n.ctx.ref(), n.as_ast())
5722 """Return the function declaration f associated with a Z3 expression of the form (_ as-array f).""" 5724 _z3_assert(
is_as_array(n),
"as-array Z3 expression expected.")
5733 """Statistics for `Solver.check()`.""" 5741 if self.
ctx.ref()
is not None:
5748 out.write(u(
'<table border="1" cellpadding="2" cellspacing="0">'))
5751 out.write(u(
'<tr style="background-color:#CFCFCF">'))
5754 out.write(u(
'<tr>'))
5756 out.write(u(
'<td>%s</td><td>%s</td></tr>' % (k, v)))
5757 out.write(u(
'</table>'))
5758 return out.getvalue()
5763 """Return the number of statistical counters. 5766 >>> s = Then('simplify', 'nlsat').solver() 5770 >>> st = s.statistics() 5777 """Return the value of statistical counter at position `idx`. The result is a pair (key, value). 5780 >>> s = Then('simplify', 'nlsat').solver() 5784 >>> st = s.statistics() 5788 ('nlsat propagations', 2) 5792 if idx >= len(self):
5801 """Return the list of statistical counters. 5804 >>> s = Then('simplify', 'nlsat').solver() 5808 >>> st = s.statistics() 5813 """Return the value of a particular statistical counter. 5816 >>> s = Then('simplify', 'nlsat').solver() 5820 >>> st = s.statistics() 5821 >>> st.get_key_value('nlsat propagations') 5824 for idx
in range(len(self)):
5830 raise Z3Exception(
"unknown key")
5833 """Access the value of statistical using attributes. 5835 Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'), 5836 we should use '_' (e.g., 'nlsat_propagations'). 5839 >>> s = Then('simplify', 'nlsat').solver() 5843 >>> st = s.statistics() 5844 >>> st.nlsat_propagations 5849 key = name.replace(
'_',
' ')
5853 raise AttributeError
5861 """Represents the result of a satisfiability check: sat, unsat, unknown. 5867 >>> isinstance(r, CheckSatResult) 5875 return isinstance(other, CheckSatResult)
and self.
r == other.r
5878 return not self.
__eq__(other)
5882 if self.
r == Z3_L_TRUE:
5884 elif self.
r == Z3_L_FALSE:
5885 return "<b>unsat</b>" 5887 return "<b>unknown</b>" 5889 if self.
r == Z3_L_TRUE:
5891 elif self.
r == Z3_L_FALSE:
5901 """Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.""" 5904 assert solver
is None or ctx
is not None 5914 if self.
solver is not None and self.
ctx.ref()
is not None:
5918 """Set a configuration option. The method `help()` return a string containing all available options. 5921 >>> # The option MBQI can be set using three different approaches. 5922 >>> s.set(mbqi=True) 5923 >>> s.set('MBQI', True) 5924 >>> s.set(':mbqi', True) 5930 """Create a backtracking point. 5952 """Backtrack \c num backtracking points. 5974 """Remove all asserted constraints and backtracking points created using `push()`. 5988 """Assert constraints into the solver. 5992 >>> s.assert_exprs(x > 0, x < 2) 5996 args = _get_args(args)
5999 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
6007 """Assert constraints into the solver. 6011 >>> s.add(x > 0, x < 2) 6022 """Assert constraints into the solver. 6026 >>> s.append(x > 0, x < 2) 6033 """Assert constraints into the solver. 6037 >>> s.insert(x > 0, x < 2) 6044 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`. 6046 If `p` is a string, it will be automatically converted into a Boolean constant. 6051 >>> s.set(unsat_core=True) 6052 >>> s.assert_and_track(x > 0, 'p1') 6053 >>> s.assert_and_track(x != 1, 'p2') 6054 >>> s.assert_and_track(x < 0, p3) 6055 >>> print(s.check()) 6057 >>> c = s.unsat_core() 6067 if isinstance(p, str):
6069 _z3_assert(isinstance(a, BoolRef),
"Boolean expression expected")
6070 _z3_assert(isinstance(p, BoolRef)
and is_const(p),
"Boolean expression expected")
6074 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not. 6080 >>> s.add(x > 0, x < 2) 6089 >>> s.add(2**x == 4) 6093 assumptions = _get_args(assumptions)
6094 num = len(assumptions)
6095 _assumptions = (Ast * num)()
6096 for i
in range(num):
6097 _assumptions[i] = assumptions[i].as_ast()
6102 """Return a model for the last `check()`. 6104 This function raises an exception if 6105 a model is not available (e.g., last `check()` returned unsat). 6109 >>> s.add(a + 2 == 0) 6118 raise Z3Exception(
"model is not available")
6121 """Return a subset (as an AST vector) of the assumptions provided to the last check(). 6123 These are the assumptions Z3 used in the unsatisfiability proof. 6124 Assumptions are available in Z3. They are used to extract unsatisfiable cores. 6125 They may be also used to "retract" assumptions. Note that, assumptions are not really 6126 "soft constraints", but they can be used to implement them. 6128 >>> p1, p2, p3 = Bools('p1 p2 p3') 6129 >>> x, y = Ints('x y') 6131 >>> s.add(Implies(p1, x > 0)) 6132 >>> s.add(Implies(p2, y > x)) 6133 >>> s.add(Implies(p2, y < 1)) 6134 >>> s.add(Implies(p3, y > -3)) 6135 >>> s.check(p1, p2, p3) 6137 >>> core = s.unsat_core() 6146 >>> # "Retracting" p2 6153 """Determine fixed values for the variables based on the solver state and assumptions. 6155 >>> a, b, c, d = Bools('a b c d') 6156 >>> s.add(Implies(a,b), Implies(b, c)) 6157 >>> s.consequences([a],[b,c,d]) 6158 (sat, [Implies(a, b), Implies(a, c)]) 6159 >>> s.consequences([Not(c),d],[a,b,c,d]) 6160 (sat, [Implies(Not(c), Not(c)), Implies(d, d), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))]) 6162 if isinstance(assumptions, list):
6164 for a
in assumptions:
6167 if isinstance(variables, list):
6172 _z3_assert(isinstance(assumptions, AstVector),
"ast vector expected")
6173 _z3_assert(isinstance(variables, AstVector),
"ast vector expected")
6176 sz = len(consequences)
6177 consequences = [ consequences[i]
for i
in range(sz) ]
6181 """Return a proof for the last `check()`. Proof construction must be enabled.""" 6185 """Return an AST vector containing all added constraints. 6199 """Return statistics for the last `check()`. 6201 >>> s = SimpleSolver() 6206 >>> st = s.statistics() 6207 >>> st.get_key_value('final checks') 6217 """Return a string describing why the last `check()` returned `unknown`. 6220 >>> s = SimpleSolver() 6221 >>> s.add(2**x == 4) 6224 >>> s.reason_unknown() 6225 '(incomplete (theory arithmetic))' 6230 """Display a string describing all available options.""" 6234 """Return the parameter description set.""" 6238 """Return a formatted string with all added constraints.""" 6239 return obj_to_string(self)
6242 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 6246 >>> s1 = Solver(ctx=c1) 6247 >>> s2 = s1.translate(c2) 6250 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
6252 return Solver(solver, target)
6255 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 6266 """return SMTLIB2 formatted benchmark for solver's assertions""" 6273 for i
in range(sz1):
6274 v[i] = es[i].as_ast()
6276 e = es[sz1].as_ast()
6282 """Create a solver customized for the given logic. 6284 The parameter `logic` is a string. It should be contains 6285 the name of a SMT-LIB logic. 6286 See http://www.smtlib.org/ for the name of all available logics. 6288 >>> s = SolverFor("QF_LIA") 6302 """Return a simple general purpose solver with limited amount of preprocessing. 6304 >>> s = SimpleSolver() 6320 """Fixedpoint API provides methods for solving with recursive predicates""" 6323 assert fixedpoint
is None or ctx
is not None 6326 if fixedpoint
is None:
6334 if self.
fixedpoint is not None and self.
ctx.ref()
is not None:
6338 """Set a configuration option. The method `help()` return a string containing all available options. 6341 Z3_fixedpoint_set_params(self.
ctx.ref(), self.
fixedpoint, p.params)
6344 """Display a string describing all available options.""" 6345 print(Z3_fixedpoint_get_help(self.
ctx.ref(), self.
fixedpoint))
6348 """Return the parameter description set.""" 6352 """Assert constraints as background axioms for the fixedpoint solver.""" 6353 args = _get_args(args)
6356 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
6359 Z3_fixedpoint_assert(self.
ctx.ref(), self.
fixedpoint, f.as_ast())
6363 Z3_fixedpoint_assert(self.
ctx.ref(), self.
fixedpoint, arg.as_ast())
6366 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6374 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6378 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 6382 """Assert rules defining recursive predicates to the fixedpoint solver. 6385 >>> s = Fixedpoint() 6386 >>> s.register_relation(a.decl()) 6387 >>> s.register_relation(b.decl()) 6398 Z3_fixedpoint_add_rule(self.
ctx.ref(), self.
fixedpoint, head.as_ast(), name)
6400 body = _get_args(body)
6402 Z3_fixedpoint_add_rule(self.
ctx.ref(), self.
fixedpoint, f.as_ast(), name)
6404 def rule(self, head, body = None, name = None):
6405 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 6409 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 6413 """Query the fixedpoint engine whether formula is derivable. 6414 You can also pass an tuple or list of recursive predicates. 6416 query = _get_args(query)
6418 if sz >= 1
and isinstance(query[0], FuncDeclRef):
6419 _decls = (FuncDecl * sz)()
6424 r = Z3_fixedpoint_query_relations(self.
ctx.ref(), self.
fixedpoint, sz, _decls)
6429 query =
And(query, self.
ctx)
6430 query = self.
abstract(query,
False)
6431 r = Z3_fixedpoint_query(self.
ctx.ref(), self.
fixedpoint, query.as_ast())
6435 """create a backtracking point for added rules, facts and assertions""" 6439 """restore to previously created backtracking point""" 6447 body = _get_args(body)
6449 Z3_fixedpoint_update_rule(self.
ctx.ref(), self.
fixedpoint, f.as_ast(), name)
6452 """Retrieve answer from last query call.""" 6453 r = Z3_fixedpoint_get_answer(self.
ctx.ref(), self.
fixedpoint)
6454 return _to_expr_ref(r, self.
ctx)
6457 """Retrieve number of levels used for predicate in PDR engine""" 6458 return Z3_fixedpoint_get_num_levels(self.
ctx.ref(), self.
fixedpoint, predicate.ast)
6461 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)""" 6462 r = Z3_fixedpoint_get_cover_delta(self.
ctx.ref(), self.
fixedpoint, level, predicate.ast)
6463 return _to_expr_ref(r, self.
ctx)
6466 """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)""" 6467 Z3_fixedpoint_add_cover(self.
ctx.ref(), self.
fixedpoint, level, predicate.ast, property.ast)
6470 """Register relation as recursive""" 6471 relations = _get_args(relations)
6473 Z3_fixedpoint_register_relation(self.
ctx.ref(), self.
fixedpoint, f.ast)
6476 """Control how relation is represented""" 6477 representations = _get_args(representations)
6478 representations = [
to_symbol(s)
for s
in representations]
6479 sz = len(representations)
6480 args = (Symbol * sz)()
6482 args[i] = representations[i]
6483 Z3_fixedpoint_set_predicate_representation(self.
ctx.ref(), self.
fixedpoint, f.ast, sz, args)
6486 """Parse rules and queries from a string""" 6490 """Parse rules and queries from a file""" 6494 """retrieve rules that have been added to fixedpoint context""" 6498 """retrieve assertions that have been added to fixedpoint context""" 6502 """Return a formatted string with all added rules and constraints.""" 6506 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 6508 return Z3_fixedpoint_to_string(self.
ctx.ref(), self.
fixedpoint, 0, (Ast * 0)())
6511 """Return a formatted string (in Lisp-like format) with all added constraints. 6512 We say the string is in s-expression format. 6513 Include also queries. 6515 args, len = _to_ast_array(queries)
6516 return Z3_fixedpoint_to_string(self.
ctx.ref(), self.
fixedpoint, len, args)
6519 """Return statistics for the last `query()`. 6524 """Return a string describing why the last `query()` returned `unknown`. 6526 return Z3_fixedpoint_get_reason_unknown(self.
ctx.ref(), self.
fixedpoint)
6529 """Add variable or several variables. 6530 The added variable or variables will be bound in the rules 6533 vars = _get_args(vars)
6553 """Finite domain sort.""" 6556 """Return the size of the finite domain sort""" 6557 r = (ctype.c_ulonglong * 1)()
6558 if Z3_get_finite_domain_sort_size(self.
ctx_ref(), self.
ast(), r):
6561 raise Z3Exception(
"Failed to retrieve finite domain sort size")
6564 """Create a named finite domain sort of a given size sz""" 6565 if not isinstance(name, Symbol):
6571 """Return True if `s` is a Z3 finite-domain sort. 6573 >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) 6575 >>> is_finite_domain_sort(IntSort()) 6578 return isinstance(s, FiniteDomainSortRef)
6582 """Finite-domain expressions.""" 6585 """Return the sort of the finite-domain expression `self`.""" 6589 """Return a Z3 floating point expression as a Python string.""" 6593 """Return `True` if `a` is a Z3 finite-domain expression. 6595 >>> s = FiniteDomainSort('S', 100) 6596 >>> b = Const('b', s) 6597 >>> is_finite_domain(b) 6599 >>> is_finite_domain(Int('x')) 6602 return isinstance(a, FiniteDomainRef)
6606 """Integer values.""" 6609 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. 6611 >>> s = FiniteDomainSort('S', 100) 6612 >>> v = FiniteDomainVal(3, s) 6621 """Return a Z3 finite-domain numeral as a Python string. 6623 >>> s = FiniteDomainSort('S', 100) 6624 >>> v = FiniteDomainVal(42, s) 6632 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. 6634 >>> s = FiniteDomainSort('S', 256) 6635 >>> FiniteDomainVal(255, s) 6637 >>> FiniteDomainVal('100', s) 6646 """Return `True` if `a` is a Z3 finite-domain value. 6648 >>> s = FiniteDomainSort('S', 100) 6649 >>> b = Const('b', s) 6650 >>> is_finite_domain_value(b) 6652 >>> b = FiniteDomainVal(10, s) 6655 >>> is_finite_domain_value(b) 6675 return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self.
_value), opt.ctx)
6679 return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self.
_value), opt.ctx)
6688 """Optimize API provides methods for solving using objective functions and weighted soft constraints""" 6693 Z3_optimize_inc_ref(self.
ctx.ref(), self.
optimize)
6696 if self.
optimize is not None and self.
ctx.ref()
is not None:
6697 Z3_optimize_dec_ref(self.
ctx.ref(), self.
optimize)
6700 """Set a configuration option. The method `help()` return a string containing all available options. 6703 Z3_optimize_set_params(self.
ctx.ref(), self.
optimize, p.params)
6706 """Display a string describing all available options.""" 6707 print(Z3_optimize_get_help(self.
ctx.ref(), self.
optimize))
6710 """Return the parameter description set.""" 6714 """Assert constraints as background axioms for the optimize solver.""" 6715 args = _get_args(args)
6717 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
6719 Z3_optimize_assert(self.
ctx.ref(), self.
optimize, f.as_ast())
6721 Z3_optimize_assert(self.
ctx.ref(), self.
optimize, arg.as_ast())
6724 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr.""" 6732 """Add soft constraint with optional weight and optional identifier. 6733 If no weight is supplied, then the penalty for violating the soft constraint 6735 Soft constraints are grouped by identifiers. Soft constraints that are 6736 added without identifiers are grouped by default. 6739 weight =
"%d" % weight
6740 elif isinstance(weight, float):
6741 weight =
"%f" % weight
6742 if not isinstance(weight, str):
6743 raise Z3Exception(
"weight should be a string or an integer")
6747 v = Z3_optimize_assert_soft(self.
ctx.ref(), self.
optimize, arg.as_ast(), weight, id)
6751 """Add objective function to maximize.""" 6755 """Add objective function to minimize.""" 6759 """create a backtracking point for added rules, facts and assertions""" 6763 """restore to previously created backtracking point""" 6767 """Check satisfiability while optimizing objective functions.""" 6771 """Return a string that describes why the last `check()` returned `unknown`.""" 6772 return Z3_optimize_get_reason_unknown(self.
ctx.ref(), self.
optimize)
6775 """Return a model for the last check().""" 6779 raise Z3Exception(
"model is not available")
6782 if not isinstance(obj, OptimizeObjective):
6783 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
6787 if not isinstance(obj, OptimizeObjective):
6788 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
6792 """Parse assertions and objectives from a file""" 6793 Z3_optimize_from_file(self.
ctx.ref(), self.
optimize, filename)
6796 """Parse assertions and objectives from a string""" 6797 Z3_optimize_from_string(self.
ctx.ref(), self.
optimize, s)
6800 """Return an AST vector containing all added constraints.""" 6804 """returns set of objective functions""" 6808 """Return a formatted string with all added rules and constraints.""" 6812 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 6814 return Z3_optimize_to_string(self.
ctx.ref(), self.
optimize)
6817 """Return statistics for the last check`. 6830 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters.""" 6838 if self.
ctx.ref()
is not None:
6842 """Return the number of subgoals in `self`. 6844 >>> a, b = Ints('a b') 6846 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 6847 >>> t = Tactic('split-clause') 6851 >>> t = Then(Tactic('split-clause'), Tactic('split-clause')) 6854 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values')) 6861 """Return one of the subgoals stored in ApplyResult object `self`. 6863 >>> a, b = Ints('a b') 6865 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 6866 >>> t = Tactic('split-clause') 6869 [a == 0, Or(b == 0, b == 1), a > b] 6871 [a == 1, Or(b == 0, b == 1), a > b] 6873 if idx >= len(self):
6878 return obj_to_string(self)
6881 """Return a textual representation of the s-expression representing the set of subgoals in `self`.""" 6885 """Convert a model for a subgoal into a model for the original goal. 6887 >>> a, b = Ints('a b') 6889 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 6890 >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs')) 6893 [Or(b == 0, b == 1), Not(0 <= b)] 6895 [Or(b == 0, b == 1), Not(1 <= b)] 6896 >>> # Remark: the subgoal r[0] is unsatisfiable 6897 >>> # Creating a solver for solving the second subgoal 6904 >>> # Model s.model() does not assign a value to `a` 6905 >>> # It is a model for subgoal `r[1]`, but not for goal `g` 6906 >>> # The method convert_model creates a model for `g` from a model for `r[1]`. 6907 >>> r.convert_model(s.model(), 1) 6911 _z3_assert(idx < len(self),
"index out of bounds")
6912 _z3_assert(isinstance(model, ModelRef),
"Z3 Model expected")
6916 """Return a Z3 expression consisting of all subgoals. 6921 >>> g.add(Or(x == 2, x == 3)) 6922 >>> r = Tactic('simplify')(g) 6924 [[Not(x <= 1), Or(x == 2, x == 3)]] 6926 And(Not(x <= 1), Or(x == 2, x == 3)) 6927 >>> r = Tactic('split-clause')(g) 6929 [[x > 1, x == 2], [x > 1, x == 3]] 6931 Or(And(x > 1, x == 2), And(x > 1, x == 3)) 6939 return Or([ self[i].
as_expr()
for i
in range(len(self)) ])
6947 """Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver(). 6949 Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond(). 6954 if isinstance(tactic, TacticObj):
6958 _z3_assert(isinstance(tactic, str),
"tactic name expected")
6962 raise Z3Exception(
"unknown tactic '%s'" % tactic)
6966 if self.
tactic is not None and self.
ctx.ref()
is not None:
6970 """Create a solver using the tactic `self`. 6972 The solver supports the methods `push()` and `pop()`, but it 6973 will always solve each `check()` from scratch. 6975 >>> t = Then('simplify', 'nlsat') 6978 >>> s.add(x**2 == 2, x > 0) 6986 def apply(self, goal, *arguments, **keywords):
6987 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 6989 >>> x, y = Ints('x y') 6990 >>> t = Tactic('solve-eqs') 6991 >>> t.apply(And(x == 0, y >= x + 1)) 6995 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expressions expected")
6996 goal = _to_goal(goal)
6997 if len(arguments) > 0
or len(keywords) > 0:
7004 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 7006 >>> x, y = Ints('x y') 7007 >>> t = Tactic('solve-eqs') 7008 >>> t(And(x == 0, y >= x + 1)) 7011 return self.
apply(goal, *arguments, **keywords)
7014 """Display a string containing a description of the available options for the `self` tactic.""" 7018 """Return the parameter description set.""" 7022 if isinstance(a, BoolRef):
7023 goal =
Goal(ctx = a.ctx)
7029 def _to_tactic(t, ctx=None):
7030 if isinstance(t, Tactic):
7035 def _and_then(t1, t2, ctx=None):
7036 t1 = _to_tactic(t1, ctx)
7037 t2 = _to_tactic(t2, ctx)
7039 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7042 def _or_else(t1, t2, ctx=None):
7043 t1 = _to_tactic(t1, ctx)
7044 t2 = _to_tactic(t2, ctx)
7046 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7050 """Return a tactic that applies the tactics in `*ts` in sequence. 7052 >>> x, y = Ints('x y') 7053 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) 7054 >>> t(And(x == 0, y > x + 1)) 7056 >>> t(And(x == 0, y > x + 1)).as_expr() 7060 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7061 ctx = ks.get(
'ctx',
None)
7064 for i
in range(num - 1):
7065 r = _and_then(r, ts[i+1], ctx)
7069 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). 7071 >>> x, y = Ints('x y') 7072 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) 7073 >>> t(And(x == 0, y > x + 1)) 7075 >>> t(And(x == 0, y > x + 1)).as_expr() 7081 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). 7084 >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) 7085 >>> # Tactic split-clause fails if there is no clause in the given goal. 7088 >>> t(Or(x == 0, x == 1)) 7089 [[x == 0], [x == 1]] 7092 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7093 ctx = ks.get(
'ctx',
None)
7096 for i
in range(num - 1):
7097 r = _or_else(r, ts[i+1], ctx)
7101 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). 7104 >>> t = ParOr(Tactic('simplify'), Tactic('fail')) 7109 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7110 ctx = _get_ctx(ks.get(
'ctx',
None))
7111 ts = [ _to_tactic(t, ctx)
for t
in ts ]
7113 _args = (TacticObj * sz)()
7115 _args[i] = ts[i].tactic
7119 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. 7121 >>> x, y = Ints('x y') 7122 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) 7123 >>> t(And(Or(x == 1, x == 2), y == x + 1)) 7124 [[x == 1, y == 2], [x == 2, y == 3]] 7126 t1 = _to_tactic(t1, ctx)
7127 t2 = _to_tactic(t2, ctx)
7129 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
7133 """Alias for ParThen(t1, t2, ctx).""" 7137 """Return a tactic that applies tactic `t` using the given configuration options. 7139 >>> x, y = Ints('x y') 7140 >>> t = With(Tactic('simplify'), som=True) 7141 >>> t((x + 1)*(y + 2) == 0) 7142 [[2*x + y + x*y == -2]] 7144 ctx = keys.get(
'ctx',
None)
7145 t = _to_tactic(t, ctx)
7150 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. 7152 >>> x, y = Ints('x y') 7153 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) 7154 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) 7156 >>> for subgoal in r: print(subgoal) 7157 [x == 0, y == 0, x > y] 7158 [x == 0, y == 1, x > y] 7159 [x == 1, y == 0, x > y] 7160 [x == 1, y == 1, x > y] 7161 >>> t = Then(t, Tactic('propagate-values')) 7165 t = _to_tactic(t, ctx)
7169 """Return a tactic that applies `t` to a given goal for `ms` milliseconds. 7171 If `t` does not terminate in `ms` milliseconds, then it fails. 7173 t = _to_tactic(t, ctx)
7177 """Return a list of all available tactics in Z3. 7180 >>> l.count('simplify') == 1 7187 """Return a short description for the tactic named `name`. 7189 >>> d = tactic_description('simplify') 7195 """Display a (tabular) description of all available tactics in Z3.""" 7198 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7201 print(
'<tr style="background-color:#CFCFCF">')
7206 print(
'<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(
tactic_description(t), 40)))
7213 """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.""" 7217 if isinstance(probe, ProbeObj):
7219 elif isinstance(probe, float):
7221 elif _is_int(probe):
7223 elif isinstance(probe, bool):
7230 _z3_assert(isinstance(probe, str),
"probe name expected")
7234 raise Z3Exception(
"unknown probe '%s'" % probe)
7238 if self.
probe is not None and self.
ctx.ref()
is not None:
7242 """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`. 7244 >>> p = Probe('size') < 10 7255 """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`. 7257 >>> p = Probe('size') > 10 7268 """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`. 7270 >>> p = Probe('size') <= 2 7281 """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`. 7283 >>> p = Probe('size') >= 2 7294 """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`. 7296 >>> p = Probe('size') == 2 7307 """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`. 7309 >>> p = Probe('size') != 2 7321 """Evaluate the probe `self` in the given goal. 7323 >>> p = Probe('size') 7333 >>> p = Probe('num-consts') 7336 >>> p = Probe('is-propositional') 7339 >>> p = Probe('is-qflia') 7344 _z3_assert(isinstance(goal, Goal)
or isinstance(goal, BoolRef),
"Z3 Goal or Boolean expression expected")
7345 goal = _to_goal(goal)
7349 """Return `True` if `p` is a Z3 probe. 7351 >>> is_probe(Int('x')) 7353 >>> is_probe(Probe('memory')) 7356 return isinstance(p, Probe)
7358 def _to_probe(p, ctx=None):
7362 return Probe(p, ctx)
7365 """Return a list of all available probes in Z3. 7368 >>> l.count('memory') == 1 7375 """Return a short description for the probe named `name`. 7377 >>> d = probe_description('memory') 7383 """Display a (tabular) description of all available probes in Z3.""" 7386 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7389 print(
'<tr style="background-color:#CFCFCF">')
7394 print(
'<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(
probe_description(p), 40)))
7400 def _probe_nary(f, args, ctx):
7402 _z3_assert(len(args) > 0,
"At least one argument expected")
7404 r = _to_probe(args[0], ctx)
7405 for i
in range(num - 1):
7406 r =
Probe(f(ctx.ref(), r.probe, _to_probe(args[i+1], ctx).probe), ctx)
7409 def _probe_and(args, ctx):
7410 return _probe_nary(Z3_probe_and, args, ctx)
7412 def _probe_or(args, ctx):
7413 return _probe_nary(Z3_probe_or, args, ctx)
7416 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 7418 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. 7420 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) 7421 >>> x, y = Ints('x y') 7427 >>> g.add(x == y + 1) 7429 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 7431 p = _to_probe(p, ctx)
7435 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 7437 >>> t = When(Probe('size') > 2, Tactic('simplify')) 7438 >>> x, y = Ints('x y') 7444 >>> g.add(x == y + 1) 7446 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 7448 p = _to_probe(p, ctx)
7449 t = _to_tactic(t, ctx)
7453 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. 7455 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt')) 7457 p = _to_probe(p, ctx)
7458 t1 = _to_tactic(t1, ctx)
7459 t2 = _to_tactic(t2, ctx)
7469 """Simplify the expression `a` using the given options. 7471 This function has many options. Use `help_simplify` to obtain the complete list. 7475 >>> simplify(x + 1 + y + x + 1) 7477 >>> simplify((x + 1)*(y + 1), som=True) 7479 >>> simplify(Distinct(x, y, 1), blast_distinct=True) 7480 And(Not(x == y), Not(x == 1), Not(y == 1)) 7481 >>> simplify(And(x == 0, y == 1), elim_and=True) 7482 Not(Or(Not(x == 0), Not(y == 1))) 7485 _z3_assert(
is_expr(a),
"Z3 expression expected")
7486 if len(arguments) > 0
or len(keywords) > 0:
7488 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
7490 return _to_expr_ref(
Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
7493 """Return a string describing all options available for Z3 `simplify` procedure.""" 7497 """Return the set of parameter descriptions for Z3 `simplify` procedure.""" 7501 """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. 7505 >>> substitute(x + 1, (x, y + 1)) 7507 >>> f = Function('f', IntSort(), IntSort()) 7508 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 7511 if isinstance(m, tuple):
7513 if isinstance(m1, list):
7516 _z3_assert(
is_expr(t),
"Z3 expression expected")
7517 _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.")
7519 _from = (Ast * num)()
7521 for i
in range(num):
7522 _from[i] = m[i][0].as_ast()
7523 _to[i] = m[i][1].as_ast()
7524 return _to_expr_ref(
Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
7527 """Substitute the free variables in t with the expression in m. 7529 >>> v0 = Var(0, IntSort()) 7530 >>> v1 = Var(1, IntSort()) 7532 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 7533 >>> # replace v0 with x+1 and v1 with x 7534 >>> substitute_vars(f(v0, v1), x + 1, x) 7538 _z3_assert(
is_expr(t),
"Z3 expression expected")
7539 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
7542 for i
in range(num):
7543 _to[i] = m[i].as_ast()
7547 """Create the sum of the Z3 expressions. 7549 >>> a, b, c = Ints('a b c') 7554 >>> A = IntVector('a', 5) 7556 a__0 + a__1 + a__2 + a__3 + a__4 7558 args = _get_args(args)
7561 ctx = _ctx_from_ast_arg_list(args)
7563 return _reduce(
lambda a, b: a + b, args, 0)
7564 args = _coerce_expr_list(args, ctx)
7566 return _reduce(
lambda a, b: a + b, args, 0)
7568 _args, sz = _to_ast_array(args)
7573 """Create the product of the Z3 expressions. 7575 >>> a, b, c = Ints('a b c') 7576 >>> Product(a, b, c) 7578 >>> Product([a, b, c]) 7580 >>> A = IntVector('a', 5) 7582 a__0*a__1*a__2*a__3*a__4 7584 args = _get_args(args)
7587 ctx = _ctx_from_ast_arg_list(args)
7589 return _reduce(
lambda a, b: a * b, args, 1)
7590 args = _coerce_expr_list(args, ctx)
7592 return _reduce(
lambda a, b: a * b, args, 1)
7594 _args, sz = _to_ast_array(args)
7598 """Create an at-most Pseudo-Boolean k constraint. 7600 >>> a, b, c = Bools('a b c') 7601 >>> f = AtMost(a, b, c, 2) 7603 args = _get_args(args)
7605 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
7606 ctx = _ctx_from_ast_arg_list(args)
7608 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
7609 args1 = _coerce_expr_list(args[:-1], ctx)
7611 _args, sz = _to_ast_array(args1)
7612 return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
7615 """Create an at-most Pseudo-Boolean k constraint. 7617 >>> a, b, c = Bools('a b c') 7618 >>> f = AtLeast(a, b, c, 2) 7625 args = _get_args(args)
7627 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
7628 ctx = _ctx_from_ast_arg_list(args)
7630 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
7631 args1 = _coerce_expr_list(args[:-1], ctx)
7632 args1 = [ mk_not(a)
for a
in args1 ]
7633 k = len(args1) - args[-1]
7634 _args, sz = _to_ast_array(args1)
7635 return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
7638 """Create a Pseudo-Boolean inequality k constraint. 7640 >>> a, b, c = Bools('a b c') 7641 >>> f = PbLe(((a,1),(b,3),(c,2)), 3) 7643 args = _get_args(args)
7644 args, coeffs = zip(*args)
7646 _z3_assert(len(args) > 0,
"Non empty list of arguments expected")
7647 ctx = _ctx_from_ast_arg_list(args)
7649 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
7650 args = _coerce_expr_list(args, ctx)
7651 _args, sz = _to_ast_array(args)
7652 _coeffs = (ctypes.c_int * len(coeffs))()
7653 for i
in range(len(coeffs)):
7654 _coeffs[i] = coeffs[i]
7655 return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
7658 """Create a Pseudo-Boolean inequality k constraint. 7660 >>> a, b, c = Bools('a b c') 7661 >>> f = PbEq(((a,1),(b,3),(c,2)), 3) 7663 args = _get_args(args)
7664 args, coeffs = zip(*args)
7666 _z3_assert(len(args) > 0,
"Non empty list of arguments expected")
7667 ctx = _ctx_from_ast_arg_list(args)
7669 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
7670 args = _coerce_expr_list(args, ctx)
7671 _args, sz = _to_ast_array(args)
7672 _coeffs = (ctypes.c_int * len(coeffs))()
7673 for i
in range(len(coeffs)):
7674 _coeffs[i] = coeffs[i]
7675 return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
7679 """Solve the constraints `*args`. 7681 This is a simple function for creating demonstrations. It creates a solver, 7682 configure it using the options in `keywords`, adds the constraints 7683 in `args`, and invokes check. 7686 >>> solve(a > 0, a < 2) 7692 if keywords.get(
'show',
False):
7696 print(
"no solution")
7698 print(
"failed to solve")
7707 """Solve the constraints `*args` using solver `s`. 7709 This is a simple function for creating demonstrations. It is similar to `solve`, 7710 but it uses the given solver `s`. 7711 It configures solver `s` using the options in `keywords`, adds the constraints 7712 in `args`, and invokes check. 7715 _z3_assert(isinstance(s, Solver),
"Solver object expected")
7718 if keywords.get(
'show',
False):
7723 print(
"no solution")
7725 print(
"failed to solve")
7731 if keywords.get(
'show',
False):
7736 """Try to prove the given claim. 7738 This is a simple function for creating demonstrations. It tries to prove 7739 `claim` by showing the negation is unsatisfiable. 7741 >>> p, q = Bools('p q') 7742 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) 7746 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
7750 if keywords.get(
'show',
False):
7756 print(
"failed to prove")
7759 print(
"counterexample")
7762 def _solve_html(*args, **keywords):
7763 """Version of funcion `solve` used in RiSE4Fun.""" 7767 if keywords.get(
'show',
False):
7768 print(
"<b>Problem:</b>")
7772 print(
"<b>no solution</b>")
7774 print(
"<b>failed to solve</b>")
7780 if keywords.get(
'show',
False):
7781 print(
"<b>Solution:</b>")
7784 def _solve_using_html(s, *args, **keywords):
7785 """Version of funcion `solve_using` used in RiSE4Fun.""" 7787 _z3_assert(isinstance(s, Solver),
"Solver object expected")
7790 if keywords.get(
'show',
False):
7791 print(
"<b>Problem:</b>")
7795 print(
"<b>no solution</b>")
7797 print(
"<b>failed to solve</b>")
7803 if keywords.get(
'show',
False):
7804 print(
"<b>Solution:</b>")
7807 def _prove_html(claim, **keywords):
7808 """Version of funcion `prove` used in RiSE4Fun.""" 7810 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
7814 if keywords.get(
'show',
False):
7818 print(
"<b>proved</b>")
7820 print(
"<b>failed to prove</b>")
7823 print(
"<b>counterexample</b>")
7826 def _dict2sarray(sorts, ctx):
7828 _names = (Symbol * sz)()
7829 _sorts = (Sort * sz) ()
7834 _z3_assert(isinstance(k, str),
"String expected")
7835 _z3_assert(
is_sort(v),
"Z3 sort expected")
7839 return sz, _names, _sorts
7841 def _dict2darray(decls, ctx):
7843 _names = (Symbol * sz)()
7844 _decls = (FuncDecl * sz) ()
7849 _z3_assert(isinstance(k, str),
"String expected")
7853 _decls[i] = v.decl().ast
7857 return sz, _names, _decls
7860 """Parse a string in SMT 2.0 format using the given sorts and decls. 7862 The arguments sorts and decls are Python dictionaries used to initialize 7863 the symbol table used for the SMT 2.0 parser. 7865 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') 7867 >>> x, y = Ints('x y') 7868 >>> f = Function('f', IntSort(), IntSort()) 7869 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) 7871 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) 7875 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
7876 dsz, dnames, ddecls = _dict2darray(decls, ctx)
7880 """Parse a file in SMT 2.0 format using the given sorts and decls. 7882 This function is similar to parse_smt2_string(). 7885 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
7886 dsz, dnames, ddecls = _dict2darray(decls, ctx)
7887 return _to_expr_ref(
Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
7890 """Create an interpolation operator. 7892 The argument is an interpolation pattern (see tree_interpolant). 7895 >>> print(Interpolant(x>0)) 7898 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
7904 """Compute interpolant for a tree of formulas. 7906 The input is an interpolation pattern over a set of formulas C. 7907 The pattern pat is a formula combining the formulas in C using 7908 logical conjunction and the "interp" operator (see Interp). This 7909 interp operator is logically the identity operator. It marks the 7910 sub-formulas of the pattern for which interpolants should be 7911 computed. The interpolant is a map sigma from marked subformulas 7912 to formulas, such that, for each marked subformula phi of pat 7913 (where phi sigma is phi with sigma(psi) substituted for each 7914 subformula psi of phi such that psi in dom(sigma)): 7916 1) phi sigma implies sigma(phi), and 7918 2) sigma(phi) is in the common uninterpreted vocabulary between 7919 the formulas of C occurring in phi and those not occurring in 7922 and moreover pat sigma implies false. In the simplest case 7923 an interpolant for the pattern "(and (interp A) B)" maps A 7924 to an interpolant for A /\ B. 7926 The return value is a vector of formulas representing sigma. This 7927 vector contains sigma(phi) for each marked subformula of pat, in 7928 pre-order traversal. This means that subformulas of phi occur before phi 7929 in the vector. Also, subformulas that occur multiply in pat will 7930 occur multiply in the result vector. 7932 If pat is satisfiable, raises an object of class ModelRef 7933 that represents a model of pat. 7935 If neither a proof of unsatisfiability nor a model is obtained 7936 (for example, because of a timeout, or because models are disabled) 7937 then None is returned. 7939 If parameters p are supplied, these are used in creating the 7940 solver that determines satisfiability. 7944 >>> print(tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))) 7945 [Not(x >= 0), Not(y <= 2)] 7947 # >>> g = And(Interpolant(x<0),x<2) 7949 # ... print tree_interpolant(g).sexpr() 7950 # ... except ModelRef as m: 7951 # ... print m.sexpr() 7952 (define-fun x () Int 7956 ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
7957 ptr = (AstVectorObj * 1)()
7958 mptr = (Model * 1)()
7962 if res == Z3_L_FALSE:
7969 """Compute an interpolant for a binary conjunction. 7971 If a & b is unsatisfiable, returns an interpolant for a & b. 7972 This is a formula phi such that 7975 2) b implies not phi 7976 3) All the uninterpreted symbols of phi occur in both a and b. 7978 If a & b is satisfiable, raises an object of class ModelRef 7979 that represents a model of a &b. 7981 If neither a proof of unsatisfiability nor a model is obtained 7982 (for example, because of a timeout, or because models are disabled) 7983 then None is returned. 7985 If parameters p are supplied, these are used in creating the 7986 solver that determines satisfiability. 7989 print(binary_interpolant(x<0,x>2)) 7994 return ti[0]
if ti
is not None else None 7997 """Compute interpolant for a sequence of formulas. 7999 If len(v) == N, and if the conjunction of the formulas in v is 8000 unsatisfiable, the interpolant is a sequence of formulas w 8001 such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1: 8003 1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N) 8004 2) All uninterpreted symbols in w[i] occur in both v[0]..v[i] 8007 Requires len(v) >= 1. 8009 If a & b is satisfiable, raises an object of class ModelRef 8010 that represents a model of a & b. 8012 If neither a proof of unsatisfiability nor a model is obtained 8013 (for example, because of a timeout, or because models are disabled) 8014 then None is returned. 8016 If parameters p are supplied, these are used in creating the 8017 solver that determines satisfiability. 8021 >>> print(sequence_interpolant([x < 0, y == x , y > 2])) 8022 [Not(x >= 0), Not(y >= 0)] 8025 for i
in range(1,len(v)):
8038 _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO
8039 _dflt_fpsort_ebits = 11
8040 _dflt_fpsort_sbits = 53
8043 """Retrieves the global default rounding mode.""" 8044 global _dflt_rounding_mode
8045 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
8047 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
8049 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
8051 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
8053 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
8057 global _dflt_rounding_mode
8059 _dflt_rounding_mode = rm.decl().kind()
8061 _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO
or 8062 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE
or 8063 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE
or 8064 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
or 8065 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
8066 "illegal rounding mode")
8067 _dflt_rounding_mode = rm
8070 return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
8073 global _dflt_fpsort_ebits
8074 global _dflt_fpsort_sbits
8075 _dflt_fpsort_ebits = ebits
8076 _dflt_fpsort_sbits = sbits
8078 def _dflt_rm(ctx=None):
8081 def _dflt_fps(ctx=None):
8084 def _coerce_fp_expr_list(alist, ctx):
8085 first_fp_sort =
None 8088 if first_fp_sort
is None:
8089 first_fp_sort = a.sort()
8090 elif first_fp_sort == a.sort():
8095 first_fp_sort =
None 8099 for i
in range(len(alist)):
8101 if (isinstance(a, str)
and a.contains(
'2**(')
and a.endswith(
')'))
or _is_int(a)
or isinstance(a, float)
or isinstance(a, bool):
8102 r.append(
FPVal(a,
None, first_fp_sort, ctx))
8105 return _coerce_expr_list(r, ctx)
8111 """Floating-point sort.""" 8114 """Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`. 8115 >>> b = FPSort(8, 24) 8122 """Retrieves the number of bits reserved for the significand in the FloatingPoint sort `self`. 8123 >>> b = FPSort(8, 24) 8130 """Try to cast `val` as a floating-point expression. 8131 >>> b = FPSort(8, 24) 8134 >>> b.cast(1.0).sexpr() 8135 '(fp #b0 #x7f #b00000000000000000000000)' 8139 _z3_assert(self.
ctx == val.ctx,
"Context mismatch")
8142 return FPVal(val,
None, self, self.
ctx)
8146 """Floating-point 16-bit (half) sort.""" 8151 """Floating-point 16-bit (half) sort.""" 8156 """Floating-point 32-bit (single) sort.""" 8161 """Floating-point 32-bit (single) sort.""" 8166 """Floating-point 64-bit (double) sort.""" 8171 """Floating-point 64-bit (double) sort.""" 8176 """Floating-point 128-bit (quadruple) sort.""" 8181 """Floating-point 128-bit (quadruple) sort.""" 8186 """"Floating-point rounding mode sort.""" 8190 """Return True if `s` is a Z3 floating-point sort. 8192 >>> is_fp_sort(FPSort(8, 24)) 8194 >>> is_fp_sort(IntSort()) 8197 return isinstance(s, FPSortRef)
8200 """Return True if `s` is a Z3 floating-point rounding mode sort. 8202 >>> is_fprm_sort(FPSort(8, 24)) 8204 >>> is_fprm_sort(RNE().sort()) 8207 return isinstance(s, FPRMSortRef)
8212 """Floating-point expressions.""" 8215 """Return the sort of the floating-point expression `self`. 8217 >>> x = FP('1.0', FPSort(8, 24)) 8220 >>> x.sort() == FPSort(8, 24) 8226 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`. 8227 >>> b = FPSort(8, 24) 8234 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`. 8235 >>> b = FPSort(8, 24) 8242 """Return a Z3 floating point expression as a Python string.""" 8246 return fpLEQ(self, other, self.
ctx)
8249 return fpLT(self, other, self.
ctx)
8252 return fpGEQ(self, other, self.
ctx)
8255 return fpGT(self, other, self.
ctx)
8258 """Create the Z3 expression `self + other`. 8260 >>> x = FP('x', FPSort(8, 24)) 8261 >>> y = FP('y', FPSort(8, 24)) 8267 [a, b] = _coerce_fp_expr_list([self, other], self.
ctx)
8268 return fpAdd(_dflt_rm(), a, b, self.
ctx)
8271 """Create the Z3 expression `other + self`. 8273 >>> x = FP('x', FPSort(8, 24)) 8277 [a, b] = _coerce_fp_expr_list([other, self], self.
ctx)
8278 return fpAdd(_dflt_rm(), a, b, self.
ctx)
8281 """Create the Z3 expression `self - other`. 8283 >>> x = FP('x', FPSort(8, 24)) 8284 >>> y = FP('y', FPSort(8, 24)) 8290 [a, b] = _coerce_fp_expr_list([self, other], self.
ctx)
8291 return fpSub(_dflt_rm(), a, b, self.
ctx)
8294 """Create the Z3 expression `other - self`. 8296 >>> x = FP('x', FPSort(8, 24)) 8300 [a, b] = _coerce_fp_expr_list([other, self], self.
ctx)
8301 return fpSub(_dflt_rm(), a, b, self.
ctx)
8304 """Create the Z3 expression `self * other`. 8306 >>> x = FP('x', FPSort(8, 24)) 8307 >>> y = FP('y', FPSort(8, 24)) 8315 [a, b] = _coerce_fp_expr_list([self, other], self.
ctx)
8316 return fpMul(_dflt_rm(), a, b, self.
ctx)
8319 """Create the Z3 expression `other * self`. 8321 >>> x = FP('x', FPSort(8, 24)) 8322 >>> y = FP('y', FPSort(8, 24)) 8328 [a, b] = _coerce_fp_expr_list([other, self], self.
ctx)
8329 return fpMul(_dflt_rm(), a, b, self.
ctx)
8332 """Create the Z3 expression `+self`.""" 8336 """Create the Z3 expression `-self`. 8338 >>> x = FP('x', Float32()) 8345 """Create the Z3 expression `self / other`. 8347 >>> x = FP('x', FPSort(8, 24)) 8348 >>> y = FP('y', FPSort(8, 24)) 8356 [a, b] = _coerce_fp_expr_list([self, other], self.
ctx)
8357 return fpDiv(_dflt_rm(), a, b, self.
ctx)
8360 """Create the Z3 expression `other / self`. 8362 >>> x = FP('x', FPSort(8, 24)) 8363 >>> y = FP('y', FPSort(8, 24)) 8369 [a, b] = _coerce_fp_expr_list([other, self], self.
ctx)
8370 return fpDiv(_dflt_rm(), a, b, self.
ctx)
8372 if not sys.version <
'3':
8374 """Create the Z3 expression division `self / other`.""" 8378 """Create the Z3 expression division `other / self`.""" 8382 """Create the Z3 expression mod `self % other`.""" 8383 return fpRem(self, other)
8386 """Create the Z3 expression mod `other % self`.""" 8387 return fpRem(other, self)
8390 """Floating-point rounding mode expressions""" 8393 """Return a Z3 floating point expression as a Python string.""" 8438 """Return `True` if `a` is a Z3 floating-point rounding mode expression. 8447 return isinstance(a, FPRMRef)
8450 """Return `True` if `a` is a Z3 floating-point rounding mode numeral value.""" 8451 return is_fprm(a)
and _is_numeral(a.ctx, a.ast)
8457 return self.
decl().kind() == Z3_OP_FPA_NAN
8460 return self.
decl().kind() == Z3_OP_FPA_PLUS_INF
or self.
decl().kind() == Z3_OP_FPA_MINUS_INF
8463 return self.
decl().kind() == Z3_OP_FPA_PLUS_ZERO
or self.
decl().kind() == Z3_OP_FPA_MINUS_ZERO
8466 k = self.
decl().kind()
8467 return (self.
num_args() == 0
and (k == Z3_OP_FPA_MINUS_INF
or k == Z3_OP_FPA_MINUS_ZERO))
or (self.
sign() ==
True)
8470 The sign of the numeral. 8472 >>> x = FPNumRef(+1.0, FPSort(8, 24)) 8475 >>> x = FPNumRef(-1.0, FPSort(8, 24)) 8480 l = (ctypes.c_int)()
8482 raise Z3Exception(
"error retrieving the sign of a numeral.")
8486 The significand of the numeral. 8488 >>> x = FPNumRef(2.5, FPSort(8, 24)) 8496 The exponent of the numeral. 8498 >>> x = FPNumRef(2.5, FPSort(8, 24)) 8506 The exponent of the numeral as a long. 8508 >>> x = FPNumRef(2.5, FPSort(8, 24)) 8509 >>> x.exponent_as_long() 8513 ptr = (ctypes.c_longlong * 1)()
8515 raise Z3Exception(
"error retrieving the exponent of a numeral.")
8519 The string representation of the numeral. 8521 >>> x = FPNumRef(20, FPSort(8, 24)) 8526 s = Z3_fpa_get_numeral_string(self.
ctx.ref(), self.
as_ast())
8527 return (
"FPVal(%s, %s)" % (s, self.
sort()))
8530 """Return `True` if `a` is a Z3 floating-point expression. 8532 >>> b = FP('b', FPSort(8, 24)) 8540 return isinstance(a, FPRef)
8543 """Return `True` if `a` is a Z3 floating-point numeral value. 8545 >>> b = FP('b', FPSort(8, 24)) 8548 >>> b = FPVal(1.0, FPSort(8, 24)) 8554 return is_fp(a)
and _is_numeral(a.ctx, a.ast)
8557 """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used. 8559 >>> Single = FPSort(8, 24) 8560 >>> Double = FPSort(11, 53) 8563 >>> x = Const('x', Single) 8564 >>> eq(x, FP('x', FPSort(8, 24))) 8570 def _to_float_str(val, exp=0):
8571 if isinstance(val, float):
8575 sone = math.copysign(1.0, val)
8580 elif val == float(
"+inf"):
8582 elif val == float(
"-inf"):
8585 v = val.as_integer_ratio()
8588 rvs = str(num) +
'/' + str(den)
8589 res = rvs +
'p' + _to_int_str(exp)
8590 elif isinstance(val, bool):
8597 elif isinstance(val, str):
8598 inx = val.find(
'*(2**')
8601 elif val[-1] ==
')':
8603 exp = str(int(val[inx+5:-1]) + int(exp))
8605 _z3_assert(
False,
"String does not have floating-point numeral form.")
8607 _z3_assert(
False,
"Python value cannot be used to create floating-point numerals.")
8611 return res +
'p' + exp
8615 """Create a Z3 floating-point NaN term. 8617 >>> s = FPSort(8, 24) 8618 >>> set_fpa_pretty(True) 8621 >>> pb = get_fpa_pretty() 8622 >>> set_fpa_pretty(False) 8624 fpNaN(FPSort(8, 24)) 8625 >>> set_fpa_pretty(pb) 8627 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
8631 """Create a Z3 floating-point +oo term. 8633 >>> s = FPSort(8, 24) 8634 >>> pb = get_fpa_pretty() 8635 >>> set_fpa_pretty(True) 8636 >>> fpPlusInfinity(s) 8638 >>> set_fpa_pretty(False) 8639 >>> fpPlusInfinity(s) 8640 fpPlusInfinity(FPSort(8, 24)) 8641 >>> set_fpa_pretty(pb) 8643 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
8647 """Create a Z3 floating-point -oo term.""" 8648 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
8652 """Create a Z3 floating-point +oo or -oo term.""" 8653 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
8654 _z3_assert(isinstance(negative, bool),
"expected Boolean flag")
8658 """Create a Z3 floating-point +0.0 term.""" 8659 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
8663 """Create a Z3 floating-point -0.0 term.""" 8664 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
8668 """Create a Z3 floating-point +0.0 or -0.0 term.""" 8669 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
8670 _z3_assert(isinstance(negative, bool),
"expected Boolean flag")
8673 def FPVal(sig, exp=None, fps=None, ctx=None):
8674 """Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used. 8676 >>> v = FPVal(20.0, FPSort(8, 24)) 8679 >>> print("0x%.8x" % v.exponent_as_long()) 8681 >>> v = FPVal(2.25, FPSort(8, 24)) 8684 >>> v = FPVal(-2.25, FPSort(8, 24)) 8687 >>> FPVal(-0.0, FPSort(8, 24)) 8689 >>> FPVal(0.0, FPSort(8, 24)) 8691 >>> FPVal(+0.0, FPSort(8, 24)) 8699 fps = _dflt_fps(ctx)
8703 val = _to_float_str(sig)
8704 if val ==
"NaN" or val ==
"nan":
8708 elif val ==
"0.0" or val ==
"+0.0":
8710 elif val ==
"+oo" or val ==
"+inf" or val ==
"+Inf":
8712 elif val ==
"-oo" or val ==
"-inf" or val ==
"-Inf":
8715 return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
8717 def FP(name, fpsort, ctx=None):
8718 """Return a floating-point constant named `name`. 8719 `fpsort` is the floating-point sort. 8720 If `ctx=None`, then the global context is used. 8722 >>> x = FP('x', FPSort(8, 24)) 8729 >>> word = FPSort(8, 24) 8730 >>> x2 = FP('x', word) 8734 if isinstance(fpsort, FPSortRef)
and ctx
is None:
8740 def FPs(names, fpsort, ctx=None):
8741 """Return an array of floating-point constants. 8743 >>> x, y, z = FPs('x y z', FPSort(8, 24)) 8750 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) 8751 fpMul(RNE(), fpAdd(RNE(), x, y), z) 8754 if isinstance(names, str):
8755 names = names.split(
" ")
8756 return [
FP(name, fpsort, ctx)
for name
in names]
8759 """Create a Z3 floating-point absolute value expression. 8761 >>> s = FPSort(8, 24) 8763 >>> x = FPVal(1.0, s) 8766 >>> y = FPVal(-20.0, s) 8771 >>> fpAbs(-1.25*(2**4)) 8777 [a] = _coerce_fp_expr_list([a], ctx)
8781 """Create a Z3 floating-point addition expression. 8783 >>> s = FPSort(8, 24) 8792 [a] = _coerce_fp_expr_list([a], ctx)
8795 def _mk_fp_unary(f, rm, a, ctx):
8797 [a] = _coerce_fp_expr_list([a], ctx)
8799 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
8800 _z3_assert(
is_fp(a),
"Second argument must be a Z3 floating-point expression")
8801 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx)
8803 def _mk_fp_unary_norm(f, a, ctx):
8805 [a] = _coerce_fp_expr_list([a], ctx)
8807 _z3_assert(
is_fp(a),
"First argument must be a Z3 floating-point expression")
8808 return FPRef(f(ctx.ref(), a.as_ast()), ctx)
8810 def _mk_fp_unary_pred(f, a, ctx):
8812 [a] = _coerce_fp_expr_list([a], ctx)
8814 _z3_assert(
is_fp(a)
or is_fp(b),
"Second or third argument must be a Z3 floating-point expression")
8815 return BoolRef(f(ctx.ref(), a.as_ast()), ctx)
8817 def _mk_fp_bin(f, rm, a, b, ctx):
8819 [a, b] = _coerce_fp_expr_list([a, b], ctx)
8821 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
8822 _z3_assert(
is_fp(a)
or is_fp(b),
"Second or third argument must be a Z3 floating-point expression")
8823 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx)
8825 def _mk_fp_bin_norm(f, a, b, ctx):
8827 [a, b] = _coerce_fp_expr_list([a, b], ctx)
8829 _z3_assert(
is_fp(a)
or is_fp(b),
"First or second argument must be a Z3 floating-point expression")
8830 return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
8832 def _mk_fp_bin_pred(f, a, b, ctx):
8834 [a, b] = _coerce_fp_expr_list([a, b], ctx)
8836 _z3_assert(
is_fp(a)
or is_fp(b),
"Second or third argument must be a Z3 floating-point expression")
8837 return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
8839 def _mk_fp_tern(f, rm, a, b, c, ctx):
8841 [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx)
8843 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
8844 _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")
8845 return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
8848 """Create a Z3 floating-point addition expression. 8850 >>> s = FPSort(8, 24) 8856 >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ 8858 >>> fpAdd(rm, x, y).sort() 8861 return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
8864 """Create a Z3 floating-point subtraction expression. 8866 >>> s = FPSort(8, 24) 8872 >>> fpSub(rm, x, y).sort() 8875 return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
8878 """Create a Z3 floating-point multiplication expression. 8880 >>> s = FPSort(8, 24) 8886 >>> fpMul(rm, x, y).sort() 8889 return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
8892 """Create a Z3 floating-point divison expression. 8894 >>> s = FPSort(8, 24) 8900 >>> fpDiv(rm, x, y).sort() 8903 return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
8906 """Create a Z3 floating-point remainder expression. 8908 >>> s = FPSort(8, 24) 8913 >>> fpRem(x, y).sort() 8916 return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
8919 """Create a Z3 floating-point minimium expression. 8921 >>> s = FPSort(8, 24) 8927 >>> fpMin(x, y).sort() 8930 return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
8933 """Create a Z3 floating-point maximum expression. 8935 >>> s = FPSort(8, 24) 8941 >>> fpMax(x, y).sort() 8944 return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
8947 """Create a Z3 floating-point fused multiply-add expression. 8949 return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
8952 """Create a Z3 floating-point square root expression. 8954 return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
8957 """Create a Z3 floating-point roundToIntegral expression. 8959 return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
8962 """Create a Z3 floating-point isNaN expression. 8964 >>> s = FPSort(8, 24) 8970 return _mk_fp_unary_norm(Z3_mk_fpa_is_nan, a, ctx)
8973 """Create a Z3 floating-point isInfinite expression. 8975 >>> s = FPSort(8, 24) 8980 return _mk_fp_unary_norm(Z3_mk_fpa_is_infinite, a, ctx)
8983 """Create a Z3 floating-point isZero expression. 8985 return _mk_fp_unary_norm(Z3_mk_fpa_is_zero, a, ctx)
8988 """Create a Z3 floating-point isNormal expression. 8990 return _mk_fp_unary_norm(Z3_mk_fpa_is_normal, a, ctx)
8993 """Create a Z3 floating-point isSubnormal expression. 8995 return _mk_fp_unary_norm(Z3_mk_fpa_is_subnormal, a, ctx)
8998 """Create a Z3 floating-point isNegative expression. 9000 return _mk_fp_unary_norm(Z3_mk_fpa_is_negative, a, ctx)
9003 """Create a Z3 floating-point isPositive expression. 9005 return _mk_fp_unary_norm(Z3_mk_fpa_is_positive, a, ctx)
9008 def _check_fp_args(a, b):
9010 _z3_assert(
is_fp(a)
or is_fp(b),
"At least one of the arguments must be a Z3 floating-point expression")
9013 """Create the Z3 floating-point expression `other < self`. 9015 >>> x, y = FPs('x y', FPSort(8, 24)) 9021 return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
9024 """Create the Z3 floating-point expression `other <= self`. 9026 >>> x, y = FPs('x y', FPSort(8, 24)) 9029 >>> (x <= y).sexpr() 9032 return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
9035 """Create the Z3 floating-point expression `other > self`. 9037 >>> x, y = FPs('x y', FPSort(8, 24)) 9043 return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
9046 """Create the Z3 floating-point expression `other >= self`. 9048 >>> x, y = FPs('x y', FPSort(8, 24)) 9051 >>> (x >= y).sexpr() 9054 return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
9057 """Create the Z3 floating-point expression `fpEQ(other, self)`. 9059 >>> x, y = FPs('x y', FPSort(8, 24)) 9062 >>> fpEQ(x, y).sexpr() 9065 return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
9068 """Create the Z3 floating-point expression `Not(fpEQ(other, self))`. 9070 >>> x, y = FPs('x y', FPSort(8, 24)) 9073 >>> (x != y).sexpr() 9079 """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp. 9081 >>> s = FPSort(8, 24) 9082 >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23)) 9084 fpFP(1, 127, 4194304) 9085 >>> xv = FPVal(-1.5, s) 9089 >>> slvr.add(fpEQ(x, xv)) 9092 >>> xv = FPVal(+1.5, s) 9096 >>> slvr.add(fpEQ(x, xv)) 9101 _z3_assert(sgn.sort().size() == 1,
"sort mismatch")
9103 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx,
"context mismatch")
9107 """Create a Z3 floating-point conversion expression from other term sorts 9110 From a bit-vector term in IEEE 754-2008 format: 9111 >>> x = FPVal(1.0, Float32()) 9112 >>> x_bv = fpToIEEEBV(x) 9113 >>> simplify(fpToFP(x_bv, Float32())) 9116 From a floating-point term with different precision: 9117 >>> x = FPVal(1.0, Float32()) 9118 >>> x_db = fpToFP(RNE(), x, Float64()) 9123 >>> x_r = RealVal(1.5) 9124 >>> simplify(fpToFP(RNE(), x_r, Float32())) 9127 From a signed bit-vector term: 9128 >>> x_signed = BitVecVal(-5, BitVecSort(32)) 9129 >>> simplify(fpToFP(RNE(), x_signed, Float32())) 9142 raise Z3Exception(
"Unsupported combination of arguments for conversion to floating-point term.")
9145 """Create a Z3 floating-point conversion expression that represents the 9146 conversion from a bit-vector term to a floating-point term. 9148 >>> x_bv = BitVecVal(0x3F800000, 32) 9149 >>> x_fp = fpBVToFP(x_bv, Float32()) 9155 _z3_assert(
is_bv(v),
"First argument must be a Z3 floating-point rounding mode expression.")
9156 _z3_assert(
is_fp_sort(sort),
"Second argument must be a Z3 floating-point sort.")
9161 """Create a Z3 floating-point conversion expression that represents the 9162 conversion from a floating-point term to a floating-point term of different precision. 9164 >>> x_sgl = FPVal(1.0, Float32()) 9165 >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64()) 9173 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9174 _z3_assert(
is_fp(v),
"Second argument must be a Z3 floating-point expression.")
9175 _z3_assert(
is_fp_sort(sort),
"Third argument must be a Z3 floating-point sort.")
9180 """Create a Z3 floating-point conversion expression that represents the 9181 conversion from a real term to a floating-point term. 9183 >>> x_r = RealVal(1.5) 9184 >>> x_fp = fpRealToFP(RNE(), x_r, Float32()) 9190 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9191 _z3_assert(
is_real(v),
"Second argument must be a Z3 expression or real sort.")
9192 _z3_assert(
is_fp_sort(sort),
"Third argument must be a Z3 floating-point sort.")
9197 """Create a Z3 floating-point conversion expression that represents the 9198 conversion from a signed bit-vector term (encoding an integer) to a floating-point term. 9200 >>> x_signed = BitVecVal(-5, BitVecSort(32)) 9201 >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32()) 9203 fpToFP(RNE(), 4294967291) 9207 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9208 _z3_assert(
is_bv(v),
"Second argument must be a Z3 expression or real sort.")
9209 _z3_assert(
is_fp_sort(sort),
"Third argument must be a Z3 floating-point sort.")
9214 """Create a Z3 floating-point conversion expression that represents the 9215 conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term. 9217 >>> x_signed = BitVecVal(-5, BitVecSort(32)) 9218 >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32()) 9220 fpToFPUnsigned(RNE(), 4294967291) 9224 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9225 _z3_assert(
is_bv(v),
"Second argument must be a Z3 expression or real sort.")
9226 _z3_assert(
is_fp_sort(sort),
"Third argument must be a Z3 floating-point sort.")
9231 """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.""" 9233 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9234 _z3_assert(
is_bv(x),
"Second argument must be a Z3 bit-vector expression")
9235 _z3_assert(
is_fp_sort(s),
"Third argument must be Z3 floating-point sort")
9240 """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector. 9242 >>> x = FP('x', FPSort(8, 24)) 9243 >>> y = fpToSBV(RTZ(), x, BitVecSort(32)) 9254 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9255 _z3_assert(
is_fp(x),
"Second argument must be a Z3 floating-point expression")
9256 _z3_assert(
is_bv_sort(s),
"Third argument must be Z3 bit-vector sort")
9261 """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector. 9263 >>> x = FP('x', FPSort(8, 24)) 9264 >>> y = fpToUBV(RTZ(), x, BitVecSort(32)) 9275 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9276 _z3_assert(
is_fp(x),
"Second argument must be a Z3 floating-point expression")
9277 _z3_assert(
is_bv_sort(s),
"Third argument must be Z3 bit-vector sort")
9282 """Create a Z3 floating-point conversion expression, from floating-point expression to real. 9284 >>> x = FP('x', FPSort(8, 24)) 9288 >>> print(is_real(y)) 9292 >>> print(is_real(x)) 9296 _z3_assert(
is_fp(x),
"First argument must be a Z3 floating-point expression")
9301 """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. 9303 The size of the resulting bit-vector is automatically determined. 9305 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion 9306 knows only one NaN and it will always produce the same bit-vector represenatation of 9309 >>> x = FP('x', FPSort(8, 24)) 9310 >>> y = fpToIEEEBV(x) 9321 _z3_assert(
is_fp(x),
"First argument must be a Z3 floating-point expression")
9334 """Sequence sort.""" 9337 """Determine if sort is a string 9338 >>> s = StringSort() 9341 >>> s = SeqSort(IntSort()) 9345 return Z3_is_string_sort(self.
ctx_ref(), self.
ast)
9348 """Create a string sort 9349 >>> s = StringSort() 9354 return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx)
9358 """Create a sequence sort over elements provided in the argument 9359 >>> s = SeqSort(IntSort()) 9360 >>> s == Unit(IntVal(1)).sort() 9363 return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx)
9366 """Sequence expression.""" 9372 return Concat(self, other)
9375 return Concat(other, self)
9389 """Return a string representation of sequence expression.""" 9393 def _coerce_seq(s, ctx=None):
9394 if isinstance(s, str):
9398 raise Z3Exception(
"Non-expression passed as a sequence")
9400 raise Z3Exception(
"Non-sequence passed as a sequence")
9403 def _get_ctx2(a, b, ctx=None):
9413 """Return `True` if `a` is a Z3 sequence expression. 9414 >>> print (is_seq(Unit(IntVal(0)))) 9416 >>> print (is_seq(StringVal("abc"))) 9419 return isinstance(a, SeqRef)
9422 """Return `True` if `a` is a Z3 string expression. 9423 >>> print (is_string(StringVal("ab"))) 9426 return isinstance(a, SeqRef)
and a.is_string()
9429 """return 'True' if 'a' is a Z3 string constant expression. 9430 >>> print (is_string_value(StringVal("a"))) 9432 >>> print (is_string_value(StringVal("a") + StringVal("b"))) 9435 return isinstance(a, SeqRef)
and a.is_string_value()
9439 """create a string expression""" 9441 return SeqRef(Z3_mk_string(ctx.ref(), s), ctx)
9444 """Return a string constant named `name`. If `ctx=None`, then the global context is used. 9452 """Return a tuple of String constants. """ 9454 if isinstance(names, str):
9455 names = names.split(
" ")
9456 return [
String(name, ctx)
for name
in names]
9459 """Create the empty sequence of the given sort 9460 >>> e = Empty(StringSort()) 9463 >>> e2 = StringVal("") 9466 >>> e3 = Empty(SeqSort(IntSort())) 9470 return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
9473 """Create a singleton sequence""" 9474 return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx)
9477 """Check if 'a' is a prefix of 'b' 9478 >>> s1 = PrefixOf("ab", "abc") 9481 >>> s2 = PrefixOf("bc", "abc") 9485 ctx = _get_ctx2(a, b)
9486 a = _coerce_seq(a, ctx)
9487 b = _coerce_seq(b, ctx)
9488 return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
9491 """Check if 'a' is a suffix of 'b' 9492 >>> s1 = SuffixOf("ab", "abc") 9495 >>> s2 = SuffixOf("bc", "abc") 9499 ctx = _get_ctx2(a, b)
9500 a = _coerce_seq(a, ctx)
9501 b = _coerce_seq(b, ctx)
9502 return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
9505 """Check if 'a' contains 'b' 9506 >>> s1 = Contains("abc", "ab") 9509 >>> s2 = Contains("abc", "bc") 9512 >>> x, y, z = Strings('x y z') 9513 >>> s3 = Contains(Concat(x,y,z), y) 9517 ctx = _get_ctx2(a, b)
9518 a = _coerce_seq(a, ctx)
9519 b = _coerce_seq(b, ctx)
9520 return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
9524 """Replace the first occurrence of 'src' by 'dst' in 's' 9525 >>> r = Replace("aaa", "a", "b") 9529 ctx = _get_ctx2(dst, s)
9530 if ctx
is None and is_expr(src):
9532 src = _coerce_seq(src, ctx)
9533 dst = _coerce_seq(dst, ctx)
9534 s = _coerce_seq(s, ctx)
9535 return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx)
9541 """Retrieve the index of substring within a string starting at a specified offset. 9542 >>> simplify(IndexOf("abcabc", "bc", 0)) 9544 >>> simplify(IndexOf("abcabc", "bc", 2)) 9550 ctx = _get_ctx2(s, substr, ctx)
9551 s = _coerce_seq(s, ctx)
9552 substr = _coerce_seq(substr, ctx)
9554 offset =
IntVal(offset, ctx)
9555 return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
9558 """Obtain the length of a sequence 's' 9559 >>> l = Length(StringVal("abc")) 9564 return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
9567 """The regular expression that accepts sequence 's' 9569 >>> s2 = Re(StringVal("ab")) 9570 >>> s3 = Re(Unit(BoolVal(True))) 9572 s = _coerce_seq(s, ctx)
9573 return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx)
9581 """Regular expression sort.""" 9586 return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.as_ast()), ctx)
9587 if s
is None or isinstance(s, Context):
9589 return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), ctx)
9590 raise Z3Exception(
"Regular expression sort constructor expects either a string or a context or no argument")
9594 """Regular expressions.""" 9597 return Union(self, other)
9601 return isinstance(s, ReRef)
9605 """Create regular expression membership test 9606 >>> re = Union(Re("a"),Re("b")) 9607 >>> print (simplify(InRe("a", re))) 9609 >>> print (simplify(InRe("b", re))) 9611 >>> print (simplify(InRe("c", re))) 9614 s = _coerce_seq(s, re.ctx)
9615 return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
9618 """Create union of regular expressions. 9619 >>> re = Union(Re("a"), Re("b"), Re("c")) 9620 >>> print (simplify(InRe("d", re))) 9623 args = _get_args(args)
9626 _z3_assert(sz > 0,
"At least one argument expected.")
9627 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
9633 v[i] = args[i].as_ast()
9634 return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx)
9637 """Create the regular expression accepting one or more repetitions of argument. 9638 >>> re = Plus(Re("a")) 9639 >>> print(simplify(InRe("aa", re))) 9641 >>> print(simplify(InRe("ab", re))) 9643 >>> print(simplify(InRe("", re))) 9646 return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)
9649 """Create the regular expression that optionally accepts the argument. 9650 >>> re = Option(Re("a")) 9651 >>> print(simplify(InRe("a", re))) 9653 >>> print(simplify(InRe("", re))) 9655 >>> print(simplify(InRe("aa", re))) 9658 return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)
9661 """Create the regular expression accepting zero or more repetitions of argument. 9662 >>> re = Star(Re("a")) 9663 >>> print(simplify(InRe("aa", re))) 9665 >>> print(simplify(InRe("ab", re))) 9667 >>> print(simplify(InRe("", re))) 9670 return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
def translate(self, target)
def __rrshift__(self, other)
Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i)
Return the name of the i probe.
def fpToIEEEBV(x, ctx=None)
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
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_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
def __init__(self, entry, ctx)
Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1)
Coerce a real to an integer.
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
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 __rdiv__(self, other)
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
def FreshReal(prefix='b', ctx=None)
def fpIsNegative(a, ctx=None)
def __rxor__(self, other)
Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i)
Return a uninterpreted sort that m assigns an interpretation.
def update_rule(self, head, body, name)
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.
unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f)
Return the arity (number of arguments) of the given function interpretation.
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
def args2params(arguments, keywords, ctx=None)
def get_cover_delta(self, level, predicate)
def RoundTowardPositive(ctx=None)
def FloatSingle(ctx=None)
Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a)
Create an AST node marking a formula position for interpolation.
def set_param(*args, **kws)
def RatVal(a, b, ctx=None)
def __rmod__(self, other)
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
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)
Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p)
Convert a Z3_pattern into Z3_ast. This is just type casting.
def RealVector(prefix, sz, ctx=None)
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s)
Retrieve documentation string corresponding to parameter name s.
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a real-numbered term.
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
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....
def translate(self, other_ctx)
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.
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s)
Return the finite set of distinct values that represent the interpretation for sort s.
def set(self, *args, **keys)
void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
def fpBVToFP(v, sort, ctx=None)
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
def FPs(names, fpsort, ctx=None)
def FPVal(sig, exp=None, fps=None, ctx=None)
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
def RealVarVector(n, ctx=None)
def __rmul__(self, other)
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it.
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t)
Return the exponent value of a floating-point numeral as a string.
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
def __call__(self, goal, *arguments, **keywords)
def fpRoundToIntegral(rm, a, ctx=None)
def to_symbol(s, ctx=None)
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
def __init__(self, descr, ctx=None)
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
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....
def __getattr__(self, name)
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
def IntVal(val, ctx=None)
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...
Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
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.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)
Return the number of parameters in the given parameter description set.
Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create array extensionality index given two arrays with the same sort. The meaning is given by the ax...
def parse_smt2_string(s, sorts={}, decls={}, ctx=None)
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
def RoundTowardNegative(ctx=None)
Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
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_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.
def __init__(self, ctx=None)
Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a)
Return the function declaration f associated with a (_ as_array f) node.
def as_decimal(self, prec)
def __init__(self, c, ctx)
def fpToFP(a1, a2=None, a3=None, ctx=None)
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m)
Return the number of uninterpreted sorts that m assigs an interpretation to.
def simplify(a, *arguments, **keywords)
Utils.
def declare_core(self, name, rec_name, *args)
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
def fpUnsignedToFP(rm, v, sort, ctx=None)
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
def solve(*args, **keywords)
unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s)
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
def RoundNearestTiesToEven(ctx=None)
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
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_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
def translate(self, target)
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_ast Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
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....
Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the right t2 times.
def get_documentation(self, n)
def With(t, *args, **keys)
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s)
Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
def as_decimal(self, prec)
def fpToUBV(rm, x, s, ctx=None)
Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i)
Return sort of the i'th bound variable.
def simplify(self, *arguments, **keywords)
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 *n)
Return the exponent value of a floating-point numeral as a signed 64-bit integer.
def get_universe(self, s)
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.
def assert_exprs(self, *args)
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
def __rtruediv__(self, other)
def fpGEQ(a, b, ctx=None)
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)
Return the name of the idx tactic.
def num_no_patterns(self)
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array)
Access the array default value. Produces the default range value, for arrays that can be represented ...
def rule(self, head, body=None, name=None)
def __call__(self, *args)
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...
def exponent_as_long(self)
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, Z3_bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p)
Convert a parameter description set into a string. This function is mainly used for printing the cont...
def fpRem(a, b, ctx=None)
Z3_bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int *sgn)
Retrieves the sign of a floating-point literal.
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
def set(self, *args, **keys)
def __setitem__(self, k, v)
def assert_exprs(self, *args)
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Brujin bound variable.
def __rsub__(self, other)
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
def is_finite_domain_sort(s)
def __init__(self, stats, ctx)
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
def denominator_as_long(self)
Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
def assert_and_track(self, a, p)
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
def BoolVector(prefix, sz, ctx=None)
def Array(name, dom, rng)
void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist)
Reclaim memory allocated for constructor list.
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])
Create a constructor.
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_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, unsigned __int64 size)
Create a named finite domain sort.
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
def set_default_rounding_mode(rm, ctx=None)
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
def Cond(p, t1, t2, ctx=None)
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a)
Convert an AST into a FUNC_DECL_AST. This is just type casting.
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 register_relation(self, *relations)
def __init__(self, fixedpoint=None, ctx=None)
def set(self, *args, **keys)
def simplify_param_descrs()
def approx(self, precision=10)
def fpToFPUnsigned(rm, x, s, ctx=None)
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...
def fpMul(rm, a, b, ctx=None)
void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p)
Increment the reference counter of the given parameter description set.
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.
def BitVec(name, bv, ctx=None)
Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the left t2 times.
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
def __getitem__(self, arg)
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
def __getitem__(self, arg)
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).
Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
def __init__(self, v=None, ctx=None)
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...
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
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...
def __radd__(self, other)
def __rdiv__(self, other)
def fpIsNormal(a, ctx=None)
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry 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_...
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
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 get_default_rounding_mode(ctx=None)
def fact(self, head, name=None)
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.
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c, Z3_ast pat, Z3_params p, Z3_ast_vector *interp, Z3_model *model)
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
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,...
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th no_pattern.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
def __init__(self, ctx=None)
def __init__(self, solver=None, ctx=None)
def ParAndThen(t1, t2, ctx=None)
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t)
Return the significand value of a floating-point numeral as a string.
def __rtruediv__(self, other)
def Bools(names, ctx=None)
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...
def RoundNearestTiesToAway(ctx=None)
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th pattern.
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_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...
def RealVal(val, ctx=None)
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
def Extract(high, low, a)
def __getitem__(self, idx)
def apply(self, goal, *arguments, **keywords)
Z3_goal Z3_API Z3_mk_goal(Z3_context c, Z3_bool models, Z3_bool unsat_cores, Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
def RealVar(idx, ctx=None)
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal.
def FloatQuadruple(ctx=None)
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
def FloatDouble(ctx=None)
void Z3_API Z3_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
def declare_var(self, *vars)
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
def add_soft(self, arg, weight="1", id=None)
def parse_smt2_file(f, sorts={}, decls={}, ctx=None)
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
def substitute_vars(t, *m)
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
def get_key_value(self, key)
def fpFMA(rm, a, b, c, ctx=None)
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i,...
Strings, Sequences and Regular expressions.
def Implies(a, b, ctx=None)
def __init__(self, tactic, ctx=None)
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
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_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p)
Return the number of parameters in the given parameter description set.
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL,...
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
def __truediv__(self, other)
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
def __init__(self, opt, value, is_max)
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
def solve_using(s, *args, **keywords)
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 StringVal(s, ctx=None)
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
def FiniteDomainVal(val, sort, ctx=None)
def FPSort(ebits, sbits, ctx=None)
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
def DeclareSort(name, ctx=None)
def Ints(names, ctx=None)
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
def Interpolant(a, ctx=None)
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 ...
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 assert_exprs(self, *args)
def FreshBool(prefix='b', ctx=None)
def probe_description(name, 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.
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v.
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
def tactic_description(name, ctx=None)
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_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
def __rshift__(self, other)
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
def is_string_value(self)
def num_constructors(self)
Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.
def __contains__(self, item)
def eval(self, t, model_completion=False)
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...
def __contains__(self, key)
def __rmul__(self, other)
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new (incremental) solver.
def numerator_as_long(self)
def FP(name, fpsort, ctx=None)
def fpToSBV(rm, x, s, ctx=None)
def fpDiv(rm, a, b, ctx=None)
def get_default_fp_sort(ctx=None)
def set_default_fp_sort(ebits, sbits, ctx=None)
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
def BitVecs(names, bv, ctx=None)
def translate(self, target)
def from_file(self, filename)
def __init__(self, probe, ctx=None)
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
def __init__(self, f, ctx)
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.
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target)
Copy a goal g from the context source to a the context target.
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places.
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i)
Return symbol of the i'th bound variable.
def __radd__(self, other)
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
def to_string(self, queries)
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.
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....
Z3_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if quantifier is universal.
def constructor(self, idx)
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to a the context target.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
def Strings(names, ctx=None)
void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d)
Validate the parameter set p against the parameter description set d.
def __getitem__(self, key)
def fpSub(rm, a, b, ctx=None)
def fpFP(sgn, exp, sig, ctx=None)
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
def __setitem__(self, i, v)
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
def parse_string(self, s)
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
def fpSqrt(rm, a, ctx=None)
def __init__(self, *args, **kws)
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 EnumSort(name, values, ctx=None)
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...
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
def get_interp(self, decl)
def __init__(self, c, ctx)
def __init__(self, name, ctx=None)
void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v)
Add a double parameter k with value v to the parameter set p.
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
def RoundTowardZero(ctx=None)
def consequences(self, assumptions, variables)
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...
def declare(self, name, *args)
def add_rule(self, head, body=None, name=None)
def __rmul__(self, other)
def BoolVal(val, ctx=None)
Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n)
Return the kind associated with the given parameter name n.
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_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
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 ...
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, Z3_bool negative)
Create a floating-point zero of sort s.
def fpMin(a, b, ctx=None)
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
def __init__(self, m, ctx)
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
def no_pattern(self, idx)
def FreshInt(prefix='x', ctx=None)
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
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...
def __rmod__(self, other)
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
def __init__(self, m=None, ctx=None)
def recognizer(self, idx)
def BitVecSort(sz, ctx=None)
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
def __getitem__(self, arg)
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.
def set_predicate_representation(self, f, *representations)
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
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...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
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.
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.
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.
def check(self, *assumptions)
def BV2Int(a, is_signed=False)
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
Z3_bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a)
The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3....
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, Z3_bool negative)
Create a floating-point infinity of sort s.
def TryFor(t, ms, ctx=None)
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
def sequence_interpolant(v, p=None, ctx=None)
Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None)
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.
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
def __rmod__(self, other)
def __init__(self, ast, ctx=None)
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
def convert_model(self, model, idx=0)
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
def __radd__(self, other)
def __init__(self, result, ctx)
def abstract(self, fml, is_forall=True)
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)
def __rtruediv__(self, other)
def set_option(*args, **kws)
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 __rlshift__(self, other)
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...
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)
def __truediv__(self, other)
def evaluate(self, t, model_completion=False)
def prove(claim, **keywords)
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v)
Add a Boolean parameter k with value v to the parameter set p.
def assert_exprs(self, *args)
def Reals(names, ctx=None)
def __rpow__(self, other)
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
def fpInfinity(s, negative)
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 Z3_API Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t)
Predicate indicating whether t is a positive floating-point number.
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
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.
def __rdiv__(self, other)
def fpFPToFP(rm, v, sort, ctx=None)
def fpNEQ(a, b, 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 Repeat(t, max=4294967295, ctx=None)
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.
def __getitem__(self, idx)
def SolverFor(logic, ctx=None)
Z3_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
def ParThen(t1, t2, ctx=None)
Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const *args)
Map f on the argument arrays.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
def __rmul__(self, other)
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.
def fpIsZero(a, ctx=None)
def __rand__(self, other)
def fpIsSubnormal(a, ctx=None)
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_...
void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
def fpRealToFP(rm, v, sort, ctx=None)
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
def __truediv__(self, other)
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read.
def fpIsPositive(a, ctx=None)
def __rsub__(self, other)
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
def is_algebraic_value(a)
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_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
def String(name, ctx=None)
def __radd__(self, other)
def __lshift__(self, other)
void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p)
Decrement the reference counter of the given parameter description set.
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_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.
def tree_interpolant(pat, p=None, ctx=None)
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
def SimpleSolver(ctx=None)
def __rsub__(self, other)
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.