diff --git a/lean_py/z3/_ast.py b/lean_py/z3/_ast.py index 858e2c9..dc73846 100644 --- a/lean_py/z3/_ast.py +++ b/lean_py/z3/_ast.py @@ -78,6 +78,16 @@ class InductiveASTSort: name: str +@dataclass(frozen=True) +class CharASTSort: + pass + + +@dataclass(frozen=True) +class SeqASTSort: + elem: ASTSort + + ASTSort = Union[ PropSort, IntASTSort, @@ -91,6 +101,8 @@ class InductiveASTSort: FpASTSort, FinDomainASTSort, InductiveASTSort, + CharASTSort, + SeqASTSort, ] # --------------------------------------------------------------------------- @@ -461,6 +473,81 @@ class InductiveRecognizerNode: arg: ASTNode +# --------------------------------------------------------------------------- +# Char expression nodes +# --------------------------------------------------------------------------- + + +@dataclass(frozen=True) +class CharLit: + val: int + + +@dataclass(frozen=True) +class CharToNatNode: + arg: ASTNode + + +@dataclass(frozen=True) +class CharFromBvNode: + arg: ASTNode + + +@dataclass(frozen=True) +class CharIsDigitNode: + arg: ASTNode + + +# --------------------------------------------------------------------------- +# Sequence expression nodes +# --------------------------------------------------------------------------- + + +@dataclass(frozen=True) +class SeqEmptyNode: + elem_sort: ASTSort + + +@dataclass(frozen=True) +class SeqUnitNode: + arg: ASTNode + + +@dataclass(frozen=True) +class SeqLenNode: + arg: ASTNode + + +@dataclass(frozen=True) +class SeqConcatNode: + lhs: ASTNode + rhs: ASTNode + + +@dataclass(frozen=True) +class SeqContainsNode: + haystack: ASTNode + needle: ASTNode + + +@dataclass(frozen=True) +class SeqPrefixOfNode: + prefix_: ASTNode + s: ASTNode + + +@dataclass(frozen=True) +class SeqSuffixOfNode: + suffix_: ASTNode + s: ASTNode + + +@dataclass(frozen=True) +class SeqNthNode: + s: ASTNode + idx: ASTNode + + ASTNode = Union[ Var, IntLit, @@ -511,6 +598,18 @@ class InductiveRecognizerNode: InductiveCtorNode, InductiveAccessorNode, InductiveRecognizerNode, + CharLit, + CharToNatNode, + CharFromBvNode, + CharIsDigitNode, + SeqEmptyNode, + SeqUnitNode, + SeqLenNode, + SeqConcatNode, + SeqContainsNode, + SeqPrefixOfNode, + SeqSuffixOfNode, + SeqNthNode, ] __all__ = [ @@ -585,5 +684,21 @@ class InductiveRecognizerNode: "InductiveCtorNode", "InductiveAccessorNode", "InductiveRecognizerNode", + # Char nodes + "CharASTSort", + "CharLit", + "CharToNatNode", + "CharFromBvNode", + "CharIsDigitNode", + # Seq nodes + "SeqASTSort", + "SeqEmptyNode", + "SeqUnitNode", + "SeqLenNode", + "SeqConcatNode", + "SeqContainsNode", + "SeqPrefixOfNode", + "SeqSuffixOfNode", + "SeqNthNode", "ASTNode", ] diff --git a/lean_py/z3/core.py b/lean_py/z3/core.py index f70f208..4786138 100644 --- a/lean_py/z3/core.py +++ b/lean_py/z3/core.py @@ -85,13 +85,28 @@ InductiveCtorNode, InductiveAccessorNode, InductiveRecognizerNode, + CharASTSort, + CharLit, + CharToNatNode, + CharFromBvNode, + CharIsDigitNode, + SeqASTSort, + SeqEmptyNode, + SeqUnitNode, + SeqLenNode, + SeqConcatNode, + SeqContainsNode, + SeqPrefixOfNode, + SeqSuffixOfNode, + SeqNthNode, ) def _is_literal(node: ASTNode) -> bool: """True for ground literal AST nodes (no variables/operations).""" return isinstance( - node, (IntLit, NatLit, BoolLit, BvLit, StringLit, FpLitNode, FinDomainLit) + node, + (IntLit, NatLit, BoolLit, BvLit, StringLit, FpLitNode, FinDomainLit, CharLit), ) @@ -1106,6 +1121,10 @@ def Const(name: str, sort: SortRef) -> ExprRef: return ArrayRef(_AstVar(name), sort, v) if isinstance(sort, StringSortRef): return StringRef(_AstVar(name), v) + if isinstance(sort, CharSortRef): + return CharRef(_AstVar(name), v) + if isinstance(sort, SeqSortRef): + return SeqRef(_AstVar(name), sort, v) if isinstance(sort, DatatypeSortRef): return DatatypeRef(_AstVar(name), sort, v) return ExprRef(_AstVar(name), sort, v) @@ -1133,6 +1152,9 @@ def RealVal(n: int | float | str) -> ArithRef: num, den = n.as_integer_ratio() return RatNumRef(num, den) if isinstance(n, str): + if "/" in n: + num, den = n.split("/", 1) + return RatNumRef(int(num.strip()), int(den.strip())) n = float(n) if "." in n or "e" in n.lower() else int(n) return RealVal(n) return ArithRef(ToRealNode(IntLit(n)), RealSort()) @@ -1481,6 +1503,10 @@ def _sort_repr(s: ASTSort) -> str: return f"({_sort_repr(s.dom)} \u2192 {_sort_repr(s.cod)})" if isinstance(s, InductiveASTSort): return s.name + if isinstance(s, CharASTSort): + return "Char" + if isinstance(s, SeqASTSort): + return f"(Seq {_sort_repr(s.elem)})" return str(s) @@ -2000,7 +2026,7 @@ def BVAddNoOverflow(a: BitVecRef, b: BitVecRef, signed: bool = False) -> BoolRef eb = ZeroExt(1, b) s = ea + eb upper = BitVecVal((1 << w) - 1, w + 1) - return s <= upper + return ULE(s, upper) def BVAddNoUnderflow(a: BitVecRef, b: BitVecRef) -> BoolRef: @@ -2062,7 +2088,7 @@ def BVMulNoOverflow(a: BitVecRef, b: BitVecRef, signed: bool = False) -> BoolRef eb = ZeroExt(w, b) p = ea * eb upper = BitVecVal((1 << w) - 1, 2 * w) - return p <= upper + return ULE(p, upper) def BVMulNoUnderflow(a: BitVecRef, b: BitVecRef) -> BoolRef: @@ -2295,23 +2321,31 @@ def StringVal(s: str) -> StringRef: return StringRef(StringLit(s)) -def Length(s: StringRef) -> ArithRef: - """String length.""" +def Length(s: StringRef | SeqRef) -> ArithRef: + """String or sequence length.""" + if isinstance(s, SeqRef): + return ArithRef(SeqLenNode(s._ast), IntSort(), s._vars) return ArithRef(StrLenNode(s._ast), IntSort(), s._vars) -def Contains(s: StringRef, t: StringRef) -> BoolRef: +def Contains(s: StringRef | SeqRef, t: StringRef | SeqRef) -> BoolRef: """Check if s contains t.""" + if isinstance(s, SeqRef) or isinstance(t, SeqRef): + return BoolRef(SeqContainsNode(s._ast, t._ast), _merge(s._vars, t._vars)) return BoolRef(StrContainsNode(s._ast, t._ast), _merge(s._vars, t._vars)) -def PrefixOf(pre: StringRef, s: StringRef) -> BoolRef: +def PrefixOf(pre: StringRef | SeqRef, s: StringRef | SeqRef) -> BoolRef: """Check if pre is a prefix of s.""" + if isinstance(pre, SeqRef) or isinstance(s, SeqRef): + return BoolRef(SeqPrefixOfNode(pre._ast, s._ast), _merge(pre._vars, s._vars)) return BoolRef(StrPrefixOfNode(pre._ast, s._ast), _merge(pre._vars, s._vars)) -def SuffixOf(suf: StringRef, s: StringRef) -> BoolRef: +def SuffixOf(suf: StringRef | SeqRef, s: StringRef | SeqRef) -> BoolRef: """Check if suf is a suffix of s.""" + if isinstance(suf, SeqRef) or isinstance(s, SeqRef): + return BoolRef(SeqSuffixOfNode(suf._ast, s._ast), _merge(suf._vars, s._vars)) return BoolRef(StrSuffixOfNode(suf._ast, s._ast), _merge(suf._vars, s._vars)) @@ -2697,6 +2731,28 @@ def _ast_children(node: ASTNode) -> list[ASTNode]: return [node.s, node.re] if isinstance(node, ReRangeNode): return [] + # Char nodes + if isinstance(node, CharLit): + return [] + if isinstance(node, (CharToNatNode, CharFromBvNode, CharIsDigitNode)): + return [node.arg] + # Seq nodes + if isinstance(node, SeqEmptyNode): + return [] + if isinstance(node, SeqUnitNode): + return [node.arg] + if isinstance(node, SeqLenNode): + return [node.arg] + if isinstance(node, SeqConcatNode): + return [node.lhs, node.rhs] + if isinstance(node, SeqContainsNode): + return [node.haystack, node.needle] + if isinstance(node, SeqPrefixOfNode): + return [node.prefix_, node.s] + if isinstance(node, SeqSuffixOfNode): + return [node.suffix_, node.s] + if isinstance(node, SeqNthNode): + return [node.s, node.idx] return [] @@ -2803,6 +2859,10 @@ def _make_typed_expr( return BitVecRef(ast, sort, vars) if isinstance(sort, StringSortRef): return StringRef(ast, vars) + if isinstance(sort, CharSortRef): + return CharRef(ast, vars) + if isinstance(sort, SeqSortRef): + return SeqRef(ast, sort, vars) return ExprRef(ast, sort, vars) @@ -2827,6 +2887,10 @@ def _sort_from_ast_sort(ast_sort: ASTSort) -> SortRef: ) if isinstance(ast_sort, UninterpASTSort): return UninterpretedSortRef(ast_sort) + if isinstance(ast_sort, CharASTSort): + return CharSortRef(ast_sort) + if isinstance(ast_sort, SeqASTSort): + return SeqSortRef(_sort_from_ast_sort(ast_sort.elem)) return SortRef(ast_sort) @@ -3795,38 +3859,73 @@ def is_finite_set_sort(s: object) -> bool: # --------------------------------------------------------------------------- -class _CharSortRef(SortRef): +class CharSortRef(SortRef): """Character sort.""" pass -def CharSort(ctx: Context | None = None) -> _CharSortRef: - return _CharSortRef(UninterpASTSort("Char")) +class CharRef(ExprRef): + """Character expression.""" + + __slots__ = () + + def __init__( + self, + ast: ASTNode, + vars: frozenset[tuple[str, ASTSort]] = frozenset(), + ) -> None: + super().__init__(ast, CharSortRef(CharASTSort()), vars) + + def to_int(self) -> ArithRef: + """Convert char to integer (code point).""" + return CharToInt(self) + + def to_bv(self) -> BitVecRef: + """Convert char to 21-bit bitvector.""" + return CharToBv(self) + + def is_digit(self) -> BoolRef: + """Check if char is a digit.""" + return CharIsDigit(self) + + def __le__(self, other: object) -> BoolRef: + if isinstance(other, ExprRef): + lhs = CharToNatNode(self._ast) + rhs = CharToNatNode(other._ast) + return BoolRef( + BinOpNode(BinOp.LE, lhs, rhs), + _merge(self._vars, other._vars), + ) + return NotImplemented + + +def CharSort(ctx: Context | None = None) -> CharSortRef: + return CharSortRef(CharASTSort()) -def CharVal(ch: str | int, ctx: Context | None = None) -> ExprRef: +def CharVal(ch: str | int, ctx: Context | None = None) -> CharRef: if isinstance(ch, str): ch = ord(ch[0]) if ch else 0 - return ExprRef(_AstVar(f"char_{ch}"), CharSort(), frozenset()) + return CharRef(CharLit(ch)) -def CharFromBv(bv: BitVecRef, ctx: Context | None = None) -> ExprRef: - return ExprRef(AppNode(_AstVar("char.from_bv"), (bv._ast,)), CharSort(), bv._vars) +def CharFromBv(bv: BitVecRef, ctx: Context | None = None) -> CharRef: + return CharRef(CharFromBvNode(bv._ast), bv._vars) def CharToBv(ch: ExprRef, ctx: Context | None = None) -> BitVecRef: return BitVecRef( - AppNode(_AstVar("char.to_bv"), (ch._ast,)), BitVecSort(8), ch._vars + CharToNatNode(ch._ast), BitVecSort(21), ch._vars ) def CharToInt(ch: ExprRef, ctx: Context | None = None) -> ArithRef: - return ArithRef(AppNode(_AstVar("char.to_int"), (ch._ast,)), IntSort(), ch._vars) + return ArithRef(CharToNatNode(ch._ast), IntSort(), ch._vars) def CharIsDigit(ch: ExprRef, ctx: Context | None = None) -> BoolRef: - return BoolRef(AppNode(_AstVar("char.is_digit"), (ch._ast,)), ch._vars) + return BoolRef(CharIsDigitNode(ch._ast), ch._vars) # --------------------------------------------------------------------------- @@ -3834,11 +3933,72 @@ def CharIsDigit(ch: ExprRef, ctx: Context | None = None) -> BoolRef: # --------------------------------------------------------------------------- -def SeqSort(s: SortRef) -> SortRef: +class SeqSortRef(SortRef): + """Sequence sort.""" + + __slots__ = ("_elem",) + + def __init__(self, elem: SortRef) -> None: + super().__init__(SeqASTSort(elem._ast_sort)) + self._elem = elem + + def basis(self) -> SortRef: + """Return the element sort.""" + return self._elem + + def is_string(self) -> bool: + """True if this is Seq(Char), i.e. String.""" + return isinstance(self._elem, CharSortRef) + + +class SeqRef(ExprRef): + """Sequence expression.""" + + __slots__ = () + + def __init__( + self, + ast: ASTNode, + sort: SeqSortRef, + vars: frozenset[tuple[str, ASTSort]] = frozenset(), + ) -> None: + super().__init__(ast, sort, vars) + + def __add__(self, other: SeqRef) -> SeqRef: + if not isinstance(other, SeqRef): + return NotImplemented + return SeqRef( + SeqConcatNode(self._ast, other._ast), + self._sort, # type: ignore[arg-type] + _merge(self._vars, other._vars), + ) + + def __getitem__(self, idx: ArithRef | int) -> ExprRef: + if isinstance(idx, int): + idx = IntVal(idx) + sort = self._sort + elem_sort = sort._elem if isinstance(sort, SeqSortRef) else IntSort() + return ExprRef( + SeqNthNode(self._ast, idx._ast), + elem_sort, + _merge(self._vars, idx._vars), + ) + + def at(self, idx: ArithRef | int) -> SeqRef: + """Return a unit sequence at the given index.""" + elem = self[idx] + return Unit(elem) + + def is_string(self) -> bool: + sort = self._sort + return isinstance(sort, SeqSortRef) and sort.is_string() + + +def SeqSort(s: SortRef) -> SeqSortRef | StringSortRef: """General sequence sort. For Char, returns StringSort.""" - if isinstance(s, _CharSortRef): + if isinstance(s, CharSortRef): return StringSort() - return SortRef(UninterpASTSort(f"Seq_{s.name()}")) + return SeqSortRef(s) def Empty(s: SortRef) -> ExprRef: @@ -3847,6 +4007,8 @@ def Empty(s: SortRef) -> ExprRef: return StringVal("") if isinstance(s, ArraySortRef): return EmptySet(s.domain()) + if isinstance(s, SeqSortRef): + return SeqRef(SeqEmptyNode(s._elem._ast_sort), s) return StringVal("") @@ -3861,7 +4023,9 @@ def Unit(e: ExprRef) -> ExprRef: """Single-element sequence.""" if isinstance(e, StringRef): return e - return ExprRef(AppNode(_AstVar("seq.unit"), (e._ast,)), e._sort, e._vars) + if isinstance(e, CharRef): + return e + return SeqRef(SeqUnitNode(e._ast), SeqSortRef(e._sort), e._vars) def SubSeq(s: StringRef, lo: ArithRef | int, length: ArithRef | int) -> StringRef: @@ -4690,6 +4854,10 @@ def PropagateFunction(name: str, *sorts: SortRef) -> FuncDeclRef: "ArraySortRef", "StringSortRef", "ReSort", + "CharSortRef", + "CharRef", + "SeqSortRef", + "SeqRef", "BoolSort", "IntSort", "NatSort", diff --git a/lean_py/z3/solver.py b/lean_py/z3/solver.py index 0bb25d1..f6b23d0 100644 --- a/lean_py/z3/solver.py +++ b/lean_py/z3/solver.py @@ -86,6 +86,20 @@ InductiveCtorNode, InductiveAccessorNode, InductiveRecognizerNode, + CharASTSort, + CharLit, + CharToNatNode, + CharFromBvNode, + CharIsDigitNode, + SeqASTSort, + SeqEmptyNode, + SeqUnitNode, + SeqLenNode, + SeqConcatNode, + SeqContainsNode, + SeqPrefixOfNode, + SeqSuffixOfNode, + SeqNthNode, ) from lean_py.z3.core import ( And, @@ -188,6 +202,11 @@ def _marshal_sort(lib: Any, sort: ASTSort) -> Any: return Z3Sort.arrow(dom, cod) if isinstance(sort, InductiveASTSort): return Z3Sort.inductive_(sort.name) + if isinstance(sort, CharASTSort): + return Z3Sort.char + if isinstance(sort, SeqASTSort): + elem = _marshal_sort(lib, sort.elem) + return Z3Sort.seq(elem) raise TypeError(f"Unknown ASTSort: {type(sort)}") @@ -376,6 +395,48 @@ def _marshal_expr(lib: Any, node: ASTNode) -> Any: if isinstance(node, InductiveRecognizerNode): arg = _marshal_expr(lib, node.arg) return Z3Expr.inductiveRecognizer(node.type_name, node.recognizer_name, arg) + # Char nodes + if isinstance(node, CharLit): + return Z3Expr.charLit(node.val) + if isinstance(node, CharToNatNode): + arg = _marshal_expr(lib, node.arg) + return Z3Expr.charToNat(arg) + if isinstance(node, CharFromBvNode): + arg = _marshal_expr(lib, node.arg) + return Z3Expr.charFromBv(arg) + if isinstance(node, CharIsDigitNode): + arg = _marshal_expr(lib, node.arg) + return Z3Expr.charIsDigit(arg) + # Seq nodes + if isinstance(node, SeqEmptyNode): + elem_sort = _marshal_sort(lib, node.elem_sort) + return Z3Expr.seqEmpty(elem_sort) + if isinstance(node, SeqUnitNode): + arg = _marshal_expr(lib, node.arg) + return Z3Expr.seqUnit(arg) + if isinstance(node, SeqLenNode): + arg = _marshal_expr(lib, node.arg) + return Z3Expr.seqLen(arg) + if isinstance(node, SeqConcatNode): + lhs = _marshal_expr(lib, node.lhs) + rhs = _marshal_expr(lib, node.rhs) + return Z3Expr.seqConcat(lhs, rhs) + if isinstance(node, SeqContainsNode): + a = _marshal_expr(lib, node.haystack) + b = _marshal_expr(lib, node.needle) + return Z3Expr.seqContains(a, b) + if isinstance(node, SeqPrefixOfNode): + a = _marshal_expr(lib, node.prefix_) + b = _marshal_expr(lib, node.s) + return Z3Expr.seqPrefixOf(a, b) + if isinstance(node, SeqSuffixOfNode): + a = _marshal_expr(lib, node.suffix_) + b = _marshal_expr(lib, node.s) + return Z3Expr.seqSuffixOf(a, b) + if isinstance(node, SeqNthNode): + a = _marshal_expr(lib, node.s) + b = _marshal_expr(lib, node.idx) + return Z3Expr.seqNth(a, b) raise TypeError(f"Unknown ASTNode: {type(node)}") diff --git a/tests/test_z3_compat.py b/tests/test_z3_compat.py index d46e650..8a1994b 100644 --- a/tests/test_z3_compat.py +++ b/tests/test_z3_compat.py @@ -156,6 +156,35 @@ RNE, RealVal, Reals, + BVAddNoOverflow, + BVMulNoOverflow, + fpIsPositive, + fpIsNegative, + CharSort, + CharSortRef, + CharVal, + CharRef, + CharFromBv, + CharToBv, + CharToInt, + CharIsDigit, + SeqSort, + SeqSortRef, + SeqRef, + Empty, + Unit, + SetSort, + EmptySet, + FullSet, + SetAdd, + SetDel, + IsMember, + SetUnion, + SetIntersect, + SetComplement, + SetDifference, + IsSubset, + ArrayRef, ) from lean_py.z3._ast import ( BinOp, @@ -1778,3 +1807,309 @@ def test_int_to_real_ground(self, kernel): """ToReal(3) == ToReal(3).""" claim = ToReal(IntVal(3)) == ToReal(IntVal(3)) assert _try_prove(claim) + + +# ------------------------------------------------------------------ +# Bug fix tests +# ------------------------------------------------------------------ + + +class TestBugFixes: + """Tests for specific bug fixes.""" + + def test_inttostr_negative(self, kernel): + """IntToStr(-5) should return empty string per SMT-LIB spec.""" + claim = IntToStr(IntVal(-5)) == StringVal("") + assert _try_prove(claim) + + def test_bv_add_no_overflow_unsigned(self, kernel): + """BVAddNoOverflow unsigned: 200 + 100 overflows 8-bit.""" + from lean_py.z3 import BVAddNoOverflow + + a = BitVecVal(200, 8) + b = BitVecVal(100, 8) + # 200 + 100 = 300 > 255, so no-overflow should be False + overflow_check = Not(BVAddNoOverflow(a, b, signed=False)) + assert _try_prove(overflow_check) + + def test_bv_mul_no_overflow_unsigned(self, kernel): + """BVMulNoOverflow unsigned: 200 * 2 overflows 8-bit.""" + from lean_py.z3 import BVMulNoOverflow + + a = BitVecVal(200, 8) + b = BitVecVal(2, 8) + # 200 * 2 = 400 > 255, so no-overflow should be False + overflow_check = Not(BVMulNoOverflow(a, b, signed=False)) + assert _try_prove(overflow_check) + + def test_fp_is_positive_zero(self, kernel): + """fpIsPositive(+0.0) should be True.""" + from lean_py.z3 import fpIsPositive + + claim = fpIsPositive(FPVal(0.0, Float64())) + assert _try_prove(claim) + + def test_fp_is_negative_neg_zero(self, kernel): + """fpIsNegative(-0.0) should be True.""" + from lean_py.z3 import fpIsNegative + + claim = fpIsNegative(FPVal(-0.0, Float64())) + assert _try_prove(claim) + + +# ------------------------------------------------------------------ +# Char tests +# ------------------------------------------------------------------ + + +class TestChar: + """Tests for Char sort and operations.""" + + def test_char_sort_creation(self): + """CharSort() creates the char sort.""" + from lean_py.z3 import CharSort, CharSortRef + + s = CharSort() + assert isinstance(s, CharSortRef) + + def test_char_val_from_str(self): + """CharVal creates a char literal from string.""" + from lean_py.z3 import CharVal, CharRef + + c = CharVal("A") + assert isinstance(c, CharRef) + + def test_char_val_from_int(self): + """CharVal creates a char literal from int.""" + from lean_py.z3 import CharVal, CharRef + + c = CharVal(65) + assert isinstance(c, CharRef) + + def test_char_to_int(self): + """CharToInt returns ArithRef.""" + from lean_py.z3 import CharVal, CharToInt + + from lean_py.z3.core import ArithRef + + c = CharVal("A") + i = CharToInt(c) + assert isinstance(i, ArithRef) + + def test_char_to_bv(self): + """CharToBv returns BitVecRef.""" + from lean_py.z3 import CharVal, CharToBv + + c = CharVal("A") + bv = CharToBv(c) + assert isinstance(bv, BitVecRef) + + def test_char_is_digit(self): + """CharIsDigit returns BoolRef.""" + from lean_py.z3 import CharVal, CharIsDigit + from lean_py.z3.core import BoolRef + + c = CharVal("5") + d = CharIsDigit(c) + assert isinstance(d, BoolRef) + + def test_char_to_int_semantic(self, kernel): + """CharToInt(CharVal('A')) == 65.""" + from lean_py.z3 import CharVal, CharToInt + + claim = CharToInt(CharVal("A")) == IntVal(65) + assert _try_prove(claim) + + def test_char_const(self): + """Const with CharSort creates CharRef.""" + from lean_py.z3 import CharSort, CharRef + + c = Const("c", CharSort()) + assert isinstance(c, CharRef) + + +# ------------------------------------------------------------------ +# Set tests +# ------------------------------------------------------------------ + + +class TestSets: + """Tests for Set sort and operations.""" + + def test_set_sort_creation(self): + """SetSort creates ArraySortRef.""" + from lean_py.z3 import SetSort, ArraySortRef + + s = SetSort(IntSort()) + assert isinstance(s, ArraySortRef) + + def test_empty_set(self): + """EmptySet creates an array expression.""" + from lean_py.z3 import EmptySet, ArrayRef + + s = EmptySet(IntSort()) + assert isinstance(s, ArrayRef) + + def test_full_set(self): + """FullSet creates an array expression.""" + from lean_py.z3 import FullSet, ArrayRef + + s = FullSet(IntSort()) + assert isinstance(s, ArrayRef) + + def test_set_add(self): + """SetAdd adds element to set.""" + from lean_py.z3 import SetAdd, EmptySet, ArrayRef + + s = SetAdd(EmptySet(IntSort()), IntVal(1)) + assert isinstance(s, ArrayRef) + + def test_is_member(self): + """IsMember tests membership.""" + from lean_py.z3 import IsMember, SetAdd, EmptySet, BoolRef + + s = SetAdd(EmptySet(IntSort()), IntVal(1)) + m = IsMember(IntVal(1), s) + assert isinstance(m, BoolRef) + + def test_is_member_semantic(self, kernel): + """IsMember(1, SetAdd(EmptySet, 1)) is provable.""" + from lean_py.z3 import IsMember, SetAdd, EmptySet + + claim = IsMember(IntVal(1), SetAdd(EmptySet(IntSort()), IntVal(1))) + assert _try_prove(claim) + + def test_set_union(self): + """SetUnion creates an array expression.""" + from lean_py.z3 import SetUnion, EmptySet, SetAdd, ArrayRef + + a = SetAdd(EmptySet(IntSort()), IntVal(1)) + b = SetAdd(EmptySet(IntSort()), IntVal(2)) + u = SetUnion(a, b) + assert isinstance(u, ExprRef) + + def test_set_intersect(self): + """SetIntersect creates an array expression.""" + from lean_py.z3 import SetIntersect, EmptySet, SetAdd + + a = SetAdd(EmptySet(IntSort()), IntVal(1)) + b = SetAdd(EmptySet(IntSort()), IntVal(1)) + i = SetIntersect(a, b) + assert isinstance(i, ExprRef) + + def test_set_complement(self): + """SetComplement creates an array expression.""" + from lean_py.z3 import SetComplement, EmptySet + + s = SetComplement(EmptySet(IntSort())) + assert isinstance(s, ExprRef) + + def test_set_difference(self): + """SetDifference creates an array expression.""" + from lean_py.z3 import SetDifference, EmptySet, SetAdd + + a = SetAdd(EmptySet(IntSort()), IntVal(1)) + b = EmptySet(IntSort()) + d = SetDifference(a, b) + assert isinstance(d, ExprRef) + + def test_is_subset(self): + """IsSubset creates a BoolRef.""" + from lean_py.z3 import IsSubset, EmptySet, SetAdd, BoolRef + + a = EmptySet(IntSort()) + b = SetAdd(EmptySet(IntSort()), IntVal(1)) + s = IsSubset(a, b) + assert isinstance(s, BoolRef) + + +# ------------------------------------------------------------------ +# Sequence tests +# ------------------------------------------------------------------ + + +class TestSequences: + """Tests for Sequence sort and operations.""" + + def test_seq_sort_creation(self): + """SeqSort creates a SeqSortRef.""" + from lean_py.z3 import SeqSort, SeqSortRef + + s = SeqSort(IntSort()) + assert isinstance(s, SeqSortRef) + + def test_seq_sort_char_is_string(self): + """SeqSort(CharSort()) returns StringSort.""" + from lean_py.z3 import SeqSort, CharSort + + s = SeqSort(CharSort()) + assert isinstance(s, StringSortRef) + + def test_empty_seq(self): + """Empty(SeqSort) creates a SeqRef.""" + from lean_py.z3 import SeqSort, SeqRef, Empty + + s = SeqSort(IntSort()) + e = Empty(s) + assert isinstance(e, SeqRef) + + def test_unit_seq(self): + """Unit creates a SeqRef from a non-string element.""" + from lean_py.z3 import Unit, SeqRef + + u = Unit(IntVal(42)) + assert isinstance(u, SeqRef) + + def test_seq_concat(self): + """Sequence concatenation via + operator.""" + from lean_py.z3 import SeqSort, SeqRef, Empty, Unit + + s1 = Unit(IntVal(1)) + s2 = Unit(IntVal(2)) + assert isinstance(s1, SeqRef) + assert isinstance(s2, SeqRef) + s3 = s1 + s2 + assert isinstance(s3, SeqRef) + + def test_seq_length(self): + """Length works on SeqRef.""" + from lean_py.z3 import Unit, SeqRef + from lean_py.z3.core import ArithRef + + s = Unit(IntVal(42)) + l = Length(s) + assert isinstance(l, ArithRef) + + def test_seq_contains(self): + """Contains works on SeqRef.""" + from lean_py.z3 import Unit, SeqRef, BoolRef + + s = Unit(IntVal(1)) + t = Unit(IntVal(1)) + c = Contains(s, t) + assert isinstance(c, BoolRef) + + def test_seq_prefix_of(self): + """PrefixOf works on SeqRef.""" + from lean_py.z3 import Unit, SeqRef, BoolRef + + s = Unit(IntVal(1)) + t = Unit(IntVal(1)) + p = PrefixOf(s, t) + assert isinstance(p, BoolRef) + + def test_seq_suffix_of(self): + """SuffixOf works on SeqRef.""" + from lean_py.z3 import Unit, SeqRef, BoolRef + + s = Unit(IntVal(1)) + t = Unit(IntVal(1)) + su = SuffixOf(s, t) + assert isinstance(su, BoolRef) + + def test_seq_const(self): + """Const with SeqSort creates SeqRef.""" + from lean_py.z3 import SeqSort, SeqRef + + s = Const("s", SeqSort(IntSort())) + assert isinstance(s, SeqRef) diff --git a/tests/test_z3_ported.py b/tests/test_z3_ported.py index eba92b3..aeb3657 100644 --- a/tests/test_z3_ported.py +++ b/tests/test_z3_ported.py @@ -1852,6 +1852,18 @@ def test_realval_int(self): v = RealVal(5) assert is_real(v) + def test_realval_fraction_string(self): + v = RealVal("1/2") + assert isinstance(v, RatNumRef) + assert v.numerator().as_long() == 1 + assert v.denominator().as_long() == 2 + + def test_realval_fraction_string_large(self): + v = RealVal("355/113") + assert isinstance(v, RatNumRef) + assert v.numerator().as_long() == 355 + assert v.denominator().as_long() == 113 + def test_boolval(self): assert isinstance(BoolVal(True)._ast, BoolLit) assert isinstance(BoolVal(False)._ast, BoolLit) diff --git a/uv.lock b/uv.lock index f3125a8..65d9526 100644 --- a/uv.lock +++ b/uv.lock @@ -169,6 +169,7 @@ dependencies = [ [package.optional-dependencies] docs = [ + { name = "myst-parser" }, { name = "sphinx" }, { name = "sphinx-autodoc-typehints" }, { name = "sphinx-rtd-theme" }, @@ -181,6 +182,7 @@ dev = [ [package.metadata] requires-dist = [ + { name = "myst-parser", marker = "extra == 'docs'" }, { name = "pycparser", specifier = ">=2.22" }, { name = "sphinx", marker = "extra == 'docs'" }, { name = "sphinx-autodoc-typehints", marker = "extra == 'docs'" }, @@ -191,6 +193,18 @@ provides-extras = ["docs"] [package.metadata.requires-dev] dev = [{ name = "pytest", specifier = ">=8.0" }] +[[package]] +name = "markdown-it-py" +version = "4.2.0" +source = { registry = "https://pypi.org/simple" } +dependencies = [ + { name = "mdurl" }, +] +sdist = { url = "https://files.pythonhosted.org/packages/06/ff/7841249c247aa650a76b9ee4bbaeae59370dc8bfd2f6c01f3630c35eb134/markdown_it_py-4.2.0.tar.gz", hash = "sha256:04a21681d6fbb623de53f6f364d352309d4094dd4194040a10fd51833e418d49", size = 82454, upload-time = "2026-05-07T12:08:28.36Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/b3/81/4da04ced5a082363ecfa159c010d200ecbd959ae410c10c0264a38cac0f5/markdown_it_py-4.2.0-py3-none-any.whl", hash = "sha256:9f7ebbcd14fe59494226453aed97c1070d83f8d24b6fc3a3bcf9a38092641c4a", size = 91687, upload-time = "2026-05-07T12:08:27.182Z" }, +] + [[package]] name = "markupsafe" version = "3.0.3" @@ -254,6 +268,44 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/70/bc/6f1c2f612465f5fa89b95bead1f44dcb607670fd42891d8fdcd5d039f4f4/markupsafe-3.0.3-cp314-cp314t-win_arm64.whl", hash = "sha256:32001d6a8fc98c8cb5c947787c5d08b0a50663d139f1305bac5885d98d9b40fa", size = 14146, upload-time = "2025-09-27T18:37:28.327Z" }, ] +[[package]] +name = "mdit-py-plugins" +version = "0.6.1" +source = { registry = "https://pypi.org/simple" } +dependencies = [ + { name = "markdown-it-py" }, +] +sdist = { url = "https://files.pythonhosted.org/packages/59/fc/f8d0863f8862f25602c0404d75568e89fb6b4109804645e5cdfb1be5cf56/mdit_py_plugins-0.6.1.tar.gz", hash = "sha256:a2bca0f039f39dbd35fb74ae1b5f998608c437463371f0ff7f49a19a17a114d0", size = 56114, upload-time = "2026-05-13T09:03:38.91Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/a5/69/6da5581c6a7fede7dc261bf4e67d6adca4196f176b43288b55b3db395b6e/mdit_py_plugins-0.6.1-py3-none-any.whl", hash = "sha256:214c82fb2ac524472ab6a5bcab1de80f73b50443e187f401bfd77efbc7c6481d", size = 66663, upload-time = "2026-05-13T09:03:37.76Z" }, +] + +[[package]] +name = "mdurl" +version = "0.1.2" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/d6/54/cfe61301667036ec958cb99bd3efefba235e65cdeb9c84d24a8293ba1d90/mdurl-0.1.2.tar.gz", hash = "sha256:bb413d29f5eea38f31dd4754dd7377d4465116fb207585f97bf925588687c1ba", size = 8729, upload-time = "2022-08-14T12:40:10.846Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/b3/38/89ba8ad64ae25be8de66a6d463314cf1eb366222074cfda9ee839c56a4b4/mdurl-0.1.2-py3-none-any.whl", hash = "sha256:84008a41e51615a49fc9966191ff91509e3c40b939176e643fd50a5c2196b8f8", size = 9979, upload-time = "2022-08-14T12:40:09.779Z" }, +] + +[[package]] +name = "myst-parser" +version = "5.1.0" +source = { registry = "https://pypi.org/simple" } +dependencies = [ + { name = "docutils" }, + { name = "jinja2" }, + { name = "markdown-it-py" }, + { name = "mdit-py-plugins" }, + { name = "pyyaml" }, + { name = "sphinx" }, +] +sdist = { url = "https://files.pythonhosted.org/packages/21/dc/603751677fff302f34396e206b610f556a59d7fe58b9a2145f54e96b48e8/myst_parser-5.1.0.tar.gz", hash = "sha256:ab69322dc6719dcc7f296479dbb70181b66df6ed315064f92dbc85c0e1bf2f02", size = 101182, upload-time = "2026-05-13T09:38:19.361Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/09/dc/f3dfb7488b770f3f67e6545085bf2abea5172e88f57b8ad25ef860ca704c/myst_parser-5.1.0-py3-none-any.whl", hash = "sha256:9c91c52b3cdb4d94a6506e4fab4e2f296c7623a0da0dcbe6de1565c3dad67a8a", size = 85817, upload-time = "2026-05-13T09:38:17.904Z" }, +] + [[package]] name = "packaging" version = "26.2" @@ -306,6 +358,52 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/d4/24/a372aaf5c9b7208e7112038812994107bc65a84cd00e0354a88c2c77a617/pytest-9.0.3-py3-none-any.whl", hash = "sha256:2c5efc453d45394fdd706ade797c0a81091eccd1d6e4bccfcd476e2b8e0ab5d9", size = 375249, upload-time = "2026-04-07T17:16:16.13Z" }, ] +[[package]] +name = "pyyaml" +version = "6.0.3" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/05/8e/961c0007c59b8dd7729d542c61a4d537767a59645b82a0b521206e1e25c2/pyyaml-6.0.3.tar.gz", hash = "sha256:d76623373421df22fb4cf8817020cbb7ef15c725b9d5e45f17e189bfc384190f", size = 130960, upload-time = "2025-09-25T21:33:16.546Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/d1/33/422b98d2195232ca1826284a76852ad5a86fe23e31b009c9886b2d0fb8b2/pyyaml-6.0.3-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:7f047e29dcae44602496db43be01ad42fc6f1cc0d8cd6c83d342306c32270196", size = 182063, upload-time = "2025-09-25T21:32:11.445Z" }, + { url = "https://files.pythonhosted.org/packages/89/a0/6cf41a19a1f2f3feab0e9c0b74134aa2ce6849093d5517a0c550fe37a648/pyyaml-6.0.3-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:fc09d0aa354569bc501d4e787133afc08552722d3ab34836a80547331bb5d4a0", size = 173973, upload-time = "2025-09-25T21:32:12.492Z" }, + { url = "https://files.pythonhosted.org/packages/ed/23/7a778b6bd0b9a8039df8b1b1d80e2e2ad78aa04171592c8a5c43a56a6af4/pyyaml-6.0.3-cp312-cp312-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:9149cad251584d5fb4981be1ecde53a1ca46c891a79788c0df828d2f166bda28", size = 775116, upload-time = "2025-09-25T21:32:13.652Z" }, + { url = "https://files.pythonhosted.org/packages/65/30/d7353c338e12baef4ecc1b09e877c1970bd3382789c159b4f89d6a70dc09/pyyaml-6.0.3-cp312-cp312-manylinux2014_s390x.manylinux_2_17_s390x.manylinux_2_28_s390x.whl", hash = "sha256:5fdec68f91a0c6739b380c83b951e2c72ac0197ace422360e6d5a959d8d97b2c", size = 844011, upload-time = "2025-09-25T21:32:15.21Z" }, + { url = "https://files.pythonhosted.org/packages/8b/9d/b3589d3877982d4f2329302ef98a8026e7f4443c765c46cfecc8858c6b4b/pyyaml-6.0.3-cp312-cp312-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:ba1cc08a7ccde2d2ec775841541641e4548226580ab850948cbfda66a1befcdc", size = 807870, upload-time = "2025-09-25T21:32:16.431Z" }, + { url = "https://files.pythonhosted.org/packages/05/c0/b3be26a015601b822b97d9149ff8cb5ead58c66f981e04fedf4e762f4bd4/pyyaml-6.0.3-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:8dc52c23056b9ddd46818a57b78404882310fb473d63f17b07d5c40421e47f8e", size = 761089, upload-time = "2025-09-25T21:32:17.56Z" }, + { url = "https://files.pythonhosted.org/packages/be/8e/98435a21d1d4b46590d5459a22d88128103f8da4c2d4cb8f14f2a96504e1/pyyaml-6.0.3-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:41715c910c881bc081f1e8872880d3c650acf13dfa8214bad49ed4cede7c34ea", size = 790181, upload-time = "2025-09-25T21:32:18.834Z" }, + { url = "https://files.pythonhosted.org/packages/74/93/7baea19427dcfbe1e5a372d81473250b379f04b1bd3c4c5ff825e2327202/pyyaml-6.0.3-cp312-cp312-win32.whl", hash = "sha256:96b533f0e99f6579b3d4d4995707cf36df9100d67e0c8303a0c55b27b5f99bc5", size = 137658, upload-time = "2025-09-25T21:32:20.209Z" }, + { url = "https://files.pythonhosted.org/packages/86/bf/899e81e4cce32febab4fb42bb97dcdf66bc135272882d1987881a4b519e9/pyyaml-6.0.3-cp312-cp312-win_amd64.whl", hash = "sha256:5fcd34e47f6e0b794d17de1b4ff496c00986e1c83f7ab2fb8fcfe9616ff7477b", size = 154003, upload-time = "2025-09-25T21:32:21.167Z" }, + { url = "https://files.pythonhosted.org/packages/1a/08/67bd04656199bbb51dbed1439b7f27601dfb576fb864099c7ef0c3e55531/pyyaml-6.0.3-cp312-cp312-win_arm64.whl", hash = "sha256:64386e5e707d03a7e172c0701abfb7e10f0fb753ee1d773128192742712a98fd", size = 140344, upload-time = "2025-09-25T21:32:22.617Z" }, + { url = "https://files.pythonhosted.org/packages/d1/11/0fd08f8192109f7169db964b5707a2f1e8b745d4e239b784a5a1dd80d1db/pyyaml-6.0.3-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:8da9669d359f02c0b91ccc01cac4a67f16afec0dac22c2ad09f46bee0697eba8", size = 181669, upload-time = "2025-09-25T21:32:23.673Z" }, + { url = "https://files.pythonhosted.org/packages/b1/16/95309993f1d3748cd644e02e38b75d50cbc0d9561d21f390a76242ce073f/pyyaml-6.0.3-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:2283a07e2c21a2aa78d9c4442724ec1eb15f5e42a723b99cb3d822d48f5f7ad1", size = 173252, upload-time = "2025-09-25T21:32:25.149Z" }, + { url = "https://files.pythonhosted.org/packages/50/31/b20f376d3f810b9b2371e72ef5adb33879b25edb7a6d072cb7ca0c486398/pyyaml-6.0.3-cp313-cp313-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:ee2922902c45ae8ccada2c5b501ab86c36525b883eff4255313a253a3160861c", size = 767081, upload-time = "2025-09-25T21:32:26.575Z" }, + { url = "https://files.pythonhosted.org/packages/49/1e/a55ca81e949270d5d4432fbbd19dfea5321eda7c41a849d443dc92fd1ff7/pyyaml-6.0.3-cp313-cp313-manylinux2014_s390x.manylinux_2_17_s390x.manylinux_2_28_s390x.whl", hash = "sha256:a33284e20b78bd4a18c8c2282d549d10bc8408a2a7ff57653c0cf0b9be0afce5", size = 841159, upload-time = "2025-09-25T21:32:27.727Z" }, + { url = "https://files.pythonhosted.org/packages/74/27/e5b8f34d02d9995b80abcef563ea1f8b56d20134d8f4e5e81733b1feceb2/pyyaml-6.0.3-cp313-cp313-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:0f29edc409a6392443abf94b9cf89ce99889a1dd5376d94316ae5145dfedd5d6", size = 801626, upload-time = "2025-09-25T21:32:28.878Z" }, + { url = "https://files.pythonhosted.org/packages/f9/11/ba845c23988798f40e52ba45f34849aa8a1f2d4af4b798588010792ebad6/pyyaml-6.0.3-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:f7057c9a337546edc7973c0d3ba84ddcdf0daa14533c2065749c9075001090e6", size = 753613, upload-time = "2025-09-25T21:32:30.178Z" }, + { url = "https://files.pythonhosted.org/packages/3d/e0/7966e1a7bfc0a45bf0a7fb6b98ea03fc9b8d84fa7f2229e9659680b69ee3/pyyaml-6.0.3-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:eda16858a3cab07b80edaf74336ece1f986ba330fdb8ee0d6c0d68fe82bc96be", size = 794115, upload-time = "2025-09-25T21:32:31.353Z" }, + { url = "https://files.pythonhosted.org/packages/de/94/980b50a6531b3019e45ddeada0626d45fa85cbe22300844a7983285bed3b/pyyaml-6.0.3-cp313-cp313-win32.whl", hash = "sha256:d0eae10f8159e8fdad514efdc92d74fd8d682c933a6dd088030f3834bc8e6b26", size = 137427, upload-time = "2025-09-25T21:32:32.58Z" }, + { url = "https://files.pythonhosted.org/packages/97/c9/39d5b874e8b28845e4ec2202b5da735d0199dbe5b8fb85f91398814a9a46/pyyaml-6.0.3-cp313-cp313-win_amd64.whl", hash = "sha256:79005a0d97d5ddabfeeea4cf676af11e647e41d81c9a7722a193022accdb6b7c", size = 154090, upload-time = "2025-09-25T21:32:33.659Z" }, + { url = "https://files.pythonhosted.org/packages/73/e8/2bdf3ca2090f68bb3d75b44da7bbc71843b19c9f2b9cb9b0f4ab7a5a4329/pyyaml-6.0.3-cp313-cp313-win_arm64.whl", hash = "sha256:5498cd1645aa724a7c71c8f378eb29ebe23da2fc0d7a08071d89469bf1d2defb", size = 140246, upload-time = "2025-09-25T21:32:34.663Z" }, + { url = "https://files.pythonhosted.org/packages/9d/8c/f4bd7f6465179953d3ac9bc44ac1a8a3e6122cf8ada906b4f96c60172d43/pyyaml-6.0.3-cp314-cp314-macosx_10_13_x86_64.whl", hash = "sha256:8d1fab6bb153a416f9aeb4b8763bc0f22a5586065f86f7664fc23339fc1c1fac", size = 181814, upload-time = "2025-09-25T21:32:35.712Z" }, + { url = "https://files.pythonhosted.org/packages/bd/9c/4d95bb87eb2063d20db7b60faa3840c1b18025517ae857371c4dd55a6b3a/pyyaml-6.0.3-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:34d5fcd24b8445fadc33f9cf348c1047101756fd760b4dacb5c3e99755703310", size = 173809, upload-time = "2025-09-25T21:32:36.789Z" }, + { url = "https://files.pythonhosted.org/packages/92/b5/47e807c2623074914e29dabd16cbbdd4bf5e9b2db9f8090fa64411fc5382/pyyaml-6.0.3-cp314-cp314-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:501a031947e3a9025ed4405a168e6ef5ae3126c59f90ce0cd6f2bfc477be31b7", size = 766454, upload-time = "2025-09-25T21:32:37.966Z" }, + { url = "https://files.pythonhosted.org/packages/02/9e/e5e9b168be58564121efb3de6859c452fccde0ab093d8438905899a3a483/pyyaml-6.0.3-cp314-cp314-manylinux2014_s390x.manylinux_2_17_s390x.manylinux_2_28_s390x.whl", hash = "sha256:b3bc83488de33889877a0f2543ade9f70c67d66d9ebb4ac959502e12de895788", size = 836355, upload-time = "2025-09-25T21:32:39.178Z" }, + { url = "https://files.pythonhosted.org/packages/88/f9/16491d7ed2a919954993e48aa941b200f38040928474c9e85ea9e64222c3/pyyaml-6.0.3-cp314-cp314-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:c458b6d084f9b935061bc36216e8a69a7e293a2f1e68bf956dcd9e6cbcd143f5", size = 794175, upload-time = "2025-09-25T21:32:40.865Z" }, + { url = "https://files.pythonhosted.org/packages/dd/3f/5989debef34dc6397317802b527dbbafb2b4760878a53d4166579111411e/pyyaml-6.0.3-cp314-cp314-musllinux_1_2_aarch64.whl", hash = "sha256:7c6610def4f163542a622a73fb39f534f8c101d690126992300bf3207eab9764", size = 755228, upload-time = "2025-09-25T21:32:42.084Z" }, + { url = "https://files.pythonhosted.org/packages/d7/ce/af88a49043cd2e265be63d083fc75b27b6ed062f5f9fd6cdc223ad62f03e/pyyaml-6.0.3-cp314-cp314-musllinux_1_2_x86_64.whl", hash = "sha256:5190d403f121660ce8d1d2c1bb2ef1bd05b5f68533fc5c2ea899bd15f4399b35", size = 789194, upload-time = "2025-09-25T21:32:43.362Z" }, + { url = "https://files.pythonhosted.org/packages/23/20/bb6982b26a40bb43951265ba29d4c246ef0ff59c9fdcdf0ed04e0687de4d/pyyaml-6.0.3-cp314-cp314-win_amd64.whl", hash = "sha256:4a2e8cebe2ff6ab7d1050ecd59c25d4c8bd7e6f400f5f82b96557ac0abafd0ac", size = 156429, upload-time = "2025-09-25T21:32:57.844Z" }, + { url = "https://files.pythonhosted.org/packages/f4/f4/a4541072bb9422c8a883ab55255f918fa378ecf083f5b85e87fc2b4eda1b/pyyaml-6.0.3-cp314-cp314-win_arm64.whl", hash = "sha256:93dda82c9c22deb0a405ea4dc5f2d0cda384168e466364dec6255b293923b2f3", size = 143912, upload-time = "2025-09-25T21:32:59.247Z" }, + { url = "https://files.pythonhosted.org/packages/7c/f9/07dd09ae774e4616edf6cda684ee78f97777bdd15847253637a6f052a62f/pyyaml-6.0.3-cp314-cp314t-macosx_10_13_x86_64.whl", hash = "sha256:02893d100e99e03eda1c8fd5c441d8c60103fd175728e23e431db1b589cf5ab3", size = 189108, upload-time = "2025-09-25T21:32:44.377Z" }, + { url = "https://files.pythonhosted.org/packages/4e/78/8d08c9fb7ce09ad8c38ad533c1191cf27f7ae1effe5bb9400a46d9437fcf/pyyaml-6.0.3-cp314-cp314t-macosx_11_0_arm64.whl", hash = "sha256:c1ff362665ae507275af2853520967820d9124984e0f7466736aea23d8611fba", size = 183641, upload-time = "2025-09-25T21:32:45.407Z" }, + { url = "https://files.pythonhosted.org/packages/7b/5b/3babb19104a46945cf816d047db2788bcaf8c94527a805610b0289a01c6b/pyyaml-6.0.3-cp314-cp314t-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:6adc77889b628398debc7b65c073bcb99c4a0237b248cacaf3fe8a557563ef6c", size = 831901, upload-time = "2025-09-25T21:32:48.83Z" }, + { url = "https://files.pythonhosted.org/packages/8b/cc/dff0684d8dc44da4d22a13f35f073d558c268780ce3c6ba1b87055bb0b87/pyyaml-6.0.3-cp314-cp314t-manylinux2014_s390x.manylinux_2_17_s390x.manylinux_2_28_s390x.whl", hash = "sha256:a80cb027f6b349846a3bf6d73b5e95e782175e52f22108cfa17876aaeff93702", size = 861132, upload-time = "2025-09-25T21:32:50.149Z" }, + { url = "https://files.pythonhosted.org/packages/b1/5e/f77dc6b9036943e285ba76b49e118d9ea929885becb0a29ba8a7c75e29fe/pyyaml-6.0.3-cp314-cp314t-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:00c4bdeba853cc34e7dd471f16b4114f4162dc03e6b7afcc2128711f0eca823c", size = 839261, upload-time = "2025-09-25T21:32:51.808Z" }, + { url = "https://files.pythonhosted.org/packages/ce/88/a9db1376aa2a228197c58b37302f284b5617f56a5d959fd1763fb1675ce6/pyyaml-6.0.3-cp314-cp314t-musllinux_1_2_aarch64.whl", hash = "sha256:66e1674c3ef6f541c35191caae2d429b967b99e02040f5ba928632d9a7f0f065", size = 805272, upload-time = "2025-09-25T21:32:52.941Z" }, + { url = "https://files.pythonhosted.org/packages/da/92/1446574745d74df0c92e6aa4a7b0b3130706a4142b2d1a5869f2eaa423c6/pyyaml-6.0.3-cp314-cp314t-musllinux_1_2_x86_64.whl", hash = "sha256:16249ee61e95f858e83976573de0f5b2893b3677ba71c9dd36b9cf8be9ac6d65", size = 829923, upload-time = "2025-09-25T21:32:54.537Z" }, + { url = "https://files.pythonhosted.org/packages/f0/7a/1c7270340330e575b92f397352af856a8c06f230aa3e76f86b39d01b416a/pyyaml-6.0.3-cp314-cp314t-win_amd64.whl", hash = "sha256:4ad1906908f2f5ae4e5a8ddfce73c320c2a1429ec52eafd27138b7f1cbe341c9", size = 174062, upload-time = "2025-09-25T21:32:55.767Z" }, + { url = "https://files.pythonhosted.org/packages/f1/12/de94a39c2ef588c7e6455cfbe7343d3b2dc9d6b6b2f40c4c6565744c873d/pyyaml-6.0.3-cp314-cp314t-win_arm64.whl", hash = "sha256:ebc55a14a21cb14062aa4162f906cd962b28e2e9ea38f9b4391244cd8de4ae0b", size = 149341, upload-time = "2025-09-25T21:32:56.828Z" }, +] + [[package]] name = "requests" version = "2.33.1"