Skip to content

Commit

Permalink
Add quick_term_or_rec filter
Browse files Browse the repository at this point in the history
  • Loading branch information
nickdrozd committed Nov 30, 2023
1 parent 04a5aa0 commit 5fd2db1
Show file tree
Hide file tree
Showing 6 changed files with 160 additions and 89 deletions.
100 changes: 100 additions & 0 deletions test/lin_rec.py
Original file line number Diff line number Diff line change
Expand Up @@ -55,3 +55,103 @@ def run(
self.cycles = cycle

return self


class LooseLinRecMachine(LinRecMachine):
# pylint: disable = while-used, too-many-locals, line-too-long
def run(self, sim_lim: int) -> Self: # no-cover
self.blanks = {}

comp = self.comp

state = 1

step = 1

self.tape = tape = HeadTape.init_stepped()

cycle = 1

while cycle < sim_lim:
steps_reset = 2 * step

leftmost = rightmost = init_pos = tape.head

init_state = state

init_tape = tape.to_ptr()

while step < steps_reset and cycle < sim_lim:
if (instr := comp[state, tape.scan]) is None:
self.undfnd = step, (state, tape.scan)
break

color, shift, next_state = instr

if (same := state == next_state) and tape.at_edge(shift):
self.spnout = step
break

stepped = tape.step(shift, color, same)

step += stepped

cycle += 1

if (state := next_state) == -1:
self.halted = step
break

if not color and tape.blank:
if state in self.blanks:
self.infrul = step
break

self.blanks[state] = step

if state == 0:
self.infrul = step
break

if (curr := tape.head) < leftmost:
leftmost = curr
elif rightmost < curr:
rightmost = curr

if state != init_state:
continue

if tape.scan != init_tape.scan:
continue

ptr = tape.to_ptr()

if 0 < (diff := curr - init_pos):
slice1 = init_tape.get_ltr(leftmost)
slice2 = ptr.get_ltr(leftmost + diff)

elif diff < 0:
slice1 = init_tape.get_rtl(rightmost)
slice2 = ptr.get_rtl(rightmost + diff)

else:
slice1 = init_tape.get_cnt(leftmost, rightmost)
slice2 = ptr.get_cnt(leftmost, rightmost)

if slice1 == slice2:
self.infrul = step
break

else:
continue

self.xlimit = None

break

else:
self.xlimit = stepped

self.cycles = cycle

return self
6 changes: 2 additions & 4 deletions test/test_lin_rado.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
from tm.show import show_state
from tm.lin_rec import (
StrictLinRecMachine,
LooseLinRecMachine,
quick_term_or_rec,
)

if TYPE_CHECKING:
Expand Down Expand Up @@ -66,9 +66,7 @@ def run_lin_rado(
bool(halt),
rejects)
if
LooseLinRecMachine(prog).run(
sim_lim = loose,
).xlimit is not None
not quick_term_or_rec(prog, loose)
}

def test_22(self):
Expand Down
17 changes: 9 additions & 8 deletions test/test_tree.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,10 @@
from typing import TYPE_CHECKING

from test.utils import read_progs
from test.lin_rec import LooseLinRecMachine

from tm.machine import Machine
from tm.lin_rec import LooseLinRecMachine
from tm.lin_rec import quick_term_or_rec
from tm.reason import BackwardReasoner, cant_halt, cant_spin_out
from tm.tree import run_tree_gen

Expand Down Expand Up @@ -281,12 +282,10 @@ def capture(prog: str) -> None:
if 'D' not in prog:
return

machines = run_variations(
prog, 1000,
lin_rec = 50,
)
if quick_term_or_rec(prog, 50):
return

for machine in machines:
for machine in run_variations(prog, 1000):
if machine.xlimit is None:
self.add_result(prog, machine)
return
Expand Down Expand Up @@ -332,9 +331,11 @@ def capture(prog: str) -> None:
if '3' not in prog:
return

if quick_term_or_rec(prog, 100):
return

machines = run_variations(
prog, 3_000,
lin_rec = 100,
block_steps = 6_000,
)

Expand Down Expand Up @@ -369,7 +370,7 @@ def capture(prog: str) -> None:
if cant_spin_out(prog):
return

if LooseLinRecMachine(prog).run(1_000).xlimit is None:
if quick_term_or_rec(prog, 1_000):
return

machine = Machine(
Expand Down
7 changes: 5 additions & 2 deletions test/test_turing.py
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

# pylint: disable-next = wildcard-import, unused-wildcard-import
from test.prog_data import *
from test.lin_rec import LinRecSampler
from test.lin_rec import LinRecSampler, LooseLinRecMachine
from test.test_num import assert_num_counts, clear_caches

from tm.reason import (
Expand All @@ -24,7 +24,7 @@
QuickMachine,
Machine,
)
from tm.lin_rec import StrictLinRecMachine, LooseLinRecMachine
from tm.lin_rec import StrictLinRecMachine, quick_term_or_rec

from tools.instr_seq import instr_seq

Expand Down Expand Up @@ -426,6 +426,9 @@ def _test_recur(
100_000
).infrul)

self.assertTrue(
quick_term_or_rec(prog, 100_000))

def _test_prover( # type: ignore[misc]
self,
prog_data: Mapping[str, Any],
Expand Down
115 changes: 42 additions & 73 deletions tm/lin_rec.py
Original file line number Diff line number Diff line change
Expand Up @@ -390,101 +390,70 @@ def check_rec(self, step: int, slot: Slot) -> RecRes | None:
return result


class LooseLinRecMachine(LinRecMachine):
# pylint: disable = while-used, too-many-locals, line-too-long
def run(self, sim_lim: int) -> Self: # no-cover
self.blanks = {}

comp = self.comp
def quick_term_or_rec(prog: str, sim_lim: int) -> bool: # no-cover
# pylint: disable = while-used, too-many-locals

state = 1
comp = tcompile(prog)

step = 1
state = 1

self.tape = tape = HeadTape.init_stepped()
tape = HeadTape.init_stepped()

cycle = 1
step, cycle = 1, 1

while cycle < sim_lim:
steps_reset = 2 * step
while cycle < sim_lim:
steps_reset = 2 * step

leftmost = rightmost = init_pos = tape.head
leftmost = rightmost = init_pos = tape.head

init_state = state
init_state = state

init_tape = tape.to_ptr()
init_tape = tape.to_ptr()

while step < steps_reset and cycle < sim_lim:
if (instr := comp[state, tape.scan]) is None:
self.undfnd = step, (state, tape.scan)
break

color, shift, next_state = instr
while step < steps_reset and cycle < sim_lim:
if (instr := comp[state, tape.scan]) is None:
return True

if (same := state == next_state) and tape.at_edge(shift):
self.spnout = step
break

stepped = tape.step(shift, color, same)

step += stepped

cycle += 1

if (state := next_state) == -1:
self.halted = step
break
color, shift, next_state = instr

if not color and tape.blank:
if state in self.blanks:
self.infrul = step
break
if (same := state == next_state) and tape.at_edge(shift):
return True

self.blanks[state] = step
stepped = tape.step(shift, color, same)

if state == 0:
self.infrul = step
break
step += stepped

if (curr := tape.head) < leftmost:
leftmost = curr
elif rightmost < curr:
rightmost = curr
cycle += 1

if state != init_state:
continue
if (state := next_state) == -1:
return True

if tape.scan != init_tape.scan:
continue
if (curr := tape.head) < leftmost:
leftmost = curr
elif rightmost < curr:
rightmost = curr

ptr = tape.to_ptr()
if state != init_state:
continue

if 0 < (diff := curr - init_pos):
slice1 = init_tape.get_ltr(leftmost)
slice2 = ptr.get_ltr(leftmost + diff)
if tape.scan != init_tape.scan:
continue

elif diff < 0:
slice1 = init_tape.get_rtl(rightmost)
slice2 = ptr.get_rtl(rightmost + diff)
ptr = tape.to_ptr()

else:
slice1 = init_tape.get_cnt(leftmost, rightmost)
slice2 = ptr.get_cnt(leftmost, rightmost)
if 0 < (diff := curr - init_pos):
slice1 = init_tape.get_ltr(leftmost)
slice2 = ptr.get_ltr(leftmost + diff)

if slice1 == slice2:
self.infrul = step
break
elif diff < 0:
slice1 = init_tape.get_rtl(rightmost)
slice2 = ptr.get_rtl(rightmost + diff)

else:
continue

self.xlimit = None
slice1 = init_tape.get_cnt(leftmost, rightmost)
slice2 = ptr.get_cnt(leftmost, rightmost)

break
if slice1 == slice2:
return True

else:
self.xlimit = stepped

self.cycles = cycle

return self
return False
4 changes: 2 additions & 2 deletions tree_gen.py
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@

from tm.reason import cant_halt, cant_spin_out
from tm.machine import Machine
from tm.lin_rec import LooseLinRecMachine
from tm.lin_rec import quick_term_or_rec

from tm.tree import run_tree_gen

Expand All @@ -16,7 +16,7 @@ def run_variations(
lin_rec: int = 1_000,
block_steps: int = 1_000,
) -> Machine | None:
if LooseLinRecMachine(prog).run(lin_rec).xlimit is None:
if quick_term_or_rec(prog, lin_rec):
return None

machine = Machine(
Expand Down

0 comments on commit 5fd2db1

Please sign in to comment.