Skip to content
Snippets Groups Projects
Commit 5c35709f authored by chrg's avatar chrg
Browse files

This is not the place for this.

parent dc3e512b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
pyrtree/.gitignore deleted 100644 → 0
+ 0
− 1
View file @ dc3e512b
__pycache__
pyrtree/expr.py deleted 100644 → 0
+ 0
− 161
View file @ dc3e512b
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 \\\\")
pyrtree/rtree.py deleted 100644 → 0
+ 0
− 264
View file @ dc3e512b
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 \\\\")
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment