splr 0.19.0

A modern CDCL SAT solver in Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97

//! Var struct and Database management API
use {
    crate::types::{
        AssignReason, DecisionLevel,
        flags::{FlagIF, FlagVar},
    },
    std::fmt,
};

/// Object representing a variable.
#[derive(Clone, Debug)]
pub struct Var {
    /// assignment
    pub(crate) assign: Option<bool>,
    /// decision level
    pub(crate) level: DecisionLevel,
    /// assign Reason
    pub(crate) reason: AssignReason,
    /// last reason for assignment.
    #[cfg(feature = "trail_saving")]
    pub(crate) reason_saved: AssignReason,
    /// the `Flag`s (8 bits)
    pub(crate) flags: FlagVar,
    /// a dynamic evaluation criterion.
    pub(crate) reward: f64,
    /// the last conflict by this
    pub(crate) last_conflict: usize,
    /// phase bias at the best assignments
    /// -  1.0: `true` always
    /// -  0.0: no bias
    /// - -1.0: `false` always
    pub(crate) polarity: f64,
}

impl Default for Var {
    fn default() -> Var {
        Var {
            assign: None,
            level: 0,
            reason: AssignReason::None,
            #[cfg(feature = "trail_saving")]
            reason_saved: AssignReason::None,
            flags: FlagVar::empty(),
            reward: 0.0,
            last_conflict: 0,
            polarity: 0.0,
        }
    }
}

impl fmt::Display for Var {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        let st = |flag, mes| if self.is(flag) { mes } else { "" };
        write!(f, "V{{{}}}", st(FlagVar::ELIMINATED, ", eliminated"),)
    }
}

impl Var {
    /// return a new vector of $n$ `Var`s.
    pub fn new_vars(n: usize) -> Vec<Var> {
        (0..n as u32 + 1)
            .map(|n| {
                Var {
                    level: n, // each literal occupies a single level.
                    ..Default::default()
                }
            })
            .collect::<Vec<_>>()
    }
    pub fn activity(&self) -> f64 {
        self.reward
    }
}

impl FlagIF for Var {
    type FlagType = FlagVar;
    #[inline]
    fn is(&self, flag: Self::FlagType) -> bool {
        self.flags.contains(flag)
    }
    #[inline]
    fn set(&mut self, f: Self::FlagType, b: bool) {
        self.flags.set(f, b);
    }
    #[inline]
    fn turn_off(&mut self, flag: Self::FlagType) {
        self.flags.remove(flag);
    }
    #[inline]
    fn turn_on(&mut self, flag: Self::FlagType) {
        self.flags.insert(flag);
    }
    #[inline]
    fn toggle(&mut self, flag: Self::FlagType) {
        self.flags.toggle(flag);
    }
}