diff --git a/pyrtree/.gitignore b/pyrtree/.gitignore deleted file mode 100644 index bee8a64b79a99590d5303307144172cfe824fbf7..0000000000000000000000000000000000000000 --- a/pyrtree/.gitignore +++ /dev/null @@ -1 +0,0 @@ -__pycache__ diff --git a/pyrtree/expr.py b/pyrtree/expr.py deleted file mode 100644 index e5f70b6c8ca0f94d82d775b7dd392f3d637e1c46..0000000000000000000000000000000000000000 --- a/pyrtree/expr.py +++ /dev/null @@ -1,161 +0,0 @@ -from dataclasses import dataclass -from functools import partial - -import rtree - - -@dataclass -class Let: - var: str - assignee: "Expr" - body: "Expr" - - def replace(self, reps): - return Let( - self.var, - self.assignee.replace(reps), - self.body.replace(reps), - ) - - def eval(self, vals=None): - vals = vals or dict() - r = self.assignee.eval(vals) - vals = vals.copy() - vals[self.var] = r - return self.body.eval(vals) - - def subterms(self): - yield self - yield from self.assignee.subterms() - yield from self.body.subterms() - - def pretty(self, prec=0): - p = f"{self.var} := {self.assignee.pretty(2)}; {self.body.pretty(1)}" - if prec >= 1: - p = f"({p})" - return p - - -@dataclass -class Add: - lhs: "Expr" - rhs: "Expr" - - def replace(self, reps): - return Add( - self.lhs.replace(reps), - self.rhs.replace(reps), - ) - - def subterms(self): - yield self - yield from self.lhs.subterms() - yield from self.rhs.subterms() - - def pretty(self, n=0): - p = f"{self.lhs.pretty(4)} + {self.rhs.pretty(3)}" - if n >= 3: - p = f"({p})" - return p - - def eval(self, vals=None): - vals = vals or dict() - lv = self.lhs.eval(vals) - rv = self.rhs.eval(vals) - return lv + rv - - -@dataclass -class Const: - n: int - - def replace(self, _): - return self - - def subterms(self): - yield self - - def pretty(self, _=0): - return str(self.n) - - def eval(self, _vals=None): - return self.n - - -@dataclass -class Var: - name: str - - def replace(self, reps): - return reps.get(self.name, self) - - def subterms(self): - yield self - - def pretty(self, _=0): - return self.name - - def eval(self, vals=None): - vals = vals or dict() - return vals.get(self.name, -1) - - -Expr = Let | Add | Const | Var - - -def reduce_expr(expr: Expr, check) -> Expr: - if isinstance(expr, Var): - return expr - elif isinstance(expr, Const): - if not expr.n == 0 and check("1) make zero"): - return Const(0) - return expr - elif isinstance(expr, Add): - lhs_ = reduce_expr(expr.lhs, check) - rhs_ = reduce_expr(expr.rhs, check) - if check("2) reduce to lhs"): - return lhs_ - if check("3) reduce to rhs"): - return rhs_ - return Add(lhs_, rhs_) - elif isinstance(expr, Let): - assignee_ = reduce_expr(expr.assignee, check) - if check("4) reduce to assingee"): - return assignee_ - if check(f"5) inline {expr.var!r}"): - return reduce_expr(expr.body.replace({expr.var: assignee_}), check) - body_ = reduce_expr(expr.body, check) - return Let(expr.var, assignee_, body_) - - -if __name__ == "__main__": - expr = Let( - "x", Const(2), Add(Const(1), Let("y", Var("x"), Add(Const(3), Var("y")))) - ) - - def input_format(a): - return f"$\\syn{{{a.pretty()}}}$" - - p = rtree.latex( - lambda e: any(isinstance(a, Add) for a in e.subterms()), - query_format=str, - input_format=input_format, - start_count=0, - ) - rt = partial(reduce_expr, expr) - p(rtree.Probe(rt, [])) - rp = rtree.reduce(p, rt) - print(f"& \\verb|{rtree.pretty(rp)}| & {input_format(rp.input)} & true \\\\") - - print() - - p = rtree.latex( - lambda e: e.eval() == expr.eval(), - query_format=str, - input_format=input_format, - start_count=0, - ) - rt = partial(reduce_expr, expr) - p(rtree.Probe(rt, [])) - rp = rtree.reduce(p, rt) - print(f"& {rtree.pretty(rp)} & {input_format(rp.input)} & true \\\\") diff --git a/pyrtree/rtree.py b/pyrtree/rtree.py deleted file mode 100644 index ac6b969a5d0f67eadfad1ff036f0bc8f4d3925f9..0000000000000000000000000000000000000000 --- a/pyrtree/rtree.py +++ /dev/null @@ -1,264 +0,0 @@ -from dataclasses import dataclass -import math -from typing import TypeVar - - -def reduce_simp(predicate, rtree): - path: list[bool] = [] - labels: list[str] = [] - - def check(label): - labels.append(label) - return path[len(labels) - 1] if len(path) >= len(labels) else False - - i = rtree(check) - while len(path) < len(labels): - path.append(True) - labels.clear() - if t := predicate(j := rtree(check)): - i = j - else: - path[-1] = False - print(f"{labels[len(path) - 1]} ... test {j!r:<10} ... {t}") - return i - - -class Probe: - def __init__(self, rtree, path, guess_depth=0): - """Test an rtree with a path, and optional number of guesses""" - self.path = path + [True] * guess_depth - self.depth = guess_depth - self.reasons = [] - - def check(reason: str): - """Check the path or default to false""" - self.reasons.append(reason) - return self.undecided() <= 0 and self.path[len(self.reasons) - 1] - - self.input = rtree(check) - - def undecided(self): - """The number of choices left on the path""" - return len(self.reasons) - len(self.path) - - -def reduce1(predicate, rtree): - # Extract the initial reduction probe, from the rightmost branch. - rp = Probe(rtree, []) - # Run exponential search after the depest sequence of trues - # that can be appended to the path without failing the predicate - depth = 1 - # Invariant: predicate(rp) == True - while rp.undecided() > 0: - # Try to probe the with current path extended by one trues - if predicate(rp_ := Probe(rtree, rp.path, depth)): - rp = rp_ - continue - rp.path.append(False) - # return the input. - return rp - - -def reduce(predicate, rtree): - # Extract the initial reduction probe, from the rightmost branch. - rp = Probe(rtree, []) - # Run exponential search after the depest sequence of trues - # that can be appended to the path without failing the predicate - depth = 1 - # Invariant: predicate(rp) == True - while rp.undecided() > 0: - # Try to probe the with current path extended by trues trues. - if predicate(rp_ := Probe(rtree, rp.path, depth)): - rp, depth = rp_, depth * 2 - continue - # Adjust the depth so that none of them are wasted. - depth += min(0, rp_.undecided()) - # Perform a binary search, accepting the nessarary trues, and - # reducing the unknown trues to 1: - while depth > 1: - # Prope the rtree with the current path extended by half the depth. - if predicate(rp_ := Probe(rtree, rp.path, depth // 2)): - rp = rp_ # Accept the current path. - depth -= depth // 2 # And try the remaining half - else: - depth //= 2 # Half the current trues - # Store that the next element in the path has to be false - rp.path.append(False) - # return the input. - return rp - - -def debug(predicate): - counter = 0 - - def newpred(rp): - nonlocal counter - counter += 1 - t = predicate(rp.input) - print( - f"{counter:02})", - ", ".join(rp.reasons[len(rp.path) - rp.depth : len(rp.path)]), - ) - print(f"... P({rp.input!r}) = {t}") - return t - - return newpred - - -def latex( - predicate, - query_format="Remove {}?".format, - input_format="\\verb|{}|".format, - start_count=0, -): - counter = start_count - 1 - - def newpred(rp): - nonlocal counter - counter += 1 - t = predicate(rp.input) - query = ", ".join(rp.reasons[len(rp.path) - rp.depth : len(rp.path)]) - theck = "true" if t else "false" - - print( - f"{counter:02} & \\verb|{pretty(rp)}| & {query_format(query)} & {input_format(rp.input)} & {theck} \\\\" - ) - return t - - return newpred - - -def table( - predicate, - input_format="{}".format, - query_format=str, - start_count=0, -): - counter = start_count - 1 - - def newpred(rp): - nonlocal counter - counter += 1 - t = predicate(rp.input) - query = ", ".join( - query_format(a) for a in rp.reasons[len(rp.path) - rp.depth : len(rp.path)] - ) - theck = "true " if t else "false" - - print(f"{counter:02} - {input_format(rp.input)} - {theck} - {query}") - return t - - return newpred - - -def pretty(rp): - from itertools import zip_longest - - def binary(a): - return "1" if a else "0" - - return "".join( - a if b != "*" else "!" - for a, b in zip_longest(map(binary, rp.path), rp.reasons, fillvalue="*") - ) - - -def reduce_abc(check) -> str: - result = "" - for x in "abc": - if not check(f"remove {x}?"): - result += x - else: - result += " " - return result - - -def reduce_dd2(c: list, check) -> list: - if check(f"ignore {c}?"): - return [] - if len(c) == 1: - return c - pivot = len(c) // 2 - c2 = reduce_dd(c[pivot:], check) - c1 = reduce_dd(c[:pivot], check) - return c1 + c2 - - -def reduce_dd(c: list, check) -> list: - if len(c) == 1: - return c - pivot = len(c) // 2 - c1 = c[:pivot] - c2 = c[pivot:] - if check(f"result in c1: {c1}?"): - return reduce_dd(c1, check) - elif check(f"result in c2: {c2}?"): - return reduce_dd(c2, check) - else: - return reduce_dd(c1, check) + reduce_dd(c2, check) - - -I = TypeVar("I") - - -def reduce_df(i: I, actions, check) -> I: - j = None - while i != j: - for act in actions: - if check(f"apply {act}?"): - i, j = act(i), i - else: - break - return i - - -def reduce_ddmin(input: list, check, n=2) -> list: - def find_next(input, n): - step = math.ceil(len(input) / n) - subsets = [(step * i, step * (i + 1)) for i in range(n)] - for i, (f, t) in enumerate(subsets): - if check(f"delta: {i}/{n}"): - return input[f:t], 2 - - for i, (f, t) in enumerate(subsets) if n != 2 else []: - if check(f"complement: {i}/{n}"): - return input[:f] + input[t:], max(n - 1, 2) - - return input, n * 2 - - while len(input) > 1 and n < 2 * len(input): - input, n = find_next(input, n) - - return input - - -def test_reduce_dd(): - from functools import partial - - p = debug(lambda a: 3 in a and 6 in a) - rp = reduce(p, partial(reduce_dd, [1, 2, 3, 4, 5, 6, 7, 8])) - print(rp) - - -def test_reduce_ddmin(): - from functools import partial - - input_format = lambda a: "".join("X" if i in a else "." for i in range(1, 9)) - p = table( - lambda a: 1 in a and 7 in a and 8 in a, - input_format=input_format, - query_format=str, - ) - rp = reduce1(p, partial(reduce_ddmin, [1, 2, 3, 4, 5, 6, 7, 8])) - print(f" - {input_format(rp.input)}") - - -if __name__ == "__main__": - p = latex( - lambda e: "a" in e or "p" in e, - start_count=0, - ) - input_format = "\\verb|{}|".format - p(Probe(reduce_abc, [])) - rp = reduce(p, reduce_abc) - print(f"&& {input_format(rp.input)} & true \\\\")