RetroSearch Browse

ctx = _get_ctx(ctx)

351 if

self.

ctx.ref()

is not None and

self.

is not None and

Z3_dec_ref

is not None

356 return

_to_ast_ref(self.

ast, self.

ctx)

359 return

obj_to_string(self)

362 return

obj_to_string(self)

365 return

self.

eq(other)

368 return

self.

hash

hash()

378 elif is_eq

(self)

and

self.num_args() == 2:

379 return

self.arg(0).

(self.arg(1))

381 raise

Z3Exception(

"Symbolic expressions cannot be cast to concrete Boolean values."

)

384 """Return a string representing the AST node in s-expression notation. 387 >>> ((x + 1)*x).sexpr() 393 """Return a pointer to the corresponding C Z3_ast object.""" 397 """Return unique identifier for object. It can be used for hash-tables and maps.""" 401 """Return a reference to the C context where this AST node is stored.""" 402 return

self.

ctx.ref()

404 def eq

(self, other):

405 """Return `True` if `self` and `other` are structurally identical. 412 >>> n1 = simplify(n1) 413 >>> n2 = simplify(n2) 418

_z3_assert(

is_ast

(other),

"Z3 AST expected"

)

422 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 428 >>> # Nodes in different contexts can't be mixed. 429 >>> # However, we can translate nodes from one context to another. 430 >>> x.translate(c2) + y 434

_z3_assert(isinstance(target, Context),

"argument must be a Z3 context"

)

441 """Return a hashcode for the `self`. 443 >>> n1 = simplify(Int('x') + 1) 444 >>> n2 = simplify(2 + Int('x') - 1) 445 >>> n1.hash() == n2.hash() 452 """Return `True` if `a` is an AST node. 456 >>> is_ast(IntVal(10)) 460 >>> is_ast(BoolSort()) 462 >>> is_ast(Function('f', IntSort(), IntSort())) 469 return

isinstance(a, AstRef)

473 """Return `True` if `a` and `b` are structurally identical AST nodes. 483 >>> eq(simplify(x + 1), simplify(1 + x)) 487

_z3_assert(

is_ast

(a)

and is_ast

(b),

"Z3 ASTs expected"

)

491 def

_ast_kind(ctx, a):

497 def

_ctx_from_ast_arg_list(args, default_ctx=None):

505

_z3_assert(ctx == a.ctx,

"Context mismatch"

)

511 def

_ctx_from_ast_args(*args):

512 return

_ctx_from_ast_arg_list(args)

515 def

_to_func_decl_array(args):

517

_args = (FuncDecl * sz)()

519

_args[i] = args[i].as_func_decl()

523 def

_to_ast_array(args):

527

_args[i] = args[i].as_ast()

531 def

_to_ref_array(ref, args):

535

_args[i] = args[i].as_ast()

539 def

_to_ast_ref(a, ctx):

540

k = _ast_kind(ctx, a)

542 return

_to_sort_ref(a, ctx)

543 elif

k == Z3_FUNC_DECL_AST:

544 return

_to_func_decl_ref(a, ctx)

546 return

_to_expr_ref(a, ctx)

555 def

_sort_kind(ctx, s):

560 """A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.""" 569 """Return the Z3 internal kind of a sort. 570 This method can be used to test if `self` is one of the Z3 builtin sorts. 573 >>> b.kind() == Z3_BOOL_SORT 575 >>> b.kind() == Z3_INT_SORT 577 >>> A = ArraySort(IntSort(), IntSort()) 578 >>> A.kind() == Z3_ARRAY_SORT 580 >>> A.kind() == Z3_INT_SORT 583 return

_sort_kind(self.

ctx, self.

ast)

586 """Return `True` if `self` is a subsort of `other`. 588 >>> IntSort().subsort(RealSort()) 594 """Try to cast `val` as an element of sort `self`. 596 This method is used in Z3Py to convert Python objects such as integers, 597 floats, longs and strings into Z3 expressions. 600 >>> RealSort().cast(x) 604

_z3_assert(

(val),

"Z3 expression expected"

)

605

_z3_assert(self.

eq(val.sort()),

"Sort mismatch"

)

609 """Return the name (string) of sort `self`. 611 >>> BoolSort().name() 613 >>> ArraySort(IntSort(), IntSort()).name() 619 """Return `True` if `self` and `other` are the same Z3 sort. 622 >>> p.sort() == BoolSort() 624 >>> p.sort() == IntSort() 632 """Return `True` if `self` and `other` are not the same Z3 sort. 635 >>> p.sort() != BoolSort() 637 >>> p.sort() != IntSort() 644 return

AstRef.__hash__(self)

648 """Return `True` if `s` is a Z3 sort. 650 >>> is_sort(IntSort()) 652 >>> is_sort(Int('x')) 654 >>> is_expr(Int('x')) 657 return

isinstance(s, SortRef)

660 def

_to_sort_ref(s, ctx):

662

_z3_assert(isinstance(s, Sort),

"Z3 Sort expected"

)

663

k = _sort_kind(ctx, s)

664 if

k == Z3_BOOL_SORT:

666 elif

k == Z3_INT_SORT

or

k == Z3_REAL_SORT:

668 elif

k == Z3_BV_SORT:

670 elif

k == Z3_ARRAY_SORT:

672 elif

k == Z3_DATATYPE_SORT:

674 elif

k == Z3_FINITE_DOMAIN_SORT:

676 elif

k == Z3_FLOATING_POINT_SORT:

678 elif

k == Z3_ROUNDING_MODE_SORT:

680 elif

k == Z3_RE_SORT:

682 elif

k == Z3_SEQ_SORT:

684 elif

k == Z3_CHAR_SORT:

686 elif

k == Z3_TYPE_VAR:

692 return

_to_sort_ref(

Z3_get_sort

(ctx.ref(), a), ctx)

696 """Create a new uninterpreted sort named `name`. 698 If `ctx=None`, then the new sort is declared in the global Z3Py context. 700 >>> A = DeclareSort('A') 701 >>> a = Const('a', A) 702 >>> b = Const('b', A) 714 """Type variable reference""" 724 """Create a new type variable named `name`. 726 If `ctx=None`, then the new sort is declared in the global Z3Py context. 741 """Function declaration. Every constant and function have an associated declaration. 743 The declaration assigns a name, a sort (i.e., type), and for function 744 the sort (i.e., type) of each of its arguments. Note that, in Z3, 745 a constant is a function with 0 arguments. 758 """Return the name of the function declaration `self`. 760 >>> f = Function('f', IntSort(), IntSort()) 763 >>> isinstance(f.name(), str) 769 """Return the number of arguments of a function declaration. 770 If `self` is a constant, then `self.arity()` is 0. 772 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 779 """Return the sort of the argument `i` of a function declaration. 780 This method assumes that `0 <= i < self.arity()`. 782 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 791 """Return the sort of the range of a function declaration. 792 For constants, this is the sort of the constant. 794 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 801 """Return the internal kind of a function declaration. 802 It can be used to identify Z3 built-in functions such as addition, multiplication, etc. 805 >>> d = (x + 1).decl() 806 >>> d.kind() == Z3_OP_ADD 808 >>> d.kind() == Z3_OP_MUL 816

result = [

None for

in range

(n)]

819 if

k == Z3_PARAMETER_INT:

821 elif

k == Z3_PARAMETER_DOUBLE:

823 elif

k == Z3_PARAMETER_RATIONAL:

825 elif

k == Z3_PARAMETER_SYMBOL:

827 elif

k == Z3_PARAMETER_SORT:

829 elif

k == Z3_PARAMETER_AST:

831 elif

k == Z3_PARAMETER_FUNC_DECL:

838 """Create a Z3 application expression using the function `self`, and the given arguments. 840 The arguments must be Z3 expressions. This method assumes that 841 the sorts of the elements in `args` match the sorts of the 842 domain. Limited coercion is supported. For example, if 843 args[0] is a Python integer, and the function expects a Z3 844 integer, then the argument is automatically converted into a 847 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 855

args = _get_args(args)

857

_args = (Ast * num)()

859 for

in range

(num):

862

tmp = self.

domain

domain(i).cast(args[i])

864

_args[i] = tmp.as_ast()

869 """Return `True` if `a` is a Z3 function declaration. 871 >>> f = Function('f', IntSort(), IntSort()) 878 return

isinstance(a, FuncDeclRef)

882 """Create a new Z3 uninterpreted function with the given sorts. 884 >>> f = Function('f', IntSort(), IntSort()) 890

_z3_assert(len(sig) > 0,

"At least two arguments expected"

)

894

_z3_assert(

(rng),

"Z3 sort expected"

)

895

dom = (Sort * arity)()

896 for

in range

(arity):

898

_z3_assert(

(sig[i]),

"Z3 sort expected"

)

905 """Create a new fresh Z3 uninterpreted function with the given sorts. 909

_z3_assert(len(sig) > 0,

"At least two arguments expected"

)

913

_z3_assert(

(rng),

"Z3 sort expected"

)

914

dom = (z3.Sort * arity)()

915 for

in range

(arity):

917

_z3_assert(

(sig[i]),

"Z3 sort expected"

)

923 def

_to_func_decl_ref(a, ctx):

928 """Create a new Z3 recursive with the given sorts.""" 931

_z3_assert(len(sig) > 0,

"At least two arguments expected"

)

935

_z3_assert(

(rng),

"Z3 sort expected"

)

936

dom = (Sort * arity)()

937 for

in range

(arity):

939

_z3_assert(

(sig[i]),

"Z3 sort expected"

)

946 """Set the body of a recursive function. 947 Recursive definitions can be simplified if they are applied to ground 950 >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx)) 951 >>> n = Int('n', ctx) 952 >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1))) 955 >>> s = Solver(ctx=ctx) 956 >>> s.add(fac(n) < 3) 959 >>> s.model().eval(fac(5)) 965

args = _get_args(args)

969

_args[i] = args[i].ast

980 """Constraints, formulas and terms are expressions in Z3. 982 Expressions are ASTs. Every expression has a sort. 983 There are three main kinds of expressions: 984 function applications, quantifiers and bounded variables. 985 A constant is a function application with 0 arguments. 986 For quantifier free problems, all expressions are 987 function applications. 997 """Return the sort of expression `self`. 1009 """Shorthand for `self.sort().kind()`. 1011 >>> a = Array('a', IntSort(), IntSort()) 1012 >>> a.sort_kind() == Z3_ARRAY_SORT 1014 >>> a.sort_kind() == Z3_INT_SORT 1017 return

self.

sort

sort().kind()

1020 """Return a Z3 expression that represents the constraint `self == other`. 1022 If `other` is `None`, then this method simply returns `False`. 1033

a, b = _coerce_exprs(self, other)

1038 return

AstRef.__hash__(self)

1041 """Return a Z3 expression that represents the constraint `self != other`. 1043 If `other` is `None`, then this method simply returns `True`. 1054

a, b = _coerce_exprs(self, other)

1055

_args, sz = _to_ast_array((a, b))

1062 """Return the Z3 function declaration associated with a Z3 application. 1064 >>> f = Function('f', IntSort(), IntSort()) 1073

_z3_assert(

is_app

(self),

"Z3 application expected"

)

1077 """Return the number of arguments of a Z3 application. 1081 >>> (a + b).num_args() 1083 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 1089

_z3_assert(

is_app

(self),

"Z3 application expected"

)

1093 """Return argument `idx` of the application `self`. 1095 This method assumes that `self` is a function application with at least `idx+1` arguments. 1099 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 1109

_z3_assert(

is_app

(self),

"Z3 application expected"

)

1110

_z3_assert(idx < self.

num_args

num_args(),

"Invalid argument index"

)

1114 """Return a list containing the children of the given expression 1118 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 1138 """inverse function to the serialize method on ExprRef. 1139 It is made available to make it easier for users to serialize expressions back and forth between 1140 strings. Solvers can be serialized using the 'sexpr()' method. 1144 if

len(s.assertions()) != 1:

1145 raise

Z3Exception(

"single assertion expected"

)

1146

fml = s.assertions()[0]

1147 if

fml.num_args() != 1:

1148 raise

Z3Exception(

"dummy function 'F' expected"

)

1151 def

_to_expr_ref(a, ctx):

1152 if

isinstance(a, Pattern):

1156 if

k == Z3_QUANTIFIER_AST:

1159 if

sk == Z3_BOOL_SORT:

1161 if

sk == Z3_INT_SORT:

1162 if

k == Z3_NUMERAL_AST:

1165 if

sk == Z3_REAL_SORT:

1166 if

k == Z3_NUMERAL_AST:

1168 if

_is_algebraic(ctx, a):

1171 if

sk == Z3_BV_SORT:

1172 if

k == Z3_NUMERAL_AST:

1176 if

sk == Z3_ARRAY_SORT:

1178 if

sk == Z3_DATATYPE_SORT:

1180 if

sk == Z3_FLOATING_POINT_SORT:

1181 if

k == Z3_APP_AST

and

_is_numeral(ctx, a):

1184 return FPRef

(a, ctx)

1185 if

sk == Z3_FINITE_DOMAIN_SORT:

1186 if

k == Z3_NUMERAL_AST:

1190 if

sk == Z3_ROUNDING_MODE_SORT:

1192 if

sk == Z3_SEQ_SORT:

1194 if

sk == Z3_CHAR_SORT:

1196 if

sk == Z3_RE_SORT:

1197 return ReRef

(a, ctx)

1201 def

_coerce_expr_merge(s, a):

1214

_z3_assert(s1.ctx == s.ctx,

"context mismatch"

)

1215

_z3_assert(

False

"sort mismatch"

)

1220 def

_coerce_exprs(a, b, ctx=None):

1222

a = _py2expr(a, ctx)

1223

b = _py2expr(b, ctx)

1224 if

isinstance(a, str)

and

isinstance(b, SeqRef):

1226 if

isinstance(b, str)

and

isinstance(a, SeqRef):

1228 if

isinstance(a, float)

and

isinstance(b, ArithRef):

1230 if

isinstance(b, float)

and

isinstance(a, ArithRef):

1234

s = _coerce_expr_merge(s, a)

1235

s = _coerce_expr_merge(s, b)

1241 def

_reduce(func, sequence, initial):

1243 for

element

in

sequence:

1244

result = func(result, element)

1248 def

_coerce_expr_list(alist, ctx=None):

1255

alist = [_py2expr(a, ctx)

for

in

alist]

1256

s = _reduce(_coerce_expr_merge, alist,

None

)

1257 return

[s.cast(a)

for

in

alist]

1261 """Return `True` if `a` is a Z3 expression. 1268 >>> is_expr(IntSort()) 1272 >>> is_expr(IntVal(1)) 1275 >>> is_expr(ForAll(x, x >= 0)) 1277 >>> is_expr(FPVal(1.0)) 1280 return

isinstance(a, ExprRef)

1284 """Return `True` if `a` is a Z3 function application. 1286 Note that, constants are function applications with 0 arguments. 1293 >>> is_app(IntSort()) 1297 >>> is_app(IntVal(1)) 1300 >>> is_app(ForAll(x, x >= 0)) 1303 if not

isinstance(a, ExprRef):

1305

k = _ast_kind(a.ctx, a)

1306 return

k == Z3_NUMERAL_AST

or

k == Z3_APP_AST

1310 """Return `True` if `a` is Z3 constant/variable expression. 1319 >>> is_const(IntVal(1)) 1322 >>> is_const(ForAll(x, x >= 0)) 1325 return is_app

(a)

and

a.num_args() == 0

1329 """Return `True` if `a` is variable. 1331 Z3 uses de-Bruijn indices for representing bound variables in 1339 >>> f = Function('f', IntSort(), IntSort()) 1340 >>> # Z3 replaces x with bound variables when ForAll is executed. 1341 >>> q = ForAll(x, f(x) == x) 1347 >>> is_var(b.arg(1)) 1350 return is_expr

(a)

and

_ast_kind(a.ctx, a) == Z3_VAR_AST

1354 """Return the de-Bruijn index of the Z3 bounded variable `a`. 1362 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 1363 >>> # Z3 replaces x and y with bound variables when ForAll is executed. 1364 >>> q = ForAll([x, y], f(x, y) == x + y) 1366 f(Var(1), Var(0)) == Var(1) + Var(0) 1370 >>> v1 = b.arg(0).arg(0) 1371 >>> v2 = b.arg(0).arg(1) 1376 >>> get_var_index(v1) 1378 >>> get_var_index(v2) 1382

_z3_assert(

is_var

(a),

"Z3 bound variable expected"

)

1387 """Return `True` if `a` is an application of the given kind `k`. 1391 >>> is_app_of(n, Z3_OP_ADD) 1393 >>> is_app_of(n, Z3_OP_MUL) 1396 return is_app

(a)

and

a.decl().kind() == k

1399 def If

(a, b, c, ctx=None):

1400 """Create a Z3 if-then-else expression. 1404 >>> max = If(x > y, x, y) 1410 if

isinstance(a, Probe)

or

isinstance(b, Tactic)

or

isinstance(c, Tactic):

1411 return Cond

(a, b, c, ctx)

1413

ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))

1416

b, c = _coerce_exprs(b, c, ctx)

1418

_z3_assert(a.ctx == b.ctx,

"Context mismatch"

)

1419 return

_to_expr_ref(

Z3_mk_ite

(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)

1423 """Create a Z3 distinct expression. 1430 >>> Distinct(x, y, z) 1432 >>> simplify(Distinct(x, y, z)) 1434 >>> simplify(Distinct(x, y, z), blast_distinct=True) 1435 And(Not(x == y), Not(x == z), Not(y == z)) 1437

args = _get_args(args)

1438

ctx = _ctx_from_ast_arg_list(args)

1440

_z3_assert(ctx

is not None

"At least one of the arguments must be a Z3 expression"

)

1441

args = _coerce_expr_list(args, ctx)

1442

_args, sz = _to_ast_array(args)

1446 def

_mk_bin(f, a, b):

1449

_z3_assert(a.ctx == b.ctx,

"Context mismatch"

)

1450

args[0] = a.as_ast()

1451

args[1] = b.as_ast()

1452 return

f(a.ctx.ref(), 2, args)

1456 """Create a constant of the given sort. 1458 >>> Const('x', IntSort()) 1462

_z3_assert(isinstance(sort, SortRef),

"Z3 sort expected"

)

1468 """Create several constants of the given sort. 1470 `names` is a string containing the names of all constants to be created. 1471 Blank spaces separate the names of different constants. 1473 >>> x, y, z = Consts('x y z', IntSort()) 1477 if

isinstance(names, str):

1478

names = names.split(

" "

)

1479 return

[

Const

(name, sort)

for

name

in

names]

1483 """Create a fresh constant of a specified sort""" 1484

ctx = _get_ctx(sort.ctx)

1489 """Create a Z3 free variable. Free variables are used to create quantified formulas. 1490 A free variable with index n is bound when it occurs within the scope of n+1 quantified 1493 >>> Var(0, IntSort()) 1495 >>> eq(Var(0, IntSort()), Var(0, BoolSort())) 1499

_z3_assert(

(s),

"Z3 sort expected"

)

1500 return

_to_expr_ref(

Z3_mk_bound

(s.ctx_ref(), idx, s.ast), s.ctx)

1505 Create a real free variable. Free variables are used to create quantified formulas. 1506 They are also used to create polynomials. 1516 Create a list of Real free variables. 1517 The variables have ids: 0, 1, ..., n-1 1519 >>> x0, x1, x2, x3 = RealVarVector(4) 1536 """Try to cast `val` as a Boolean. 1538 >>> x = BoolSort().cast(True) 1548 if

isinstance(val, bool):

1552

msg =

"True, False or Z3 Boolean expression expected. Received %s of type %s" 1553

_z3_assert(

(val), msg % (val, type(val)))

1554 if not

self.

eq(val.sort()):

1555

_z3_assert(self.

eq(val.sort()),

"Value cannot be converted into a Z3 Boolean value"

)

1559 return

isinstance(other, ArithSortRef)

1569 """All Boolean expressions are instances of this class.""" 1575 if

isinstance(other, BoolRef):

1576

other =

(other, 1, 0)

1577 return If

(self, 1, 0) + other

1586 """Create the Z3 expression `self * other`. 1588 if

isinstance(other, int)

and

other == 1:

1589 return If

(self, 1, 0)

1590 if

isinstance(other, int)

and

other == 0:

1592 if

isinstance(other, BoolRef):

1593

other =

(other, 1, 0)

1594 return If

(self, other, 0)

1597 return And

(self, other)

1600 return Or

(self, other)

1603 return Xor

(self, other)

1612 """Return `True` if `a` is a Z3 Boolean expression. 1618 >>> is_bool(And(p, q)) 1626 return

isinstance(a, BoolRef)

1630 """Return `True` if `a` is the Z3 true expression. 1635 >>> is_true(simplify(p == p)) 1640 >>> # True is a Python Boolean expression 1648 """Return `True` if `a` is the Z3 false expression. 1655 >>> is_false(BoolVal(False)) 1662 """Return `True` if `a` is a Z3 and expression. 1664 >>> p, q = Bools('p q') 1665 >>> is_and(And(p, q)) 1667 >>> is_and(Or(p, q)) 1674 """Return `True` if `a` is a Z3 or expression. 1676 >>> p, q = Bools('p q') 1679 >>> is_or(And(p, q)) 1686 """Return `True` if `a` is a Z3 implication expression. 1688 >>> p, q = Bools('p q') 1689 >>> is_implies(Implies(p, q)) 1691 >>> is_implies(And(p, q)) 1698 """Return `True` if `a` is a Z3 not expression. 1710 """Return `True` if `a` is a Z3 equality expression. 1712 >>> x, y = Ints('x y') 1720 """Return `True` if `a` is a Z3 distinct expression. 1722 >>> x, y, z = Ints('x y z') 1723 >>> is_distinct(x == y) 1725 >>> is_distinct(Distinct(x, y, z)) 1732 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. 1736 >>> p = Const('p', BoolSort()) 1739 >>> r = Function('r', IntSort(), IntSort(), BoolSort()) 1742 >>> is_bool(r(0, 1)) 1750 """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used. 1754 >>> is_true(BoolVal(True)) 1758 >>> is_false(BoolVal(False)) 1769 """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used. 1781 """Return a tuple of Boolean constants. 1783 `names` is a single string containing all names separated by blank spaces. 1784 If `ctx=None`, then the global context is used. 1786 >>> p, q, r = Bools('p q r') 1787 >>> And(p, Or(q, r)) 1791 if

isinstance(names, str):

1792

names = names.split(

" "

)

1793 return

[

Bool

(name, ctx)

for

name

in

names]

1797 """Return a list of Boolean constants of size `sz`. 1799 The constants are named using the given prefix. 1800 If `ctx=None`, then the global context is used. 1802 >>> P = BoolVector('p', 3) 1806 And(p__0, p__1, p__2) 1808 return

[

Bool

(

"%s__%s"

% (prefix, i))

for

in range

(sz)]

1812 """Return a fresh Boolean constant in the given context using the given prefix. 1814 If `ctx=None`, then the global context is used. 1816 >>> b1 = FreshBool() 1817 >>> b2 = FreshBool() 1826 """Create a Z3 implies expression. 1828 >>> p, q = Bools('p q') 1832

ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))

1840 """Create a Z3 Xor expression. 1842 >>> p, q = Bools('p q') 1845 >>> simplify(Xor(p, q)) 1848

ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))

1856 """Create a Z3 not expression or probe. 1861 >>> simplify(Not(Not(p))) 1864

ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))

1881 def

_has_probe(args):

1882 """Return `True` if one of the elements of the given collection is a Z3 probe.""" 1890 """Create a Z3 and-expression or and-probe. 1892 >>> p, q, r = Bools('p q r') 1895 >>> P = BoolVector('p', 5) 1897 And(p__0, p__1, p__2, p__3, p__4) 1901

last_arg = args[len(args) - 1]

1902 if

isinstance(last_arg, Context):

1903

ctx = args[len(args) - 1]

1904

args = args[:len(args) - 1]

1905 elif

len(args) == 1

and

isinstance(args[0], AstVector):

1907

args = [a

for

in

args[0]]

1910

args = _get_args(args)

1911

ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))

1913

_z3_assert(ctx

is not None

"At least one of the arguments must be a Z3 expression or probe"

)

1914 if

_has_probe(args):

1915 return

_probe_and(args, ctx)

1917

args = _coerce_expr_list(args, ctx)

1918

_args, sz = _to_ast_array(args)

1923 """Create a Z3 or-expression or or-probe. 1925 >>> p, q, r = Bools('p q r') 1928 >>> P = BoolVector('p', 5) 1930 Or(p__0, p__1, p__2, p__3, p__4) 1934

last_arg = args[len(args) - 1]

1935 if

isinstance(last_arg, Context):

1936

ctx = args[len(args) - 1]

1937

args = args[:len(args) - 1]

1938 elif

len(args) == 1

and

isinstance(args[0], AstVector):

1940

args = [a

for

in

args[0]]

1943

args = _get_args(args)

1944

ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))

1946

_z3_assert(ctx

is not None

"At least one of the arguments must be a Z3 expression or probe"

)

1947 if

_has_probe(args):

1948 return

_probe_or(args, ctx)

1950

args = _coerce_expr_list(args, ctx)

1951

_args, sz = _to_ast_array(args)

1962 """Patterns are hints for quantifier instantiation. 1974 """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. 1976 >>> f = Function('f', IntSort(), IntSort()) 1978 >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ]) 1980 ForAll(x, f(x) == 0) 1981 >>> q.num_patterns() 1983 >>> is_pattern(q.pattern(0)) 1988 return

isinstance(a, PatternRef)

1992 """Create a Z3 multi-pattern using the given expressions `*args` 1994 >>> f = Function('f', IntSort(), IntSort()) 1995 >>> g = Function('g', IntSort(), IntSort()) 1997 >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ]) 1999 ForAll(x, f(x) != g(x)) 2000 >>> q.num_patterns() 2002 >>> is_pattern(q.pattern(0)) 2005 MultiPattern(f(Var(0)), g(Var(0))) 2008

_z3_assert(len(args) > 0,

"At least one argument expected"

)

2009

_z3_assert(all([

(a)

for

in

args]),

"Z3 expressions expected"

)

2011

args, sz = _to_ast_array(args)

2015 def

_to_pattern(arg):

2029 """Universally and Existentially quantified formulas.""" 2032 return

self.

2038 """Return the Boolean sort or sort of Lambda.""" 2044 """Return `True` if `self` is a universal quantifier. 2046 >>> f = Function('f', IntSort(), IntSort()) 2048 >>> q = ForAll(x, f(x) == 0) 2051 >>> q = Exists(x, f(x) != 0) 2058 """Return `True` if `self` is an existential quantifier. 2060 >>> f = Function('f', IntSort(), IntSort()) 2062 >>> q = ForAll(x, f(x) == 0) 2065 >>> q = Exists(x, f(x) != 0) 2072 """Return `True` if `self` is a lambda expression. 2074 >>> f = Function('f', IntSort(), IntSort()) 2076 >>> q = Lambda(x, f(x)) 2079 >>> q = Exists(x, f(x) != 0) 2086 """Return the Z3 expression `self[arg]`. 2089

_z3_assert(self.

is_lambda

is_lambda(),

"quantifier should be a lambda expression"

)

2090 return

_array_select(self, arg)

2093 """Return the weight annotation of `self`. 2095 >>> f = Function('f', IntSort(), IntSort()) 2097 >>> q = ForAll(x, f(x) == 0) 2100 >>> q = ForAll(x, f(x) == 0, weight=10) 2107 """Return the skolem id of `self`. 2112 """Return the quantifier id of `self`. 2117 """Return the number of patterns (i.e., quantifier instantiation hints) in `self`. 2119 >>> f = Function('f', IntSort(), IntSort()) 2120 >>> g = Function('g', IntSort(), IntSort()) 2122 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ]) 2123 >>> q.num_patterns() 2129 """Return a pattern (i.e., quantifier instantiation hints) in `self`. 2131 >>> f = Function('f', IntSort(), IntSort()) 2132 >>> g = Function('g', IntSort(), IntSort()) 2134 >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ]) 2135 >>> q.num_patterns() 2143

_z3_assert(idx < self.

num_patterns

num_patterns(),

"Invalid pattern idx"

)

2147 """Return the number of no-patterns.""" 2151 """Return a no-pattern.""" 2153

_z3_assert(idx < self.

num_no_patterns

num_no_patterns(),

"Invalid no-pattern idx"

)

2157 """Return the expression being quantified. 2159 >>> f = Function('f', IntSort(), IntSort()) 2161 >>> q = ForAll(x, f(x) == 0) 2168 """Return the number of variables bounded by this quantifier. 2170 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 2173 >>> q = ForAll([x, y], f(x, y) >= x) 2180 """Return a string representing a name used when displaying the quantifier. 2182 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 2185 >>> q = ForAll([x, y], f(x, y) >= x) 2192

_z3_assert(idx < self.

num_vars

num_vars(),

"Invalid variable idx"

)

2196 """Return the sort of a bound variable. 2198 >>> f = Function('f', IntSort(), RealSort(), IntSort()) 2201 >>> q = ForAll([x, y], f(x, y) >= x) 2208

_z3_assert(idx < self.

num_vars

num_vars(),

"Invalid variable idx"

)

2212 """Return a list containing a single element self.body() 2214 >>> f = Function('f', IntSort(), IntSort()) 2216 >>> q = ForAll(x, f(x) == 0) 2220 return

[self.

body

body()]

2224 """Return `True` if `a` is a Z3 quantifier. 2226 >>> f = Function('f', IntSort(), IntSort()) 2228 >>> q = ForAll(x, f(x) == 0) 2229 >>> is_quantifier(q) 2231 >>> is_quantifier(f(x)) 2234 return

isinstance(a, QuantifierRef)

2237 def

_mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):

2239

_z3_assert(

is_bool

(body)

or is_app

(vs)

or

(len(vs) > 0

and is_app

(vs[0])),

"Z3 expression expected"

)

2240

_z3_assert(

is_const

(vs)

or

(len(vs) > 0

and

all([

is_const

(v)

for

in

vs])),

"Invalid bounded variable(s)"

)

2241

_z3_assert(all([

is_pattern

(a)

or is_expr

(a)

for

in

patterns]),

"Z3 patterns expected"

)

2242

_z3_assert(all([

(p)

for

in

no_patterns]),

"no patterns are Z3 expressions"

)

2253

_vs = (Ast * num_vars)()

2254 for

in range

(num_vars):

2256

_vs[i] = vs[i].as_ast()

2257

patterns = [_to_pattern(p)

for

in

patterns]

2258

num_pats = len(patterns)

2259

_pats = (Pattern * num_pats)()

2260 for

in range

(num_pats):

2261

_pats[i] = patterns[i].ast

2262

_no_pats, num_no_pats = _to_ast_array(no_patterns)

2268

num_no_pats, _no_pats,

2269

body.as_ast()), ctx)

2272 def ForAll

(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):

2273 """Create a Z3 forall formula. 2275 The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations. 2277 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 2280 >>> ForAll([x, y], f(x, y) >= x) 2281 ForAll([x, y], f(x, y) >= x) 2282 >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ]) 2283 ForAll([x, y], f(x, y) >= x) 2284 >>> ForAll([x, y], f(x, y) >= x, weight=10) 2285 ForAll([x, y], f(x, y) >= x) 2287 return

_mk_quantifier(

True

, vs, body, weight, qid, skid, patterns, no_patterns)

2290 def Exists

(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):

2291 """Create a Z3 exists formula. 2293 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. 2296 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 2299 >>> q = Exists([x, y], f(x, y) >= x, skid="foo") 2301 Exists([x, y], f(x, y) >= x) 2302 >>> is_quantifier(q) 2304 >>> r = Tactic('nnf')(q).as_expr() 2305 >>> is_quantifier(r) 2308 return

_mk_quantifier(

False

, vs, body, weight, qid, skid, patterns, no_patterns)

2312 """Create a Z3 lambda expression. 2314 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 2315 >>> mem0 = Array('mem0', IntSort(), IntSort()) 2316 >>> lo, hi, e, i = Ints('lo hi e i') 2317 >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i])) 2319 Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i])) 2325

_vs = (Ast * num_vars)()

2326 for

in range

(num_vars):

2328

_vs[i] = vs[i].as_ast()

2339 """Real and Integer sorts.""" 2342 """Return `True` if `self` is of the sort Real. 2347 >>> (x + 1).is_real() 2353 return

self.

kind

kind() == Z3_REAL_SORT

2356 """Return `True` if `self` is of the sort Integer. 2361 >>> (x + 1).is_int() 2367 return

self.

kind

kind() == Z3_INT_SORT

2373 """Return `True` if `self` is a subsort of `other`.""" 2377 """Try to cast `val` as an Integer or Real. 2379 >>> IntSort().cast(10) 2381 >>> is_int(IntSort().cast(10)) 2385 >>> RealSort().cast(10) 2387 >>> is_real(RealSort().cast(10)) 2392

_z3_assert(self.

ctx ctx

ctx == val.ctx,

"Context mismatch"

)

2394 if

self.

eq(val_s):

2396 if

val_s.is_int()

and

self.

is_real

is_real():

2398 if

val_s.is_bool()

and

self.

is_int

is_int():

2399 return If

(val, 1, 0)

2400 if

val_s.is_bool()

and

self.

is_real

is_real():

2403

_z3_assert(

False

"Z3 Integer/Real expression expected"

)

2405 if

self.

is_int

is_int():

2410

msg =

"int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" 2411

_z3_assert(

False

, msg % self)

2415 """Return `True` if s is an arithmetical sort (type). 2417 >>> is_arith_sort(IntSort()) 2419 >>> is_arith_sort(RealSort()) 2421 >>> is_arith_sort(BoolSort()) 2423 >>> n = Int('x') + 1 2424 >>> is_arith_sort(n.sort()) 2427 return

isinstance(s, ArithSortRef)

2431 """Integer and Real expressions.""" 2434 """Return the sort (type) of the arithmetical expression `self`. 2438 >>> (Real('x') + 1).sort() 2444 """Return `True` if `self` is an integer expression. 2449 >>> (x + 1).is_int() 2452 >>> (x + y).is_int() 2458 """Return `True` if `self` is an real expression. 2463 >>> (x + 1).is_real() 2469 """Create the Z3 expression `self + other`. 2478

a, b = _coerce_exprs(self, other)

2479 return ArithRef

(_mk_bin(Z3_mk_add, a, b), self.

ctx)

2482 """Create the Z3 expression `other + self`. 2488

a, b = _coerce_exprs(self, other)

2489 return ArithRef

(_mk_bin(Z3_mk_add, b, a), self.

ctx)

2492 """Create the Z3 expression `self * other`. 2501 if

isinstance(other, BoolRef):

2502 return If

(other, self, 0)

2503

a, b = _coerce_exprs(self, other)

2504 return ArithRef

(_mk_bin(Z3_mk_mul, a, b), self.

ctx)

2507 """Create the Z3 expression `other * self`. 2513

a, b = _coerce_exprs(self, other)

2514 return ArithRef

(_mk_bin(Z3_mk_mul, b, a), self.

ctx)

2517 """Create the Z3 expression `self - other`. 2526

a, b = _coerce_exprs(self, other)

2527 return ArithRef

(_mk_bin(Z3_mk_sub, a, b), self.

ctx)

2530 """Create the Z3 expression `other - self`. 2536

a, b = _coerce_exprs(self, other)

2537 return ArithRef

(_mk_bin(Z3_mk_sub, b, a), self.

ctx)

2540 """Create the Z3 expression `self**other` (** is the power operator). 2547 >>> simplify(IntVal(2)**8) 2550

a, b = _coerce_exprs(self, other)

2554 """Create the Z3 expression `other**self` (** is the power operator). 2561 >>> simplify(2**IntVal(8)) 2564

a, b = _coerce_exprs(self, other)

2568 """Create the Z3 expression `other/self`. 2587

a, b = _coerce_exprs(self, other)

2591 """Create the Z3 expression `other/self`.""" 2592 return

self.

__div__

__div__(other)

2595 """Create the Z3 expression `other/self`. 2608

a, b = _coerce_exprs(self, other)

2612 """Create the Z3 expression `other/self`.""" 2613 return

self.

__rdiv__

__rdiv__(other)

2616 """Create the Z3 expression `other%self`. 2622 >>> simplify(IntVal(10) % IntVal(3)) 2625

a, b = _coerce_exprs(self, other)

2627

_z3_assert(a.is_int(),

"Z3 integer expression expected"

)

2631 """Create the Z3 expression `other%self`. 2637

a, b = _coerce_exprs(self, other)

2639

_z3_assert(a.is_int(),

"Z3 integer expression expected"

)

2643 """Return an expression representing `-self`. 2663 """Create the Z3 expression `other <= self`. 2665 >>> x, y = Ints('x y') 2672

a, b = _coerce_exprs(self, other)

2676 """Create the Z3 expression `other < self`. 2678 >>> x, y = Ints('x y') 2685

a, b = _coerce_exprs(self, other)

2689 """Create the Z3 expression `other > self`. 2691 >>> x, y = Ints('x y') 2698

a, b = _coerce_exprs(self, other)

2702 """Create the Z3 expression `other >= self`. 2704 >>> x, y = Ints('x y') 2711

a, b = _coerce_exprs(self, other)

2716 """Return `True` if `a` is an arithmetical expression. 2725 >>> is_arith(IntVal(1)) 2733 return

isinstance(a, ArithRef)

2737 """Return `True` if `a` is an integer expression. 2744 >>> is_int(IntVal(1)) 2756 """Return `True` if `a` is a real expression. 2768 >>> is_real(RealVal(1)) 2771 return is_arith

(a)

and

a.is_real()

2774 def

_is_numeral(ctx, a):

2778 def

_is_algebraic(ctx, a):

2783 """Return `True` if `a` is an integer value of sort Int. 2785 >>> is_int_value(IntVal(1)) 2789 >>> is_int_value(Int('x')) 2791 >>> n = Int('x') + 1 2796 >>> is_int_value(n.arg(1)) 2798 >>> is_int_value(RealVal("1/3")) 2800 >>> is_int_value(RealVal(1)) 2803 return is_arith

(a)

and

a.is_int()

and

_is_numeral(a.ctx, a.as_ast())

2807 """Return `True` if `a` is rational value of sort Real. 2809 >>> is_rational_value(RealVal(1)) 2811 >>> is_rational_value(RealVal("3/5")) 2813 >>> is_rational_value(IntVal(1)) 2815 >>> is_rational_value(1) 2817 >>> n = Real('x') + 1 2820 >>> is_rational_value(n.arg(1)) 2822 >>> is_rational_value(Real('x')) 2825 return is_arith

(a)

and

a.is_real()

and

_is_numeral(a.ctx, a.as_ast())

2829 """Return `True` if `a` is an algebraic value of sort Real. 2831 >>> is_algebraic_value(RealVal("3/5")) 2833 >>> n = simplify(Sqrt(2)) 2836 >>> is_algebraic_value(n) 2839 return is_arith

(a)

and

a.is_real()

and

_is_algebraic(a.ctx, a.as_ast())

2843 """Return `True` if `a` is an expression of the form b + c. 2845 >>> x, y = Ints('x y') 2855 """Return `True` if `a` is an expression of the form b * c. 2857 >>> x, y = Ints('x y') 2867 """Return `True` if `a` is an expression of the form b - c. 2869 >>> x, y = Ints('x y') 2879 """Return `True` if `a` is an expression of the form b / c. 2881 >>> x, y = Reals('x y') 2886 >>> x, y = Ints('x y') 2896 """Return `True` if `a` is an expression of the form b div c. 2898 >>> x, y = Ints('x y') 2908 """Return `True` if `a` is an expression of the form b % c. 2910 >>> x, y = Ints('x y') 2920 """Return `True` if `a` is an expression of the form b <= c. 2922 >>> x, y = Ints('x y') 2932 """Return `True` if `a` is an expression of the form b < c. 2934 >>> x, y = Ints('x y') 2944 """Return `True` if `a` is an expression of the form b >= c. 2946 >>> x, y = Ints('x y') 2956 """Return `True` if `a` is an expression of the form b > c. 2958 >>> x, y = Ints('x y') 2968 """Return `True` if `a` is an expression of the form IsInt(b). 2971 >>> is_is_int(IsInt(x)) 2980 """Return `True` if `a` is an expression of the form ToReal(b). 2995 """Return `True` if `a` is an expression of the form ToInt(b). 3010 """Integer values.""" 3013 """Return a Z3 integer numeral as a Python long (bignum) numeral. 3022

_z3_assert(self.

is_int

is_int(),

"Integer value expected"

)

3026 """Return a Z3 integer numeral as a Python string. 3034 """Return a Z3 integer numeral as a Python binary string. 3036 >>> v.as_binary_string() 3043 """Rational values.""" 3046 """ Return the numerator of a Z3 rational numeral. 3048 >>> is_rational_value(RealVal("3/5")) 3050 >>> n = RealVal("3/5") 3053 >>> is_rational_value(Q(3,5)) 3055 >>> Q(3,5).numerator() 3061 """ Return the denominator of a Z3 rational numeral. 3063 >>> is_rational_value(Q(3,5)) 3072 """ Return the numerator as a Python long. 3074 >>> v = RealVal(10000000000) 3079 >>> v.numerator_as_long() + 1 == 10000000001 3085 """ Return the denominator as a Python long. 3087 >>> v = RealVal("1/3") 3090 >>> v.denominator_as_long() 3105

_z3_assert(self.

is_int_value

is_int_value(),

"Expected integer fraction"

)

3109 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places. 3111 >>> v = RealVal("1/5") 3114 >>> v = RealVal("1/3") 3121 """Return a Z3 rational numeral as a Python string. 3130 """Return a Z3 rational as a Python Fraction object. 3132 >>> v = RealVal("1/5") 3140 """Algebraic irrational values.""" 3143 """Return a Z3 rational number that approximates the algebraic number `self`. 3144 The result `r` is such that |r - self| <= 1/10^precision 3146 >>> x = simplify(Sqrt(2)) 3148 6838717160008073720548335/4835703278458516698824704 3155 """Return a string representation of the algebraic number `self` in decimal notation 3156 using `prec` decimal places. 3158 >>> x = simplify(Sqrt(2)) 3159 >>> x.as_decimal(10) 3161 >>> x.as_decimal(20) 3162 '1.41421356237309504880?' 3173 def

_py2expr(a, ctx=None):

3174 if

isinstance(a, bool):

3178 if

isinstance(a, float):

3180 if

isinstance(a, str):

3185

_z3_assert(

False

"Python bool, int, long or float expected"

)

3189 """Return the integer sort in the given context. If `ctx=None`, then the global context is used. 3193 >>> x = Const('x', IntSort()) 3196 >>> x.sort() == IntSort() 3198 >>> x.sort() == BoolSort() 3206 """Return the real sort in the given context. If `ctx=None`, then the global context is used. 3210 >>> x = Const('x', RealSort()) 3215 >>> x.sort() == RealSort() 3222 def

_to_int_str(val):

3223 if

isinstance(val, float):

3224 return

str(int(val))

3225 elif

isinstance(val, bool):

3235 """Return a Z3 integer value. If `ctx=None`, then the global context is used. 3247 """Return a Z3 real value. 3249 `val` may be a Python int, long, float or string representing a number in decimal or rational notation. 3250 If `ctx=None`, then the global context is used. 3254 >>> RealVal(1).sort() 3266 """Return a Z3 rational a/b. 3268 If `ctx=None`, then the global context is used. 3272 >>> RatVal(3,5).sort() 3276

_z3_assert(_is_int(a)

or

isinstance(a, str),

"First argument cannot be converted into an integer"

)

3277

_z3_assert(_is_int(b)

or

isinstance(b, str),

"Second argument cannot be converted into an integer"

)

3281 def Q

(a, b, ctx=None):

3282 """Return a Z3 rational a/b. 3284 If `ctx=None`, then the global context is used. 3295 """Return an integer constant named `name`. If `ctx=None`, then the global context is used. 3308 """Return a tuple of Integer constants. 3310 >>> x, y, z = Ints('x y z') 3315 if

isinstance(names, str):

3316

names = names.split(

" "

)

3317 return

[

Int

(name, ctx)

for

name

in

names]

3321 """Return a list of integer constants of size `sz`. 3323 >>> X = IntVector('x', 3) 3330 return

[

Int

(

"%s__%s"

% (prefix, i), ctx)

for

in range

(sz)]

3334 """Return a fresh integer constant in the given context using the given prefix. 3348 """Return a real constant named `name`. If `ctx=None`, then the global context is used. 3361 """Return a tuple of real constants. 3363 >>> x, y, z = Reals('x y z') 3366 >>> Sum(x, y, z).sort() 3370 if

isinstance(names, str):

3371

names = names.split(

" "

)

3372 return

[

Real

(name, ctx)

for

name

in

names]

3376 """Return a list of real constants of size `sz`. 3378 >>> X = RealVector('x', 3) 3387 return

[

Real

(

"%s__%s"

% (prefix, i), ctx)

for

in range

(sz)]

3391 """Return a fresh real constant in the given context using the given prefix. 3405 """ Return the Z3 expression ToReal(a). 3417

_z3_assert(a.is_int(),

"Z3 integer expression expected."

)

3423 """ Return the Z3 expression ToInt(a). 3435

_z3_assert(a.is_real(),

"Z3 real expression expected."

)

3441 """ Return the Z3 predicate IsInt(a). 3444 >>> IsInt(x + "1/2") 3446 >>> solve(IsInt(x + "1/2"), x > 0, x < 1) 3448 >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2") 3452

_z3_assert(a.is_real(),

"Z3 real expression expected."

)

3458 """ Return a Z3 expression which represents the square root of a. 3471 """ Return a Z3 expression which represents the cubic root of a. 3490 """Bit-vector sort.""" 3493 """Return the size (number of bits) of the bit-vector sort `self`. 3495 >>> b = BitVecSort(32) 3505 """Try to cast `val` as a Bit-Vector. 3507 >>> b = BitVecSort(32) 3510 >>> b.cast(10).sexpr() 3515

_z3_assert(self.

ctx ctx

ctx == val.ctx,

"Context mismatch"

)

3523 """Return True if `s` is a Z3 bit-vector sort. 3525 >>> is_bv_sort(BitVecSort(32)) 3527 >>> is_bv_sort(IntSort()) 3530 return

isinstance(s, BitVecSortRef)

3534 """Bit-vector expressions.""" 3537 """Return the sort of the bit-vector expression `self`. 3539 >>> x = BitVec('x', 32) 3542 >>> x.sort() == BitVecSort(32) 3548 """Return the number of bits of the bit-vector expression `self`. 3550 >>> x = BitVec('x', 32) 3553 >>> Concat(x, x).size() 3559 """Create the Z3 expression `self + other`. 3561 >>> x = BitVec('x', 32) 3562 >>> y = BitVec('y', 32) 3568

a, b = _coerce_exprs(self, other)

3572 """Create the Z3 expression `other + self`. 3574 >>> x = BitVec('x', 32) 3578

a, b = _coerce_exprs(self, other)

3582 """Create the Z3 expression `self * other`. 3584 >>> x = BitVec('x', 32) 3585 >>> y = BitVec('y', 32) 3591

a, b = _coerce_exprs(self, other)

3595 """Create the Z3 expression `other * self`. 3597 >>> x = BitVec('x', 32) 3601

a, b = _coerce_exprs(self, other)

3605 """Create the Z3 expression `self - other`. 3607 >>> x = BitVec('x', 32) 3608 >>> y = BitVec('y', 32) 3614

a, b = _coerce_exprs(self, other)

3618 """Create the Z3 expression `other - self`. 3620 >>> x = BitVec('x', 32) 3624

a, b = _coerce_exprs(self, other)

3628 """Create the Z3 expression bitwise-or `self | other`. 3630 >>> x = BitVec('x', 32) 3631 >>> y = BitVec('y', 32) 3637

a, b = _coerce_exprs(self, other)

3641 """Create the Z3 expression bitwise-or `other | self`. 3643 >>> x = BitVec('x', 32) 3647

a, b = _coerce_exprs(self, other)

3651 """Create the Z3 expression bitwise-and `self & other`. 3653 >>> x = BitVec('x', 32) 3654 >>> y = BitVec('y', 32) 3660

a, b = _coerce_exprs(self, other)

3664 """Create the Z3 expression bitwise-or `other & self`. 3666 >>> x = BitVec('x', 32) 3670

a, b = _coerce_exprs(self, other)

3674 """Create the Z3 expression bitwise-xor `self ^ other`. 3676 >>> x = BitVec('x', 32) 3677 >>> y = BitVec('y', 32) 3683

a, b = _coerce_exprs(self, other)

3687 """Create the Z3 expression bitwise-xor `other ^ self`. 3689 >>> x = BitVec('x', 32) 3693

a, b = _coerce_exprs(self, other)

3699 >>> x = BitVec('x', 32) 3706 """Return an expression representing `-self`. 3708 >>> x = BitVec('x', 32) 3717 """Create the Z3 expression bitwise-not `~self`. 3719 >>> x = BitVec('x', 32) 3728 """Create the Z3 expression (signed) division `self / other`. 3730 Use the function UDiv() for unsigned division. 3732 >>> x = BitVec('x', 32) 3733 >>> y = BitVec('y', 32) 3740 >>> UDiv(x, y).sexpr() 3743

a, b = _coerce_exprs(self, other)

3747 """Create the Z3 expression (signed) division `self / other`.""" 3748 return

self.

__div__

__div__(other)

3751 """Create the Z3 expression (signed) division `other / self`. 3753 Use the function UDiv() for unsigned division. 3755 >>> x = BitVec('x', 32) 3758 >>> (10 / x).sexpr() 3759 '(bvsdiv #x0000000a x)' 3760 >>> UDiv(10, x).sexpr() 3761 '(bvudiv #x0000000a x)' 3763

a, b = _coerce_exprs(self, other)

3767 """Create the Z3 expression (signed) division `other / self`.""" 3768 return

self.

__rdiv__

__rdiv__(other)

3771 """Create the Z3 expression (signed) mod `self % other`. 3773 Use the function URem() for unsigned remainder, and SRem() for signed remainder. 3775 >>> x = BitVec('x', 32) 3776 >>> y = BitVec('y', 32) 3783 >>> URem(x, y).sexpr() 3785 >>> SRem(x, y).sexpr() 3788

a, b = _coerce_exprs(self, other)

3792 """Create the Z3 expression (signed) mod `other % self`. 3794 Use the function URem() for unsigned remainder, and SRem() for signed remainder. 3796 >>> x = BitVec('x', 32) 3799 >>> (10 % x).sexpr() 3800 '(bvsmod #x0000000a x)' 3801 >>> URem(10, x).sexpr() 3802 '(bvurem #x0000000a x)' 3803 >>> SRem(10, x).sexpr() 3804 '(bvsrem #x0000000a x)' 3806

a, b = _coerce_exprs(self, other)

3810 """Create the Z3 expression (signed) `other <= self`. 3812 Use the function ULE() for unsigned less than or equal to. 3814 >>> x, y = BitVecs('x y', 32) 3817 >>> (x <= y).sexpr() 3819 >>> ULE(x, y).sexpr() 3822

a, b = _coerce_exprs(self, other)

3826 """Create the Z3 expression (signed) `other < self`. 3828 Use the function ULT() for unsigned less than. 3830 >>> x, y = BitVecs('x y', 32) 3835 >>> ULT(x, y).sexpr() 3838

a, b = _coerce_exprs(self, other)

3842 """Create the Z3 expression (signed) `other > self`. 3844 Use the function UGT() for unsigned greater than. 3846 >>> x, y = BitVecs('x y', 32) 3851 >>> UGT(x, y).sexpr() 3854

a, b = _coerce_exprs(self, other)

3858 """Create the Z3 expression (signed) `other >= self`. 3860 Use the function UGE() for unsigned greater than or equal to. 3862 >>> x, y = BitVecs('x y', 32) 3865 >>> (x >= y).sexpr() 3867 >>> UGE(x, y).sexpr() 3870

a, b = _coerce_exprs(self, other)

3874 """Create the Z3 expression (arithmetical) right shift `self >> other` 3876 Use the function LShR() for the right logical shift 3878 >>> x, y = BitVecs('x y', 32) 3881 >>> (x >> y).sexpr() 3883 >>> LShR(x, y).sexpr() 3887 >>> BitVecVal(4, 3).as_signed_long() 3889 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() 3891 >>> simplify(BitVecVal(4, 3) >> 1) 3893 >>> simplify(LShR(BitVecVal(4, 3), 1)) 3895 >>> simplify(BitVecVal(2, 3) >> 1) 3897 >>> simplify(LShR(BitVecVal(2, 3), 1)) 3900

a, b = _coerce_exprs(self, other)

3904 """Create the Z3 expression left shift `self << other` 3906 >>> x, y = BitVecs('x y', 32) 3909 >>> (x << y).sexpr() 3911 >>> simplify(BitVecVal(2, 3) << 1) 3914

a, b = _coerce_exprs(self, other)

3918 """Create the Z3 expression (arithmetical) right shift `other` >> `self`. 3920 Use the function LShR() for the right logical shift 3922 >>> x = BitVec('x', 32) 3925 >>> (10 >> x).sexpr() 3926 '(bvashr #x0000000a x)' 3928

a, b = _coerce_exprs(self, other)

3932 """Create the Z3 expression left shift `other << self`. 3934 Use the function LShR() for the right logical shift 3936 >>> x = BitVec('x', 32) 3939 >>> (10 << x).sexpr() 3940 '(bvshl #x0000000a x)' 3942

a, b = _coerce_exprs(self, other)

3947 """Bit-vector values.""" 3950 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. 3952 >>> v = BitVecVal(0xbadc0de, 32) 3955 >>> print("0x%.8x" % v.as_long()) 3961 """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. 3962 The most significant bit is assumed to be the sign. 3964 >>> BitVecVal(4, 3).as_signed_long() 3966 >>> BitVecVal(7, 3).as_signed_long() 3968 >>> BitVecVal(3, 3).as_signed_long() 3970 >>> BitVecVal(2**32 - 1, 32).as_signed_long() 3972 >>> BitVecVal(2**64 - 1, 64).as_signed_long() 3975

sz = self.

size

size()

3977 if

val >= 2**(sz - 1):

3979 if

val < -2**(sz - 1):

3991 """Return `True` if `a` is a Z3 bit-vector expression. 3993 >>> b = BitVec('b', 32) 4001 return

isinstance(a, BitVecRef)

4005 """Return `True` if `a` is a Z3 bit-vector numeral value. 4007 >>> b = BitVec('b', 32) 4010 >>> b = BitVecVal(10, 32) 4016 return is_bv

(a)

and

_is_numeral(a.ctx, a.as_ast())

4020 """Return the Z3 expression BV2Int(a). 4022 >>> b = BitVec('b', 3) 4023 >>> BV2Int(b).sort() 4028 >>> x > BV2Int(b, is_signed=False) 4030 >>> x > BV2Int(b, is_signed=True) 4031 x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) 4032 >>> solve(x > BV2Int(b), b == 1, x < 3) 4036

_z3_assert(

(a),

"First argument must be a Z3 bit-vector expression"

)

4043 """Return the z3 expression Int2BV(a, num_bits). 4044 It is a bit-vector of width num_bits and represents the 4045 modulo of a by 2^num_bits 4052 """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. 4054 >>> Byte = BitVecSort(8) 4055 >>> Word = BitVecSort(16) 4058 >>> x = Const('x', Byte) 4059 >>> eq(x, BitVec('x', 8)) 4067 """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used. 4069 >>> v = BitVecVal(10, 32) 4072 >>> print("0x%.8x" % v.as_long()) 4084 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort. 4085 If `ctx=None`, then the global context is used. 4087 >>> x = BitVec('x', 16) 4094 >>> word = BitVecSort(16) 4095 >>> x2 = BitVec('x', word) 4099 if

isinstance(bv, BitVecSortRef):

4108 """Return a tuple of bit-vector constants of size bv. 4110 >>> x, y, z = BitVecs('x y z', 16) 4117 >>> Product(x, y, z) 4119 >>> simplify(Product(x, y, z)) 4123 if

isinstance(names, str):

4124

names = names.split(

" "

)

4125 return

[

BitVec

(name, bv, ctx)

for

name

in

names]

4129 """Create a Z3 bit-vector concatenation expression. 4131 >>> v = BitVecVal(1, 4) 4132 >>> Concat(v, v+1, v) 4133 Concat(Concat(1, 1 + 1), 1) 4134 >>> simplify(Concat(v, v+1, v)) 4136 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long()) 4139

args = _get_args(args)

4142

_z3_assert(sz >= 2,

"At least two arguments expected."

)

4149 if is_seq

(args[0])

or

isinstance(args[0], str):

4150

args = [_coerce_seq(s, ctx)

for

in

args]

4152

_z3_assert(all([

is_seq

(a)

for

in

args]),

"All arguments must be sequence expressions."

)

4154 for

in range

(sz):

4155

v[i] = args[i].as_ast()

4160

_z3_assert(all([

is_re

(a)

for

in

args]),

"All arguments must be regular expressions."

)

4162 for

in range

(sz):

4163

v[i] = args[i].as_ast()

4167

_z3_assert(all([

(a)

for

in

args]),

"All arguments must be Z3 bit-vector expressions."

)

4169 for

in range

(sz - 1):

4175 """Create a Z3 bit-vector extraction expression. 4176 Extract is overloaded to also work on sequence extraction. 4177 The functions SubString and SubSeq are redirected to Extract. 4178 For this case, the arguments are reinterpreted as: 4179 high - is a sequence (string) 4181 a - is the length to be extracted 4183 >>> x = BitVec('x', 8) 4184 >>> Extract(6, 2, x) 4186 >>> Extract(6, 2, x).sort() 4188 >>> simplify(Extract(StringVal("abcd"),2,1)) 4191 if

isinstance(high, str):

4195

offset, length = _coerce_exprs(low, a, s.ctx)

4198

_z3_assert(low <= high,

"First argument must be greater than or equal to second argument"

)

4199

_z3_assert(_is_int(high)

and

high >= 0

and

_is_int(low)

and

low >= 0,

4200 "First and second arguments must be non negative integers"

)

4201

_z3_assert(

(a),

"Third argument must be a Z3 bit-vector expression"

)

4205 def

_check_bv_args(a, b):

4207

_z3_assert(

(a)

or is_bv

(b),

"First or second argument must be a Z3 bit-vector expression"

)

4211 """Create the Z3 expression (unsigned) `other <= self`. 4213 Use the operator <= for signed less than or equal to. 4215 >>> x, y = BitVecs('x y', 32) 4218 >>> (x <= y).sexpr() 4220 >>> ULE(x, y).sexpr() 4223

_check_bv_args(a, b)

4224

a, b = _coerce_exprs(a, b)

4229 """Create the Z3 expression (unsigned) `other < self`. 4231 Use the operator < for signed less than. 4233 >>> x, y = BitVecs('x y', 32) 4238 >>> ULT(x, y).sexpr() 4241

_check_bv_args(a, b)

4242

a, b = _coerce_exprs(a, b)

4247 """Create the Z3 expression (unsigned) `other >= self`. 4249 Use the operator >= for signed greater than or equal to. 4251 >>> x, y = BitVecs('x y', 32) 4254 >>> (x >= y).sexpr() 4256 >>> UGE(x, y).sexpr() 4259

_check_bv_args(a, b)

4260

a, b = _coerce_exprs(a, b)

4265 """Create the Z3 expression (unsigned) `other > self`. 4267 Use the operator > for signed greater than. 4269 >>> x, y = BitVecs('x y', 32) 4274 >>> UGT(x, y).sexpr() 4277

_check_bv_args(a, b)

4278

a, b = _coerce_exprs(a, b)

4283 """Create the Z3 expression (unsigned) division `self / other`. 4285 Use the operator / for signed division. 4287 >>> x = BitVec('x', 32) 4288 >>> y = BitVec('y', 32) 4291 >>> UDiv(x, y).sort() 4295 >>> UDiv(x, y).sexpr() 4298

_check_bv_args(a, b)

4299

a, b = _coerce_exprs(a, b)

4304 """Create the Z3 expression (unsigned) remainder `self % other`. 4306 Use the operator % for signed modulus, and SRem() for signed remainder. 4308 >>> x = BitVec('x', 32) 4309 >>> y = BitVec('y', 32) 4312 >>> URem(x, y).sort() 4316 >>> URem(x, y).sexpr() 4319

_check_bv_args(a, b)

4320

a, b = _coerce_exprs(a, b)

4325 """Create the Z3 expression signed remainder. 4327 Use the operator % for signed modulus, and URem() for unsigned remainder. 4329 >>> x = BitVec('x', 32) 4330 >>> y = BitVec('y', 32) 4333 >>> SRem(x, y).sort() 4337 >>> SRem(x, y).sexpr() 4340

_check_bv_args(a, b)

4341

a, b = _coerce_exprs(a, b)

4346 """Create the Z3 expression logical right shift. 4348 Use the operator >> for the arithmetical right shift. 4350 >>> x, y = BitVecs('x y', 32) 4353 >>> (x >> y).sexpr() 4355 >>> LShR(x, y).sexpr() 4359 >>> BitVecVal(4, 3).as_signed_long() 4361 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() 4363 >>> simplify(BitVecVal(4, 3) >> 1) 4365 >>> simplify(LShR(BitVecVal(4, 3), 1)) 4367 >>> simplify(BitVecVal(2, 3) >> 1) 4369 >>> simplify(LShR(BitVecVal(2, 3), 1)) 4372

_check_bv_args(a, b)

4373

a, b = _coerce_exprs(a, b)

4378 """Return an expression representing `a` rotated to the left `b` times. 4380 >>> a, b = BitVecs('a b', 16) 4381 >>> RotateLeft(a, b) 4383 >>> simplify(RotateLeft(a, 0)) 4385 >>> simplify(RotateLeft(a, 16)) 4388

_check_bv_args(a, b)

4389

a, b = _coerce_exprs(a, b)

4394 """Return an expression representing `a` rotated to the right `b` times. 4396 >>> a, b = BitVecs('a b', 16) 4397 >>> RotateRight(a, b) 4399 >>> simplify(RotateRight(a, 0)) 4401 >>> simplify(RotateRight(a, 16)) 4404

_check_bv_args(a, b)

4405

a, b = _coerce_exprs(a, b)

4410 """Return a bit-vector expression with `n` extra sign-bits. 4412 >>> x = BitVec('x', 16) 4413 >>> n = SignExt(8, x) 4420 >>> v0 = BitVecVal(2, 2) 4425 >>> v = simplify(SignExt(6, v0)) 4430 >>> print("%.x" % v.as_long()) 4434

_z3_assert(_is_int(n),

"First argument must be an integer"

)

4435

_z3_assert(

(a),

"Second argument must be a Z3 bit-vector expression"

)

4440 """Return a bit-vector expression with `n` extra zero-bits. 4442 >>> x = BitVec('x', 16) 4443 >>> n = ZeroExt(8, x) 4450 >>> v0 = BitVecVal(2, 2) 4455 >>> v = simplify(ZeroExt(6, v0)) 4462

_z3_assert(_is_int(n),

"First argument must be an integer"

)

4463

_z3_assert(

(a),

"Second argument must be a Z3 bit-vector expression"

)

4468 """Return an expression representing `n` copies of `a`. 4470 >>> x = BitVec('x', 8) 4471 >>> n = RepeatBitVec(4, x) 4476 >>> v0 = BitVecVal(10, 4) 4477 >>> print("%.x" % v0.as_long()) 4479 >>> v = simplify(RepeatBitVec(4, v0)) 4482 >>> print("%.x" % v.as_long()) 4486

_z3_assert(_is_int(n),

"First argument must be an integer"

)

4487

_z3_assert(

(a),

"Second argument must be a Z3 bit-vector expression"

)

4492 """Return the reduction-and expression of `a`.""" 4494

_z3_assert(

(a),

"First argument must be a Z3 bit-vector expression"

)

4499 """Return the reduction-or expression of `a`.""" 4501

_z3_assert(

(a),

"First argument must be a Z3 bit-vector expression"

)

4506 """A predicate the determines that bit-vector addition does not overflow""" 4507

_check_bv_args(a, b)

4508

a, b = _coerce_exprs(a, b)

4513 """A predicate the determines that signed bit-vector addition does not underflow""" 4514

_check_bv_args(a, b)

4515

a, b = _coerce_exprs(a, b)

4520 """A predicate the determines that bit-vector subtraction does not overflow""" 4521

_check_bv_args(a, b)

4522

a, b = _coerce_exprs(a, b)

4527 """A predicate the determines that bit-vector subtraction does not underflow""" 4528

_check_bv_args(a, b)

4529

a, b = _coerce_exprs(a, b)

4534 """A predicate the determines that bit-vector signed division does not overflow""" 4535

_check_bv_args(a, b)

4536

a, b = _coerce_exprs(a, b)

4541 """A predicate the determines that bit-vector unary negation does not overflow""" 4543

_z3_assert(

(a),

"First argument must be a Z3 bit-vector expression"

)

4548 """A predicate the determines that bit-vector multiplication does not overflow""" 4549

_check_bv_args(a, b)

4550

a, b = _coerce_exprs(a, b)

4555 """A predicate the determines that bit-vector signed multiplication does not underflow""" 4556

_check_bv_args(a, b)

4557

a, b = _coerce_exprs(a, b)

4571 """Return the domain of the array sort `self`. 4573 >>> A = ArraySort(IntSort(), BoolSort()) 4580 """Return the domain of the array sort `self`. 4585 """Return the range of the array sort `self`. 4587 >>> A = ArraySort(IntSort(), BoolSort()) 4595 """Array expressions. """ 4598 """Return the array sort of the array expression `self`. 4600 >>> a = Array('a', IntSort(), BoolSort()) 4607 """Shorthand for `self.sort().domain()`. 4609 >>> a = Array('a', IntSort(), BoolSort()) 4616 """Shorthand for self.sort().domain_n(i)`.""" 4620 """Shorthand for `self.sort().range()`. 4622 >>> a = Array('a', IntSort(), BoolSort()) 4629 """Return the Z3 expression `self[arg]`. 4631 >>> a = Array('a', IntSort(), BoolSort()) 4638 return

_array_select(self, arg)

4644 def

_array_select(ar, arg):

4645 if

isinstance(arg, tuple):

4646

args = [ar.sort().

domain_n

(i).cast(arg[i])

for

in range

(len(arg))]

4647

_args, sz = _to_ast_array(args)

4648 return

_to_expr_ref(

Z3_mk_select_n

(ar.ctx_ref(), ar.as_ast(), sz, _args), ar.ctx)

4649

arg = ar.sort().

domain

().cast(arg)

4650 return

_to_expr_ref(

Z3_mk_select

(ar.ctx_ref(), ar.as_ast(), arg.as_ast()), ar.ctx)

4658 """Return `True` if `a` is a Z3 array expression. 4660 >>> a = Array('a', IntSort(), IntSort()) 4663 >>> is_array(Store(a, 0, 1)) 4668 return

isinstance(a, ArrayRef)

4672 """Return `True` if `a` is a Z3 constant array. 4674 >>> a = K(IntSort(), 10) 4675 >>> is_const_array(a) 4677 >>> a = Array('a', IntSort(), IntSort()) 4678 >>> is_const_array(a) 4685 """Return `True` if `a` is a Z3 constant array. 4687 >>> a = K(IntSort(), 10) 4690 >>> a = Array('a', IntSort(), IntSort()) 4698 """Return `True` if `a` is a Z3 map array expression. 4700 >>> f = Function('f', IntSort(), IntSort()) 4701 >>> b = Array('b', IntSort(), IntSort()) 4714 """Return `True` if `a` is a Z3 default array expression. 4715 >>> d = Default(K(IntSort(), 10)) 4719 return is_app_of

(a, Z3_OP_ARRAY_DEFAULT)

4723 """Return the function declaration associated with a Z3 map array expression. 4725 >>> f = Function('f', IntSort(), IntSort()) 4726 >>> b = Array('b', IntSort(), IntSort()) 4728 >>> eq(f, get_map_func(a)) 4732 >>> get_map_func(a)(0) 4736

_z3_assert(

is_map

(a),

"Z3 array map expression expected."

)

4747 """Return the Z3 array sort with the given domain and range sorts. 4749 >>> A = ArraySort(IntSort(), BoolSort()) 4756 >>> AA = ArraySort(IntSort(), A) 4758 Array(Int, Array(Int, Bool)) 4760

sig = _get_args(sig)

4762

_z3_assert(len(sig) > 1,

"At least two arguments expected"

)

4763

arity = len(sig) - 1

4768

_z3_assert(

(s),

"Z3 sort expected"

)

4769

_z3_assert(s.ctx == r.ctx,

"Context mismatch"

)

4773

dom = (Sort * arity)()

4774 for

in range

(arity):

4780 """Return an array constant named `name` with the given domain and range sorts. 4782 >>> a = Array('a', IntSort(), IntSort()) 4794 """Return a Z3 store array expression. 4796 >>> a = Array('a', IntSort(), IntSort()) 4797 >>> i, v = Ints('i v') 4798 >>> s = Update(a, i, v) 4801 >>> prove(s[i] == v) 4804 >>> prove(Implies(i != j, s[j] == a[j])) 4808

_z3_assert(

is_array_sort

(a),

"First argument must be a Z3 array expression"

)

4809

args = _get_args(args)

4812 raise

Z3Exception(

"array update requires index and value arguments"

)

4816

i = a.sort().domain().cast(i)

4817

v = a.sort().

range

().cast(v)

4818 return

_to_expr_ref(

Z3_mk_store

(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)

4819

v = a.sort().

range

().cast(args[-1])

4820

idxs = [a.sort().domain_n(i).cast(args[i])

for

in range

(len(args)-1)]

4821

_args, sz = _to_ast_array(idxs)

4822 return

_to_expr_ref(

Z3_mk_store_n

(ctx.ref(), a.as_ast(), sz, _args, v.as_ast()), ctx)

4826 """ Return a default value for array expression. 4827 >>> b = K(IntSort(), 1) 4828 >>> prove(Default(b) == 1) 4832

_z3_assert(

is_array_sort

(a),

"First argument must be a Z3 array expression"

)

4837 """Return a Z3 store array expression. 4839 >>> a = Array('a', IntSort(), IntSort()) 4840 >>> i, v = Ints('i v') 4841 >>> s = Store(a, i, v) 4844 >>> prove(s[i] == v) 4847 >>> prove(Implies(i != j, s[j] == a[j])) 4854 """Return a Z3 select array expression. 4856 >>> a = Array('a', IntSort(), IntSort()) 4860 >>> eq(Select(a, i), a[i]) 4863

args = _get_args(args)

4865

_z3_assert(

is_array_sort

(a),

"First argument must be a Z3 array expression"

)

4870 """Return a Z3 map array expression. 4872 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 4873 >>> a1 = Array('a1', IntSort(), IntSort()) 4874 >>> a2 = Array('a2', IntSort(), IntSort()) 4875 >>> b = Map(f, a1, a2) 4878 >>> prove(b[0] == f(a1[0], a2[0])) 4881

args = _get_args(args)

4883

_z3_assert(len(args) > 0,

"At least one Z3 array expression expected"

)

4884

_z3_assert(

is_func_decl

(f),

"First argument must be a Z3 function declaration"

)

4885

_z3_assert(all([

is_array

(a)

for

in

args]),

"Z3 array expected expected"

)

4886

_z3_assert(len(args) == f.arity(),

"Number of arguments mismatch"

)

4887

_args, sz = _to_ast_array(args)

4893 """Return a Z3 constant array expression. 4895 >>> a = K(IntSort(), 10) 4907

_z3_assert(

(dom),

"Z3 sort expected"

)

4910

v = _py2expr(v, ctx)

4915 """Return extensionality index for one-dimensional arrays. 4916 >> a, b = Consts('a b', SetSort(IntSort())) 4923 return

_to_expr_ref(

Z3_mk_array_ext

(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

4928

k = _py2expr(k, ctx)

4933 """Return `True` if `a` is a Z3 array select application. 4935 >>> a = Array('a', IntSort(), IntSort()) 4946 """Return `True` if `a` is a Z3 array store application. 4948 >>> a = Array('a', IntSort(), IntSort()) 4951 >>> is_store(Store(a, 0, 1)) 4964 """ Create a set sort over element sort s""" 4969 """Create the empty set 4970 >>> EmptySet(IntSort()) 4978 """Create the full set 4979 >>> FullSet(IntSort()) 4987 """ Take the union of sets 4988 >>> a = Const('a', SetSort(IntSort())) 4989 >>> b = Const('b', SetSort(IntSort())) 4993

args = _get_args(args)

4994

ctx = _ctx_from_ast_arg_list(args)

4995

_args, sz = _to_ast_array(args)

5000 """ Take the union of sets 5001 >>> a = Const('a', SetSort(IntSort())) 5002 >>> b = Const('b', SetSort(IntSort())) 5003 >>> SetIntersect(a, b) 5006

args = _get_args(args)

5007

ctx = _ctx_from_ast_arg_list(args)

5008

_args, sz = _to_ast_array(args)

5013 """ Add element e to set s 5014 >>> a = Const('a', SetSort(IntSort())) 5018

ctx = _ctx_from_ast_arg_list([s, e])

5019

e = _py2expr(e, ctx)

5024 """ Remove element e to set s 5025 >>> a = Const('a', SetSort(IntSort())) 5029

ctx = _ctx_from_ast_arg_list([s, e])

5030

e = _py2expr(e, ctx)

5035 """ The complement of set s 5036 >>> a = Const('a', SetSort(IntSort())) 5037 >>> SetComplement(a) 5045 """ The set difference of a and b 5046 >>> a = Const('a', SetSort(IntSort())) 5047 >>> b = Const('b', SetSort(IntSort())) 5048 >>> SetDifference(a, b) 5051

ctx = _ctx_from_ast_arg_list([a, b])

5056 """ Check if e is a member of set s 5057 >>> a = Const('a', SetSort(IntSort())) 5061

ctx = _ctx_from_ast_arg_list([s, e])

5062

e = _py2expr(e, ctx)

5067 """ Check if a is a subset of b 5068 >>> a = Const('a', SetSort(IntSort())) 5069 >>> b = Const('b', SetSort(IntSort())) 5073

ctx = _ctx_from_ast_arg_list([a, b])

5083 def

_valid_accessor(acc):

5084 """Return `True` if acc is pair of the form (String, Datatype or Sort). """ 5085 if not

isinstance(acc, tuple):

5089 return

isinstance(acc[0], str)

and

(isinstance(acc[1], Datatype)

or is_sort

(acc[1]))

5093 """Helper class for declaring Z3 datatypes. 5095 >>> List = Datatype('List') 5096 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 5097 >>> List.declare('nil') 5098 >>> List = List.create() 5099 >>> # List is now a Z3 declaration 5102 >>> List.cons(10, List.nil) 5104 >>> List.cons(10, List.nil).sort() 5106 >>> cons = List.cons 5110 >>> n = cons(1, cons(0, nil)) 5112 cons(1, cons(0, nil)) 5113 >>> simplify(cdr(n)) 5115 >>> simplify(car(n)) 5126

r.constructors = copy.deepcopy(self.

constructors

constructors)

5131

_z3_assert(isinstance(name, str),

"String expected"

)

5132

_z3_assert(isinstance(rec_name, str),

"String expected"

)

5134

all([_valid_accessor(a)

for

in

args]),

5135 "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)"

5137

self.

constructors

constructors.append((name, rec_name, args))

5140 """Declare constructor named `name` with the given accessors `args`. 5141 Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort 5142 or a reference to the datatypes being declared. 5144 In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))` 5145 declares the constructor named `cons` that builds a new List using an integer and a List. 5146 It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer 5147 of a `cons` cell, and `cdr` the list of a `cons` cell. After all constructors were declared, 5148 we use the method create() to create the actual datatype in Z3. 5150 >>> List = Datatype('List') 5151 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 5152 >>> List.declare('nil') 5153 >>> List = List.create() 5156

_z3_assert(isinstance(name, str),

"String expected"

)

5157

_z3_assert(name !=

""

"Constructor name cannot be empty"

)

5158 return

self.

declare_core

declare_core(name,

"is-"

+ name, *args)

5161 return "Datatype(%s, %s)"

% (self.

name

name, self.

constructors

constructors)

5164 """Create a Z3 datatype based on the constructors declared using the method `declare()`. 5166 The function `CreateDatatypes()` must be used to define mutually recursive datatypes. 5168 >>> List = Datatype('List') 5169 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 5170 >>> List.declare('nil') 5171 >>> List = List.create() 5174 >>> List.cons(10, List.nil) 5181 """Auxiliary object used to create Z3 datatypes.""" 5188 if

self.

ctx.ref()

is not None and

Z3_del_constructor

is not None

5193 """Auxiliary object used to create Z3 datatypes.""" 5200 if

self.

ctx.ref()

is not None and

Z3_del_constructor_list

is not None

5205 """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects. 5207 In the following example we define a Tree-List using two mutually recursive datatypes. 5209 >>> TreeList = Datatype('TreeList') 5210 >>> Tree = Datatype('Tree') 5211 >>> # Tree has two constructors: leaf and node 5212 >>> Tree.declare('leaf', ('val', IntSort())) 5213 >>> # a node contains a list of trees 5214 >>> Tree.declare('node', ('children', TreeList)) 5215 >>> TreeList.declare('nil') 5216 >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList)) 5217 >>> Tree, TreeList = CreateDatatypes(Tree, TreeList) 5218 >>> Tree.val(Tree.leaf(10)) 5220 >>> simplify(Tree.val(Tree.leaf(10))) 5222 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil))) 5224 node(cons(leaf(10), cons(leaf(20), nil))) 5225 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil)) 5226 >>> simplify(n2 == n1) 5228 >>> simplify(TreeList.car(Tree.children(n2)) == n1) 5233

_z3_assert(len(ds) > 0,

"At least one Datatype must be specified"

)

5234

_z3_assert(all([isinstance(d, Datatype)

for

in

ds]),

"Arguments must be Datatypes"

)

5235

_z3_assert(all([d.ctx == ds[0].ctx

for

in

ds]),

"Context mismatch"

)

5236

_z3_assert(all([d.constructors != []

for

in

ds]),

"Non-empty Datatypes expected"

)

5239

names = (Symbol * num)()

5240

out = (Sort * num)()

5241

clists = (ConstructorList * num)()

5243 for

in range

(num):

5246

num_cs = len(d.constructors)

5247

cs = (Constructor * num_cs)()

5248 for

in range

(num_cs):

5249

c = d.constructors[j]

5254

fnames = (Symbol * num_fs)()

5255

sorts = (Sort * num_fs)()

5256

refs = (ctypes.c_uint * num_fs)()

5257 for

in range

(num_fs):

5261 if

isinstance(ftype, Datatype):

5264

ds.count(ftype) == 1,

5265 "One and only one occurrence of each datatype is expected"

5268

refs[k] = ds.index(ftype)

5271

_z3_assert(

(ftype),

"Z3 sort expected"

)

5272

sorts[k] = ftype.ast

5274

cs[j] =

Z3_mk_constructor

(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)

5281 for

in range

(num):

5283

num_cs = dref.num_constructors()

5284 for

in range

(num_cs):

5285

cref = dref.constructor(j)

5286

cref_name = cref.name()

5287

cref_arity = cref.arity()

5288 if

cref.arity() == 0:

5290

setattr(dref, cref_name, cref)

5291

rref = dref.recognizer(j)

5292

setattr(dref,

"is_"

+ cref_name, rref)

5293 for

in range

(cref_arity):

5294

aref = dref.accessor(j, k)

5295

setattr(dref, aref.name(), aref)

5297 return

tuple(result)

5301 """Datatype sorts.""" 5304 """Return the number of constructors in the given Z3 datatype. 5306 >>> List = Datatype('List') 5307 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 5308 >>> List.declare('nil') 5309 >>> List = List.create() 5310 >>> # List is now a Z3 declaration 5311 >>> List.num_constructors() 5317 """Return a constructor of the datatype `self`. 5319 >>> List = Datatype('List') 5320 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 5321 >>> List.declare('nil') 5322 >>> List = List.create() 5323 >>> # List is now a Z3 declaration 5324 >>> List.num_constructors() 5326 >>> List.constructor(0) 5328 >>> List.constructor(1) 5332

_z3_assert(idx < self.

num_constructors

num_constructors(),

"Invalid constructor index"

)

5336 """In Z3, each constructor has an associated recognizer predicate. 5338 If the constructor is named `name`, then the recognizer `is_name`. 5340 >>> List = Datatype('List') 5341 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 5342 >>> List.declare('nil') 5343 >>> List = List.create() 5344 >>> # List is now a Z3 declaration 5345 >>> List.num_constructors() 5347 >>> List.recognizer(0) 5349 >>> List.recognizer(1) 5351 >>> simplify(List.is_nil(List.cons(10, List.nil))) 5353 >>> simplify(List.is_cons(List.cons(10, List.nil))) 5355 >>> l = Const('l', List) 5356 >>> simplify(List.is_cons(l)) 5360

_z3_assert(idx < self.

num_constructors

num_constructors(),

"Invalid recognizer index"

)

5364 """In Z3, each constructor has 0 or more accessor. 5365 The number of accessors is equal to the arity of the constructor. 5367 >>> List = Datatype('List') 5368 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 5369 >>> List.declare('nil') 5370 >>> List = List.create() 5371 >>> List.num_constructors() 5373 >>> List.constructor(0) 5375 >>> num_accs = List.constructor(0).arity() 5378 >>> List.accessor(0, 0) 5380 >>> List.accessor(0, 1) 5382 >>> List.constructor(1) 5384 >>> num_accs = List.constructor(1).arity() 5389

_z3_assert(i < self.

num_constructors

num_constructors(),

"Invalid constructor index"

)

5390

_z3_assert(j < self.

constructor

constructor(i).arity(),

"Invalid accessor index"

)

5398 """Datatype expressions.""" 5401 """Return the datatype sort of the datatype expression `self`.""" 5405 """Create a reference to a sort that was declared, or will be declared, as a recursive datatype""" 5410 """Create a named tuple sort base on a set of underlying sorts 5412 >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()]) 5415

projects = [(

"project%d"

% i, sorts[i])

for

in range

(len(sorts))]

5416

tuple.declare(name, *projects)

5417

tuple = tuple.create()

5418 return

tuple, tuple.constructor(0), [tuple.accessor(0, i)

for

in range

(len(sorts))]

5422 """Create a named tagged union sort base on a set of underlying sorts 5424 >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()]) 5427 for

in range

(len(sorts)):

5428

sum.declare(

"inject%d"

% i, (

"project%d"

% i, sorts[i]))

5430 return

sum, [(sum.constructor(i), sum.accessor(i, 0))

for

in range

(len(sorts))]

5434 """Return a new enumeration sort named `name` containing the given values. 5436 The result is a pair (sort, list of constants). 5438 >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue']) 5441

_z3_assert(isinstance(name, str),

"Name must be a string"

)

5442

_z3_assert(all([isinstance(v, str)

for

in

values]),

"Enumeration sort values must be strings"

)

5443

_z3_assert(len(values) > 0,

"At least one value expected"

)

5446

_val_names = (Symbol * num)()

5447 for

in range

(num):

5448

_val_names[i] =

to_symbol

(values[i], ctx)

5449

_values = (FuncDecl * num)()

5450

_testers = (FuncDecl * num)()

5454 for

in range

(num):

5456

V = [a()

for

in

5467 """Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3. 5469 Consider using the function `args2params` to create instances of this object. 5477

self.

params

params = params

5484 if

self.

ctx.ref()

is not None and

Z3_params_dec_ref

is not None

5488 """Set parameter name with value val.""" 5490

_z3_assert(isinstance(name, str),

"parameter name must be a string"

)

5492 if

isinstance(val, bool):

5496 elif

isinstance(val, float):

5498 elif

isinstance(val, str):

5502

_z3_assert(

False

"invalid parameter value"

)

5508

_z3_assert(isinstance(ds, ParamDescrsRef),

"parameter description set expected"

)

5513 """Convert python arguments into a Z3_params object. 5514 A ':' is added to the keywords, and '_' is replaced with '-' 5516 >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) 5517 (params model true relevancy 2 elim_and true) 5520

_z3_assert(len(arguments) % 2 == 0,

"Argument list must have an even number of elements."

)

5536 """Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3. 5540

_z3_assert(isinstance(descr, ParamDescrs),

"parameter description object expected"

)

5546 return

ParamsDescrsRef(self.

descr

descr, self.

ctx)

5549 if

self.

ctx.ref()

is not None and

Z3_param_descrs_dec_ref

is not None

5553 """Return the size of in the parameter description `self`. 5558 """Return the size of in the parameter description `self`. 5560 return

self.

size

size()

5563 """Return the i-th parameter name in the parameter description `self`. 5568 """Return the kind of the parameter named `n`. 5573 """Return the documentation string of the parameter named `n`. 5579 return

self.

get_name

get_name(arg)

5581 return

self.

get_kind

get_kind(arg)

5594 """Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible). 5596 Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals. 5597 A goal has a solution if one of its subgoals has a solution. 5598 A goal is unsatisfiable if all subgoals are unsatisfiable. 5601 def __init__

(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):

5603

_z3_assert(goal

is None or

ctx

is not None

5604 "If goal is different from None, then ctx must be also different from None"

)

5607 if

self.

goal

is None

5612 if

self.

goal

is not None and

self.

ctx.ref()

is not None and

Z3_goal_dec_ref

is not None

5616 """Return the depth of the goal `self`. 5617 The depth corresponds to the number of tactics applied to `self`. 5619 >>> x, y = Ints('x y') 5621 >>> g.add(x == 0, y >= x + 1) 5624 >>> r = Then('simplify', 'solve-eqs')(g) 5625 >>> # r has 1 subgoal 5634 """Return `True` if `self` contains the `False` constraints. 5636 >>> x, y = Ints('x y') 5638 >>> g.inconsistent() 5640 >>> g.add(x == 0, x == 1) 5643 >>> g.inconsistent() 5645 >>> g2 = Tactic('propagate-values')(g)[0] 5646 >>> g2.inconsistent() 5652 """Return the precision (under-approximation, over-approximation, or precise) of the goal `self`. 5655 >>> g.prec() == Z3_GOAL_PRECISE 5657 >>> x, y = Ints('x y') 5658 >>> g.add(x == y + 1) 5659 >>> g.prec() == Z3_GOAL_PRECISE 5661 >>> t = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10) 5664 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0] 5665 >>> g2.prec() == Z3_GOAL_PRECISE 5667 >>> g2.prec() == Z3_GOAL_UNDER 5673 """Alias for `prec()`. 5676 >>> g.precision() == Z3_GOAL_PRECISE 5679 return

self.

prec

prec()

5682 """Return the number of constraints in the goal `self`. 5687 >>> x, y = Ints('x y') 5688 >>> g.add(x == 0, y > x) 5695 """Return the number of constraints in the goal `self`. 5700 >>> x, y = Ints('x y') 5701 >>> g.add(x == 0, y > x) 5705 return

self.

size

size()

5708 """Return a constraint in the goal `self`. 5711 >>> x, y = Ints('x y') 5712 >>> g.add(x == 0, y > x) 5721 """Return a constraint in the goal `self`. 5724 >>> x, y = Ints('x y') 5725 >>> g.add(x == 0, y > x) 5731 if

arg >= len(self):

5733 return

self.

get

get(arg)

5736 """Assert constraints into the goal. 5740 >>> g.assert_exprs(x > 0, x < 2) 5744

args = _get_args(args)

5755 >>> g.append(x > 0, x < 2) 5766 >>> g.insert(x > 0, x < 2) 5777 >>> g.add(x > 0, x < 2) 5784 """Retrieve model from a satisfiable goal 5785 >>> a, b = Ints('a b') 5787 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 5788 >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs')) 5791 [Or(b == 0, b == 1), Not(0 <= b)] 5793 [Or(b == 0, b == 1), Not(1 <= b)] 5794 >>> # Remark: the subgoal r[0] is unsatisfiable 5795 >>> # Creating a solver for solving the second subgoal 5802 >>> # Model s.model() does not assign a value to `a` 5803 >>> # It is a model for subgoal `r[1]`, but not for goal `g` 5804 >>> # The method convert_model creates a model for `g` from a model for `r[1]`. 5805 >>> r[1].convert_model(s.model()) 5809

_z3_assert(isinstance(model, ModelRef),

"Z3 Model expected"

)

5813 return

obj_to_string(self)

5816 """Return a textual representation of the s-expression representing the goal.""" 5820 """Return a textual representation of the goal in DIMACS format.""" 5824 """Copy goal `self` to context `target`. 5832 >>> g2 = g.translate(c2) 5835 >>> g.ctx == main_ctx() 5839 >>> g2.ctx == main_ctx() 5843

_z3_assert(isinstance(target, Context),

"target must be a context"

)

5853 """Return a new simplified goal. 5855 This method is essentially invoking the simplify tactic. 5859 >>> g.add(x + 1 >= 2) 5862 >>> g2 = g.simplify() 5865 >>> # g was not modified 5869

t =

Tactic

(

"simplify"

)

5870 return

t.apply(self, *arguments, **keywords)[0]

5873 """Return goal `self` as a single Z3 expression. 5890 return

self.

get

get(0)

5892 return And

([self.

get

get(i)

for

in range

(len(self))], self.

ctx)

5902 """A collection (vector) of ASTs.""" 5911 assert

ctx

is not None 5916 if

self.

vector

is not None and

self.

ctx.ref()

is not None and

Z3_ast_vector_dec_ref

is not None

5920 """Return the size of the vector `self`. 5925 >>> A.push(Int('x')) 5926 >>> A.push(Int('x')) 5933 """Return the AST at position `i`. 5936 >>> A.push(Int('x') + 1) 5937 >>> A.push(Int('y')) 5944 if

isinstance(i, int):

5948 if

i >= self.

__len__

__len__():

5952 elif

isinstance(i, slice):

5955

result.append(_to_ast_ref(

5962 """Update AST at position `i`. 5965 >>> A.push(Int('x') + 1) 5966 >>> A.push(Int('y')) 5973 if

i >= self.

__len__

__len__():

5978 """Add `v` in the end of the vector. 5983 >>> A.push(Int('x')) 5990 """Resize the vector to `sz` elements. 5996 >>> for i in range(10): A[i] = Int('x') 6003 """Return `True` if the vector contains `item`. 6026 """Copy vector `self` to context `other_ctx`. 6032 >>> B = A.translate(c2) 6048 return

obj_to_string(self)

6051 """Return a textual representation of the s-expression representing the vector.""" 6062 """A mapping from ASTs to ASTs.""" 6071 assert

ctx

is not None 6079 if

self.

map

is not None and

self.

ctx.ref()

is not None and

Z3_ast_map_dec_ref

is not None

6083 """Return the size of the map. 6089 >>> M[x] = IntVal(1) 6096 """Return `True` if the map contains key `key`. 6109 """Retrieve the value associated with key `key`. 6120 """Add/Update key `k` with value `v`. 6129 >>> M[x] = IntVal(1) 6139 """Remove the entry associated with key `k`. 6153 """Remove all entries from the map. 6158 >>> M[x+x] = IntVal(1) 6168 """Return an AstVector containing all keys in the map. 6173 >>> M[x+x] = IntVal(1) 6187 """Store the value of the interpretation of a function in a particular point.""" 6198 if

self.

ctx.ref()

is not None and

Z3_func_entry_dec_ref

is not None

6202 """Return the number of arguments in the given entry. 6204 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 6206 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 6211 >>> f_i.num_entries() 6213 >>> e = f_i.entry(0) 6220 """Return the value of argument `idx`. 6222 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 6224 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 6229 >>> f_i.num_entries() 6231 >>> e = f_i.entry(0) 6242 ... except IndexError: 6243 ... print("index error") 6246 if

idx >= self.

num_args

num_args():

6251 """Return the value of the function at point `self`. 6253 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 6255 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 6260 >>> f_i.num_entries() 6262 >>> e = f_i.entry(0) 6273 """Return entry `self` as a Python list. 6274 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 6276 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 6281 >>> f_i.num_entries() 6283 >>> e = f_i.entry(0) 6288

args.append(self.

value

value())

6292 return

repr(self.

as_list

as_list())

6296 """Stores the interpretation of a function in a Z3 model.""" 6301 if

self.

is not None

6305 if

self.

is not None and

self.

ctx.ref()

is not None and

Z3_func_interp_dec_ref

is not None

6310 Return the `else` value for a function interpretation. 6311 Return None if Z3 did not specify the `else` value for 6314 >>> f = Function('f', IntSort(), IntSort()) 6316 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 6322 >>> m[f].else_value() 6327 return

_to_expr_ref(r, self.

ctx)

6332 """Return the number of entries/points in the function interpretation `self`. 6334 >>> f = Function('f', IntSort(), IntSort()) 6336 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 6342 >>> m[f].num_entries() 6348 """Return the number of arguments for each entry in the function interpretation `self`. 6350 >>> f = Function('f', IntSort(), IntSort()) 6352 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 6362 """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`. 6364 >>> f = Function('f', IntSort(), IntSort()) 6366 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 6372 >>> m[f].num_entries() 6382 """Copy model 'self' to context 'other_ctx'. 6393 """Return the function interpretation as a Python list. 6394 >>> f = Function('f', IntSort(), IntSort()) 6396 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 6410 return

obj_to_string(self)

6414 """Model/Solution of a satisfiability problem (aka system of constraints).""" 6417 assert

ctx

is not None 6423 if

self.

ctx.ref()

is not None and

Z3_model_dec_ref

is not None

6427 return

obj_to_string(self)

6430 """Return a textual representation of the s-expression representing the model.""" 6433 def eval

(self, t, model_completion=False):

6434 """Evaluate the expression `t` in the model `self`. 6435 If `model_completion` is enabled, then a default interpretation is automatically added 6436 for symbols that do not have an interpretation in the model `self`. 6440 >>> s.add(x > 0, x < 2) 6453 >>> m.eval(y, model_completion=True) 6455 >>> # Now, m contains an interpretation for y 6461 return

_to_expr_ref(r[0], self.

ctx)

6462 raise

Z3Exception(

"failed to evaluate expression in the model"

)

6465 """Alias for `eval`. 6469 >>> s.add(x > 0, x < 2) 6473 >>> m.evaluate(x + 1) 6475 >>> m.evaluate(x == 1) 6478 >>> m.evaluate(y + x) 6482 >>> m.evaluate(y, model_completion=True) 6484 >>> # Now, m contains an interpretation for y 6485 >>> m.evaluate(y + x) 6488 return

self.

eval

eval(t, model_completion)

6491 """Return the number of constant and function declarations in the model `self`. 6493 >>> f = Function('f', IntSort(), IntSort()) 6496 >>> s.add(x > 0, f(x) != x) 6505 return

num_consts + num_funcs

6508 """Return the interpretation for a given declaration or constant. 6510 >>> f = Function('f', IntSort(), IntSort()) 6513 >>> s.add(x > 0, x < 2, f(x) == 0) 6523

_z3_assert(isinstance(decl, FuncDeclRef)

or is_const

(decl),

"Z3 declaration expected"

)

6527 if

decl.arity() == 0:

6529 if

_r.value

is None

6531

r = _to_expr_ref(_r, self.

ctx)

6545

sz = fi.num_entries()

6549

e =

Store

(e, fe.arg_value(0), fe.value())

6560 """Return the number of uninterpreted sorts that contain an interpretation in the model `self`. 6562 >>> A = DeclareSort('A') 6563 >>> a, b = Consts('a b', A) 6575 """Return the uninterpreted sort at position `idx` < self.num_sorts(). 6577 >>> A = DeclareSort('A') 6578 >>> B = DeclareSort('B') 6579 >>> a1, a2 = Consts('a1 a2', A) 6580 >>> b1, b2 = Consts('b1 b2', B) 6582 >>> s.add(a1 != a2, b1 != b2) 6598 """Return all uninterpreted sorts that have an interpretation in the model `self`. 6600 >>> A = DeclareSort('A') 6601 >>> B = DeclareSort('B') 6602 >>> a1, a2 = Consts('a1 a2', A) 6603 >>> b1, b2 = Consts('b1 b2', B) 6605 >>> s.add(a1 != a2, b1 != b2) 6615 """Return the interpretation for the uninterpreted sort `s` in the model `self`. 6617 >>> A = DeclareSort('A') 6618 >>> a, b = Consts('a b', A) 6624 >>> m.get_universe(A) 6628

_z3_assert(isinstance(s, SortRef),

"Z3 sort expected"

)

6635 """If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. 6636 If `idx` is a declaration, then the actual interpretation is returned. 6638 The elements can be retrieved using position or the actual declaration. 6640 >>> f = Function('f', IntSort(), IntSort()) 6643 >>> s.add(x > 0, x < 2, f(x) == 0) 6657 >>> for d in m: print("%s -> %s" % (d, m[d])) 6662 if

idx >= len(self):

6665 if

(idx < num_consts):

6669 if

isinstance(idx, FuncDeclRef):

6672 return

self.

get_interp

get_interp(idx.decl())

6673 if

isinstance(idx, SortRef):

6676

_z3_assert(

False

"Integer, Z3 declaration, or Z3 constant expected"

)

6680 """Return a list with all symbols that have an interpretation in the model `self`. 6681 >>> f = Function('f', IntSort(), IntSort()) 6684 >>> s.add(x > 0, x < 2, f(x) == 0) 6699 """Update the interpretation of a constant""" 6702 if is_func_decl

(x)

and

x.arity() != 0

and

isinstance(value, FuncInterp):

6706 for

in range

(value.num_entries()):

6711

v.push(e.arg_value(j))

6716 raise

Z3Exception(

"Expecting 0-ary function or constant expression"

)

6717

value = _py2expr(value)

6721 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 6724

_z3_assert(isinstance(target, Context),

"argument must be a Z3 context"

)

6741 """Return true if n is a Z3 expression of the form (_ as-array f).""" 6742 return

isinstance(n, ExprRef)

and Z3_is_as_array

(n.ctx.ref(), n.as_ast())

6746 """Return the function declaration f associated with a Z3 expression of the form (_ as-array f).""" 6748

_z3_assert(

is_as_array

(n),

"as-array Z3 expression expected."

)

6759 """Statistics for `Solver.check()`.""" 6770 if

self.

ctx.ref()

is not None and

Z3_stats_dec_ref

is not None

6777

out.write(u(

'<table border="1" cellpadding="2" cellspacing="0">'

))

6780

out.write(u(

'<tr style="background-color:#CFCFCF">'

))

6783

out.write(u(

"<tr>"

))

6785

out.write(u(

"<td>%s</td><td>%s</td></tr>"

% (k, v)))

6786

out.write(u(

"</table>"

))

6787 return

out.getvalue()

6792 """Return the number of statistical counters. 6795 >>> s = Then('simplify', 'nlsat').solver() 6799 >>> st = s.statistics() 6806 """Return the value of statistical counter at position `idx`. The result is a pair (key, value). 6809 >>> s = Then('simplify', 'nlsat').solver() 6813 >>> st = s.statistics() 6817 ('nlsat propagations', 2) 6819 ('nlsat restarts', 1) 6821 if

idx >= len(self):

6830 """Return the list of statistical counters. 6833 >>> s = Then('simplify', 'nlsat').solver() 6837 >>> st = s.statistics() 6842 """Return the value of a particular statistical counter. 6845 >>> s = Then('simplify', 'nlsat').solver() 6849 >>> st = s.statistics() 6850 >>> st.get_key_value('nlsat propagations') 6853 for

idx

in range

(len(self)):

6859 raise

Z3Exception(

"unknown key"

)

6862 """Access the value of statistical using attributes. 6864 Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'), 6865 we should use '_' (e.g., 'nlsat_propagations'). 6868 >>> s = Then('simplify', 'nlsat').solver() 6872 >>> st = s.statistics() 6873 >>> st.nlsat_propagations 6878

key = name.replace(

"_"

" "

)

6882 raise

AttributeError

6892 """Represents the result of a satisfiability check: sat, unsat, unknown. 6898 >>> isinstance(r, CheckSatResult) 6909 return

isinstance(other, CheckSatResult)

and

self.

r == other.r

6912 return not

self.

__eq__

__eq__(other)

6916 if

self.

r == Z3_L_TRUE:

6918 elif

self.

r == Z3_L_FALSE:

6919 return "unsat" 6921 return "unknown" 6923 if

self.

r == Z3_L_TRUE:

6925 elif

self.

r == Z3_L_FALSE:

6930 def

_repr_html_(self):

6931

in_html = in_html_mode()

6932

set_html_mode(

True

)

6934

set_html_mode(in_html)

6945 Solver API provides methods for implementing the main SMT 2.0 commands: 6946 push, pop, check, get-model, etc. 6949 def __init__

(self, solver=None, ctx=None, logFile=None):

6950 assert

solver

is None or

ctx

is not None 6957

self.

solver

solver = solver

6959 if

logFile

is not None

6960

self.

set

set(

"smtlib2_log"

, logFile)

6963 if

self.

solver

is not None and

self.

ctx.ref()

is not None and

Z3_solver_dec_ref

is not None

6973 def set

(self, *args, **keys):

6974 """Set a configuration option. 6975 The method `help()` return a string containing all available options. 6978 >>> # The option MBQI can be set using three different approaches. 6979 >>> s.set(mbqi=True) 6980 >>> s.set('MBQI', True) 6981 >>> s.set(':mbqi', True) 6987 """Create a backtracking point. 7009 """Backtrack \\c num backtracking points. 7031 """Return the current number of backtracking points. 7049 """Remove all asserted constraints and backtracking points created using `push()`. 7063 """Assert constraints into the solver. 7067 >>> s.assert_exprs(x > 0, x < 2) 7071

args = _get_args(args)

7074 if

isinstance(arg, Goal)

or

isinstance(arg, AstVector):

7082 """Assert constraints into the solver. 7086 >>> s.add(x > 0, x < 2) 7097 """Assert constraints into the solver. 7101 >>> s.append(x > 0, x < 2) 7108 """Assert constraints into the solver. 7112 >>> s.insert(x > 0, x < 2) 7119 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`. 7121 If `p` is a string, it will be automatically converted into a Boolean constant. 7126 >>> s.set(unsat_core=True) 7127 >>> s.assert_and_track(x > 0, 'p1') 7128 >>> s.assert_and_track(x != 1, 'p2') 7129 >>> s.assert_and_track(x < 0, p3) 7130 >>> print(s.check()) 7132 >>> c = s.unsat_core() 7142 if

isinstance(p, str):

7144

_z3_assert(isinstance(a, BoolRef),

"Boolean expression expected"

)

7145

_z3_assert(isinstance(p, BoolRef)

and is_const

(p),

"Boolean expression expected"

)

7149 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not. 7155 >>> s.add(x > 0, x < 2) 7158 >>> s.model().eval(x) 7164 >>> s.add(2**x == 4) 7169

assumptions = _get_args(assumptions)

7170

num = len(assumptions)

7171

_assumptions = (Ast * num)()

7172 for

in range

(num):

7173

_assumptions[i] = s.cast(assumptions[i]).as_ast()

7178 """Return a model for the last `check()`. 7180 This function raises an exception if 7181 a model is not available (e.g., last `check()` returned unsat). 7185 >>> s.add(a + 2 == 0) 7194 raise

Z3Exception(

"model is not available"

)

7197 """Import model converter from other into the current solver""" 7201 """Interrupt the execution of the solver object. 7202 Remarks: This ensures that the interrupt applies only 7203 to the given solver object and it applies only if it is running. 7208 """Return a subset (as an AST vector) of the assumptions provided to the last check(). 7210 These are the assumptions Z3 used in the unsatisfiability proof. 7211 Assumptions are available in Z3. They are used to extract unsatisfiable cores. 7212 They may be also used to "retract" assumptions. Note that, assumptions are not really 7213 "soft constraints", but they can be used to implement them. 7215 >>> p1, p2, p3 = Bools('p1 p2 p3') 7216 >>> x, y = Ints('x y') 7218 >>> s.add(Implies(p1, x > 0)) 7219 >>> s.add(Implies(p2, y > x)) 7220 >>> s.add(Implies(p2, y < 1)) 7221 >>> s.add(Implies(p3, y > -3)) 7222 >>> s.check(p1, p2, p3) 7224 >>> core = s.unsat_core() 7233 >>> # "Retracting" p2 7240 """Determine fixed values for the variables based on the solver state and assumptions. 7242 >>> a, b, c, d = Bools('a b c d') 7243 >>> s.add(Implies(a,b), Implies(b, c)) 7244 >>> s.consequences([a],[b,c,d]) 7245 (sat, [Implies(a, b), Implies(a, c)]) 7246 >>> s.consequences([Not(c),d],[a,b,c,d]) 7247 (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))]) 7249 if

isinstance(assumptions, list):

7251 for

in

assumptions:

7254 if

isinstance(variables, list):

7259

_z3_assert(isinstance(assumptions, AstVector),

"ast vector expected"

)

7260

_z3_assert(isinstance(variables, AstVector),

"ast vector expected"

)

7263

variables.vector, consequences.vector)

7264

sz = len(consequences)

7265

consequences = [consequences[i]

for

in range

(sz)]

7269 """Parse assertions from a file""" 7273 """Parse assertions from a string""" 7278 The method takes an optional set of variables that restrict which 7279 variables may be used as a starting point for cubing. 7280 If vars is not None, then the first case split is based on a variable in 7284 if

vars

is not None

7291 if

(len(r) == 1

and is_false

(r[0])):

7298 """Access the set of variables that were touched by the most recently generated cube. 7299 This set of variables can be used as a starting point for additional cubes. 7300 The idea is that variables that appear in clauses that are reduced by the most recent 7301 cube are likely more useful to cube on.""" 7305

t = _py2expr(t, self.

ctx)

7306 """Retrieve congruence closure root of the term t relative to the current search state 7307 The function primarily works for SimpleSolver. Terms and variables that are 7308 eliminated during pre-processing are not visible to the congruence closure. 7313

t = _py2expr(t, self.

ctx)

7314 """Retrieve congruence closure sibling of the term t relative to the current search state 7315 The function primarily works for SimpleSolver. Terms and variables that are 7316 eliminated during pre-processing are not visible to the congruence closure. 7321 """Return a proof for the last `check()`. Proof construction must be enabled.""" 7325 """Return an AST vector containing all added constraints. 7339 """Return an AST vector containing all currently inferred units. 7344 """Return an AST vector containing all atomic formulas in solver state that are not units. 7349 """Return trail and decision levels of the solver state after a check() call. 7351

trail = self.

trail

trail()

7352

levels = (ctypes.c_uint * len(trail))()

7354 return

trail, levels

7357 """initialize the solver's state by setting the initial value of var to value 7360

value = s.cast(value)

7364 """Return trail of the solver state after a check() call. 7369 """Return statistics for the last `check()`. 7371 >>> s = SimpleSolver() 7376 >>> st = s.statistics() 7377 >>> st.get_key_value('final checks') 7387 """Return a string describing why the last `check()` returned `unknown`. 7390 >>> s = SimpleSolver() 7391 >>> s.add(2**x == 4) 7394 >>> s.reason_unknown() 7395 '(incomplete (theory arithmetic))' 7400 """Display a string describing all available options.""" 7404 """Return the parameter description set.""" 7408 """Return a formatted string with all added constraints.""" 7409 return

obj_to_string(self)

7412 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 7416 >>> s1 = Solver(ctx=c1) 7417 >>> s2 = s1.translate(c2) 7420

_z3_assert(isinstance(target, Context),

"argument must be a Z3 context"

)

7422 return Solver

(solver, target)

7431 """Return a formatted string (in Lisp-like format) with all added constraints. 7432 We say the string is in s-expression format. 7443 """Return a textual representation of the solver in DIMACS format.""" 7447 """return SMTLIB2 formatted benchmark for solver's assertions""" 7454 for

in range

(sz1):

7455

v[i] = es[i].as_ast()

7457

e = es[sz1].as_ast()

7461

self.

ctx.ref(),

"benchmark generated from python API"

""

"unknown"

""

, sz1, v, e,

7466 """Create a solver customized for the given logic. 7468 The parameter `logic` is a string. It should be contains 7469 the name of a SMT-LIB logic. 7470 See http://www.smtlib.org/ for the name of all available logics. 7472 >>> s = SolverFor("QF_LIA") 7487 """Return a simple general purpose solver with limited amount of preprocessing. 7489 >>> s = SimpleSolver() 7506 """Fixedpoint API provides methods for solving with recursive predicates""" 7509 assert

fixedpoint

is None or

ctx

is not None 7512 if

fixedpoint

is None

7520 return

FixedPoint(self.

fixedpoint, self.

ctx)

7523 if

self.

is not None and

self.

ctx.ref()

is not None and

Z3_fixedpoint_dec_ref

is not None

7526 def set

(self, *args, **keys):

7527 """Set a configuration option. The method `help()` return a string containing all available options. 7533 """Display a string describing all available options.""" 7537 """Return the parameter description set.""" 7541 """Assert constraints as background axioms for the fixedpoint solver.""" 7542

args = _get_args(args)

7545 if

isinstance(arg, Goal)

or

isinstance(arg, AstVector):

7555 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 7563 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 7567 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 7571 """Assert rules defining recursive predicates to the fixedpoint solver. 7574 >>> s = Fixedpoint() 7575 >>> s.register_relation(a.decl()) 7576 >>> s.register_relation(b.decl()) 7586

head = self.

abstract

abstract(head)

7589

body = _get_args(body)

7593 def rule

(self, head, body=None, name=None):

7594 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 7595

self.

add_rule

add_rule(head, body, name)

7598 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 7599

self.

add_rule

add_rule(head,

None

, name)

7602 """Query the fixedpoint engine whether formula is derivable. 7603 You can also pass an tuple or list of recursive predicates. 7605

query = _get_args(query)

7607 if

sz >= 1

and

isinstance(query[0], FuncDeclRef):

7608

_decls = (FuncDecl * sz)()

7618

query =

And

(query, self.

ctx)

7619

query = self.

abstract

abstract(query,

False

)

7624 """Query the fixedpoint engine whether formula is derivable starting at the given query level. 7626

query = _get_args(query)

7628 if

sz >= 1

and

isinstance(query[0], FuncDecl):

7629

_z3_assert(

False

"unsupported"

)

7635

query = self.

abstract

abstract(query,

False

)

7636

r = Z3_fixedpoint_query_from_lvl(self.

ctx.ref(), self.

fixedpoint, query.as_ast(), lvl)

7644

body = _get_args(body)

7649 """Retrieve answer from last query call.""" 7651 return

_to_expr_ref(r, self.

ctx)

7654 """Retrieve a ground cex from last query call.""" 7655

r = Z3_fixedpoint_get_ground_sat_answer(self.

ctx.ref(), self.

fixedpoint)

7656 return

_to_expr_ref(r, self.

ctx)

7659 """retrieve rules along the counterexample trace""" 7663 """retrieve rule names along the counterexample trace""" 7666

names = _symbol2py(self.

ctx, Z3_fixedpoint_get_rule_names_along_trace(self.

ctx.ref(), self.

fixedpoint))

7668 return

names.split(

";"

)

7671 """Retrieve number of levels used for predicate in PDR engine""" 7675 """Retrieve properties known about predicate for the level'th unfolding. 7676 -1 is treated as the limit (infinity) 7679 return

_to_expr_ref(r, self.

ctx)

7682 """Add property to predicate for the level'th unfolding. 7683 -1 is treated as infinity (infinity) 7688 """Register relation as recursive""" 7689

relations = _get_args(relations)

7694 """Control how relation is represented""" 7695

representations = _get_args(representations)

7696

representations = [

to_symbol

(s)

for

in

representations]

7697

sz = len(representations)

7698

args = (Symbol * sz)()

7699 for

in range

(sz):

7700

args[i] = representations[i]

7704 """Parse rules and queries from a string""" 7708 """Parse rules and queries from a file""" 7712 """retrieve rules that have been added to fixedpoint context""" 7716 """retrieve assertions that have been added to fixedpoint context""" 7720 """Return a formatted string with all added rules and constraints.""" 7721 return

self.

sexpr

sexpr()

7724 """Return a formatted string (in Lisp-like format) with all added constraints. 7725 We say the string is in s-expression format. 7730 """Return a formatted string (in Lisp-like format) with all added constraints. 7731 We say the string is in s-expression format. 7732 Include also queries. 7734

args, len = _to_ast_array(queries)

7738 """Return statistics for the last `query()`. 7743 """Return a string describing why the last `query()` returned `unknown`. 7748 """Add variable or several variables. 7749 The added variable or variables will be bound in the rules 7752

vars = _get_args(vars)

7754

self.

vars

vars += [v]

7757 if

self.

vars

vars == []:

7772 """Finite domain sort.""" 7775 """Return the size of the finite domain sort""" 7776

r = (ctypes.c_ulonglong * 1)()

7780 raise

Z3Exception(

"Failed to retrieve finite domain sort size"

)

7784 """Create a named finite domain sort of a given size sz""" 7785 if not

isinstance(name, Symbol):

7792 """Return True if `s` is a Z3 finite-domain sort. 7794 >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) 7796 >>> is_finite_domain_sort(IntSort()) 7799 return

isinstance(s, FiniteDomainSortRef)

7803 """Finite-domain expressions.""" 7806 """Return the sort of the finite-domain expression `self`.""" 7810 """Return a Z3 floating point expression as a Python string.""" 7815 """Return `True` if `a` is a Z3 finite-domain expression. 7817 >>> s = FiniteDomainSort('S', 100) 7818 >>> b = Const('b', s) 7819 >>> is_finite_domain(b) 7821 >>> is_finite_domain(Int('x')) 7824 return

isinstance(a, FiniteDomainRef)

7828 """Integer values.""" 7831 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. 7833 >>> s = FiniteDomainSort('S', 100) 7834 >>> v = FiniteDomainVal(3, s) 7843 """Return a Z3 finite-domain numeral as a Python string. 7845 >>> s = FiniteDomainSort('S', 100) 7846 >>> v = FiniteDomainVal(42, s) 7854 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. 7856 >>> s = FiniteDomainSort('S', 256) 7857 >>> FiniteDomainVal(255, s) 7859 >>> FiniteDomainVal('100', s) 7869 """Return `True` if `a` is a Z3 finite-domain value. 7871 >>> s = FiniteDomainSort('S', 100) 7872 >>> b = Const('b', s) 7873 >>> is_finite_domain_value(b) 7875 >>> b = FiniteDomainVal(10, s) 7878 >>> is_finite_domain_value(b) 7892

self.

_opt = opt

7893

self.

_value

_value = value

7894

self.

_is_max

_is_max = is_max

7897

opt = self.

7901

opt = self.

7905

opt = self.

7909

opt = self.

7914 return

self.

upper

upper()

7916 return

self.

lower

lower()

7919 return "%s:%s"

% (self.

_value

_value, self.

_is_max

_is_max)

7925 def

_global_on_model(ctx):

7926

(fn, mdl) = _on_models[ctx]

7930

_on_model_eh = on_model_eh_type(_global_on_model)

7934 """Optimize API provides methods for solving using objective functions and weighted soft constraints""" 7938 if

optimize

is None

7949 if

self.

optimize

is not None and

self.

ctx.ref()

is not None and

Z3_optimize_dec_ref

is not None

7954 def set

(self, *args, **keys):

7955 """Set a configuration option. 7956 The method `help()` return a string containing all available options. 7962 """Display a string describing all available options.""" 7966 """Return the parameter description set.""" 7970 """Assert constraints as background axioms for the optimize solver.""" 7971

args = _get_args(args)

7974 if

isinstance(arg, Goal)

or

isinstance(arg, AstVector):

7982 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr.""" 7990 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`. 7992 If `p` is a string, it will be automatically converted into a Boolean constant. 7997 >>> s.assert_and_track(x > 0, 'p1') 7998 >>> s.assert_and_track(x != 1, 'p2') 7999 >>> s.assert_and_track(x < 0, p3) 8000 >>> print(s.check()) 8002 >>> c = s.unsat_core() 8012 if

isinstance(p, str):

8014

_z3_assert(isinstance(a, BoolRef),

"Boolean expression expected"

)

8015

_z3_assert(isinstance(p, BoolRef)

and is_const

(p),

"Boolean expression expected"

)

8019 """Add soft constraint with optional weight and optional identifier. 8020 If no weight is supplied, then the penalty for violating the soft constraint 8022 Soft constraints are grouped by identifiers. Soft constraints that are 8023 added without identifiers are grouped by default. 8026

weight =

"%d"

% weight

8027 elif

isinstance(weight, float):

8028

weight =

"%f"

% weight

8029 if not

isinstance(weight, str):

8030 raise

Z3Exception(

"weight should be a string or an integer"

)

8038 if

sys.version_info.major >= 3

and

isinstance(arg, Iterable):

8039 return

[asoft(a)

for

in

arg]

8043 """initialize the solver's state by setting the initial value of var to value 8046

value = s.cast(value)

8050 """Add objective function to maximize.""" 8058 """Add objective function to minimize.""" 8066 """create a backtracking point for added rules, facts and assertions""" 8070 """restore to previously created backtracking point""" 8074 """Check consistency and produce optimal values.""" 8075

assumptions = _get_args(assumptions)

8076

num = len(assumptions)

8077

_assumptions = (Ast * num)()

8078 for

in range

(num):

8079

_assumptions[i] = assumptions[i].as_ast()

8083 """Return a string that describes why the last `check()` returned `unknown`.""" 8087 """Return a model for the last check().""" 8091 raise

Z3Exception(

"model is not available"

)

8097 if not

isinstance(obj, OptimizeObjective):

8098 raise

Z3Exception(

"Expecting objective handle returned by maximize/minimize"

)

8102 if not

isinstance(obj, OptimizeObjective):

8103 raise

Z3Exception(

"Expecting objective handle returned by maximize/minimize"

)

8107 if not

isinstance(obj, OptimizeObjective):

8108 raise

Z3Exception(

"Expecting objective handle returned by maximize/minimize"

)

8109 return

obj.lower_values()

8112 if not

isinstance(obj, OptimizeObjective):

8113 raise

Z3Exception(

"Expecting objective handle returned by maximize/minimize"

)

8114 return

obj.upper_values()

8117 """Parse assertions and objectives from a file""" 8121 """Parse assertions and objectives from a string""" 8125 """Return an AST vector containing all added constraints.""" 8129 """returns set of objective functions""" 8133 """Return a formatted string with all added rules and constraints.""" 8134 return

self.

sexpr

sexpr()

8137 """Return a formatted string (in Lisp-like format) with all added constraints. 8138 We say the string is in s-expression format. 8143 """Return statistics for the last check`. 8148 """Register a callback that is invoked with every incremental improvement to 8149 objective values. The callback takes a model as argument. 8150 The life-time of the model is limited to the callback so the 8151 model has to be (deep) copied if it is to be used after the callback 8153

id = len(_on_models) + 41

8155

_on_models[id] = (on_model, mdl)

8158

self.

ctx.ref(), self.

optimize

optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,

8168 """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. 8169 It also contains model and proof converters. 8181 if

self.

ctx.ref()

is not None and

Z3_apply_result_dec_ref

is not None

8185 """Return the number of subgoals in `self`. 8187 >>> a, b = Ints('a b') 8189 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 8190 >>> t = Tactic('split-clause') 8194 >>> t = Then(Tactic('split-clause'), Tactic('split-clause')) 8197 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values')) 8204 """Return one of the subgoals stored in ApplyResult object `self`. 8206 >>> a, b = Ints('a b') 8208 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 8209 >>> t = Tactic('split-clause') 8212 [a == 0, Or(b == 0, b == 1), a > b] 8214 [a == 1, Or(b == 0, b == 1), a > b] 8216 if

idx >= len(self):

8221 return

obj_to_string(self)

8224 """Return a textual representation of the s-expression representing the set of subgoals in `self`.""" 8228 """Return a Z3 expression consisting of all subgoals. 8233 >>> g.add(Or(x == 2, x == 3)) 8234 >>> r = Tactic('simplify')(g) 8236 [[Not(x <= 1), Or(x == 2, x == 3)]] 8238 And(Not(x <= 1), Or(x == 2, x == 3)) 8239 >>> r = Tactic('split-clause')(g) 8241 [[x > 1, x == 2], [x > 1, x == 3]] 8243 Or(And(x > 1, x == 2), And(x > 1, x == 3)) 8260 """Simplifiers act as pre-processing utilities for solvers. 8261 Build a custom simplifier and add it to a solver""" 8266 if

isinstance(simplifier, SimplifierObj):

8268 elif

isinstance(simplifier, list):

8269

simps = [

Simplifier

(s, ctx)

for

in

simplifier]

8270

self.

simplifier

simplifier = simps[0].simplifier

8271 for

in range

(1, len(simps)):

8277

_z3_assert(isinstance(simplifier, str),

"simplifier name expected"

)

8281 raise

Z3Exception(

"unknown simplifier '%s'"

% simplifier)

8288 if

self.

simplifier

is not None and

self.

ctx.ref()

is not None and

Z3_simplifier_dec_ref

is not None

8292 """Return a simplifier that uses the given configuration options""" 8297 """Return a solver that applies the simplification pre-processing specified by the simplifier""" 8301 """Display a string containing a description of the available options for the `self` simplifier.""" 8305 """Return the parameter description set.""" 8317 """Tactics transform, solver and/or simplify sets of constraints (Goal). 8318 A Tactic can be converted into a Solver using the method solver(). 8320 Several combinators are available for creating new tactics using the built-in ones: 8321 Then(), OrElse(), FailIf(), Repeat(), When(), Cond(). 8327 if

isinstance(tactic, TacticObj):

8328

self.

tactic

tactic = tactic

8331

_z3_assert(isinstance(tactic, str),

"tactic name expected"

)

8335 raise

Z3Exception(

"unknown tactic '%s'"

% tactic)

8342 if

self.

tactic

is not None and

self.

ctx.ref()

is not None and

Z3_tactic_dec_ref

is not None

8346 """Create a solver using the tactic `self`. 8348 The solver supports the methods `push()` and `pop()`, but it 8349 will always solve each `check()` from scratch. 8351 >>> t = Then('simplify', 'nlsat') 8354 >>> s.add(x**2 == 2, x > 0) 8362 def apply

(self, goal, *arguments, **keywords):

8363 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 8365 >>> x, y = Ints('x y') 8366 >>> t = Tactic('solve-eqs') 8367 >>> t.apply(And(x == 0, y >= x + 1)) 8371

_z3_assert(isinstance(goal, (Goal, BoolRef)),

"Z3 Goal or Boolean expressions expected"

)

8372

goal = _to_goal(goal)

8373 if

len(arguments) > 0

or

len(keywords) > 0:

8380 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. 8382 >>> x, y = Ints('x y') 8383 >>> t = Tactic('solve-eqs') 8384 >>> t(And(x == 0, y >= x + 1)) 8387 return

self.

apply

apply(goal, *arguments, **keywords)

8390 """Display a string containing a description of the available options for the `self` tactic.""" 8394 """Return the parameter description set.""" 8399 if

isinstance(a, BoolRef):

8400

goal =

Goal

(ctx=a.ctx)

8407 def

_to_tactic(t, ctx=None):

8408 if

isinstance(t, Tactic):

8414 def

_and_then(t1, t2, ctx=None):

8415

t1 = _to_tactic(t1, ctx)

8416

t2 = _to_tactic(t2, ctx)

8418

_z3_assert(t1.ctx == t2.ctx,

"Context mismatch"

)

8422 def

_or_else(t1, t2, ctx=None):

8423

t1 = _to_tactic(t1, ctx)

8424

t2 = _to_tactic(t2, ctx)

8426

_z3_assert(t1.ctx == t2.ctx,

"Context mismatch"

)

8431 """Return a tactic that applies the tactics in `*ts` in sequence. 8433 >>> x, y = Ints('x y') 8434 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) 8435 >>> t(And(x == 0, y > x + 1)) 8437 >>> t(And(x == 0, y > x + 1)).as_expr() 8441

_z3_assert(len(ts) >= 2,

"At least two arguments expected"

)

8442

ctx = ks.get(

"ctx"

None

)

8445 for

in range

(num - 1):

8446

r = _and_then(r, ts[i + 1], ctx)

8451 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). 8453 >>> x, y = Ints('x y') 8454 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) 8455 >>> t(And(x == 0, y > x + 1)) 8457 >>> t(And(x == 0, y > x + 1)).as_expr() 8464 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). 8467 >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) 8468 >>> # Tactic split-clause fails if there is no clause in the given goal. 8471 >>> t(Or(x == 0, x == 1)) 8472 [[x == 0], [x == 1]] 8475

_z3_assert(len(ts) >= 2,

"At least two arguments expected"

)

8476

ctx = ks.get(

"ctx"

None

)

8479 for

in range

(num - 1):

8480

r = _or_else(r, ts[i + 1], ctx)

8485 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). 8488 >>> t = ParOr(Tactic('simplify'), Tactic('fail')) 8493

_z3_assert(len(ts) >= 2,

"At least two arguments expected"

)

8494

ctx = _get_ctx(ks.get(

"ctx"

None

))

8495

ts = [_to_tactic(t, ctx)

for

in

ts]

8497

_args = (TacticObj * sz)()

8498 for

in range

(sz):

8499

_args[i] = ts[i].tactic

8504 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. 8505 The subgoals are processed in parallel. 8507 >>> x, y = Ints('x y') 8508 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) 8509 >>> t(And(Or(x == 1, x == 2), y == x + 1)) 8510 [[x == 1, y == 2], [x == 2, y == 3]] 8512

t1 = _to_tactic(t1, ctx)

8513

t2 = _to_tactic(t2, ctx)

8515

_z3_assert(t1.ctx == t2.ctx,

"Context mismatch"

)

8520 """Alias for ParThen(t1, t2, ctx).""" 8525 """Return a tactic that applies tactic `t` using the given configuration options. 8527 >>> x, y = Ints('x y') 8528 >>> t = With(Tactic('simplify'), som=True) 8529 >>> t((x + 1)*(y + 2) == 0) 8530 [[2*x + y + x*y == -2]] 8532

ctx = keys.pop(

"ctx"

None

)

8533

t = _to_tactic(t, ctx)

8539 """Return a tactic that applies tactic `t` using the given configuration options. 8541 >>> x, y = Ints('x y') 8543 >>> p.set("som", True) 8544 >>> t = WithParams(Tactic('simplify'), p) 8545 >>> t((x + 1)*(y + 2) == 0) 8546 [[2*x + y + x*y == -2]] 8548

t = _to_tactic(t,

None

)

8553 """Return a tactic that keeps applying `t` until the goal is not modified anymore 8554 or the maximum number of iterations `max` is reached. 8556 >>> x, y = Ints('x y') 8557 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) 8558 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) 8560 >>> for subgoal in r: print(subgoal) 8561 [x == 0, y == 0, x > y] 8562 [x == 0, y == 1, x > y] 8563 [x == 1, y == 0, x > y] 8564 [x == 1, y == 1, x > y] 8565 >>> t = Then(t, Tactic('propagate-values')) 8569

t = _to_tactic(t, ctx)

8574 """Return a tactic that applies `t` to a given goal for `ms` milliseconds. 8576 If `t` does not terminate in `ms` milliseconds, then it fails. 8578

t = _to_tactic(t, ctx)

8583 """Return a list of all available tactics in Z3. 8586 >>> l.count('simplify') == 1 8594 """Return a short description for the tactic named `name`. 8596 >>> d = tactic_description('simplify') 8603 """Display a (tabular) description of all available tactics in Z3.""" 8606

print(

'<table border="1" cellpadding="2" cellspacing="0">'

)

8609

print(

'<tr style="background-color:#CFCFCF">'

)

8614

print(

"<td>%s</td><td>%s</td></tr>"

% (t, insert_line_breaks(

tactic_description

(t), 40)))

8622 """Probes are used to inspect a goal (aka problem) and collect information that may be used 8623 to decide which solver and/or preprocessing step will be used. 8629 if

isinstance(probe, ProbeObj):

8630

self.

probe

probe = probe

8631 elif

isinstance(probe, float):

8633 elif

_is_int(probe):

8635 elif

isinstance(probe, bool):

8642

_z3_assert(isinstance(probe, str),

"probe name expected"

)

8646 raise

Z3Exception(

"unknown probe '%s'"

% probe)

8653 if

self.

probe

is not None and

self.

ctx.ref()

is not None and

Z3_probe_dec_ref

is not None

8657 """Return a probe that evaluates to "true" when the value returned by `self` 8658 is less than the value returned by `other`. 8660 >>> p = Probe('size') < 10 8671 """Return a probe that evaluates to "true" when the value returned by `self` 8672 is greater than the value returned by `other`. 8674 >>> p = Probe('size') > 10 8685 """Return a probe that evaluates to "true" when the value returned by `self` 8686 is less than or equal to the value returned by `other`. 8688 >>> p = Probe('size') <= 2 8699 """Return a probe that evaluates to "true" when the value returned by `self` 8700 is greater than or equal to the value returned by `other`. 8702 >>> p = Probe('size') >= 2 8713 """Return a probe that evaluates to "true" when the value returned by `self` 8714 is equal to the value returned by `other`. 8716 >>> p = Probe('size') == 2 8727 """Return a probe that evaluates to "true" when the value returned by `self` 8728 is not equal to the value returned by `other`. 8730 >>> p = Probe('size') != 2 8738

p = self.

__eq__

__eq__(other)

8742 """Evaluate the probe `self` in the given goal. 8744 >>> p = Probe('size') 8754 >>> p = Probe('num-consts') 8757 >>> p = Probe('is-propositional') 8760 >>> p = Probe('is-qflia') 8765

_z3_assert(isinstance(goal, (Goal, BoolRef)),

"Z3 Goal or Boolean expression expected"

)

8766

goal = _to_goal(goal)

8771 """Return `True` if `p` is a Z3 probe. 8773 >>> is_probe(Int('x')) 8775 >>> is_probe(Probe('memory')) 8778 return

isinstance(p, Probe)

8781 def

_to_probe(p, ctx=None):

8785 return Probe

(p, ctx)

8789 """Return a list of all available probes in Z3. 8792 >>> l.count('memory') == 1 8800 """Return a short description for the probe named `name`. 8802 >>> d = probe_description('memory') 8809 """Display a (tabular) description of all available probes in Z3.""" 8812

print(

'<table border="1" cellpadding="2" cellspacing="0">'

)

8815

print(

'<tr style="background-color:#CFCFCF">'

)

8820

print(

"<td>%s</td><td>%s</td></tr>"

% (p, insert_line_breaks(

probe_description

(p), 40)))

8827 def

_probe_nary(f, args, ctx):

8829

_z3_assert(len(args) > 0,

"At least one argument expected"

)

8831

r = _to_probe(args[0], ctx)

8832 for

in range

(num - 1):

8833

r =

Probe

(f(ctx.ref(), r.probe, _to_probe(args[i + 1], ctx).probe), ctx)

8837 def

_probe_and(args, ctx):

8838 return

_probe_nary(Z3_probe_and, args, ctx)

8841 def

_probe_or(args, ctx):

8842 return

_probe_nary(Z3_probe_or, args, ctx)

8846 """Return a tactic that fails if the probe `p` evaluates to true. 8847 Otherwise, it returns the input goal unmodified. 8849 In the following example, the tactic applies 'simplify' if and only if there are 8850 more than 2 constraints in the goal. 8852 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) 8853 >>> x, y = Ints('x y') 8859 >>> g.add(x == y + 1) 8861 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 8863

p = _to_probe(p, ctx)

8868 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. 8869 Otherwise, it returns the input goal unmodified. 8871 >>> t = When(Probe('size') > 2, Tactic('simplify')) 8872 >>> x, y = Ints('x y') 8878 >>> g.add(x == y + 1) 8880 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 8882

p = _to_probe(p, ctx)

8883

t = _to_tactic(t, ctx)

8888 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. 8890 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt')) 8892

p = _to_probe(p, ctx)

8893

t1 = _to_tactic(t1, ctx)

8894

t2 = _to_tactic(t2, ctx)

8905 """Simplify the expression `a` using the given options. 8907 This function has many options. Use `help_simplify` to obtain the complete list. 8911 >>> simplify(x + 1 + y + x + 1) 8913 >>> simplify((x + 1)*(y + 1), som=True) 8915 >>> simplify(Distinct(x, y, 1), blast_distinct=True) 8916 And(Not(x == y), Not(x == 1), Not(y == 1)) 8917 >>> simplify(And(x == 0, y == 1), elim_and=True) 8918 Not(Or(Not(x == 0), Not(y == 1))) 8921

_z3_assert(

(a),

"Z3 expression expected"

)

8922 if

len(arguments) > 0

or

len(keywords) > 0:

8924 return

_to_expr_ref(

Z3_simplify_ex

(a.ctx_ref(), a.as_ast(), p.params), a.ctx)

8926 return

_to_expr_ref(

Z3_simplify

(a.ctx_ref(), a.as_ast()), a.ctx)

8930 """Return a string describing all options available for Z3 `simplify` procedure.""" 8935 """Return the set of parameter descriptions for Z3 `simplify` procedure.""" 8940 """Apply substitution m on t, m is a list of pairs of the form (from, to). 8941 Every occurrence in t of from is replaced with to. 8945 >>> substitute(x + 1, (x, y + 1)) 8947 >>> f = Function('f', IntSort(), IntSort()) 8948 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 8951 if

isinstance(m, tuple):

8953 if

isinstance(m1, list)

and

all(isinstance(p, tuple)

for

in

m1):

8956

_z3_assert(

(t),

"Z3 expression expected"

)

8958

all([isinstance(p, tuple)

and is_expr

(p[0])

and is_expr

(p[1])

for

in

m]),

8959 "Z3 invalid substitution, expression pairs expected."

)

8961

all([p[0].sort().

(p[1].sort())

for

in

m]),

8962 'Z3 invalid substitution, mismatching "from" and "to" sorts.'

)

8964

_from = (Ast * num)()

8966 for

in range

(num):

8967

_from[i] = m[i][0].as_ast()

8968

_to[i] = m[i][1].as_ast()

8969 return

_to_expr_ref(

Z3_substitute

(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)

8973 """Substitute the free variables in t with the expression in m. 8975 >>> v0 = Var(0, IntSort()) 8976 >>> v1 = Var(1, IntSort()) 8978 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 8979 >>> # replace v0 with x+1 and v1 with x 8980 >>> substitute_vars(f(v0, v1), x + 1, x) 8984

_z3_assert(

(t),

"Z3 expression expected"

)

8985

_z3_assert(all([

(n)

for

in

m]),

"Z3 invalid substitution, list of expressions expected."

)

8988 for

in range

(num):

8989

_to[i] = m[i].as_ast()

8993 """Apply substitution m on t, m is a list of pairs of a function and expression (from, to) 8994 Every occurrence in to of the function from is replaced with the expression to. 8995 The expression to can have free variables, that refer to the arguments of from. 8998 if

isinstance(m, tuple):

9000 if

isinstance(m1, list)

and

all(isinstance(p, tuple)

for

in

m1):

9003

_z3_assert(

(t),

"Z3 expression expected"

)

9004

_z3_assert(all([isinstance(p, tuple)

and is_func_decl

(p[0])

and is_expr

(p[1])

for

in

m]),

"Z3 invalid substitution, function pairs expected."

)

9006

_from = (FuncDecl * num)()

9008 for

in range

(num):

9009

_from[i] = m[i][0].as_func_decl()

9010

_to[i] = m[i][1].as_ast()

9011 return

_to_expr_ref(

Z3_substitute_funs

(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)

9015 """Create the sum of the Z3 expressions. 9017 >>> a, b, c = Ints('a b c') 9022 >>> A = IntVector('a', 5) 9024 a__0 + a__1 + a__2 + a__3 + a__4 9026

args = _get_args(args)

9029

ctx = _ctx_from_ast_arg_list(args)

9031 return

_reduce(

lambda

a, b: a + b, args, 0)

9032

args = _coerce_expr_list(args, ctx)

9034 return

_reduce(

lambda

a, b: a + b, args, 0)

9036

_args, sz = _to_ast_array(args)

9041 """Create the product of the Z3 expressions. 9043 >>> a, b, c = Ints('a b c') 9044 >>> Product(a, b, c) 9046 >>> Product([a, b, c]) 9048 >>> A = IntVector('a', 5) 9050 a__0*a__1*a__2*a__3*a__4 9052

args = _get_args(args)

9055

ctx = _ctx_from_ast_arg_list(args)

9057 return

_reduce(

lambda

a, b: a * b, args, 1)

9058

args = _coerce_expr_list(args, ctx)

9060 return

_reduce(

lambda

a, b: a * b, args, 1)

9062

_args, sz = _to_ast_array(args)

9066 """Create the absolute value of an arithmetic expression""" 9067 return If

(arg > 0, arg, -arg)

9071 """Create an at-most Pseudo-Boolean k constraint. 9073 >>> a, b, c = Bools('a b c') 9074 >>> f = AtMost(a, b, c, 2) 9076

args = _get_args(args)

9078

_z3_assert(len(args) > 1,

"Non empty list of arguments expected"

)

9079

ctx = _ctx_from_ast_arg_list(args)

9081

_z3_assert(ctx

is not None

"At least one of the arguments must be a Z3 expression"

)

9082

args1 = _coerce_expr_list(args[:-1], ctx)

9084

_args, sz = _to_ast_array(args1)

9089 """Create an at-least Pseudo-Boolean k constraint. 9091 >>> a, b, c = Bools('a b c') 9092 >>> f = AtLeast(a, b, c, 2) 9094

args = _get_args(args)

9096

_z3_assert(len(args) > 1,

"Non empty list of arguments expected"

)

9097

ctx = _ctx_from_ast_arg_list(args)

9099

_z3_assert(ctx

is not None

"At least one of the arguments must be a Z3 expression"

)

9100

args1 = _coerce_expr_list(args[:-1], ctx)

9102

_args, sz = _to_ast_array(args1)

9106 def

_reorder_pb_arg(arg):

9108 if not

_is_int(b)

and

_is_int(a):

9113 def

_pb_args_coeffs(args, default_ctx=None):

9114

args = _get_args_ast_list(args)

9116 return

_get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()

9117

args = [_reorder_pb_arg(arg)

for

arg

in

args]

9118

args, coeffs = zip(*args)

9120

_z3_assert(len(args) > 0,

"Non empty list of arguments expected"

)

9121

ctx = _ctx_from_ast_arg_list(args)

9123

_z3_assert(ctx

is not None

"At least one of the arguments must be a Z3 expression"

)

9124

args = _coerce_expr_list(args, ctx)

9125

_args, sz = _to_ast_array(args)

9126

_coeffs = (ctypes.c_int * len(coeffs))()

9127 for

in range

(len(coeffs)):

9128

_z3_check_cint_overflow(coeffs[i],

"coefficient"

)

9129

_coeffs[i] = coeffs[i]

9130 return

ctx, sz, _args, _coeffs, args

9134 """Create a Pseudo-Boolean inequality k constraint. 9136 >>> a, b, c = Bools('a b c') 9137 >>> f = PbLe(((a,1),(b,3),(c,2)), 3) 9139

_z3_check_cint_overflow(k,

"k"

)

9140

ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)

9145 """Create a Pseudo-Boolean inequality k constraint. 9147 >>> a, b, c = Bools('a b c') 9148 >>> f = PbGe(((a,1),(b,3),(c,2)), 3) 9150

_z3_check_cint_overflow(k,

"k"

)

9151

ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)

9156 """Create a Pseudo-Boolean equality k constraint. 9158 >>> a, b, c = Bools('a b c') 9159 >>> f = PbEq(((a,1),(b,3),(c,2)), 3) 9161

_z3_check_cint_overflow(k,

"k"

)

9162

ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)

9167 """Solve the constraints `*args`. 9169 This is a simple function for creating demonstrations. It creates a solver, 9170 configure it using the options in `keywords`, adds the constraints 9171 in `args`, and invokes check. 9174 >>> solve(a > 0, a < 2) 9177

show = keywords.pop(

"show"

False

)

9185

print(

"no solution"

)

9187

print(

"failed to solve"

)

9197 """Solve the constraints `*args` using solver `s`. 9199 This is a simple function for creating demonstrations. It is similar to `solve`, 9200 but it uses the given solver `s`. 9201 It configures solver `s` using the options in `keywords`, adds the constraints 9202 in `args`, and invokes check. 9204

show = keywords.pop(

"show"

False

)

9206

_z3_assert(isinstance(s, Solver),

"Solver object expected"

)

9214

print(

"no solution"

)

9216

print(

"failed to solve"

)

9223

print(

"Solution:"

)

9227 def prove

(claim, show=False, **keywords):

9228 """Try to prove the given claim. 9230 This is a simple function for creating demonstrations. It tries to prove 9231 `claim` by showing the negation is unsatisfiable. 9233 >>> p, q = Bools('p q') 9234 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) 9238

_z3_assert(

is_bool

(claim),

"Z3 Boolean expression expected"

)

9248

print(

"failed to prove"

)

9251

print(

"counterexample"

)

9255 def

_solve_html(*args, **keywords):

9256 """Version of function `solve` that renders HTML output.""" 9257

show = keywords.pop(

"show"

False

)

9262

print(

"Problem:"

)

9266

print(

"no solution"

)

9268

print(

"failed to solve"

)

9275

print(

"Solution:"

)

9279 def

_solve_using_html(s, *args, **keywords):

9280 """Version of function `solve_using` that renders HTML.""" 9281

show = keywords.pop(

"show"

False

)

9283

_z3_assert(isinstance(s, Solver),

"Solver object expected"

)

9287

print(

"Problem:"

)

9291

print(

"no solution"

)

9293

print(

"failed to solve"

)

9300

print(

"Solution:"

)

9304 def

_prove_html(claim, show=False, **keywords):

9305 """Version of function `prove` that renders HTML.""" 9307

_z3_assert(

is_bool

(claim),

"Z3 Boolean expression expected"

)

9315

print(

"proved"

)

9317

print(

"failed to prove"

)

9320

print(

"counterexample"

)

9324 def

_dict2sarray(sorts, ctx):

9326

_names = (Symbol * sz)()

9327

_sorts = (Sort * sz)()

9332

_z3_assert(isinstance(k, str),

"String expected"

)

9333

_z3_assert(

(v),

"Z3 sort expected"

)

9337 return

sz, _names, _sorts

9340 def

_dict2darray(decls, ctx):

9342

_names = (Symbol * sz)()

9343

_decls = (FuncDecl * sz)()

9348

_z3_assert(isinstance(k, str),

"String expected"

)

9352

_decls[i] = v.decl().ast

9356 return

sz, _names, _decls

9365 if

self.

ctx.ref()

is not None and

self.

pctx

is not None and

Z3_parser_context_dec_ref

is not None

9367

self.

pctx

pctx =

None 9379 """Parse a string in SMT 2.0 format using the given sorts and decls. 9381 The arguments sorts and decls are Python dictionaries used to initialize 9382 the symbol table used for the SMT 2.0 parser. 9384 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') 9386 >>> x, y = Ints('x y') 9387 >>> f = Function('f', IntSort(), IntSort()) 9388 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) 9390 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) 9394

ssz, snames, ssorts = _dict2sarray(sorts, ctx)

9395

dsz, dnames, ddecls = _dict2darray(decls, ctx)

9400 """Parse a file in SMT 2.0 format using the given sorts and decls. 9402 This function is similar to parse_smt2_string(). 9405

ssz, snames, ssorts = _dict2sarray(sorts, ctx)

9406

dsz, dnames, ddecls = _dict2darray(decls, ctx)

9418

_dflt_rounding_mode = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN

9419

_dflt_fpsort_ebits = 11

9420

_dflt_fpsort_sbits = 53

9424 """Retrieves the global default rounding mode.""" 9425 global

_dflt_rounding_mode

9426 if

_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:

9428 elif

_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:

9430 elif

_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:

9432 elif

_dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:

9434 elif

_dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:

9438

_ROUNDING_MODES = frozenset({

9439

Z3_OP_FPA_RM_TOWARD_ZERO,

9440

Z3_OP_FPA_RM_TOWARD_NEGATIVE,

9441

Z3_OP_FPA_RM_TOWARD_POSITIVE,

9442

Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,

9443

Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY

9448 global

_dflt_rounding_mode

9450

_dflt_rounding_mode = rm.decl().kind()

9452

_z3_assert(_dflt_rounding_mode

in

_ROUNDING_MODES,

"illegal rounding mode"

)

9453

_dflt_rounding_mode = rm

9457 return FPSort

(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)

9461 global

_dflt_fpsort_ebits

9462 global

_dflt_fpsort_sbits

9463

_dflt_fpsort_ebits = ebits

9464

_dflt_fpsort_sbits = sbits

9467 def

_dflt_rm(ctx=None):

9471 def

_dflt_fps(ctx=None):

9475 def

_coerce_fp_expr_list(alist, ctx):

9476

first_fp_sort =

None 9479 if

first_fp_sort

is None

9480

first_fp_sort = a.sort()

9481 elif

first_fp_sort == a.sort():

9486

first_fp_sort =

None 9490 for

in range

(len(alist)):

9492

is_repr = isinstance(a, str)

and

a.contains(

"2**("

)

and

a.endswith(

")"

)

9493 if

is_repr

or

_is_int(a)

or

isinstance(a, (float, bool)):

9494

r.append(

FPVal

(a,

None

, first_fp_sort, ctx))

9497 return

_coerce_expr_list(r, ctx)

9503 """Floating-point sort.""" 9506 """Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`. 9507 >>> b = FPSort(8, 24) 9514 """Retrieves the number of bits reserved for the significand in the FloatingPoint sort `self`. 9515 >>> b = FPSort(8, 24) 9522 """Try to cast `val` as a floating-point expression. 9523 >>> b = FPSort(8, 24) 9526 >>> b.cast(1.0).sexpr() 9527 '(fp #b0 #x7f #b00000000000000000000000)' 9531

_z3_assert(self.

ctx ctx

ctx == val.ctx,

"Context mismatch"

)

9538 """Floating-point 16-bit (half) sort.""" 9544 """Floating-point 16-bit (half) sort.""" 9550 """Floating-point 32-bit (single) sort.""" 9556 """Floating-point 32-bit (single) sort.""" 9562 """Floating-point 64-bit (double) sort.""" 9568 """Floating-point 64-bit (double) sort.""" 9574 """Floating-point 128-bit (quadruple) sort.""" 9580 """Floating-point 128-bit (quadruple) sort.""" 9586 """"Floating-point rounding mode sort.""" 9590 """Return True if `s` is a Z3 floating-point sort. 9592 >>> is_fp_sort(FPSort(8, 24)) 9594 >>> is_fp_sort(IntSort()) 9597 return

isinstance(s, FPSortRef)

9601 """Return True if `s` is a Z3 floating-point rounding mode sort. 9603 >>> is_fprm_sort(FPSort(8, 24)) 9605 >>> is_fprm_sort(RNE().sort()) 9608 return

isinstance(s, FPRMSortRef)

9614 """Floating-point expressions.""" 9617 """Return the sort of the floating-point expression `self`. 9619 >>> x = FP('1.0', FPSort(8, 24)) 9622 >>> x.sort() == FPSort(8, 24) 9628 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`. 9629 >>> b = FPSort(8, 24) 9636 """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`. 9637 >>> b = FPSort(8, 24) 9644 """Return a Z3 floating point expression as a Python string.""" 9648 return fpLEQ

(self, other, self.

ctx)

9651 return fpLT

(self, other, self.

ctx)

9654 return fpGEQ

(self, other, self.

ctx)

9657 return fpGT

(self, other, self.

ctx)

9660 """Create the Z3 expression `self + other`. 9662 >>> x = FP('x', FPSort(8, 24)) 9663 >>> y = FP('y', FPSort(8, 24)) 9669

[a, b] = _coerce_fp_expr_list([self, other], self.

ctx)

9670 return fpAdd

(_dflt_rm(), a, b, self.

ctx)

9673 """Create the Z3 expression `other + self`. 9675 >>> x = FP('x', FPSort(8, 24)) 9679

[a, b] = _coerce_fp_expr_list([other, self], self.

ctx)

9680 return fpAdd

(_dflt_rm(), a, b, self.

ctx)

9683 """Create the Z3 expression `self - other`. 9685 >>> x = FP('x', FPSort(8, 24)) 9686 >>> y = FP('y', FPSort(8, 24)) 9692

[a, b] = _coerce_fp_expr_list([self, other], self.

ctx)

9693 return fpSub

(_dflt_rm(), a, b, self.

ctx)

9696 """Create the Z3 expression `other - self`. 9698 >>> x = FP('x', FPSort(8, 24)) 9702

[a, b] = _coerce_fp_expr_list([other, self], self.

ctx)

9703 return fpSub

(_dflt_rm(), a, b, self.

ctx)

9706 """Create the Z3 expression `self * other`. 9708 >>> x = FP('x', FPSort(8, 24)) 9709 >>> y = FP('y', FPSort(8, 24)) 9717

[a, b] = _coerce_fp_expr_list([self, other], self.

ctx)

9718 return fpMul

(_dflt_rm(), a, b, self.

ctx)

9721 """Create the Z3 expression `other * self`. 9723 >>> x = FP('x', FPSort(8, 24)) 9724 >>> y = FP('y', FPSort(8, 24)) 9730

[a, b] = _coerce_fp_expr_list([other, self], self.

ctx)

9731 return fpMul

(_dflt_rm(), a, b, self.

ctx)

9734 """Create the Z3 expression `+self`.""" 9738 """Create the Z3 expression `-self`. 9740 >>> x = FP('x', Float32()) 9747 """Create the Z3 expression `self / other`. 9749 >>> x = FP('x', FPSort(8, 24)) 9750 >>> y = FP('y', FPSort(8, 24)) 9758

[a, b] = _coerce_fp_expr_list([self, other], self.

ctx)

9759 return fpDiv

(_dflt_rm(), a, b, self.

ctx)

9762 """Create the Z3 expression `other / self`. 9764 >>> x = FP('x', FPSort(8, 24)) 9765 >>> y = FP('y', FPSort(8, 24)) 9771

[a, b] = _coerce_fp_expr_list([other, self], self.

ctx)

9772 return fpDiv

(_dflt_rm(), a, b, self.

ctx)

9775 """Create the Z3 expression division `self / other`.""" 9776 return

self.

__div__

__div__(other)

9779 """Create the Z3 expression division `other / self`.""" 9780 return

self.

__rdiv__

__rdiv__(other)

9783 """Create the Z3 expression mod `self % other`.""" 9784 return fpRem

(self, other)

9787 """Create the Z3 expression mod `other % self`.""" 9788 return fpRem

(other, self)

9792 """Floating-point rounding mode expressions""" 9795 """Return a Z3 floating point expression as a Python string.""" 9850 """Return `True` if `a` is a Z3 floating-point rounding mode expression. 9859 return

isinstance(a, FPRMRef)

9863 """Return `True` if `a` is a Z3 floating-point rounding mode numeral value.""" 9864 return is_fprm

(a)

and

_is_numeral(a.ctx, a.ast)

9870 """The sign of the numeral. 9872 >>> x = FPVal(+1.0, FPSort(8, 24)) 9875 >>> x = FPVal(-1.0, FPSort(8, 24)) 9881

num = (ctypes.c_int)()

9884 raise

Z3Exception(

"error retrieving the sign of a numeral."

)

9885 return

num.value != 0

9887 """The sign of a floating-point numeral as a bit-vector expression. 9889 Remark: NaN's are invalid arguments. 9895 """The significand of the numeral. 9897 >>> x = FPVal(2.5, FPSort(8, 24)) 9905 """The significand of the numeral as a long. 9907 >>> x = FPVal(2.5, FPSort(8, 24)) 9908 >>> x.significand_as_long() 9913

ptr = (ctypes.c_ulonglong * 1)()

9915 raise

Z3Exception(

"error retrieving the significand of a numeral."

)

9918 """The significand of the numeral as a bit-vector expression. 9920 Remark: NaN are invalid arguments. 9926 """The exponent of the numeral. 9928 >>> x = FPVal(2.5, FPSort(8, 24)) 9936 """The exponent of the numeral as a long. 9938 >>> x = FPVal(2.5, FPSort(8, 24)) 9939 >>> x.exponent_as_long() 9944

ptr = (ctypes.c_longlong * 1)()

9946 raise

Z3Exception(

"error retrieving the exponent of a numeral."

)

9949 """The exponent of the numeral as a bit-vector expression. 9951 Remark: NaNs are invalid arguments. 9957 """Indicates whether the numeral is a NaN.""" 9962 """Indicates whether the numeral is +oo or -oo.""" 9967 """Indicates whether the numeral is +zero or -zero.""" 9972 """Indicates whether the numeral is normal.""" 9977 """Indicates whether the numeral is subnormal.""" 9982 """Indicates whether the numeral is positive.""" 9987 """Indicates whether the numeral is negative.""" 9993 The string representation of the numeral. 9995 >>> x = FPVal(20, FPSort(8, 24)) 10002 return

(

"FPVal(%s, %s)"

% (s, self.

sort sort

sort()))

10006 """Return `True` if `a` is a Z3 floating-point expression. 10008 >>> b = FP('b', FPSort(8, 24)) 10013 >>> is_fp(Int('x')) 10016 return

isinstance(a, FPRef)

10020 """Return `True` if `a` is a Z3 floating-point numeral value. 10022 >>> b = FP('b', FPSort(8, 24)) 10025 >>> b = FPVal(1.0, FPSort(8, 24)) 10031 return is_fp

(a)

and

_is_numeral(a.ctx, a.ast)

10035 """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used. 10037 >>> Single = FPSort(8, 24) 10038 >>> Double = FPSort(11, 53) 10041 >>> x = Const('x', Single) 10042 >>> eq(x, FP('x', FPSort(8, 24))) 10045

ctx = _get_ctx(ctx)

10049 def

_to_float_str(val, exp=0):

10050 if

isinstance(val, float):

10051 if

math.isnan(val):

10054

sone = math.copysign(1.0, val)

10059 elif

val == float(

"+inf"

10061 elif

val == float(

"-inf"

10064

v = val.as_integer_ratio()

10067

rvs = str(num) +

"/"

+ str(den)

10068

res = rvs +

"p"

+ _to_int_str(exp)

10069 elif

isinstance(val, bool):

10076 elif

isinstance(val, str):

10077

inx = val.find(

"*(2**"

)

10080 elif

val[-1] ==

")"

10082

exp = str(int(val[inx + 5:-1]) + int(exp))

10084

_z3_assert(

False

"String does not have floating-point numeral form."

)

10086

_z3_assert(

False

"Python value cannot be used to create floating-point numerals."

)

10090 return

res +

"p"

+ exp

10094 """Create a Z3 floating-point NaN term. 10096 >>> s = FPSort(8, 24) 10097 >>> set_fpa_pretty(True) 10100 >>> pb = get_fpa_pretty() 10101 >>> set_fpa_pretty(False) 10103 fpNaN(FPSort(8, 24)) 10104 >>> set_fpa_pretty(pb) 10106

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10111 """Create a Z3 floating-point +oo term. 10113 >>> s = FPSort(8, 24) 10114 >>> pb = get_fpa_pretty() 10115 >>> set_fpa_pretty(True) 10116 >>> fpPlusInfinity(s) 10118 >>> set_fpa_pretty(False) 10119 >>> fpPlusInfinity(s) 10120 fpPlusInfinity(FPSort(8, 24)) 10121 >>> set_fpa_pretty(pb) 10123

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10128 """Create a Z3 floating-point -oo term.""" 10129

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10134 """Create a Z3 floating-point +oo or -oo term.""" 10135

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10136

_z3_assert(isinstance(negative, bool),

"expected Boolean flag"

)

10141 """Create a Z3 floating-point +0.0 term.""" 10142

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10147 """Create a Z3 floating-point -0.0 term.""" 10148

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10153 """Create a Z3 floating-point +0.0 or -0.0 term.""" 10154

_z3_assert(isinstance(s, FPSortRef),

"sort mismatch"

)

10155

_z3_assert(isinstance(negative, bool),

"expected Boolean flag"

)

10159 def FPVal

(sig, exp=None, fps=None, ctx=None):

10160 """Return a floating-point value of value `val` and sort `fps`. 10161 If `ctx=None`, then the global context is used. 10163 >>> v = FPVal(20.0, FPSort(8, 24)) 10166 >>> print("0x%.8x" % v.exponent_as_long(False)) 10168 >>> v = FPVal(2.25, FPSort(8, 24)) 10171 >>> v = FPVal(-2.25, FPSort(8, 24)) 10174 >>> FPVal(-0.0, FPSort(8, 24)) 10176 >>> FPVal(0.0, FPSort(8, 24)) 10178 >>> FPVal(+0.0, FPSort(8, 24)) 10181

ctx = _get_ctx(ctx)

10186

fps = _dflt_fps(ctx)

10187

_z3_assert(

(fps),

"sort mismatch"

)

10190

val = _to_float_str(sig)

10191 if

val ==

"NaN" or

val ==

"nan"

10193 elif

val ==

"-0.0"

10195 elif

val ==

"0.0" or

val ==

"+0.0"

10197 elif

val ==

"+oo" or

val ==

"+inf" or

val ==

"+Inf"

10199 elif

val ==

"-oo" or

val ==

"-inf" or

val ==

"-Inf"

10205 def FP

(name, fpsort, ctx=None):

10206 """Return a floating-point constant named `name`. 10207 `fpsort` is the floating-point sort. 10208 If `ctx=None`, then the global context is used. 10210 >>> x = FP('x', FPSort(8, 24)) 10217 >>> word = FPSort(8, 24) 10218 >>> x2 = FP('x', word) 10222 if

isinstance(fpsort, FPSortRef)

and

ctx

is None

10225

ctx = _get_ctx(ctx)

10229 def FPs

(names, fpsort, ctx=None):

10230 """Return an array of floating-point constants. 10232 >>> x, y, z = FPs('x y z', FPSort(8, 24)) 10239 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) 10242

ctx = _get_ctx(ctx)

10243 if

isinstance(names, str):

10244

names = names.split(

" "

)

10245 return

[

(name, fpsort, ctx)

for

name

in

names]

10249 """Create a Z3 floating-point absolute value expression. 10251 >>> s = FPSort(8, 24) 10253 >>> x = FPVal(1.0, s) 10256 >>> y = FPVal(-20.0, s) 10260 fpAbs(-1.25*(2**4)) 10261 >>> fpAbs(-1.25*(2**4)) 10262 fpAbs(-1.25*(2**4)) 10263 >>> fpAbs(x).sort() 10266

ctx = _get_ctx(ctx)

10267

[a] = _coerce_fp_expr_list([a], ctx)

10272 """Create a Z3 floating-point addition expression. 10274 >>> s = FPSort(8, 24) 10279 >>> fpNeg(x).sort() 10282

ctx = _get_ctx(ctx)

10283

[a] = _coerce_fp_expr_list([a], ctx)

10287 def

_mk_fp_unary(f, rm, a, ctx):

10288

ctx = _get_ctx(ctx)

10289

[a] = _coerce_fp_expr_list([a], ctx)

10291

_z3_assert(

(rm),

"First argument must be a Z3 floating-point rounding mode expression"

)

10292

_z3_assert(

(a),

"Second argument must be a Z3 floating-point expression"

)

10293 return FPRef

(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx)

10296 def

_mk_fp_unary_pred(f, a, ctx):

10297

ctx = _get_ctx(ctx)

10298

[a] = _coerce_fp_expr_list([a], ctx)

10300

_z3_assert(

(a),

"First argument must be a Z3 floating-point expression"

)

10301 return BoolRef

(f(ctx.ref(), a.as_ast()), ctx)

10304 def

_mk_fp_bin(f, rm, a, b, ctx):

10305

ctx = _get_ctx(ctx)

10306

[a, b] = _coerce_fp_expr_list([a, b], ctx)

10308

_z3_assert(

(rm),

"First argument must be a Z3 floating-point rounding mode expression"

)

10309

_z3_assert(

(a)

or is_fp

(b),

"Second or third argument must be a Z3 floating-point expression"

)

10310 return FPRef

(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx)

10313 def

_mk_fp_bin_norm(f, a, b, ctx):

10314

ctx = _get_ctx(ctx)

10315

[a, b] = _coerce_fp_expr_list([a, b], ctx)

10317

_z3_assert(

(a)

or is_fp

(b),

"First or second argument must be a Z3 floating-point expression"

)

10318 return FPRef

(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

10321 def

_mk_fp_bin_pred(f, a, b, ctx):

10322

ctx = _get_ctx(ctx)

10323

[a, b] = _coerce_fp_expr_list([a, b], ctx)

10325

_z3_assert(

(a)

or is_fp

(b),

"First or second argument must be a Z3 floating-point expression"

)

10326 return BoolRef

(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)

10329 def

_mk_fp_tern(f, rm, a, b, c, ctx):

10330

ctx = _get_ctx(ctx)

10331

[a, b, c] = _coerce_fp_expr_list([a, b, c], ctx)

10333

_z3_assert(

(rm),

"First argument must be a Z3 floating-point rounding mode expression"

)

10335

c),

"Second, third or fourth argument must be a Z3 floating-point expression"

)

10336 return FPRef

(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)

10340 """Create a Z3 floating-point addition expression. 10342 >>> s = FPSort(8, 24) 10346 >>> fpAdd(rm, x, y) 10348 >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ 10350 >>> fpAdd(rm, x, y).sort() 10353 return

_mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)

10357 """Create a Z3 floating-point subtraction expression. 10359 >>> s = FPSort(8, 24) 10363 >>> fpSub(rm, x, y) 10365 >>> fpSub(rm, x, y).sort() 10368 return

_mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)

10372 """Create a Z3 floating-point multiplication expression. 10374 >>> s = FPSort(8, 24) 10378 >>> fpMul(rm, x, y) 10380 >>> fpMul(rm, x, y).sort() 10383 return

_mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)

10387 """Create a Z3 floating-point division expression. 10389 >>> s = FPSort(8, 24) 10393 >>> fpDiv(rm, x, y) 10395 >>> fpDiv(rm, x, y).sort() 10398 return

_mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)

10402 """Create a Z3 floating-point remainder expression. 10404 >>> s = FPSort(8, 24) 10409 >>> fpRem(x, y).sort() 10412 return

_mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)

10416 """Create a Z3 floating-point minimum expression. 10418 >>> s = FPSort(8, 24) 10424 >>> fpMin(x, y).sort() 10427 return

_mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)

10431 """Create a Z3 floating-point maximum expression. 10433 >>> s = FPSort(8, 24) 10439 >>> fpMax(x, y).sort() 10442 return

_mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)

10446 """Create a Z3 floating-point fused multiply-add expression. 10448 return

_mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)

10452 """Create a Z3 floating-point square root expression. 10454 return

_mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)

10458 """Create a Z3 floating-point roundToIntegral expression. 10460 return

_mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)

10464 """Create a Z3 floating-point isNaN expression. 10466 >>> s = FPSort(8, 24) 10472 return

_mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)

10476 """Create a Z3 floating-point isInfinite expression. 10478 >>> s = FPSort(8, 24) 10483 return

_mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)

10487 """Create a Z3 floating-point isZero expression. 10489 return

_mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)

10493 """Create a Z3 floating-point isNormal expression. 10495 return

_mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)

10499 """Create a Z3 floating-point isSubnormal expression. 10501 return

_mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)

10505 """Create a Z3 floating-point isNegative expression. 10507 return

_mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)

10511 """Create a Z3 floating-point isPositive expression. 10513 return

_mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)

10516 def

_check_fp_args(a, b):

10518

_z3_assert(

(a)

or is_fp

(b),

"First or second argument must be a Z3 floating-point expression"

)

10522 """Create the Z3 floating-point expression `other < self`. 10524 >>> x, y = FPs('x y', FPSort(8, 24)) 10527 >>> (x < y).sexpr() 10530 return

_mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)

10534 """Create the Z3 floating-point expression `other <= self`. 10536 >>> x, y = FPs('x y', FPSort(8, 24)) 10539 >>> (x <= y).sexpr() 10542 return

_mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)

10546 """Create the Z3 floating-point expression `other > self`. 10548 >>> x, y = FPs('x y', FPSort(8, 24)) 10551 >>> (x > y).sexpr() 10554 return

_mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)

10558 """Create the Z3 floating-point expression `other >= self`. 10560 >>> x, y = FPs('x y', FPSort(8, 24)) 10563 >>> (x >= y).sexpr() 10566 return

_mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)

10570 """Create the Z3 floating-point expression `fpEQ(other, self)`. 10572 >>> x, y = FPs('x y', FPSort(8, 24)) 10575 >>> fpEQ(x, y).sexpr() 10578 return

_mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)

10582 """Create the Z3 floating-point expression `Not(fpEQ(other, self))`. 10584 >>> x, y = FPs('x y', FPSort(8, 24)) 10587 >>> (x != y).sexpr() 10590 return Not

(

fpEQ

(a, b, ctx))

10594 """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp. 10596 >>> s = FPSort(8, 24) 10597 >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23)) 10599 fpFP(1, 127, 4194304) 10600 >>> xv = FPVal(-1.5, s) 10603 >>> slvr = Solver() 10604 >>> slvr.add(fpEQ(x, xv)) 10607 >>> xv = FPVal(+1.5, s) 10610 >>> slvr = Solver() 10611 >>> slvr.add(fpEQ(x, xv)) 10615

_z3_assert(

(sgn)

and is_bv

(exp)

and is_bv

(sig),

"sort mismatch"

)

10616

_z3_assert(sgn.sort().size() == 1,

"sort mismatch"

)

10617

ctx = _get_ctx(ctx)

10618

_z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx,

"context mismatch"

)

10623 """Create a Z3 floating-point conversion expression from other term sorts 10626 From a bit-vector term in IEEE 754-2008 format: 10627 >>> x = FPVal(1.0, Float32()) 10628 >>> x_bv = fpToIEEEBV(x) 10629 >>> simplify(fpToFP(x_bv, Float32())) 10632 From a floating-point term with different precision: 10633 >>> x = FPVal(1.0, Float32()) 10634 >>> x_db = fpToFP(RNE(), x, Float64()) 10639 >>> x_r = RealVal(1.5) 10640 >>> simplify(fpToFP(RNE(), x_r, Float32())) 10643 From a signed bit-vector term: 10644 >>> x_signed = BitVecVal(-5, BitVecSort(32)) 10645 >>> simplify(fpToFP(RNE(), x_signed, Float32())) 10648

ctx = _get_ctx(ctx)

10658 raise

Z3Exception(

"Unsupported combination of arguments for conversion to floating-point term."

)

10662 """Create a Z3 floating-point conversion expression that represents the 10663 conversion from a bit-vector term to a floating-point term. 10665 >>> x_bv = BitVecVal(0x3F800000, 32) 10666 >>> x_fp = fpBVToFP(x_bv, Float32()) 10672

_z3_assert(

(v),

"First argument must be a Z3 bit-vector expression"

)

10673

_z3_assert(

(sort),

"Second argument must be a Z3 floating-point sort."

)

10674

ctx = _get_ctx(ctx)

10679 """Create a Z3 floating-point conversion expression that represents the 10680 conversion from a floating-point term to a floating-point term of different precision. 10682 >>> x_sgl = FPVal(1.0, Float32()) 10683 >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64()) 10686 >>> simplify(x_dbl) 10691

_z3_assert(

(rm),

"First argument must be a Z3 floating-point rounding mode expression."

)

10692

_z3_assert(

(v),

"Second argument must be a Z3 floating-point expression."

)

10693

_z3_assert(

(sort),

"Third argument must be a Z3 floating-point sort."

)

10694

ctx = _get_ctx(ctx)

10699 """Create a Z3 floating-point conversion expression that represents the 10700 conversion from a real term to a floating-point term. 10702 >>> x_r = RealVal(1.5) 10703 >>> x_fp = fpRealToFP(RNE(), x_r, Float32()) 10709

_z3_assert(

(rm),

"First argument must be a Z3 floating-point rounding mode expression."

)

10710

_z3_assert(

is_real

(v),

"Second argument must be a Z3 expression or real sort."

)

10711

_z3_assert(

(sort),

"Third argument must be a Z3 floating-point sort."

)

10712

ctx = _get_ctx(ctx)

10717 """Create a Z3 floating-point conversion expression that represents the 10718 conversion from a signed bit-vector term (encoding an integer) to a floating-point term. 10720 >>> x_signed = BitVecVal(-5, BitVecSort(32)) 10721 >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32()) 10723 fpToFP(RNE(), 4294967291) 10727

_z3_assert(

(rm),

"First argument must be a Z3 floating-point rounding mode expression."

)

10728

_z3_assert(

(v),

"Second argument must be a Z3 bit-vector expression"

)

10729

_z3_assert(

(sort),

"Third argument must be a Z3 floating-point sort."

)

10730

ctx = _get_ctx(ctx)

10735 """Create a Z3 floating-point conversion expression that represents the 10736 conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term. 10738 >>> x_signed = BitVecVal(-5, BitVecSort(32)) 10739 >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32()) 10741 fpToFPUnsigned(RNE(), 4294967291) 10745

_z3_assert(

(rm),

"First argument must be a Z3 floating-point rounding mode expression."

)

10746

_z3_assert(

(v),

"Second argument must be a Z3 bit-vector expression"

)

10747

_z3_assert(

(sort),

"Third argument must be a Z3 floating-point sort."

)

10748

ctx = _get_ctx(ctx)

10753 """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.""" 10755

_z3_assert(

(rm),

"First argument must be a Z3 floating-point rounding mode expression"

)

10756

_z3_assert(

(x),

"Second argument must be a Z3 bit-vector expression"

)

10757

_z3_assert(

(s),

"Third argument must be Z3 floating-point sort"

)

10758

ctx = _get_ctx(ctx)

10763 """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector. 10765 >>> x = FP('x', FPSort(8, 24)) 10766 >>> y = fpToSBV(RTZ(), x, BitVecSort(32)) 10767 >>> print(is_fp(x)) 10769 >>> print(is_bv(y)) 10771 >>> print(is_fp(y)) 10773 >>> print(is_bv(x)) 10777

_z3_assert(

(rm),

"First argument must be a Z3 floating-point rounding mode expression"

)

10778

_z3_assert(

(x),

"Second argument must be a Z3 floating-point expression"

)

10779

_z3_assert(

is_bv_sort

(s),

"Third argument must be Z3 bit-vector sort"

)

10780

ctx = _get_ctx(ctx)

10785 """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector. 10787 >>> x = FP('x', FPSort(8, 24)) 10788 >>> y = fpToUBV(RTZ(), x, BitVecSort(32)) 10789 >>> print(is_fp(x)) 10791 >>> print(is_bv(y)) 10793 >>> print(is_fp(y)) 10795 >>> print(is_bv(x)) 10799

_z3_assert(

(rm),

"First argument must be a Z3 floating-point rounding mode expression"

)

10800

_z3_assert(

(x),

"Second argument must be a Z3 floating-point expression"

)

10801

_z3_assert(

is_bv_sort

(s),

"Third argument must be Z3 bit-vector sort"

)

10802

ctx = _get_ctx(ctx)

10807 """Create a Z3 floating-point conversion expression, from floating-point expression to real. 10809 >>> x = FP('x', FPSort(8, 24)) 10810 >>> y = fpToReal(x) 10811 >>> print(is_fp(x)) 10813 >>> print(is_real(y)) 10815 >>> print(is_fp(y)) 10817 >>> print(is_real(x)) 10821

_z3_assert(

(x),

"First argument must be a Z3 floating-point expression"

)

10822

ctx = _get_ctx(ctx)

10827 """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. 10829 The size of the resulting bit-vector is automatically determined. 10831 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion 10832 knows only one NaN and it will always produce the same bit-vector representation of 10835 >>> x = FP('x', FPSort(8, 24)) 10836 >>> y = fpToIEEEBV(x) 10837 >>> print(is_fp(x)) 10839 >>> print(is_bv(y)) 10841 >>> print(is_fp(y)) 10843 >>> print(is_bv(x)) 10847

_z3_assert(

(x),

"First argument must be a Z3 floating-point expression"

)

10848

ctx = _get_ctx(ctx)

10859 """Sequence sort.""" 10862 """Determine if sort is a string 10863 >>> s = StringSort() 10866 >>> s = SeqSort(IntSort()) 10876 """Character sort.""" 10880 """Create a string sort 10881 >>> s = StringSort() 10885

ctx = _get_ctx(ctx)

10889 """Create a character sort 10890 >>> ch = CharSort() 10894

ctx = _get_ctx(ctx)

10899 """Create a sequence sort over elements provided in the argument 10900 >>> s = SeqSort(IntSort()) 10901 >>> s == Unit(IntVal(1)).sort() 10908 """Sequence expression.""" 10914 return Concat

(self, other)

10917 return Concat

(other, self)

10936 """Return a string representation of sequence expression.""" 10938

string_length = ctypes.c_uint()

10940 return

string_at(chars, size=string_length.value).decode(

"latin-1"

)

10956 def

_coerce_char(ch, ctx=None):

10957 if

isinstance(ch, str):

10958

ctx = _get_ctx(ctx)

10961 raise

Z3Exception(

"Character expression expected"

)

10965 """Character expression.""" 10968

other = _coerce_char(other, self.

ctx)

10982

ctx = _get_ctx(ctx)

10983 if

isinstance(ch, str):

10985 if not

isinstance(ch, int):

10986 raise

Z3Exception(

"character value should be an ordinal"

)

10987 return

_to_expr_ref(

Z3_mk_char

(ctx.ref(), ch), ctx)

10991 raise

Z3Exception(

"Bit-vector expression needed"

)

10995

ch = _coerce_char(ch, ctx)

10999

ch = _coerce_char(ch, ctx)

11003

ch = _coerce_char(ch, ctx)

11004 return

ch.is_digit()

11006 def

_coerce_seq(s, ctx=None):

11007 if

isinstance(s, str):

11008

ctx = _get_ctx(ctx)

11011 raise

Z3Exception(

"Non-expression passed as a sequence"

)

11013 raise

Z3Exception(

"Non-sequence passed as a sequence"

)

11017 def

_get_ctx2(a, b, ctx=None):

11028 """Return `True` if `a` is a Z3 sequence expression. 11029 >>> print (is_seq(Unit(IntVal(0)))) 11031 >>> print (is_seq(StringVal("abc"))) 11034 return

isinstance(a, SeqRef)

11038 """Return `True` if `a` is a Z3 string expression. 11039 >>> print (is_string(StringVal("ab"))) 11042 return

isinstance(a, SeqRef)

and

a.is_string()

11046 """return 'True' if 'a' is a Z3 string constant expression. 11047 >>> print (is_string_value(StringVal("a"))) 11049 >>> print (is_string_value(StringVal("a") + StringVal("b"))) 11052 return

isinstance(a, SeqRef)

and

a.is_string_value()

11055 """create a string expression""" 11056

s =

""

.join(str(ch)

if

32 <= ord(ch)

and

ord(ch) < 127

else "\\u{%x}"

% (ord(ch))

for

in

11057

ctx = _get_ctx(ctx)

11062 """Return a string constant named `name`. If `ctx=None`, then the global context is used. 11064 >>> x = String('x') 11066

ctx = _get_ctx(ctx)

11071 """Return a tuple of String constants. """ 11072

ctx = _get_ctx(ctx)

11073 if

isinstance(names, str):

11074

names = names.split(

" "

)

11075 return

[

String

(name, ctx)

for

name

in

names]

11079 """Extract substring or subsequence starting at offset""" 11080 return Extract

(s, offset, length)

11084 """Extract substring or subsequence starting at offset""" 11085 return Extract

(s, offset, length)

11089 """Create the empty sequence of the given sort 11090 >>> e = Empty(StringSort()) 11091 >>> e2 = StringVal("") 11092 >>> print(e.eq(e2)) 11094 >>> e3 = Empty(SeqSort(IntSort())) 11097 >>> e4 = Empty(ReSort(SeqSort(IntSort()))) 11099 Empty(ReSort(Seq(Int))) 11101 if

isinstance(s, SeqSortRef):

11103 if

isinstance(s, ReSortRef):

11105 raise

Z3Exception(

"Non-sequence, non-regular expression sort passed to Empty"

)

11109 """Create the regular expression that accepts the universal language 11110 >>> e = Full(ReSort(SeqSort(IntSort()))) 11112 Full(ReSort(Seq(Int))) 11113 >>> e1 = Full(ReSort(StringSort())) 11115 Full(ReSort(String)) 11117 if

isinstance(s, ReSortRef):

11119 raise

Z3Exception(

"Non-sequence, non-regular expression sort passed to Full"

)

11124 """Create a singleton sequence""" 11129 """Check if 'a' is a prefix of 'b' 11130 >>> s1 = PrefixOf("ab", "abc") 11133 >>> s2 = PrefixOf("bc", "abc") 11137

ctx = _get_ctx2(a, b)

11138

a = _coerce_seq(a, ctx)

11139

b = _coerce_seq(b, ctx)

11144 """Check if 'a' is a suffix of 'b' 11145 >>> s1 = SuffixOf("ab", "abc") 11148 >>> s2 = SuffixOf("bc", "abc") 11152

ctx = _get_ctx2(a, b)

11153

a = _coerce_seq(a, ctx)

11154

b = _coerce_seq(b, ctx)

11159 """Check if 'a' contains 'b' 11160 >>> s1 = Contains("abc", "ab") 11163 >>> s2 = Contains("abc", "bc") 11166 >>> x, y, z = Strings('x y z') 11167 >>> s3 = Contains(Concat(x,y,z), y) 11171

ctx = _get_ctx2(a, b)

11172

a = _coerce_seq(a, ctx)

11173

b = _coerce_seq(b, ctx)

11178 """Replace the first occurrence of 'src' by 'dst' in 's' 11179 >>> r = Replace("aaa", "a", "b") 11183

ctx = _get_ctx2(dst, s)

11184 if

ctx

is None and is_expr

(src):

11186

src = _coerce_seq(src, ctx)

11187

dst = _coerce_seq(dst, ctx)

11188

s = _coerce_seq(s, ctx)

11193 """Retrieve the index of substring within a string starting at a specified offset. 11194 >>> simplify(IndexOf("abcabc", "bc", 0)) 11196 >>> simplify(IndexOf("abcabc", "bc", 2)) 11199 if

offset

is None

11204

ctx = _get_ctx2(s, substr, ctx)

11205

s = _coerce_seq(s, ctx)

11206

substr = _coerce_seq(substr, ctx)

11207 if

_is_int(offset):

11208

offset =

IntVal

(offset, ctx)

11213 """Retrieve the last index of substring within a string""" 11215

ctx = _get_ctx2(s, substr, ctx)

11216

s = _coerce_seq(s, ctx)

11217

substr = _coerce_seq(substr, ctx)

11222 """Obtain the length of a sequence 's' 11223 >>> l = Length(StringVal("abc")) 11231 """Map function 'f' over sequence 's'""" 11232

ctx = _get_ctx2(f, s)

11233

s = _coerce_seq(s, ctx)

11234 return

_to_expr_ref(

Z3_mk_seq_map

(s.ctx_ref(), f.as_ast(), s.as_ast()), ctx)

11237 """Map function 'f' over sequence 's' at index 'i'""" 11238

ctx = _get_ctx(f, s)

11239

s = _coerce_seq(s, ctx)

11242 return

_to_expr_ref(

Z3_mk_seq_mapi

(s.ctx_ref(), f.as_ast(), i.as_ast(), s.as_ast()), ctx)

11245

ctx = _get_ctx2(f, s)

11246

s = _coerce_seq(s, ctx)

11248 return

_to_expr_ref(

Z3_mk_seq_foldl

(s.ctx_ref(), f.as_ast(), a.as_ast(), s.as_ast()), ctx)

11251

ctx = _get_ctx2(f, s)

11252

s = _coerce_seq(s, ctx)

11255 return

_to_expr_ref(

Z3_mk_seq_foldli

(s.ctx_ref(), f.as_ast(), i.as_ast(), a.as_ast(), s.as_ast()), ctx)

11258 """Convert string expression to integer 11259 >>> a = StrToInt("1") 11260 >>> simplify(1 == a) 11262 >>> b = StrToInt("2") 11263 >>> simplify(1 == b) 11265 >>> c = StrToInt(IntToStr(2)) 11266 >>> simplify(1 == c) 11274 """Convert integer expression to string""" 11281 """Convert a unit length string to integer code""" 11287 """Convert code to a string""" 11293 """The regular expression that accepts sequence 's' 11295 >>> s2 = Re(StringVal("ab")) 11296 >>> s3 = Re(Unit(BoolVal(True))) 11298

s = _coerce_seq(s, ctx)

11305 """Regular expression sort.""" 11314 if

is None or

isinstance(s, Context):

11317 raise

Z3Exception(

"Regular expression sort constructor expects either a string or a context or no argument"

)

11321 """Regular expressions.""" 11324 return Union

(self, other)

11328 return

isinstance(s, ReRef)

11332 """Create regular expression membership test 11333 >>> re = Union(Re("a"),Re("b")) 11334 >>> print (simplify(InRe("a", re))) 11336 >>> print (simplify(InRe("b", re))) 11338 >>> print (simplify(InRe("c", re))) 11341

s = _coerce_seq(s, re.ctx)

11346 """Create union of regular expressions. 11347 >>> re = Union(Re("a"), Re("b"), Re("c")) 11348 >>> print (simplify(InRe("d", re))) 11351

args = _get_args(args)

11354

_z3_assert(sz > 0,

"At least one argument expected."

)

11355

_z3_assert(all([

is_re

(a)

for

in

args]),

"All arguments must be regular expressions."

)

11360 for

in range

(sz):

11361

v[i] = args[i].as_ast()

11366 """Create intersection of regular expressions. 11367 >>> re = Intersect(Re("a"), Re("b"), Re("c")) 11369

args = _get_args(args)

11372

_z3_assert(sz > 0,

"At least one argument expected."

)

11373

_z3_assert(all([

is_re

(a)

for

in

args]),

"All arguments must be regular expressions."

)

11378 for

in range

(sz):

11379

v[i] = args[i].as_ast()

11384 """Create the regular expression accepting one or more repetitions of argument. 11385 >>> re = Plus(Re("a")) 11386 >>> print(simplify(InRe("aa", re))) 11388 >>> print(simplify(InRe("ab", re))) 11390 >>> print(simplify(InRe("", re))) 11394

_z3_assert(

(re),

"expression expected"

)

11399 """Create the regular expression that optionally accepts the argument. 11400 >>> re = Option(Re("a")) 11401 >>> print(simplify(InRe("a", re))) 11403 >>> print(simplify(InRe("", re))) 11405 >>> print(simplify(InRe("aa", re))) 11409

_z3_assert(

(re),

"expression expected"

)

11414 """Create the complement regular expression.""" 11419 """Create the regular expression accepting zero or more repetitions of argument. 11420 >>> re = Star(Re("a")) 11421 >>> print(simplify(InRe("aa", re))) 11423 >>> print(simplify(InRe("ab", re))) 11425 >>> print(simplify(InRe("", re))) 11429

_z3_assert(

(re),

"expression expected"

)

11434 """Create the regular expression accepting between a lower and upper bound repetitions 11435 >>> re = Loop(Re("a"), 1, 3) 11436 >>> print(simplify(InRe("aa", re))) 11438 >>> print(simplify(InRe("aaaa", re))) 11440 >>> print(simplify(InRe("", re))) 11444

_z3_assert(

(re),

"expression expected"

)

11449 """Create the range regular expression over two sequences of length 1 11450 >>> range = Range("a","z") 11451 >>> print(simplify(InRe("b", range))) 11453 >>> print(simplify(InRe("bb", range))) 11456

lo = _coerce_seq(lo, ctx)

11457

hi = _coerce_seq(hi, ctx)

11459

_z3_assert(

(lo),

"expression expected"

)

11460

_z3_assert(

(hi),

"expression expected"

)

11464 """Create the difference regular expression 11467

_z3_assert(

(a),

"expression expected"

)

11468

_z3_assert(

(b),

"expression expected"

)

11472 """Create a regular expression that accepts all single character strings 11496 """Given a binary relation R, such that the two arguments have the same sort 11497 create the transitive closure relation R+. 11498 The transitive closure R+ is a new relation. 11504

super(ctypes.c_void_p, ast).__init__(ptr)

11508

ctx = ContextObj(ptr)

11509

super(ctypes.c_void_p, ctx).__init__(ptr)

11513

v = AstVectorObj(ptr)

11514

super(ctypes.c_void_p, v).__init__(ptr)

11522

_my_hacky_class =

None 11524

onc = _my_hacky_class

11525

p = _to_expr_ref(

(p), onc.ctx)

11527

deps = [dep[i]

for

in range

(n)]

11528

onc.on_clause(p, deps, clause)

11530

_on_clause_eh = Z3_on_clause_eh(on_clause_eh)

11538 global

_my_hacky_class

11539

_my_hacky_class = self

11549 if

self.

is None

11551

self.

lock = threading.Lock()

11554 if

self.

lock:

11555 with

self.

lock:

11556

r = self.

bases[ctx]

11558

r = self.

bases[ctx]

11562 if

self.

lock:

11563 with

self.

lock:

11564

self.

bases[ctx] = r

11566

self.

bases[ctx] = r

11569 if

self.

lock:

11570 with

self.

lock:

11571

id = len(self.

bases) + 3

11572

self.

bases[id] = r

11574

id = len(self.

bases) + 3

11575

self.

bases[id] = r

11579

_prop_closures =

None 11583 global

_prop_closures

11584 if

_prop_closures

is None

11589

prop = _prop_closures.get(ctx)

11595

prop = _prop_closures.get(ctx)

11597

prop.pop(num_scopes)

11601

_prop_closures.set_threaded()

11602

prop = _prop_closures.get(ctx)

11609

new_prop = prop.fresh(nctx)

11610

_prop_closures.set(new_prop.id, new_prop)

11615

prop = _prop_closures.get(ctx)

11618

id = _to_expr_ref(

(id), prop.ctx())

11619

value = _to_expr_ref(

(value), prop.ctx())

11620

prop.fixed(id, value)

11624

prop = _prop_closures.get(ctx)

11627

id = _to_expr_ref(

(id), prop.ctx())

11633

prop = _prop_closures.get(ctx)

11640

prop = _prop_closures.get(ctx)

11643

x = _to_expr_ref(

(x), prop.ctx())

11644

y = _to_expr_ref(

(y), prop.ctx())

11649

prop = _prop_closures.get(ctx)

11652

x = _to_expr_ref(

(x), prop.ctx())

11653

y = _to_expr_ref(

(y), prop.ctx())

11658

prop = _prop_closures.get(ctx)

11661

t = _to_expr_ref(

(t_ref), prop.ctx())

11662

prop.decide(t, idx, phase)

11666

_user_prop_push = Z3_push_eh(user_prop_push)

11667

_user_prop_pop = Z3_pop_eh(user_prop_pop)

11668

_user_prop_fresh = Z3_fresh_eh(user_prop_fresh)

11669

_user_prop_fixed = Z3_fixed_eh(user_prop_fixed)

11670

_user_prop_created = Z3_created_eh(user_prop_created)

11671

_user_prop_final = Z3_final_eh(user_prop_final)

11672

_user_prop_eq = Z3_eq_eh(user_prop_eq)

11673

_user_prop_diseq = Z3_eq_eh(user_prop_diseq)

11674

_user_prop_decide = Z3_decide_eh(user_prop_decide)

11678 """Create a function that gets tracked by user propagator. 11679 Every term headed by this function symbol is tracked. 11680 If a term is fixed and the fixed callback is registered a 11681 callback is invoked that the term headed by this function is fixed. 11683

sig = _get_args(sig)

11685

_z3_assert(len(sig) > 0,

"At least two arguments expected"

)

11686

arity = len(sig) - 1

11689

_z3_assert(

(rng),

"Z3 sort expected"

)

11690

dom = (Sort * arity)()

11691 for

in range

(arity):

11693

_z3_assert(

(sig[i]),

"Z3 sort expected"

)

11694

dom[i] = sig[i].ast

11710 assert

is None or

ctx

is None 11713

self.

_ctx =

None 11716

self.

id = _prop_closures.insert(self)

11727

ctypes.c_void_p(self.

id),

11733 if

self.

_ctx:

11734

self.

_ctx.ctx =

None 11740 return

self.

solver

solver.ctx

11743 return

self.

ctx().ref()

11746 assert not

self.

fixed

11747 assert not

self.

11750

self.

fixed

fixed = fixed

11753 assert not

self.

created

11754 assert not

self.

11757

self.

created

created = created

11760 assert not

self.

final

11761 assert not

self.

11764

self.

final

final = final

11767 assert not

self.

11768 assert not

self.

11774 assert not

self.

diseq

11775 assert not

self.

11778

self.

diseq

diseq = diseq

11781 assert not

self.

decide

11782 assert not

self.

11788 raise

Z3Exception(

"push needs to be overwritten"

)

11791 raise

Z3Exception(

"pop needs to be overwritten"

)

11794 raise

Z3Exception(

"fresh needs to be overwritten"

)

11797 assert not

self.