logic_form/
lib.rs

1#![feature(step_trait)]
2
3mod assign;
4mod cnf;
5mod dagcnf;
6pub mod dimacs;
7mod lbool;
8mod litordvec;
9mod litvec;
10mod litvvec;
11mod utils;
12
13pub use assign::*;
14pub use cnf::*;
15pub use dagcnf::*;
16pub use lbool::*;
17pub use litordvec::*;
18pub use litvec::*;
19pub use litvvec::*;
20pub use utils::*;
21
22use std::{
23    fmt::{self, Debug, Display},
24    hash::Hash,
25    iter::Step,
26    ops::{Add, AddAssign, Deref, Not},
27};
28
29#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Default)]
30pub struct Var(pub u32);
31
32impl Var {
33    pub const CONST: Var = Var(0);
34
35    #[inline]
36    pub fn new(x: usize) -> Self {
37        Self(x as _)
38    }
39
40    #[inline]
41    pub fn lit(&self) -> Lit {
42        Lit(self.0 << 1)
43    }
44
45    #[inline]
46    pub fn is_constant(&self) -> bool {
47        *self == Self::CONST
48    }
49}
50
51impl Add<Var> for Var {
52    type Output = Var;
53
54    #[inline]
55    fn add(self, rhs: Var) -> Self::Output {
56        Self(self.0 + rhs.0)
57    }
58}
59
60impl AddAssign<Var> for Var {
61    #[inline]
62    fn add_assign(&mut self, rhs: Var) {
63        self.0 += rhs.0;
64    }
65}
66
67impl From<Lit> for Var {
68    #[inline]
69    fn from(value: Lit) -> Self {
70        value.var()
71    }
72}
73
74impl Deref for Var {
75    type Target = u32;
76
77    #[inline]
78    fn deref(&self) -> &Self::Target {
79        &self.0
80    }
81}
82
83impl Display for Var {
84    #[inline]
85    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
86        write!(f, "{}", self.0)
87    }
88}
89
90impl Step for Var {
91    #[inline]
92    fn steps_between(start: &Self, end: &Self) -> (usize, Option<usize>) {
93        u32::steps_between(&start.0, &end.0)
94    }
95
96    #[inline]
97    fn forward_checked(start: Self, count: usize) -> Option<Self> {
98        u32::forward_checked(start.0, count).map(Self)
99    }
100
101    #[inline]
102    fn backward_checked(start: Self, count: usize) -> Option<Self> {
103        u32::backward_checked(start.0, count).map(Self)
104    }
105}
106
107macro_rules! impl_var_traits {
108    ($T:ty) => {
109        impl PartialEq<$T> for Var {
110            #[inline]
111            fn eq(&self, other: &$T) -> bool {
112                self.0.eq(&(*other as u32))
113            }
114        }
115
116        impl PartialOrd<$T> for Var {
117            #[inline]
118            fn partial_cmp(&self, other: &$T) -> Option<std::cmp::Ordering> {
119                self.0.partial_cmp(&(*other as u32))
120            }
121        }
122
123        impl From<Var> for $T {
124            #[inline]
125            fn from(value: Var) -> Self {
126                value.0 as $T
127            }
128        }
129
130        impl From<$T> for Var {
131            #[inline]
132            fn from(value: $T) -> Self {
133                Self(value as u32)
134            }
135        }
136
137        impl Add<$T> for Var {
138            type Output = Var;
139
140            #[inline]
141            fn add(self, rhs: $T) -> Self::Output {
142                Self(self.0 + rhs as u32)
143            }
144        }
145
146        impl AddAssign<$T> for Var {
147            #[inline]
148            fn add_assign(&mut self, rhs: $T) {
149                self.0 += rhs as u32;
150            }
151        }
152    };
153}
154
155impl_var_traits!(u32);
156impl_var_traits!(i32);
157impl_var_traits!(usize);
158impl_var_traits!(isize);
159
160#[derive(Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Default)]
161pub struct Lit(u32);
162
163impl From<Var> for Lit {
164    #[inline]
165    fn from(value: Var) -> Self {
166        Self(value.0 << 1)
167    }
168}
169
170impl From<Lit> for u32 {
171    #[inline]
172    fn from(val: Lit) -> Self {
173        val.0
174    }
175}
176
177impl From<Lit> for i32 {
178    #[inline]
179    fn from(val: Lit) -> Self {
180        let mut v: i32 = val.var().into();
181        if !val.polarity() {
182            v = -v;
183        }
184        v
185    }
186}
187
188impl From<i32> for Lit {
189    #[inline]
190    fn from(value: i32) -> Self {
191        Self::new(Var(value.unsigned_abs()), value > 0)
192    }
193}
194
195impl Lit {
196    #[inline]
197    pub fn new(var: Var, polarity: bool) -> Self {
198        Lit(var.0 + var.0 + !polarity as u32)
199    }
200
201    #[inline]
202    pub fn var(&self) -> Var {
203        Var(self.0 >> 1)
204    }
205
206    #[inline]
207    pub fn polarity(&self) -> bool {
208        self.0 & 1 == 0
209    }
210
211    #[inline]
212    pub fn constant(polarity: bool) -> Self {
213        Self::new(Var::CONST, !polarity)
214    }
215
216    #[inline]
217    pub fn is_constant(&self, polarity: bool) -> bool {
218        *self == Self::constant(polarity)
219    }
220
221    #[inline]
222    pub fn not_if(&self, c: bool) -> Self {
223        if c { !*self } else { *self }
224    }
225
226    #[inline]
227    pub fn cube(&self) -> LitVec {
228        LitVec::from([*self])
229    }
230
231    #[inline]
232    pub fn map_var(&self, map: impl Fn(Var) -> Var) -> Self {
233        Self::new(map(self.var()), self.polarity())
234    }
235}
236
237impl Not for Lit {
238    type Output = Self;
239
240    #[inline]
241    fn not(mut self) -> Self::Output {
242        self.0 ^= 1;
243        self
244    }
245}
246
247impl Debug for Lit {
248    #[inline]
249    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
250        if self.polarity() {
251            write!(f, "{}", self.var())
252        } else {
253            write!(f, "-{}", self.var())
254        }
255    }
256}
257
258impl Display for Lit {
259    #[inline]
260    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
261        Debug::fmt(&self, f)
262    }
263}
logic_form/lib.rs

logic_form/
lib.rs
