splr/
state.rs

1/// Module `state` is a collection of internal data.
2#[cfg(feature = "platform_wasm")]
3use instant::{Duration, Instant};
4#[cfg(not(feature = "platform_wasm"))]
5use std::time::{Duration, Instant};
6use {
7    crate::{
8        assign, cdb,
9        solver::{RestartManager, SolverEvent, StageManager},
10        types::*,
11    },
12    std::{
13        fmt,
14        io::{stdout, Write},
15        ops::{Index, IndexMut},
16    },
17};
18const PROGRESS_REPORT_ROWS: usize = 7;
19
20/// API for state/statistics management, providing [`progress`](`crate::state::StateIF::progress`).
21pub trait StateIF {
22    /// return `true` if it is timed out.
23    fn is_timeout(&self) -> bool;
24    /// return elapsed time as a fraction.
25    /// return None if something is wrong.
26    fn elapsed(&self) -> Option<f64>;
27    /// write a header of stat data to stdio.
28    fn progress_header(&mut self);
29    /// write stat data to stdio.
30    fn progress<A, C>(&mut self, asg: &A, cdb: &C)
31    where
32        A: PropertyDereference<assign::property::Tusize, usize>
33            + PropertyDereference<assign::property::Tf64, f64>
34            + PropertyReference<assign::property::TEma, EmaView>,
35        C: PropertyDereference<cdb::property::Tusize, usize>
36            + PropertyDereference<cdb::property::Tf64, f64>
37            + PropertyReference<cdb::property::TEma, EmaView>;
38    /// write a short message to stdout.
39    fn flush<S: AsRef<str>>(&self, mes: S);
40    /// write a one-line message as log.
41    fn log<S: AsRef<str>>(&mut self, tick: Option<(Option<usize>, Option<usize>, usize)>, mes: S);
42}
43
44/// stat index.
45#[derive(Clone, Eq, PartialEq)]
46pub enum Stat {
47    Restart,
48    /// the number of vivification
49    Vivification,
50    /// the number of vivified (shrunk) clauses
51    VivifiedClause,
52    /// the number of vivified (asserted) vars
53    VivifiedVar,
54    /// the number of invocations of simplify
55    Simplify,
56    /// the number of subsumed clause by processor
57    SubsumedClause,
58    /// for SLS
59    SLS,
60    /// don't use this dummy (sentinel at the tail).
61    EndOfStatIndex,
62}
63
64impl Index<Stat> for [usize] {
65    type Output = usize;
66    #[inline]
67    fn index(&self, i: Stat) -> &usize {
68        #[cfg(feature = "unsafe_access")]
69        unsafe {
70            self.get_unchecked(i as usize)
71        }
72        #[cfg(not(feature = "unsafe_access"))]
73        &self[i as usize]
74    }
75}
76
77impl IndexMut<Stat> for [usize] {
78    #[inline]
79    fn index_mut(&mut self, i: Stat) -> &mut usize {
80        #[cfg(feature = "unsafe_access")]
81        unsafe {
82            self.get_unchecked_mut(i as usize)
83        }
84        #[cfg(not(feature = "unsafe_access"))]
85        &mut self[i as usize]
86    }
87}
88
89/// Data storage for [`Solver`](`crate::solver::Solver`).
90#[derive(Clone, Debug)]
91pub struct State {
92    /// solver configuration
93    pub config: Config,
94    /// the problem.
95    pub cnf: CNFDescription,
96    /// collection of statistics data
97    pub stats: [usize; Stat::EndOfStatIndex as usize],
98    // Restart
99    pub restart: RestartManager,
100    /// StageManager
101    pub stm: StageManager,
102    /// problem description
103    pub target: CNFDescription,
104    /// strategy adjustment interval in conflict
105    pub reflection_interval: usize,
106
107    //
108    //## MISC
109    //
110    /// EMA of backjump levels
111    pub b_lvl: Ema,
112    /// EMA of conflicting levels
113    pub c_lvl: Ema,
114    /// EMA of c_lbd - b_lbd, or Exploration vs. Eploitation
115    pub e_mode: Ema2,
116    pub e_mode_threshold: f64,
117    pub exploration_rate_ema: Ema,
118
119    #[cfg(feature = "support_user_assumption")]
120    /// hold conflicting user-defined *assumed* literals for UNSAT problems
121    pub conflicts: Vec<Lit>,
122
123    #[cfg(feature = "chronoBT")]
124    /// chronoBT threshold
125    pub chrono_bt_threshold: DecisionLevel,
126
127    /// hold the previous number of non-conflicting assignment
128    pub last_asg: usize,
129    /// working place to build learnt clauses
130    pub new_learnt: Vec<Lit>,
131    /// working place to store given clauses' ids which is used to derive a good learnt
132    pub derive20: Vec<ClauseId>,
133    /// `progress` invocation counter
134    pub progress_cnt: usize,
135    /// keep the previous statistics values
136    pub record: ProgressRecord,
137    /// progress of SLS
138    pub sls_index: usize,
139    /// start clock for timeout handling
140    pub start: Instant,
141    /// upper limit for timeout handling
142    pub time_limit: f64,
143    /// logging facility.
144    log_messages: Vec<String>,
145}
146
147impl Default for State {
148    fn default() -> State {
149        State {
150            config: Config::default(),
151            cnf: CNFDescription::default(),
152            stats: [0; Stat::EndOfStatIndex as usize],
153            restart: RestartManager::default(),
154            stm: StageManager::default(),
155            target: CNFDescription::default(),
156            reflection_interval: 10_000,
157
158            b_lvl: Ema::new(5_000),
159            c_lvl: Ema::new(5_000),
160            e_mode: Ema2::new(40).with_slow(4_000).with_value(10.0),
161            e_mode_threshold: 1.20,
162            exploration_rate_ema: Ema::new(1000),
163
164            #[cfg(feature = "support_user_assumption")]
165            conflicts: Vec::new(),
166
167            #[cfg(feature = "chronoBT")]
168            chrono_bt_threshold: 100,
169
170            last_asg: 0,
171            new_learnt: Vec::new(),
172            derive20: Vec::new(),
173            progress_cnt: 0,
174            record: ProgressRecord::default(),
175            sls_index: 0,
176            start: Instant::now(),
177            time_limit: 0.0,
178            log_messages: Vec::new(),
179        }
180    }
181}
182
183impl Index<Stat> for State {
184    type Output = usize;
185    #[inline]
186    fn index(&self, i: Stat) -> &usize {
187        #[cfg(feature = "unsafe_access")]
188        unsafe {
189            self.stats.get_unchecked(i as usize)
190        }
191        #[cfg(not(feature = "unsafe_access"))]
192        &self.stats[i as usize]
193    }
194}
195
196impl IndexMut<Stat> for State {
197    #[inline]
198    fn index_mut(&mut self, i: Stat) -> &mut usize {
199        #[cfg(feature = "unsafe_access")]
200        unsafe {
201            self.stats.get_unchecked_mut(i as usize)
202        }
203        #[cfg(not(feature = "unsafe_access"))]
204        &mut self.stats[i as usize]
205    }
206}
207
208impl Instantiate for State {
209    fn instantiate(config: &Config, cnf: &CNFDescription) -> State {
210        State {
211            config: config.clone(),
212            cnf: cnf.clone(),
213            restart: RestartManager::instantiate(config, cnf),
214            stm: StageManager::instantiate(config, cnf),
215            target: cnf.clone(),
216            time_limit: config.c_timeout,
217            ..State::default()
218        }
219    }
220    fn handle(&mut self, e: SolverEvent) {
221        match e {
222            SolverEvent::NewVar => {
223                self.target.num_of_variables += 1;
224            }
225            SolverEvent::Assert(_) => (),
226            SolverEvent::Conflict => (),
227            SolverEvent::Eliminate(_) => (),
228            SolverEvent::Instantiate => (),
229            SolverEvent::Reinitialize => (),
230            SolverEvent::Restart => {
231                self[Stat::Restart] += 1;
232                self.restart.handle(SolverEvent::Restart);
233            }
234            SolverEvent::Stage(_) => (),
235
236            #[cfg(feature = "clause_vivification")]
237            SolverEvent::Vivify(_) => (),
238        }
239    }
240}
241
242macro_rules! im {
243    ($format: expr, $state: expr, $key: expr, $val: expr) => {
244        match ($val, $key) {
245            (v, LogUsizeId::End) => format!($format, v),
246            (v, k) => {
247                let ptr = &mut $state.record[k];
248                if $state.config.no_color {
249                    *ptr = v;
250                    format!($format, *ptr)
251                } else if (v as f64) * 1.6 < *ptr as f64 {
252                    *ptr = v;
253                    format!("\x1B[001m\x1B[031m{}\x1B[000m", format!($format, *ptr))
254                } else if v < *ptr {
255                    *ptr = v;
256                    format!("\x1B[031m{}\x1B[000m", format!($format, *ptr))
257                } else if (*ptr as f64) * 1.6 < v as f64 {
258                    *ptr = v;
259                    format!("\x1B[001m\x1B[036m{}\x1B[000m", format!($format, *ptr))
260                } else if *ptr < v {
261                    *ptr = v;
262                    format!("\x1B[036m{}\x1B[000m", format!($format, *ptr))
263                } else {
264                    *ptr = v;
265                    format!($format, *ptr)
266                }
267            }
268        }
269    };
270    ($format: expr, $state: expr, $key: expr, $val: expr, $threshold: expr) => {
271        match ($val, $key) {
272            (v, LogUsizeId::End) => format!($format, v),
273            (v, k) => {
274                let ptr = &mut $state.record[k];
275                if $state.config.no_color {
276                    *ptr = v;
277                    format!($format, *ptr)
278                } else if v < $threshold {
279                    *ptr = v;
280                    format!("\x1B[031m{}\x1B[000m", format!($format, *ptr))
281                } else if $threshold < v {
282                    *ptr = v;
283                    format!("\x1B[036m{}\x1B[000m", format!($format, *ptr))
284                } else {
285                    *ptr = v;
286                    format!($format, *ptr)
287                }
288            }
289        }
290    };
291}
292
293macro_rules! i {
294    ($format: expr, $state: expr, $key: expr, $val: expr) => {
295        match ($val, $key) {
296            (v, LogUsizeId::End) => format!($format, v),
297            (v, k) => {
298                let ptr = &mut $state.record[k];
299                *ptr = v;
300                format!($format, *ptr)
301            }
302        }
303    };
304}
305
306macro_rules! fm {
307    ($format: expr, $state: expr, $key: expr, $val: expr) => {
308        match ($val, $key) {
309            (v, LogF64Id::End) => format!($format, v),
310            (v, k) => {
311                let ptr = &mut $state.record[k];
312                if $state.config.no_color {
313                    *ptr = v;
314                    format!($format, *ptr)
315                } else if v * 1.6 < *ptr {
316                    *ptr = v;
317                    format!("\x1B[001m\x1B[031m{}\x1B[000m", format!($format, *ptr))
318                } else if v < *ptr {
319                    *ptr = v;
320                    format!("\x1B[031m{}\x1B[000m", format!($format, *ptr))
321                } else if *ptr * 1.6 < v {
322                    *ptr = v;
323                    format!("\x1B[001m\x1B[036m{}\x1B[000m", format!($format, *ptr))
324                } else if *ptr < v {
325                    *ptr = v;
326                    format!("\x1B[036m{}\x1B[000m", format!($format, *ptr))
327                } else {
328                    *ptr = v;
329                    format!($format, *ptr)
330                }
331            }
332        }
333    };
334    ($format: expr, $state: expr, $key: expr, $val: expr, $threshold: expr) => {
335        match ($val, $key) {
336            (v, LogF64Id::End) => format!($format, v),
337            (v, k) => {
338                let ptr = &mut $state.record[k];
339                if $state.config.no_color {
340                    *ptr = v;
341                    format!($format, *ptr)
342                } else if v < $threshold {
343                    *ptr = v;
344                    format!("\x1B[031m{}\x1B[000m", format!($format, *ptr))
345                } else if $threshold < v {
346                    *ptr = v;
347                    format!("\x1B[036m{}\x1B[000m", format!($format, *ptr))
348                } else {
349                    *ptr = v;
350                    format!($format, *ptr)
351                }
352            }
353        }
354    };
355}
356
357#[allow(unused_macros)]
358macro_rules! f {
359    ($format: expr, $state: expr, $key: expr, $val: expr) => {
360        match ($val, $key) {
361            (v, LogF64Id::End) => format!($format, v),
362            (v, k) => {
363                let ptr = &mut $state.record[k];
364                *ptr = v;
365                format!($format, *ptr)
366            }
367        }
368    };
369}
370
371impl StateIF for State {
372    fn is_timeout(&self) -> bool {
373        Duration::from_secs(self.config.c_timeout as u64) < self.start.elapsed()
374    }
375    fn elapsed(&self) -> Option<f64> {
376        Some(
377            self.start.elapsed().as_secs_f64()
378                / Duration::from_secs(self.config.c_timeout as u64).as_secs_f64(),
379        )
380    }
381    fn progress_header(&mut self) {
382        if !self.config.splr_interface || self.config.quiet_mode {
383            return;
384        }
385        if self.config.use_log {
386            self.dump_header();
387            return;
388        }
389        if 0 == self.progress_cnt {
390            self.progress_cnt = 1;
391            println!("{self}");
392
393            //## PROGRESS REPORT ROWS
394            for _i in 0..PROGRESS_REPORT_ROWS - 1 {
395                println!("                                                  ");
396            }
397        }
398    }
399    fn flush<S: AsRef<str>>(&self, mes: S) {
400        if self.config.splr_interface && !self.config.quiet_mode && !self.config.use_log {
401            if mes.as_ref().is_empty() {
402                print!("\x1B[1G\x1B[K")
403            } else {
404                print!("{}", mes.as_ref());
405            }
406            stdout().flush().unwrap();
407        }
408    }
409    fn log<S: AsRef<str>>(&mut self, tick: Option<(Option<usize>, Option<usize>, usize)>, mes: S) {
410        if self.config.splr_interface && !self.config.quiet_mode && !self.config.use_log {
411            self.log_messages.insert(
412                0,
413                match tick {
414                    Some((Some(seg), Some(cyc), stg)) => {
415                        format!("stage({:>2},{:>4},{:>5}): {}", seg, cyc, stg, mes.as_ref())
416                    }
417                    Some((None, Some(cyc), stg)) => {
418                        format!("stage(  ,{:>4},{:>5}): {}", cyc, stg, mes.as_ref())
419                    }
420                    Some((None, None, stg)) => {
421                        format!("stage(  ,    ,{:>5}): {}", stg, mes.as_ref())
422                    }
423                    Some(_) => unreachable!(),
424                    None => format!("### {}", mes.as_ref()),
425                },
426            );
427        }
428    }
429    /// `mes` should be shorter than or equal to 9, or 8 + a delimiter.
430    #[allow(clippy::cognitive_complexity)]
431    fn progress<A, C>(&mut self, asg: &A, cdb: &C)
432    where
433        A: PropertyDereference<assign::property::Tusize, usize>
434            + PropertyDereference<assign::property::Tf64, f64>
435            + PropertyReference<assign::property::TEma, EmaView>,
436        C: PropertyDereference<cdb::property::Tusize, usize>
437            + PropertyDereference<cdb::property::Tf64, f64>
438            + PropertyReference<cdb::property::TEma, EmaView>,
439    {
440        if !self.config.splr_interface || self.config.quiet_mode {
441            self.log_messages.clear();
442            self.record_stats(asg, cdb);
443            return;
444        }
445
446        //
447        //## Gather stats from all modules
448        //
449        let asg_num_vars = asg.derefer(assign::property::Tusize::NumVar);
450        let asg_num_asserted_vars = asg.derefer(assign::property::Tusize::NumAssertedVar);
451        let asg_num_eliminated_vars = asg.derefer(assign::property::Tusize::NumEliminatedVar);
452        let asg_num_unasserted_vars = asg.derefer(assign::property::Tusize::NumUnassertedVar);
453        let asg_num_unreachables = asg.derefer(assign::property::Tusize::NumUnreachableVar);
454        let rate = (asg_num_asserted_vars + asg_num_eliminated_vars) as f64 / asg_num_vars as f64;
455        let asg_num_conflict = asg.derefer(assign::property::Tusize::NumConflict);
456        let asg_num_decision = asg.derefer(assign::property::Tusize::NumDecision);
457        let asg_num_propagation = asg.derefer(assign::property::Tusize::NumPropagation);
458        // let asg_cwss: f64 = asg.derefer(assign::property::Tf64::CurrentWorkingSetSize);
459        let asg_dpc_ema = asg.refer(assign::property::TEma::DecisionPerConflict);
460        let asg_ppc_ema = asg.refer(assign::property::TEma::PropagationPerConflict);
461        let asg_cpr_ema = asg.refer(assign::property::TEma::ConflictPerRestart);
462
463        let cdb_num_clause = cdb.derefer(cdb::property::Tusize::NumClause);
464        let cdb_num_bi_clause = cdb.derefer(cdb::property::Tusize::NumBiClause);
465        let cdb_num_lbd2 = cdb.derefer(cdb::property::Tusize::NumLBD2);
466        let cdb_num_learnt = cdb.derefer(cdb::property::Tusize::NumLearnt);
467        let cdb_lb_ent: f64 = cdb.derefer(cdb::property::Tf64::LiteralBlockEntanglement);
468        let rst_num_rst: usize = self[Stat::Restart];
469        let rst_asg: &EmaView = asg.refer(assign::property::TEma::AssignRate);
470        let rst_lbd: &EmaView = cdb.refer(cdb::property::TEma::LBD);
471        let rst_eng: f64 = self.restart.penetration_energy_charged;
472        let stg_segment: usize = self.stm.current_segment();
473
474        if self.config.use_log {
475            self.dump(asg, cdb);
476            return;
477        }
478        self.progress_cnt += 1;
479        // print!("\x1B[9A\x1B[1G");
480        print!("\x1B[");
481        print!("{PROGRESS_REPORT_ROWS}");
482        print!("A\x1B[1G");
483
484        if self.config.show_journal {
485            while let Some(m) = self.log_messages.pop() {
486                if self.config.no_color {
487                    println!("{m}");
488                } else {
489                    println!("\x1B[2K\x1B[000m\x1B[034m{m}\x1B[000m");
490                }
491            }
492        } else {
493            self.log_messages.clear();
494        }
495        println!("\x1B[2K{self}");
496        println!(
497            "\x1B[2K #conflict:{}, #decision:{}, #propagate:{}",
498            i!("{:>11}", self, LogUsizeId::NumConflict, asg_num_conflict),
499            i!("{:>13}", self, LogUsizeId::NumDecision, asg_num_decision),
500            i!(
501                "{:>15}",
502                self,
503                LogUsizeId::NumPropagate,
504                asg_num_propagation
505            ),
506        );
507        println!(
508            "\x1B[2K  Assignment|#rem:{}, #fix:{}, #elm:{}, prg%:{}",
509            im!(
510                "{:>9}",
511                self,
512                LogUsizeId::RemainingVar,
513                asg_num_unasserted_vars
514            ),
515            im!(
516                "{:>9}",
517                self,
518                LogUsizeId::AssertedVar,
519                asg_num_asserted_vars
520            ),
521            im!(
522                "{:>9}",
523                self,
524                LogUsizeId::EliminatedVar,
525                asg_num_eliminated_vars
526            ),
527            fm!("{:>9.4}", self, LogF64Id::Progress, rate * 100.0),
528        );
529        println!(
530            "\x1B[2K      Clause|Remv:{}, LBD2:{}, BinC:{}, Perm:{}",
531            im!("{:>9}", self, LogUsizeId::RemovableClause, cdb_num_learnt),
532            im!("{:>9}", self, LogUsizeId::LBD2Clause, cdb_num_lbd2),
533            im!(
534                "{:>9}",
535                self,
536                LogUsizeId::BiClause,
537                cdb_num_bi_clause // cdb_num_bi_learnt
538            ),
539            im!(
540                "{:>9}",
541                self,
542                LogUsizeId::PermanentClause,
543                cdb_num_clause - cdb_num_learnt
544            ),
545        );
546        self[LogUsizeId::StageSegment] = stg_segment;
547        self[LogF64Id::RestartEnergy] = rst_eng;
548        self[LogF64Id::TrendASG] = rst_asg.trend();
549        println!(
550            "\x1B[2K    Conflict|entg:{}, cLvl:{}, bLvl:{}, /cpr:{}",
551            fm!(
552                "{:>9.4}",
553                self,
554                LogF64Id::LiteralBlockEntanglement,
555                cdb_lb_ent
556            ),
557            fm!("{:>9.4}", self, LogF64Id::CLevel, self.c_lvl.get()),
558            fm!("{:>9.4}", self, LogF64Id::BLevel, self.b_lvl.get()),
559            fm!(
560                "{:>9.2}",
561                self,
562                LogF64Id::ConflictPerRestart,
563                asg_cpr_ema.get()
564            )
565        );
566        println!(
567            "\x1B[2K    Learning|avrg:{}, trnd:{}, #RST:{}, /dpc:{}",
568            fm!("{:>9.4}", self, LogF64Id::EmaLBD, rst_lbd.get_fast()),
569            fm!("{:>9.4}", self, LogF64Id::TrendLBD, rst_lbd.trend()),
570            im!("{:>9}", self, LogUsizeId::Restart, rst_num_rst),
571            fm!(
572                "{:>9.2}",
573                self,
574                LogF64Id::DecisionPerConflict,
575                asg_dpc_ema.get()
576            ),
577        );
578        println!(
579            "\x1B[2K        misc|vivC:{}, xplr:{}, core:{}, /ppc:{}",
580            im!(
581                "{:>9}",
582                self,
583                LogUsizeId::VivifiedClause,
584                self[Stat::VivifiedClause]
585            ),
586            fm!(
587                "{:>9.4}",
588                self,
589                LogF64Id::ExExTrend,
590                // self.e_mode.trend(),
591                self.exploration_rate_ema.get() // , self.e_mode_threshold
592            ),
593            im!(
594                "{:>9}",
595                self,
596                LogUsizeId::UnreachableCore,
597                if asg_num_unreachables == 0 {
598                    self[LogUsizeId::UnreachableCore]
599                } else {
600                    asg_num_unreachables
601                }
602            ),
603            fm!(
604                "{:>9.2}",
605                self,
606                LogF64Id::PropagationPerConflict,
607                asg_ppc_ema.get()
608            ),
609        );
610        self[LogUsizeId::Stage] = self.stm.current_stage();
611        self[LogUsizeId::StageCycle] = self.stm.current_cycle();
612        self[LogUsizeId::Vivify] = self[Stat::Vivification];
613        self.flush("");
614    }
615}
616
617impl State {
618    #[allow(clippy::cognitive_complexity)]
619    fn record_stats<A, C>(&mut self, asg: &A, cdb: &C)
620    where
621        A: PropertyDereference<assign::property::Tusize, usize>
622            + PropertyReference<assign::property::TEma, EmaView>,
623        C: PropertyDereference<cdb::property::Tusize, usize>
624            + PropertyDereference<cdb::property::Tf64, f64>
625            + PropertyReference<cdb::property::TEma, EmaView>,
626    {
627        self[LogUsizeId::NumConflict] = asg.derefer(assign::property::Tusize::NumConflict);
628        self[LogUsizeId::NumDecision] = asg.derefer(assign::property::Tusize::NumDecision);
629        self[LogUsizeId::NumPropagate] = asg.derefer(assign::property::Tusize::NumPropagation);
630        self[LogUsizeId::RemainingVar] = asg.derefer(assign::property::Tusize::NumUnassertedVar);
631        self[LogUsizeId::AssertedVar] = asg.derefer(assign::property::Tusize::NumAssertedVar);
632        self[LogUsizeId::EliminatedVar] = asg.derefer(assign::property::Tusize::NumEliminatedVar);
633        self[LogF64Id::Progress] = 100.0
634            * (self[LogUsizeId::AssertedVar]
635                + asg.derefer(assign::property::Tusize::NumEliminatedVar)) as f64
636            / asg.derefer(assign::property::Tusize::NumVar) as f64;
637        self[LogUsizeId::RemovableClause] = cdb.derefer(cdb::property::Tusize::NumLearnt);
638        self[LogUsizeId::LBD2Clause] = cdb.derefer(cdb::property::Tusize::NumLBD2);
639        self[LogUsizeId::BiClause] = cdb.derefer(cdb::property::Tusize::NumBiClause);
640        self[LogUsizeId::PermanentClause] =
641            cdb.derefer(cdb::property::Tusize::NumClause) - self[LogUsizeId::RemovableClause];
642        self[LogUsizeId::Restart] = self[Stat::Restart];
643        self[LogUsizeId::Stage] = self.stm.current_stage();
644        self[LogUsizeId::StageCycle] = self.stm.current_cycle();
645        self[LogUsizeId::StageSegment] = self.stm.max_scale();
646        self[LogUsizeId::Simplify] = self[Stat::Simplify];
647        self[LogUsizeId::SubsumedClause] = self[Stat::SubsumedClause];
648        self[LogUsizeId::VivifiedClause] = self[Stat::VivifiedClause];
649        self[LogUsizeId::VivifiedVar] = self[Stat::VivifiedVar];
650        self[LogUsizeId::Vivify] = self[Stat::Vivification];
651        let rst_lbd: &EmaView = cdb.refer(cdb::property::TEma::LBD);
652        self[LogF64Id::EmaLBD] = rst_lbd.get_fast();
653        self[LogF64Id::TrendLBD] = rst_lbd.trend();
654
655        self[LogF64Id::LiteralBlockEntanglement] =
656            cdb.derefer(cdb::property::Tf64::LiteralBlockEntanglement);
657        self[LogF64Id::DecisionPerConflict] =
658            asg.refer(assign::property::TEma::DecisionPerConflict).get();
659
660        self[LogF64Id::TrendASG] = asg.refer(assign::property::TEma::AssignRate).trend();
661        self[LogF64Id::CLevel] = self.c_lvl.get();
662        self[LogF64Id::BLevel] = self.b_lvl.get();
663        self[LogF64Id::PropagationPerConflict] = asg
664            .refer(assign::property::TEma::PropagationPerConflict)
665            .get();
666        {
667            let core = asg.derefer(assign::property::Tusize::NumUnreachableVar);
668            if 0 < core {
669                self[LogUsizeId::UnreachableCore] = core;
670            }
671        }
672        self[LogF64Id::ConflictPerRestart] =
673            asg.refer(assign::property::TEma::ConflictPerRestart).get();
674    }
675}
676
677impl fmt::Display for State {
678    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
679        let tm: f64 = (self.start.elapsed().as_millis() as f64) / 1_000.0;
680        let vc = format!(
681            "{},{}",
682            self.target.num_of_variables, self.target.num_of_clauses,
683        );
684        let vclen = vc.len();
685        let width = 59;
686        let mut fname = match &self.target.pathname {
687            CNFIndicator::Void => "(no cnf)".to_string(),
688            CNFIndicator::File(f) => f.to_string(),
689            CNFIndicator::LitVec(n) => format!("(embedded {n} element vector)"),
690        };
691        if width <= fname.len() {
692            fname.truncate(58 - vclen);
693        }
694        let fnlen = fname.len();
695        if width < vclen + fnlen + 1 {
696            write!(f, "{fname:<width$} |time:{tm:>9.2}")
697        } else {
698            write!(f, "{fname}{:>w$} |time:{tm:>9.2}", &vc, w = width - fnlen,)
699        }
700    }
701}
702
703impl Index<LogUsizeId> for State {
704    type Output = usize;
705    #[inline]
706    fn index(&self, i: LogUsizeId) -> &Self::Output {
707        #[cfg(feature = "unsafe_access")]
708        unsafe {
709            self.record.vali.get_unchecked(i as usize)
710        }
711        #[cfg(not(feature = "unsafe_access"))]
712        &self.record.vali[i as usize]
713    }
714}
715
716impl IndexMut<LogUsizeId> for State {
717    #[inline]
718    fn index_mut(&mut self, i: LogUsizeId) -> &mut Self::Output {
719        #[cfg(feature = "unsafe_access")]
720        unsafe {
721            self.record.vali.get_unchecked_mut(i as usize)
722        }
723        #[cfg(not(feature = "unsafe_access"))]
724        &mut self.record.vali[i as usize]
725    }
726}
727
728impl Index<LogF64Id> for State {
729    type Output = f64;
730    #[inline]
731    fn index(&self, i: LogF64Id) -> &Self::Output {
732        #[cfg(feature = "unsafe_access")]
733        unsafe {
734            self.record.valf.get_unchecked(i as usize)
735        }
736        #[cfg(not(feature = "unsafe_access"))]
737        &self.record.valf[i as usize]
738    }
739}
740
741impl IndexMut<LogF64Id> for State {
742    #[inline]
743    fn index_mut(&mut self, i: LogF64Id) -> &mut Self::Output {
744        #[cfg(feature = "unsafe_access")]
745        unsafe {
746            self.record.valf.get_unchecked_mut(i as usize)
747        }
748        #[cfg(not(feature = "unsafe_access"))]
749        &mut self.record.valf[i as usize]
750    }
751}
752
753impl State {
754    #[allow(dead_code)]
755    fn dump_header_details(&self) {
756        println!(
757            "   #mode,         Variable Assignment      ,,  \
758             Clause Database ent  ,,  Restart Strategy       ,, \
759             Misc Progress Parameters,,   Eliminator"
760        );
761        println!(
762            "   #init,    #remain,#asserted,#elim,total%,,#learnt,  \
763             #perm,#binary,,block,force, #asgn,  lbd/,,    lbd, \
764             back lv, conf lv,,clause,   var"
765        );
766    }
767    fn dump_header(&self) {
768        println!(
769            "c |      RESTARTS     |       ORIGINAL FORMULA     |       LEARNT CLAUSES     | Progress |\n\
770             c |   number av. cnfl |  Remains  Elim-ed  Clauses | #rdct   Learnts     LBD2 |          |\n\
771             c |-------------------|----------------------------|--------------------------|----------|"
772        );
773    }
774    fn dump<A, C>(&mut self, asg: &A, cdb: &C)
775    where
776        A: PropertyDereference<assign::property::Tusize, usize>,
777        C: PropertyDereference<cdb::property::Tusize, usize>,
778    {
779        self.progress_cnt += 1;
780        let asg_num_vars = asg.derefer(assign::property::Tusize::NumVar);
781        let asg_num_asserted_vars = asg.derefer(assign::property::Tusize::NumAssertedVar);
782        let asg_num_eliminated_vars = asg.derefer(assign::property::Tusize::NumEliminatedVar);
783        let asg_num_unasserted_vars = asg.derefer(assign::property::Tusize::NumUnassertedVar);
784        let rate = (asg_num_asserted_vars + asg_num_eliminated_vars) as f64 / asg_num_vars as f64;
785        let asg_num_conflict = asg.derefer(assign::property::Tusize::NumConflict);
786        let asg_num_restart = asg.derefer(assign::property::Tusize::NumRestart);
787        let cdb_num_clause = cdb.derefer(cdb::property::Tusize::NumClause);
788        let cdb_num_lbd2 = cdb.derefer(cdb::property::Tusize::NumLBD2);
789        let cdb_num_learnt = cdb.derefer(cdb::property::Tusize::NumLearnt);
790        let cdb_num_reduction = cdb.derefer(cdb::property::Tusize::NumReduction);
791        println!(
792            "c | {:>8} {:>8} | {:>8} {:>8} {:>8} |  {:>4}  {:>8} {:>8} | {:>6.3} % |",
793            asg_num_restart,                           // restart
794            asg_num_conflict / asg_num_restart.max(1), // average cfc (Conflict / Restart)
795            asg_num_unasserted_vars,                   // alive vars
796            asg_num_eliminated_vars,                   // eliminated vars
797            cdb_num_clause - cdb_num_learnt,           // given clauses
798            cdb_num_reduction,                         // clause reduction
799            cdb_num_learnt,                            // alive learnts
800            cdb_num_lbd2,                              // learnts with LBD = 2
801            rate * 100.0,                              // progress
802        );
803    }
804    #[allow(dead_code)]
805    fn dump_details<A, C>(&mut self, asg: &A, cdb: &C)
806    where
807        A: PropertyDereference<assign::property::Tusize, usize>
808            + PropertyReference<assign::property::TEma, EmaView>,
809        C: PropertyDereference<cdb::property::Tusize, usize>
810            + PropertyReference<cdb::property::TEma, EmaView>,
811    {
812        self.progress_cnt += 1;
813        let asg_num_vars = asg.derefer(assign::property::Tusize::NumVar);
814        let asg_num_asserted_vars = asg.derefer(assign::property::Tusize::NumAssertedVar);
815        let asg_num_eliminated_vars = asg.derefer(assign::property::Tusize::NumEliminatedVar);
816        let asg_num_unasserted_vars = asg.derefer(assign::property::Tusize::NumUnassertedVar);
817        let rate = (asg_num_asserted_vars + asg_num_eliminated_vars) as f64 / asg_num_vars as f64;
818        let asg_num_restart = asg.derefer(assign::property::Tusize::NumRestart);
819        let cdb_num_clause = cdb.derefer(cdb::property::Tusize::NumClause);
820        let cdb_num_learnt = cdb.derefer(cdb::property::Tusize::NumLearnt);
821        let rst_asg = asg.refer(assign::property::TEma::AssignRate);
822        let rst_lbd = cdb.refer(cdb::property::TEma::LBD);
823
824        println!(
825            "{:>3},{:>7},{:>7},{:>7},{:>6.3},,{:>7},{:>7},\
826             {:>7},,{:>5},{:>5},{:>6.2},{:>6.2},,{:>7.2},{:>8.2},{:>8.2},,\
827             {:>6},{:>6}",
828            self.progress_cnt,
829            asg_num_unasserted_vars,
830            asg_num_asserted_vars,
831            asg_num_eliminated_vars,
832            rate * 100.0,
833            cdb_num_learnt,
834            cdb_num_clause,
835            0,
836            0,
837            asg_num_restart,
838            rst_asg.trend(),
839            rst_lbd.get(),
840            rst_lbd.trend(),
841            self.b_lvl.get(),
842            self.c_lvl.get(),
843            0, // elim.clause_queue_len(),
844            0, // elim.var_queue_len(),
845        );
846    }
847}
848
849/// Index for `Usize` data, used in [`ProgressRecord`](`crate::state::ProgressRecord`).
850#[derive(Clone, Copy, Debug)]
851pub enum LogUsizeId {
852    //
853    //## primary stats
854    //
855    NumConflict = 0,
856    NumPropagate,
857    NumDecision,
858
859    //
860    //## vars
861    //
862    RemainingVar,
863    AssertedVar,
864    EliminatedVar,
865    UnreachableCore,
866
867    //
868    //## clause
869    //
870    RemovableClause,
871    LBD2Clause,
872    BiClause,
873    PermanentClause,
874
875    //
876    //## restart
877    //
878    Restart,
879
880    //
881    //## stage
882    //
883    Stage,
884    StageCycle,
885    StageSegment,
886
887    //
888    //## pre(in)-processor
889    //
890    Simplify,
891    SubsumedClause,
892    VivifiedClause,
893    VivifiedVar,
894    Vivify,
895
896    //
897    //## Stochastic Local Search
898    //
899    SLS,
900
901    // the sentinel
902    End,
903}
904
905/// Index for `f64` data, used in [`ProgressRecord`](`crate::state::ProgressRecord`).
906#[derive(Clone, Copy, Debug)]
907pub enum LogF64Id {
908    Progress = 0,
909    EmaASG,
910    EmaCCC,
911    EmaLBD,
912    EmaMLD,
913    TrendASG,
914    TrendLBD,
915    BLevel,
916    CLevel,
917    ExExTrend,
918    DecisionPerConflict,
919    ConflictPerRestart,
920    PropagationPerConflict,
921    LiteralBlockEntanglement,
922    RestartEnergy,
923
924    End,
925}
926
927/// Record of old stats.
928#[derive(Clone, Debug)]
929pub struct ProgressRecord {
930    pub vali: [usize; LogUsizeId::End as usize],
931    pub valf: [f64; LogF64Id::End as usize],
932}
933
934impl Default for ProgressRecord {
935    fn default() -> ProgressRecord {
936        ProgressRecord {
937            vali: [0; LogUsizeId::End as usize],
938            valf: [0.0; LogF64Id::End as usize],
939        }
940    }
941}
942
943impl Index<LogUsizeId> for ProgressRecord {
944    type Output = usize;
945    #[inline]
946    fn index(&self, i: LogUsizeId) -> &usize {
947        #[cfg(feature = "unsafe_access")]
948        unsafe {
949            self.vali.get_unchecked(i as usize)
950        }
951        #[cfg(not(feature = "unsafe_access"))]
952        &self.vali[i as usize]
953    }
954}
955
956impl IndexMut<LogUsizeId> for ProgressRecord {
957    #[inline]
958    fn index_mut(&mut self, i: LogUsizeId) -> &mut usize {
959        #[cfg(feature = "unsafe_access")]
960        unsafe {
961            self.vali.get_unchecked_mut(i as usize)
962        }
963        #[cfg(not(feature = "unsafe_access"))]
964        &mut self.vali[i as usize]
965    }
966}
967
968impl Index<LogF64Id> for ProgressRecord {
969    type Output = f64;
970    #[inline]
971    fn index(&self, i: LogF64Id) -> &f64 {
972        #[cfg(feature = "unsafe_access")]
973        unsafe {
974            self.valf.get_unchecked(i as usize)
975        }
976        #[cfg(not(feature = "unsafe_access"))]
977        &self.valf[i as usize]
978    }
979}
980
981impl IndexMut<LogF64Id> for ProgressRecord {
982    #[inline]
983    fn index_mut(&mut self, i: LogF64Id) -> &mut f64 {
984        #[cfg(feature = "unsafe_access")]
985        unsafe {
986            self.valf.get_unchecked_mut(i as usize)
987        }
988        #[cfg(not(feature = "unsafe_access"))]
989        &mut self.valf[i as usize]
990    }
991}
992
993pub mod property {
994    use super::*;
995
996    #[derive(Clone, Copy, Debug, Eq, PartialEq)]
997    pub enum Tusize {
998        /// the number of vivification
999        Vivification,
1000        /// the number of vivified (shrunk) clauses
1001        VivifiedClause,
1002        /// the number of vivified (asserted) vars
1003        VivifiedVar,
1004
1005        //
1006        //## from stageManager
1007        //
1008        NumCycle,
1009        NumStage,
1010        IntervalScale,
1011        IntervalScaleMax,
1012    }
1013
1014    pub const USIZES: [Tusize; 7] = [
1015        Tusize::Vivification,
1016        Tusize::VivifiedClause,
1017        Tusize::VivifiedVar,
1018        Tusize::NumCycle,
1019        Tusize::NumStage,
1020        Tusize::IntervalScale,
1021        Tusize::IntervalScaleMax,
1022    ];
1023
1024    impl PropertyDereference<Tusize, usize> for State {
1025        #[inline]
1026        fn derefer(&self, k: Tusize) -> usize {
1027            match k {
1028                Tusize::Vivification => self[Stat::Vivification],
1029                Tusize::VivifiedClause => self[Stat::VivifiedClause],
1030                Tusize::VivifiedVar => self[Stat::VivifiedVar],
1031                Tusize::NumCycle => self.stm.current_cycle(),
1032                Tusize::NumStage => self.stm.current_stage(),
1033                Tusize::IntervalScale => self.stm.current_scale(),
1034                Tusize::IntervalScaleMax => self.stm.max_scale(),
1035            }
1036        }
1037    }
1038
1039    #[derive(Clone, Copy, Debug, Eq, PartialEq)]
1040    pub enum TEma {
1041        BackjumpLevel,
1042        ConflictLevel,
1043    }
1044
1045    pub const EMAS: [TEma; 2] = [TEma::BackjumpLevel, TEma::ConflictLevel];
1046
1047    impl PropertyReference<TEma, EmaView> for State {
1048        #[inline]
1049        fn refer(&self, k: TEma) -> &EmaView {
1050            match k {
1051                TEma::BackjumpLevel => self.b_lvl.as_view(),
1052                TEma::ConflictLevel => self.c_lvl.as_view(),
1053            }
1054        }
1055    }
1056}
splr/state.rs

splr/
state.rs
