logic_form/
cnf.rs

1use crate::{DagCnf, Lit, LitVec, Var};
2use giputils::hash::{GHashMap, GHashSet};
3use std::{
4    iter::once,
5    ops::{Deref, DerefMut},
6};
7
8#[derive(Debug, Clone)]
9pub struct Cnf {
10    max_var: Var,
11    cls: Vec<LitVec>,
12}
13
14impl Cnf {
15    pub fn new() -> Self {
16        Self::default()
17    }
18
19    #[inline]
20    pub fn max_var(&self) -> Var {
21        self.max_var
22    }
23
24    #[inline]
25    pub fn new_var(&mut self) -> Var {
26        self.max_var += 1;
27        self.max_var
28    }
29
30    #[inline]
31    pub fn new_var_to(&mut self, n: Var) {
32        self.max_var = self.max_var.max(n);
33    }
34
35    #[inline]
36    pub fn add_clause(&mut self, cls: &[Lit]) {
37        if let Some(m) = cls.iter().map(|l| l.var()).max() {
38            self.max_var = self.max_var.max(m);
39        }
40        self.cls.push(LitVec::from(cls));
41    }
42
43    #[inline]
44    pub fn add_clauses(&mut self, cls: impl Iterator<Item = LitVec>) {
45        for cls in cls {
46            self.add_clause(&cls);
47        }
48    }
49
50    #[inline]
51    pub fn clauses(&self) -> &[LitVec] {
52        &self.cls
53    }
54
55    pub fn rearrange(&mut self, additional: impl Iterator<Item = Var>) -> GHashMap<Var, Var> {
56        let mut domain = GHashSet::from_iter(additional.chain(once(Var::CONST)));
57        for cls in self.cls.iter() {
58            for l in cls.iter() {
59                domain.insert(l.var());
60            }
61        }
62        let mut domain = Vec::from_iter(domain);
63        domain.sort();
64        let mut domain_map = GHashMap::new();
65        for (i, d) in domain.iter().enumerate() {
66            domain_map.insert(*d, Var::new(i));
67        }
68        let map_lit = |l: &Lit| l.map_var(|v| domain_map[&v]);
69        for cls in self.cls.iter_mut() {
70            for l in cls.iter_mut() {
71                *l = map_lit(l);
72            }
73        }
74        self.max_var = Var::new(domain.len() - 1);
75        domain_map
76    }
77
78    pub fn set_cls(&mut self, cls: Vec<LitVec>) {
79        self.cls = cls;
80    }
81}
82
83impl Deref for Cnf {
84    type Target = [LitVec];
85
86    #[inline]
87    fn deref(&self) -> &Self::Target {
88        &self.cls
89    }
90}
91
92impl DerefMut for Cnf {
93    #[inline]
94    fn deref_mut(&mut self) -> &mut Self::Target {
95        &mut self.cls
96    }
97}
98
99impl Default for Cnf {
100    fn default() -> Self {
101        Self {
102            max_var: Var(0),
103            cls: vec![LitVec::from([Lit::constant(true)])],
104        }
105    }
106}
107
108impl DagCnf {
109    #[inline]
110    pub fn lower(&self) -> Cnf {
111        Cnf {
112            max_var: self.max_var(),
113            cls: self.clause().cloned().collect(),
114        }
115    }
116}
logic_form/cnf.rs

logic_form/
cnf.rs
