Skip to content

Commit

Permalink
Remove log option
Browse files Browse the repository at this point in the history
  • Loading branch information
@shnarazk
shnarazk committed Feb 9, 2025
1 parent 257de87 commit 7df2938
Show file tree
Hide file tree
Showing 4 changed files with 5 additions and 107 deletions.
1 change: 1 addition & 0 deletions ChangeLog.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
- Refactor visivility of modules and structs
- Rename `property` to `stats`
- Use struct names directly instead of trait requirements
- Remove log option

## 0.17.6, 2025-02-01

Expand Down
11 changes: 1 addition & 10 deletions src/config.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,9 +48,6 @@ pub struct Config {
/// Writes a DRAT UNSAT certification file
pub use_certification: bool,

/// Uses Glucose-like progress report
pub use_log: bool,

//
//## clause management
//
Expand Down Expand Up @@ -105,7 +102,6 @@ impl Default for Config {
quiet_mode: false,
show_journal: false,
use_certification: false,
use_log: false,

crw_dcy_rat: 0.95,
cls_rdc_lbd: 5,
Expand Down Expand Up @@ -143,9 +139,7 @@ impl Config {
let mut iter = args.skip(1);
while let Some(arg) = iter.next() {
if let Some(stripped) = arg.strip_prefix("--") {
let flags = [
"no-color", "quiet", "certify", "journal", "log", "help", "version",
];
let flags = ["no-color", "quiet", "certify", "journal", "help", "version"];
let options_usize = ["cl", "crl", "stat", "ecl", "evl", "evo"];
let options_f64 = ["timeout", "cdr", "cr1", "cr2", "vdr", "vds"];
let options_path = ["dir", "proof", "result"];
Expand All @@ -159,7 +153,6 @@ impl Config {
"quiet" => self.quiet_mode = true,
"certify" => self.use_certification = true,
"journal" => self.show_journal = true,
"log" => self.use_log = true,
"help" => help = true,
"version" => version = true,
_ => panic!("invalid flag: {name}"),
Expand Down Expand Up @@ -227,7 +220,6 @@ impl Config {
"q" => self.quiet_mode = true,
"c" => self.use_certification = true,
"j" => self.show_journal = true,
"l" => self.use_log = true,
"h" => help = true,
"V" => version = true,
_ => panic!("invalid flag: {name}"),
Expand Down Expand Up @@ -332,7 +324,6 @@ FLAGS:
-q, --quiet Disable any progress message
-c, --certify Writes a DRAT UNSAT certification file
-j, --journal Shows log about restart stages
-l, --log Uses Glucose-like progress report
-V, --version Prints version information
OPTIONS:
--cl <c-cls-lim> Soft limit of #clauses (6MC/GB){:>10}
Expand Down
98 changes: 2 additions & 96 deletions src/state.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -377,10 +377,6 @@ impl StateIF for State {
if !self.config.splr_interface || self.config.quiet_mode {
return;
}
if self.config.use_log {
self.dump_header();
return;
}
if 0 == self.progress_cnt {
self.progress_cnt = 1;
println!("{self}");
Expand All @@ -392,7 +388,7 @@ impl StateIF for State {
}
}
fn flush<S: AsRef<str>>(&self, mes: S) {
if self.config.splr_interface && !self.config.quiet_mode && !self.config.use_log {
if self.config.splr_interface && !self.config.quiet_mode {
if mes.as_ref().is_empty() {
print!("\x1B[1G\x1B[K")
} else {
Expand All @@ -402,7 +398,7 @@ impl StateIF for State {
}
}
fn log<S: AsRef<str>>(&mut self, tick: Option<(Option<usize>, Option<usize>, usize)>, mes: S) {
if self.config.splr_interface && !self.config.quiet_mode && !self.config.use_log {
if self.config.splr_interface && !self.config.quiet_mode {
self.log_messages.insert(
0,
match tick {
Expand Down Expand Up @@ -458,10 +454,6 @@ impl StateIF for State {
let rst_eng: f64 = self.restart.penetration_energy_charged;
let stg_segment: usize = self.stm.current_segment();

if self.config.use_log {
self.dump(asg, cdb);
return;
}
self.progress_cnt += 1;
// print!("\x1B[9A\x1B[1G");
print!("\x1B[");
Expand Down Expand Up @@ -723,92 +715,6 @@ impl IndexMut<LogF64Id> for State {
}
}

impl State {
#[allow(dead_code)]
fn dump_header_details(&self) {
println!(
" #mode, Variable Assignment ,, \
Clause Database ent ,, Restart Strategy ,, \
Misc Progress Parameters,, Eliminator"
);
println!(
" #init, #remain,#asserted,#elim,total%,,#learnt, \
#perm,#binary,,block,force, #asgn, lbd/,, lbd, \
back lv, conf lv,,clause, var"
);
}
fn dump_header(&self) {
println!(
"c | RESTARTS | ORIGINAL FORMULA | LEARNT CLAUSES | Progress |\n\
c | number av. cnfl | Remains Elim-ed Clauses | #rdct Learnts LBD2 | |\n\
c |-------------------|----------------------------|--------------------------|----------|"
);
}
fn dump(&mut self, asg: &AssignStack, cdb: &ClauseDB) {
self.progress_cnt += 1;
let asg_num_vars = VarRef::num_vars();
let asg_num_asserted_vars = asg.num_asserted_vars();
let asg_num_eliminated_vars = asg.num_eliminated_vars();
let asg_num_unasserted_vars = asg.num_unasserted_vars();
let rate = (asg_num_asserted_vars + asg_num_eliminated_vars) as f64 / asg_num_vars as f64;
let asg_num_conflict = asg.num_conflicts();
let asg_num_restart = asg.num_restart();
let cdb_num_clause = cdb.num_clauses();
let cdb_num_lbd2 = cdb.num_lbd2();
let cdb_num_learnt = cdb.num_learnts();
let cdb_num_reduction = cdb.num_reduction();
println!(
"c | {:>8} {:>8} | {:>8} {:>8} {:>8} | {:>4} {:>8} {:>8} | {:>6.3} % |",
asg_num_restart, // restart
asg_num_conflict / asg_num_restart.max(1), // average cfc (Conflict / Restart)
asg_num_unasserted_vars, // alive vars
asg_num_eliminated_vars, // eliminated vars
cdb_num_clause - cdb_num_learnt, // given clauses
cdb_num_reduction, // clause reduction
cdb_num_learnt, // alive learnts
cdb_num_lbd2, // learnts with LBD = 2
rate * 100.0, // progress
);
}
#[allow(dead_code)]
fn dump_details(&mut self, asg: &AssignStack, cdb: &ClauseDB) {
self.progress_cnt += 1;
let asg_num_vars = VarRef::num_vars();
let asg_num_asserted_vars = asg.num_asserted_vars();
let asg_num_eliminated_vars = asg.num_eliminated_vars();
let asg_num_unasserted_vars = asg.num_unasserted_vars();
let rate = (asg_num_asserted_vars + asg_num_eliminated_vars) as f64 / asg_num_vars as f64;
let asg_num_restart = asg.num_restart();
let cdb_num_clause = cdb.num_clauses();
let cdb_num_learnt = cdb.num_learnts();
let rst_asg = asg.assign_rate();
let rst_lbd = cdb.lbd();

println!(
"{:>3},{:>7},{:>7},{:>7},{:>6.3},,{:>7},{:>7},\
{:>7},,{:>5},{:>5},{:>6.2},{:>6.2},,{:>7.2},{:>8.2},{:>8.2},,\
{:>6},{:>6}",
self.progress_cnt,
asg_num_unasserted_vars,
asg_num_asserted_vars,
asg_num_eliminated_vars,
rate * 100.0,
cdb_num_learnt,
cdb_num_clause,
0,
0,
asg_num_restart,
rst_asg.trend(),
rst_lbd.get(),
rst_lbd.trend(),
self.b_lvl.get(),
self.c_lvl.get(),
0, // elim.clause_queue_len(),
0, // elim.var_queue_len(),
);
}
}

/// Index for `Usize` data, used in [`ProgressRecord`](`crate::state::ProgressRecord`).
#[derive(Clone, Copy, Debug)]
pub enum LogUsizeId {
Expand Down
2 changes: 1 addition & 1 deletion src/vam.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,7 @@ use rustc_data_structures::fx::FxHashMap;

/// API for var selection, depending on an internal heap.
pub trait VarSelectIF {
/// give rewards to vars selected by SLS
/// give rewards to the vars selected by SLS
fn reward_by_sls(assignment: &FxHashMap<VarId, bool>) -> usize;
/// select a new decision variable.
fn select_decision_literal(asg: &mut AssignStack) -> Lit;
Expand Down

0 comments on commit 7df2938

Please sign in to comment.