ty

Author: philzook58

src/kdrag/contrib/fast/__init__.py

@@ -49,11 +49,11 @@
 
 
 def ctxptr(ctx: z3.Context):
-    return ffibuilder.cast("void *", ctx.ctx.value)  # type: ignore
+    return ffibuilder.cast("void *", ctx.ctx.value)  # type: ignore[possibly-missing-attribute]
 
 
 def astptr(ast: z3.AstRef):
-    return ffibuilder.cast("void *", ast.as_ast().value)  # type: ignore
+    return ffibuilder.cast("void *", ast.as_ast().value)
 
 
 def intify(ptr):

src/kdrag/contrib/pcode/__init__.py

@@ -750,7 +750,7 @@ def sym_execute(
                 elif max_insns <= 0:
                     res.append(SimState(memstate1, pc1, path_cond))
                 else:
-                    todo.append((memstate1, pc1, max_insns, path_cond))  # type: ignore
+                    todo.append((memstate1, pc1, max_insns, path_cond))
         return res
 
     def execute_block(self, memstate: MemState, addr: int) -> list[SimState]:

src/kdrag/hypothesis.py

@@ -238,10 +238,10 @@ def val_of_sort(
         return smt_datatype_val(s)
     else:
         # return smt_generic_val(s) # This is really slow. We're better off just throwing an error
-        if slow_generic:
-            return smt_generic_val(s)
-        else:
-            raise NotImplementedError(f"Don't know how to generate values for {s}")
+        # if slow_generic:
+        #    return smt_generic_val(s)
+        # else:
+        raise NotImplementedError(f"Don't know how to generate values for {s}")
 
 
 # def expr_of_sort(s: smt.SortRef):

src/kdrag/kernel.py

@@ -87,7 +87,7 @@ def __call__(self, *args: "smt.ExprRef | Proof"):
                     a if isinstance(a, smt.ExprRef) else smt._py2expr(a)
                     for a in args[n : n + i]
                 ]
-                acc = instan(subargs, acc)  # type: ignore
+                acc = instan(subargs, acc)
                 n += i
             elif smt.is_implies(self.thm):
                 x = args[n]

src/kdrag/notation.py

@@ -240,19 +240,19 @@ def GenericDispatch(default_factory) -> SortDispatch:
 
 or_ = SortDispatch(name="or_", pointwise=True)
 """Sort based dispatch for `|` syntax"""
-smt.ExprRef.__or__ = lambda x, y: or_(x, y)  # type: ignore
+smt.ExprRef.__or__ = lambda x, y: or_(x, y)  # type: ignore[invalid-assignment]
 smt.QuantifierRef.__or__ = lambda x, y: or_(x, y)  # type: ignore
 or_.register(smt.BoolSort(), smt.Or)
 
 invert = SortDispatch(name="invert", pointwise=True)
 """Sort based dispatch for `~` syntax"""
-smt.ExprRef.__invert__ = lambda x: invert(x)  # type: ignore
+smt.ExprRef.__invert__ = lambda x: invert(x)  # type: ignore[invalid-assignment]
 smt.QuantifierRef.__invert__ = lambda x: invert(x)  # type: ignore
 invert.register(smt.BoolSort(), smt.Not)
 
 lt = SortDispatch(name="lt", pointwise=True)
 """Sort based dispatch for `<` syntax"""
-smt.ExprRef.__lt__ = lambda x, y: lt(x, y)  # type: ignore
+smt.ExprRef.__lt__ = lambda x, y: lt(x, y)  # type: ignore[invalid-assignment]
 lt.register(smt.IntSort(), lambda x, y: x < y)
 lt.register(smt.RealSort(), lambda x, y: x < y)
 # Conceptually this kind of makes sense, but SubSet is the more natural thing.
@@ -261,51 +261,51 @@ def GenericDispatch(default_factory) -> SortDispatch:
 
 le = SortDispatch(name="le", pointwise=True)
 """Sort based dispatch for `<=` syntax"""
-smt.ExprRef.__le__ = lambda x, y: le(x, y)  # type: ignore
+smt.ExprRef.__le__ = lambda x, y: le(x, y)  # type: ignore[invalid-assignment]
 le.register(smt.IntSort(), lambda x, y: x <= y)
 le.register(smt.RealSort(), lambda x, y: x <= y)
 # le.register(smt.BoolSort(), lambda x, y: smt.Implies(x, y))
 
 ge = SortDispatch(name="ge", pointwise=True)
 """Sort based dispatch for `>=` syntax"""
-smt.ExprRef.__ge__ = lambda x, y: ge(x, y)  # type: ignore
+smt.ExprRef.__ge__ = lambda x, y: ge(x, y)  # type: ignore[invalid-assignment]
 ge.register(smt.IntSort(), lambda x, y: x >= y)
 ge.register(smt.RealSort(), lambda x, y: x >= y)
 # ge.register(smt.BoolSort(), lambda x, y: smt.Implies(y, x))
 
 gt = SortDispatch(name="gt", pointwise=True)
 """Sort based dispatch for `>` syntax"""
-smt.ExprRef.__gt__ = lambda x, y: gt(x, y)  # type: ignore
+smt.ExprRef.__gt__ = lambda x, y: gt(x, y)  # type: ignore[invalid-assignment]
 gt.register(smt.IntSort(), lambda x, y: x > y)
 gt.register(smt.RealSort(), lambda x, y: x > y)
 # gt.register(smt.BoolSort(), lambda x, y: smt.And(x, smt.Not(y)))
 
 # contains cannot work because python demands a concrete bool.
 # contains = SortDispatch(name="contains")
-# smt.ExprRef.__contains__ = lambda x, y: contains(x, y)  # type: ignore
+# smt.ExprRef.__contains__ = lambda x, y: contains(x, y)
 
 eq = SortDispatch(name="eq", default=smt.Eq)
 """Sort based dispatch for `==` syntax"""
-smt.ExprRef.__eq__ = lambda x, y: eq(x, y)  # type: ignore
+smt.ExprRef.__eq__ = lambda x, y: eq(x, y)  # type: ignore[invalid-assignment]
 
 
 ne = SortDispatch(name="ne", default=smt.NEq)
 """Sort based dispatch for `!=` syntax"""
-smt.ExprRef.__ne__ = lambda x, y: ne(x, y)  # type: ignore
+smt.ExprRef.__ne__ = lambda x, y: ne(x, y)  # type: ignore[invalid-assignment]
 
 wf = SortDispatch(name="wf")
 """`wf` is a special predicate for well-formedness. It is auto inserted by QForAll and QExists."""
-smt.ExprRef.wf = lambda x: wf(x)  # type: ignore
+smt.ExprRef.wf = lambda x: wf(x)
 
 measure = SortDispatch(name="measure")
 """`measure is an Int value associated with an ExprRef for use in defining well-founded recursion."""
-# smt.ExprRef.measure = lambda x: measure(x)  # type: ignore
-measure.register(smt.IntSort(), lambda x: smt.Abs(x))  # type: ignore
+# smt.ExprRef.measure = lambda x: measure(x)
+measure.register(smt.IntSort(), lambda x: smt.Abs(x))
 measure.register(smt.BoolSort(), lambda x: smt.If(x, smt.IntVal(1), smt.IntVal(0)))
 
 choose = SortDispatch(name="choose")
 """Sort based dispatch for Hilbert choice operator."""
-# smt.ExprRef.choose = lambda P: choose(P)  # type: ignore
+# smt.ExprRef.choose = lambda P: choose(P)
 
 # These are of questionable utility, but conceptually should be here.
 forall = SortDispatch(name="forall")
@@ -356,7 +356,7 @@ def induct_default(x, P):
 
 induct = SortDispatch(name="induct", default=induct_default)
 """Sort based dispatch for induction principles. Should instantiate an induction scheme for variable x and predicate P"""
-smt.ExprRef.induct = lambda x, P: induct(x, P)  # type: ignore
+smt.ExprRef.induct = lambda x, P: induct(x, P)
 
 
 def induct_int(x, P):

src/kdrag/parsers/microlean.py

@@ -135,7 +135,7 @@ def sort(tree: Tree, env: Env) -> smt.SortRef:
             return smt.ArraySort(sort(left, env), sort(right, env))
             # return smt.ArraySort(*(sort(s) for s in left.children), sort(right,env))
         case Tree("bitvecsort", [n]):
-            n1 = int(n)  # type: ignore
+            n1 = int(n)
             return smt.BitVecSort(n1)
         case Tree("sortlit", [name]):
             if name == "Int":
@@ -203,10 +203,10 @@ def quant(vs, body_tree, q, env) -> smt.QuantifierRef:
 def _pattern_head(tree, env: Env) -> smt.ExprRef:
     match tree:
         case Tree("const", [name, *attrs]):
-            res = env[name]  # type: ignore
+            res = env[name]
             for attr in attrs:
-                res = getattr(res, str(attr))  # type: ignore
-            return res  # type: ignore
+                res = getattr(res, str(attr))
+            return res
         case Tree("pat_app", [inner]):
             return _pattern_head(inner, env)
         case _:
@@ -223,20 +223,20 @@ def pattern(tree, env: Env, expected_sort: smt.SortRef | None) -> smt.ExprRef:
             text = str(n)
             if "." in text:
                 return smt.RealVal(text)
-            return int(text)  # type: ignore
+            return int(text)  # type: ignore[invalid-return-type]
         case Tree("const", [name, *attrs]):
             if name in env.locals or name in env.globals:
-                res = env[name]  # type: ignore
+                res = env[name]
             else:
                 if expected_sort is None:
                     raise ValueError("Cannot infer sort for pattern variable", name)
                 res = smt.Const(str(name), expected_sort)
                 env[str(name)] = res
             for attr in attrs:
-                res = getattr(res, str(attr))  # type: ignore
+                res = getattr(res, str(attr))
             if isinstance(res, smt.FuncDeclRef) and res.arity() == 0:
                 return res()
-            return res  # type: ignore
+            return res
         case Tree("true", []):
             return smt.BoolVal(True)
         case Tree("false", []):
@@ -264,12 +264,12 @@ def expr(tree, env: Env, expected_sort: Optional[smt.SortRef] = None) -> smt.Exp
             text = str(n)
             if "." in text:
                 return smt.RealVal(text)
-            return int(text)  # type: ignore
+            return int(text)  # type: ignore[invalid-return-type]
         case Tree("const", [name, *attrs]):
-            res = env[name]  # type: ignore
+            res = env[name]
             for attr in attrs:
-                res = getattr(res, str(attr))  # type: ignore
-            return res  # type: ignore
+                res = getattr(res, str(attr))
+            return res
         case Tree("true", []):
             return smt.BoolVal(True)
         case Tree("false", []):

src/kdrag/parsers/tptp.py

@@ -9,7 +9,7 @@
 from enum import Enum
 from typing import Any, Optional, cast
 
-import lark  # type: ignore[reportMissingImports]
+import lark
 import kdrag.smt as smt
 
 # https://github.com/inpefess/tptp-lark-parser/blob/master/tptp_lark_parser/resources/TPTP.lark
@@ -459,7 +459,7 @@ def _type_repr_to_sort(
             rng_sort = self._type_repr_to_sort(rng)
             if isinstance(rng_sort, tuple):
                 rng_doms, rng_rng = rng_sort
-                dom_sorts.extend(cast(list[smt.SortRef], rng_doms))  # type: ignore
+                dom_sorts.extend(cast(list[smt.SortRef], rng_doms))
                 rng_sort = rng_rng
             return (
                 cast(list[smt.SortRef], dom_sorts),

src/kdrag/reflect.py

@@ -449,37 +449,37 @@ def rec(expr: ast.expr) -> smt.ExprRef:
             # case ast.UnaryOp(ast.UAdd(), operand):
             #    return +rec(operand)
             case ast.UnaryOp(ast.Not(), operand):
-                return ~rec(operand)  # type: ignore
+                return ~rec(operand)
             case ast.UnaryOp(ast.USub(), operand):
-                return -rec(operand)  # type: ignore
+                return -rec(operand)
             case ast.UnaryOp(ast.Invert(), operand):
-                return ~rec(operand)  # type: ignore
+                return ~rec(operand)
             case ast.UnaryOp(_, operand):
                 raise NotImplementedError(f"UnaryOp {expr.op}")
             case ast.BinOp(left=l, op=ast.Add(), right=r):
-                return rec(l) + rec(r)  # type: ignore
+                return rec(l) + rec(r)
             case ast.BinOp(left=l, op=ast.Sub(), right=r):
-                return rec(l) - rec(r)  # type: ignore
+                return rec(l) - rec(r)
             case ast.BinOp(left=l, op=ast.Mult(), right=r):
-                return rec(l) * rec(r)  # type: ignore
+                return rec(l) * rec(r)
             case ast.BinOp(left=l, op=ast.Div(), right=r):
-                return rec(l) / rec(r)  # type: ignore
+                return rec(l) / rec(r)
             case ast.BinOp(left=l, op=ast.Mod(), right=r):
-                return rec(l) % rec(r)  # type: ignore
+                return rec(l) % rec(r)
             case ast.BinOp(left=l, op=ast.Pow(), right=r):
-                return rec(l) ** rec(r)  # type: ignore
+                return rec(l) ** rec(r)
             case ast.BinOp(left=l, op=ast.LShift(), right=r):
-                return rec(l) << rec(r)  # type: ignore
+                return rec(l) << rec(r)
             case ast.BinOp(left=l, op=ast.RShift(), right=r):
-                return rec(l) >> rec(r)  # type: ignore
+                return rec(l) >> rec(r)
             case ast.BinOp(left=l, op=ast.BitOr(), right=r):
-                return rec(l) | rec(r)  # type: ignore
+                return rec(l) | rec(r)
             case ast.BinOp(left=l, op=ast.BitXor(), right=r):
-                return rec(l) ^ rec(r)  # type: ignore
+                return rec(l) ^ rec(r)
             case ast.BinOp(left=l, op=ast.BitAnd(), right=r):
-                return rec(l) & rec(r)  # type: ignore
+                return rec(l) & rec(r)
             case ast.BinOp(left=l, op=ast.FloorDiv(), right=r):
-                return rec(l) // rec(r)  # type: ignore
+                return rec(l) // rec(r)
             case ast.BoolOp(op=ast.And(), values=values):
                 return smt.And(*map(rec, values))
             case ast.BoolOp(op=ast.Or(), values=values):
@@ -495,13 +495,13 @@ def rec(expr: ast.expr) -> smt.ExprRef:
                         case ast.NotEq():
                             acc.append(left != right)
                         case ast.Lt():
-                            acc.append(left < right)  # type: ignore
+                            acc.append(left < right)
                         case ast.LtE():
-                            acc.append(left <= right)  # type: ignore
+                            acc.append(left <= right)
                         case ast.Gt():
-                            acc.append(left > right)  # type: ignore
+                            acc.append(left > right)
                         case ast.GtE():
-                            acc.append(left >= right)  # type: ignore
+                            acc.append(left >= right)
                         case _:
                             raise NotImplementedError(f"Compare {op}")
                     left = right
@@ -696,7 +696,7 @@ def reflect(f, globals=None) -> smt.FuncDeclRef:
     assert z3fun.arity() == z3fun1.arity() and all(
         z3fun.domain(i) == z3fun1.domain(i) for i in range(z3fun.arity())
     )
-    return functools.update_wrapper(z3fun1, f)  # type: ignore
+    return functools.update_wrapper(z3fun1, f)  # type: ignore[invalid-return-type]
 
 
 def datatype(s: str, locals=None, globals=None) -> smt.DatatypeSortRef:

src/kdrag/smt.pyi

@@ -593,6 +593,12 @@ class ExprRef(AstRef):
         ...
     def __xor__(self, other):  # -> ExprRef:
         ...
+    def __lshift__(self, other):  # -> ExprRef:
+        ...
+    def __rshift__(self, other):  # -> ExprRef:
+        ...
+    def __pow__(self, other):  # -> ExprRef:
+        ...
     def __invert__(self):  # -> ExprRef:
         ...
     def __call__(self, *args):  # -> ExprRef:

src/kdrag/solvers/egraph.py

@@ -351,7 +351,7 @@ def dot(self, filename: str = "egraph") -> graphviz.Digraph:
         eclasses = self.eclasses()
 
         for eid, funcs in eclasses.items():
-            with dot.subgraph(name=f"cluster_{eid}") as c:  # type: ignore
+            with dot.subgraph(name=f"cluster_{eid}") as c:
                 assert c is not None
                 c.attr(style="dotted,rounded")
                 rep = f"e_rep_{eid}"