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()) 1422 return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx) 1424 def BoolVal(val, ctx=None): 1425 """Return the Boolean value `
True`
or `
False`. If `ctx=
None`, then the
global context
is used.
1438 return BoolRef(Z3_mk_false(ctx.ref()), ctx) 1440 return BoolRef(Z3_mk_true(ctx.ref()), ctx) 1442 def Bool(name, ctx=None): 1443 """Return a Boolean constant named `name`. If `ctx=
None`, then the
global context
is used.
1451 return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx) 1453 def Bools(names, ctx=None): 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] 1468 def BoolVector(prefix, sz, ctx=None): 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.
1478 And(p__0, p__1, p__2)
1480 return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ] 1482 def FreshBool(prefix='b', ctx=None): 1483 """Return a fresh Boolean constant
in the given context using the given prefix.
1485 If `ctx=
None`, then the
global context
is used.
1493 return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx) 1495 def Implies(a, b, ctx=None): 1496 """Create a Z3 implies expression.
1498 >>> p, q =
Bools(
'p q')
1504 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 1508 return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 1510 def Xor(a, b, ctx=None): 1511 """Create a Z3 Xor expression.
1513 >>> p, q =
Bools(
'p q')
1519 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 1523 return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 1525 def Not(a, ctx=None): 1526 """Create a Z3
not expression
or probe.
1534 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) 1536 # Not is also used to build probes 1537 return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx) 1541 return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), 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')
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) 1581 return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx) 1584 """Create a Z3
or-expression
or or-probe.
1586 >>> p, q, r =
Bools(
'p q r')
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) 1611 return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx) 1613 ######################################### 1617 ######################################### 1619 class PatternRef(ExprRef): 1620 """Patterns are hints
for quantifier instantiation.
1622 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1625 return Z3_pattern_to_ast(self.ctx_ref(), self.ast) 1628 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1631 """Return `
True`
if `a`
is a Z3 pattern (hint
for quantifier instantiation.
1633 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1637 >>> q =
ForAll(x, f(x) == 0, patterns = [ f(x) ])
1640 >>> q.num_patterns()
1647 return isinstance(a, PatternRef) 1649 def MultiPattern(*args): 1650 """Create a Z3 multi-pattern using the given expressions `*args`
1652 See http://rise4fun.com/Z3Py/tutorial/advanced
for more details.
1660 >>> q.num_patterns()
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): 1678 return MultiPattern(arg) 1680 ######################################### 1684 ######################################### 1686 class QuantifierRef(BoolRef): 1687 """Universally
and Existentially quantified formulas.
""" 1693 return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) 1696 """Return the Boolean sort.
""" 1697 return BoolSort(self.ctx) 1699 def is_forall(self): 1700 """Return `
True`
if `self`
is a universal quantifier.
1704 >>> q =
ForAll(x, f(x) == 0)
1707 >>> q =
Exists(x, f(x) != 0)
1711 return Z3_is_quantifier_forall(self.ctx_ref(), self.ast) 1714 """Return the weight annotation of `self`.
1718 >>> q =
ForAll(x, f(x) == 0)
1721 >>> q =
ForAll(x, f(x) == 0, weight=10)
1725 return int(Z3_get_quantifier_weight(self.ctx_ref(), self.ast)) 1727 def num_patterns(self): 1728 """Return the number of patterns (i.e., quantifier instantiation hints)
in `self`.
1733 >>> q =
ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ])
1734 >>> q.num_patterns()
1737 return int(Z3_get_quantifier_num_patterns(self.ctx_ref(), self.ast)) 1739 def pattern(self, idx): 1740 """Return a pattern (i.e., quantifier instantiation hints)
in `self`.
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") 1755 return PatternRef(Z3_get_quantifier_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1757 def num_no_patterns(self): 1758 """Return the number of no-patterns.
""" 1759 return Z3_get_quantifier_num_no_patterns(self.ctx_ref(), self.ast) 1761 def no_pattern(self, idx): 1762 """Return a no-pattern.
""" 1764 _z3_assert(idx < self.num_no_patterns(), "Invalid no-pattern idx") 1765 return _to_expr_ref(Z3_get_quantifier_no_pattern_ast(self.ctx_ref(), self.ast, idx), self.ctx) 1768 """Return the expression being quantified.
1772 >>> q =
ForAll(x, f(x) == 0)
1776 return _to_expr_ref(Z3_get_quantifier_body(self.ctx_ref(), self.ast), self.ctx) 1779 """Return the number of variables bounded by this quantifier.
1784 >>> q =
ForAll([x, y], f(x, y) >= x)
1788 return int(Z3_get_quantifier_num_bound(self.ctx_ref(), self.ast)) 1790 def var_name(self, idx): 1791 """Return a string representing a name used when displaying the quantifier.
1796 >>> q =
ForAll([x, y], f(x, y) >= x)
1803 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1804 return _symbol2py(self.ctx, Z3_get_quantifier_bound_name(self.ctx_ref(), self.ast, idx)) 1806 def var_sort(self, idx): 1807 """Return the sort of a bound variable.
1812 >>> q =
ForAll([x, y], f(x, y) >= x)
1819 _z3_assert(idx < self.num_vars(), "Invalid variable idx") 1820 return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx) 1823 """Return a list containing a single element self.
body()
1827 >>> q =
ForAll(x, f(x) == 0)
1831 return [ self.body() ] 1833 def is_quantifier(a): 1834 """Return `
True`
if `a`
is a Z3 quantifier.
1838 >>> q =
ForAll(x, f(x) == 0)
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): 1860 ## TODO: Check if is constant 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) 1868 qid = to_symbol(qid, ctx) 1869 skid = to_symbol(skid, ctx) 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.
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.
1905 >>> q =
Exists([x, y], f(x, y) >= x, skid=
"foo")
1907 Exists([x, y], f(x, y) >= x)
1910 >>> r =
Tactic(
'nnf')(q).as_expr()
1914 return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns) 1916 ######################################### 1920 ######################################### 1922 class ArithSortRef(SortRef): 1923 """Real
and Integer sorts.
""" 1926 """Return `
True`
if `self`
is of the sort Real.
1937 return self.kind() == Z3_REAL_SORT 1940 """Return `
True`
if `self`
is of the sort Integer.
1951 return self.kind() == Z3_INT_SORT 1953 def subsort(self, other): 1954 """Return `
True`
if `self`
is a subsort of `other`.
""" 1955 return self.is_int() and is_arith_sort(other) and other.is_real() 1957 def cast(self, val): 1958 """Try to cast `val`
as an Integer
or Real.
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(): 1982 return ToReal(If(val, 1, 0)) 1984 _z3_assert(False, "Z3 Integer/Real expression expected" ) 1987 return IntVal(val, self.ctx) 1989 return RealVal(val, self.ctx) 1991 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected") 1993 def is_arith_sort(s): 1994 """Return `
True`
if s
is an arithmetical sort (type).
2002 >>> n =
Int(
'x') + 1
2006 return isinstance(s, ArithSortRef) 2008 class ArithRef(ExprRef): 2009 """Integer
and Real expressions.
""" 2012 """Return the sort (type) of the arithmetical expression `self`.
2019 return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 2022 """Return `
True`
if `self`
is an integer expression.
2033 return self.sort().is_int() 2036 """Return `
True`
if `self`
is an real expression.
2044 return self.sort().is_real() 2046 def __add__(self, other): 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) 2059 def __radd__(self, other): 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) 2069 def __mul__(self, other): 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) 2082 def __rmul__(self, other): 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) 2092 def __sub__(self, other): 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) 2105 def __rsub__(self, other): 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) 2115 def __pow__(self, other): 2116 """Create the Z3 expression `self**other` (**
is the power operator).
2126 a, b = _coerce_exprs(self, other) 2127 return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2129 def __rpow__(self, other): 2130 """Create the Z3 expression `other**self` (**
is the power operator).
2140 a, b = _coerce_exprs(self, other) 2141 return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2143 def __div__(self, other): 2144 """Create the Z3 expression `other/self`.
2163 a, b = _coerce_exprs(self, other) 2164 return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2166 def __truediv__(self, other): 2167 """Create the Z3 expression `other/self`.
""" 2168 return self.__div__(other) 2170 def __rdiv__(self, other): 2171 """Create the Z3 expression `other/self`.
2184 a, b = _coerce_exprs(self, other) 2185 return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2187 def __rtruediv__(self, other): 2188 """Create the Z3 expression `other/self`.
""" 2189 return self.__rdiv__(other) 2191 def __mod__(self, other): 2192 """Create the Z3 expression `other%self`.
2201 a, b = _coerce_exprs(self, other) 2203 _z3_assert(a.is_int(), "Z3 integer expression expected") 2204 return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2206 def __rmod__(self, other): 2207 """Create the Z3 expression `other%self`.
2213 a, b = _coerce_exprs(self, other) 2215 _z3_assert(a.is_int(), "Z3 integer expression expected") 2216 return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 2219 """Return an expression representing `-self`.
2227 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx) 2238 def __le__(self, other): 2239 """Create the Z3 expression `other <= self`.
2241 >>> x, y =
Ints(
'x y')
2248 a, b = _coerce_exprs(self, other) 2249 return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2251 def __lt__(self, other): 2252 """Create the Z3 expression `other < self`.
2254 >>> x, y =
Ints(
'x y')
2261 a, b = _coerce_exprs(self, other) 2262 return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2264 def __gt__(self, other): 2265 """Create the Z3 expression `other > self`.
2267 >>> x, y =
Ints(
'x y')
2274 a, b = _coerce_exprs(self, other) 2275 return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2277 def __ge__(self, other): 2278 """Create the Z3 expression `other >= self`.
2280 >>> x, y =
Ints(
'x y')
2287 a, b = _coerce_exprs(self, other) 2288 return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 2291 """Return `
True`
if `a`
is an arithmetical expression.
2308 return isinstance(a, ArithRef) 2311 """Return `
True`
if `a`
is an integer expression.
2326 return is_arith(a) and a.is_int() 2329 """Return `
True`
if `a`
is a real expression.
2344 return is_arith(a) and a.is_real() 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) 2352 def is_int_value(a): 2353 """Return `
True`
if `a`
is an integer value of sort Int.
2361 >>> n =
Int(
'x') + 1
2373 return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast()) 2375 def is_rational_value(a): 2376 """Return `
True`
if `a`
is rational value of sort Real.
2386 >>> n =
Real(
'x') + 1
2394 return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast()) 2396 def is_algebraic_value(a): 2397 """Return `
True`
if `a`
is an algerbraic value of sort Real.
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')
2418 return is_app_of(a, Z3_OP_ADD) 2421 """Return `
True`
if `a`
is an expression of the form b * c.
2423 >>> x, y =
Ints(
'x y')
2429 return is_app_of(a, Z3_OP_MUL) 2432 """Return `
True`
if `a`
is an expression of the form b - c.
2434 >>> x, y =
Ints(
'x y')
2440 return is_app_of(a, Z3_OP_SUB) 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')
2456 return is_app_of(a, Z3_OP_DIV) 2459 """Return `
True`
if `a`
is an expression of the form b div c.
2461 >>> x, y =
Ints(
'x y')
2467 return is_app_of(a, Z3_OP_IDIV) 2470 """Return `
True`
if `a`
is an expression of the form b % c.
2472 >>> x, y =
Ints(
'x y')
2478 return is_app_of(a, Z3_OP_MOD) 2481 """Return `
True`
if `a`
is an expression of the form b <= c.
2483 >>> x, y =
Ints(
'x y')
2489 return is_app_of(a, Z3_OP_LE) 2492 """Return `
True`
if `a`
is an expression of the form b < c.
2494 >>> x, y =
Ints(
'x y')
2500 return is_app_of(a, Z3_OP_LT) 2503 """Return `
True`
if `a`
is an expression of the form b >= c.
2505 >>> x, y =
Ints(
'x y')
2511 return is_app_of(a, Z3_OP_GE) 2514 """Return `
True`
if `a`
is an expression of the form b > c.
2516 >>> x, y =
Ints(
'x y')
2522 return is_app_of(a, Z3_OP_GT) 2525 """Return `
True`
if `a`
is an expression of the form
IsInt(b).
2533 return is_app_of(a, Z3_OP_IS_INT) 2536 """Return `
True`
if `a`
is an expression of the form
ToReal(b).
2547 return is_app_of(a, Z3_OP_TO_REAL) 2550 """Return `
True`
if `a`
is an expression of the form
ToInt(b).
2561 return is_app_of(a, Z3_OP_TO_INT) 2563 class IntNumRef(ArithRef): 2564 """Integer values.
""" 2567 """Return a Z3 integer numeral
as a Python long (bignum) numeral.
2576 _z3_assert(self.is_int(), "Integer value expected") 2577 return int(self.as_string()) 2579 def as_string(self): 2580 """Return a Z3 integer numeral
as a Python string.
2585 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2587 class RatNumRef(ArithRef): 2588 """Rational values.
""" 2590 def numerator(self): 2591 """ Return the numerator of a Z3 rational numeral.
2603 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx) 2605 def denominator(self): 2606 """ Return the denominator of a Z3 rational numeral.
2614 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx) 2616 def numerator_as_long(self): 2617 """ Return the numerator
as a Python long.
2624 >>> v.numerator_as_long() + 1 == 10000000001
2627 return self.numerator().as_long() 2629 def denominator_as_long(self): 2630 """ Return the denominator
as a Python long.
2635 >>> v.denominator_as_long()
2638 return self.denominator().as_long() 2640 def as_decimal(self, prec): 2641 """ Return a Z3 rational value
as a string
in decimal notation using at most `prec` decimal places.
2650 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2652 def as_string(self): 2653 """Return a Z3 rational numeral
as a Python string.
2659 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 2661 def as_fraction(self): 2662 """Return a Z3 rational
as a Python Fraction object.
2668 return Fraction(self.numerator_as_long(), self.denominator_as_long()) 2670 class AlgebraicNumRef(ArithRef): 2671 """Algebraic irrational values.
""" 2673 def approx(self, precision=10): 2674 """Return a Z3 rational number that approximates the algebraic number `self`.
2675 The result `r`
is such that |r - self| <= 1/10^precision
2679 6838717160008073720548335/4835703278458516698824704
2683 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx) 2684 def as_decimal(self, prec): 2685 """Return a string representation of the algebraic number `self`
in decimal notation using `prec` decimal places
2688 >>> x.as_decimal(10)
2690 >>> x.as_decimal(20)
2691 '1.41421356237309504880?' 2693 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) 2695 def _py2expr(a, ctx=None): 2696 if isinstance(a, bool): 2697 return BoolVal(a, ctx) 2699 return IntVal(a, ctx) 2700 if isinstance(a, float): 2701 return RealVal(a, ctx) 2703 _z3_assert(False, "Python bool, int, long or float expected") 2705 def IntSort(ctx=None): 2706 """Return the integer sort
in the given context. If `ctx=
None`, then the
global context
is used.
2719 return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx) 2721 def RealSort(ctx=None): 2722 """Return the real sort
in the given context. If `ctx=
None`, then the
global context
is used.
2735 return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx) 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") 2752 def IntVal(val, ctx=None): 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) 2763 def RealVal(val, ctx=None): 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.
2779 return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx) 2781 def RatVal(a, b, ctx=None): 2782 """Return a Z3 rational a/b.
2784 If `ctx=
None`, then the
global context
is used.
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") 2794 return simplify(RealVal(a, ctx)/RealVal(b, ctx)) 2796 def Q(a, b, ctx=None): 2797 """Return a Z3 rational a/b.
2799 If `ctx=
None`, then the
global context
is used.
2806 return simplify(RatVal(a, b)) 2808 def Int(name, ctx=None): 2809 """Return an integer constant named `name`. If `ctx=
None`, then the
global context
is used.
2818 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx) 2820 def Ints(names, ctx=None): 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] 2832 def IntVector(prefix, sz, ctx=None): 2833 """Return a list of integer constants of size `sz`.
2841 return [ Int('%s__%s' % (prefix, i)) for i in range(sz) ] 2843 def FreshInt(prefix='x', ctx=None): 2844 """Return a fresh integer constant
in the given context using the given prefix.
2854 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx) 2856 def Real(name, ctx=None): 2857 """Return a real constant named `name`. If `ctx=
None`, then the
global context
is used.
2866 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx) 2868 def Reals(names, ctx=None): 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] 2882 def RealVector(prefix, sz, ctx=None): 2883 """Return a list of real constants of size `sz`.
2893 return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ] 2895 def FreshReal(prefix='b', ctx=None): 2896 """Return a fresh real constant
in the given context using the given prefix.
2906 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx) 2909 """ Return the Z3 expression
ToReal(a).
2921 _z3_assert(a.is_int(), "Z3 integer expression expected.") 2923 return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx) 2926 """ Return the Z3 expression
ToInt(a).
2938 _z3_assert(a.is_real(), "Z3 real expression expected.") 2940 return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx) 2943 """ Return the Z3 predicate
IsInt(a).
2946 >>>
IsInt(x +
"1/2")
2950 >>>
solve(
IsInt(x +
"1/2"), x > 0, x < 1, x !=
"1/2")
2954 _z3_assert(a.is_real(), "Z3 real expression expected.") 2956 return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx) 2958 def Sqrt(a, ctx=None): 2959 """ Return a Z3 expression which represents the square root of a.
2970 def Cbrt(a, ctx=None): 2971 """ Return a Z3 expression which represents the cubic root of a.
2982 ######################################### 2986 ######################################### 2988 class BitVecSortRef(SortRef): 2989 """Bit-vector sort.
""" 2992 """Return the size (number of bits) of the bit-vector sort `self`.
2998 return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast)) 3000 def subsort(self, other): 3001 return is_bv_sort(other) and self.size() < other.size() 3003 def cast(self, val): 3004 """Try to cast `val`
as a Bit-Vector.
3009 >>> b.cast(10).
sexpr()
3014 _z3_assert(self.ctx == val.ctx, "Context mismatch") 3015 # Idea: use sign_extend if sort of val is a bitvector of smaller size 3018 return BitVecVal(val, self) 3021 """Return
True if `s`
is a Z3 bit-vector sort.
3028 return isinstance(s, BitVecSortRef) 3030 class BitVecRef(ExprRef): 3031 """Bit-vector expressions.
""" 3034 """Return the sort of the bit-vector expression `self`.
3042 return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 3045 """Return the number of bits of the bit-vector expression `self`.
3053 return self.sort().size() 3055 def __add__(self, other): 3056 """Create the Z3 expression `self + other`.
3065 a, b = _coerce_exprs(self, other) 3066 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3068 def __radd__(self, other): 3069 """Create the Z3 expression `other + self`.
3075 a, b = _coerce_exprs(self, other) 3076 return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3078 def __mul__(self, other): 3079 """Create the Z3 expression `self * other`.
3088 a, b = _coerce_exprs(self, other) 3089 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3091 def __rmul__(self, other): 3092 """Create the Z3 expression `other * self`.
3098 a, b = _coerce_exprs(self, other) 3099 return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3101 def __sub__(self, other): 3102 """Create the Z3 expression `self - other`.
3111 a, b = _coerce_exprs(self, other) 3112 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3114 def __rsub__(self, other): 3115 """Create the Z3 expression `other - self`.
3121 a, b = _coerce_exprs(self, other) 3122 return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3124 def __or__(self, other): 3125 """Create the Z3 expression bitwise-
or `self | other`.
3134 a, b = _coerce_exprs(self, other) 3135 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3137 def __ror__(self, other): 3138 """Create the Z3 expression bitwise-
or `other | self`.
3144 a, b = _coerce_exprs(self, other) 3145 return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3147 def __and__(self, other): 3148 """Create the Z3 expression bitwise-
and `self & other`.
3157 a, b = _coerce_exprs(self, other) 3158 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3160 def __rand__(self, other): 3161 """Create the Z3 expression bitwise-
or `other & self`.
3167 a, b = _coerce_exprs(self, other) 3168 return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3170 def __xor__(self, other): 3171 """Create the Z3 expression bitwise-xor `self ^ other`.
3180 a, b = _coerce_exprs(self, other) 3181 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3183 def __rxor__(self, other): 3184 """Create the Z3 expression bitwise-xor `other ^ self`.
3190 a, b = _coerce_exprs(self, other) 3191 return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3203 """Return an expression representing `-self`.
3211 return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx) 3213 def __invert__(self): 3214 """Create the Z3 expression bitwise-
not `~self`.
3222 return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx) 3224 def __div__(self, other): 3225 """Create the Z3 expression (signed) division `self / other`.
3227 Use the function
UDiv()
for unsigned division.
3240 a, b = _coerce_exprs(self, other) 3241 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3243 def __truediv__(self, other): 3244 """Create the Z3 expression (signed) division `self / other`.
""" 3245 return self.__div__(other) 3247 def __rdiv__(self, other): 3248 """Create the Z3 expression (signed) division `other / self`.
3250 Use the function
UDiv()
for unsigned division.
3255 >>> (10 / x).
sexpr()
3256 '(bvsdiv #x0000000a x)' 3258 '(bvudiv #x0000000a x)' 3260 a, b = _coerce_exprs(self, other) 3261 return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3263 def __rtruediv__(self, other): 3264 """Create the Z3 expression (signed) division `other / self`.
""" 3265 return self.__rdiv__(other) 3267 def __mod__(self, other): 3268 """Create the Z3 expression (signed) mod `self % other`.
3270 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3285 a, b = _coerce_exprs(self, other) 3286 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3288 def __rmod__(self, other): 3289 """Create the Z3 expression (signed) mod `other % self`.
3291 Use the function
URem()
for unsigned remainder,
and SRem()
for signed remainder.
3296 >>> (10 % x).
sexpr()
3297 '(bvsmod #x0000000a x)' 3299 '(bvurem #x0000000a x)' 3301 '(bvsrem #x0000000a x)' 3303 a, b = _coerce_exprs(self, other) 3304 return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3306 def __le__(self, other): 3307 """Create the Z3 expression (signed) `other <= self`.
3309 Use the function
ULE()
for unsigned less than
or equal to.
3314 >>> (x <= y).
sexpr()
3319 a, b = _coerce_exprs(self, other) 3320 return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3322 def __lt__(self, other): 3323 """Create the Z3 expression (signed) `other < self`.
3325 Use the function
ULT()
for unsigned less than.
3335 a, b = _coerce_exprs(self, other) 3336 return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3338 def __gt__(self, other): 3339 """Create the Z3 expression (signed) `other > self`.
3341 Use the function
UGT()
for unsigned greater than.
3351 a, b = _coerce_exprs(self, other) 3352 return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3354 def __ge__(self, other): 3355 """Create the Z3 expression (signed) `other >= self`.
3357 Use the function
UGE()
for unsigned greater than
or equal to.
3362 >>> (x >= y).
sexpr()
3367 a, b = _coerce_exprs(self, other) 3368 return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3370 def __rshift__(self, other): 3371 """Create the Z3 expression (arithmetical) right shift `self >> other`
3373 Use the function
LShR()
for the right logical shift
3378 >>> (x >> y).
sexpr()
3397 a, b = _coerce_exprs(self, other) 3398 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3400 def __lshift__(self, other): 3401 """Create the Z3 expression left shift `self << other`
3406 >>> (x << y).
sexpr()
3411 a, b = _coerce_exprs(self, other) 3412 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) 3414 def __rrshift__(self, other): 3415 """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
3417 Use the function
LShR()
for the right logical shift
3422 >>> (10 >> x).
sexpr()
3423 '(bvashr #x0000000a x)' 3425 a, b = _coerce_exprs(self, other) 3426 return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3428 def __rlshift__(self, other): 3429 """Create the Z3 expression left shift `other << self`.
3431 Use the function
LShR()
for the right logical shift
3436 >>> (10 << x).
sexpr()
3437 '(bvshl #x0000000a x)' 3439 a, b = _coerce_exprs(self, other) 3440 return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx) 3442 class BitVecNumRef(BitVecRef): 3443 """Bit-vector values.
""" 3446 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral.
3451 >>> print(
"0x%.8x" % v.as_long())
3454 return int(self.as_string()) 3456 def as_signed_long(self): 3457 """Return a Z3 bit-vector numeral
as a Python long (bignum) numeral. The most significant bit
is assumed to be the sign.
3471 val = self.as_long() 3472 if val >= 2**(sz - 1): 3474 if val < -2**(sz - 1): 3478 def as_string(self): 3479 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 3482 """Return `
True`
if `a`
is a Z3 bit-vector expression.
3492 return isinstance(a, BitVecRef) 3495 """Return `
True`
if `a`
is a Z3 bit-vector numeral value.
3506 return is_bv(a) and _is_numeral(a.ctx, a.as_ast()) 3508 def BV2Int(a, is_signed=False): 3509 """Return the Z3 expression
BV2Int(a).
3517 >>> x >
BV2Int(b, is_signed=
False)
3519 >>> x >
BV2Int(b, is_signed=
True)
3525 _z3_assert(is_bv(a), "Z3 bit-vector expression expected") 3527 ## investigate problem with bv2int 3528 return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx) 3530 def BitVecSort(sz, ctx=None): 3531 """Return a Z3 bit-vector sort of the given size. If `ctx=
None`, then the
global context
is used.
3537 >>> x =
Const(
'x', Byte)
3542 return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx) 3544 def BitVecVal(val, bv, ctx=None): 3545 """Return a bit-vector value with the given number of bits. If `ctx=
None`, then the
global context
is used.
3550 >>> print(
"0x%.8x" % v.as_long())
3555 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx) 3558 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx) 3560 def BitVec(name, bv, ctx=None): 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.
3572 >>> x2 =
BitVec(
'x', word)
3576 if isinstance(bv, BitVecSortRef): 3580 bv = BitVecSort(bv, ctx) 3581 return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx) 3583 def BitVecs(names, bv, ctx=None): 3584 """Return a tuple of bit-vector constants of size bv.
3586 >>> x, y, z =
BitVecs(
'x y z', 16)
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.
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): 3645 r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx) 3648 def Extract(high, low, a): 3649 """Create a Z3 bit-vector extraction expression,
or create a string extraction expression.
3659 if isinstance(high, str): 3660 high = StringVal(high) 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") 3673 return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx) 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.
3687 >>> (x <= y).sexpr()
3689 >>>
ULE(x, y).sexpr()
3692 _check_bv_args(a, b) 3693 a, b = _coerce_exprs(a, b) 3694 return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3697 """Create the Z3 expression (unsigned) `other < self`.
3699 Use the operator <
for signed less than.
3706 >>>
ULT(x, y).sexpr()
3709 _check_bv_args(a, b) 3710 a, b = _coerce_exprs(a, b) 3711 return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3714 """Create the Z3 expression (unsigned) `other >= self`.
3716 Use the operator >=
for signed greater than
or equal to.
3721 >>> (x >= y).sexpr()
3723 >>>
UGE(x, y).sexpr()
3726 _check_bv_args(a, b) 3727 a, b = _coerce_exprs(a, b) 3728 return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3731 """Create the Z3 expression (unsigned) `other > self`.
3733 Use the operator >
for signed greater than.
3740 >>>
UGT(x, y).sexpr()
3743 _check_bv_args(a, b) 3744 a, b = _coerce_exprs(a, b) 3745 return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3748 """Create the Z3 expression (unsigned) division `self / other`.
3750 Use the operator /
for signed division.
3756 >>>
UDiv(x, y).sort()
3760 >>>
UDiv(x, y).sexpr()
3763 _check_bv_args(a, b) 3764 a, b = _coerce_exprs(a, b) 3765 return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3768 """Create the Z3 expression (unsigned) remainder `self % other`.
3770 Use the operator %
for signed modulus,
and SRem()
for signed remainder.
3776 >>>
URem(x, y).sort()
3780 >>>
URem(x, y).sexpr()
3783 _check_bv_args(a, b) 3784 a, b = _coerce_exprs(a, b) 3785 return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3788 """Create the Z3 expression signed remainder.
3790 Use the operator %
for signed modulus,
and URem()
for unsigned remainder.
3796 >>>
SRem(x, y).sort()
3800 >>>
SRem(x, y).sexpr()
3803 _check_bv_args(a, b) 3804 a, b = _coerce_exprs(a, b) 3805 return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3808 """Create the Z3 expression logical right shift.
3810 Use the operator >>
for the arithmetical right shift.
3815 >>> (x >> y).sexpr()
3817 >>>
LShR(x, y).sexpr()
3834 _check_bv_args(a, b) 3835 a, b = _coerce_exprs(a, b) 3836 return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3838 def RotateLeft(a, b): 3839 """Return an expression representing `a` rotated to the left `b` times.
3849 _check_bv_args(a, b) 3850 a, b = _coerce_exprs(a, b) 3851 return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3853 def RotateRight(a, b): 3854 """Return an expression representing `a` rotated to the right `b` times.
3864 _check_bv_args(a, b) 3865 a, b = _coerce_exprs(a, b) 3866 return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) 3869 """Return a bit-vector expression with `n` extra sign-bits.
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") 3895 return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 3898 """Return a bit-vector expression with `n` extra zero-bits.
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") 3922 return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx) 3924 def RepeatBitVec(n, a): 3925 """Return an expression representing `n` copies of `a`.
3934 >>> print(
"%.x" % v0.as_long())
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") 3945 return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx) 3948 """Return the reduction-
and expression of `a`.
""" 3950 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 3951 return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) 3954 """Return the reduction-
or expression of `a`.
""" 3956 _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") 3957 return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) 3959 ######################################### 3963 ######################################### 3965 class ArraySortRef(SortRef): 3969 """Return the domain of the array sort `self`.
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`.
3984 return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx) 3986 class ArrayRef(ExprRef): 3987 """Array expressions.
""" 3990 """Return the array sort of the array expression `self`.
3996 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4005 return self.sort().domain() 4014 return self.sort().range() 4016 def __getitem__(self, arg): 4017 """Return the Z3 expression `self[arg]`.
4026 arg = self.domain().cast(arg) 4027 return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx) 4030 return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx) 4034 """Return `
True`
if `a`
is a Z3 array expression.
4044 return isinstance(a, ArrayRef) 4046 def is_const_array(a): 4047 """Return `
True`
if `a`
is a Z3 constant array.
4056 return is_app_of(a, Z3_OP_CONST_ARRAY) 4059 """Return `
True`
if `a`
is a Z3 constant array.
4068 return is_app_of(a, Z3_OP_CONST_ARRAY) 4071 """Return `
True`
if `a`
is a Z3 map array expression.
4083 return is_app_of(a, Z3_OP_ARRAY_MAP) 4086 """Return `
True`
if `a`
is a Z3 default array expression.
4091 return is_app_of(a, Z3_OP_ARRAY_DEFAULT) 4093 def get_map_func(a): 4094 """Return the function declaration associated with a Z3 map array expression.
4107 _z3_assert(is_map(a), "Z3 array map expression expected.") 4108 return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx) 4110 def ArraySort(d, r): 4111 """Return the Z3 array sort with the given domain
and range sorts.
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") 4129 return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx) 4131 def Array(name, dom, rng): 4132 """Return an array constant named `name` with the given domain
and range sorts.
4140 s = ArraySort(dom, rng) 4142 return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx) 4144 def Update(a, i, v): 4145 """Return a Z3 store array expression.
4148 >>> i, v =
Ints(
'i v')
4152 >>>
prove(s[i] == v)
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.
4172 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4177 """Return a Z3 store array expression.
4180 >>> i, v =
Ints(
'i v')
4181 >>> s =
Store(a, i, v)
4184 >>>
prove(s[i] == v)
4190 return Update(a, i, v) 4193 """Return a Z3 select array expression.
4203 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 4208 """Return a Z3 map array expression.
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) 4227 return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx) 4230 """Return a Z3 constant array expression.
4244 _z3_assert(is_sort(dom), "Z3 sort expected") 4247 v = _py2expr(v, ctx) 4248 return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx) 4251 """Return extensionality index
for arrays.
4254 _z3_assert(is_array(a) and is_array(b)) 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.
4267 return is_app_of(a, Z3_OP_SELECT) 4270 """Return `
True`
if `a`
is a Z3 array store application.
4278 return is_app_of(a, Z3_OP_STORE) 4280 ######################################### 4284 ######################################### 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.
4294 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4295 >>> List.declare(
'nil')
4296 >>> List = List.create()
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))
4316 def __init__(self, name, ctx=None): 4317 self.ctx = _get_ctx(ctx) 4319 self.constructors = [] 4321 def declare_core(self, name, rec_name, *args): 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)") 4326 self.constructors.append((name, rec_name, args)) 4328 def declare(self, name, *args): 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.
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") 4346 return self.declare_core(name, "is_" + name, *args) 4349 return "Datatype(%s, %s)" % (self.name, self.constructors) 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.
4357 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4358 >>> List.declare(
'nil')
4359 >>> List = List.create()
4362 >>> List.cons(10, List.nil)
4365 return CreateDatatypes([self])[0] 4367 class ScopedConstructor: 4368 """Auxiliary object used to create Z3 datatypes.
""" 4369 def __init__(self, c, ctx): 4373 if self.ctx.ref() is not None: 4374 Z3_del_constructor(self.ctx.ref(), self.c) 4376 class ScopedConstructorList: 4377 """Auxiliary object used to create Z3 datatypes.
""" 4378 def __init__(self, c, ctx): 4382 if self.ctx.ref() is not None: 4383 Z3_del_constructor_list(self.ctx.ref(), self.c) 4385 def CreateDatatypes(*ds): 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')
4393 >>> Tree.declare(
'leaf', (
'val',
IntSort()))
4395 >>> Tree.declare(
'node', (
'children', TreeList))
4396 >>> TreeList.declare(
'nil')
4397 >>> TreeList.declare(
'cons', (
'car', Tree), (
'cdr', 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))
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): 4426 names[i] = to_symbol(d.name, ctx) 4427 num_cs = len(d.constructors) 4428 cs = (Constructor * num_cs)() 4429 for j in range(num_cs): 4430 c = d.constructors[j] 4431 cname = to_symbol(c[0], ctx) 4432 rname = to_symbol(c[1], ctx) 4435 fnames = (Symbol * num_fs)() 4436 sorts = (Sort * num_fs)() 4437 refs = (ctypes.c_uint * num_fs)() 4438 for k in range(num_fs): 4441 fnames[k] = to_symbol(fname, ctx) 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 4452 cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs) 4453 to_delete.append(ScopedConstructor(cs[j], ctx)) 4454 clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs) 4455 to_delete.append(ScopedConstructorList(clists[i], ctx)) 4456 Z3_mk_datatypes(ctx.ref(), num, names, out, clists) 4458 ## Create a field for every constructor, recognizer and accessor 4459 for i in range(num): 4460 dref = DatatypeSortRef(out[i], ctx) 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) 4477 class DatatypeSortRef(SortRef): 4478 """Datatype sorts.
""" 4479 def num_constructors(self): 4480 """Return the number of constructors
in the given Z3 datatype.
4483 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4484 >>> List.declare(
'nil')
4485 >>> List = List.create()
4487 >>> List.num_constructors()
4490 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast)) 4492 def constructor(self, idx): 4493 """Return a constructor of the datatype `self`.
4496 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4497 >>> List.declare(
'nil')
4498 >>> List = List.create()
4500 >>> List.num_constructors()
4502 >>> List.constructor(0)
4504 >>> List.constructor(1)
4508 _z3_assert(idx < self.num_constructors(), "Invalid constructor index") 4509 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx) 4511 def recognizer(self, idx): 4512 """In Z3, each constructor has an associated recognizer predicate.
4514 If the constructor
is named `name`, then the recognizer `is_name`.
4517 >>> List.declare(
'cons', (
'car',
IntSort()), (
'cdr', List))
4518 >>> List.declare(
'nil')
4519 >>> List = List.create()
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)
4536 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index") 4537 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx) 4539 def accessor(self, i, j): 4540 """In Z3, each constructor has 0
or more accessor. The number of accessors
is equal to the arity of the constructor.
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()
4564 _z3_assert(i < self.num_constructors(), "Invalid constructor index") 4565 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index") 4566 return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx) 4568 class DatatypeRef(ExprRef): 4569 """Datatype expressions.
""" 4571 """Return the datatype sort of the datatype expression `self`.
""" 4572 return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 4574 def EnumSort(name, values, ctx=None): 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): 4589 _val_names[i] = to_symbol(values[i]) 4590 _values = (FuncDecl * num)() 4591 _testers = (FuncDecl * num)() 4592 name = to_symbol(name) 4593 S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx) 4595 for i in range(num): 4596 V.append(FuncDeclRef(_values[i], ctx)) 4597 V = [a() for a in V] 4600 ######################################### 4604 ######################################### 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.
4611 def __init__(self, ctx=None): 4612 self.ctx = _get_ctx(ctx) 4613 self.params = Z3_mk_params(self.ctx.ref()) 4614 Z3_params_inc_ref(self.ctx.ref(), self.params) 4617 if self.ctx.ref() is not None: 4618 Z3_params_dec_ref(self.ctx.ref(), self.params) 4620 def set(self, name, val): 4621 """Set parameter name with value val.
""" 4623 _z3_assert(isinstance(name, str), "parameter name must be a string") 4624 name_sym = to_symbol(name, self.ctx) 4625 if isinstance(val, bool): 4626 Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val) 4628 Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val) 4629 elif isinstance(val, float): 4630 Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val) 4631 elif isinstance(val, str): 4632 Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx)) 4635 _z3_assert(False, "invalid parameter value") 4638 return Z3_params_to_string(self.ctx.ref(), self.params) 4640 def validate(self, ds): 4641 _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected") 4642 Z3_params_validate(self.ctx.ref(), self.params, ds.descr) 4644 def args2params(arguments, keywords, ctx=None): 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.") 4666 class ParamDescrsRef: 4667 """Set of parameter descriptions
for Solvers, Tactics
and Simplifiers
in Z3.
4669 def __init__(self, descr, ctx=None): 4670 _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected") 4671 self.ctx = _get_ctx(ctx) 4673 Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr) 4676 if self.ctx.ref() is not None: 4677 Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr) 4680 """Return the size of
in the parameter description `self`.
4682 return int(Z3_param_descrs_size(self.ctx.ref(), self.descr)) 4685 """Return the size of
in the parameter description `self`.
4689 def get_name(self, i): 4690 """Return the i-th parameter name
in the parameter description `self`.
4692 return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i)) 4694 def get_kind(self, n): 4695 """Return the kind of the parameter named `n`.
4697 return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 4699 def get_documentation(self, n): 4700 """Return the documentation string of the parameter named `n`.
4702 return Z3_param_descrs_get_documentation(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) 4704 def __getitem__(self, arg): 4706 return self.get_name(arg) 4708 return self.get_kind(arg) 4711 return Z3_param_descrs_to_string(self.ctx.ref(), self.descr) 4713 ######################################### 4717 ######################################### 4719 class Goal(Z3PPObject): 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") 4730 self.ctx = _get_ctx(ctx) 4732 if self.goal is None: 4733 self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs) 4734 Z3_goal_inc_ref(self.ctx.ref(), self.goal) 4737 if self.goal is not None and self.ctx.ref() is not None: 4738 Z3_goal_dec_ref(self.ctx.ref(), self.goal) 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)
4755 return int(Z3_goal_depth(self.ctx.ref(), self.goal)) 4757 def inconsistent(self): 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()
4773 return Z3_goal_inconsistent(self.ctx.ref(), self.goal) 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
4794 return Z3_goal_precision(self.ctx.ref(), self.goal) 4796 def precision(self): 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)
4816 return int(Z3_goal_size(self.ctx.ref(), self.goal)) 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)
4842 return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx) 4844 def __getitem__(self, arg): 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) 4859 def assert_exprs(self, *args): 4860 """Assert constraints into the goal.
4864 >>> g.assert_exprs(x > 0, x < 2)
4868 args = _get_args(args) 4869 s = BoolSort(self.ctx) 4872 Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast()) 4874 def append(self, *args): 4879 >>> g.append(x > 0, x < 2)
4883 self.assert_exprs(*args) 4885 def insert(self, *args): 4890 >>> g.insert(x > 0, x < 2)
4894 self.assert_exprs(*args) 4896 def add(self, *args): 4901 >>> g.add(x > 0, x < 2)
4905 self.assert_exprs(*args) 4908 return obj_to_string(self) 4911 """Return a textual representation of the s-expression representing the goal.
""" 4912 return Z3_goal_to_string(self.ctx.ref(), self.goal) 4914 def translate(self, target): 4915 """Copy goal `self` to context `target`.
4923 >>> g2 = g.translate(c2)
4934 _z3_assert(isinstance(target, Context), "target must be a context") 4935 return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target) 4937 def simplify(self, *arguments, **keywords): 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()
4954 t = Tactic('simplify') 4955 return t.apply(self, *arguments, **keywords)[0] 4958 """Return goal `self`
as a single Z3 expression.
4973 return BoolVal(True, self.ctx) 4977 return And([ self.get(i) for i in range(len(self)) ], self.ctx) 4979 ######################################### 4983 ######################################### 4984 class AstVector(Z3PPObject): 4985 """A collection (vector) of ASTs.
""" 4987 def __init__(self, v=None, ctx=None): 4990 self.ctx = _get_ctx(ctx) 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)) 5015 def __getitem__(self, i): 5016 """Return the AST at position `i`.
5019 >>> A.push(
Int(
'x') + 1)
5020 >>> A.push(
Int(
'y'))
5026 if i >= self.__len__(): 5028 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx) 5030 def __setitem__(self, i, v): 5031 """Update AST at position `i`.
5034 >>> A.push(
Int(
'x') + 1)
5035 >>> A.push(
Int(
'y'))
5042 if i >= self.__len__(): 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()) 5058 def resize(self, sz): 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) 5071 def __contains__(self, item): 5072 """Return `
True`
if the vector contains `item`.
5094 def translate(self, other_ctx): 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) 5114 ######################################### 5118 ######################################### 5120 """A mapping
from ASTs to ASTs.
""" 5122 def __init__(self, m=None, ctx=None): 5125 self.ctx = _get_ctx(ctx) 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.
5148 return int(Z3_ast_map_size(self.ctx.ref(), self.map)) 5150 def __contains__(self, key): 5151 """Return `
True`
if the map contains key `key`.
5161 return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast()) 5163 def __getitem__(self, key): 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) 5174 def __setitem__(self, k, v): 5175 """Add/Update key `k` with value `v`.
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.
5220 Z3_ast_map_reset(self.ctx.ref(), self.map) 5223 """Return an AstVector containing all keys
in the map.
5232 return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx) 5234 ######################################### 5238 ######################################### 5241 """Store the value of the interpretation of a function
in a particular point.
""" 5243 def __init__(self, entry, ctx): 5246 Z3_func_entry_inc_ref(self.ctx.ref(), self.entry) 5249 if self.ctx.ref() is not None: 5250 Z3_func_entry_dec_ref(self.ctx.ref(), self.entry) 5253 """Return the number of arguments
in the given entry.
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)
5268 return int(Z3_func_entry_get_num_args(self.ctx.ref(), self.entry)) 5270 def arg_value(self, idx): 5271 """Return the value of argument `idx`.
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")
5297 if idx >= self.num_args(): 5299 return _to_expr_ref(Z3_func_entry_get_arg(self.ctx.ref(), self.entry, idx), self.ctx) 5302 """Return the value of the function at point `self`.
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)
5321 return _to_expr_ref(Z3_func_entry_get_value(self.ctx.ref(), self.entry), self.ctx) 5324 """Return entry `self`
as a Python list.
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)
5338 args = [ self.arg_value(i) for i in range(self.num_args())] 5339 args.append(self.value()) 5343 return repr(self.as_list()) 5345 class FuncInterp(Z3PPObject): 5346 """Stores the interpretation of a function
in a Z3 model.
""" 5348 def __init__(self, f, ctx): 5351 if self.f is not None: 5352 Z3_func_interp_inc_ref(self.ctx.ref(), self.f) 5355 if self.f is not None and self.ctx.ref() is not None: 5356 Z3_func_interp_dec_ref(self.ctx.ref(), self.f) 5358 def else_value(self): 5360 Return the `
else` value
for a function interpretation.
5361 Return
None if Z3 did
not specify the `
else` value
for 5366 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5371 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5375 r = Z3_func_interp_get_else(self.ctx.ref(), self.f) 5377 return _to_expr_ref(r, self.ctx) 5381 def num_entries(self): 5382 """Return the number of entries/points
in the function interpretation `self`.
5386 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5391 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5395 return int(Z3_func_interp_get_num_entries(self.ctx.ref(), self.f)) 5398 """Return the number of arguments
for each entry
in the function interpretation `self`.
5402 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5409 return int(Z3_func_interp_get_arity(self.ctx.ref(), self.f)) 5411 def entry(self, idx): 5412 """Return an entry at position `idx < self.
num_entries()`
in the function interpretation `self`.
5416 >>> s.add(
f(0) == 1,
f(1) == 1,
f(2) == 0)
5421 [0 -> 1, 1 -> 1, 2 -> 0,
else -> 1]
5431 if idx >= self.num_entries(): 5433 return FuncEntry(Z3_func_interp_get_entry(self.ctx.ref(), self.f, idx), self.ctx) 5436 """Return the function interpretation
as a Python list.
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]
5448 r = [ self.entry(i).as_list() for i in range(self.num_entries())] 5449 r.append(self.else_value()) 5453 return obj_to_string(self) 5455 class ModelRef(Z3PPObject): 5456 """Model/Solution of a satisfiability problem (aka system of constraints).
""" 5458 def __init__(self, m, ctx): 5459 assert ctx is not None 5462 Z3_model_inc_ref(self.ctx.ref(), self.model) 5465 if self.ctx.ref() is not None: 5466 Z3_model_dec_ref(self.ctx.ref(), self.model) 5469 return obj_to_string(self) 5472 """Return a textual representation of the s-expression representing the model.
""" 5473 return Z3_model_to_string(self.ctx.ref(), self.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)
5500 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r): 5501 return _to_expr_ref(r[0], self.ctx) 5502 raise Z3Exception("failed to evaluate expression in the model") 5504 def evaluate(self, t, model_completion=False): 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)
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`.
5536 >>> s.add(x > 0, f(x) != x)
5543 return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model)) 5545 def get_interp(self, decl): 5546 """Return the interpretation
for a given declaration
or constant.
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: 5566 _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast) 5567 if _r.value is None: 5569 r = _to_expr_ref(_r, self.ctx) 5571 return self.get_interp(get_as_array_func(r)) 5575 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) 5579 def num_sorts(self): 5580 """Return the number of unintepreted sorts that contain an interpretation
in the model `self`.
5583 >>> a, b =
Consts(
'a b', A)
5592 return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model)) 5594 def get_sort(self, idx): 5595 """Return the unintepreted sort at position `idx` < self.
num_sorts().
5599 >>> a1, a2 =
Consts(
'a1 a2', A)
5600 >>> b1, b2 =
Consts(
'b1 b2', B)
5602 >>> s.add(a1 != a2, b1 != b2)
5613 if idx >= self.num_sorts(): 5615 return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx) 5618 """Return all uninterpreted sorts that have an interpretation
in the model `self`.
5622 >>> a1, a2 =
Consts(
'a1 a2', A)
5623 >>> b1, b2 =
Consts(
'b1 b2', B)
5625 >>> s.add(a1 != a2, b1 != b2)
5632 return [ self.get_sort(i) for i in range(self.num_sorts()) ] 5634 def get_universe(self, s): 5635 """Return the intepretation
for the uninterpreted sort `s`
in the model `self`.
5638 >>> a, b =
Consts(
'a b', A)
5644 >>> m.get_universe(A)
5648 _z3_assert(isinstance(s, SortRef), "Z3 sort expected") 5650 return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx) 5654 def __getitem__(self, idx): 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.
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): 5683 num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model) 5684 if (idx < num_consts): 5685 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx) 5687 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx) 5688 if isinstance(idx, FuncDeclRef): 5689 return self.get_interp(idx) 5691 return self.get_interp(idx.decl()) 5692 if isinstance(idx, SortRef): 5693 return self.get_universe(idx) 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`.
5703 >>> s.add(x > 0, x < 2, f(x) == 0)
5711 for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)): 5712 r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx)) 5713 for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)): 5714 r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx)) 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()) 5721 def get_as_array_func(n): 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.") 5725 return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx) 5727 ######################################### 5731 ######################################### 5733 """Statistics
for `Solver.check()`.
""" 5735 def __init__(self, stats, ctx): 5738 Z3_stats_inc_ref(self.ctx.ref(), self.stats) 5741 if self.ctx.ref() is not None: 5742 Z3_stats_dec_ref(self.ctx.ref(), self.stats) 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() 5760 return Z3_stats_to_string(self.ctx.ref(), self.stats) 5763 """Return the number of statistical counters.
5766 >>> s =
Then(
'simplify',
'nlsat').solver()
5770 >>> st = s.statistics()
5774 return int(Z3_stats_size(self.ctx.ref(), self.stats)) 5776 def __getitem__(self, idx): 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): 5794 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 5795 val = int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 5797 val = Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 5798 return (Z3_stats_get_key(self.ctx.ref(), self.stats, idx), val) 5801 """Return the list of statistical counters.
5804 >>> s =
Then(
'simplify',
'nlsat').solver()
5808 >>> st = s.statistics()
5810 return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))] 5812 def get_key_value(self, key): 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)): 5825 if key == Z3_stats_get_key(self.ctx.ref(), self.stats, idx): 5826 if Z3_stats_is_uint(self.ctx.ref(), self.stats, idx): 5827 return int(Z3_stats_get_uint_value(self.ctx.ref(), self.stats, idx)) 5829 return Z3_stats_get_double_value(self.ctx.ref(), self.stats, idx) 5830 raise Z3Exception("unknown key") 5832 def __getattr__(self, name): 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('_', ' ') 5851 return self.get_key_value(key) 5853 raise AttributeError 5855 ######################################### 5859 ######################################### 5860 class CheckSatResult: 5861 """Represents the result of a satisfiability check: sat, unsat, unknown.
5867 >>> isinstance(r, CheckSatResult)
5871 def __init__(self, r): 5874 def __eq__(self, other): 5875 return isinstance(other, CheckSatResult) and self.r == other.r 5877 def __ne__(self, other): 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: 5896 sat = CheckSatResult(Z3_L_TRUE) 5897 unsat = CheckSatResult(Z3_L_FALSE) 5898 unknown = CheckSatResult(Z3_L_UNDEF) 5900 class Solver(Z3PPObject): 5901 """Solver API provides methods
for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.
""" 5903 def __init__(self, solver=None, ctx=None): 5904 assert solver is None or ctx is not None 5905 self.ctx = _get_ctx(ctx) 5908 self.solver = Z3_mk_solver(self.ctx.ref()) 5910 self.solver = solver 5911 Z3_solver_inc_ref(self.ctx.ref(), self.solver) 5914 if self.solver is not None and self.ctx.ref() is not None: 5915 Z3_solver_dec_ref(self.ctx.ref(), self.solver) 5917 def set(self, *args, **keys): 5918 """Set a configuration option. The method `
help()`
return a string containing all available options.
5922 >>> s.set(mbqi=
True)
5923 >>> s.set(
'MBQI',
True)
5924 >>> s.set(
':mbqi',
True)
5926 p = args2params(args, keys, self.ctx) 5927 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params) 5930 """Create a backtracking point.
5949 Z3_solver_push(self.ctx.ref(), self.solver) 5951 def pop(self, num=1): 5952 """Backtrack \c num backtracking points.
5971 Z3_solver_pop(self.ctx.ref(), self.solver, num) 5974 """Remove all asserted constraints
and backtracking points created using `
push()`.
5985 Z3_solver_reset(self.ctx.ref(), self.solver) 5987 def assert_exprs(self, *args): 5988 """Assert constraints into the solver.
5992 >>> s.assert_exprs(x > 0, x < 2)
5996 args = _get_args(args) 5997 s = BoolSort(self.ctx) 5999 if isinstance(arg, Goal) or isinstance(arg, AstVector): 6001 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast()) 6004 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast()) 6006 def add(self, *args): 6007 """Assert constraints into the solver.
6011 >>> s.add(x > 0, x < 2)
6015 self.assert_exprs(*args) 6017 def __iadd__(self, fml): 6021 def append(self, *args): 6022 """Assert constraints into the solver.
6026 >>> s.append(x > 0, x < 2)
6030 self.assert_exprs(*args) 6032 def insert(self, *args): 6033 """Assert constraints into the solver.
6037 >>> s.insert(x > 0, x < 2)
6041 self.assert_exprs(*args) 6043 def assert_and_track(self, a, p): 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): 6068 p = Bool(p, self.ctx) 6069 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected") 6070 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected") 6071 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast()) 6073 def check(self, *assumptions): 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() 6098 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions) 6099 return CheckSatResult(r) 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)
6116 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx) 6118 raise Z3Exception("model is not available") 6120 def unsat_core(self): 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')
6134 >>> s.add(
Implies(p3, y > -3))
6135 >>> s.check(p1, p2, p3)
6137 >>> core = s.unsat_core()
6150 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx) 6152 def consequences(self, assumptions, variables): 6153 """Determine fixed values
for the variables based on the solver state
and assumptions.
6155 >>> a, b, c, d =
Bools(
'a b c d')
6157 >>> s.consequences([a],[b,c,d])
6159 >>> s.consequences([
Not(c),d],[a,b,c,d])
6162 if isinstance(assumptions, list): 6163 _asms = AstVector(None, self.ctx) 6164 for a in assumptions: 6167 if isinstance(variables, list): 6168 _vars = AstVector(None, self.ctx) 6172 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected") 6173 _z3_assert(isinstance(variables, AstVector), "ast vector expected") 6174 consequences = AstVector(None, self.ctx) 6175 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector) 6176 sz = len(consequences) 6177 consequences = [ consequences[i] for i in range(sz) ] 6178 return CheckSatResult(r), consequences 6181 """Return a proof
for the last `
check()`. Proof construction must be enabled.
""" 6182 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx) 6184 def assertions(self): 6185 """Return an AST vector containing all added constraints.
6196 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx) 6198 def statistics(self): 6199 """Return statistics
for the last `
check()`.
6206 >>> st = s.statistics()
6207 >>> st.get_key_value(
'final checks')
6214 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx) 6216 def reason_unknown(self): 6217 """Return a string describing why the last `
check()` returned `unknown`.
6221 >>> s.add(2**x == 4)
6224 >>> s.reason_unknown()
6225 '(incomplete (theory arithmetic))' 6227 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver) 6230 """Display a string describing all available options.
""" 6231 print(Z3_solver_get_help(self.ctx.ref(), self.solver)) 6233 def param_descrs(self): 6234 """Return the parameter description set.
""" 6235 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx) 6238 """Return a formatted string with all added constraints.
""" 6239 return obj_to_string(self) 6241 def translate(self, target): 6242 """Translate `self` to the context `target`. That
is,
return a copy of `self`
in the context `target`.
6247 >>> s2 = s1.translate(c2)
6250 _z3_assert(isinstance(target, Context), "argument must be a Z3 context") 6251 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref()) 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.
6263 return Z3_solver_to_string(self.ctx.ref(), self.solver) 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) 7877 return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) 7879 def parse_smt2_file(f, sorts={}, decls={}, ctx=None): 7880 """Parse a file
in SMT 2.0 format using the given sorts
and decls.
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) 7889 def Interpolant(a,ctx=None): 7890 """Create an interpolation operator.
7892 The argument
is an interpolation pattern (see tree_interpolant).
7898 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) 7901 return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx) 7903 def tree_interpolant(pat,p=None,ctx=None): 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.
7945 [
Not(x >= 0),
Not(y <= 2)]
7952 (define-fun x () Int
7956 ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx)) 7957 ptr = (AstVectorObj * 1)() 7958 mptr = (Model * 1)() 7961 res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr) 7962 if res == Z3_L_FALSE: 7963 return AstVector(ptr[0],ctx) 7965 raise ModelRef(mptr[0], ctx) 7968 def binary_interpolant(a,b,p=None,ctx=None): 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.
7992 f = And(Interpolant(a),b) 7993 ti = tree_interpolant(f,p,ctx) 7994 return ti[0] if ti is not None else None 7996 def sequence_interpolant(v,p=None,ctx=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.
8022 [
Not(x >= 0),
Not(y >= 0)]
8025 for i in range(1,len(v)): 8026 f = And(Interpolant(f),v[i]) 8027 return tree_interpolant(f,p,ctx) 8030 ######################################### 8032 # Floating-Point Arithmetic 8034 ######################################### 8037 # Global default rounding mode 8038 _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO 8039 _dflt_fpsort_ebits = 11 8040 _dflt_fpsort_sbits = 53 8042 def get_default_rounding_mode(ctx=None): 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: 8056 def set_default_rounding_mode(rm, ctx=None): 8057 global _dflt_rounding_mode 8058 if is_fprm_value(rm): 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 8069 def get_default_fp_sort(ctx=None): 8070 return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx) 8072 def set_default_fp_sort(ebits, sbits, ctx=None): 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): 8079 return get_default_rounding_mode(ctx) 8081 def _dflt_fps(ctx=None): 8082 return get_default_fp_sort(ctx) 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(): 8091 pass # OK, same as before 8093 # we saw at least 2 different float sorts; something will 8094 # throw a sort mismatch later, for now assume None. 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) 8110 class FPSortRef(SortRef): 8111 """Floating-point sort.
""" 8114 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint sort `self`.
8119 return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast)) 8122 """Retrieves the number of bits reserved
for the significand
in the FloatingPoint sort `self`.
8127 return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast)) 8129 def cast(self, val): 8130 """Try to cast `val`
as a floating-point expression.
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) 8145 def Float16(ctx=None): 8146 """Floating-point 16-bit (half) sort.
""" 8148 return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx) 8150 def FloatHalf(ctx=None): 8151 """Floating-point 16-bit (half) sort.
""" 8153 return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx) 8155 def Float32(ctx=None): 8156 """Floating-point 32-bit (single) sort.
""" 8158 return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx) 8160 def FloatSingle(ctx=None): 8161 """Floating-point 32-bit (single) sort.
""" 8163 return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx) 8165 def Float64(ctx=None): 8166 """Floating-point 64-bit (double) sort.
""" 8168 return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx) 8170 def FloatDouble(ctx=None): 8171 """Floating-point 64-bit (double) sort.
""" 8173 return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx) 8175 def Float128(ctx=None): 8176 """Floating-point 128-bit (quadruple) sort.
""" 8178 return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx) 8180 def FloatQuadruple(ctx=None): 8181 """Floating-point 128-bit (quadruple) sort.
""" 8183 return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx) 8185 class FPRMSortRef(SortRef): 8186 """"Floating-point rounding mode sort.""" 8190 """Return True if `s` is a Z3 floating-point sort.
8197 return isinstance(s, FPSortRef) 8199 def is_fprm_sort(s): 8200 """Return
True if `s`
is a Z3 floating-point rounding mode sort.
8207 return isinstance(s, FPRMSortRef) 8211 class FPRef(ExprRef): 8212 """Floating-point expressions.
""" 8215 """Return the sort of the floating-point expression `self`.
8220 >>> x.sort() ==
FPSort(8, 24)
8223 return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 8226 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8231 return self.sort().ebits(); 8234 """Retrieves the number of bits reserved
for the exponent
in the FloatingPoint expression `self`.
8239 return self.sort().sbits(); 8241 def as_string(self): 8242 """Return a Z3 floating point expression
as a Python string.
""" 8243 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8245 def __le__(self, other): 8246 return fpLEQ(self, other, self.ctx) 8248 def __lt__(self, other): 8249 return fpLT(self, other, self.ctx) 8251 def __ge__(self, other): 8252 return fpGEQ(self, other, self.ctx) 8254 def __gt__(self, other): 8255 return fpGT(self, other, self.ctx) 8257 def __add__(self, other): 8258 """Create the Z3 expression `self + other`.
8267 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8268 return fpAdd(_dflt_rm(), a, b, self.ctx) 8270 def __radd__(self, other): 8271 """Create the Z3 expression `other + self`.
8277 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8278 return fpAdd(_dflt_rm(), a, b, self.ctx) 8280 def __sub__(self, other): 8281 """Create the Z3 expression `self - other`.
8290 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8291 return fpSub(_dflt_rm(), a, b, self.ctx) 8293 def __rsub__(self, other): 8294 """Create the Z3 expression `other - self`.
8300 [a, b] = _coerce_fp_expr_list([other, self], self.ctx) 8301 return fpSub(_dflt_rm(), a, b, self.ctx) 8303 def __mul__(self, other): 8304 """Create the Z3 expression `self * other`.
8315 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8316 return fpMul(_dflt_rm(), a, b, self.ctx) 8318 def __rmul__(self, other): 8319 """Create the Z3 expression `other * self`.
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`.
8344 def __div__(self, other): 8345 """Create the Z3 expression `self / other`.
8356 [a, b] = _coerce_fp_expr_list([self, other], self.ctx) 8357 return fpDiv(_dflt_rm(), a, b, self.ctx) 8359 def __rdiv__(self, other): 8360 """Create the Z3 expression `other / self`.
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': 8373 def __truediv__(self, other): 8374 """Create the Z3 expression division `self / other`.
""" 8375 return self.__div__(other) 8377 def __rtruediv__(self, other): 8378 """Create the Z3 expression division `other / self`.
""" 8379 return self.__rdiv__(other) 8381 def __mod__(self, other): 8382 """Create the Z3 expression mod `self % other`.
""" 8383 return fpRem(self, other) 8385 def __rmod__(self, other): 8386 """Create the Z3 expression mod `other % self`.
""" 8387 return fpRem(other, self) 8389 class FPRMRef(ExprRef): 8390 """Floating-point rounding mode expressions
""" 8392 def as_string(self): 8393 """Return a Z3 floating point expression
as a Python string.
""" 8394 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 8397 def RoundNearestTiesToEven(ctx=None): 8399 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8403 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx) 8405 def RoundNearestTiesToAway(ctx=None): 8407 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8411 return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx) 8413 def RoundTowardPositive(ctx=None): 8415 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8419 return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx) 8421 def RoundTowardNegative(ctx=None): 8423 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8427 return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx) 8429 def RoundTowardZero(ctx=None): 8431 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8435 return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx) 8438 """Return `
True`
if `a`
is a Z3 floating-point rounding mode expression.
8447 return isinstance(a, FPRMRef) 8449 def is_fprm_value(a): 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) 8455 class FPNumRef(FPRef): 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 8465 def isNegative(self): 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.
8480 l = (ctypes.c_int)() 8481 if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False: 8482 raise Z3Exception("error retrieving the sign of a numeral.") 8486 The significand of the numeral.
8492 def significand(self): 8493 return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast()) 8496 The exponent of the numeral.
8503 return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast()) 8506 The exponent of the numeral
as a long.
8509 >>> x.exponent_as_long()
8512 def exponent_as_long(self): 8513 ptr = (ctypes.c_longlong * 1)() 8514 if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr): 8515 raise Z3Exception("error retrieving the exponent of a numeral.") 8519 The string representation of the numeral.
8525 def as_string(self): 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.
8540 return isinstance(a, FPRef) 8543 """Return `
True`
if `a`
is a Z3 floating-point numeral value.
8554 return is_fp(a) and _is_numeral(a.ctx, a.ast) 8556 def FPSort(ebits, sbits, ctx=None): 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)
8568 return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx) 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.
8618 >>> set_fpa_pretty(
True)
8621 >>> pb = get_fpa_pretty()
8622 >>> set_fpa_pretty(
False)
8625 >>> set_fpa_pretty(pb)
8627 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8628 return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx) 8630 def fpPlusInfinity(s): 8631 """Create a Z3 floating-point +oo term.
8634 >>> pb = get_fpa_pretty()
8635 >>> set_fpa_pretty(
True)
8638 >>> set_fpa_pretty(
False)
8641 >>> set_fpa_pretty(pb)
8643 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8644 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx) 8646 def fpMinusInfinity(s): 8647 """Create a Z3 floating-point -oo term.
""" 8648 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8649 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx) 8651 def fpInfinity(s, negative): 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") 8655 return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx) 8658 """Create a Z3 floating-point +0.0 term.
""" 8659 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8660 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx) 8663 """Create a Z3 floating-point -0.0 term.
""" 8664 _z3_assert(isinstance(s, FPSortRef), "sort mismatch") 8665 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx) 8667 def fpZero(s, negative): 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") 8671 return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx) 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.
8679 >>> print(
"0x%.8x" % v.exponent_as_long())
8699 fps = _dflt_fps(ctx) 8700 _z3_assert(is_fp_sort(fps), "sort mismatch") 8703 val = _to_float_str(sig) 8704 if val == "NaN" or val == "nan": 8707 return fpMinusZero(fps) 8708 elif val == "0.0" or val == "+0.0": 8709 return fpPlusZero(fps) 8710 elif val == "+oo" or val == "+inf" or val == "+Inf": 8711 return fpPlusInfinity(fps) 8712 elif val == "-oo" or val == "-inf" or val == "-Inf": 8713 return fpMinusInfinity(fps) 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.
8730 >>> x2 =
FP(
'x', word)
8734 if isinstance(fpsort, FPSortRef) and ctx is None: 8738 return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx) 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))
8754 if isinstance(names, str): 8755 names = names.split(" ") 8756 return [FP(name, fpsort, ctx) for name in names] 8758 def fpAbs(a, ctx=None): 8759 """Create a Z3 floating-point absolute value expression.
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) 8778 return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx) 8780 def fpNeg(a, ctx=None): 8781 """Create a Z3 floating-point addition expression.
8792 [a] = _coerce_fp_expr_list([a], ctx) 8793 return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), 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) 8847 def fpAdd(rm, a, b, ctx=None): 8848 """Create a Z3 floating-point addition expression.
8858 >>>
fpAdd(rm, x, y).sort()
8861 return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx) 8863 def fpSub(rm, a, b, ctx=None): 8864 """Create a Z3 floating-point subtraction expression.
8872 >>>
fpSub(rm, x, y).sort()
8875 return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx) 8877 def fpMul(rm, a, b, ctx=None): 8878 """Create a Z3 floating-point multiplication expression.
8886 >>>
fpMul(rm, x, y).sort()
8889 return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx) 8891 def fpDiv(rm, a, b, ctx=None): 8892 """Create a Z3 floating-point divison expression.
8900 >>>
fpDiv(rm, x, y).sort()
8903 return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx) 8905 def fpRem(a, b, ctx=None): 8906 """Create a Z3 floating-point remainder expression.
8913 >>>
fpRem(x, y).sort()
8916 return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx) 8918 def fpMin(a, b, ctx=None): 8919 """Create a Z3 floating-point minimium expression.
8927 >>>
fpMin(x, y).sort()
8930 return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx) 8932 def fpMax(a, b, ctx=None): 8933 """Create a Z3 floating-point maximum expression.
8941 >>>
fpMax(x, y).sort()
8944 return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx) 8946 def fpFMA(rm, a, b, c, ctx=None): 8947 """Create a Z3 floating-point fused multiply-add expression.
8949 return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx) 8951 def fpSqrt(rm, a, ctx=None): 8952 """Create a Z3 floating-point square root expression.
8954 return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx) 8956 def fpRoundToIntegral(rm, a, ctx=None): 8957 """Create a Z3 floating-point roundToIntegral expression.
8959 return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx) 8961 def fpIsNaN(a, ctx=None): 8962 """Create a Z3 floating-point isNaN expression.
8970 return _mk_fp_unary_norm(Z3_mk_fpa_is_nan, a, ctx) 8972 def fpIsInf(a, ctx=None): 8973 """Create a Z3 floating-point isInfinite expression.
8980 return _mk_fp_unary_norm(Z3_mk_fpa_is_infinite, a, ctx) 8982 def fpIsZero(a, ctx=None): 8983 """Create a Z3 floating-point isZero expression.
8985 return _mk_fp_unary_norm(Z3_mk_fpa_is_zero, a, ctx) 8987 def fpIsNormal(a, ctx=None): 8988 """Create a Z3 floating-point isNormal expression.
8990 return _mk_fp_unary_norm(Z3_mk_fpa_is_normal, a, ctx) 8992 def fpIsSubnormal(a, ctx=None): 8993 """Create a Z3 floating-point isSubnormal expression.
8995 return _mk_fp_unary_norm(Z3_mk_fpa_is_subnormal, a, ctx) 8997 def fpIsNegative(a, ctx=None): 8998 """Create a Z3 floating-point isNegative expression.
9000 return _mk_fp_unary_norm(Z3_mk_fpa_is_negative, a, ctx) 9002 def fpIsPositive(a, ctx=None): 9003 """Create a Z3 floating-point isPositive expression.
9005 return _mk_fp_unary_norm(Z3_mk_fpa_is_positive, a, ctx) 9006 return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), 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") 9012 def fpLT(a, b, ctx=None): 9013 """Create the Z3 floating-point expression `other < self`.
9021 return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx) 9023 def fpLEQ(a, b, ctx=None): 9024 """Create the Z3 floating-point expression `other <= self`.
9029 >>> (x <= y).sexpr()
9032 return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx) 9034 def fpGT(a, b, ctx=None): 9035 """Create the Z3 floating-point expression `other > self`.
9043 return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx) 9045 def fpGEQ(a, b, ctx=None): 9046 """Create the Z3 floating-point expression `other >= self`.
9051 >>> (x >= y).sexpr()
9054 return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx) 9056 def fpEQ(a, b, ctx=None): 9057 """Create the Z3 floating-point expression `
fpEQ(other, self)`.
9062 >>>
fpEQ(x, y).sexpr()
9065 return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx) 9067 def fpNEQ(a, b, ctx=None): 9068 """Create the Z3 floating-point expression `
Not(
fpEQ(other, self))`.
9073 >>> (x != y).sexpr()
9076 return Not(fpEQ(a, b, ctx)) 9078 def fpFP(sgn, exp, sig, ctx=None): 9079 """Create the Z3 floating-point value `
fpFP(sgn, sig, exp)`
from the three bit-vectors sgn, sig,
and exp.
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))
9100 _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch") 9101 _z3_assert(sgn.sort().size() == 1, "sort mismatch") 9103 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch") 9104 return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx) 9106 def fpToFP(a1, a2=None, a3=None, ctx=None): 9107 """Create a Z3 floating-point conversion expression
from other term sorts
9110 From a bit-vector term
in IEEE 754-2008 format:
9116 From a floating-point term with different precision:
9127 From a signed bit-vector term:
9133 if is_bv(a1) and is_fp_sort(a2): 9134 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx) 9135 elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3): 9136 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9137 elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3): 9138 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9139 elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3): 9140 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx) 9142 raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.") 9144 def fpBVToFP(v, sort, ctx=None): 9145 """Create a Z3 floating-point conversion expression that represents the
9146 conversion
from a bit-vector term to a floating-point term.
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.") 9158 return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx) 9160 def fpFPToFP(rm, v, sort, ctx=None): 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.
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.") 9177 return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9179 def fpRealToFP(rm, v, sort, ctx=None): 9180 """Create a Z3 floating-point conversion expression that represents the
9181 conversion
from a real term to a floating-point term.
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.") 9194 return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9196 def fpSignedToFP(rm, v, sort, ctx=None): 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.
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.") 9211 return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9213 def fpUnsignedToFP(rm, v, sort, ctx=None): 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.
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.") 9228 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) 9230 def fpToFPUnsigned(rm, x, s, ctx=None): 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") 9237 return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx) 9239 def fpToSBV(rm, x, s, ctx=None): 9240 """Create a Z3 floating-point conversion expression,
from floating-point expression to signed bit-vector.
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") 9258 return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9260 def fpToUBV(rm, x, s, ctx=None): 9261 """Create a Z3 floating-point conversion expression,
from floating-point expression to unsigned bit-vector.
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") 9279 return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx) 9281 def fpToReal(x, ctx=None): 9282 """Create a Z3 floating-point conversion expression,
from floating-point expression to real.
9296 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9298 return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx) 9300 def fpToIEEEBV(x, ctx=None): 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
9321 _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression") 9323 return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx) 9327 ######################################### 9329 # Strings, Sequences and Regular expressions 9331 ######################################### 9333 class SeqSortRef(SortRef): 9334 """Sequence sort.
""" 9336 def is_string(self): 9337 """Determine
if sort
is a string
9345 return Z3_is_string_sort(self.ctx_ref(), self.ast) 9347 def StringSort(ctx=None): 9348 """Create a string sort
9354 return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx) 9358 """Create a sequence sort over elements provided
in the argument
9363 return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx) 9365 class SeqRef(ExprRef): 9366 """Sequence expression.
""" 9369 return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) 9371 def __add__(self, other): 9372 return Concat(self, other) 9374 def __radd__(self, other): 9375 return Concat(other, self) 9377 def __getitem__(self, i): 9379 i = IntVal(i, self.ctx) 9380 return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) 9382 def is_string(self): 9383 return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast())) 9385 def is_string_value(self): 9386 return Z3_is_string(self.ctx_ref(), self.as_ast()) 9388 def as_string(self): 9389 """Return a string representation of sequence expression.
""" 9390 return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) 9393 def _coerce_seq(s, ctx=None): 9394 if isinstance(s, str): 9396 s = StringVal(s, ctx) 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.
9419 return isinstance(a, SeqRef) 9422 """Return `
True`
if `a`
is a Z3 string expression.
9426 return isinstance(a, SeqRef) and a.is_string() 9428 def is_string_value(a): 9429 """return 'True' if 'a' is a Z3 string constant expression.
9435 return isinstance(a, SeqRef) and a.is_string_value() 9438 def StringVal(s, ctx=None): 9439 """create a string expression
""" 9441 return SeqRef(Z3_mk_string(ctx.ref(), s), ctx) 9443 def String(name, ctx=None): 9444 """Return a string constant named `name`. If `ctx=
None`, then the
global context
is used.
9449 return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx) 9451 def Strings(names, ctx=None): 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
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' 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' 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' 9512 >>> x, y, z =
Strings(
'x y z')
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) 9523 def Replace(s, src, dst): 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) 9537 def IndexOf(s, substr): 9538 return IndexOf(s, substr, IntVal(0)) 9540 def IndexOf(s, substr, offset): 9541 """Retrieve the index of substring within a string starting at a specified offset.
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' 9564 return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx) 9566 def Re(s, ctx=None): 9567 """The regular expression that accepts sequence
's' 9572 s = _coerce_seq(s, ctx) 9573 return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx) 9578 ## Regular expressions 9580 class ReSortRef(SortRef): 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") 9593 class ReRef(ExprRef): 9594 """Regular expressions.
""" 9596 def __add__(self, other): 9597 return Union(self, other) 9601 return isinstance(s, ReRef) 9605 """Create regular expression membership test
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.
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.
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.
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.
9670 return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)
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_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
def simplify(a, arguments, keywords)
Utils.
Z3_bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
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 update_rule(self, head, body, name)
def args2params(arguments, keywords, ctx=None)
def get_cover_delta(self, level, predicate)
def RatVal(a, b, ctx=None)
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
def __getitem__(self, idx)
def RealVector(prefix, sz, ctx=None)
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1...
Z3_string Z3_API Z3_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.
def fpBVToFP(v, sort, ctx=None)
def FPs(names, fpsort, ctx=None)
def FPVal(sig, exp=None, fps=None, ctx=None)
def RealVarVector(n, ctx=None)
def substitute_vars(t, m)
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
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 declare(self, name, args)
def assert_exprs(self, args)
def set_option(args, kws)
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
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...
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
def parse_smt2_string(s, sorts={}, decls={}, ctx=None)
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.
def __init__(self, ctx=None)
def fpToFP(a1, a2=None, a3=None, ctx=None)
def assert_exprs(self, args)
def fpUnsignedToFP(rm, v, sort, ctx=None)
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].
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
def register_relation(self, relations)
def fpToUBV(rm, x, s, ctx=None)
def fpGEQ(a, b, ctx=None)
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)
Return the name of the idx tactic.
def rule(self, head, body=None, name=None)
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 fpRem(a, b, ctx=None)
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
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 is_finite_domain_sort(s)
def BoolVector(prefix, sz, ctx=None)
def Array(name, dom, rng)
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.
def Cond(p, t1, t2, ctx=None)
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
def fpMax(a, b, ctx=None)
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
def __init__(self, fixedpoint=None, ctx=None)
def simplify_param_descrs()
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)
def BitVec(name, bv, ctx=None)
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_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_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...
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
def binary_interpolant(a, b, p=None, ctx=None)
def fpSignedToFP(rm, v, sort, ctx=None)
def fact(self, head, name=None)
Z3_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_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
def __init__(self, args, kws)
def ParAndThen(t1, t2, ctx=None)
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...
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.
def RealVal(val, ctx=None)
def Extract(high, low, a)
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=[])
def solve_using(s, args, keywords)
def set_predicate_representation(self, f, representations)
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 add_soft(self, arg, weight="1", id=None)
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
def Implies(a, b, ctx=None)
def __init__(self, tactic, ctx=None)
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.
def apply(self, goal, arguments, keywords)
def solve(args, keywords)
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.
def check(self, assumptions)
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)
def __call__(self, goal, arguments, keywords)
def FiniteDomainVal(val, sort, ctx=None)
def FPSort(ebits, sbits, ctx=None)
def prove(claim, keywords)
def DeclareSort(name, ctx=None)
def Ints(names, ctx=None)
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 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.
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.
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new (incremental) solver.
def FP(name, fpsort, ctx=None)
def fpToSBV(rm, x, s, ctx=None)
def fpDiv(rm, a, b, ctx=None)
def BitVecs(names, bv, ctx=None)
def translate(self, target)
def from_file(self, filename)
def __init__(self, probe, ctx=None)
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.
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...
def Strings(names, ctx=None)
def fpSub(rm, a, b, ctx=None)
def fpFP(sgn, exp, sig, ctx=None)
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
def parse_string(self, s)
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...
def declare_var(self, vars)
def add_rule(self, head, body=None, name=None)
def __rmul__(self, other)
def BoolVal(val, ctx=None)
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_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
def fpMin(a, b, ctx=None)
def FreshInt(prefix='x', ctx=None)
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 BitVecSort(sz, ctx=None)
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...
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 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.
def TryFor(t, ms, ctx=None)
def sequence_interpolant(v, p=None, ctx=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...
def __init__(self, ast, ctx=None)
def convert_model(self, model, idx=0)
def __init__(self, result, ctx)
def abstract(self, fml, is_forall=True)
def set(self, args, keys)
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
def fpToReal(x, ctx=None)
Z3_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...
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 Reals(names, ctx=None)
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
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...
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 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)
def SolverFor(logic, ctx=None)
def ParThen(t1, t2, ctx=None)
def set(self, args, keys)
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
void Z3_API Z3_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_...
def fpRealToFP(rm, v, sort, ctx=None)
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.
def String(name, ctx=None)
Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
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...
def SimpleSolver(ctx=None)