| |
- AstMap
- CheckSatResult
- Context
- Datatype
- FuncEntry
- OptimizeObjective
- ParamDescrsRef
- ParamsRef
- Probe
- ScopedConstructor
- ScopedConstructorList
- Statistics
- Tactic
- Z3PPObject
-
- ApplyResult
- AstRef
-
- ExprRef
-
- ArithRef
-
- AlgebraicNumRef
- IntNumRef
- RatNumRef
- ArrayRef
- BitVecRef
-
- BitVecNumRef
- BoolRef
-
- QuantifierRef
- DatatypeRef
- FPRMRef
- FPRef
-
- FPNumRef
- PatternRef
- FuncDeclRef
- SortRef
-
- ArithSortRef
- ArraySortRef
- BitVecSortRef
- BoolSortRef
- DatatypeSortRef
- FPRMSortRef
- FPSortRef
- FiniteDomainSortRef
- AstVector
- Fixedpoint
- FuncInterp
- Goal
- ModelRef
- Optimize
- 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 `self.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 `self.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 `self.sort().domain()`.
>>> a = Array('a', IntSort(), BoolSort())
>>> a.domain()
Int
- mk_default(self)
- range(self)
- Shorthand for `self.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 `self.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 `self.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 `self.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 `self.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
- is_bool(self)
- is_int(self)
- 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 Context |
|
A Context manages all other Z3 objects, global configuration options, etc.
Z3Py uses a default global context. For most applications this is sufficient.
An application may use multiple Z3 contexts. Objects created in one context
cannot be used in another one. However, several objects may be "translated" from
one context to another. It is not safe to access Z3 objects from multiple threads.
The only exception is the method `interrupt()` that can be used to interrupt() a long
computation.
The initialization method receives global configuration options for the new context. |
|
Methods defined here:
- __del__(self)
- __init__(self, *args, **kws)
- interrupt(self)
- Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
This method can be invoked from a thread different from the one executing the
interruptable procedure.
- ref(self)
- Return a reference to the actual C pointer to the Z3 context.
|
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 `self.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 `self.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 FPNumRef(FPRef) |
| |
- Method resolution order:
- FPNumRef
- FPRef
- ExprRef
- AstRef
- Z3PPObject
Methods defined here:
- as_string(self)
- exponent(self)
- exponent_as_long(self)
- isInf(self)
- isNaN(self)
- isNegative(self)
- isZero(self)
- sign(self)
- significand(self)
Methods inherited from FPRef:
- __add__(self, other)
- Create the Z3 expression `self + other`.
>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x + y
x + y
>>> (x + y).sort()
FPSort(8, 24)
- __ge__(self, other)
- __gt__(self, other)
- __le__(self, other)
- __lt__(self, other)
- __mod__(self, other)
- Create the Z3 expression mod `self % other`.
- __mul__(self, other)
- Create the Z3 expression `self * other`.
>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x * y
x * y
>>> (x * y).sort()
FPSort(8, 24)
>>> 10 * y
1.25*(2**3) * y
- __ne__(self, other)
- __neg__(self)
- Create the Z3 expression `-self`.
- __pos__(self)
- Create the Z3 expression `+self`.
- __radd__(self, other)
- Create the Z3 expression `other + self`.
>>> x = FP('x', FPSort(8, 24))
>>> 10 + x
1.25*(2**3) + x
- __rmod__(self, other)
- Create the Z3 expression mod `other % self`.
- __rmul__(self, other)
- Create the Z3 expression `other * self`.
>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x * y
x * y
>>> x * 10
x * 1.25*(2**3)
- __rsub__(self, other)
- Create the Z3 expression `other - self`.
>>> x = FP('x', FPSort(8, 24))
>>> 10 - x
1.25*(2**3) - x
- __rtruediv__(self, other)
- Create the Z3 expression division `other / self`.
- __sub__(self, other)
- Create the Z3 expression `self - other`.
>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x - y
x - y
>>> (x - y).sort()
FPSort(8, 24)
- __truediv__(self, other)
- Create the Z3 expression division `self / other`.
- ebits(self)
- Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
>>> b = FPSort(8, 24)
>>> b.ebits()
8
- sbits(self)
- Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
>>> b = FPSort(8, 24)
>>> b.sbits()
24
- sort(self)
- Return the sort of the floating-point expression `self`.
>>> x = FP('1.0', FPSort(8, 24))
>>> x.sort()
FPSort(8, 24)
>>> x.sort() == FPSort(8, 24)
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
- 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 `self.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 FPRMRef(ExprRef) |
|
Floating-point rounding mode expressions |
|
- Method resolution order:
- FPRMRef
- ExprRef
- AstRef
- Z3PPObject
Methods defined here:
- as_string(self)
- Return a Z3 floating point expression as a Python string.
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(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 `self.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 FPRMSortRef(SortRef) |
|
"Floating-point rounding mode sort. |
|
- Method resolution order:
- FPRMSortRef
- SortRef
- AstRef
- Z3PPObject
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 FPRef(ExprRef) |
|
Floating-point expressions. |
|
- Method resolution order:
- FPRef
- ExprRef
- AstRef
- Z3PPObject
Methods defined here:
- __add__(self, other)
- Create the Z3 expression `self + other`.
>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x + y
x + y
>>> (x + y).sort()
FPSort(8, 24)
- __ge__(self, other)
- __gt__(self, other)
- __le__(self, other)
- __lt__(self, other)
- __mod__(self, other)
- Create the Z3 expression mod `self % other`.
- __mul__(self, other)
- Create the Z3 expression `self * other`.
>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x * y
x * y
>>> (x * y).sort()
FPSort(8, 24)
>>> 10 * y
1.25*(2**3) * y
- __ne__(self, other)
- __neg__(self)
- Create the Z3 expression `-self`.
- __pos__(self)
- Create the Z3 expression `+self`.
- __radd__(self, other)
- Create the Z3 expression `other + self`.
>>> x = FP('x', FPSort(8, 24))
>>> 10 + x
1.25*(2**3) + x
- __rmod__(self, other)
- Create the Z3 expression mod `other % self`.
- __rmul__(self, other)
- Create the Z3 expression `other * self`.
>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x * y
x * y
>>> x * 10
x * 1.25*(2**3)
- __rsub__(self, other)
- Create the Z3 expression `other - self`.
>>> x = FP('x', FPSort(8, 24))
>>> 10 - x
1.25*(2**3) - x
- __rtruediv__(self, other)
- Create the Z3 expression division `other / self`.
- __sub__(self, other)
- Create the Z3 expression `self - other`.
>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x - y
x - y
>>> (x - y).sort()
FPSort(8, 24)
- __truediv__(self, other)
- Create the Z3 expression division `self / other`.
- as_string(self)
- Return a Z3 floating point expression as a Python string.
- ebits(self)
- Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
>>> b = FPSort(8, 24)
>>> b.ebits()
8
- sbits(self)
- Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
>>> b = FPSort(8, 24)
>>> b.sbits()
24
- sort(self)
- Return the sort of the floating-point expression `self`.
>>> x = FP('1.0', FPSort(8, 24))
>>> x.sort()
FPSort(8, 24)
>>> x.sort() == FPSort(8, 24)
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
- 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 `self.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 FPSortRef(SortRef) |
|
Floating-point sort. |
|
- Method resolution order:
- FPSortRef
- SortRef
- AstRef
- Z3PPObject
Methods defined here:
- cast(self, val)
- Try to cast `val` as a Floating-point expression
>>> b = FPSort(8, 24)
>>> b.cast(1.0)
1
>>> b.cast(1.0).sexpr()
'(fp #b0 #x7f #b00000000000000000000000)'
- ebits(self)
- Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`.
>>> b = FPSort(8, 24)
>>> b.ebits()
8
- sbits(self)
- Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`.
>>> b = FPSort(8, 24)
>>> b.sbits()
24
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 FiniteDomainSortRef(SortRef) |
|
Finite domain sort. |
|
- Method resolution order:
- FiniteDomainSortRef
- SortRef
- AstRef
- Z3PPObject
Methods defined here:
- size(self)
- Return the size of the finite domain sort
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 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 `self.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 < self.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 < self.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 `self.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` < self.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 Optimize(Z3PPObject) |
|
Optimize API provides methods for solving using objective functions and weighted soft constraints |
|
Methods defined here:
- __del__(self)
- __init__(self, ctx=None)
- __repr__(self)
- Return a formatted string with all added rules and constraints.
- add(self, *args)
- Assert constraints as background axioms for the optimize solver. Alias for assert_expr.
- add_soft(self, arg, weight='1', id=None)
- Add soft constraint with optional weight and optional identifier.
If no weight is supplied, then the penalty for violating the soft constraint
is 1.
Soft constraints are grouped by identifiers. Soft constraints that are
added without identifiers are grouped by default.
- assert_exprs(self, *args)
- Assert constraints as background axioms for the optimize solver.
- check(self)
- Check satisfiability while optimizing objective functions.
- help(self)
- Display a string describing all available options.
- lower(self, obj)
- maximize(self, arg)
- Add objective function to maximize.
- minimize(self, arg)
- Add objective function to minimize.
- model(self)
- Return a model for the last check().
- param_descrs(self)
- Return the parameter description set.
- pop(self)
- restore to previously created backtracking point
- push(self)
- create a backtracking point for added rules, facts and assertions
- reason_unknown(self)
- Return a string that describes why the last `check()` returned `unknown`.
- set(self, *args, **keys)
- Set a configuration option. The method `help()` return a string containing all available options.
- 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()`.
- upper(self, obj)
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 `self.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 self.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 `self.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 `self.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 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', 'rlimit count', 'max memory', 'memory', 'num allocs']
>>> 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)
6
>>> 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)
6
- __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', 'rlimit count', 'max memory', 'memory', 'num allocs']
|
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)
| |