﻿ Python: module z3

Z3 is a high performance theorem prover developed at Microsoft Research. Z3 is used in many applications such as: software/hardware verification and testing, constraint solving, analysis of hybrid systems, security, biology (in silico analysis), and geometrical problems.

Several online tutorials for Z3Py are available at:
http://rise4fun.com/Z3Py/tutorial/guide

Small example:

>>> x = Int('x')
>>> y = Int('y')
>>> s = Solver()
>>> s.add(y == x + 1)
>>> s.check()
sat
>>> s.model()
[x = 1, y = 2]

Z3 exceptions:

>>> try:
...   x = Int('x')
...   y = Bool('y')
...   # the expression x + y is type incorrect
...   n = x + y
... except Z3Exception as ex:
...   print "failed:", ex
failed: 'sort mismatch'

Modules

 ctypes io os sys z3 z3core

Classes

AstMap
CheckSatResult
Context
Datatype
FuncEntry
ParamDescrsRef
ParamsRef
Probe
ScopedConstructor
ScopedConstructorList
Statistics
Tactic
Z3PPObject
ApplyResult
AstRef
ExprRef
ArithRef
AlgebraicNumRef
IntNumRef
RatNumRef
ArrayRef
BitVecRef
BitVecNumRef
BoolRef
QuantifierRef
DatatypeRef
PatternRef
FuncDeclRef
SortRef
ArithSortRef
ArraySortRef
BitVecSortRef
BoolSortRef
DatatypeSortRef
AstVector
Fixedpoint
FuncInterp
Goal
ModelRef
Solver

 class AlgebraicNumRef(ArithRef) Algebraic irrational values. Method resolution order: AlgebraicNumRef ArithRef ExprRef AstRef Z3PPObject Methods defined here: approx(self, precision=10)Return a Z3 rational number that approximates the algebraic number `self`.  The result `r` is such that |r - self| <= 1/10^precision    >>> x = simplify(Sqrt(2)) >>> x.approx(20) 6838717160008073720548335/4835703278458516698824704 >>> x.approx(5) 2965821/2097152 as_decimal(self, prec)Return a string representation of the algebraic number `self` in decimal notation using `prec` decimal places   >>> x = simplify(Sqrt(2)) >>> x.as_decimal(10) '1.4142135623?' >>> x.as_decimal(20) '1.41421356237309504880?' Methods inherited from ArithRef: __add__(self, other)Create the Z3 expression `self + other`.   >>> x = Int('x') >>> y = Int('y') >>> x + y x + y >>> (x + y).sort() Int __div__(self, other)Create the Z3 expression `other/self`.   >>> x = Int('x') >>> y = Int('y') >>> x/y x/y >>> (x/y).sort() Int >>> (x/y).sexpr() '(div x y)' >>> x = Real('x') >>> y = Real('y') >>> x/y x/y >>> (x/y).sort() Real >>> (x/y).sexpr() '(/ x y)' __ge__(self, other)Create the Z3 expression `other >= self`.   >>> x, y = Ints('x y') >>> x >= y x >= y >>> y = Real('y') >>> x >= y ToReal(x) >= y __gt__(self, other)Create the Z3 expression `other > self`.   >>> x, y = Ints('x y') >>> x > y x > y >>> y = Real('y') >>> x > y ToReal(x) > y __le__(self, other)Create the Z3 expression `other <= self`.   >>> x, y = Ints('x y') >>> x <= y x <= y >>> y = Real('y') >>> x <= y ToReal(x) <= y __lt__(self, other)Create the Z3 expression `other < self`.   >>> x, y = Ints('x y') >>> x < y x < y >>> y = Real('y') >>> x < y ToReal(x) < y __mod__(self, other)Create the Z3 expression `other%self`.   >>> x = Int('x') >>> y = Int('y') >>> x % y x%y >>> simplify(IntVal(10) % IntVal(3)) 1 __mul__(self, other)Create the Z3 expression `self * other`.   >>> x = Real('x') >>> y = Real('y') >>> x * y x*y >>> (x * y).sort() Real __neg__(self)Return an expression representing `-self`.   >>> x = Int('x') >>> -x -x >>> simplify(-(-x)) x __pos__(self)Return `self`.   >>> x = Int('x') >>> +x x __pow__(self, other)Create the Z3 expression `self**other` (** is the power operator).   >>> x = Real('x') >>> x**3 x**3 >>> (x**3).sort() Real >>> simplify(IntVal(2)**8) 256 __radd__(self, other)Create the Z3 expression `other + self`.   >>> x = Int('x') >>> 10 + x 10 + x __rdiv__(self, other)Create the Z3 expression `other/self`.   >>> x = Int('x') >>> 10/x 10/x >>> (10/x).sexpr() '(div 10 x)' >>> x = Real('x') >>> 10/x 10/x >>> (10/x).sexpr() '(/ 10.0 x)' __rmod__(self, other)Create the Z3 expression `other%self`.   >>> x = Int('x') >>> 10 % x 10%x __rmul__(self, other)Create the Z3 expression `other * self`.   >>> x = Real('x') >>> 10 * x 10*x __rpow__(self, other)Create the Z3 expression `other**self` (** is the power operator).   >>> x = Real('x') >>> 2**x 2**x >>> (2**x).sort() Real >>> simplify(2**IntVal(8)) 256 __rsub__(self, other)Create the Z3 expression `other - self`.   >>> x = Int('x') >>> 10 - x 10 - x __rtruediv__(self, other)Create the Z3 expression `other/self`. __sub__(self, other)Create the Z3 expression `self - other`.   >>> x = Int('x') >>> y = Int('y') >>> x - y x - y >>> (x - y).sort() Int __truediv__(self, other)Create the Z3 expression `other/self`. is_int(self)Return `True` if `self` is an integer expression.   >>> x = Int('x') >>> x.is_int() True >>> (x + 1).is_int() True >>> y = Real('y') >>> (x + y).is_int() False is_real(self)Return `True` if `self` is an real expression.   >>> x = Real('x') >>> x.is_real() True >>> (x + 1).is_real() True sort(self)Return the sort (type) of the arithmetical expression `self`.   >>> Int('x').sort() Int >>> (Real('x') + 1).sort() Real Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 as_ast(self) children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class ApplyResult(Z3PPObject) An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters. Methods defined here: __del__(self) __getitem__(self, idx)Return one of the subgoals stored in ApplyResult object `self`.   >>> a, b = Ints('a b') >>> g = Goal() >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) >>> t = Tactic('split-clause') >>> r = t(g) >>> r[0]         [a == 0, Or(b == 0, b == 1), a > b] >>> r[1] [a == 1, Or(b == 0, b == 1), a > b] __init__(self, result, ctx) __len__(self)Return the number of subgoals in `self`.   >>> a, b = Ints('a b') >>> g = Goal() >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) >>> t = Tactic('split-clause') >>> r = t(g) >>> len(r) 2 >>> t = Then(Tactic('split-clause'), Tactic('split-clause')) >>> len(t(g)) 4 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values')) >>> len(t(g)) 1 __repr__(self) as_expr(self)Return a Z3 expression consisting of all subgoals.   >>> x = Int('x') >>> g = Goal() >>> g.add(x > 1) >>> g.add(Or(x == 2, x == 3)) >>> r = Tactic('simplify')(g) >>> r [[Not(x <= 1), Or(x == 2, x == 3)]] >>> r.as_expr() And(Not(x <= 1), Or(x == 2, x == 3)) >>> r = Tactic('split-clause')(g) >>> r [[x > 1, x == 2], [x > 1, x == 3]] >>> r.as_expr() Or(And(x > 1, x == 2), And(x > 1, x == 3)) convert_model(self, model, idx=0)Convert a model for a subgoal into a model for the original goal.   >>> a, b = Ints('a b') >>> g = Goal() >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs')) >>> r = t(g) >>> r[0]         [Or(b == 0, b == 1), Not(0 <= b)] >>> r[1] [Or(b == 0, b == 1), Not(1 <= b)] >>> # Remark: the subgoal r[0] is unsatisfiable >>> # Creating a solver for solving the second subgoal >>> s = Solver() >>> s.add(r[1]) >>> s.check() sat >>> s.model() [b = 0] >>> # Model s.model() does not assign a value to `a` >>> # It is a model for subgoal `r[1]`, but not for goal `g` >>> # The method convert_model creates a model for `g` from a model for `r[1]`. >>> r.convert_model(s.model(), 1) [b = 0, a = 1] sexpr(self)Return a textual representation of the s-expression representing the set of subgoals in `self`. Methods inherited from Z3PPObject: use_pp(self)

 class ArithRef(ExprRef) Integer and Real expressions. Method resolution order: ArithRef ExprRef AstRef Z3PPObject Methods defined here: __add__(self, other)Create the Z3 expression `self + other`.   >>> x = Int('x') >>> y = Int('y') >>> x + y x + y >>> (x + y).sort() Int __div__(self, other)Create the Z3 expression `other/self`.   >>> x = Int('x') >>> y = Int('y') >>> x/y x/y >>> (x/y).sort() Int >>> (x/y).sexpr() '(div x y)' >>> x = Real('x') >>> y = Real('y') >>> x/y x/y >>> (x/y).sort() Real >>> (x/y).sexpr() '(/ x y)' __ge__(self, other)Create the Z3 expression `other >= self`.   >>> x, y = Ints('x y') >>> x >= y x >= y >>> y = Real('y') >>> x >= y ToReal(x) >= y __gt__(self, other)Create the Z3 expression `other > self`.   >>> x, y = Ints('x y') >>> x > y x > y >>> y = Real('y') >>> x > y ToReal(x) > y __le__(self, other)Create the Z3 expression `other <= self`.   >>> x, y = Ints('x y') >>> x <= y x <= y >>> y = Real('y') >>> x <= y ToReal(x) <= y __lt__(self, other)Create the Z3 expression `other < self`.   >>> x, y = Ints('x y') >>> x < y x < y >>> y = Real('y') >>> x < y ToReal(x) < y __mod__(self, other)Create the Z3 expression `other%self`.   >>> x = Int('x') >>> y = Int('y') >>> x % y x%y >>> simplify(IntVal(10) % IntVal(3)) 1 __mul__(self, other)Create the Z3 expression `self * other`.   >>> x = Real('x') >>> y = Real('y') >>> x * y x*y >>> (x * y).sort() Real __neg__(self)Return an expression representing `-self`.   >>> x = Int('x') >>> -x -x >>> simplify(-(-x)) x __pos__(self)Return `self`.   >>> x = Int('x') >>> +x x __pow__(self, other)Create the Z3 expression `self**other` (** is the power operator).   >>> x = Real('x') >>> x**3 x**3 >>> (x**3).sort() Real >>> simplify(IntVal(2)**8) 256 __radd__(self, other)Create the Z3 expression `other + self`.   >>> x = Int('x') >>> 10 + x 10 + x __rdiv__(self, other)Create the Z3 expression `other/self`.   >>> x = Int('x') >>> 10/x 10/x >>> (10/x).sexpr() '(div 10 x)' >>> x = Real('x') >>> 10/x 10/x >>> (10/x).sexpr() '(/ 10.0 x)' __rmod__(self, other)Create the Z3 expression `other%self`.   >>> x = Int('x') >>> 10 % x 10%x __rmul__(self, other)Create the Z3 expression `other * self`.   >>> x = Real('x') >>> 10 * x 10*x __rpow__(self, other)Create the Z3 expression `other**self` (** is the power operator).   >>> x = Real('x') >>> 2**x 2**x >>> (2**x).sort() Real >>> simplify(2**IntVal(8)) 256 __rsub__(self, other)Create the Z3 expression `other - self`.   >>> x = Int('x') >>> 10 - x 10 - x __rtruediv__(self, other)Create the Z3 expression `other/self`. __sub__(self, other)Create the Z3 expression `self - other`.   >>> x = Int('x') >>> y = Int('y') >>> x - y x - y >>> (x - y).sort() Int __truediv__(self, other)Create the Z3 expression `other/self`. is_int(self)Return `True` if `self` is an integer expression.   >>> x = Int('x') >>> x.is_int() True >>> (x + 1).is_int() True >>> y = Real('y') >>> (x + y).is_int() False is_real(self)Return `True` if `self` is an real expression.   >>> x = Real('x') >>> x.is_real() True >>> (x + 1).is_real() True sort(self)Return the sort (type) of the arithmetical expression `self`.   >>> Int('x').sort() Int >>> (Real('x') + 1).sort() Real Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 as_ast(self) children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class ArithSortRef(SortRef) Real and Integer sorts. Method resolution order: ArithSortRef SortRef AstRef Z3PPObject Methods defined here: cast(self, val)Try to cast `val` as an Integer or Real.   >>> IntSort().cast(10) 10 >>> is_int(IntSort().cast(10)) True >>> is_int(10) False >>> RealSort().cast(10) 10 >>> is_real(RealSort().cast(10)) True is_int(self)Return `True` if `self` is the real sort.   >>> x = Int('x') >>> x.is_int() True >>> (x + 1).is_int() True >>> x = Real('x') >>> x.is_int() False is_real(self)Return `True` if `self` is the integer sort.   >>> x = Real('x') >>> x.is_real() True >>> (x + 1).is_real() True >>> x = Int('x') >>> x.is_real() False subsort(self, other)Return `True` if `self` is a subsort of `other`. Methods inherited from SortRef: __eq__(self, other)Return `True` if `self` and `other` are the same Z3 sort.   >>> p = Bool('p') >>> p.sort() == BoolSort() True >>> p.sort() == IntSort() False __ne__(self, other)Return `True` if `self` and `other` are not the same Z3 sort.   >>> p = Bool('p') >>> p.sort() != BoolSort() False >>> p.sort() != IntSort() True as_ast(self) kind(self)Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.   >>> b = BoolSort() >>> b.kind() == Z3_BOOL_SORT True >>> b.kind() == Z3_INT_SORT False >>> A = ArraySort(IntSort(), IntSort()) >>> A.kind() == Z3_ARRAY_SORT True >>> A.kind() == Z3_INT_SORT False name(self)Return the name (string) of sort `self`.   >>> BoolSort().name() 'Bool' >>> ArraySort(IntSort(), IntSort()).name() 'Array' Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class ArrayRef(ExprRef) Array expressions. Method resolution order: ArrayRef ExprRef AstRef Z3PPObject Methods defined here: __getitem__(self, arg)Return the Z3 expression `self[arg]`.   >>> a = Array('a', IntSort(), BoolSort()) >>> i = Int('i') >>> a[i] a[i] >>> a[i].sexpr() '(select a i)' domain(self)Shorthand for `sort().domain()`.   >>> a = Array('a', IntSort(), BoolSort()) >>> a.domain() Int range(self)Shorthand for `sort().range()`.   >>> a = Array('a', IntSort(), BoolSort()) >>> a.range() Bool sort(self)Return the array sort of the array expression `self`.   >>> a = Array('a', IntSort(), BoolSort()) >>> a.sort() Array(Int, Bool) Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 as_ast(self) children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class ArraySortRef(SortRef) Array sorts. Method resolution order: ArraySortRef SortRef AstRef Z3PPObject Methods defined here: domain(self)Return the domain of the array sort `self`.   >>> A = ArraySort(IntSort(), BoolSort()) >>> A.domain() Int range(self)Return the range of the array sort `self`.   >>> A = ArraySort(IntSort(), BoolSort()) >>> A.range() Bool Methods inherited from SortRef: __eq__(self, other)Return `True` if `self` and `other` are the same Z3 sort.   >>> p = Bool('p') >>> p.sort() == BoolSort() True >>> p.sort() == IntSort() False __ne__(self, other)Return `True` if `self` and `other` are not the same Z3 sort.   >>> p = Bool('p') >>> p.sort() != BoolSort() False >>> p.sort() != IntSort() True as_ast(self) cast(self, val)Try to cast `val` as an element of sort `self`.    This method is used in Z3Py to convert Python objects such as integers, floats, longs and strings into Z3 expressions.   >>> x = Int('x') >>> RealSort().cast(x) ToReal(x) kind(self)Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.   >>> b = BoolSort() >>> b.kind() == Z3_BOOL_SORT True >>> b.kind() == Z3_INT_SORT False >>> A = ArraySort(IntSort(), IntSort()) >>> A.kind() == Z3_ARRAY_SORT True >>> A.kind() == Z3_INT_SORT False name(self)Return the name (string) of sort `self`.   >>> BoolSort().name() 'Bool' >>> ArraySort(IntSort(), IntSort()).name() 'Array' subsort(self, other)Return `True` if `self` is a subsort of `other`.    >>> IntSort().subsort(RealSort()) True Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class AstMap A mapping from ASTs to ASTs. Methods defined here: __contains__(self, key)Return `True` if the map contains key `key`.   >>> M = AstMap() >>> x = Int('x') >>> M[x] = x + 1 >>> x in M True >>> x+1 in M False __del__(self) __getitem__(self, key)Retrieve the value associated with key `key`.   >>> M = AstMap() >>> x = Int('x') >>> M[x] = x + 1 >>> M[x] x + 1 __init__(self, m=None, ctx=None) __len__(self)Return the size of the map.    >>> M = AstMap() >>> len(M) 0 >>> x = Int('x') >>> M[x] = IntVal(1) >>> len(M) 1 __repr__(self) __setitem__(self, k, v)Add/Update key `k` with value `v`.   >>> M = AstMap() >>> x = Int('x') >>> M[x] = x + 1 >>> len(M) 1 >>> M[x] x + 1 >>> M[x] = IntVal(1) >>> M[x] 1 erase(self, k)Remove the entry associated with key `k`.   >>> M = AstMap() >>> x = Int('x') >>> M[x] = x + 1 >>> len(M) 1 >>> M.erase(x) >>> len(M) 0 keys(self)Return an AstVector containing all keys in the map.   >>> M = AstMap() >>> x = Int('x') >>> M[x]   = x + 1 >>> M[x+x] = IntVal(1) >>> M.keys() [x, x + x] reset(self)Remove all entries from the map.   >>> M = AstMap() >>> x = Int('x') >>> M[x]   = x + 1 >>> M[x+x] = IntVal(1) >>> len(M) 2 >>> M.reset() >>> len(M) 0

 class AstRef(Z3PPObject) AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions. Methods defined here: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) as_ast(self)Return a pointer to the corresponding C Z3_ast object. ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class AstVector(Z3PPObject) A collection (vector) of ASTs. Methods defined here: __contains__(self, item)Return `True` if the vector contains `item`.   >>> x = Int('x') >>> A = AstVector() >>> x in A False >>> A.push(x) >>> x in A True >>> (x+1) in A False >>> A.push(x+1) >>> (x+1) in A True >>> A [x, x + 1] __del__(self) __getitem__(self, i)Return the AST at position `i`.   >>> A = AstVector() >>> A.push(Int('x') + 1) >>> A.push(Int('y')) >>> A[0] x + 1 >>> A[1] y __init__(self, v=None, ctx=None) __len__(self)Return the size of the vector `self`.   >>> A = AstVector() >>> len(A) 0 >>> A.push(Int('x')) >>> A.push(Int('x')) >>> len(A) 2 __repr__(self) __setitem__(self, i, v)Update AST at position `i`.   >>> A = AstVector() >>> A.push(Int('x') + 1) >>> A.push(Int('y')) >>> A[0] x + 1 >>> A[0] = Int('x') >>> A[0] x push(self, v)Add `v` in the end of the vector.   >>> A = AstVector() >>> len(A) 0 >>> A.push(Int('x')) >>> len(A) 1 resize(self, sz)Resize the vector to `sz` elements.   >>> A = AstVector() >>> A.resize(10) >>> len(A) 10 >>> for i in range(10): A[i] = Int('x') >>> A[5] x sexpr(self)Return a textual representation of the s-expression representing the vector. translate(self, other_ctx)Copy vector `self` to context `other_ctx`.   >>> x = Int('x') >>> A = AstVector() >>> A.push(x) >>> c2 = Context() >>> B = A.translate(c2) >>> B [x] Methods inherited from Z3PPObject: use_pp(self)

 class BitVecNumRef(BitVecRef) Bit-vector values. Method resolution order: BitVecNumRef BitVecRef ExprRef AstRef Z3PPObject Methods defined here: as_long(self)Return a Z3 bit-vector numeral as a Python long (bignum) numeral.    >>> v = BitVecVal(0xbadc0de, 32) >>> v 195936478 >>> print "0x%.8x" % v.as_long() 0x0badc0de as_signed_long(self)Return a Z3 bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign.   >>> BitVecVal(4, 3).as_signed_long() -4L >>> BitVecVal(7, 3).as_signed_long() -1L >>> BitVecVal(3, 3).as_signed_long() 3L >>> BitVecVal(2L**32 - 1, 32).as_signed_long() -1L >>> BitVecVal(2L**64 - 1, 64).as_signed_long() -1L as_string(self) Methods inherited from BitVecRef: __add__(self, other)Create the Z3 expression `self + other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x + y x + y >>> (x + y).sort() BitVec(32) __and__(self, other)Create the Z3 expression bitwise-and `self & other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x & y x & y >>> (x & y).sort() BitVec(32) __div__(self, other)Create the Z3 expression (signed) division `self / other`.   Use the function UDiv() for unsigned division.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x / y x/y >>> (x / y).sort() BitVec(32) >>> (x / y).sexpr() '(bvsdiv x y)' >>> UDiv(x, y).sexpr() '(bvudiv x y)' __ge__(self, other)Create the Z3 expression (signed) `other >= self`.   Use the function UGE() for unsigned greater than or equal to.   >>> x, y = BitVecs('x y', 32) >>> x >= y x >= y >>> (x >= y).sexpr() '(bvsge x y)' >>> UGE(x, y).sexpr() '(bvuge x y)' __gt__(self, other)Create the Z3 expression (signed) `other > self`.   Use the function UGT() for unsigned greater than.   >>> x, y = BitVecs('x y', 32) >>> x > y x > y >>> (x > y).sexpr() '(bvsgt x y)' >>> UGT(x, y).sexpr() '(bvugt x y)' __invert__(self)Create the Z3 expression bitwise-not `~self`.   >>> x = BitVec('x', 32) >>> ~x ~x >>> simplify(~(~x)) x __le__(self, other)Create the Z3 expression (signed) `other <= self`.   Use the function ULE() for unsigned less than or equal to.   >>> x, y = BitVecs('x y', 32) >>> x <= y x <= y >>> (x <= y).sexpr() '(bvsle x y)' >>> ULE(x, y).sexpr() '(bvule x y)' __lshift__(self, other)Create the Z3 expression left shift `self << other`   >>> x, y = BitVecs('x y', 32) >>> x << y x << y >>> (x << y).sexpr() '(bvshl x y)' >>> simplify(BitVecVal(2, 3) << 1) 4 __lt__(self, other)Create the Z3 expression (signed) `other < self`.   Use the function ULT() for unsigned less than.   >>> x, y = BitVecs('x y', 32) >>> x < y x < y >>> (x < y).sexpr() '(bvslt x y)' >>> ULT(x, y).sexpr() '(bvult x y)' __mod__(self, other)Create the Z3 expression (signed) mod `self % other`.   Use the function URem() for unsigned remainder, and SRem() for signed remainder.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x % y x%y >>> (x % y).sort() BitVec(32) >>> (x % y).sexpr() '(bvsmod x y)' >>> URem(x, y).sexpr() '(bvurem x y)' >>> SRem(x, y).sexpr() '(bvsrem x y)' __mul__(self, other)Create the Z3 expression `self * other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x * y x*y >>> (x * y).sort() BitVec(32) __neg__(self)Return an expression representing `-self`.   >>> x = BitVec('x', 32) >>> -x -x >>> simplify(-(-x)) x __or__(self, other)Create the Z3 expression bitwise-or `self | other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x | y x | y >>> (x | y).sort() BitVec(32) __pos__(self)Return `self`.   >>> x = BitVec('x', 32) >>> +x x __radd__(self, other)Create the Z3 expression `other + self`.   >>> x = BitVec('x', 32) >>> 10 + x 10 + x __rand__(self, other)Create the Z3 expression bitwise-or `other & self`.   >>> x = BitVec('x', 32) >>> 10 & x 10 & x __rdiv__(self, other)Create the Z3 expression (signed) division `other / self`.   Use the function UDiv() for unsigned division.   >>> x = BitVec('x', 32) >>> 10 / x 10/x >>> (10 / x).sexpr() '(bvsdiv #x0000000a x)' >>> UDiv(10, x).sexpr() '(bvudiv #x0000000a x)' __rlshift__(self, other)Create the Z3 expression left shift `other << self`.   Use the function LShR() for the right logical shift   >>> x = BitVec('x', 32) >>> 10 << x 10 << x >>> (10 << x).sexpr() '(bvshl #x0000000a x)' __rmod__(self, other)Create the Z3 expression (signed) mod `other % self`.   Use the function URem() for unsigned remainder, and SRem() for signed remainder.   >>> x = BitVec('x', 32) >>> 10 % x 10%x >>> (10 % x).sexpr() '(bvsmod #x0000000a x)' >>> URem(10, x).sexpr() '(bvurem #x0000000a x)' >>> SRem(10, x).sexpr() '(bvsrem #x0000000a x)' __rmul__(self, other)Create the Z3 expression `other * self`.   >>> x = BitVec('x', 32) >>> 10 * x 10*x __ror__(self, other)Create the Z3 expression bitwise-or `other | self`.   >>> x = BitVec('x', 32) >>> 10 | x 10 | x __rrshift__(self, other)Create the Z3 expression (arithmetical) right shift `other` >> `self`.   Use the function LShR() for the right logical shift   >>> x = BitVec('x', 32) >>> 10 >> x 10 >> x >>> (10 >> x).sexpr() '(bvashr #x0000000a x)' __rshift__(self, other)Create the Z3 expression (arithmetical) right shift `self >> other`   Use the function LShR() for the right logical shift   >>> x, y = BitVecs('x y', 32) >>> x >> y x >> y >>> (x >> y).sexpr() '(bvashr x y)' >>> LShR(x, y).sexpr() '(bvlshr x y)' >>> BitVecVal(4, 3) 4 >>> BitVecVal(4, 3).as_signed_long() -4L >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() -2L >>> simplify(BitVecVal(4, 3) >> 1) 6 >>> simplify(LShR(BitVecVal(4, 3), 1)) 2 >>> simplify(BitVecVal(2, 3) >> 1) 1 >>> simplify(LShR(BitVecVal(2, 3), 1)) 1 __rsub__(self, other)Create the Z3 expression `other - self`.   >>> x = BitVec('x', 32) >>> 10 - x 10 - x __rtruediv__(self, other)Create the Z3 expression (signed) division `other / self`. __rxor__(self, other)Create the Z3 expression bitwise-xor `other ^ self`.   >>> x = BitVec('x', 32) >>> 10 ^ x 10 ^ x __sub__(self, other)Create the Z3 expression `self - other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x - y x - y >>> (x - y).sort() BitVec(32) __truediv__(self, other)Create the Z3 expression (signed) division `self / other`. __xor__(self, other)Create the Z3 expression bitwise-xor `self ^ other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x ^ y x ^ y >>> (x ^ y).sort() BitVec(32) size(self)Return the number of bits of the bit-vector expression `self`.   >>> x = BitVec('x', 32) >>> (x + 1).size() 32 >>> Concat(x, x).size() 64 sort(self)Return the sort of the bit-vector expression `self`.   >>> x = BitVec('x', 32) >>> x.sort() BitVec(32) >>> x.sort() == BitVecSort(32) True Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 as_ast(self) children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class BitVecRef(ExprRef) Bit-vector expressions. Method resolution order: BitVecRef ExprRef AstRef Z3PPObject Methods defined here: __add__(self, other)Create the Z3 expression `self + other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x + y x + y >>> (x + y).sort() BitVec(32) __and__(self, other)Create the Z3 expression bitwise-and `self & other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x & y x & y >>> (x & y).sort() BitVec(32) __div__(self, other)Create the Z3 expression (signed) division `self / other`.   Use the function UDiv() for unsigned division.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x / y x/y >>> (x / y).sort() BitVec(32) >>> (x / y).sexpr() '(bvsdiv x y)' >>> UDiv(x, y).sexpr() '(bvudiv x y)' __ge__(self, other)Create the Z3 expression (signed) `other >= self`.   Use the function UGE() for unsigned greater than or equal to.   >>> x, y = BitVecs('x y', 32) >>> x >= y x >= y >>> (x >= y).sexpr() '(bvsge x y)' >>> UGE(x, y).sexpr() '(bvuge x y)' __gt__(self, other)Create the Z3 expression (signed) `other > self`.   Use the function UGT() for unsigned greater than.   >>> x, y = BitVecs('x y', 32) >>> x > y x > y >>> (x > y).sexpr() '(bvsgt x y)' >>> UGT(x, y).sexpr() '(bvugt x y)' __invert__(self)Create the Z3 expression bitwise-not `~self`.   >>> x = BitVec('x', 32) >>> ~x ~x >>> simplify(~(~x)) x __le__(self, other)Create the Z3 expression (signed) `other <= self`.   Use the function ULE() for unsigned less than or equal to.   >>> x, y = BitVecs('x y', 32) >>> x <= y x <= y >>> (x <= y).sexpr() '(bvsle x y)' >>> ULE(x, y).sexpr() '(bvule x y)' __lshift__(self, other)Create the Z3 expression left shift `self << other`   >>> x, y = BitVecs('x y', 32) >>> x << y x << y >>> (x << y).sexpr() '(bvshl x y)' >>> simplify(BitVecVal(2, 3) << 1) 4 __lt__(self, other)Create the Z3 expression (signed) `other < self`.   Use the function ULT() for unsigned less than.   >>> x, y = BitVecs('x y', 32) >>> x < y x < y >>> (x < y).sexpr() '(bvslt x y)' >>> ULT(x, y).sexpr() '(bvult x y)' __mod__(self, other)Create the Z3 expression (signed) mod `self % other`.   Use the function URem() for unsigned remainder, and SRem() for signed remainder.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x % y x%y >>> (x % y).sort() BitVec(32) >>> (x % y).sexpr() '(bvsmod x y)' >>> URem(x, y).sexpr() '(bvurem x y)' >>> SRem(x, y).sexpr() '(bvsrem x y)' __mul__(self, other)Create the Z3 expression `self * other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x * y x*y >>> (x * y).sort() BitVec(32) __neg__(self)Return an expression representing `-self`.   >>> x = BitVec('x', 32) >>> -x -x >>> simplify(-(-x)) x __or__(self, other)Create the Z3 expression bitwise-or `self | other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x | y x | y >>> (x | y).sort() BitVec(32) __pos__(self)Return `self`.   >>> x = BitVec('x', 32) >>> +x x __radd__(self, other)Create the Z3 expression `other + self`.   >>> x = BitVec('x', 32) >>> 10 + x 10 + x __rand__(self, other)Create the Z3 expression bitwise-or `other & self`.   >>> x = BitVec('x', 32) >>> 10 & x 10 & x __rdiv__(self, other)Create the Z3 expression (signed) division `other / self`.   Use the function UDiv() for unsigned division.   >>> x = BitVec('x', 32) >>> 10 / x 10/x >>> (10 / x).sexpr() '(bvsdiv #x0000000a x)' >>> UDiv(10, x).sexpr() '(bvudiv #x0000000a x)' __rlshift__(self, other)Create the Z3 expression left shift `other << self`.   Use the function LShR() for the right logical shift   >>> x = BitVec('x', 32) >>> 10 << x 10 << x >>> (10 << x).sexpr() '(bvshl #x0000000a x)' __rmod__(self, other)Create the Z3 expression (signed) mod `other % self`.   Use the function URem() for unsigned remainder, and SRem() for signed remainder.   >>> x = BitVec('x', 32) >>> 10 % x 10%x >>> (10 % x).sexpr() '(bvsmod #x0000000a x)' >>> URem(10, x).sexpr() '(bvurem #x0000000a x)' >>> SRem(10, x).sexpr() '(bvsrem #x0000000a x)' __rmul__(self, other)Create the Z3 expression `other * self`.   >>> x = BitVec('x', 32) >>> 10 * x 10*x __ror__(self, other)Create the Z3 expression bitwise-or `other | self`.   >>> x = BitVec('x', 32) >>> 10 | x 10 | x __rrshift__(self, other)Create the Z3 expression (arithmetical) right shift `other` >> `self`.   Use the function LShR() for the right logical shift   >>> x = BitVec('x', 32) >>> 10 >> x 10 >> x >>> (10 >> x).sexpr() '(bvashr #x0000000a x)' __rshift__(self, other)Create the Z3 expression (arithmetical) right shift `self >> other`   Use the function LShR() for the right logical shift   >>> x, y = BitVecs('x y', 32) >>> x >> y x >> y >>> (x >> y).sexpr() '(bvashr x y)' >>> LShR(x, y).sexpr() '(bvlshr x y)' >>> BitVecVal(4, 3) 4 >>> BitVecVal(4, 3).as_signed_long() -4L >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() -2L >>> simplify(BitVecVal(4, 3) >> 1) 6 >>> simplify(LShR(BitVecVal(4, 3), 1)) 2 >>> simplify(BitVecVal(2, 3) >> 1) 1 >>> simplify(LShR(BitVecVal(2, 3), 1)) 1 __rsub__(self, other)Create the Z3 expression `other - self`.   >>> x = BitVec('x', 32) >>> 10 - x 10 - x __rtruediv__(self, other)Create the Z3 expression (signed) division `other / self`. __rxor__(self, other)Create the Z3 expression bitwise-xor `other ^ self`.   >>> x = BitVec('x', 32) >>> 10 ^ x 10 ^ x __sub__(self, other)Create the Z3 expression `self - other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x - y x - y >>> (x - y).sort() BitVec(32) __truediv__(self, other)Create the Z3 expression (signed) division `self / other`. __xor__(self, other)Create the Z3 expression bitwise-xor `self ^ other`.   >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> x ^ y x ^ y >>> (x ^ y).sort() BitVec(32) size(self)Return the number of bits of the bit-vector expression `self`.   >>> x = BitVec('x', 32) >>> (x + 1).size() 32 >>> Concat(x, x).size() 64 sort(self)Return the sort of the bit-vector expression `self`.   >>> x = BitVec('x', 32) >>> x.sort() BitVec(32) >>> x.sort() == BitVecSort(32) True Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 as_ast(self) children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class BitVecSortRef(SortRef) Bit-vector sort. Method resolution order: BitVecSortRef SortRef AstRef Z3PPObject Methods defined here: cast(self, val)Try to cast `val` as a Bit-Vector.   >>> b = BitVecSort(32) >>> b.cast(10) 10 >>> b.cast(10).sexpr() '#x0000000a' size(self)Return the size (number of bits) of the bit-vector sort `self`.   >>> b = BitVecSort(32) >>> b.size() 32 subsort(self, other) Methods inherited from SortRef: __eq__(self, other)Return `True` if `self` and `other` are the same Z3 sort.   >>> p = Bool('p') >>> p.sort() == BoolSort() True >>> p.sort() == IntSort() False __ne__(self, other)Return `True` if `self` and `other` are not the same Z3 sort.   >>> p = Bool('p') >>> p.sort() != BoolSort() False >>> p.sort() != IntSort() True as_ast(self) kind(self)Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.   >>> b = BoolSort() >>> b.kind() == Z3_BOOL_SORT True >>> b.kind() == Z3_INT_SORT False >>> A = ArraySort(IntSort(), IntSort()) >>> A.kind() == Z3_ARRAY_SORT True >>> A.kind() == Z3_INT_SORT False name(self)Return the name (string) of sort `self`.   >>> BoolSort().name() 'Bool' >>> ArraySort(IntSort(), IntSort()).name() 'Array' Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class BoolRef(ExprRef) All Boolean expressions are instances of this class. Method resolution order: BoolRef ExprRef AstRef Z3PPObject Methods defined here: sort(self) Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 as_ast(self) children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class BoolSortRef(SortRef) Boolean sort. Method resolution order: BoolSortRef SortRef AstRef Z3PPObject Methods defined here: cast(self, val)Try to cast `val` as a Boolean.   >>> x = BoolSort().cast(True) >>> x True >>> is_expr(x) True >>> is_expr(True) False >>> x.sort() Bool Methods inherited from SortRef: __eq__(self, other)Return `True` if `self` and `other` are the same Z3 sort.   >>> p = Bool('p') >>> p.sort() == BoolSort() True >>> p.sort() == IntSort() False __ne__(self, other)Return `True` if `self` and `other` are not the same Z3 sort.   >>> p = Bool('p') >>> p.sort() != BoolSort() False >>> p.sort() != IntSort() True as_ast(self) kind(self)Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.   >>> b = BoolSort() >>> b.kind() == Z3_BOOL_SORT True >>> b.kind() == Z3_INT_SORT False >>> A = ArraySort(IntSort(), IntSort()) >>> A.kind() == Z3_ARRAY_SORT True >>> A.kind() == Z3_INT_SORT False name(self)Return the name (string) of sort `self`.   >>> BoolSort().name() 'Bool' >>> ArraySort(IntSort(), IntSort()).name() 'Array' subsort(self, other)Return `True` if `self` is a subsort of `other`.    >>> IntSort().subsort(RealSort()) True Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class CheckSatResult Represents the result of a satisfiability check: sat, unsat, unknown.   >>> s = Solver() >>> s.check() sat >>> r = s.check() >>> isinstance(r, CheckSatResult) True Methods defined here: __eq__(self, other) __init__(self, r) __ne__(self, other) __repr__(self)

 class Context A Context manages all other Z3 objects, global configuration options, etc.   Z3Py uses a default global context. For most applications this is sufficient. An application may use multiple Z3 contexts. Objects created in one context cannot be used in another one. However, several objects may be "translated" from one context to another. It is not safe to access Z3 objects from multiple threads. The only exception is the method `interrupt()` that can be used to interrupt() a long  computation. The initialization method receives global configuration options for the new context. Methods defined here: __del__(self) __init__(self, *args, **kws) interrupt(self)Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.     This method can be invoked from a thread different from the one executing the interruptable procedure. ref(self)Return a reference to the actual C pointer to the Z3 context. set(self, *args, **kws)Set global configuration options.    Z3 command line options can be set using this method.  The option names can be specified in different ways:   >>> ctx = Context() >>> ctx.set('WELL_SORTED_CHECK', True) >>> ctx.set(':well-sorted-check', True) >>> ctx.set(well_sorted_check=True)

 class Datatype Helper class for declaring Z3 datatypes.    >>> List = Datatype('List') >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) >>> List.declare('nil') >>> List = List.create() >>> # List is now a Z3 declaration >>> List.nil nil >>> List.cons(10, List.nil) cons(10, nil) >>> List.cons(10, List.nil).sort() List >>> cons = List.cons >>> nil  = List.nil >>> car  = List.car >>> cdr  = List.cdr >>> n = cons(1, cons(0, nil)) >>> n cons(1, cons(0, nil)) >>> simplify(cdr(n)) cons(0, nil) >>> simplify(car(n)) 1 Methods defined here: __init__(self, name, ctx=None) __repr__(self) create(self)Create a Z3 datatype based on the constructors declared using the mehtod `declare()`.   The function `CreateDatatypes()` must be used to define mutually recursive datatypes.   >>> List = Datatype('List') >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) >>> List.declare('nil') >>> List = List.create() >>> List.nil nil >>> List.cons(10, List.nil) cons(10, nil) declare(self, name, *args)Declare constructor named `name` with the given accessors `args`.  Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared.    In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))`  declares the constructor named `cons` that builds a new List using an integer and a List.  It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell,  and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create  the actual datatype in Z3.   >>> List = Datatype('List') >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) >>> List.declare('nil') >>> List = List.create() declare_core(self, name, rec_name, *args)

 class DatatypeRef(ExprRef) Datatype expressions. Method resolution order: DatatypeRef ExprRef AstRef Z3PPObject Methods defined here: sort(self)Return the datatype sort of the datatype expression `self`. Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 as_ast(self) children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class DatatypeSortRef(SortRef) Datatype sorts. Method resolution order: DatatypeSortRef SortRef AstRef Z3PPObject Methods defined here: accessor(self, i, j)In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.   >>> List = Datatype('List') >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) >>> List.declare('nil') >>> List = List.create() >>> List.num_constructors() 2 >>> List.constructor(0) cons >>> num_accs = List.constructor(0).arity() >>> num_accs 2 >>> List.accessor(0, 0) car >>> List.accessor(0, 1) cdr >>> List.constructor(1) nil >>> num_accs = List.constructor(1).arity() >>> num_accs 0 constructor(self, idx)Return a constructor of the datatype `self`.   >>> List = Datatype('List') >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) >>> List.declare('nil') >>> List = List.create() >>> # List is now a Z3 declaration >>> List.num_constructors() 2 >>> List.constructor(0) cons >>> List.constructor(1) nil num_constructors(self)Return the number of constructors in the given Z3 datatype.    >>> List = Datatype('List') >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) >>> List.declare('nil') >>> List = List.create() >>> # List is now a Z3 declaration >>> List.num_constructors() 2 recognizer(self, idx)In Z3, each constructor has an associated recognizer predicate.    If the constructor is named `name`, then the recognizer `is_name`.   >>> List = Datatype('List') >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) >>> List.declare('nil') >>> List = List.create() >>> # List is now a Z3 declaration >>> List.num_constructors() 2 >>> List.recognizer(0) is_cons >>> List.recognizer(1) is_nil >>> simplify(List.is_nil(List.cons(10, List.nil))) False >>> simplify(List.is_cons(List.cons(10, List.nil))) True >>> l = Const('l', List) >>> simplify(List.is_cons(l)) is_cons(l) Methods inherited from SortRef: __eq__(self, other)Return `True` if `self` and `other` are the same Z3 sort.   >>> p = Bool('p') >>> p.sort() == BoolSort() True >>> p.sort() == IntSort() False __ne__(self, other)Return `True` if `self` and `other` are not the same Z3 sort.   >>> p = Bool('p') >>> p.sort() != BoolSort() False >>> p.sort() != IntSort() True as_ast(self) cast(self, val)Try to cast `val` as an element of sort `self`.    This method is used in Z3Py to convert Python objects such as integers, floats, longs and strings into Z3 expressions.   >>> x = Int('x') >>> RealSort().cast(x) ToReal(x) kind(self)Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.   >>> b = BoolSort() >>> b.kind() == Z3_BOOL_SORT True >>> b.kind() == Z3_INT_SORT False >>> A = ArraySort(IntSort(), IntSort()) >>> A.kind() == Z3_ARRAY_SORT True >>> A.kind() == Z3_INT_SORT False name(self)Return the name (string) of sort `self`.   >>> BoolSort().name() 'Bool' >>> ArraySort(IntSort(), IntSort()).name() 'Array' subsort(self, other)Return `True` if `self` is a subsort of `other`.    >>> IntSort().subsort(RealSort()) True Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class ExprRef(AstRef) Constraints, formulas and terms are expressions in Z3.   Expressions are ASTs. Every expression has a sort. There are three main kinds of expressions:  function applications, quantifiers and bounded variables. A constant is a function application with 0 arguments. For quantifier free problems, all expressions are  function applications. Method resolution order: ExprRef AstRef Z3PPObject Methods defined here: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 as_ast(self) children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort(self)Return the sort of expression `self`.   >>> x = Int('x') >>> (x + 1).sort() Int >>> y = Real('y') >>> (x + y).sort() Real sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class FuncDeclRef(AstRef) Function declaration. Every constant and function have an associated declaration.   The declaration assigns a name, a sort (i.e., type), and for function the sort (i.e., type) of each of its arguments. Note that, in Z3,  a constant is a function with 0 arguments. Method resolution order: FuncDeclRef AstRef Z3PPObject Methods defined here: __call__(self, *args)Create a Z3 application expression using the function `self`, and the given arguments.    The arguments must be Z3 expressions. This method assumes that the sorts of the elements in `args` match the sorts of the domain. Limited coersion is supported.  For example, if args[0] is a Python integer, and the function expects a Z3 integer, then the argument is automatically converted into a Z3 integer.   >>> f = Function('f', IntSort(), RealSort(), BoolSort()) >>> x = Int('x') >>> y = Real('y') >>> f(x, y) f(x, y) >>> f(x, x) f(x, ToReal(x)) arity(self)Return the number of arguments of a function declaration. If `self` is a constant, then `arity()` is 0.   >>> f = Function('f', IntSort(), RealSort(), BoolSort()) >>> f.arity() 2 as_ast(self) domain(self, i)Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < arity()`.   >>> f = Function('f', IntSort(), RealSort(), BoolSort()) >>> f.domain(0) Int >>> f.domain(1) Real kind(self)Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc.   >>> x = Int('x') >>> d = (x + 1).decl() >>> d.kind() == Z3_OP_ADD True >>> d.kind() == Z3_OP_MUL False name(self)Return the name of the function declaration `self`.   >>> f = Function('f', IntSort(), IntSort()) >>> f.name() 'f' >>> isinstance(f.name(), str) True range(self)Return the sort of the range of a function declaration. For constants, this is the sort of the constant.   >>> f = Function('f', IntSort(), RealSort(), BoolSort()) >>> f.range() Bool Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class FuncEntry Store the value of the interpretation of a function in a particular point. Methods defined here: __del__(self) __init__(self, entry, ctx) __repr__(self) arg_value(self, idx)Return the value of argument `idx`.   >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) >>> s.check() sat >>> m = s.model() >>> f_i = m[f] >>> f_i.num_entries() 3 >>> e = f_i.entry(0) >>> e [0, 1, 10] >>> e.num_args() 2 >>> e.arg_value(0) 0 >>> e.arg_value(1) 1 >>> try: ...   e.arg_value(2) ... except IndexError: ...   print "index error" index error as_list(self)Return entry `self` as a Python list. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) >>> s.check() sat >>> m = s.model() >>> f_i = m[f] >>> f_i.num_entries() 3 >>> e = f_i.entry(0) >>> e.as_list() [0, 1, 10] num_args(self)Return the number of arguments in the given entry.   >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) >>> s.check() sat >>> m = s.model() >>> f_i = m[f] >>> f_i.num_entries() 3 >>> e = f_i.entry(0) >>> e.num_args() 2 value(self)Return the value of the function at point `self`.   >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) >>> s.check() sat >>> m = s.model() >>> f_i = m[f] >>> f_i.num_entries() 3 >>> e = f_i.entry(0) >>> e [0, 1, 10] >>> e.num_args() 2 >>> e.value() 10

 class FuncInterp(Z3PPObject) Stores the interpretation of a function in a Z3 model. Methods defined here: __del__(self) __init__(self, f, ctx) __repr__(self) arity(self)Return the number of arguments for each entry in the function interpretation `self`.   >>> f = Function('f', IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) >>> s.check() sat >>> m = s.model() >>> m[f].arity() 1 as_list(self)Return the function interpretation as a Python list. >>> f = Function('f', IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) >>> s.check() sat >>> m = s.model() >>> m[f] [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] >>> m[f].as_list() [[0, 1], [1, 1], [2, 0], 1] else_value(self)Return the `else` value for a function interpretation.   >>> f = Function('f', IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) >>> s.check() sat >>> m = s.model() >>> m[f] [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] >>> m[f].else_value() 1 entry(self, idx)Return an entry at position `idx < num_entries()` in the function interpretation `self`.   >>> f = Function('f', IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) >>> s.check() sat >>> m = s.model() >>> m[f] [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] >>> m[f].num_entries() 3 >>> m[f].entry(0) [0, 1] >>> m[f].entry(1) [1, 1] >>> m[f].entry(2) [2, 0] num_entries(self)Return the number of entries/points in the function interpretation `self`.   >>> f = Function('f', IntSort(), IntSort()) >>> s = Solver() >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) >>> s.check() sat >>> m = s.model() >>> m[f] [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] >>> m[f].num_entries() 3 Methods inherited from Z3PPObject: use_pp(self)

 class IntNumRef(ArithRef) Integer values. Method resolution order: IntNumRef ArithRef ExprRef AstRef Z3PPObject Methods defined here: as_long(self)Return a Z3 integer numeral as a Python long (bignum) numeral.    >>> v = IntVal(1) >>> v + 1 1 + 1 >>> v.as_long() + 1 2L as_string(self)Return a Z3 integer numeral as a Python string. >>> v = IntVal(100) >>> v.as_string() '100' Methods inherited from ArithRef: __add__(self, other)Create the Z3 expression `self + other`.   >>> x = Int('x') >>> y = Int('y') >>> x + y x + y >>> (x + y).sort() Int __div__(self, other)Create the Z3 expression `other/self`.   >>> x = Int('x') >>> y = Int('y') >>> x/y x/y >>> (x/y).sort() Int >>> (x/y).sexpr() '(div x y)' >>> x = Real('x') >>> y = Real('y') >>> x/y x/y >>> (x/y).sort() Real >>> (x/y).sexpr() '(/ x y)' __ge__(self, other)Create the Z3 expression `other >= self`.   >>> x, y = Ints('x y') >>> x >= y x >= y >>> y = Real('y') >>> x >= y ToReal(x) >= y __gt__(self, other)Create the Z3 expression `other > self`.   >>> x, y = Ints('x y') >>> x > y x > y >>> y = Real('y') >>> x > y ToReal(x) > y __le__(self, other)Create the Z3 expression `other <= self`.   >>> x, y = Ints('x y') >>> x <= y x <= y >>> y = Real('y') >>> x <= y ToReal(x) <= y __lt__(self, other)Create the Z3 expression `other < self`.   >>> x, y = Ints('x y') >>> x < y x < y >>> y = Real('y') >>> x < y ToReal(x) < y __mod__(self, other)Create the Z3 expression `other%self`.   >>> x = Int('x') >>> y = Int('y') >>> x % y x%y >>> simplify(IntVal(10) % IntVal(3)) 1 __mul__(self, other)Create the Z3 expression `self * other`.   >>> x = Real('x') >>> y = Real('y') >>> x * y x*y >>> (x * y).sort() Real __neg__(self)Return an expression representing `-self`.   >>> x = Int('x') >>> -x -x >>> simplify(-(-x)) x __pos__(self)Return `self`.   >>> x = Int('x') >>> +x x __pow__(self, other)Create the Z3 expression `self**other` (** is the power operator).   >>> x = Real('x') >>> x**3 x**3 >>> (x**3).sort() Real >>> simplify(IntVal(2)**8) 256 __radd__(self, other)Create the Z3 expression `other + self`.   >>> x = Int('x') >>> 10 + x 10 + x __rdiv__(self, other)Create the Z3 expression `other/self`.   >>> x = Int('x') >>> 10/x 10/x >>> (10/x).sexpr() '(div 10 x)' >>> x = Real('x') >>> 10/x 10/x >>> (10/x).sexpr() '(/ 10.0 x)' __rmod__(self, other)Create the Z3 expression `other%self`.   >>> x = Int('x') >>> 10 % x 10%x __rmul__(self, other)Create the Z3 expression `other * self`.   >>> x = Real('x') >>> 10 * x 10*x __rpow__(self, other)Create the Z3 expression `other**self` (** is the power operator).   >>> x = Real('x') >>> 2**x 2**x >>> (2**x).sort() Real >>> simplify(2**IntVal(8)) 256 __rsub__(self, other)Create the Z3 expression `other - self`.   >>> x = Int('x') >>> 10 - x 10 - x __rtruediv__(self, other)Create the Z3 expression `other/self`. __sub__(self, other)Create the Z3 expression `self - other`.   >>> x = Int('x') >>> y = Int('y') >>> x - y x - y >>> (x - y).sort() Int __truediv__(self, other)Create the Z3 expression `other/self`. is_int(self)Return `True` if `self` is an integer expression.   >>> x = Int('x') >>> x.is_int() True >>> (x + 1).is_int() True >>> y = Real('y') >>> (x + y).is_int() False is_real(self)Return `True` if `self` is an real expression.   >>> x = Real('x') >>> x.is_real() True >>> (x + 1).is_real() True sort(self)Return the sort (type) of the arithmetical expression `self`.   >>> Int('x').sort() Int >>> (Real('x') + 1).sort() Real Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 as_ast(self) children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class ParamDescrsRef Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3. Methods defined here: __del__(self) __getitem__(self, arg) __init__(self, descr, ctx=None) __len__(self)Return the size of in the parameter description `self`. get_kind(self, n)Return the kind of the parameter named `n`. get_name(self, i)Return the i-th parameter name in the parameter description `self`. size(self)Return the size of in the parameter description `self`.

 class ParamsRef Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3.   Consider using the function `args2params` to create instances of this object. Methods defined here: __del__(self) __init__(self, ctx=None) __repr__(self) set(self, name, val)Set parameter name with value val. validate(self, ds)

 class PatternRef(ExprRef) Patterns are hints for quantifier instantiation.    See http://rise4fun.com/Z3Py/tutorial/advanced for more details. Method resolution order: PatternRef ExprRef AstRef Z3PPObject Methods defined here: as_ast(self) Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort(self)Return the sort of expression `self`.   >>> x = Int('x') >>> (x + 1).sort() Int >>> y = Real('y') >>> (x + y).sort() Real sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class QuantifierRef(BoolRef) Universally and Existentially quantified formulas. Method resolution order: QuantifierRef BoolRef ExprRef AstRef Z3PPObject Methods defined here: as_ast(self) body(self)Return the expression being quantified.   >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0) >>> q.body() f(Var(0)) == 0 children(self)Return a list containing a single element body()   >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0) >>> q.children() [f(Var(0)) == 0] is_forall(self)Return `True` if `self` is a universal quantifier.   >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0) >>> q.is_forall() True >>> q = Exists(x, f(x) != 0) >>> q.is_forall() False no_pattern(self, idx)Return a no-pattern. num_no_patterns(self)Return the number of no-patterns. num_patterns(self)Return the number of patterns (i.e., quantifier instantiation hints) in `self`.   >>> f = Function('f', IntSort(), IntSort()) >>> g = Function('g', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ]) >>> q.num_patterns() 2 num_vars(self)Return the number of variables bounded by this quantifier.    >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') >>> y = Int('y') >>> q = ForAll([x, y], f(x, y) >= x) >>> q.num_vars()  2 pattern(self, idx)Return a pattern (i.e., quantifier instantiation hints) in `self`.   >>> f = Function('f', IntSort(), IntSort()) >>> g = Function('g', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) != g(x), patterns = [ f(x), g(x) ]) >>> q.num_patterns() 2 >>> q.pattern(0) f(Var(0)) >>> q.pattern(1) g(Var(0)) sort(self)Return the Boolean sort. var_name(self, idx)Return a string representing a name used when displaying the quantifier.    >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') >>> y = Int('y') >>> q = ForAll([x, y], f(x, y) >= x) >>> q.var_name(0) 'x' >>> q.var_name(1) 'y' var_sort(self, idx)Return the sort of a bound variable.   >>> f = Function('f', IntSort(), RealSort(), IntSort()) >>> x = Int('x') >>> y = Real('y') >>> q = ForAll([x, y], f(x, y) >= x) >>> q.var_sort(0) Int >>> q.var_sort(1) Real weight(self)Return the weight annotation of `self`.   >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0) >>> q.weight() 1 >>> q = ForAll(x, f(x) == 0, weight=10) >>> q.weight() 10 Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class RatNumRef(ArithRef) Rational values. Method resolution order: RatNumRef ArithRef ExprRef AstRef Z3PPObject Methods defined here: as_decimal(self, prec)Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.   >>> v = RealVal("1/5") >>> v.as_decimal(3) '0.2' >>> v = RealVal("1/3") >>> v.as_decimal(3) '0.333?' as_string(self)Return a Z3 rational numeral as a Python string.   >>> v = Q(3,6) >>> v.as_string() '1/2' denominator(self)Return the denominator of a Z3 rational numeral.    >>> is_rational_value(Q(3,5)) True >>> n = Q(3,5) >>> n.denominator() 5 denominator_as_long(self)Return the denominator as a Python long.   >>> v = RealVal("1/3") >>> v 1/3 >>> v.denominator_as_long() 3L numerator(self)Return the numerator of a Z3 rational numeral.    >>> is_rational_value(RealVal("3/5")) True >>> n = RealVal("3/5") >>> n.numerator() 3 >>> is_rational_value(Q(3,5)) True >>> Q(3,5).numerator() 3 numerator_as_long(self)Return the numerator as a Python long.   >>> v = RealVal(10000000000) >>> v 10000000000 >>> v + 1 10000000000 + 1 >>> v.numerator_as_long() + 1 10000000001L Methods inherited from ArithRef: __add__(self, other)Create the Z3 expression `self + other`.   >>> x = Int('x') >>> y = Int('y') >>> x + y x + y >>> (x + y).sort() Int __div__(self, other)Create the Z3 expression `other/self`.   >>> x = Int('x') >>> y = Int('y') >>> x/y x/y >>> (x/y).sort() Int >>> (x/y).sexpr() '(div x y)' >>> x = Real('x') >>> y = Real('y') >>> x/y x/y >>> (x/y).sort() Real >>> (x/y).sexpr() '(/ x y)' __ge__(self, other)Create the Z3 expression `other >= self`.   >>> x, y = Ints('x y') >>> x >= y x >= y >>> y = Real('y') >>> x >= y ToReal(x) >= y __gt__(self, other)Create the Z3 expression `other > self`.   >>> x, y = Ints('x y') >>> x > y x > y >>> y = Real('y') >>> x > y ToReal(x) > y __le__(self, other)Create the Z3 expression `other <= self`.   >>> x, y = Ints('x y') >>> x <= y x <= y >>> y = Real('y') >>> x <= y ToReal(x) <= y __lt__(self, other)Create the Z3 expression `other < self`.   >>> x, y = Ints('x y') >>> x < y x < y >>> y = Real('y') >>> x < y ToReal(x) < y __mod__(self, other)Create the Z3 expression `other%self`.   >>> x = Int('x') >>> y = Int('y') >>> x % y x%y >>> simplify(IntVal(10) % IntVal(3)) 1 __mul__(self, other)Create the Z3 expression `self * other`.   >>> x = Real('x') >>> y = Real('y') >>> x * y x*y >>> (x * y).sort() Real __neg__(self)Return an expression representing `-self`.   >>> x = Int('x') >>> -x -x >>> simplify(-(-x)) x __pos__(self)Return `self`.   >>> x = Int('x') >>> +x x __pow__(self, other)Create the Z3 expression `self**other` (** is the power operator).   >>> x = Real('x') >>> x**3 x**3 >>> (x**3).sort() Real >>> simplify(IntVal(2)**8) 256 __radd__(self, other)Create the Z3 expression `other + self`.   >>> x = Int('x') >>> 10 + x 10 + x __rdiv__(self, other)Create the Z3 expression `other/self`.   >>> x = Int('x') >>> 10/x 10/x >>> (10/x).sexpr() '(div 10 x)' >>> x = Real('x') >>> 10/x 10/x >>> (10/x).sexpr() '(/ 10.0 x)' __rmod__(self, other)Create the Z3 expression `other%self`.   >>> x = Int('x') >>> 10 % x 10%x __rmul__(self, other)Create the Z3 expression `other * self`.   >>> x = Real('x') >>> 10 * x 10*x __rpow__(self, other)Create the Z3 expression `other**self` (** is the power operator).   >>> x = Real('x') >>> 2**x 2**x >>> (2**x).sort() Real >>> simplify(2**IntVal(8)) 256 __rsub__(self, other)Create the Z3 expression `other - self`.   >>> x = Int('x') >>> 10 - x 10 - x __rtruediv__(self, other)Create the Z3 expression `other/self`. __sub__(self, other)Create the Z3 expression `self - other`.   >>> x = Int('x') >>> y = Int('y') >>> x - y x - y >>> (x - y).sort() Int __truediv__(self, other)Create the Z3 expression `other/self`. is_int(self)Return `True` if `self` is an integer expression.   >>> x = Int('x') >>> x.is_int() True >>> (x + 1).is_int() True >>> y = Real('y') >>> (x + y).is_int() False is_real(self)Return `True` if `self` is an real expression.   >>> x = Real('x') >>> x.is_real() True >>> (x + 1).is_real() True sort(self)Return the sort (type) of the arithmetical expression `self`.   >>> Int('x').sort() Int >>> (Real('x') + 1).sort() Real Methods inherited from ExprRef: __eq__(self, other)Return a Z3 expression that represents the constraint `self == other`.   If `other` is `None`, then this method simply returns `False`.    >>> a = Int('a') >>> b = Int('b') >>> a == b a == b >>> a == None False __ne__(self, other)Return a Z3 expression that represents the constraint `self != other`.   If `other` is `None`, then this method simply returns `True`.    >>> a = Int('a') >>> b = Int('b') >>> a != b a != b >>> a != None True arg(self, idx)Return argument `idx` of the application `self`.    This method assumes that `self` is a function application with at least `idx+1` arguments.   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.arg(0) a >>> t.arg(1) b >>> t.arg(2) 0 as_ast(self) children(self)Return a list containing the children of the given expression   >>> a = Int('a') >>> b = Int('b') >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.children() [a, b, 0] decl(self)Return the Z3 function declaration associated with a Z3 application.   >>> f = Function('f', IntSort(), IntSort()) >>> a = Int('a') >>> t = f(a) >>> eq(t.decl(), f) True >>> (a + 1).decl() + num_args(self)Return the number of arguments of a Z3 application.   >>> a = Int('a') >>> b = Int('b') >>> (a + b).num_args() 2 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) >>> t = f(a, b, 0) >>> t.num_args() 3 sort_kind(self)Shorthand for `sort().kind()`.   >>> a = Array('a', IntSort(), IntSort()) >>> a.sort_kind() == Z3_ARRAY_SORT True >>> a.sort_kind() == Z3_INT_SORT False Methods inherited from AstRef: __del__(self) __init__(self, ast, ctx=None) __repr__(self) __str__(self) ctx_ref(self)Return a reference to the C context where this AST node is stored. eq(self, other)Return `True` if `self` and `other` are structurally identical.   >>> x = Int('x') >>> n1 = x + 1 >>> n2 = 1 + x >>> n1.eq(n2) False >>> n1 = simplify(n1) >>> n2 = simplify(n2) >>> n1.eq(n2) True hash(self)Return a hashcode for the `self`.   >>> n1 = simplify(Int('x') + 1) >>> n2 = simplify(2 + Int('x') - 1) >>> n1.hash() == n2.hash() True sexpr(self)Return an string representing the AST node in s-expression notation.   >>> x = Int('x') >>> ((x + 1)*x).sexpr() '(* (+ x 1) x)' translate(self, target)Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.    >>> c1 = Context() >>> c2 = Context() >>> x  = Int('x', c1) >>> y  = Int('y', c2) >>> # Nodes in different contexts can't be mixed. >>> # However, we can translate nodes from one context to another. >>> x.translate(c2) + y x + y Methods inherited from Z3PPObject: use_pp(self)

 class ScopedConstructor Auxiliary object used to create Z3 datatypes. Methods defined here: __del__(self) __init__(self, c, ctx)

 class ScopedConstructorList Auxiliary object used to create Z3 datatypes. Methods defined here: __del__(self) __init__(self, c, ctx)