Skip to content

Commit

Permalink
Add SegmentResult
Browse files Browse the repository at this point in the history
  • Loading branch information
nickdrozd committed Dec 30, 2024
1 parent 6793474 commit 43d5815
Show file tree
Hide file tree
Showing 7 changed files with 172 additions and 131 deletions.
85 changes: 49 additions & 36 deletions src/segment.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,84 +12,113 @@ use crate::{
tape::{BasicBlock as Block, Block as _, Count},
};

pub type Step = usize;
type Segments = usize;

const MAX_DEPTH: usize = 3_000;

/**************************************/

#[derive(PartialEq, Eq)]
enum Goal {
pub enum SegmentResult {
Halt,
Blank,
Repeat,
Spinout,
DepthLimit,
SegmentLimit,
Refuted(Step),
}

enum SearchResult {
Limit,
Repeat,
Reached,
Found(Goal),
impl SegmentResult {
pub const fn is_refuted(&self) -> bool {
matches!(self, Self::Refuted(_))
}
}

use Goal::*;
use SearchResult::*;

pub fn segment_cant_halt(
prog: &CompProg,
params: Params,
segs: Segments,
) -> Option<Segments> {
) -> SegmentResult {
segment_cant_reach(prog, params, segs, &Halt)
}

pub fn segment_cant_blank(
prog: &CompProg,
params: Params,
segs: Segments,
) -> Option<Segments> {
) -> SegmentResult {
segment_cant_reach(prog, params, segs, &Blank)
}

pub fn segment_cant_spin_out(
prog: &CompProg,
params: Params,
segs: Segments,
) -> Option<Segments> {
) -> SegmentResult {
segment_cant_reach(prog, params, segs, &Spinout)
}

/**************************************/

#[derive(PartialEq, Eq)]
enum Goal {
Halt,
Blank,
Spinout,
}

enum SearchResult {
Limit,
Repeat,
Reached,
Found(Goal),
}

use Goal::*;
use SearchResult::*;

impl From<Goal> for SegmentResult {
fn from(goal: Goal) -> Self {
match goal {
Halt => Self::Halt,
Blank => Self::Blank,
Spinout => Self::Spinout,
}
}
}

fn segment_cant_reach(
prog: &CompProg,
params: Params,
segs: Segments,
goal: &Goal,
) -> Option<Segments> {
) -> SegmentResult {
assert!(segs >= 2);

let prog = AnalyzedProg::new(prog, params);

if (goal == &Halt && prog.halts.is_empty())
|| (goal == &Spinout && prog.spinouts.is_empty())
{
return Some(0);
return SegmentResult::Refuted(0);
}

for seg in 2..=segs {
let Some(result) = all_segments_reached(&prog, 2 + seg, goal)
else {
return Some(seg);
return SegmentResult::Refuted(seg);
};

match result {
Reached => continue,
Limit => return None,
Repeat => return Some(seg),
Found(found) => return (found != *goal).then_some(seg),
Limit => return SegmentResult::DepthLimit,
Repeat => return SegmentResult::Repeat,
Found(found) => return found.into(),
}
}

None
SegmentResult::SegmentLimit
}

/**************************************/
Expand Down Expand Up @@ -866,22 +895,6 @@ fn test_reached_states() {
}
}

#[test]
fn test_cant_halt() {
let results = [
("1RB ... ... ...", (2, 2), None),
("1RB ... 1LB 0RC 1LC 1LA", (3, 2), None),
("1RB 1RC 0LA 0RA 0LB ...", (3, 2), Some(2)),
];

for (prog, params, result) in results {
assert_eq!(
result,
segment_cant_halt(&CompProg::from_str(prog), params, 2),
);
}
}

#[cfg(test)]
macro_rules! tape {
(
Expand Down
26 changes: 13 additions & 13 deletions src/tree.rs
Original file line number Diff line number Diff line change
Expand Up @@ -302,7 +302,7 @@ fn skip_all(comp: &CompProg, params: Params, halt: bool) -> bool {
|| quick_term_or_rec(comp, 301, true)
|| cant_reach(comp, 256).is_settled()
|| check_inf(comp, params, opt_block(comp, 300), 306)
|| segment_cant_reach(comp, params, 3).is_some()
|| segment_cant_reach(comp, params, 3).is_refuted()
}

#[test]
Expand Down Expand Up @@ -543,7 +543,7 @@ fn assert_segment(params: Params, halt: u8, expected: (u64, u64)) {
build_tree(params, halt_flag, 300, &|prog| {
*access(&visited_count) += 1;

if cant_reach(prog, params, segs).is_some() {
if cant_reach(prog, params, segs).is_refuted() {
return;
}

Expand All @@ -570,26 +570,26 @@ macro_rules! assert_segment_results {
#[test]
fn test_segment() {
assert_segment_results![
((2, 2), 1, (10, 36)),
((2, 2), 0, (15, 106)),
((2, 2), 1, (21, 36)),
((2, 2), 0, (28, 106)),
//
((3, 2), 1, (1_027, 3_140)),
((3, 2), 0, (1_362, 13_128)),
((3, 2), 1, (1_245, 3_140)),
((3, 2), 0, (2_045, 13_128)),
//
((2, 3), 1, (684, 2_447)),
((2, 3), 0, (907, 9_168)),
((2, 3), 1, (892, 2_447)),
((2, 3), 0, (1_396, 9_168)),
];
}

#[test]
#[ignore]
fn test_segment_slow() {
assert_segment_results![
((4, 2), 1, (139_175, 467_142)),
((4, 2), 0, (222_047, 2_291_637)),
((4, 2), 1, (161_731, 467_142)),
((4, 2), 0, (280_689, 2_291_637)),
//
((2, 4), 1, (114_955, 312_642)),
((2, 4), 0, (166_146, 1_719_237)),
((2, 4), 1, (130_046, 312_642)),
((2, 4), 0, (202_779, 1_719_237)),
];
}

Expand All @@ -611,7 +611,7 @@ fn assert_blank(params: Params, expected: (u64, u64)) {
|| !run_prover(&prog.show(Some(params)), run as u64)
.blanks
.is_empty()
|| segment_cant_blank(prog, params, 11).is_some()
|| segment_cant_blank(prog, params, 11).is_refuted()
{
return;
}
Expand Down
50 changes: 44 additions & 6 deletions src/wrappers.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ use crate::{
},
segment::{
segment_cant_blank, segment_cant_halt, segment_cant_spin_out,
SegmentResult as SegmentResultRs,
},
};

Expand Down Expand Up @@ -115,6 +116,43 @@ pub fn py_cant_spin_out(prog: &str, depth: Depth) -> BackwardResult {

/***************************************/

#[expect(non_camel_case_types)]
#[pyclass]
pub enum SegmentResult {
halt {},
blank {},
repeat {},
spinout {},
depth_limit {},
segment_limit {},
refuted { step: Step },
}

#[pymethods]
impl SegmentResult {
const fn is_refuted(&self) -> bool {
matches!(self, Self::refuted { .. })
}

const fn is_settled(&self) -> bool {
!matches!(self, Self::depth_limit {} | Self::segment_limit {})
}
}

impl From<SegmentResultRs> for SegmentResult {
fn from(result: SegmentResultRs) -> Self {
match result {
SegmentResultRs::Halt => Self::halt {},
SegmentResultRs::Blank => Self::blank {},
SegmentResultRs::Repeat => Self::repeat {},
SegmentResultRs::Spinout => Self::spinout {},
SegmentResultRs::DepthLimit => Self::depth_limit {},
SegmentResultRs::SegmentLimit => Self::segment_limit {},
SegmentResultRs::Refuted(step) => Self::refuted { step },
}
}
}

fn get_comp(prog: &str) -> (CompProg, Params) {
let prog = CompProg::from_str(prog);

Expand All @@ -128,25 +166,25 @@ fn get_comp(prog: &str) -> (CompProg, Params) {
}

#[pyfunction]
pub fn py_segment_cant_halt(prog: &str, segs: usize) -> Option<usize> {
pub fn py_segment_cant_halt(prog: &str, segs: usize) -> SegmentResult {
let (comp, params) = get_comp(prog);

segment_cant_halt(&comp, params, segs)
segment_cant_halt(&comp, params, segs).into()
}

#[pyfunction]
pub fn py_segment_cant_blank(prog: &str, segs: usize) -> Option<usize> {
pub fn py_segment_cant_blank(prog: &str, segs: usize) -> SegmentResult {
let (comp, params) = get_comp(prog);

segment_cant_blank(&comp, params, segs)
segment_cant_blank(&comp, params, segs).into()
}

#[pyfunction]
pub fn py_segment_cant_spin_out(
prog: &str,
segs: usize,
) -> Option<usize> {
) -> SegmentResult {
let (comp, params) = get_comp(prog);

segment_cant_spin_out(&comp, params, segs)
segment_cant_spin_out(&comp, params, segs).into()
}
Loading

0 comments on commit 43d5815

Please sign in to comment.