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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147

//! Decision var selection

use {
    super::{heap::VarHeapIF, stack::AssignStack},
    crate::types::*,
};

#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
pub enum RephaseTarget {
    #[default]
    Walk,
    Best,
    False,
    True,
    Random,
    Inverted,
    Polarity,
}

impl RephaseTarget {
    /// return a symbolic (Unicode) letter for each value of `PhaseRotation`.
    pub fn as_mnemonic(&self) -> &str {
        match self {
            RephaseTarget::Walk => "→",
            RephaseTarget::Best => "★",
            RephaseTarget::False => "⊥",
            RephaseTarget::True => "⊤",
            RephaseTarget::Random => "∼",
            RephaseTarget::Inverted => "¬",
            RephaseTarget::Polarity => "φ",
        }
    }
}

/// ```ignore
/// let x: Option<bool> = var_assign!(self, lit.vi());
/// ```
#[cfg(feature = "unsafe_access")]
macro_rules! var_assign {
    ($asg: expr, $var: expr) => {
        unsafe { $asg.var.get_unchecked($var).assign }
    };
}
#[cfg(not(feature = "unsafe_access"))]
macro_rules! var_assign {
    ($asg: expr, $var: expr) => {
        $asg.var[$var].assign
    };
}

/// API for var selection, depending on an internal heap.
pub trait VarSelectIF {
    /// return `None` if current assignment is not compatible with the values.
    /// Othewise return `Some(the core size)`.
    fn check_best_phases(&mut self) -> Option<usize>;
    /// select a new decision variable.
    fn select_decision_literal(&mut self) -> Lit;
    /// update the internal heap on var order.
    fn update_order(&mut self, v: VarId);
    /// rebuild the internal var_order
    fn rebuild_order(&mut self);
    /// save the current assignments as the best phases.
    /// return the core size.
    fn save_best_phases(&mut self, new_best: bool) -> usize;
    fn clear_best_phases(&mut self);
}

impl VarSelectIF for AssignStack {
    fn check_best_phases(&mut self) -> Option<usize> {
        let mut alives = 0;
        let mut inconsistent: bool = false;
        for (vi, b) in self.best_phases.iter_mut().enumerate().skip(1) {
            match (b.0, self.var[vi].assign) {
                (Some(_), None) if !self.var[vi].is(FlagVar::ELIMINATED) => {
                    alives += 1;
                }
                (Some(bp), Some(a)) if bp == a => {
                    *b = (None, DecisionLevel::MAX);
                }
                (Some(_), Some(_)) => {
                    inconsistent = true;
                    break;
                }
                _ => (),
            }
        }
        if inconsistent {
            self.best_phases.fill((None, DecisionLevel::default()));
            None
        } else {
            Some(self.num_vars - alives - self.num_asserted_vars - self.num_eliminated_vars)
        }
    }
    fn select_decision_literal(&mut self) -> Lit {
        let vi = self.select_var();
        Lit::from((vi, self.var[vi].is(FlagVar::PHASE)))
    }
    fn update_order(&mut self, v: VarId) {
        self.update_heap(v);
    }
    fn rebuild_order(&mut self) {
        self.clear_heap();
        for vi in 1..self.var.len() {
            if var_assign!(self, vi).is_none() && !self.var[vi].is(FlagVar::ELIMINATED) {
                self.insert_heap(vi);
            }
        }
    }
    fn save_best_phases(&mut self, new_best: bool) -> usize {
        let mut alives: usize = 0;
        for (vi, v) in self.var.iter_mut().enumerate().skip(1) {
            if let Some(b) = v.assign
                && v.level > self.root_level
                && !v.is(FlagVar::ELIMINATED)
            {
                if new_best {
                    self.best_phases[vi] = (Some(b), v.level);
                }
                alives += 1;
            } else {
                if new_best {
                    self.best_phases[vi] = (None, DecisionLevel::MAX);
                }
            }
        }
        self.num_vars - alives - self.num_asserted_vars - self.num_eliminated_vars
    }
    fn clear_best_phases(&mut self) {
        for (vi, v) in self.var.iter_mut().enumerate().skip(1) {
            if v.level > self.root_level && !v.is(FlagVar::ELIMINATED) {
                self.best_phases[vi] = (None, DecisionLevel::MAX);
            }
        }
    }
}

impl AssignStack {
    /// select a decision var
    fn select_var(&mut self) -> VarId {
        loop {
            let vi = self.get_heap_root();
            if var_assign!(self, vi).is_none() && !self.var[vi].is(FlagVar::ELIMINATED) {
                return vi;
            }
        }
    }
}