splr/
types.rs

1/// Module `types' provides various building blocks, including
2/// some common traits.
3pub use crate::{
4    assign::AssignReason,
5    cdb::{Clause, ClauseDB, ClauseIF, ClauseId, ClauseIdIF},
6    config::Config,
7    primitive::{ema::*, luby::*},
8    solver::SolverEvent,
9};
10
11use std::{
12    cmp::Ordering,
13    fmt,
14    fs::File,
15    io::{BufRead, BufReader},
16    num::NonZeroU32,
17    ops::{Index, IndexMut, Not},
18    path::Path,
19};
20
21/// API for accessing internal data in a module.
22/// For example, `State::progress` needs to access misc parameters and statistics,
23/// which, however, should be used locally in the defining modules.
24/// To avoid to make them public, we define a generic accessor or exporter here.
25pub trait PropertyReference<I, O> {
26    fn refer(&self, key: I) -> &O;
27}
28
29pub trait PropertyDereference<I, O: Sized> {
30    fn derefer(&self, key: I) -> O;
31}
32
33/// API for Literal like `vi`, `as_bool`, `is_none` and so on.
34pub trait LitIF {
35    /// convert to bool
36    fn as_bool(&self) -> bool;
37    /// convert to var index.
38    fn vi(self) -> VarId;
39}
40
41/// API for reward based activity management.
42pub trait ActivityIF<Ix> {
43    /// return one's activity.
44    fn activity(&self, ix: Ix) -> f64;
45    /// set activity
46    fn set_activity(&mut self, ix: Ix, val: f64);
47    /// modify one's activity at conflict analysis in `conflict_analyze` in [`solver`](`crate::solver`).
48    fn reward_at_analysis(&mut self, _ix: Ix) {
49        #[cfg(debug)]
50        todo!()
51    }
52    /// modify one's activity at value assignment in assign.
53    fn reward_at_assign(&mut self, _ix: Ix) {
54        #[cfg(debug)]
55        todo!()
56    }
57    /// modify one's activity at value assignment in unit propagation.
58    fn reward_at_propagation(&mut self, _ix: Ix) {
59        #[cfg(debug)]
60        todo!()
61    }
62    /// modify one's activity at value un-assignment in [`cancel_until`](`crate::assign::PropagateIF::cancel_until`).
63    fn reward_at_unassign(&mut self, _ix: Ix) {
64        #[cfg(debug)]
65        todo!()
66    }
67    /// update reward decay.
68    fn update_activity_decay(&mut self, _decay: f64);
69    /// update internal counter.
70    fn update_activity_tick(&mut self);
71}
72
73/// API for object instantiation based on `Configuration` and `CNFDescription`.
74/// This is implemented by *all the Splr modules* except `Configuration` and `CNFDescription`.
75///
76/// # Example
77///
78/// ```
79/// use crate::{splr::config::Config, splr::types::*};
80/// use splr::{cdb::ClauseDB, solver::Solver};
81/// let _ = ClauseDB::instantiate(&Config::default(), &CNFDescription::default());
82/// let _ = Solver::instantiate(&Config::default(), &CNFDescription::default());
83///```
84pub trait Instantiate {
85    /// make and return an object from `Config` and `CNFDescription`.
86    fn instantiate(conf: &Config, cnf: &CNFDescription) -> Self;
87    /// update by a solver event.
88    fn handle(&mut self, _e: SolverEvent) {}
89}
90
91/// API for O(n) deletion from a list, providing `delete_unstable`.
92pub trait Delete<T> {
93    /// *O(n)* item deletion protocol.
94    fn delete_unstable<F>(&mut self, filter: F)
95    where
96        F: FnMut(&T) -> bool;
97}
98
99/// 'Variable' identifier or 'variable' index, starting with one.
100/// Implementation note: NonZeroUsize can be used but requires a lot of changes.
101/// The current abstraction is incomplete.
102pub type VarId = usize;
103
104/// Decision Level Representation.
105pub type DecisionLevel = u32;
106
107/// Literal encoded on `u32` as:
108///
109/// - the literal corresponding to a positive occurrence of *variable `n` is `2 * n` and
110/// - that for the negative one is `2 * n + 1`.
111///
112/// # Examples
113///
114/// ```
115/// use splr::types::*;
116/// assert_eq!(2usize, Lit::from(-1i32).into());
117/// assert_eq!(3usize, Lit::from( 1i32).into());
118/// assert_eq!(4usize, Lit::from(-2i32).into());
119/// assert_eq!(5usize, Lit::from( 2i32).into());
120/// assert_eq!( 1i32, Lit::from( 1i32).into());
121/// assert_eq!(-1i32, Lit::from(-1i32).into());
122/// assert_eq!( 2i32, Lit::from( 2i32).into());
123/// assert_eq!(-2i32, Lit::from(-2i32).into());
124/// ```
125#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
126pub struct Lit {
127    /// literal encoded into folded u32
128    ordinal: NonZeroU32,
129}
130
131impl fmt::Display for Lit {
132    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
133        write!(f, "{}L", i32::from(self))
134    }
135}
136
137impl fmt::Debug for Lit {
138    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
139        write!(f, "{}L", i32::from(self))
140    }
141}
142
143/// convert literals to `[i32]` (for debug).
144pub fn i32s(v: &[Lit]) -> Vec<i32> {
145    v.iter().map(|l| i32::from(*l)).collect::<Vec<_>>()
146}
147
148impl From<(VarId, bool)> for Lit {
149    #[inline]
150    fn from((vi, b): (VarId, bool)) -> Self {
151        Lit {
152            ordinal: unsafe { NonZeroU32::new_unchecked(((vi as u32) << 1) + (b as u32)) },
153        }
154    }
155}
156
157impl From<usize> for Lit {
158    #[inline]
159    fn from(l: usize) -> Self {
160        Lit {
161            ordinal: unsafe { NonZeroU32::new_unchecked(l as u32) },
162        }
163    }
164}
165
166impl From<u32> for Lit {
167    #[inline]
168    fn from(l: u32) -> Self {
169        Lit {
170            ordinal: unsafe { NonZeroU32::new_unchecked(l) },
171        }
172    }
173}
174
175impl From<i32> for Lit {
176    #[inline]
177    fn from(x: i32) -> Self {
178        Lit {
179            ordinal: unsafe {
180                NonZeroU32::new_unchecked((if x < 0 { -2 * x } else { 2 * x + 1 }) as u32)
181            },
182        }
183    }
184}
185
186impl From<ClauseId> for Lit {
187    #[inline]
188    fn from(cid: ClauseId) -> Self {
189        Lit {
190            ordinal: unsafe {
191                NonZeroU32::new_unchecked(NonZeroU32::get(cid.ordinal) & 0x7FFF_FFFF)
192            },
193        }
194    }
195}
196
197impl From<Lit> for bool {
198    /// - positive Lit (= even u32) => Some(true)
199    /// - negative Lit (= odd u32)  => Some(false)
200    #[inline]
201    fn from(l: Lit) -> bool {
202        (NonZeroU32::get(l.ordinal) & 1) != 0
203    }
204}
205
206impl From<Lit> for ClauseId {
207    #[inline]
208    fn from(l: Lit) -> ClauseId {
209        ClauseId {
210            ordinal: unsafe { NonZeroU32::new_unchecked(NonZeroU32::get(l.ordinal) | 0x8000_0000) },
211        }
212    }
213}
214
215impl From<Lit> for usize {
216    #[inline]
217    fn from(l: Lit) -> usize {
218        NonZeroU32::get(l.ordinal) as usize
219    }
220}
221
222impl From<Lit> for i32 {
223    #[inline]
224    fn from(l: Lit) -> i32 {
225        if NonZeroU32::get(l.ordinal) % 2 == 0 {
226            -((NonZeroU32::get(l.ordinal) >> 1) as i32)
227        } else {
228            (NonZeroU32::get(l.ordinal) >> 1) as i32
229        }
230    }
231}
232
233impl From<&Lit> for i32 {
234    #[inline]
235    fn from(l: &Lit) -> i32 {
236        if NonZeroU32::get(l.ordinal) % 2 == 0 {
237            -((NonZeroU32::get(l.ordinal) >> 1) as i32)
238        } else {
239            (NonZeroU32::get(l.ordinal) >> 1) as i32
240        }
241    }
242}
243
244impl Not for Lit {
245    type Output = Lit;
246    #[inline]
247    fn not(self) -> Self {
248        Lit {
249            ordinal: unsafe { NonZeroU32::new_unchecked(NonZeroU32::get(self.ordinal) ^ 1) },
250        }
251    }
252}
253
254impl Index<Lit> for [bool] {
255    type Output = bool;
256    #[inline]
257    fn index(&self, l: Lit) -> &Self::Output {
258        #[cfg(feature = "unsafe_access")]
259        unsafe {
260            self.get_unchecked(usize::from(l))
261        }
262        #[cfg(not(feature = "unsafe_access"))]
263        &self[usize::from(l)]
264    }
265}
266
267impl IndexMut<Lit> for [bool] {
268    #[inline]
269    fn index_mut(&mut self, l: Lit) -> &mut Self::Output {
270        #[cfg(feature = "unsafe_access")]
271        unsafe {
272            self.get_unchecked_mut(usize::from(l))
273        }
274        #[cfg(not(feature = "unsafe_access"))]
275        &mut self[usize::from(l)]
276    }
277}
278
279impl Index<Lit> for Vec<bool> {
280    type Output = bool;
281    #[inline]
282    fn index(&self, l: Lit) -> &Self::Output {
283        #[cfg(feature = "unsafe_access")]
284        unsafe {
285            self.get_unchecked(usize::from(l))
286        }
287        #[cfg(not(feature = "unsafe_access"))]
288        &self[usize::from(l)]
289    }
290}
291
292impl IndexMut<Lit> for Vec<bool> {
293    #[inline]
294    fn index_mut(&mut self, l: Lit) -> &mut Self::Output {
295        #[cfg(feature = "unsafe_access")]
296        unsafe {
297            self.get_unchecked_mut(usize::from(l))
298        }
299        #[cfg(not(feature = "unsafe_access"))]
300        &mut self[usize::from(l)]
301    }
302}
303
304/// # Examples
305///
306/// ```
307/// use splr::types::*;
308/// assert_eq!(Lit::from(1i32), Lit::from((1 as VarId, true)));
309/// assert_eq!(Lit::from(2i32), Lit::from((2 as VarId, true)));
310/// assert_eq!(1, Lit::from((1usize, true)).vi());
311/// assert_eq!(1, Lit::from((1usize, false)).vi());
312/// assert_eq!(2, Lit::from((2usize, true)).vi());
313/// assert_eq!(2, Lit::from((2usize, false)).vi());
314/// assert_eq!(Lit::from( 1i32), !Lit::from(-1i32));
315/// assert_eq!(Lit::from(-1i32), !Lit::from( 1i32));
316/// assert_eq!(Lit::from( 2i32), !Lit::from(-2i32));
317/// assert_eq!(Lit::from(-2i32), !Lit::from( 2i32));
318/// ```
319impl LitIF for Lit {
320    #[inline]
321    fn as_bool(&self) -> bool {
322        NonZeroU32::get(self.ordinal) & 1 == 1
323    }
324    #[inline]
325    fn vi(self) -> VarId {
326        (NonZeroU32::get(self.ordinal) >> 1) as VarId
327    }
328}
329
330/// Capture a conflict
331pub type ConflictContext = (Lit, AssignReason);
332
333/// Return type of unit propagation
334pub type PropagationResult = Result<(), ConflictContext>;
335
336// A generic reference to a clause or something else.
337// we can use DEAD for simply satisfied form, f.e. an empty forms,
338// while EmptyClause can be used for simply UNSAT form.
339#[derive(Clone, Debug, Eq, PartialEq)]
340pub enum RefClause {
341    Clause(ClauseId),
342    Dead,
343    EmptyClause,
344    RegisteredClause(ClauseId),
345    UnitClause(Lit),
346}
347
348impl RefClause {
349    pub fn as_cid(&self) -> ClauseId {
350        match self {
351            RefClause::Clause(cid) => *cid,
352            RefClause::RegisteredClause(cid) => *cid,
353            _ => panic!("invalid reference to clause"),
354        }
355    }
356    pub fn is_new(&self) -> Option<ClauseId> {
357        match self {
358            RefClause::Clause(cid) => Some(*cid),
359            RefClause::RegisteredClause(_) => None,
360            RefClause::EmptyClause => None,
361            RefClause::Dead => None,
362            RefClause::UnitClause(_) => None,
363        }
364    }
365}
366
367/// Internal errors.
368/// Note: returning `Result<(), a-singleton>` is identical to returning `bool`.
369#[derive(Debug, Eq, PartialEq)]
370pub enum SolverError {
371    // StateUNSAT = 0,
372    // StateSAT,
373    // A given CNF contains empty clauses or derives them during reading
374    EmptyClause,
375    // A clause contains a literal out of the range defined in its header.
376    // '0' is an example.
377    InvalidLiteral,
378    // Exceptions caused by file operations
379    IOError,
380    // UNSAT with some internal context
381    Inconsistent,
382    OutOfMemory,
383    // UNSAT with some internal context
384    RootLevelConflict(ConflictContext),
385    TimeOut,
386    SolverBug,
387    // For now, this is used for catching errors relating to clock
388    UndescribedError,
389}
390
391impl fmt::Display for SolverError {
392    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
393        write!(f, "{self:?}")
394    }
395}
396
397/// A Return type used by solver functions.
398pub type MaybeInconsistent = Result<(), SolverError>;
399
400/// CNF locator
401#[derive(Clone, Debug, Default)]
402pub enum CNFIndicator {
403    /// not specified
404    #[default]
405    Void,
406    /// from a file
407    File(String),
408    /// embedded directly
409    LitVec(usize),
410}
411
412impl fmt::Display for CNFIndicator {
413    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
414        match self {
415            CNFIndicator::Void => write!(f, "No CNF specified)"),
416            CNFIndicator::File(file) => write!(f, "CNF file({file})"),
417            CNFIndicator::LitVec(n) => write!(f, "A vec({n} clauses)"),
418        }
419    }
420}
421
422// impl CNFIndicator {
423//     pub fn to_string(&self) -> String {
424//         match self {
425//             CNFIndicator::Void => "(no cnf)".to_string(),
426//             CNFIndicator::File(f) => f.to_string(),
427//             CNFIndicator::LitVec(v) => format!("(embedded {} element vector)", v.len()).to_string(),
428//         }
429//     }
430// }
431
432/// Data storage about a problem.
433#[derive(Clone, Debug)]
434pub struct CNFDescription {
435    pub num_of_variables: usize,
436    pub num_of_clauses: usize,
437    pub pathname: CNFIndicator,
438}
439
440impl Default for CNFDescription {
441    fn default() -> CNFDescription {
442        CNFDescription {
443            num_of_variables: 0,
444            num_of_clauses: 0,
445            pathname: CNFIndicator::Void,
446        }
447    }
448}
449
450impl fmt::Display for CNFDescription {
451    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
452        let CNFDescription {
453            num_of_variables: nv,
454            num_of_clauses: nc,
455            pathname: path,
456        } = &self;
457        write!(f, "CNF({nv}, {nc}, {path})")
458    }
459}
460
461impl<V: AsRef<[i32]>> From<&[V]> for CNFDescription {
462    fn from(vec: &[V]) -> Self {
463        let num_of_variables = vec
464            .iter()
465            .map(|clause| clause.as_ref().iter().map(|l| l.abs()).max().unwrap_or(0))
466            .max()
467            .unwrap_or(0) as usize;
468        CNFDescription {
469            num_of_variables,
470            num_of_clauses: vec.len(),
471            pathname: CNFIndicator::LitVec(vec.len()),
472        }
473    }
474}
475
476/// A wrapper structure to make a CNFDescription from a file.
477/// To make CNFDescription clone-able, a BufReader should be separated from it.
478/// If you want to make a CNFDescription which isn't connected to a file,
479/// just call CNFDescription::default() directly.
480#[derive(Debug)]
481pub struct CNFReader {
482    pub cnf: CNFDescription,
483    pub reader: BufReader<File>,
484}
485
486impl TryFrom<&Path> for CNFReader {
487    type Error = SolverError;
488    fn try_from(path: &Path) -> Result<Self, Self::Error> {
489        let pathname = if path.to_string_lossy().is_empty() {
490            "--".to_string()
491        } else {
492            Path::new(&path.to_string_lossy().into_owned())
493                .file_name()
494                .map_or("aStrangeNamed".to_string(), |f| {
495                    f.to_string_lossy().into_owned()
496                })
497        };
498        let fs = File::open(path).map_or(Err(SolverError::IOError), Ok)?;
499        let mut reader = BufReader::new(fs);
500        let mut buf = String::new();
501        let mut nv: usize = 0;
502        let mut nc: usize = 0;
503        let mut found_valid_header = false;
504        loop {
505            buf.clear();
506            match reader.read_line(&mut buf) {
507                Ok(0) => break,
508                Ok(_k) => {
509                    let mut iter = buf.split_whitespace();
510                    if iter.next() == Some("p") && iter.next() == Some("cnf") {
511                        if let Some(v) = iter.next().map(|s| s.parse::<usize>().ok().unwrap()) {
512                            if let Some(c) = iter.next().map(|s| s.parse::<usize>().ok().unwrap()) {
513                                nv = v;
514                                nc = c;
515                                found_valid_header = true;
516                                break;
517                            }
518                        }
519                    }
520                    continue;
521                }
522                Err(e) => {
523                    println!("{e}");
524                    return Err(SolverError::IOError);
525                }
526            }
527        }
528        if !found_valid_header {
529            return Err(SolverError::IOError);
530        }
531        let cnf = CNFDescription {
532            num_of_variables: nv,
533            num_of_clauses: nc,
534            pathname: CNFIndicator::File(pathname),
535        };
536        Ok(CNFReader { cnf, reader })
537    }
538}
539
540impl<T> Delete<T> for Vec<T> {
541    fn delete_unstable<F>(&mut self, filter: F)
542    where
543        F: FnMut(&T) -> bool,
544    {
545        if let Some(i) = self.iter().position(filter) {
546            self.swap_remove(i);
547        }
548    }
549}
550
551/// API for object properties.
552pub trait FlagIF {
553    type FlagType;
554    /// return true if the flag in on.
555    fn is(&self, flag: Self::FlagType) -> bool;
556    /// set the flag.
557    fn set(&mut self, f: Self::FlagType, b: bool);
558    // toggle the flag.
559    fn toggle(&mut self, flag: Self::FlagType);
560    /// toggle the flag off.
561    fn turn_off(&mut self, flag: Self::FlagType);
562    /// toggle the flag on.
563    fn turn_on(&mut self, flag: Self::FlagType);
564}
565
566bitflags! {
567    /// Misc flags used by [`Clause`](`crate::cdb::Clause`).
568    #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
569    pub struct FlagClause: u8 {
570        /// a clause is a generated clause by conflict analysis and is removable.
571        const LEARNT       = 0b0000_0001;
572        /// used in conflict analyze
573        const USED         = 0b0000_0010;
574        /// a clause or var is enqueued for eliminator.
575        const ENQUEUED     = 0b0000_0100;
576        /// a clause is registered in vars' occurrence list.
577        const OCCUR_LINKED = 0b0000_1000;
578        /// a given clause derived a learnt which LBD is smaller than 20.
579        const DERIVE20     = 0b0001_0000;
580    }
581}
582
583bitflags! {
584    /// Misc flags used by [`Var`](`crate::assign::Var`).
585    #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
586    pub struct FlagVar: u8 {
587        /// * the previous assigned value of a Var.
588        const PHASE        = 0b0000_0001;
589        /// used in conflict analyze
590        const USED         = 0b0000_0010;
591        /// a var is eliminated and managed by eliminator.
592        const ELIMINATED   = 0b0000_0100;
593        /// a clause or var is enqueued for eliminator.
594        const ENQUEUED     = 0b0000_1000;
595        /// a var is checked during in the current conflict analysis.
596        const CA_SEEN      = 0b0001_0000;
597
598        #[cfg(feature = "debug_propagation")]
599        /// check propagation
600        const PROPAGATED   = 0b0010_0000;
601    }
602}
603
604#[derive(Debug, Default)]
605pub struct Logger {
606    dest: Option<File>,
607}
608
609impl fmt::Display for Logger {
610    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
611        write!(f, "Dump({:?})", self.dest)
612    }
613}
614
615impl Logger {
616    pub fn new<T: AsRef<str>>(fname: T) -> Self {
617        Logger {
618            dest: File::create(fname.as_ref()).ok(),
619        }
620    }
621    pub fn dump(&mut self, mes: String) {
622        use std::io::Write;
623        if let Some(f) = &mut self.dest {
624            f.write_all(&mes.into_bytes())
625                .unwrap_or_else(|_| panic!("fail to dump {f:?}"));
626        } else {
627            println!("{mes}");
628        }
629    }
630}
631
632#[derive(Clone, Debug)]
633pub struct OrderedProxy<T: Clone + Default + Sized + Ord> {
634    index: f64,
635    body: T,
636}
637
638impl<T: Clone + Default + Sized + Ord> Default for OrderedProxy<T> {
639    fn default() -> Self {
640        OrderedProxy {
641            index: 0.0,
642            body: T::default(),
643        }
644    }
645}
646
647impl<T: Clone + Default + Sized + Ord> PartialEq for OrderedProxy<T> {
648    fn eq(&self, other: &OrderedProxy<T>) -> bool {
649        self.index == other.index && self.body == other.body
650    }
651}
652
653impl<T: Clone + Default + Sized + Ord> Eq for OrderedProxy<T> {}
654
655impl<T: Clone + Default + PartialEq + Ord> PartialOrd for OrderedProxy<T> {
656    fn partial_cmp(&self, other: &OrderedProxy<T>) -> Option<Ordering> {
657        Some(self.cmp(other))
658    }
659}
660
661impl<T: Clone + Default + PartialEq + Ord> Ord for OrderedProxy<T> {
662    fn cmp(&self, other: &OrderedProxy<T>) -> Ordering {
663        if (self.index - other.index).abs() < f64::EPSILON {
664            self.body.cmp(&other.body)
665        } else if self.index < other.index {
666            Ordering::Less
667        } else {
668            Ordering::Greater
669        }
670    }
671}
672
673impl<T: Clone + Default + Sized + Ord> OrderedProxy<T> {
674    pub fn new(body: T, index: f64) -> Self {
675        OrderedProxy { index, body }
676    }
677    pub fn new_invert(body: T, rindex: f64) -> Self {
678        OrderedProxy {
679            index: -rindex,
680            body,
681        }
682    }
683    pub fn to(&self) -> T {
684        self.body.clone()
685    }
686    pub fn value(&self) -> f64 {
687        self.index
688    }
689}
690
691#[cfg(feature = "boundary_check")]
692#[derive(Clone, Debug, PartialEq, PartialOrd)]
693pub enum Propagate {
694    None,
695    CacheSatisfied(usize),
696    FindNewWatch(usize, Lit, Lit),
697    BecameUnit(usize, Lit),
698    EmitConflict(usize, Lit),
699    SandboxCacheSatisfied(usize),
700    SandboxFindNewWatch(usize, Lit, Lit),
701    SandboxBecameUnit(usize),
702    SandboxEmitConflict(usize, Lit),
703}
704
705#[cfg(feature = "boundary_check")]
706#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
707pub enum VarState {
708    AssertedSandbox(usize),
709    Assigned(usize),
710    AssignedSandbox(usize),
711    Propagated(usize),
712    Unassigned(usize),
713}
714
715#[cfg(test)]
716mod tests {
717    use super::*;
718    use std::path::Path;
719
720    #[test]
721    fn test_cnf() {
722        if let Ok(reader) = CNFReader::try_from(Path::new("cnfs/sample.cnf")) {
723            assert_eq!(reader.cnf.num_of_variables, 250);
724            assert_eq!(reader.cnf.num_of_clauses, 1065);
725        } else {
726            panic!("failed to load cnfs/sample.cnf");
727        }
728    }
729}
splr/types.rs

splr/
types.rs
