mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 16:38:45 +00:00
Code Activity

remove references to TypeGuard

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-04-04 19:41:50 -07:00
parent a5048e4563
commit 305f1e8498
1 changed files with 28 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -61,7 +61,6 @@ from typing import (
Any, Any,
Iterable, Iterable,
Sequence, Sequence,
TypeGuard,
TypeVar, TypeVar,
Self, Self,
Union, Union,
@ -464,7 +463,7 @@ class AstRef(Z3PPObject):
return None return None
def is_ast(a : Any) -> TypeGuard[AstRef]: def is_ast(a : Any) -> bool:
"""Return `True` if `a` is an AST node. """Return `True` if `a` is an AST node.
>>> is_ast(10) >>> is_ast(10)
@ -660,7 +659,7 @@ class SortRef(AstRef):
return AstRef.__hash__(self) return AstRef.__hash__(self)
def is_sort(s : Any) -> TypeGuard[SortRef]: def is_sort(s : Any) -> bool:
"""Return `True` if `s` is a Z3 sort. """Return `True` if `s` is a Z3 sort.
>>> is_sort(IntSort()) >>> is_sort(IntSort())
@ -1641,7 +1640,7 @@ class BoolRef(ExprRef):
def is_bool(a : Any) -> TypeGuard[BoolRef]: def is_bool(a : Any) -> bool:
"""Return `True` if `a` is a Z3 Boolean expression. """Return `True` if `a` is a Z3 Boolean expression.
>>> p = Bool('p') >>> p = Bool('p')
@ -1659,7 +1658,7 @@ def is_bool(a : Any) -> TypeGuard[BoolRef]:
return isinstance(a, BoolRef) return isinstance(a, BoolRef)
def is_true(a : Any) -> TypeGuard[BoolRef]: def is_true(a : Any) -> bool:
"""Return `True` if `a` is the Z3 true expression. """Return `True` if `a` is the Z3 true expression.
>>> p = Bool('p') >>> p = Bool('p')
@ -1677,7 +1676,7 @@ def is_true(a : Any) -> TypeGuard[BoolRef]:
return is_app_of(a, Z3_OP_TRUE) return is_app_of(a, Z3_OP_TRUE)
def is_false(a : Any) -> TypeGuard[BoolRef]: def is_false(a : Any) -> bool:
"""Return `True` if `a` is the Z3 false expression. """Return `True` if `a` is the Z3 false expression.
>>> p = Bool('p') >>> p = Bool('p')
@ -1691,7 +1690,7 @@ def is_false(a : Any) -> TypeGuard[BoolRef]:
return is_app_of(a, Z3_OP_FALSE) return is_app_of(a, Z3_OP_FALSE)
def is_and(a : Any) -> TypeGuard[BoolRef]: def is_and(a : Any) -> bool:
"""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')
@ -1703,7 +1702,7 @@ def is_and(a : Any) -> TypeGuard[BoolRef]:
return is_app_of(a, Z3_OP_AND) return is_app_of(a, Z3_OP_AND)
def is_or(a : Any) -> TypeGuard[BoolRef]: def is_or(a : Any) -> bool:
"""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')
@ -1715,7 +1714,7 @@ def is_or(a : Any) -> TypeGuard[BoolRef]:
return is_app_of(a, Z3_OP_OR) return is_app_of(a, Z3_OP_OR)
def is_implies(a : Any) -> TypeGuard[BoolRef]: def is_implies(a : Any) -> bool:
"""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')
@ -1727,7 +1726,7 @@ def is_implies(a : Any) -> TypeGuard[BoolRef]:
return is_app_of(a, Z3_OP_IMPLIES) return is_app_of(a, Z3_OP_IMPLIES)
def is_not(a : Any) -> TypeGuard[BoolRef]: def is_not(a : Any) -> bool:
"""Return `True` if `a` is a Z3 not expression. """Return `True` if `a` is a Z3 not expression.
>>> p = Bool('p') >>> p = Bool('p')
@ -1739,7 +1738,7 @@ def is_not(a : Any) -> TypeGuard[BoolRef]:
return is_app_of(a, Z3_OP_NOT) return is_app_of(a, Z3_OP_NOT)
def is_eq(a : Any) -> TypeGuard[BoolRef]: def is_eq(a : Any) -> bool:
"""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')
@ -1749,7 +1748,7 @@ def is_eq(a : Any) -> TypeGuard[BoolRef]:
return is_app_of(a, Z3_OP_EQ) return is_app_of(a, Z3_OP_EQ)
def is_distinct(a : Any) -> TypeGuard[BoolRef]: def is_distinct(a : Any) -> bool:
"""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')
@ -2444,7 +2443,7 @@ class ArithSortRef(SortRef):
_z3_assert(False, msg % self) _z3_assert(False, msg % self)
def is_arith_sort(s : Any) -> TypeGuard[ArithSortRef]: def is_arith_sort(s : Any) -> bool:
"""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())
@ -2766,7 +2765,7 @@ def is_arith(a):
return isinstance(a, ArithRef) return isinstance(a, ArithRef)
def is_int(a) -> TypeGuard[ArithRef]: def is_int(a) -> bool:
"""Return `True` if `a` is an integer expression. """Return `True` if `a` is an integer expression.
>>> x = Int('x') >>> x = Int('x')
@ -2872,7 +2871,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 : Any) -> TypeGuard[ArithRef]: def is_add(a : Any) -> bool:
"""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')
@ -2884,7 +2883,7 @@ def is_add(a : Any) -> TypeGuard[ArithRef]:
return is_app_of(a, Z3_OP_ADD) return is_app_of(a, Z3_OP_ADD)
def is_mul(a : Any) -> TypeGuard[ArithRef]: def is_mul(a : Any) -> bool:
"""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')
@ -2896,7 +2895,7 @@ def is_mul(a : Any) -> TypeGuard[ArithRef]:
return is_app_of(a, Z3_OP_MUL) return is_app_of(a, Z3_OP_MUL)
def is_sub(a : Any) -> TypeGuard[ArithRef]: def is_sub(a : Any) -> bool:
"""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')
@ -2908,7 +2907,7 @@ def is_sub(a : Any) -> TypeGuard[ArithRef]:
return is_app_of(a, Z3_OP_SUB) return is_app_of(a, Z3_OP_SUB)
def is_div(a : Any) -> TypeGuard[ArithRef]: def is_div(a : Any) -> bool:
"""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')
@ -2925,7 +2924,7 @@ def is_div(a : Any) -> TypeGuard[ArithRef]:
return is_app_of(a, Z3_OP_DIV) return is_app_of(a, Z3_OP_DIV)
def is_idiv(a : Any) -> TypeGuard[ArithRef]: def is_idiv(a : Any) -> bool:
"""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')
@ -2937,7 +2936,7 @@ def is_idiv(a : Any) -> TypeGuard[ArithRef]:
return is_app_of(a, Z3_OP_IDIV) return is_app_of(a, Z3_OP_IDIV)
def is_mod(a : Any) -> TypeGuard[ArithRef]: def is_mod(a : Any) -> bool:
"""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')
@ -2949,7 +2948,7 @@ def is_mod(a : Any) -> TypeGuard[ArithRef]:
return is_app_of(a, Z3_OP_MOD) return is_app_of(a, Z3_OP_MOD)
def is_le(a : Any) -> TypeGuard[ArithRef]: def is_le(a : Any) -> bool:
"""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')
@ -2961,7 +2960,7 @@ def is_le(a : Any) -> TypeGuard[ArithRef]:
return is_app_of(a, Z3_OP_LE) return is_app_of(a, Z3_OP_LE)
def is_lt(a : Any) -> TypeGuard[ArithRef]: def is_lt(a : Any) -> bool:
"""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')
@ -2973,7 +2972,7 @@ def is_lt(a : Any) -> TypeGuard[ArithRef]:
return is_app_of(a, Z3_OP_LT) return is_app_of(a, Z3_OP_LT)
def is_ge(a : Any) -> TypeGuard[ArithRef]: def is_ge(a : Any) -> bool:
"""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')
@ -2985,7 +2984,7 @@ def is_ge(a : Any) -> TypeGuard[ArithRef]:
return is_app_of(a, Z3_OP_GE) return is_app_of(a, Z3_OP_GE)
def is_gt(a : Any) -> TypeGuard[ArithRef]: def is_gt(a : Any) -> bool:
"""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')
@ -3009,7 +3008,7 @@ def is_is_int(a : Any) -> bool:
return is_app_of(a, Z3_OP_IS_INT) return is_app_of(a, Z3_OP_IS_INT)
def is_to_real(a : Any) -> TypeGuard[ArithRef]: def is_to_real(a : Any) -> bool:
"""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')
@ -3024,7 +3023,7 @@ def is_to_real(a : Any) -> TypeGuard[ArithRef]:
return is_app_of(a, Z3_OP_TO_REAL) return is_app_of(a, Z3_OP_TO_REAL)
def is_to_int(a : Any) -> TypeGuard[ArithRef]: def is_to_int(a : Any) -> bool:
"""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')
@ -4700,7 +4699,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 : Any) -> TypeGuard[ArrayRef]: def is_array(a : Any) -> bool:
"""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())
@ -11151,7 +11150,7 @@ def is_seq(a):
return isinstance(a, SeqRef) return isinstance(a, SeqRef)
def is_string(a: Any) -> TypeGuard[SeqRef]: def is_string(a: Any) -> bool:
"""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
@ -11159,7 +11158,7 @@ def is_string(a: Any) -> TypeGuard[SeqRef]:
return isinstance(a, SeqRef) and a.is_string() return isinstance(a, SeqRef) and a.is_string()
def is_string_value(a: Any) -> TypeGuard[SeqRef]: def is_string_value(a: Any) -> bool:
"""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