diff --git a/src/bin/splw.rs b/src/bin/splw.rs index e0abd9ef5..16b69b15c 100644 --- a/src/bin/splw.rs +++ b/src/bin/splw.rs @@ -60,8 +60,9 @@ mod restart { } impl Observer { - pub(super) fn reflect(&mut self, solver: &Splr, state: &SearchState) { - let span = state.current_span(); + pub(super) fn reflect(&mut self, solver: &Splr, state: &mut SearchState) { + let span = *state.span_history.iter().max().unwrap_or(&1); + state.span_history.clear(); let result = solver .asg .refer(assign::property::TEma::ConflictPerRestart) @@ -99,10 +100,10 @@ mod restart { Span::styled("lg(64)", Style::default()), ]; let chart = Chart::new(vec![ - // Dataset::default() - // .data(&self.spans) - // .style(Style::default().fg(Color::LightBlue)) - // .marker(symbols::Marker::HalfBlock), + Dataset::default() + .data(&self.spans) + .style(Style::default().fg(Color::Blue)) + .marker(symbols::Marker::Braille), Dataset::default() .data(&self.cpr) .style(Style::default().fg(Color::LightRed)) @@ -366,7 +367,7 @@ impl App { self.var_act_shift_stats[i] = (d * 100.0) as u64; } - self.restart_view.reflect(&self.solver, &self.state); + self.restart_view.reflect(&self.solver, &mut self.state); #[cfg(feature = "spin")] self.spin_view.reflect(&self.solver); @@ -599,7 +600,7 @@ fn main() -> Result<(), Box> { } Ok(solver) => solver, }; - let Ok(sc) = splr.prepare() else { + let Ok(ss) = splr.prepare() else { return Err("failed to start SAT preproecss".into()); }; enable_raw_mode()?; @@ -608,7 +609,7 @@ fn main() -> Result<(), Box> { let backend = CrosstermBackend::new(stdout); let mut terminal = Terminal::new(backend)?; - let mut app = App::solver(splr, sc); + let mut app = App::solver(splr, ss); let result = app.run(&mut terminal); disable_raw_mode()?; diff --git a/src/solver/search.rs b/src/solver/search.rs index 7ddfe3541..baf6899f5 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -26,8 +26,11 @@ pub struct SearchState { core_was_rebuilt: Option, previous_stage: Option, elapsed_time: f64, + #[cfg(feature = "rephase")] sls_core: usize, + #[cfg(feature = "graph_view")] + pub span_history: Vec, } impl SearchState { @@ -423,6 +426,8 @@ impl SolveIF for Solver { elapsed_time: 0.0, #[cfg(feature = "rephase")] sls_core: cdb.derefer(cdb::property::Tusize::NumClause), + #[cfg(feature = "graph_view")] + span_history: Vec::new(), }) } fn search_stage(&mut self, ss: &mut SearchState) -> Result, SolverError> { @@ -465,6 +470,10 @@ impl SolveIF for Solver { cdb.check_consistency(asg, "before simplify"); } ss.from_segment_beginning = 0; + + #[cfg(feature = "graph_view")] + ss.span_history.push(ss.current_span); + let next_stage: Option = state .stm .prepare_new_stage(asg.derefer(assign::Tusize::NumConflict));