oxiz_sat/
literal.rs

1//! Literals and Variables
2
3#[allow(unused_imports)]
4use crate::prelude::*;
5use core::ops::Not;
6
7/// A variable in the SAT formula
8#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
9pub struct Var(pub u32);
10
11impl Var {
12    /// Create a new variable from a raw index
13    #[must_use]
14    pub const fn new(idx: u32) -> Self {
15        Self(idx)
16    }
17
18    /// Get the raw index
19    #[must_use]
20    pub const fn index(self) -> usize {
21        self.0 as usize
22    }
23}
24
25/// A literal (positive or negative occurrence of a variable)
26#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
27pub struct Lit(u32);
28
29impl Lit {
30    /// Create a positive literal from a variable
31    #[must_use]
32    pub const fn pos(var: Var) -> Self {
33        Self(var.0 << 1)
34    }
35
36    /// Create a negative literal from a variable
37    #[must_use]
38    pub const fn neg(var: Var) -> Self {
39        Self((var.0 << 1) | 1)
40    }
41
42    /// Create a literal from a signed integer (DIMACS format)
43    /// Positive int -> positive literal, negative int -> negative literal
44    #[must_use]
45    pub fn from_dimacs(lit: i32) -> Self {
46        debug_assert!(lit != 0);
47        let var = Var::new(lit.unsigned_abs() - 1);
48        if lit > 0 {
49            Self::pos(var)
50        } else {
51            Self::neg(var)
52        }
53    }
54
55    /// Convert to DIMACS format
56    #[must_use]
57    pub fn to_dimacs(self) -> i32 {
58        let var = (self.var().0 + 1) as i32;
59        if self.is_pos() { var } else { -var }
60    }
61
62    /// Get the variable of this literal
63    #[must_use]
64    pub const fn var(self) -> Var {
65        Var(self.0 >> 1)
66    }
67
68    /// Check if this is a positive literal
69    #[must_use]
70    pub const fn is_pos(self) -> bool {
71        (self.0 & 1) == 0
72    }
73
74    /// Check if this is a negative literal
75    #[must_use]
76    pub const fn is_neg(self) -> bool {
77        (self.0 & 1) == 1
78    }
79
80    /// Get the negation of this literal
81    #[must_use]
82    pub const fn negate(self) -> Self {
83        Self(self.0 ^ 1)
84    }
85
86    /// Get the sign (true for positive, false for negative)
87    #[must_use]
88    pub const fn sign(self) -> bool {
89        self.is_pos()
90    }
91
92    /// Get the raw encoding
93    #[must_use]
94    pub const fn code(self) -> u32 {
95        self.0
96    }
97
98    /// Create from raw encoding
99    #[must_use]
100    pub const fn from_code(code: u32) -> Self {
101        Self(code)
102    }
103
104    /// Get the index for array access (2 * var + sign)
105    #[must_use]
106    pub const fn index(self) -> usize {
107        self.0 as usize
108    }
109}
110
111impl Not for Lit {
112    type Output = Self;
113
114    fn not(self) -> Self::Output {
115        self.negate()
116    }
117}
118
119/// Boolean value or undefined
120#[derive(Debug, Clone, Copy, PartialEq, Eq)]
121pub enum LBool {
122    /// True
123    True,
124    /// False
125    False,
126    /// Undefined
127    Undef,
128}
129
130impl LBool {
131    /// Create from a boolean
132    #[must_use]
133    pub const fn from_bool(b: bool) -> Self {
134        if b { Self::True } else { Self::False }
135    }
136
137    /// Check if defined
138    #[must_use]
139    pub const fn is_defined(self) -> bool {
140        !matches!(self, Self::Undef)
141    }
142
143    /// Check if true
144    #[must_use]
145    pub const fn is_true(self) -> bool {
146        matches!(self, Self::True)
147    }
148
149    /// Check if false
150    #[must_use]
151    pub const fn is_false(self) -> bool {
152        matches!(self, Self::False)
153    }
154
155    /// Negate
156    #[must_use]
157    pub const fn negate(self) -> Self {
158        match self {
159            Self::True => Self::False,
160            Self::False => Self::True,
161            Self::Undef => Self::Undef,
162        }
163    }
164}
165
166impl From<bool> for LBool {
167    fn from(b: bool) -> Self {
168        Self::from_bool(b)
169    }
170}
171
172#[cfg(test)]
173mod tests {
174    use super::*;
175
176    #[test]
177    fn test_literal_creation() {
178        let var = Var::new(0);
179        let pos = Lit::pos(var);
180        let neg = Lit::neg(var);
181
182        assert!(pos.is_pos());
183        assert!(neg.is_neg());
184        assert_eq!(pos.var(), var);
185        assert_eq!(neg.var(), var);
186        assert_eq!(pos.negate(), neg);
187        assert_eq!(neg.negate(), pos);
188    }
189
190    #[test]
191    fn test_dimacs_conversion() {
192        let lit = Lit::from_dimacs(1);
193        assert!(lit.is_pos());
194        assert_eq!(lit.var(), Var::new(0));
195        assert_eq!(lit.to_dimacs(), 1);
196
197        let lit = Lit::from_dimacs(-2);
198        assert!(lit.is_neg());
199        assert_eq!(lit.var(), Var::new(1));
200        assert_eq!(lit.to_dimacs(), -2);
201    }
202
203    #[test]
204    fn test_lbool() {
205        assert!(LBool::True.is_true());
206        assert!(LBool::False.is_false());
207        assert!(!LBool::Undef.is_defined());
208
209        assert_eq!(LBool::True.negate(), LBool::False);
210        assert_eq!(LBool::False.negate(), LBool::True);
211        assert_eq!(LBool::Undef.negate(), LBool::Undef);
212    }
213}
oxiz_sat/literal.rs

oxiz_sat/
literal.rs
