Skip to content

Commit

Permalink
(splw) add Restart gap viewer
Browse files Browse the repository at this point in the history
  • Loading branch information
shnarazk committed Aug 12, 2024
1 parent 879600c commit 0b1cb9e
Show file tree
Hide file tree
Showing 4 changed files with 119 additions and 15 deletions.
4 changes: 2 additions & 2 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ default = [

### For SAT researcher
"graph_view",
"spin",
# "spin",

### platform dependency
# "platform_wasm"
Expand All @@ -69,7 +69,7 @@ graph_view = [
"crossterm",
"interleave",
"ratatui",
"spin"
# "spin"
]
incremental_solver = [] # for all solution SAT sover; requires no cluse_elimination
interleave = [] # switch to multi-step search IF
Expand Down
1 change: 1 addition & 0 deletions src/assign/learning_rate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ impl ActivityIF<VarId> for AssignStack {
self.var[vi].turn_on(FlagVar::USED);
}
#[inline]
#[allow(unused_variables)]
fn reward_at_assign(&mut self, vi: VarId) {
#[cfg(feature = "spin")]
if let Some(b) = self.var[vi].assign {
Expand Down
126 changes: 113 additions & 13 deletions src/bin/splw.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,96 @@ use {
},
};

mod restart {
use {
ratatui::{
prelude::*,
style::Color,
widgets::{block::*, *},
},
splr::{
assign,
solver::{SearchState, Solver as Splr},
EmaIF, PropertyReference,
},
std::collections::VecDeque,
};

const LEN: usize = 80;

#[derive(Debug, Default)]
pub(super) struct Observer {
hist: VecDeque<(usize, f64)>,
cpr: Vec<(f64, f64)>,
spans: Vec<(f64, f64)>,
}

impl Observer {
pub(super) fn reflect(&mut self, solver: &Splr, state: &SearchState) {
let span = state.current_span();
let result = solver
.asg
.refer(assign::property::TEma::ConflictPerRestart)
.get();
self.hist.push_back((span, result));
if LEN < self.hist.len() {
self.hist.pop_front();
}
}
pub(super) fn build_chart<'a>(&'a mut self) -> Chart<'a> {
self.spans = self
.hist
.iter()
.enumerate()
.map(|(i, d)| (i as f64, d.0 as f64))
.collect::<Vec<_>>();
self.cpr = self
.hist
.iter()
.enumerate()
.map(|(i, d)| (i as f64, d.1.log2().clamp(0.0, 8.0)))
.collect::<Vec<_>>();
let x_labels = vec![
Span::styled(format!("-{}", LEN), Style::default()),
Span::styled(format!("-{}", 3 * LEN / 4), Style::default()),
Span::styled(format!("-{}", LEN / 2), Style::default()),
Span::styled(format!("-{}", LEN / 4), Style::default()),
];
let y_labels = vec![
Span::styled("0.0", Style::default()),
Span::styled("2.0", Style::default()),
Span::styled("4.0", Style::default()),
Span::styled("6.0", Style::default()),
Span::styled("8.0", Style::default()),
];
let chart = Chart::new(vec![
// Dataset::default().data(&self.spans),
Dataset::default().data(&self.cpr),
])
.block(
Block::bordered()
.title(" Log-scaled restart gaps ".cyan().bold())
.title_alignment(Alignment::Center),
)
.x_axis(
Axis::default()
.title("Restart")
.style(Style::default().fg(Color::Gray))
.labels(x_labels)
.bounds([0.0, LEN as f64]),
)
.y_axis(
Axis::default()
.title("Restart gaps")
.style(Style::default().fg(Color::Gray))
.labels(y_labels)
.bounds([0.0, 8.0]),
);
chart
}
}
}

#[cfg(feature = "spin")]
mod spin {
use {
Expand All @@ -52,12 +142,12 @@ mod spin {
};

#[derive(Debug, Default)]
pub(super) struct SpinObserver {
pub(super) struct Observer {
var_spin_hist: HashMap<usize, f64>,
spin_stats: [u64; 11],
var_spin_shift_stats: [u64; 21],
}
impl SpinObserver {
impl Observer {
pub fn reflect(&mut self, solver: &Splr) {
let root_level = solver.asg.root_level();
// build spin stats data
Expand Down Expand Up @@ -172,9 +262,10 @@ pub struct App {
solver: Splr,
state: SearchState,
counter: i16,
restart_view: restart::Observer,

#[cfg(feature = "spin")]
spin_view: spin::SpinObserver,
spin_view: spin::Observer,

var_act_hist: HashMap<usize, f64>,
act_stats: [u64; 11],
Expand All @@ -190,9 +281,10 @@ impl App {
act_stats: [0; 11],
var_act_shift_stats: [0; 21],
var_act_hist: HashMap::new(),
restart_view: restart::Observer::default(),

#[cfg(feature = "spin")]
spin_view: spin::SpinObserver::default(),
spin_view: spin::Observer::default(),
}
}
fn run<B: Backend>(&mut self, terminal: &mut Terminal<B>) -> Result<(), Box<dyn Error>> {
Expand Down Expand Up @@ -265,6 +357,7 @@ impl App {
self.var_act_shift_stats[i] = (d * 100.0) as u64;
}

self.restart_view.reflect(&self.solver, &self.state);
#[cfg(feature = "spin")]
self.spin_view.reflect(&self.solver);

Expand Down Expand Up @@ -294,22 +387,29 @@ impl App {
}
}
}
fn render_frame(&self, frame: &mut Frame) {
fn render_frame(&mut self, frame: &mut Frame) {
let chunks = Layout::default()
.direction(Direction::Vertical)
.constraints([
Constraint::Min(5),
Constraint::Min(5),
Constraint::Min(5),
Constraint::Min(5),
])
.constraints(
#[cfg(feature = "spin")]
[
Constraint::Min(5),
Constraint::Min(5),
Constraint::Min(5),
Constraint::Min(5),
Constraint::Min(5),
],
#[cfg(not(feature = "spin"))]
[Constraint::Min(5), Constraint::Min(5), Constraint::Min(5)],
)
.split(frame.area());
frame.render_widget(self.var_activity_bar_chart(), chunks[0]);
frame.render_widget(self.va_history_bar_chart(), chunks[1]);
frame.render_widget(self.restart_view.build_chart(), chunks[2]);
#[cfg(feature = "spin")]
{
frame.render_widget(self.spin_view.build_bar_chart1(), chunks[2]);
frame.render_widget(self.spin_view.build_bar_chart2(), chunks[3]);
frame.render_widget(self.spin_view.build_bar_chart1(), chunks[3]);
frame.render_widget(self.spin_view.build_bar_chart2(), chunks[4]);
}
}
fn handle_events(&mut self) -> io::Result<bool> {
Expand Down
3 changes: 3 additions & 0 deletions src/solver/search.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,9 @@ impl SearchState {
pub fn current_core(&self) -> usize {
self.current_core
}
pub fn current_span(&self) -> usize {
self.current_span
}
}

/// API to [`solve`](`crate::solver::SolveIF::solve`) SAT problems.
Expand Down

0 comments on commit 0b1cb9e

Please sign in to comment.