mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

add selected type annotations to python API

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-04 18:39:39 -07:00
parent 26ab0de8fc
commit 5e10fd39fc
1 changed files with 54 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

97
src/api/python/z3/z3.py
View file

@ -56,6 +56,18 @@ import copy
if sys.version_info.major >= 3: if sys.version_info.major >= 3:
from typing import Iterable from typing import Iterable
from collections.abc import Callable
from typing import (
Any,
Iterable,
Sequence,
TypeGuard,
TypeVar,
Self,
Union,
)
Z3_DEBUG = __debug__ Z3_DEBUG = __debug__
@ -121,7 +133,7 @@ def append_log(s):
Z3_append_log(s) Z3_append_log(s)
def to_symbol(s, ctx=None): def to_symbol(s : int | str, ctx = None):
"""Convert an integer or string into a Z3 symbol.""" """Convert an integer or string into a Z3 symbol."""
if _is_int(s): if _is_int(s):
return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s) return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
@ -236,7 +248,7 @@ class Context:
_main_ctx = None _main_ctx = None
def main_ctx(): def main_ctx() -> Context:
"""Return a reference to the global Z3 context. """Return a reference to the global Z3 context.
>>> x = Real('x') >>> x = Real('x')
@ -257,14 +269,14 @@ def main_ctx():
return _main_ctx return _main_ctx
def _get_ctx(ctx): def _get_ctx(ctx : Context | None) -> Context:
if ctx is None: if ctx is None:
return main_ctx() return main_ctx()
else: else:
return ctx return ctx
def get_ctx(ctx): def get_ctx(ctx : Context | None) -> Context:
return _get_ctx(ctx) return _get_ctx(ctx)
@ -292,7 +304,7 @@ def set_param(*args, **kws):
prev = None prev = None
def reset_params(): def reset_params() -> None:
"""Reset all global (or module) parameters. """Reset all global (or module) parameters.
""" """
Z3_global_param_reset_all() Z3_global_param_reset_all()
@ -304,7 +316,7 @@ def set_option(*args, **kws):
return set_param(*args, **kws) return set_param(*args, **kws)
def get_param(name): def get_param(name : str) -> str:
"""Return the value of a Z3 global (or module) parameter """Return the value of a Z3 global (or module) parameter
>>> get_param('nlsat.reorder') >>> get_param('nlsat.reorder')
@ -452,7 +464,7 @@ class AstRef(Z3PPObject):
return None return None
def is_ast(a): def is_ast(a : Any) -> TypeGuard[AstRef]:
"""Return `True` if `a` is an AST node. """Return `True` if `a` is an AST node.
>>> is_ast(10) >>> is_ast(10)
@ -473,7 +485,7 @@ def is_ast(a):
return isinstance(a, AstRef) return isinstance(a, AstRef)
def eq(a, b): def eq(a : AstRef, b : AstRef) -> bool:
"""Return `True` if `a` and `b` are structurally identical AST nodes. """Return `True` if `a` and `b` are structurally identical AST nodes.
>>> x = Int('x') >>> x = Int('x')
@ -492,7 +504,7 @@ def eq(a, b):
return a.eq(b) return a.eq(b)
def _ast_kind(ctx, a): def _ast_kind(ctx : Context, a : Any) -> int:
if is_ast(a): if is_ast(a):
a = a.as_ast() a = a.as_ast()
return Z3_get_ast_kind(ctx.ref(), a) return Z3_get_ast_kind(ctx.ref(), a)
@ -648,7 +660,7 @@ class SortRef(AstRef):
return AstRef.__hash__(self) return AstRef.__hash__(self)
def is_sort(s): def is_sort(s : Any) -> TypeGuard[SortRef]:
"""Return `True` if `s` is a Z3 sort. """Return `True` if `s` is a Z3 sort.
>>> is_sort(IntSort()) >>> is_sort(IntSort())
@ -692,11 +704,11 @@ def _to_sort_ref(s, ctx):
return SortRef(s, ctx) return SortRef(s, ctx)
def _sort(ctx, a): def _sort(ctx : Context, a : Any) -> SortRef:
return _to_sort_ref(Z3_get_sort(ctx.ref(), a), ctx) return _to_sort_ref(Z3_get_sort(ctx.ref(), a), ctx)
def DeclareSort(name, ctx=None): def DeclareSort(name, ctx : Context | None = None) -> SortRef:
"""Create a new uninterpreted sort named `name`. """Create a new uninterpreted sort named `name`.
If `ctx=None`, then the new sort is declared in the global Z3Py context. If `ctx=None`, then the new sort is declared in the global Z3Py context.
@ -1500,7 +1512,7 @@ def FreshConst(sort, prefix="c"):
return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx) return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
def Var(idx, s): def Var(idx : int, s : SortRef) -> ExprRef:
"""Create a Z3 free variable. Free variables are used to create quantified formulas. """Create a Z3 free variable. Free variables are used to create quantified formulas.
A free variable with index n is bound when it occurs within the scope of n+1 quantified A free variable with index n is bound when it occurs within the scope of n+1 quantified
declarations. declarations.
@ -1515,7 +1527,7 @@ def Var(idx, s):
return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx) return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
def RealVar(idx, ctx=None): def RealVar(idx: int, ctx: Context | None = None) -> ExprRef:
""" """
Create a real free variable. Free variables are used to create quantified formulas. Create a real free variable. Free variables are used to create quantified formulas.
They are also used to create polynomials. They are also used to create polynomials.
@ -1525,8 +1537,7 @@ def RealVar(idx, ctx=None):
""" """
return Var(idx, RealSort(ctx)) return Var(idx, RealSort(ctx))
def RealVarVector(n: int, ctx: Context | None = None) -> list[ExprRef]:
def RealVarVector(n, ctx=None):
""" """
Create a list of Real free variables. Create a list of Real free variables.
The variables have ids: 0, 1, ..., n-1 The variables have ids: 0, 1, ..., n-1
@ -1630,7 +1641,7 @@ class BoolRef(ExprRef):
def is_bool(a): def is_bool(a : Any) -> TypeGuard[BoolRef]:
"""Return `True` if `a` is a Z3 Boolean expression. """Return `True` if `a` is a Z3 Boolean expression.
>>> p = Bool('p') >>> p = Bool('p')
@ -1648,7 +1659,7 @@ def is_bool(a):
return isinstance(a, BoolRef) return isinstance(a, BoolRef)
def is_true(a): def is_true(a : Any) -> TypeGuard[BoolRef]:
"""Return `True` if `a` is the Z3 true expression. """Return `True` if `a` is the Z3 true expression.
>>> p = Bool('p') >>> p = Bool('p')
@ -1666,7 +1677,7 @@ def is_true(a):
return is_app_of(a, Z3_OP_TRUE) return is_app_of(a, Z3_OP_TRUE)
def is_false(a): def is_false(a : Any) -> TypeGuard[BoolRef]:
"""Return `True` if `a` is the Z3 false expression. """Return `True` if `a` is the Z3 false expression.
>>> p = Bool('p') >>> p = Bool('p')
@ -1680,7 +1691,7 @@ def is_false(a):
return is_app_of(a, Z3_OP_FALSE) return is_app_of(a, Z3_OP_FALSE)
def is_and(a): def is_and(a : Any) -> TypeGuard[BoolRef]:
"""Return `True` if `a` is a Z3 and expression. """Return `True` if `a` is a Z3 and expression.
>>> p, q = Bools('p q') >>> p, q = Bools('p q')
@ -1692,7 +1703,7 @@ def is_and(a):
return is_app_of(a, Z3_OP_AND) return is_app_of(a, Z3_OP_AND)
def is_or(a): def is_or(a : Any) -> TypeGuard[BoolRef]:
"""Return `True` if `a` is a Z3 or expression. """Return `True` if `a` is a Z3 or expression.
>>> p, q = Bools('p q') >>> p, q = Bools('p q')
@ -1704,7 +1715,7 @@ def is_or(a):
return is_app_of(a, Z3_OP_OR) return is_app_of(a, Z3_OP_OR)
def is_implies(a): def is_implies(a : Any) -> TypeGuard[BoolRef]:
"""Return `True` if `a` is a Z3 implication expression. """Return `True` if `a` is a Z3 implication expression.
>>> p, q = Bools('p q') >>> p, q = Bools('p q')
@ -1716,7 +1727,7 @@ def is_implies(a):
return is_app_of(a, Z3_OP_IMPLIES) return is_app_of(a, Z3_OP_IMPLIES)
def is_not(a): def is_not(a : Any) -> TypeGuard[BoolRef]:
"""Return `True` if `a` is a Z3 not expression. """Return `True` if `a` is a Z3 not expression.
>>> p = Bool('p') >>> p = Bool('p')
@ -1728,7 +1739,7 @@ def is_not(a):
return is_app_of(a, Z3_OP_NOT) return is_app_of(a, Z3_OP_NOT)
def is_eq(a): def is_eq(a : Any) -> TypeGuard[BoolRef]:
"""Return `True` if `a` is a Z3 equality expression. """Return `True` if `a` is a Z3 equality expression.
>>> x, y = Ints('x y') >>> x, y = Ints('x y')
@ -1738,7 +1749,7 @@ def is_eq(a):
return is_app_of(a, Z3_OP_EQ) return is_app_of(a, Z3_OP_EQ)
def is_distinct(a): def is_distinct(a : Any) -> TypeGuard[BoolRef]:
"""Return `True` if `a` is a Z3 distinct expression. """Return `True` if `a` is a Z3 distinct expression.
>>> x, y, z = Ints('x y z') >>> x, y, z = Ints('x y z')
@ -2433,7 +2444,7 @@ class ArithSortRef(SortRef):
_z3_assert(False, msg % self) _z3_assert(False, msg % self)
def is_arith_sort(s): def is_arith_sort(s : Any) -> TypeGuard[ArithSortRef]:
"""Return `True` if s is an arithmetical sort (type). """Return `True` if s is an arithmetical sort (type).
>>> is_arith_sort(IntSort()) >>> is_arith_sort(IntSort())
@ -2755,7 +2766,7 @@ def is_arith(a):
return isinstance(a, ArithRef) return isinstance(a, ArithRef)
def is_int(a): def is_int(a) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an integer expression. """Return `True` if `a` is an integer expression.
>>> x = Int('x') >>> x = Int('x')
@ -2861,7 +2872,7 @@ def is_algebraic_value(a):
return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast()) return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
def is_add(a): def is_add(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form b + c. """Return `True` if `a` is an expression of the form b + c.
>>> x, y = Ints('x y') >>> x, y = Ints('x y')
@ -2873,7 +2884,7 @@ def is_add(a):
return is_app_of(a, Z3_OP_ADD) return is_app_of(a, Z3_OP_ADD)
def is_mul(a): def is_mul(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form b * c. """Return `True` if `a` is an expression of the form b * c.
>>> x, y = Ints('x y') >>> x, y = Ints('x y')
@ -2885,7 +2896,7 @@ def is_mul(a):
return is_app_of(a, Z3_OP_MUL) return is_app_of(a, Z3_OP_MUL)
def is_sub(a): def is_sub(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form b - c. """Return `True` if `a` is an expression of the form b - c.
>>> x, y = Ints('x y') >>> x, y = Ints('x y')
@ -2897,7 +2908,7 @@ def is_sub(a):
return is_app_of(a, Z3_OP_SUB) return is_app_of(a, Z3_OP_SUB)
def is_div(a): def is_div(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form b / c. """Return `True` if `a` is an expression of the form b / c.
>>> x, y = Reals('x y') >>> x, y = Reals('x y')
@ -2914,7 +2925,7 @@ def is_div(a):
return is_app_of(a, Z3_OP_DIV) return is_app_of(a, Z3_OP_DIV)
def is_idiv(a): def is_idiv(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form b div c. """Return `True` if `a` is an expression of the form b div c.
>>> x, y = Ints('x y') >>> x, y = Ints('x y')
@ -2926,7 +2937,7 @@ def is_idiv(a):
return is_app_of(a, Z3_OP_IDIV) return is_app_of(a, Z3_OP_IDIV)
def is_mod(a): def is_mod(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form b % c. """Return `True` if `a` is an expression of the form b % c.
>>> x, y = Ints('x y') >>> x, y = Ints('x y')
@ -2938,7 +2949,7 @@ def is_mod(a):
return is_app_of(a, Z3_OP_MOD) return is_app_of(a, Z3_OP_MOD)
def is_le(a): def is_le(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form b <= c. """Return `True` if `a` is an expression of the form b <= c.
>>> x, y = Ints('x y') >>> x, y = Ints('x y')
@ -2950,7 +2961,7 @@ def is_le(a):
return is_app_of(a, Z3_OP_LE) return is_app_of(a, Z3_OP_LE)
def is_lt(a): def is_lt(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form b < c. """Return `True` if `a` is an expression of the form b < c.
>>> x, y = Ints('x y') >>> x, y = Ints('x y')
@ -2962,7 +2973,7 @@ def is_lt(a):
return is_app_of(a, Z3_OP_LT) return is_app_of(a, Z3_OP_LT)
def is_ge(a): def is_ge(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form b >= c. """Return `True` if `a` is an expression of the form b >= c.
>>> x, y = Ints('x y') >>> x, y = Ints('x y')
@ -2974,7 +2985,7 @@ def is_ge(a):
return is_app_of(a, Z3_OP_GE) return is_app_of(a, Z3_OP_GE)
def is_gt(a): def is_gt(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form b > c. """Return `True` if `a` is an expression of the form b > c.
>>> x, y = Ints('x y') >>> x, y = Ints('x y')
@ -2986,7 +2997,7 @@ def is_gt(a):
return is_app_of(a, Z3_OP_GT) return is_app_of(a, Z3_OP_GT)
def is_is_int(a): def is_is_int(a : Any) -> bool:
"""Return `True` if `a` is an expression of the form IsInt(b). """Return `True` if `a` is an expression of the form IsInt(b).
>>> x = Real('x') >>> x = Real('x')
@ -2998,7 +3009,7 @@ def is_is_int(a):
return is_app_of(a, Z3_OP_IS_INT) return is_app_of(a, Z3_OP_IS_INT)
def is_to_real(a): def is_to_real(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form ToReal(b). """Return `True` if `a` is an expression of the form ToReal(b).
>>> x = Int('x') >>> x = Int('x')
@ -3013,7 +3024,7 @@ def is_to_real(a):
return is_app_of(a, Z3_OP_TO_REAL) return is_app_of(a, Z3_OP_TO_REAL)
def is_to_int(a): def is_to_int(a : Any) -> TypeGuard[ArithRef]:
"""Return `True` if `a` is an expression of the form ToInt(b). """Return `True` if `a` is an expression of the form ToInt(b).
>>> x = Real('x') >>> x = Real('x')
@ -4689,7 +4700,7 @@ def is_array_sort(a):
return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
def is_array(a): def is_array(a : Any) -> TypeGuard[ArrayRef]:
"""Return `True` if `a` is a Z3 array expression. """Return `True` if `a` is a Z3 array expression.
>>> a = Array('a', IntSort(), IntSort()) >>> a = Array('a', IntSort(), IntSort())
@ -11140,7 +11151,7 @@ def is_seq(a):
return isinstance(a, SeqRef) return isinstance(a, SeqRef)
def is_string(a): def is_string(a: Any) -> TypeGuard[SeqRef]:
"""Return `True` if `a` is a Z3 string expression. """Return `True` if `a` is a Z3 string expression.
>>> print (is_string(StringVal("ab"))) >>> print (is_string(StringVal("ab")))
True True
@ -11148,7 +11159,7 @@ def is_string(a):
return isinstance(a, SeqRef) and a.is_string() return isinstance(a, SeqRef) and a.is_string()
def is_string_value(a): def is_string_value(a: Any) -> TypeGuard[SeqRef]:
"""return 'True' if 'a' is a Z3 string constant expression. """return 'True' if 'a' is a Z3 string constant expression.
>>> print (is_string_value(StringVal("a"))) >>> print (is_string_value(StringVal("a")))
True True