| | |
- builtins.object
-
- AstMap
- CheckSatResult
- Context
- Datatype
- FuncEntry
- OnClause
- OptimizeObjective
- ParamDescrsRef
- ParamsRef
- ParserContext
- Probe
- PropClosures
- ScopedConstructor
- ScopedConstructorList
- Statistics
- Tactic
- UserPropagateBase
- Z3PPObject
-
- ApplyResult
- AstRef
-
- ExprRef
-
- ArithRef
-
- AlgebraicNumRef
- IntNumRef
- RatNumRef
- ArrayRef
- BitVecRef
-
- BitVecNumRef
- BoolRef
-
- QuantifierRef
- CharRef
- DatatypeRef
- FPRMRef
- FPRef
-
- FPNumRef
- FiniteDomainRef
-
- FiniteDomainNumRef
- PatternRef
- ReRef
- SeqRef
- FuncDeclRef
- SortRef
-
- ArithSortRef
- ArraySortRef
- BitVecSortRef
- BoolSortRef
- CharSortRef
- DatatypeSortRef
- FPRMSortRef
- FPSortRef
- FiniteDomainSortRef
- ReSortRef
- SeqSortRef
- AstVector
- Fixedpoint
- FuncInterp
- Goal
- ModelRef
- Optimize
- Solver
class AlgebraicNumRef(ArithRef) |
| |
AlgebraicNumRef(ast, ctx=None)
Algebraic irrational values.
|
| |
- Method resolution order:
- AlgebraicNumRef
- ArithRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
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?'
- index(self)
- poly(self)
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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ApplyResult(Z3PPObject) |
| |
ApplyResult(result, ctx)
An ApplyResult object contains the subgoals produced by a tactic when applied to a goal.
It also contains model and proof converters.
|
| |
- Method resolution order:
- ApplyResult
- Z3PPObject
- builtins.object
Methods defined here:
- __deepcopy__(self, memo={})
- __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)
- Initialize self. See help(type(self)) for accurate signature.
- __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)
- Return 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))
- sexpr(self)
- Return a textual representation of the s-expression representing the set of subgoals in `self`.
Methods inherited from Z3PPObject:
- use_pp(self)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ArithRef(ExprRef) |
| |
ArithRef(ast, ctx=None)
Integer and Real expressions.
|
| |
- Method resolution order:
- ArithRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ArithSortRef(SortRef) |
| |
ArithSortRef(ast, ctx=None)
Real and Integer sorts.
|
| |
- Method resolution order:
- ArithSortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
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_bool(self)
- 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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ArrayRef(ExprRef) |
| |
ArrayRef(ast, ctx=None)
Array expressions.
|
| |
- Method resolution order:
- ArrayRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
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)'
- default(self)
- domain(self)
- Shorthand for `self.sort().domain()`.
>>> a = Array('a', IntSort(), BoolSort())
>>> a.domain()
Int
- domain_n(self, i)
- Shorthand for self.sort().domain_n(i)`.
- 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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ArraySortRef(SortRef) |
| |
ArraySortRef(ast, ctx=None)
Array sorts.
|
| |
- Method resolution order:
- ArraySortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- domain(self)
- Return the domain of the array sort `self`.
>>> A = ArraySort(IntSort(), BoolSort())
>>> A.domain()
Int
- domain_n(self, i)
- Return the domain of the array sort `self`.
- 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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- 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)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class AstMap(builtins.object) |
| |
AstMap(m=None, ctx=None)
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
- __deepcopy__(self, memo={})
- __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)
- Initialize self. See help(type(self)) for accurate signature.
- __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)
- Return 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
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class AstRef(Z3PPObject) |
| |
AstRef(ast, ctx=None)
AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions.
|
| |
- Method resolution order:
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __eq__(self, other)
- Return self==value.
- __hash__(self)
- Return hash(self).
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class AstVector(Z3PPObject) |
| |
AstVector(v=None, ctx=None)
A collection (vector) of ASTs.
|
| |
- Method resolution order:
- AstVector
- Z3PPObject
- builtins.object
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]
- __copy__(self)
- __deepcopy__(self, memo={})
- __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)
- Initialize self. See help(type(self)) for accurate signature.
- __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)
- Return 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class BitVecNumRef(BitVecRef) |
| |
BitVecNumRef(ast, ctx=None)
Bit-vector values.
|
| |
- Method resolution order:
- BitVecNumRef
- BitVecRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- as_binary_string(self)
- 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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class BitVecRef(ExprRef) |
| |
BitVecRef(ast, ctx=None)
Bit-vector expressions.
|
| |
- Method resolution order:
- BitVecRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class BitVecSortRef(SortRef) |
| |
BitVecSortRef(ast, ctx=None)
Bit-vector sort.
|
| |
- Method resolution order:
- BitVecSortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
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)
- Return `True` if `self` is a subsort of `other`.
>>> IntSort().subsort(RealSort())
True
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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class BoolRef(ExprRef) |
| |
BoolRef(ast, ctx=None)
All Boolean expressions are instances of this class.
|
| |
- Method resolution order:
- BoolRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- __mul__(self, other)
- Create the Z3 expression `self * other`.
- __rmul__(self, other)
- sort(self)
- Return the sort of expression `self`.
>>> x = Int('x')
>>> (x + 1).sort()
Int
>>> y = Real('y')
>>> (x + y).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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class BoolSortRef(SortRef) |
| |
BoolSortRef(ast, ctx=None)
Boolean sort.
|
| |
- Method resolution order:
- BoolSortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
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)
- Return `True` if `self` is a subsort of `other`.
>>> IntSort().subsort(RealSort())
True
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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class CharRef(ExprRef) |
| |
CharRef(ast, ctx=None)
Character expression.
|
| |
- Method resolution order:
- CharRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- __le__(self, other)
- Return self<=value.
- is_digit(self)
- to_bv(self)
- to_int(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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class CharSortRef(SortRef) |
| |
CharSortRef(ast, ctx=None)
Character sort.
|
| |
- Method resolution order:
- CharSortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- 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)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class CheckSatResult(builtins.object) |
| |
CheckSatResult(r)
Represents the result of a satisfiability check: sat, unsat, unknown.
>>> s = Solver()
>>> s.check()
sat
>>> r = s.check()
>>> isinstance(r, CheckSatResult)
True
|
| |
Methods defined here:
- __deepcopy__(self, memo={})
- __eq__(self, other)
- Return self==value.
- __init__(self, r)
- Initialize self. See help(type(self)) for accurate signature.
- __ne__(self, other)
- Return self!=value.
- __repr__(self)
- Return repr(self).
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
Data and other attributes defined here:
- __hash__ = None
|
class Context(builtins.object) |
| |
Context(*args, **kws)
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)
- Initialize self. See help(type(self)) for accurate signature.
- 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
interruptible procedure.
- param_descrs(self)
- Return the global parameter description set.
- ref(self)
- Return a reference to the actual C pointer to the Z3 context.
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class Datatype(builtins.object) |
| |
Datatype(name, ctx=None)
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:
- __deepcopy__(self, memo={})
- __init__(self, name, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __repr__(self)
- Return repr(self).
- create(self)
- Create a Z3 datatype based on the constructors declared using the method `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 following 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)
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class DatatypeRef(ExprRef) |
| |
DatatypeRef(ast, ctx=None)
Datatype expressions.
|
| |
- Method resolution order:
- DatatypeRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class DatatypeSortRef(SortRef) |
| |
DatatypeSortRef(ast, ctx=None)
Datatype sorts.
|
| |
- Method resolution order:
- DatatypeSortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- 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)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ExprRef(AstRef) |
| |
ExprRef(ast, ctx=None)
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
- builtins.object
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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FPNumRef(FPRef) |
| |
FPNumRef(ast, ctx=None)
The sign of the numeral.
>>> x = FPVal(+1.0, FPSort(8, 24))
>>> x.sign()
False
>>> x = FPVal(-1.0, FPSort(8, 24))
>>> x.sign()
True
|
| |
- Method resolution order:
- FPNumRef
- FPRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- as_string(self)
- Return a Z3 floating point expression as a Python string.
- exponent(self, biased=True)
- exponent_as_bv(self, biased=True)
- exponent_as_long(self, biased=True)
- isInf(self)
- isNaN(self)
- isNegative(self)
- isNormal(self)
- isPositive(self)
- isSubnormal(self)
- isZero(self)
- sign(self)
- sign_as_bv(self)
- significand(self)
- significand_as_bv(self)
- significand_as_long(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)
- __div__(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
- __ge__(self, other)
- Return self>=value.
- __gt__(self, other)
- Return self>value.
- __le__(self, other)
- Return self<=value.
- __lt__(self, other)
- Return self<value.
- __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
- __neg__(self)
- Create the Z3 expression `-self`.
>>> x = FP('x', Float32())
>>> -x
-x
- __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
- __rdiv__(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)
- __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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FPRMRef(ExprRef) |
| |
FPRMRef(ast, ctx=None)
Floating-point rounding mode expressions
|
| |
- Method resolution order:
- FPRMRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FPRMSortRef(SortRef) |
| |
FPRMSortRef(ast, ctx=None)
"Floating-point rounding mode sort.
|
| |
- Method resolution order:
- FPRMSortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- 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)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FPRef(ExprRef) |
| |
FPRef(ast, ctx=None)
Floating-point expressions.
|
| |
- Method resolution order:
- FPRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
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)
- __div__(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
- __ge__(self, other)
- Return self>=value.
- __gt__(self, other)
- Return self>value.
- __le__(self, other)
- Return self<=value.
- __lt__(self, other)
- Return self<value.
- __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
- __neg__(self)
- Create the Z3 expression `-self`.
>>> x = FP('x', Float32())
>>> -x
-x
- __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
- __rdiv__(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)
- __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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FPSortRef(SortRef) |
| |
FPSortRef(ast, ctx=None)
Floating-point sort.
|
| |
- Method resolution order:
- FPSortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
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 significand 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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FiniteDomainNumRef(FiniteDomainRef) |
| |
FiniteDomainNumRef(ast, ctx=None)
Integer values.
|
| |
- Method resolution order:
- FiniteDomainNumRef
- FiniteDomainRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- as_long(self)
- Return a Z3 finite-domain numeral as a Python long (bignum) numeral.
>>> s = FiniteDomainSort('S', 100)
>>> v = FiniteDomainVal(3, s)
>>> v
3
>>> v.as_long() + 1
4
- as_string(self)
- Return a Z3 finite-domain numeral as a Python string.
>>> s = FiniteDomainSort('S', 100)
>>> v = FiniteDomainVal(42, s)
>>> v.as_string()
'42'
Methods inherited from FiniteDomainRef:
- sort(self)
- Return the sort of the finite-domain 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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FiniteDomainRef(ExprRef) |
| |
FiniteDomainRef(ast, ctx=None)
Finite-domain expressions.
|
| |
- Method resolution order:
- FiniteDomainRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- as_string(self)
- Return a Z3 floating point expression as a Python string.
- sort(self)
- Return the sort of the finite-domain 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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FiniteDomainSortRef(SortRef) |
| |
FiniteDomainSortRef(ast, ctx=None)
Finite domain sort.
|
| |
- Method resolution order:
- FiniteDomainSortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- 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)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class Fixedpoint(Z3PPObject) |
| |
Fixedpoint(fixedpoint=None, ctx=None)
Fixedpoint API provides methods for solving with recursive predicates
|
| |
- Method resolution order:
- Fixedpoint
- Z3PPObject
- builtins.object
Methods defined here:
- __deepcopy__(self, memo={})
- __del__(self)
- __iadd__(self, fml)
- __init__(self, fixedpoint=None, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __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_ground_sat_answer(self)
- Retrieve a ground cex from last query call.
- get_num_levels(self, predicate)
- Retrieve number of levels used for predicate in PDR engine
- get_rule_names_along_trace(self)
- retrieve rule names along the counterexample trace
- get_rules(self)
- retrieve rules that have been added to fixedpoint context
- get_rules_along_trace(self)
- retrieve rules along the counterexample trace
- 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
- query(self, *query)
- Query the fixedpoint engine whether formula is derivable.
You can also pass an tuple or list of recursive predicates.
- query_from_lvl(self, lvl, *query)
- Query the fixedpoint engine whether formula is derivable starting at the given query level.
- 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FuncDeclRef(AstRef) |
| |
FuncDeclRef(ast, ctx=None)
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
- builtins.object
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 coercion 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __eq__(self, other)
- Return self==value.
- __hash__(self)
- Return hash(self).
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FuncEntry(builtins.object) |
| |
FuncEntry(entry, ctx)
Store the value of the interpretation of a function in a particular point.
|
| |
Methods defined here:
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, entry, ctx)
- Initialize self. See help(type(self)) for accurate signature.
- __repr__(self)
- Return 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()
1
>>> e = f_i.entry(0)
>>> e
[1, 2, 20]
>>> e.num_args()
2
>>> e.arg_value(0)
1
>>> e.arg_value(1)
2
>>> 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()
1
>>> e = f_i.entry(0)
>>> e.as_list()
[1, 2, 20]
- 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()
1
>>> 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()
1
>>> e = f_i.entry(0)
>>> e
[1, 2, 20]
>>> e.num_args()
2
>>> e.value()
20
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class FuncInterp(Z3PPObject) |
| |
FuncInterp(f, ctx)
Stores the interpretation of a function in a Z3 model.
|
| |
- Method resolution order:
- FuncInterp
- Z3PPObject
- builtins.object
Methods defined here:
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, f, ctx)
- Initialize self. See help(type(self)) for accurate signature.
- __repr__(self)
- Return 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]
[2 -> 0, else -> 1]
>>> m[f].as_list()
[[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]
[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]
[2 -> 0, else -> 1]
>>> m[f].num_entries()
1
>>> m[f].entry(0)
[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]
[2 -> 0, else -> 1]
>>> m[f].num_entries()
1
- translate(self, other_ctx)
- Copy model 'self' to context 'other_ctx'.
Methods inherited from Z3PPObject:
- use_pp(self)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class Goal(Z3PPObject) |
| |
Goal(models=True, unsat_cores=False, proofs=False, ctx=None, goal=None)
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.
|
| |
- Method resolution order:
- Goal
- Z3PPObject
- builtins.object
Methods defined here:
- __copy__(self)
- __deepcopy__(self, memo={})
- __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)
- Initialize self. See help(type(self)) for accurate signature.
- __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)
- Return 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]
- convert_model(self, model)
- Retrieve model from a satisfiable 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[1].convert_model(s.model())
[b = 0, a = 1]
- 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
- dimacs(self, include_names=True)
- Return a textual representation of the goal in DIMACS format.
- 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class IntNumRef(ArithRef) |
| |
IntNumRef(ast, ctx=None)
Integer values.
|
| |
- Method resolution order:
- IntNumRef
- ArithRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- as_binary_string(self)
- Return a Z3 integer numeral as a Python binary string.
>>> v = IntVal(10)
>>> v.as_binary_string()
'1010'
- 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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ModelRef(Z3PPObject) |
| |
ModelRef(m, ctx)
Model/Solution of a satisfiability problem (aka system of constraints).
|
| |
- Method resolution order:
- ModelRef
- Z3PPObject
- builtins.object
Methods defined here:
- __copy__(self)
- __deepcopy__(self, memo={})
- __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 interpretation 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]
[else -> 0]
>>> for d in m: print("%s -> %s" % (d, m[d]))
x -> 1
f -> [else -> 0]
- __init__(self, m, ctx)
- Initialize self. See help(type(self)) for accurate signature.
- __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)
- Return repr(self).
- decls(self)
- Return a list with all symbols that have an interpretation 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]
[else -> 0]
- get_sort(self, idx)
- Return the uninterpreted 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 interpretation 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!1, A!val!0]
- num_sorts(self)
- Return the number of uninterpreted 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]
- translate(self, target)
- Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
- update_value(self, x, value)
- Update the interpretation of a constant
Methods inherited from Z3PPObject:
- use_pp(self)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class OnClause(builtins.object) |
| |
OnClause(s, on_clause)
|
| |
Methods defined here:
- __init__(self, s, on_clause)
- Initialize self. See help(type(self)) for accurate signature.
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class Optimize(Z3PPObject) |
| |
Optimize(ctx=None)
Optimize API provides methods for solving using objective functions and weighted soft constraints
|
| |
- Method resolution order:
- Optimize
- Z3PPObject
- builtins.object
Methods defined here:
- __deepcopy__(self, memo={})
- __del__(self)
- __iadd__(self, fml)
- __init__(self, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __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_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 = Optimize()
>>> 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 as background axioms for the optimize solver.
- assertions(self)
- Return an AST vector containing all added constraints.
- check(self, *assumptions)
- Check satisfiability while optimizing objective functions.
- from_file(self, filename)
- Parse assertions and objectives from a file
- from_string(self, s)
- Parse assertions and objectives from a string
- help(self)
- Display a string describing all available options.
- lower(self, obj)
- lower_values(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().
- objectives(self)
- returns set of objective functions
- 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.
- set_on_model(self, on_model)
- Register a callback that is invoked with every incremental improvement to
objective values. The callback takes a model as argument.
The life-time of the model is limited to the callback so the
model has to be (deep) copied if it is to be used after the callback
- 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 check`.
- unsat_core(self)
- upper(self, obj)
- upper_values(self, obj)
Methods inherited from Z3PPObject:
- use_pp(self)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ParamDescrsRef(builtins.object) |
| |
ParamDescrsRef(descr, ctx=None)
Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3.
|
| |
Methods defined here:
- __deepcopy__(self, memo={})
- __del__(self)
- __getitem__(self, arg)
- __init__(self, descr, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __len__(self)
- Return the size of in the parameter description `self`.
- __repr__(self)
- Return repr(self).
- get_documentation(self, n)
- Return the documentation string of the parameter named `n`.
- 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`.
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ParamsRef(builtins.object) |
| |
ParamsRef(ctx=None, params=None)
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:
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ctx=None, params=None)
- Initialize self. See help(type(self)) for accurate signature.
- __repr__(self)
- Return repr(self).
- set(self, name, val)
- Set parameter name with value val.
- validate(self, ds)
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class PatternRef(ExprRef) |
| |
PatternRef(ast, ctx=None)
Patterns are hints for quantifier instantiation.
|
| |
- Method resolution order:
- PatternRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- as_ast(self)
- Return a pointer to the corresponding C Z3_ast object.
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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()
+
- from_string(self, s)
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class Probe(builtins.object) |
| |
Probe(probe, ctx=None)
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
- __deepcopy__(self, memo={})
- __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)
- Initialize self. See help(type(self)) for accurate signature.
- __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
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
Data and other attributes defined here:
- __hash__ = None
|
class PropClosures(builtins.object) |
| | |
Methods defined here:
- __init__(self)
- Initialize self. See help(type(self)) for accurate signature.
- get(self, ctx)
- insert(self, r)
- set(self, ctx, r)
- set_threaded(self)
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class QuantifierRef(BoolRef) |
| |
QuantifierRef(ast, ctx=None)
Universally and Existentially quantified formulas.
|
| |
- Method resolution order:
- QuantifierRef
- BoolRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- __getitem__(self, arg)
- Return the Z3 expression `self[arg]`.
- as_ast(self)
- Return a pointer to the corresponding C Z3_ast object.
- 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)
- Return unique identifier for object. It can be used for hash-tables and maps.
- is_exists(self)
- Return `True` if `self` is an existential quantifier.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.is_exists()
False
>>> q = Exists(x, f(x) != 0)
>>> q.is_exists()
True
- 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
- is_lambda(self)
- Return `True` if `self` is a lambda expression.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = Lambda(x, f(x))
>>> q.is_lambda()
True
>>> q = Exists(x, f(x) != 0)
>>> q.is_lambda()
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 or sort of Lambda.
- 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 BoolRef:
- __mul__(self, other)
- Create the Z3 expression `self * other`.
- __rmul__(self, other)
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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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()
+
- from_string(self, s)
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class RatNumRef(ArithRef) |
| |
RatNumRef(ast, ctx=None)
Rational values.
|
| |
- Method resolution order:
- RatNumRef
- ArithRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
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_long(self)
- 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
- 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_int_value(self)
- is_real(self)
- Return `True` if `self` is an real expression.
>>> x = Real('x')
>>> x.is_real()
True
>>> (x + 1).is_real()
True
- 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`.
- 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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ReRef(ExprRef) |
| |
ReRef(ast, ctx=None)
Regular expressions.
|
| |
- Method resolution order:
- ReRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- __add__(self, other)
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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ReSortRef(SortRef) |
| |
ReSortRef(ast, ctx=None)
Regular expression sort.
|
| |
- Method resolution order:
- ReSortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- basis(self)
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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- 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)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class ScopedConstructor(builtins.object) |
| |
ScopedConstructor(c, ctx)
Auxiliary object used to create Z3 datatypes.
|
| |
Methods defined here:
- __del__(self)
- __init__(self, c, ctx)
- Initialize self. See help(type(self)) for accurate signature.
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class SeqRef(ExprRef) |
| |
SeqRef(ast, ctx=None)
Sequence expression.
|
| |
- Method resolution order:
- SeqRef
- ExprRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- __add__(self, other)
- __ge__(self, other)
- Return self>=value.
- __getitem__(self, i)
- __gt__(self, other)
- Return self>value.
- __le__(self, other)
- Return self<=value.
- __lt__(self, other)
- Return self<value.
- __radd__(self, other)
- as_string(self)
- Return a string representation of sequence expression.
- at(self, i)
- is_string(self)
- is_string_value(self)
- sort(self)
- Return the sort of expression `self`.
>>> x = Int('x')
>>> (x + 1).sort()
Int
>>> y = Real('y')
>>> (x + y).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 is None
False
- __hash__(self)
- Hash code.
- __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 is not 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)
- Return a pointer to the corresponding C Z3_ast object.
- 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()
+
- from_string(self, s)
- get_id(self)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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
- params(self)
- serialize(self)
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class SeqSortRef(SortRef) |
| |
SeqSortRef(ast, ctx=None)
Sequence sort.
|
| |
- Method resolution order:
- SeqSortRef
- SortRef
- AstRef
- Z3PPObject
- builtins.object
Methods defined here:
- basis(self)
- is_string(self)
- Determine if sort is a string
>>> s = StringSort()
>>> s.is_string()
True
>>> s = SeqSort(IntSort())
>>> s.is_string()
False
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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- 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)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class Solver(Z3PPObject) |
| |
Solver(solver=None, ctx=None, logFile=None)
Solver API provides methods for implementing the main SMT 2.0 commands:
push, pop, check, get-model, etc.
|
| |
- Method resolution order:
- Solver
- Z3PPObject
- builtins.object
Methods defined here:
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __iadd__(self, fml)
- __init__(self, solver=None, ctx=None, logFile=None)
- Initialize self. See help(type(self)) for accurate signature.
- __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().eval(x)
1
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown
- consequences(self, assumptions, variables)
- Determine fixed values for the variables based on the solver state and assumptions.
>>> s = Solver()
>>> a, b, c, d = Bools('a b c d')
>>> s.add(Implies(a,b), Implies(b, c))
>>> s.consequences([a],[b,c,d])
(sat, [Implies(a, b), Implies(a, c)])
>>> s.consequences([Not(c),d],[a,b,c,d])
(sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
- cube(self, vars=None)
- Get set of cubes
The method takes an optional set of variables that restrict which
variables may be used as a starting point for cubing.
If vars is not None, then the first case split is based on a variable in
this set.
- cube_vars(self)
- Access the set of variables that were touched by the most recently generated cube.
This set of variables can be used as a starting point for additional cubes.
The idea is that variables that appear in clauses that are reduced by the most recent
cube are likely more useful to cube on.
- dimacs(self, include_names=True)
- Return a textual representation of the solver in DIMACS format.
- from_file(self, filename)
- Parse assertions from a file
- from_string(self, s)
- Parse assertions from a string
- help(self)
- Display a string describing all available options.
- import_model_converter(self, other)
- Import model converter from other into the current solver
- 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]
- next(self, t)
- non_units(self)
- Return an AST vector containing all atomic formulas in solver state that are not units.
- num_scopes(self)
- Return the current number of backtracking points.
>>> s = Solver()
>>> s.num_scopes()
0
>>> s.push()
>>> s.num_scopes()
1
>>> s.push()
>>> s.num_scopes()
2
>>> s.pop()
>>> s.num_scopes()
1
- 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
[]
- root(self, t)
- 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
- trail(self)
- Return trail of the solver state after a check() call.
- trail_levels(self)
- Return trail and decision levels of the solver state after a check() call.
- translate(self, target)
- Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
>>> c1 = Context()
>>> c2 = Context()
>>> s1 = Solver(ctx=c1)
>>> s2 = s1.translate(c2)
- units(self)
- Return an AST vector containing all currently inferred units.
- 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class SortRef(AstRef) |
| |
SortRef(ast, ctx=None)
A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.
|
| |
- Method resolution order:
- SortRef
- AstRef
- Z3PPObject
- builtins.object
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
- __hash__(self)
- Hash code.
- __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)
- Return a pointer to the corresponding C Z3_ast object.
- 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)
- Return unique identifier for object. It can be used for hash-tables and maps.
- 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:
- __bool__(self)
- __copy__(self)
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, ast, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- __nonzero__(self)
- __repr__(self)
- Return repr(self).
- __str__(self)
- Return 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 a 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)
Data descriptors inherited from Z3PPObject:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class Statistics(builtins.object) |
| |
Statistics(stats, ctx)
Statistics for `Solver.check()`.
|
| |
Methods defined here:
- __deepcopy__(self, memo={})
- __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.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)
- Initialize self. See help(type(self)) for accurate signature.
- __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)
- Return 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()
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class Tactic(builtins.object) |
| |
Tactic(tactic, ctx=None)
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]]
- __deepcopy__(self, memo={})
- __del__(self)
- __init__(self, tactic, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- 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, logFile=None)
- 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?]
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class UserPropagateBase(builtins.object) |
| |
UserPropagateBase(s, ctx=None)
|
| |
Methods defined here:
- __del__(self)
- __init__(self, s, ctx=None)
- Initialize self. See help(type(self)) for accurate signature.
- add(self, e)
- add_created(self, created)
- add_decide(self, decide)
- add_diseq(self, diseq)
- add_eq(self, eq)
- add_final(self, final)
- add_fixed(self, fixed)
- conflict(self, deps=[], eqs=[])
- ctx(self)
- ctx_ref(self)
- fresh(self, new_ctx)
- next_split(self, t, idx, phase)
- # Tell the solver to perform the next split on a given term
# If the term is a bit-vector the index idx specifies the index of the Boolean variable being
# split on. A phase of true = 1/false = -1/undef = 0 = let solver decide is the last argument.
- pop(self, num_scopes)
- propagate(self, e, ids, eqs=[])
- # Propagation can only be invoked as during a fixed or final callback.
- push(self)
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class Z3PPObject(builtins.object) |
| |
Superclass for all Z3 objects that have support for pretty printing.
|
| |
Methods defined here:
- use_pp(self)
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
| |