226 lines
7.2 KiB
Python
226 lines
7.2 KiB
Python
from typing import ClassVar, Literal, TypeVar, final
|
|
|
|
from typing_extensions import Generic, Self, TypeAlias
|
|
|
|
__version__: str
|
|
|
|
def parse_expr(expr_str: str) -> Expr: ...
|
|
|
|
class Expr: ...
|
|
|
|
class NumExpr(Expr):
|
|
def __ge__(self, other: Self) -> NumExpr: ...
|
|
def __gt__(self, other: Self) -> NumExpr: ...
|
|
def __le__(self, other: Self) -> NumExpr: ...
|
|
def __lt__(self, other: Self) -> NumExpr: ...
|
|
def __mul__(self, other: Self) -> NumExpr: ...
|
|
def __eq__(self, other: Self) -> NumExpr: ... # type: ignore[override]
|
|
def __ne__(self, other: Self) -> NumExpr: ... # type: ignore[override]
|
|
def __neg__(self) -> NumExpr: ...
|
|
def __add__(self, other: Self) -> NumExpr: ...
|
|
def __radd__(self, other: Self) -> NumExpr: ...
|
|
def __rmul__(self, other: Self) -> NumExpr: ...
|
|
def __sub__(self, other: Self) -> NumExpr: ...
|
|
def __rsub__(self, other: Self) -> NumExpr: ...
|
|
def __truediv__(self, other: Self) -> NumExpr: ...
|
|
def __rtruediv__(self, other: Self) -> NumExpr: ...
|
|
def __abs__(self) -> NumExpr: ...
|
|
|
|
@final
|
|
class ConstInt(NumExpr):
|
|
def __init__(self, value: int) -> None: ...
|
|
|
|
@final
|
|
class ConstUInt(NumExpr):
|
|
def __init__(self, value: int) -> None: ...
|
|
|
|
@final
|
|
class ConstFloat(NumExpr):
|
|
def __init__(self, value: float) -> None: ...
|
|
|
|
@final
|
|
class VarInt(NumExpr):
|
|
def __init__(self, name: str) -> None: ...
|
|
|
|
@final
|
|
class VarUInt(NumExpr):
|
|
def __init__(self, name: str) -> None: ...
|
|
|
|
@final
|
|
class VarFloat(NumExpr):
|
|
def __init__(self, name: str) -> None: ...
|
|
|
|
@final
|
|
class Negate(NumExpr):
|
|
def __init__(self, arg: NumExpr) -> None: ...
|
|
|
|
@final
|
|
class Add(NumExpr):
|
|
def __init__(self, args: list[NumExpr]) -> None: ...
|
|
|
|
@final
|
|
class Mul(NumExpr):
|
|
def __init__(self, args: list[NumExpr]) -> None: ...
|
|
|
|
@final
|
|
class Div(NumExpr):
|
|
def __init__(self, dividend: NumExpr, divisor: NumExpr) -> None: ...
|
|
|
|
@final
|
|
class Abs(NumExpr):
|
|
def __init__(self, arg: NumExpr) -> None: ...
|
|
|
|
class BoolExpr(Expr):
|
|
def __and__(self, other: Self) -> BoolExpr: ...
|
|
def __invert__(self) -> BoolExpr: ...
|
|
def __or__(self, other: Self) -> BoolExpr: ...
|
|
def __rand__(self, other: Self) -> BoolExpr: ...
|
|
def __ror__(self, other: Self) -> BoolExpr: ...
|
|
|
|
@final
|
|
class ConstBool(BoolExpr):
|
|
def __init__(self, value: bool) -> None: ...
|
|
|
|
@final
|
|
class VarBool(BoolExpr):
|
|
def __init__(self, name: str) -> None: ...
|
|
|
|
@final
|
|
class Cmp(BoolExpr):
|
|
@staticmethod
|
|
def equal(lhs: NumExpr, rhs: NumExpr) -> Cmp: ...
|
|
@staticmethod
|
|
def greater_than(lhs: NumExpr, rhs: NumExpr) -> Cmp: ...
|
|
@staticmethod
|
|
def greater_than_eq(lhs: NumExpr, rhs: NumExpr) -> Cmp: ...
|
|
@staticmethod
|
|
def less_than(lhs: NumExpr, rhs: NumExpr) -> Cmp: ...
|
|
@staticmethod
|
|
def less_than_eq(lhs: NumExpr, rhs: NumExpr) -> Cmp: ...
|
|
@staticmethod
|
|
def not_equal(lhs: NumExpr, rhs: NumExpr) -> Cmp: ...
|
|
|
|
@final
|
|
class Not(BoolExpr):
|
|
def __init__(self, arg: BoolExpr) -> None: ...
|
|
|
|
@final
|
|
class And(BoolExpr):
|
|
def __init__(self, args: list[BoolExpr]) -> None: ...
|
|
|
|
@final
|
|
class Or(BoolExpr):
|
|
def __init__(self, args: list[BoolExpr]) -> None: ...
|
|
|
|
@final
|
|
class Next(BoolExpr):
|
|
def __init__(self, arg: BoolExpr) -> None: ...
|
|
|
|
@final
|
|
class Oracle(BoolExpr):
|
|
def __init__(self, arg: BoolExpr, steps: int) -> None: ...
|
|
|
|
@final
|
|
class Always(BoolExpr):
|
|
def __init__(self, arg: BoolExpr, *, interval: tuple[float | None, float | None]) -> None: ...
|
|
|
|
@final
|
|
class Eventually(BoolExpr):
|
|
def __init__(self, arg: BoolExpr, *, interval: tuple[float | None, float | None]) -> None: ...
|
|
|
|
@final
|
|
class Until(BoolExpr):
|
|
def __init__(self, lhs: BoolExpr, rhs: BoolExpr, *, interval: tuple[float | None, float | None]) -> None: ...
|
|
|
|
@final
|
|
class dtype: # noqa: N801
|
|
bool_: ClassVar[dtype] = ...
|
|
float64: ClassVar[dtype] = ...
|
|
int64: ClassVar[dtype] = ...
|
|
uint64: ClassVar[dtype] = ...
|
|
|
|
@classmethod
|
|
def convert(cls, dtype: type[bool | int | float] | Self) -> Self: ... # noqa: Y041
|
|
def __eq__(self, other: object) -> bool: ...
|
|
def __int__(self) -> int: ...
|
|
|
|
_T = TypeVar("_T", bool, int, float)
|
|
|
|
class Signal(Generic[_T]):
|
|
def __init__(self, *, interpolation_method: _InterpolationMethod = "linear") -> None: ...
|
|
@classmethod
|
|
def constant(cls, value: _T, *, interpolation_method: _InterpolationMethod = "linear") -> Self: ...
|
|
@classmethod
|
|
def from_samples(
|
|
cls, samples: list[tuple[float, _T]], *, interpolation_method: _InterpolationMethod = "linear"
|
|
) -> Self: ...
|
|
def push(self, time: float, value: _T) -> None: ...
|
|
def at(self, time: float) -> _T | None: ...
|
|
def is_empty(self) -> bool: ...
|
|
@property
|
|
def start_time(self) -> float | None: ...
|
|
@property
|
|
def end_time(self) -> float | None: ...
|
|
@property
|
|
def kind(self) -> dtype: ...
|
|
|
|
@final
|
|
class BoolSignal(Signal[bool]):
|
|
def __init__(self, *, interpolation_method: _InterpolationMethod = "linear") -> None: ...
|
|
@classmethod
|
|
def constant(cls, value: bool, *, interpolation_method: _InterpolationMethod = "linear") -> Self: ...
|
|
@classmethod
|
|
def from_samples(
|
|
cls, samples: list[tuple[float, bool]], *, interpolation_method: _InterpolationMethod = "linear"
|
|
) -> Self: ...
|
|
def push(self, time: float, value: bool) -> None: ...
|
|
def at(self, time: float) -> bool | None: ...
|
|
|
|
_InterpolationMethod: TypeAlias = Literal["linear", "constant"]
|
|
|
|
@final
|
|
class IntSignal(Signal[int]):
|
|
def __init__(self, *, interpolation_method: _InterpolationMethod = "linear") -> None: ...
|
|
@classmethod
|
|
def constant(cls, value: int, *, interpolation_method: _InterpolationMethod = "linear") -> Self: ...
|
|
@classmethod
|
|
def from_samples(
|
|
cls, samples: list[tuple[float, int]], *, interpolation_method: _InterpolationMethod = "linear"
|
|
) -> Self: ...
|
|
def push(self, time: float, value: int) -> None: ...
|
|
def at(self, time: float) -> int | None: ...
|
|
|
|
@final
|
|
class UnsignedIntSignal(Signal[int]):
|
|
def __init__(self, *, interpolation_method: _InterpolationMethod = "linear") -> None: ...
|
|
@classmethod
|
|
def constant(cls, value: int, *, interpolation_method: _InterpolationMethod = "linear") -> Self: ...
|
|
@classmethod
|
|
def from_samples(
|
|
cls, samples: list[tuple[float, int]], *, interpolation_method: _InterpolationMethod = "linear"
|
|
) -> Self: ...
|
|
def push(self, time: float, value: int) -> None: ...
|
|
def at(self, time: float) -> int | None: ...
|
|
|
|
@final
|
|
class FloatSignal(Signal[float]):
|
|
def __init__(self, *, interpolation_method: _InterpolationMethod = "linear") -> None: ...
|
|
@classmethod
|
|
def constant(cls, value: float, *, interpolation_method: _InterpolationMethod = "linear") -> Self: ...
|
|
@classmethod
|
|
def from_samples(
|
|
cls, samples: list[tuple[float, float]], *, interpolation_method: _InterpolationMethod = "linear"
|
|
) -> Self: ...
|
|
def push(self, time: float, value: float) -> None: ...
|
|
def at(self, time: float) -> float | None: ...
|
|
|
|
@final
|
|
class Trace:
|
|
def __init__(self, signals: dict[str, Signal]) -> None: ...
|
|
|
|
def eval_bool_semantics(
|
|
expr: BoolExpr, trace: Trace, *, interpolation_method: _InterpolationMethod = "linear"
|
|
) -> BoolSignal: ...
|
|
def eval_robust_semantics(
|
|
expr: BoolExpr, trace: Trace, *, interpolation_method: _InterpolationMethod = "linear"
|
|
) -> BoolSignal: ...
|