z3
index
c:\dev\z3-master\src\api\python\z3.py

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
 
Please send feedback, comments and/or corrections to leonardo@microsoft.com. Your comments are very valuable.
 
Small example:
 
>>> x = Int('x')
>>> y = Int('y')
>>> s = Solver()
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> s.add(y == x + 1)
>>> s.check()
sat
>>> m = s.model()
>>> m[x]
1
>>> m[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: %s" % ex)
failed: sort mismatch

 
Modules
       
codecs
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()
+
get_id(self)
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()
+
get_id(self)
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 of the sort Integer.
 
>>> 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 of the sort Real.
 
>>> 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)
get_id(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()
+
get_id(self)
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)
get_id(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 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
get_id(self)
Return unique identifier for object. It can be used for hash-tables and maps.
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()
-4
>>> BitVecVal(7, 3).as_signed_long()
-1
>>> BitVecVal(3, 3).as_signed_long()
3
>>> BitVecVal(2**32 - 1, 32).as_signed_long()
-1
>>> BitVecVal(2**64 - 1, 64).as_signed_long()
-1
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()
-4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2
>>> 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()
+
get_id(self)
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()
-4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2
>>> 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()
+
get_id(self)
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)
get_id(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()
+
get_id(self)
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)
get_id(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
    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.

 
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()
+
get_id(self)
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)
get_id(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 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()
+
get_id(self)
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 Fixedpoint(Z3PPObject)
    Fixedpoint API provides methods for solving with recursive predicates
 
  Methods defined here:
__del__(self)
__init__(self, fixedpoint=None, ctx=None)
__repr__(self)
Return a formatted string with all added rules and constraints.
abstract(self, fml, is_forall=True)
add(self, *args)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
add_cover(self, level, predicate, property)
Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)
add_rule(self, head, body=None, name=None)
Assert rules defining recursive predicates to the fixedpoint solver.
>>> a = Bool('a')
>>> b = Bool('b')
>>> s = Fixedpoint()
>>> s.register_relation(a.decl())
>>> s.register_relation(b.decl())
>>> s.fact(a)
>>> s.rule(b, a)
>>> s.query(b)
sat
append(self, *args)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
assert_exprs(self, *args)
Assert constraints as background axioms for the fixedpoint solver.
declare_var(self, *vars)
Add variable or several variables.
The added variable or variables will be bound in the rules
and queries
fact(self, head, name=None)
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.
get_answer(self)
Retrieve answer from last query call.
get_assertions(self)
retrieve assertions that have been added to fixedpoint context
get_cover_delta(self, level, predicate)
Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)
get_num_levels(self, predicate)
Retrieve number of levels used for predicate in PDR engine
get_rules(self)
retrieve rules that have been added to fixedpoint context
help(self)
Display a string describing all available options.
insert(self, *args)
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
param_descrs(self)
Return the parameter description set.
parse_file(self, f)
Parse rules and queries from a file
parse_string(self, s)
Parse rules and queries from a string
pop(self)
restore to previously created backtracking point
push(self)
create a backtracking point for added rules, facts and assertions
query(self, *query)
Query the fixedpoint engine whether formula is derivable.
You can also pass an tuple or list of recursive predicates.
reason_unknown(self)
Return a string describing why the last `query()` returned `unknown`.
register_relation(self, *relations)
Register relation as recursive
rule(self, head, body=None, name=None)
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.
set(self, *args, **keys)
Set a configuration option. The method `help()` return a string containing all available options.
set_predicate_representation(self, f, *representations)
Control how relation is represented
sexpr(self)
Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
statistics(self)
Return statistics for the last `query()`.
to_string(self, queries)
Return a formatted string (in Lisp-like format) with all added constraints.
We say the string is in s-expression format.
Include also queries.
update_rule(self, head, body, name)
update rule

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)
as_func_decl(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
get_id(self)
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.
Return None if Z3 did not specify the `else` value for
this object.
 
>>> 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 Goal(Z3PPObject)
    Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible).
 
Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
A goal has a solution if one of its subgoals has a solution.
A goal is unsatisfiable if all subgoals are unsatisfiable.
 
  Methods defined here:
__del__(self)
__getitem__(self, arg)
Return a constraint in the goal `self`.
 
>>> g = Goal()
>>> x, y = Ints('x y')
>>> g.add(x == 0, y > x)
>>> g[0]
x == 0
>>> g[1]
y > x
__init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None)
__len__(self)
Return the number of constraints in the goal `self`.
 
>>> g = Goal()
>>> len(g)
0
>>> x, y = Ints('x y')
>>> g.add(x == 0, y > x)
>>> len(g)
2
__repr__(self)
add(self, *args)
Add constraints.
 
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0, x < 2)
>>> g
[x > 0, x < 2]
append(self, *args)
Add constraints.
 
>>> x = Int('x')
>>> g = Goal()
>>> g.append(x > 0, x < 2)
>>> g
[x > 0, x < 2]
as_expr(self)
Return goal `self` as a single Z3 expression.
 
>>> x = Int('x')
>>> g = Goal()
>>> g.as_expr()
True
>>> g.add(x > 1)
>>> g.as_expr()
x > 1
>>> g.add(x < 10)
>>> g.as_expr()
And(x > 1, x < 10)
assert_exprs(self, *args)
Assert constraints into the goal.
 
>>> x = Int('x')
>>> g = Goal()
>>> g.assert_exprs(x > 0, x < 2)
>>> g
[x > 0, x < 2]
depth(self)
Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
 
>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.add(x == 0, y >= x + 1)
>>> g.depth()
0
>>> r = Then('simplify', 'solve-eqs')(g)
>>> # r has 1 subgoal
>>> len(r)
1
>>> r[0].depth()
2
get(self, i)
Return a constraint in the goal `self`.
 
>>> g = Goal()
>>> x, y = Ints('x y')
>>> g.add(x == 0, y > x)
>>> g.get(0)
x == 0
>>> g.get(1)
y > x
inconsistent(self)
Return `True` if `self` contains the `False` constraints.
 
>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.inconsistent()
False
>>> g.add(x == 0, x == 1)
>>> g 
[x == 0, x == 1]
>>> g.inconsistent()
False
>>> g2 = Tactic('propagate-values')(g)[0]
>>> g2.inconsistent()
True
insert(self, *args)
Add constraints.
 
>>> x = Int('x')
>>> g = Goal()
>>> g.insert(x > 0, x < 2)
>>> g
[x > 0, x < 2]
prec(self)
Return the precision (under-approximation, over-approximation, or precise) of the goal `self`.
 
>>> g = Goal()
>>> g.prec() == Z3_GOAL_PRECISE
True
>>> x, y = Ints('x y')
>>> g.add(x == y + 1)
>>> g.prec() == Z3_GOAL_PRECISE
True
>>> t  = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10)
>>> g2 = t(g)[0]
>>> g2
[x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
>>> g2.prec() == Z3_GOAL_PRECISE
False
>>> g2.prec() == Z3_GOAL_UNDER
True
precision(self)
Alias for `prec()`.
 
>>> g = Goal()
>>> g.precision() == Z3_GOAL_PRECISE
True
sexpr(self)
Return a textual representation of the s-expression representing the goal.
simplify(self, *arguments, **keywords)
Return a new simplified goal.
 
This method is essentially invoking the simplify tactic.
 
>>> g = Goal()
>>> x = Int('x')
>>> g.add(x + 1 >= 2)
>>> g
[x + 1 >= 2]
>>> g2 = g.simplify()
>>> g2
[x >= 1]
>>> # g was not modified
>>> g
[x + 1 >= 2]
size(self)
Return the number of constraints in the goal `self`.
 
>>> g = Goal()
>>> g.size()
0
>>> x, y = Ints('x y')
>>> g.add(x == 0, y > x)
>>> g.size()
2
translate(self, target)
Copy goal `self` to context `target`.
 
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 10)
>>> g
[x > 10]
>>> c2 = Context()
>>> g2 = g.translate(c2)
>>> g2
[x > 10]
>>> g.ctx == main_ctx()
True
>>> g2.ctx == c2
True
>>> g2.ctx == main_ctx()
False

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
2
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()
+
get_id(self)
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 ModelRef(Z3PPObject)
    Model/Solution of a satisfiability problem (aka system of constraints).
 
  Methods defined here:
__del__(self)
__getitem__(self, idx)
If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpreation is returned.
 
The elements can be retrieved using position or the actual declaration.
 
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2, f(x) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> len(m)
2
>>> m[0]
x
>>> m[1]
f
>>> m[x]
1
>>> m[f]
[1 -> 0, else -> 0]
>>> for d in m: print("%s -> %s" % (d, m[d]))
x -> 1
f -> [1 -> 0, else -> 0]
__init__(self, m, ctx)
__len__(self)
Return the number of constant and function declarations in the model `self`.
 
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, f(x) != x)
>>> s.check()
sat
>>> m = s.model()
>>> len(m)
2
__repr__(self)
decls(self)
Return a list with all symbols that have an interpreation in the model `self`.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2, f(x) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m.decls()
[x, f]
eval(self, t, model_completion=False)
Evaluate the expression `t` in the model `self`. If `model_completion` is enabled, then a default interpretation is automatically added for symbols that do not have an interpretation in the model `self`.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> m = s.model()
>>> m.eval(x + 1)
2
>>> m.eval(x == 1)
True
>>> y = Int('y')
>>> m.eval(y + x)
1 + y
>>> m.eval(y)
y
>>> m.eval(y, model_completion=True)
0
>>> # Now, m contains an interpretation for y
>>> m.eval(y + x)
1
evaluate(self, t, model_completion=False)
Alias for `eval`.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> m = s.model()
>>> m.evaluate(x + 1)
2
>>> m.evaluate(x == 1)
True
>>> y = Int('y')
>>> m.evaluate(y + x)
1 + y
>>> m.evaluate(y)
y
>>> m.evaluate(y, model_completion=True)
0
>>> # Now, m contains an interpretation for y
>>> m.evaluate(y + x)
1
get_interp(self, decl)
Return the interpretation for a given declaration or constant.
 
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2, f(x) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[x]
1
>>> m[f]
[1 -> 0, else -> 0]
get_sort(self, idx)
Return the unintepreted sort at position `idx` < num_sorts().
 
>>> A = DeclareSort('A')
>>> B = DeclareSort('B')
>>> a1, a2 = Consts('a1 a2', A)
>>> b1, b2 = Consts('b1 b2', B)
>>> s = Solver()
>>> s.add(a1 != a2, b1 != b2)
>>> s.check()
sat
>>> m = s.model()
>>> m.num_sorts()
2
>>> m.get_sort(0)
A
>>> m.get_sort(1)
B
get_universe(self, s)
Return the intepretation for the uninterpreted sort `s` in the model `self`.
 
>>> A = DeclareSort('A')
>>> a, b = Consts('a b', A)
>>> s = Solver()
>>> s.add(a != b)
>>> s.check()
sat
>>> m = s.model()
>>> m.get_universe(A)
[A!val!0, A!val!1]
num_sorts(self)
Return the number of unintepreted sorts that contain an interpretation in the model `self`.
 
>>> A = DeclareSort('A')
>>> a, b = Consts('a b', A)
>>> s = Solver()
>>> s.add(a != b)
>>> s.check()
sat
>>> m = s.model()
>>> m.num_sorts()
1
sexpr(self)
Return a textual representation of the s-expression representing the model.
sorts(self)
Return all uninterpreted sorts that have an interpretation in the model `self`.
 
>>> A = DeclareSort('A')
>>> B = DeclareSort('B')
>>> a1, a2 = Consts('a1 a2', A)
>>> b1, b2 = Consts('b1 b2', B)
>>> s = Solver()
>>> s.add(a1 != a2, b1 != b2)
>>> s.check()
sat
>>> m = s.model()
>>> m.sorts()
[A, B]

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`.
__repr__(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)
get_id(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 Probe
    Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used.
 
  Methods defined here:
__call__(self, goal)
Evaluate the probe `self` in the given goal.
 
>>> p = Probe('size')
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
2.0
>>> g.add(x < 20)
>>> p(g)
3.0
>>> p = Probe('num-consts')
>>> p(g)
1.0
>>> p = Probe('is-propositional')
>>> p(g)
0.0
>>> p = Probe('is-qflia')
>>> p(g)
1.0
__del__(self)
__eq__(self, other)
Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`.
 
>>> p = Probe('size') == 2
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
1.0
__ge__(self, other)
Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`.
 
>>> p = Probe('size') >= 2
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
1.0
__gt__(self, other)
Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`.
 
>>> p = Probe('size') > 10
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
0.0
__init__(self, probe, ctx=None)
__le__(self, other)
Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`.
 
>>> p = Probe('size') <= 2
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
1.0
__lt__(self, other)
Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`.
 
>>> p = Probe('size') < 10
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
1.0
__ne__(self, other)
Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`.
 
>>> p = Probe('size') != 2
>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(x < 10)
>>> p(g)
0.0

 
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]
get_id(self)
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_fraction(self)
Return a Z3 rational as a Python Fraction object.
 
>>> v = RealVal("1/5")
>>> v.as_fraction()
Fraction(1, 5)
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()
3
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 == 10000000001
True

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()
+
get_id(self)
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)

 
class Solver(Z3PPObject)
    Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc.
 
  Methods defined here:
__del__(self)
__init__(self, solver=None, ctx=None)
__repr__(self)
Return a formatted string with all added constraints.
add(self, *args)
Assert constraints into the solver.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s
[x > 0, x < 2]
append(self, *args)
Assert constraints into the solver.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.append(x > 0, x < 2)
>>> s
[x > 0, x < 2]
assert_and_track(self, a, p)
Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
 
If `p` is a string, it will be automatically converted into a Boolean constant.
 
>>> x = Int('x')
>>> p3 = Bool('p3')
>>> s = Solver()
>>> s.set(unsat_core=True)
>>> s.assert_and_track(x > 0,  'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0,  p3)
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True
assert_exprs(self, *args)
Assert constraints into the solver.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.assert_exprs(x > 0, x < 2)
>>> s
[x > 0, x < 2]
assertions(self)
Return an AST vector containing all added constraints.
 
>>> s = Solver()
>>> s.assertions()
[]
>>> a = Int('a')
>>> s.add(a > 0)
>>> s.add(a < 10)
>>> s.assertions()
[a > 0, a < 10]
check(self, *assumptions)
Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.check()
sat
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> s.model()
[x = 1]
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown
help(self)
Display a string describing all available options.
insert(self, *args)
Assert constraints into the solver.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.insert(x > 0, x < 2)
>>> s
[x > 0, x < 2]
model(self)
Return a model for the last `check()`. 
 
This function raises an exception if 
a model is not available (e.g., last `check()` returned unsat).
 
>>> s = Solver()
>>> a = Int('a')
>>> s.add(a + 2 == 0)
>>> s.check()
sat
>>> s.model()
[a = -2]
param_descrs(self)
Return the parameter description set.
pop(self, num=1)
Backtrack \c num backtracking points.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]
proof(self)
Return a proof for the last `check()`. Proof construction must be enabled.
push(self)
Create a backtracking point.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]
reason_unknown(self)
Return a string describing why the last `check()` returned `unknown`.
 
>>> x = Int('x')
>>> s = SimpleSolver()
>>> s.add(2**x == 4)
>>> s.check()
unknown
>>> s.reason_unknown()
'(incomplete (theory arithmetic))'
reset(self)
Remove all asserted constraints and backtracking points created using `push()`.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.reset()
>>> s
[]
set(self, *args, **keys)
Set a configuration option. The method `help()` return a string containing all available options.
 
>>> s = Solver()
>>> # The option MBQI can be set using three different approaches.
>>> s.set(mbqi=True)
>>> s.set('MBQI', True)
>>> s.set(':mbqi', True)
sexpr(self)
Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
 
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> r = s.sexpr()
statistics(self)
Return statistics for the last `check()`.
 
>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> st.get_key_value('final checks')
1
>>> len(st) > 0
True
>>> st[0] != 0
True
to_smt2(self)
return SMTLIB2 formatted benchmark for solver's assertions
unsat_core(self)
Return a subset (as an AST vector) of the assumptions provided to the last check().
 
These are the assumptions Z3 used in the unsatisfiability proof.
Assumptions are available in Z3. They are used to extract unsatisfiable cores. 
They may be also used to "retract" assumptions. Note that, assumptions are not really 
"soft constraints", but they can be used to implement them. 
 
>>> p1, p2, p3 = Bools('p1 p2 p3')
>>> x, y       = Ints('x y')
>>> s          = Solver()
>>> s.add(Implies(p1, x > 0))
>>> s.add(Implies(p2, y > x))
>>> s.add(Implies(p2, y < 1))
>>> s.add(Implies(p3, y > -3))
>>> s.check(p1, p2, p3)
unsat
>>> core = s.unsat_core()
>>> len(core)
2
>>> p1 in core
True
>>> p2 in core
True
>>> p3 in core
False
>>> # "Retracting" p2
>>> s.check(p1, p3)
sat

Methods inherited from Z3PPObject:
use_pp(self)

 
class SortRef(AstRef)
    A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.
 
 
Method resolution order:
SortRef
AstRef
Z3PPObject

Methods defined here:
__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)
get_id(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 Statistics
    Statistics for `Solver.check()`.
 
  Methods defined here:
__del__(self)
__getattr__(self, name)
Access the value of statistical using attributes.
 
Remark: to access a counter containing blank spaces (e.g., 'nlsat propagations'),
we should use '_' (e.g., 'nlsat_propagations').
 
>>> x = Int('x') 
>>> s = Then('simplify', 'nlsat').solver()
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics() 
>>> st.keys()
['nlsat propagations', 'nlsat stages']
>>> st.nlsat_propagations
2
>>> st.nlsat_stages
2
__getitem__(self, idx)
Return the value of statistical counter at position `idx`. The result is a pair (key, value).
 
>>> x = Int('x') 
>>> s = Then('simplify', 'nlsat').solver()
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> len(st)
2
>>> st[0]
('nlsat propagations', 2)
>>> st[1]
('nlsat stages', 2)
__init__(self, stats, ctx)
__len__(self)
Return the number of statistical counters. 
 
>>> x = Int('x') 
>>> s = Then('simplify', 'nlsat').solver()
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> len(st)
2
__repr__(self)
get_key_value(self, key)
Return the value of a particular statistical counter.
 
>>> x = Int('x') 
>>> s = Then('simplify', 'nlsat').solver()
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> st.get_key_value('nlsat propagations')
2
keys(self)
Return the list of statistical counters.
 
>>> x = Int('x') 
>>> s = Then('simplify', 'nlsat').solver()
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> st.keys()
['nlsat propagations', 'nlsat stages']

 
class Tactic
    Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver().
 
Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond().
 
  Methods defined here:
__call__(self, goal, *arguments, **keywords)
Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
 
>>> x, y = Ints('x y')
>>> t = Tactic('solve-eqs')
>>> t(And(x == 0, y >= x + 1))
[[y >= 1]]
__del__(self)
__init__(self, tactic, ctx=None)
apply(self, goal, *arguments, **keywords)
Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
 
>>> x, y = Ints('x y')
>>> t = Tactic('solve-eqs')
>>> t.apply(And(x == 0, y >= x + 1))
[[y >= 1]]
help(self)
Display a string containing a description of the available options for the `self` tactic.
param_descrs(self)
Return the parameter description set.
solver(self)
Create a solver using the tactic `self`.
 
The solver supports the methods `push()` and `pop()`, but it
will always solve each `check()` from scratch.
 
>>> t = Then('simplify', 'nlsat')
>>> s = t.solver()
>>> x = Real('x')
>>> s.add(x**2 == 2, x > 0)
>>> s.check()
sat
>>> s.model()
[x = 1.4142135623?]

 
class Z3PPObject
    Superclass for all Z3 objects that have support for pretty printing.
 
  Methods defined here:
use_pp(self)

 
Functions
       
And(*args)
Create a Z3 and-expression or and-probe. 
 
>>> p, q, r = Bools('p q r')
>>> And(p, q, r)
And(p, q, r)
>>> P = BoolVector('p', 5)
>>> And(P)
And(p__0, p__1, p__2, p__3, p__4)
AndThen(*ts, **ks)
Return a tactic that applies the tactics in `*ts` in sequence.
 
>>> x, y = Ints('x y')
>>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
>>> t(And(x == 0, y > x + 1))
[[Not(y <= 1)]]
>>> t(And(x == 0, y > x + 1)).as_expr()
Not(y <= 1)
Array(name, dom, rng)
Return an array constant named `name` with the given domain and range sorts.
 
>>> a = Array('a', IntSort(), IntSort())
>>> a.sort()
Array(Int, Int)
>>> a[0]
a[0]
ArraySort(d, r)
Return the Z3 array sort with the given domain and range sorts.
 
>>> A = ArraySort(IntSort(), BoolSort())
>>> A
Array(Int, Bool)
>>> A.domain()
Int
>>> A.range()
Bool
>>> AA = ArraySort(IntSort(), A)
>>> AA
Array(Int, Array(Int, Bool))
BV2Int(a)
Return the Z3 expression BV2Int(a). 
 
>>> b = BitVec('b', 3)
>>> BV2Int(b).sort()
Int
>>> x = Int('x')
>>> x > BV2Int(b)
x > BV2Int(b)
>>> solve(x > BV2Int(b), b == 1, x < 3)
[b = 1, x = 2]
BitVec(name, bv, ctx=None)
Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
If `ctx=None`, then the global context is used.
 
>>> x  = BitVec('x', 16)
>>> is_bv(x)
True
>>> x.size()
16
>>> x.sort()
BitVec(16)
>>> word = BitVecSort(16)
>>> x2 = BitVec('x', word)
>>> eq(x, x2)
True
BitVecSort(sz, ctx=None)
Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
 
>>> Byte = BitVecSort(8)
>>> Word = BitVecSort(16)
>>> Byte
BitVec(8)
>>> x = Const('x', Byte)
>>> eq(x, BitVec('x', 8))
True
BitVecVal(val, bv, ctx=None)
Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
 
>>> v = BitVecVal(10, 32)
>>> v
10
>>> print("0x%.8x" % v.as_long())
0x0000000a
BitVecs(names, bv, ctx=None)
Return a tuple of bit-vector constants of size bv. 
 
>>> x, y, z = BitVecs('x y z', 16)
>>> x.size()
16
>>> x.sort()
BitVec(16)
>>> Sum(x, y, z)
0 + x + y + z
>>> Product(x, y, z)
1*x*y*z
>>> simplify(Product(x, y, z))
x*y*z
Bool(name, ctx=None)
Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
 
>>> p = Bool('p')
>>> q = Bool('q')
>>> And(p, q)
And(p, q)
BoolSort(ctx=None)
Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
 
>>> BoolSort()
Bool
>>> p = Const('p', BoolSort())
>>> is_bool(p)
True
>>> r = Function('r', IntSort(), IntSort(), BoolSort())
>>> r(0, 1)
r(0, 1)
>>> is_bool(r(0, 1))
True
BoolVal(val, ctx=None)
Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
 
>>> BoolVal(True)
True
>>> is_true(BoolVal(True))
True
>>> is_true(True)
False
>>> is_false(BoolVal(False))
True
BoolVector(prefix, sz, ctx=None)
Return a list of Boolean constants of size `sz`.
 
The constants are named using the given prefix.
If `ctx=None`, then the global context is used.
 
>>> P = BoolVector('p', 3)
>>> P
[p__0, p__1, p__2]
>>> And(P)
And(p__0, p__1, p__2)
Bools(names, ctx=None)
Return a tuple of Boolean constants. 
 
`names` is a single string containing all names separated by blank spaces. 
If `ctx=None`, then the global context is used.
 
>>> p, q, r = Bools('p q r')
>>> And(p, Or(q, r))
And(p, Or(q, r))
Cbrt(a, ctx=None)
Return a Z3 expression which represents the cubic root of a. 
 
>>> x = Real('x')
>>> Cbrt(x)
x**(1/3)
Concat(*args)
Create a Z3 bit-vector concatenation expression. 
 
>>> v = BitVecVal(1, 4)
>>> Concat(v, v+1, v)
Concat(Concat(1, 1 + 1), 1)
>>> simplify(Concat(v, v+1, v))
289
>>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
121
Cond(p, t1, t2, ctx=None)
Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
 
>>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
Const(name, sort)
Create a constant of the given sort.
 
>>> Const('x', IntSort())
x
Consts(names, sort)
Create a several constants of the given sort. 
 
`names` is a string containing the names of all constants to be created. 
Blank spaces separate the names of different constants.
 
>>> x, y, z = Consts('x y z', IntSort())
>>> x + y + z
x + y + z
CreateDatatypes(*ds)
Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
 
In the following example we define a Tree-List using two mutually recursive datatypes.
 
>>> TreeList = Datatype('TreeList')
>>> Tree     = Datatype('Tree')
>>> # Tree has two constructors: leaf and node
>>> Tree.declare('leaf', ('val', IntSort()))
>>> # a node contains a list of trees
>>> Tree.declare('node', ('children', TreeList))
>>> TreeList.declare('nil')
>>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
>>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
>>> Tree.val(Tree.leaf(10))
val(leaf(10))
>>> simplify(Tree.val(Tree.leaf(10)))
10
>>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
>>> n1
node(cons(leaf(10), cons(leaf(20), nil)))
>>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
>>> simplify(n2 == n1)
False
>>> simplify(TreeList.car(Tree.children(n2)) == n1)
True
DeclareSort(name, ctx=None)
Create a new uninterpred sort named `name`.
 
If `ctx=None`, then the new sort is declared in the global Z3Py context.
 
>>> A = DeclareSort('A')
>>> a = Const('a', A)
>>> b = Const('b', A)
>>> a.sort() == A
True
>>> b.sort() == A
True
>>> a == b
a == b
Distinct(*args)
Create a Z3 distinct expression. 
 
>>> x = Int('x')
>>> y = Int('y')
>>> Distinct(x, y)
x != y
>>> z = Int('z')
>>> Distinct(x, y, z)
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z))
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z), blast_distinct=True)
And(Not(x == y), Not(x == z), Not(y == z))
EnumSort(name, values, ctx=None)
Return a new enumeration sort named `name` containing the given values.
 
The result is a pair (sort, list of constants).
Example:
    >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
Exists(vs, body, weight=1, qid='', skid='', patterns=[], no_patterns=[])
Create a Z3 exists formula.
 
The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
 
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
 
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> q = Exists([x, y], f(x, y) >= x, skid="foo")
>>> q
Exists([x, y], f(x, y) >= x)
>>> is_quantifier(q)
True
>>> r = Tactic('nnf')(q).as_expr()
>>> is_quantifier(r)
False
Extract(high, low, a)
Create a Z3 bit-vector extraction expression.
 
>>> x = BitVec('x', 8)
>>> Extract(6, 2, x)
Extract(6, 2, x)
>>> Extract(6, 2, x).sort()
BitVec(5)
FailIf(p, ctx=None)
Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
 
In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
 
>>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(y > 0)
>>> t(g)
[[x > 0, y > 0]]
>>> g.add(x == y + 1)
>>> t(g)
[[Not(x <= 0), Not(y <= 0), x == 1 + y]]
ForAll(vs, body, weight=1, qid='', skid='', patterns=[], no_patterns=[])
Create a Z3 forall formula.
 
The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
 
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
 
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> ForAll([x, y], f(x, y) >= x)
ForAll([x, y], f(x, y) >= x)
>>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
ForAll([x, y], f(x, y) >= x)
>>> ForAll([x, y], f(x, y) >= x, weight=10)
ForAll([x, y], f(x, y) >= x)
FreshBool(prefix='b', ctx=None)
Return a fresh Boolean constant in the given context using the given prefix.
 
If `ctx=None`, then the global context is used.    
 
>>> b1 = FreshBool()
>>> b2 = FreshBool()
>>> eq(b1, b2)
False
FreshInt(prefix='x', ctx=None)
Return a fresh integer constant in the given context using the given prefix.
 
>>> x = FreshInt()
>>> y = FreshInt()
>>> eq(x, y)
False
>>> x.sort()
Int
FreshReal(prefix='b', ctx=None)
Return a fresh real constant in the given context using the given prefix.
 
>>> x = FreshReal()
>>> y = FreshReal()
>>> eq(x, y)
False
>>> x.sort()
Real
Function(name, *sig)
Create a new Z3 uninterpreted function with the given sorts. 
 
>>> f = Function('f', IntSort(), IntSort())
>>> f(f(0))
f(f(0))
If(a, b, c, ctx=None)
Create a Z3 if-then-else expression. 
 
>>> x = Int('x')
>>> y = Int('y')
>>> max = If(x > y, x, y)
>>> max
If(x > y, x, y)
>>> simplify(max)
If(x <= y, y, x)
Implies(a, b, ctx=None)
Create a Z3 implies expression. 
 
>>> p, q = Bools('p q')
>>> Implies(p, q)
Implies(p, q)
>>> simplify(Implies(p, q))
Or(Not(p), q)
Int(name, ctx=None)
Return an integer constant named `name`. If `ctx=None`, then the global context is used.
 
>>> x = Int('x')
>>> is_int(x)
True
>>> is_int(x + 1)
True
IntSort(ctx=None)
Return the interger sort in the given context. If `ctx=None`, then the global context is used.
 
>>> IntSort()
Int
>>> x = Const('x', IntSort())
>>> is_int(x)
True
>>> x.sort() == IntSort()
True
>>> x.sort() == BoolSort()
False
IntVal(val, ctx=None)
Return a Z3 integer value. If `ctx=None`, then the global context is used.
 
>>> IntVal(1)
1
>>> IntVal("100")
100
IntVector(prefix, sz, ctx=None)
Return a list of integer constants of size `sz`.
 
>>> X = IntVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2
Interpolant(a, ctx=None)
Create an interpolation operator.
 
The argument is an interpolation pattern (see tree_interpolant). 
 
>>> x = Int('x')
>>> print Interpolant(x>0)
interp(x > 0)
Ints(names, ctx=None)
Return a tuple of Integer constants. 
 
>>> x, y, z = Ints('x y z')
>>> Sum(x, y, z)
x + y + z
IsInt(a)
Return the Z3 predicate IsInt(a). 
 
>>> x = Real('x')
>>> IsInt(x + "1/2")
IsInt(x + 1/2)
>>> solve(IsInt(x + "1/2"), x > 0, x < 1)
[x = 1/2]
>>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
no solution
K(dom, v)
Return a Z3 constant array expression. 
 
>>> a = K(IntSort(), 10)
>>> a
K(Int, 10)
>>> a.sort()
Array(Int, Int)
>>> i = Int('i')
>>> a[i]
K(Int, 10)[i]
>>> simplify(a[i])
10
LShR(a, b)
Create the Z3 expression logical right shift.
 
Use the operator >> for the arithmetical right shift.
 
>>> x, y = BitVecs('x y', 32)
>>> LShR(x, y)
LShR(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()
-4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2
>>> 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
Map(f, *args)
Return a Z3 map array expression. 
 
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> a1 = Array('a1', IntSort(), IntSort())
>>> a2 = Array('a2', IntSort(), IntSort())
>>> b  = Map(f, a1, a2)
>>> b
Map(f, a1, a2)
>>> prove(b[0] == f(a1[0], a2[0]))
proved
MultiPattern(*args)
Create a Z3 multi-pattern using the given expressions `*args`
 
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
 
>>> f = Function('f', IntSort(), IntSort())
>>> g = Function('g', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
>>> q
ForAll(x, f(x) != g(x))
>>> q.num_patterns()
1
>>> is_pattern(q.pattern(0))
True
>>> q.pattern(0)
MultiPattern(f(Var(0)), g(Var(0)))
Not(a, ctx=None)
Create a Z3 not expression or probe. 
 
>>> p = Bool('p')
>>> Not(Not(p))
Not(Not(p))
>>> simplify(Not(Not(p)))
p
Or(*args)
Create a Z3 or-expression or or-probe. 
 
>>> p, q, r = Bools('p q r')
>>> Or(p, q, r)
Or(p, q, r)
>>> P = BoolVector('p', 5)
>>> Or(P)
Or(p__0, p__1, p__2, p__3, p__4)
OrElse(*ts, **ks)
Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
 
>>> x = Int('x')
>>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
>>> # Tactic split-clause fails if there is no clause in the given goal.
>>> t(x == 0)
[[x == 0]]
>>> t(Or(x == 0, x == 1))
[[x == 0], [x == 1]]
ParAndThen(t1, t2, ctx=None)
Alias for ParThen(t1, t2, ctx).
ParOr(*ts, **ks)
Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
 
>>> x = Int('x')
>>> t = ParOr(Tactic('simplify'), Tactic('fail'))
>>> t(x + 1 == 2)
[[x == 1]]
ParThen(t1, t2, ctx=None)
Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
 
>>> x, y = Ints('x y')
>>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
>>> t(And(Or(x == 1, x == 2), y == x + 1))
[[x == 1, y == 2], [x == 2, y == 3]]
Product(*args)
Create the product of the Z3 expressions. 
 
>>> a, b, c = Ints('a b c')
>>> Product(a, b, c)
a*b*c
>>> Product([a, b, c])
a*b*c
>>> A = IntVector('a', 5)
>>> Product(A)
a__0*a__1*a__2*a__3*a__4
Q(a, b, ctx=None)
Return a Z3 rational a/b.
 
If `ctx=None`, then the global context is used.
 
>>> Q(3,5)
3/5
>>> Q(3,5).sort()
Real
RatVal(a, b, ctx=None)
Return a Z3 rational a/b.
 
If `ctx=None`, then the global context is used.
 
>>> RatVal(3,5)
3/5
>>> RatVal(3,5).sort()
Real
Real(name, ctx=None)
Return a real constant named `name`. If `ctx=None`, then the global context is used.
 
>>> x = Real('x')
>>> is_real(x)
True
>>> is_real(x + 1)
True
RealSort(ctx=None)
Return the real sort in the given context. If `ctx=None`, then the global context is used.
 
>>> RealSort()
Real
>>> x = Const('x', RealSort())
>>> is_real(x)
True
>>> is_int(x)
False
>>> x.sort() == RealSort()
True
RealVal(val, ctx=None)
Return a Z3 real value. 
 
`val` may be a Python int, long, float or string representing a number in decimal or rational notation.
If `ctx=None`, then the global context is used.
 
>>> RealVal(1)
1
>>> RealVal(1).sort()
Real
>>> RealVal("3/5")
3/5
>>> RealVal("1.5")
3/2
RealVar(idx, ctx=None)
Create a real free variable. Free variables are used to create quantified formulas.
They are also used to create polynomials.
 
>>> RealVar(0)
Var(0)
RealVarVector(n, ctx=None)
Create a list of Real free variables.
The variables have ids: 0, 1, ..., n-1
 
>>> x0, x1, x2, x3 = RealVarVector(4)
>>> x2
Var(2)
RealVector(prefix, sz, ctx=None)
Return a list of real constants of size `sz`.
 
>>> X = RealVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2
>>> Sum(X).sort()
Real
Reals(names, ctx=None)
Return a tuple of real constants. 
 
>>> x, y, z = Reals('x y z')
>>> Sum(x, y, z)
x + y + z
>>> Sum(x, y, z).sort()
Real
Repeat(t, max=4294967295L, ctx=None)
Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
 
>>> x, y = Ints('x y')
>>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
>>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
>>> r = t(c)
>>> for subgoal in r: print(subgoal)
[x == 0, y == 0, x > y]
[x == 0, y == 1, x > y]
[x == 1, y == 0, x > y]
[x == 1, y == 1, x > y]
>>> t = Then(t, Tactic('propagate-values'))
>>> t(c)
[[x == 1, y == 0]]
RepeatBitVec(n, a)
Return an expression representing `n` copies of `a`.
 
>>> x = BitVec('x', 8)
>>> n = RepeatBitVec(4, x)
>>> n
RepeatBitVec(4, x)
>>> n.size()
32
>>> v0 = BitVecVal(10, 4)
>>> print("%.x" % v0.as_long())
a
>>> v = simplify(RepeatBitVec(4, v0))
>>> v.size()
16
>>> print("%.x" % v.as_long())
aaaa
RotateLeft(a, b)
Return an expression representing `a` rotated to the left `b` times.
 
>>> a, b = BitVecs('a b', 16)
>>> RotateLeft(a, b)
RotateLeft(a, b)
>>> simplify(RotateLeft(a, 0))
a
>>> simplify(RotateLeft(a, 16))
a
RotateRight(a, b)
Return an expression representing `a` rotated to the right `b` times.
 
>>> a, b = BitVecs('a b', 16)
>>> RotateRight(a, b)
RotateRight(a, b)
>>> simplify(RotateRight(a, 0))
a
>>> simplify(RotateRight(a, 16))
a
SRem(a, b)
Create the Z3 expression signed remainder.
 
Use the operator % for signed modulus, and URem() for unsigned remainder.
 
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> SRem(x, y)
SRem(x, y)
>>> SRem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> SRem(x, y).sexpr()
'(bvsrem x y)'
Select(a, i)
Return a Z3 select array expression.
 
>>> a = Array('a', IntSort(), IntSort())
>>> i = Int('i')
>>> Select(a, i)
a[i]
>>> eq(Select(a, i), a[i])
True
SignExt(n, a)
Return a bit-vector expression with `n` extra sign-bits.
 
>>> x = BitVec('x', 16)
>>> n = SignExt(8, x)
>>> n.size()
24
>>> n
SignExt(8, x)
>>> n.sort()
BitVec(24)
>>> v0 = BitVecVal(2, 2)
>>> v0
2
>>> v0.size()
2
>>> v  = simplify(SignExt(6, v0))
>>> v
254
>>> v.size()
8
>>> print("%.x" % v.as_long())
fe
SimpleSolver(ctx=None)
Return a simple general purpose solver with limited amount of preprocessing.
 
>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat
SolverFor(logic, ctx=None)
Create a solver customized for the given logic. 
 
The parameter `logic` is a string. It should be contains
the name of a SMT-LIB logic.
See http://www.smtlib.org/ for the name of all available logics.
 
>>> s = SolverFor("QF_LIA")
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> s.check()
sat
>>> s.model()
[x = 1]
Sqrt(a, ctx=None)
Return a Z3 expression which represents the square root of a. 
 
>>> x = Real('x')
>>> Sqrt(x)
x**(1/2)
Store(a, i, v)
Return a Z3 store array expression.
 
>>> a    = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s    = Store(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j    = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved
Sum(*args)
Create the sum of the Z3 expressions. 
 
>>> a, b, c = Ints('a b c')
>>> Sum(a, b, c)
a + b + c
>>> Sum([a, b, c])
a + b + c
>>> A = IntVector('a', 5)
>>> Sum(A)
a__0 + a__1 + a__2 + a__3 + a__4
Then(*ts, **ks)
Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
 
>>> x, y = Ints('x y')
>>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
>>> t(And(x == 0, y > x + 1))
[[Not(y <= 1)]]
>>> t(And(x == 0, y > x + 1)).as_expr()
Not(y <= 1)
ToInt(a)
Return the Z3 expression ToInt(a). 
 
>>> x = Real('x')
>>> x.sort()
Real
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> n.sort()
Int
ToReal(a)
Return the Z3 expression ToReal(a). 
 
>>> x = Int('x')
>>> x.sort()
Int
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> n.sort()
Real
TryFor(t, ms, ctx=None)
Return a tactic that applies `t` to a given goal for `ms` milliseconds.
 
If `t` does not terminate in `ms` milliseconds, then it fails.
UDiv(a, b)
Create the Z3 expression (unsigned) division `self / other`.
 
Use the operator / for signed division.
 
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> UDiv(x, y)
UDiv(x, y)
>>> UDiv(x, y).sort()
BitVec(32)
>>> (x / y).sexpr()
'(bvsdiv x y)'
>>> UDiv(x, y).sexpr()
'(bvudiv x y)'
UGE(a, b)
Create the Z3 expression (unsigned) `other >= self`.
 
Use the operator >= for signed greater than or equal to.
 
>>> x, y = BitVecs('x y', 32)
>>> UGE(x, y)
UGE(x, y)
>>> (x >= y).sexpr()
'(bvsge x y)'
>>> UGE(x, y).sexpr()
'(bvuge x y)'
UGT(a, b)
Create the Z3 expression (unsigned) `other > self`.
 
Use the operator > for signed greater than.
 
>>> x, y = BitVecs('x y', 32)
>>> UGT(x, y)
UGT(x, y)
>>> (x > y).sexpr()
'(bvsgt x y)'
>>> UGT(x, y).sexpr()
'(bvugt x y)'
ULE(a, b)
Create the Z3 expression (unsigned) `other <= self`.
 
Use the operator <= for signed less than or equal to.
 
>>> x, y = BitVecs('x y', 32)
>>> ULE(x, y)
ULE(x, y)
>>> (x <= y).sexpr()
'(bvsle x y)'
>>> ULE(x, y).sexpr()
'(bvule x y)'
ULT(a, b)
Create the Z3 expression (unsigned) `other < self`.
 
Use the operator < for signed less than.
 
>>> x, y = BitVecs('x y', 32)
>>> ULT(x, y)
ULT(x, y)
>>> (x < y).sexpr()
'(bvslt x y)'
>>> ULT(x, y).sexpr()
'(bvult x y)'
URem(a, b)
Create the Z3 expression (unsigned) remainder `self % other`.
 
Use the operator % for signed modulus, and SRem() for signed remainder.
 
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> URem(x, y)
URem(x, y)
>>> URem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> URem(x, y).sexpr()
'(bvurem x y)'
Update(a, i, v)
Return a Z3 store array expression.
 
>>> a    = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s    = Update(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j    = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved
Var(idx, s)
Create a Z3 free variable. Free variables are used to create quantified formulas.
 
>>> Var(0, IntSort())
Var(0)
>>> eq(Var(0, IntSort()), Var(0, BoolSort()))
False
When(p, t, ctx=None)
Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
 
>>> t = When(Probe('size') > 2, Tactic('simplify'))
>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(y > 0)
>>> t(g)
[[x > 0, y > 0]]
>>> g.add(x == y + 1)
>>> t(g)
[[Not(x <= 0), Not(y <= 0), x == 1 + y]]
With(t, *args, **keys)
Return a tactic that applies tactic `t` using the given configuration options.
 
>>> x, y = Ints('x y')
>>> t = With(Tactic('simplify'), som=True)
>>> t((x + 1)*(y + 2) == 0)
[[2*x + y + x*y == -2]]
Xor(a, b, ctx=None)
Create a Z3 Xor expression.
 
>>> p, q = Bools('p q')
>>> Xor(p, q)
Xor(p, q)
>>> simplify(Xor(p, q))
Not(p) == q
ZeroExt(n, a)
Return a bit-vector expression with `n` extra zero-bits.
 
>>> x = BitVec('x', 16)
>>> n = ZeroExt(8, x)
>>> n.size()
24
>>> n
ZeroExt(8, x)
>>> n.sort()
BitVec(24)
>>> v0 = BitVecVal(2, 2)
>>> v0
2
>>> v0.size()
2
>>> v  = simplify(ZeroExt(6, v0))
>>> v
2
>>> v.size()
8
append_log(s)
Append user-defined string to interaction log.
args2params(arguments, keywords, ctx=None)
Convert python arguments into a Z3_params object.
A ':' is added to the keywords, and '_' is replaced with '-'
 
>>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
(params model true relevancy 2 elim_and true)
binary_interpolant(a, b, p=None, ctx=None)
Compute an interpolant for a binary conjunction.
 
If a & b is unsatisfiable, returns an interpolant for a & b.
This is a formula phi such that
 
1) a implies phi
2) b implies not phi
3) All the uninterpreted symbols of phi occur in both a and b.
 
If a & b is satisfiable, raises an object of class ModelRef
that represents a model of a &b.
 
If parameters p are supplied, these are used in creating the
solver that determines satisfiability.
 
x = Int('x')
print binary_interpolant(x<0,x>2)
Not(x >= 0)
describe_probes()
Display a (tabular) description of all available probes in Z3.
describe_tactics()
Display a (tabular) description of all available tactics in Z3.
disable_trace(msg)
enable_trace(msg)
eq(a, b)
Return `True` if `a` and `b` are structurally identical AST nodes.
 
>>> x = Int('x')
>>> y = Int('y')
>>> eq(x, y)
False
>>> eq(x + 1, x + 1)
True
>>> eq(x + 1, 1 + x)
False
>>> eq(simplify(x + 1), simplify(1 + x))
True
get_as_array_func(n)
Return the function declaration f associated with a Z3 expression of the form (_ as-array f).
get_map_func(a)
Return the function declaration associated with a Z3 map array expression.
 
>>> f = Function('f', IntSort(), IntSort())
>>> b = Array('b', IntSort(), IntSort())
>>> a  = Map(f, b)
>>> eq(f, get_map_func(a))
True
>>> get_map_func(a)
f
>>> get_map_func(a)(0)
f(0)
get_param(name)
Return the value of a Z3 global (or module) parameter
 
>>> get_param('nlsat.reorder')
'true'
get_var_index(a)
Return the de-Bruijn index of the Z3 bounded variable `a`.
 
>>> x = Int('x')
>>> y = Int('y')
>>> is_var(x)
False
>>> is_const(x)
True
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> # Z3 replaces x and y with bound variables when ForAll is executed.
>>> q = ForAll([x, y], f(x, y) == x + y)
>>> q.body()
f(Var(1), Var(0)) == Var(1) + Var(0)
>>> b = q.body()
>>> b.arg(0)
f(Var(1), Var(0))
>>> v1 = b.arg(0).arg(0)
>>> v2 = b.arg(0).arg(1)
>>> v1
Var(1)
>>> v2
Var(0)
>>> get_var_index(v1)
1
>>> get_var_index(v2)
0
get_version()
get_version_string()
help_simplify()
Return a string describing all options available for Z3 `simplify` procedure.
is_K(a)
Return `True` if `a` is a Z3 constant array.
 
>>> a = K(IntSort(), 10)
>>> is_K(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_K(a)
False
is_add(a)
Return `True` if `a` is an expression of the form b + c.
 
>>> x, y = Ints('x y')
>>> is_add(x + y)
True
>>> is_add(x - y)
False
is_algebraic_value(a)
Return `True` if `a` is an algerbraic value of sort Real.
 
>>> is_algebraic_value(RealVal("3/5"))
False
>>> n = simplify(Sqrt(2))
>>> n
1.4142135623?
>>> is_algebraic_value(n)
True
is_and(a)
Return `True` if `a` is a Z3 and expression.
 
>>> p, q = Bools('p q')
>>> is_and(And(p, q))
True
>>> is_and(Or(p, q))
False
is_app(a)
Return `True` if `a` is a Z3 function application. 
 
Note that, constants are function applications with 0 arguments. 
 
>>> a = Int('a')
>>> is_app(a)
True
>>> is_app(a + 1)
True
>>> is_app(IntSort())
False
>>> is_app(1)
False
>>> is_app(IntVal(1))
True
>>> x = Int('x')
>>> is_app(ForAll(x, x >= 0))
False
is_app_of(a, k)
Return `True` if `a` is an application of the given kind `k`. 
 
>>> x = Int('x')
>>> n = x + 1
>>> is_app_of(n, Z3_OP_ADD)
True
>>> is_app_of(n, Z3_OP_MUL)
False
is_arith(a)
Return `True` if `a` is an arithmetical expression.
 
>>> x = Int('x')
>>> is_arith(x)
True
>>> is_arith(x + 1)
True
>>> is_arith(1)
False
>>> is_arith(IntVal(1))
True
>>> y = Real('y')
>>> is_arith(y)
True
>>> is_arith(y + 1)
True
is_arith_sort(s)
Return `True` if s is an arithmetical sort (type).
 
>>> is_arith_sort(IntSort())
True
>>> is_arith_sort(RealSort())
True
>>> is_arith_sort(BoolSort())
False
>>> n = Int('x') + 1
>>> is_arith_sort(n.sort())
True
is_array(a)
Return `True` if `a` is a Z3 array expression.
 
>>> a = Array('a', IntSort(), IntSort())
>>> is_array(a)
True
>>> is_array(Store(a, 0, 1))
True
>>> is_array(a[0])
False
is_as_array(n)
Return true if n is a Z3 expression of the form (_ as-array f).
is_ast(a)
Return `True` if `a` is an AST node.
 
>>> is_ast(10)
False
>>> is_ast(IntVal(10))
True
>>> is_ast(Int('x'))
True
>>> is_ast(BoolSort())
True
>>> is_ast(Function('f', IntSort(), IntSort()))
True
>>> is_ast("x")
False
>>> is_ast(Solver())
False
is_bool(a)
Return `True` if `a` is a Z3 Boolean expression.
 
>>> p = Bool('p')
>>> is_bool(p)
True
>>> q = Bool('q')
>>> is_bool(And(p, q))
True
>>> x = Real('x')
>>> is_bool(x)
False
>>> is_bool(x == 0)
True
is_bv(a)
Return `True` if `a` is a Z3 bit-vector expression.
 
>>> b = BitVec('b', 32)
>>> is_bv(b)
True
>>> is_bv(b + 10)
True
>>> is_bv(Int('x'))
False
is_bv_sort(s)
Return True if `s` is a Z3 bit-vector sort.
 
>>> is_bv_sort(BitVecSort(32))
True
>>> is_bv_sort(IntSort())
False
is_bv_value(a)
Return `True` if `a` is a Z3 bit-vector numeral value.
 
>>> b = BitVec('b', 32)
>>> is_bv_value(b)
False
>>> b = BitVecVal(10, 32)
>>> b
10
>>> is_bv_value(b)
True
is_const(a)
Return `True` if `a` is Z3 constant/variable expression. 
 
>>> a = Int('a')
>>> is_const(a)
True
>>> is_const(a + 1)
False
>>> is_const(1)
False
>>> is_const(IntVal(1))
True
>>> x = Int('x')
>>> is_const(ForAll(x, x >= 0))
False
is_const_array(a)
Return `True` if `a` is a Z3 constant array.
 
>>> a = K(IntSort(), 10)
>>> is_const_array(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_const_array(a)
False
is_distinct(a)
Return `True` if `a` is a Z3 distinct expression.
 
>>> x, y, z = Ints('x y z')
>>> is_distinct(x == y)
False
>>> is_distinct(Distinct(x, y, z))
True
is_div(a)
Return `True` if `a` is an expression of the form b / c.
 
>>> x, y = Reals('x y')
>>> is_div(x / y)
True
>>> is_div(x + y)
False
>>> x, y = Ints('x y')
>>> is_div(x / y)
False
>>> is_idiv(x / y)
True
is_eq(a)
Return `True` if `a` is a Z3 equality expression.
 
>>> x, y = Ints('x y')
>>> is_eq(x == y)
True
is_expr(a)
Return `True` if `a` is a Z3 expression.
 
>>> a = Int('a')
>>> is_expr(a)
True
>>> is_expr(a + 1)
True
>>> is_expr(IntSort())
False
>>> is_expr(1)
False
>>> is_expr(IntVal(1))
True
>>> x = Int('x')
>>> is_expr(ForAll(x, x >= 0))
True
is_false(a)
Return `True` if `a` is the Z3 false expression.
 
>>> p = Bool('p')
>>> is_false(p)
False
>>> is_false(False)
False
>>> is_false(BoolVal(False))
True
is_func_decl(a)
Return `True` if `a` is a Z3 function declaration.
 
>>> f = Function('f', IntSort(), IntSort())
>>> is_func_decl(f)
True
>>> x = Real('x')
>>> is_func_decl(x)
False
is_ge(a)
Return `True` if `a` is an expression of the form b >= c.
 
>>> x, y = Ints('x y')
>>> is_ge(x >= y)
True
>>> is_ge(x == y)
False
is_gt(a)
Return `True` if `a` is an expression of the form b > c.
 
>>> x, y = Ints('x y')
>>> is_gt(x > y)
True
>>> is_gt(x == y)
False
is_idiv(a)
Return `True` if `a` is an expression of the form b div c.
 
>>> x, y = Ints('x y')
>>> is_idiv(x / y)
True
>>> is_idiv(x + y)
False
is_int(a)
Return `True` if `a` is an integer expression.
 
>>> x = Int('x')
>>> is_int(x + 1)
True
>>> is_int(1)
False
>>> is_int(IntVal(1))
True
>>> y = Real('y')
>>> is_int(y)
False
>>> is_int(y + 1)
False
is_int_value(a)
Return `True` if `a` is an integer value of sort Int.
 
>>> is_int_value(IntVal(1))
True
>>> is_int_value(1)
False
>>> is_int_value(Int('x'))
False
>>> n = Int('x') + 1
>>> n
x + 1
>>> n.arg(1)
1
>>> is_int_value(n.arg(1))
True
>>> is_int_value(RealVal("1/3"))
False
>>> is_int_value(RealVal(1))
False
is_is_int(a)
Return `True` if `a` is an expression of the form IsInt(b).
 
>>> x = Real('x')
>>> is_is_int(IsInt(x))
True
>>> is_is_int(x)
False
is_le(a)
Return `True` if `a` is an expression of the form b <= c.
 
>>> x, y = Ints('x y')
>>> is_le(x <= y)
True
>>> is_le(x < y)
False
is_lt(a)
Return `True` if `a` is an expression of the form b < c.
 
>>> x, y = Ints('x y')
>>> is_lt(x < y)
True
>>> is_lt(x == y)
False
is_map(a)
Return `True` if `a` is a Z3 map array expression. 
 
>>> f = Function('f', IntSort(), IntSort())
>>> b = Array('b', IntSort(), IntSort())
>>> a  = Map(f, b)
>>> a
Map(f, b)
>>> is_map(a)
True
>>> is_map(b)
False
is_mod(a)
Return `True` if `a` is an expression of the form b % c.
 
>>> x, y = Ints('x y')
>>> is_mod(x % y)
True
>>> is_mod(x + y)
False
is_mul(a)
Return `True` if `a` is an expression of the form b * c.
 
>>> x, y = Ints('x y')
>>> is_mul(x * y)
True
>>> is_mul(x - y)
False
is_not(a)
Return `True` if `a` is a Z3 not expression.
 
>>> p = Bool('p')
>>> is_not(p)
False
>>> is_not(Not(p))
True
is_or(a)
Return `True` if `a` is a Z3 or expression.
 
>>> p, q = Bools('p q')
>>> is_or(Or(p, q))
True
>>> is_or(And(p, q))
False
is_pattern(a)
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
 
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
 
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
>>> q
ForAll(x, f(x) == 0)
>>> q.num_patterns()
1
>>> is_pattern(q.pattern(0))
True
>>> q.pattern(0)
f(Var(0))
is_probe(p)
Return `True` if `p` is a Z3 probe.
 
>>> is_probe(Int('x'))
False
>>> is_probe(Probe('memory'))
True
is_quantifier(a)
Return `True` if `a` is a Z3 quantifier.
 
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> is_quantifier(q)
True
>>> is_quantifier(f(x))
False
is_rational_value(a)
Return `True` if `a` is rational value of sort Real.
 
>>> is_rational_value(RealVal(1))
True
>>> is_rational_value(RealVal("3/5"))
True
>>> is_rational_value(IntVal(1))
False
>>> is_rational_value(1)
False
>>> n = Real('x') + 1
>>> n.arg(1)
1
>>> is_rational_value(n.arg(1))
True
>>> is_rational_value(Real('x'))
False
is_real(a)
Return `True` if `a` is a real expression.
 
>>> x = Int('x')
>>> is_real(x + 1)
False
>>> y = Real('y')
>>> is_real(y)
True
>>> is_real(y + 1)
True
>>> is_real(1)
False
>>> is_real(RealVal(1))
True
is_select(a)
Return `True` if `a` is a Z3 array select application.
 
>>> a = Array('a', IntSort(), IntSort())
>>> is_select(a)
False
>>> i = Int('i')
>>> is_select(a[i])
True
is_sort(s)
Return `True` if `s` is a Z3 sort.
 
>>> is_sort(IntSort())
True
>>> is_sort(Int('x'))
False
>>> is_expr(Int('x'))
True
is_store(a)
Return `True` if `a` is a Z3 array store application.
 
>>> a = Array('a', IntSort(), IntSort())
>>> is_store(a)
False
>>> is_store(Store(a, 0, 1))
True
is_sub(a)
Return `True` if `a` is an expression of the form b - c.
 
>>> x, y = Ints('x y')
>>> is_sub(x - y)
True
>>> is_sub(x + y)
False
is_to_int(a)
Return `True` if `a` is an expression of the form ToInt(b).
 
>>> x = Real('x')
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> is_to_int(n)
True
>>> is_to_int(x)
False
is_to_real(a)
Return `True` if `a` is an expression of the form ToReal(b).
 
>>> x = Int('x')
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> is_to_real(n)
True
>>> is_to_real(x)
False
is_true(a)
Return `True` if `a` is the Z3 true expression.
 
>>> p = Bool('p')
>>> is_true(p)
False
>>> is_true(simplify(p == p))
True
>>> x = Real('x')
>>> is_true(x == 0)
False
>>> # True is a Python Boolean expression
>>> is_true(True)
False
is_var(a)
Return `True` if `a` is variable. 
 
Z3 uses de-Bruijn indices for representing bound variables in
quantifiers.
 
>>> x = Int('x')
>>> is_var(x)
False
>>> is_const(x)
True
>>> f = Function('f', IntSort(), IntSort())
>>> # Z3 replaces x with bound variables when ForAll is executed.
>>> q = ForAll(x, f(x) == x)
>>> b = q.body()
>>> b
f(Var(0)) == Var(0)
>>> b.arg(1)
Var(0)
>>> is_var(b.arg(1))
True
main_ctx()
Return a reference to the global Z3 context. 
 
>>> x = Real('x')
>>> x.ctx == main_ctx()
True
>>> c = Context()
>>> c == main_ctx()
False
>>> x2 = Real('x', c)
>>> x2.ctx == c
True
>>> eq(x, x2)
False
open_log(fname)
Log interaction to a file. This function must be invoked immediately after init().
parse_smt2_file(f, sorts={}, decls={}, ctx=None)
Parse a file in SMT 2.0 format using the given sorts and decls.
 
This function is similar to parse_smt2_string().
parse_smt2_string(s, sorts={}, decls={}, ctx=None)
Parse a string in SMT 2.0 format using the given sorts and decls.
 
The arguments sorts and decls are Python dictionaries used to initialize
the symbol table used for the SMT 2.0 parser.
 
>>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
And(x > 0, x < 10)
>>> x, y = Ints('x y')
>>> f = Function('f', IntSort(), IntSort())
>>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
x + f(y) > 0
>>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
a > 0
probe_description(name, ctx=None)
Return a short description for the probe named `name`.
 
>>> d = probe_description('memory')
probes(ctx=None)
Return a list of all available probes in Z3.
 
>>> l = probes()
>>> l.count('memory') == 1
True
prove(claim, **keywords)
Try to prove the given claim.
 
This is a simple function for creating demonstrations.  It tries to prove
`claim` by showing the negation is unsatisfiable.
 
>>> p, q = Bools('p q')
>>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
proved
reset_params()
Reset all global (or module) parameters.
sequence_interpolant(v, p=None, ctx=None)
Compute interpolant for a sequence of formulas.
 
If len(v) == N, and if the conjunction of the formulas in v is
unsatisfiable, the interpolant is a sequence of formulas w
such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
 
1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
and v[i+1]..v[n]
 
Requires len(v) >= 1. 
 
If a & b is satisfiable, raises an object of class ModelRef
that represents a model of a & b.
 
If parameters p are supplied, these are used in creating the
solver that determines satisfiability.
 
>>> x = Int('x')
>>> y = Int('y')
>>> print sequence_interpolant([x < 0, y == x , y > 2])
[Not(x >= 0), Not(y >= 0)]
set_option(*args, **kws)
Alias for 'set_param' for backward compatibility.
set_param(*args, **kws)
Set Z3 global (or module) parameters.
 
>>> set_param(precision=10)
simplify(a, *arguments, **keywords)
Simplify the expression `a` using the given options.
 
This function has many options. Use `help_simplify` to obtain the complete list.
 
>>> x = Int('x')
>>> y = Int('y')
>>> simplify(x + 1 + y + x + 1)
2 + 2*x + y
>>> simplify((x + 1)*(y + 1), som=True)
1 + x + y + x*y
>>> simplify(Distinct(x, y, 1), blast_distinct=True)
And(Not(x == y), Not(x == 1), Not(y == 1))
>>> simplify(And(x == 0, y == 1), elim_and=True)
Not(Or(Not(x == 0), Not(y == 1)))
simplify_param_descrs()
Return the set of parameter descriptions for Z3 `simplify` procedure.
solve(*args, **keywords)
Solve the constraints `*args`.
 
This is a simple function for creating demonstrations. It creates a solver,
configure it using the options in `keywords`, adds the constraints
in `args`, and invokes check.
 
>>> a = Int('a')
>>> solve(a > 0, a < 2)
[a = 1]
solve_using(s, *args, **keywords)
Solve the constraints `*args` using solver `s`.
 
This is a simple function for creating demonstrations. It is similar to `solve`,
but it uses the given solver `s`.
It configures solver `s` using the options in `keywords`, adds the constraints
in `args`, and invokes check.
substitute(t, *m)
Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to.
 
>>> x = Int('x')
>>> y = Int('y')
>>> substitute(x + 1, (x, y + 1))
y + 1 + 1
>>> f = Function('f', IntSort(), IntSort())
>>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
1 + 1
substitute_vars(t, *m)
Substitute the free variables in t with the expression in m.
 
>>> v0 = Var(0, IntSort())
>>> v1 = Var(1, IntSort())
>>> x  = Int('x')
>>> f  = Function('f', IntSort(), IntSort(), IntSort())
>>> # replace v0 with x+1 and v1 with x
>>> substitute_vars(f(v0, v1), x + 1, x)
f(x + 1, x)
tactic_description(name, ctx=None)
Return a short description for the tactic named `name`.
 
>>> d = tactic_description('simplify')
tactics(ctx=None)
Return a list of all available tactics in Z3.
 
>>> l = tactics()
>>> l.count('simplify') == 1
True
to_symbol(s, ctx=None)
Convert an integer or string into a Z3 symbol.
tree_interpolant(pat, p=None, ctx=None)
Compute interpolant for a tree of formulas.
 
The input is an interpolation pattern over a set of formulas C.
The pattern pat is a formula combining the formulas in C using
logical conjunction and the "interp" operator (see Interp). This
interp operator is logically the identity operator. It marks the
sub-formulas of the pattern for which interpolants should be
computed. The interpolant is a map sigma from marked subformulas
to formulas, such that, for each marked subformula phi of pat
(where phi sigma is phi with sigma(psi) substituted for each
subformula psi of phi such that psi in dom(sigma)):
 
  1) phi sigma implies sigma(phi), and
 
  2) sigma(phi) is in the common uninterpreted vocabulary between
  the formulas of C occurring in phi and those not occurring in
  phi
 
  and moreover pat sigma implies false. In the simplest case
  an interpolant for the pattern "(and (interp A) B)" maps A
  to an interpolant for A /\ B. 
 
  The return value is a vector of formulas representing sigma. This
  vector contains sigma(phi) for each marked subformula of pat, in
  pre-order traversal. This means that subformulas of phi occur before phi
  in the vector. Also, subformulas that occur multiply in pat will
  occur multiply in the result vector.
 
If pat is satisfiable, raises an object of class ModelRef
that represents a model of pat.
 
If parameters p are supplied, these are used in creating the
solver that determines satisfiability.
 
>>> x = Int('x')
>>> y = Int('y')
>>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
[Not(x >= 0), Not(y <= 2)]
 
>>> g = And(Interpolant(x<0),x<2)
>>> try:
...     print tree_interpolant(g).sexpr()
... except ModelRef as m:
...     print m.sexpr()
(define-fun x () Int
  (- 1))

 
Data
        Z3_APP_AST = 1
Z3_ARRAY_SORT = 5
Z3_BOOL_SORT = 1
Z3_BV_SORT = 4
Z3_CANCELED = 4
Z3_DATATYPE_SORT = 6
Z3_DEC_REF_ERROR = 11
Z3_EXCEPTION = 12
Z3_FILE_ACCESS_ERROR = 8
Z3_FINITE_DOMAIN_SORT = 8
Z3_FUNC_DECL_AST = 5
Z3_GOAL_OVER = 2
Z3_GOAL_PRECISE = 0
Z3_GOAL_UNDER = 1
Z3_GOAL_UNDER_OVER = 3
Z3_INTERNAL_FATAL = 9
Z3_INT_SORT = 2
Z3_INT_SYMBOL = 0
Z3_INVALID_ARG = 3
Z3_INVALID_PATTERN = 6
Z3_INVALID_USAGE = 10
Z3_IOB = 2
Z3_L_FALSE = -1
Z3_L_TRUE = 1
Z3_L_UNDEF = 0
Z3_MEMOUT_FAIL = 7
Z3_MEMOUT_WATERMARK = 3
Z3_NO_FAILURE = 0
Z3_NO_PARSER = 5
Z3_NUMERAL_AST = 0
Z3_NUM_CONFLICTS = 5
Z3_OK = 0
Z3_OP_ADD = 518
Z3_OP_AGNUM = 513
Z3_OP_AND = 261
Z3_OP_ANUM = 512
Z3_OP_ARRAY_DEFAULT = 772
Z3_OP_ARRAY_MAP = 771
Z3_OP_AS_ARRAY = 778
Z3_OP_BADD = 1028
Z3_OP_BAND = 1049
Z3_OP_BASHR = 1066
Z3_OP_BCOMP = 1063
Z3_OP_BIT0 = 1026
Z3_OP_BIT1 = 1025
Z3_OP_BLSHR = 1065
Z3_OP_BMUL = 1030
Z3_OP_BNAND = 1053
Z3_OP_BNEG = 1027
Z3_OP_BNOR = 1054
Z3_OP_BNOT = 1051
Z3_OP_BNUM = 1024
Z3_OP_BOR = 1050
Z3_OP_BREDAND = 1062
Z3_OP_BREDOR = 1061
Z3_OP_BSDIV = 1031
Z3_OP_BSDIV0 = 1036
Z3_OP_BSHL = 1064
Z3_OP_BSMOD = 1035
Z3_OP_BSMOD0 = 1040
Z3_OP_BSREM = 1033
Z3_OP_BSREM0 = 1038
Z3_OP_BSUB = 1029
Z3_OP_BUDIV = 1032
Z3_OP_BUDIV0 = 1037
Z3_OP_BUREM = 1034
Z3_OP_BUREM0 = 1039
Z3_OP_BV2INT = 1072
Z3_OP_BXNOR = 1055
Z3_OP_BXOR = 1052
Z3_OP_CARRY = 1073
Z3_OP_CONCAT = 1056
Z3_OP_CONST_ARRAY = 770
Z3_OP_DISTINCT = 259
Z3_OP_DIV = 522
Z3_OP_DT_ACCESSOR = 2050
Z3_OP_DT_CONSTRUCTOR = 2048
Z3_OP_DT_RECOGNISER = 2049
Z3_OP_EQ = 258
Z3_OP_EXTRACT = 1059
Z3_OP_EXT_ROTATE_LEFT = 1069
Z3_OP_EXT_ROTATE_RIGHT = 1070
Z3_OP_FALSE = 257
Z3_OP_FD_LT = 1549
Z3_OP_GE = 515
Z3_OP_GT = 517
Z3_OP_IDIV = 523
Z3_OP_IFF = 263
Z3_OP_IMPLIES = 266
Z3_OP_INT2BV = 1071
Z3_OP_INTERP = 268
Z3_OP_IS_INT = 528
Z3_OP_ITE = 260
Z3_OP_LABEL = 1792
Z3_OP_LABEL_LIT = 1793
Z3_OP_LE = 514
Z3_OP_LT = 516
Z3_OP_MOD = 525
Z3_OP_MUL = 521
Z3_OP_NOT = 265
Z3_OP_OEQ = 267
Z3_OP_OR = 262
Z3_OP_POWER = 529
Z3_OP_PR_AND_ELIM = 1292
Z3_OP_PR_APPLY_DEF = 1310
Z3_OP_PR_ASSERTED = 1282
Z3_OP_PR_CNF_STAR = 1315
Z3_OP_PR_COMMUTATIVITY = 1307
Z3_OP_PR_DEF_AXIOM = 1308
Z3_OP_PR_DEF_INTRO = 1309
Z3_OP_PR_DER = 1300
Z3_OP_PR_DISTRIBUTIVITY = 1291
Z3_OP_PR_ELIM_UNUSED_VARS = 1299
Z3_OP_PR_GOAL = 1283
Z3_OP_PR_HYPER_RESOLVE = 1319
Z3_OP_PR_HYPOTHESIS = 1302
Z3_OP_PR_IFF_FALSE = 1306
Z3_OP_PR_IFF_OEQ = 1311
Z3_OP_PR_IFF_TRUE = 1305
Z3_OP_PR_LEMMA = 1303
Z3_OP_PR_MODUS_PONENS = 1284
Z3_OP_PR_MODUS_PONENS_OEQ = 1317
Z3_OP_PR_MONOTONICITY = 1289
Z3_OP_PR_NNF_NEG = 1313
Z3_OP_PR_NNF_POS = 1312
Z3_OP_PR_NNF_STAR = 1314
Z3_OP_PR_NOT_OR_ELIM = 1293
Z3_OP_PR_PULL_QUANT = 1296
Z3_OP_PR_PULL_QUANT_STAR = 1297
Z3_OP_PR_PUSH_QUANT = 1298
Z3_OP_PR_QUANT_INST = 1301
Z3_OP_PR_QUANT_INTRO = 1290
Z3_OP_PR_REFLEXIVITY = 1285
Z3_OP_PR_REWRITE = 1294
Z3_OP_PR_REWRITE_STAR = 1295
Z3_OP_PR_SKOLEMIZE = 1316
Z3_OP_PR_SYMMETRY = 1286
Z3_OP_PR_TH_LEMMA = 1318
Z3_OP_PR_TRANSITIVITY = 1287
Z3_OP_PR_TRANSITIVITY_STAR = 1288
Z3_OP_PR_TRUE = 1281
Z3_OP_PR_UNDEF = 1280
Z3_OP_PR_UNIT_RESOLUTION = 1304
Z3_OP_RA_CLONE = 1548
Z3_OP_RA_COMPLEMENT = 1546
Z3_OP_RA_EMPTY = 1537
Z3_OP_RA_FILTER = 1543
Z3_OP_RA_IS_EMPTY = 1538
Z3_OP_RA_JOIN = 1539
Z3_OP_RA_NEGATION_FILTER = 1544
Z3_OP_RA_PROJECT = 1542
Z3_OP_RA_RENAME = 1545
Z3_OP_RA_SELECT = 1547
Z3_OP_RA_STORE = 1536
Z3_OP_RA_UNION = 1540
Z3_OP_RA_WIDEN = 1541
Z3_OP_REM = 524
Z3_OP_REPEAT = 1060
Z3_OP_ROTATE_LEFT = 1067
Z3_OP_ROTATE_RIGHT = 1068
Z3_OP_SELECT = 769
Z3_OP_SET_COMPLEMENT = 776
Z3_OP_SET_DIFFERENCE = 775
Z3_OP_SET_INTERSECT = 774
Z3_OP_SET_SUBSET = 777
Z3_OP_SET_UNION = 773
Z3_OP_SGEQ = 1044
Z3_OP_SGT = 1048
Z3_OP_SIGN_EXT = 1057
Z3_OP_SLEQ = 1042
Z3_OP_SLT = 1046
Z3_OP_STORE = 768
Z3_OP_SUB = 519
Z3_OP_TO_INT = 527
Z3_OP_TO_REAL = 526
Z3_OP_TRUE = 256
Z3_OP_UGEQ = 1043
Z3_OP_UGT = 1047
Z3_OP_ULEQ = 1041
Z3_OP_ULT = 1045
Z3_OP_UMINUS = 520
Z3_OP_UNINTERPRETED = 2051
Z3_OP_XOR = 264
Z3_OP_XOR3 = 1074
Z3_OP_ZERO_EXT = 1058
Z3_PARAMETER_AST = 5
Z3_PARAMETER_DOUBLE = 1
Z3_PARAMETER_FUNC_DECL = 6
Z3_PARAMETER_INT = 0
Z3_PARAMETER_RATIONAL = 2
Z3_PARAMETER_SORT = 4
Z3_PARAMETER_SYMBOL = 3
Z3_PARSER_ERROR = 4
Z3_PK_BOOL = 1
Z3_PK_DOUBLE = 2
Z3_PK_INVALID = 6
Z3_PK_OTHER = 5
Z3_PK_STRING = 4
Z3_PK_SYMBOL = 3
Z3_PK_UINT = 0
Z3_PRINT_LOW_LEVEL = 1
Z3_PRINT_SMTLIB2_COMPLIANT = 3
Z3_PRINT_SMTLIB_COMPLIANT = 2
Z3_PRINT_SMTLIB_FULL = 0
Z3_QUANTIFIERS = 7
Z3_QUANTIFIER_AST = 3
Z3_REAL_SORT = 3
Z3_RELATION_SORT = 7
Z3_SORT_AST = 4
Z3_SORT_ERROR = 1
Z3_STRING_SYMBOL = 1
Z3_THEORY = 6
Z3_TIMEOUT = 2
Z3_UNINTERPRETED_SORT = 0
Z3_UNKNOWN = 1
Z3_UNKNOWN_AST = 1000
Z3_UNKNOWN_SORT = 1000
Z3_VAR_AST = 2
sat = sat
unknown = unknown
unsat = unsat