ccs2/ast/
formula.rs

1use crate::ast::{JoinedBy, Key, Specificity};
2use std::{collections::BTreeSet, fmt::Display, hash::Hash, ops::Add};
3
4/// A conjunction of literal matchers
5#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
6pub struct Clause {
7    literals: BTreeSet<Key>,
8}
9impl Clause {
10    pub fn with_literal(key: Key) -> Self {
11        Self {
12            literals: BTreeSet::from([key]),
13        }
14    }
15
16    pub fn with_literals(keys: impl IntoIterator<Item = Key>) -> Self {
17        Self {
18            literals: BTreeSet::from_iter(keys),
19        }
20    }
21
22    pub fn is_empty(&self) -> bool {
23        self.literals.is_empty()
24    }
25
26    pub fn first(&self) -> Option<Key> {
27        self.literals.iter().next().cloned()
28    }
29
30    pub fn is_subset(&self, other: &Clause) -> bool {
31        self.literals.is_subset(&other.literals)
32    }
33
34    pub fn is_strict_subset(&self, other: &Clause) -> bool {
35        self.is_subset(other) && self.literals.len() < other.literals.len()
36    }
37
38    pub fn elements(&self) -> &BTreeSet<Key> {
39        &self.literals
40    }
41
42    pub fn union(&self, other: &Clause) -> Clause {
43        Clause {
44            literals: self.literals.union(&other.literals).cloned().collect(),
45        }
46    }
47
48    pub fn specificity(&self) -> Specificity {
49        self.literals
50            .iter()
51            .map(|lit| lit.specificity)
52            .reduce(Add::add)
53            .unwrap_or(Specificity::zero())
54    }
55
56    pub fn len(&self) -> usize {
57        self.literals.len()
58    }
59}
60impl PartialOrd for Clause {
61    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
62        Some(self.cmp(other))
63    }
64}
65/// note: we rely on this ordering when building the dag
66impl Ord for Clause {
67    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
68        self.literals
69            .len()
70            .cmp(&other.literals.len())
71            .then_with(|| self.literals.cmp(&other.literals))
72    }
73}
74impl Display for Clause {
75    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
76        let literals: String = self.literals.iter().joined_by(" ");
77        write!(f, "{literals}")
78    }
79}
80impl From<Key> for Clause {
81    fn from(value: Key) -> Self {
82        Self::with_literal(value)
83    }
84}
85
86#[derive(Clone, Debug, Eq)]
87pub struct Formula {
88    clauses: BTreeSet<Clause>,
89    shared: BTreeSet<Clause>,
90}
91impl Default for Formula {
92    fn default() -> Self {
93        Self::with_clause(Clause::default())
94    }
95}
96
97impl Formula {
98    pub fn new(clauses: BTreeSet<Clause>, shared: BTreeSet<Clause>) -> Self {
99        Self { clauses, shared }
100    }
101
102    pub fn with_clause(clause: Clause) -> Self {
103        Self::new(BTreeSet::from([clause]), Default::default())
104    }
105
106    pub fn with_clauses(clauses: impl IntoIterator<Item = Clause>) -> Self {
107        Self::new(BTreeSet::from_iter(clauses), Default::default())
108    }
109
110    pub fn is_empty(&self) -> bool {
111        self.first().is_empty()
112    }
113
114    pub fn first(&self) -> &Clause {
115        self.clauses
116            .first()
117            .expect("Empty formula should be impossible!")
118    }
119
120    pub fn is_subset(&self, other: &Formula) -> bool {
121        self.clauses.is_subset(&other.clauses)
122    }
123
124    pub fn into_inner(self) -> (BTreeSet<Clause>, BTreeSet<Clause>) {
125        (self.clauses, self.shared)
126    }
127
128    pub fn elements(&self) -> &BTreeSet<Clause> {
129        &self.clauses
130    }
131
132    pub fn shared(&self) -> &BTreeSet<Clause> {
133        &self.shared
134    }
135
136    pub fn merge(self, other: Formula) -> Self {
137        let merged = Self::new(
138            self.clauses.into_union(other.clauses),
139            self.shared.into_union(other.shared),
140        );
141        merged.normalize()
142    }
143
144    pub fn len(&self) -> usize {
145        self.clauses.len()
146    }
147
148    ///Normalize a formula.
149    ///
150    /// For any formula, we define a normal form which exists, is unique, and is equivalent
151    /// to the original formula under the usual interpretation of boolean logic.
152    ///
153    /// Clauses are always normal, since all literals are positive. Formulae are normalized
154    /// by removing any clause subsumed by any other. A clause c is subsumed by a clause s
155    /// if s <= c. This is the obvious O(mn) algorithm. Our formulae are usually of size 1,
156    /// so this is just fine.
157    pub fn normalize(self) -> Self {
158        let mut minimized = BTreeSet::<Clause>::default();
159        for c in self.clauses.into_iter() {
160            minimized.retain(|s| !subsumes(&c, s));
161            if !minimized.iter().any(|s| subsumes(s, &c)) {
162                minimized.insert(c);
163            }
164        }
165        // note *strict* subset check here...
166        let shared: BTreeSet<_> = self
167            .shared
168            .into_iter()
169            .filter(|s| minimized.iter().any(|c| s.is_strict_subset(c)))
170            .collect();
171
172        Self {
173            clauses: minimized,
174            shared,
175        }
176    }
177}
178impl Hash for Formula {
179    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
180        self.clauses.hash(state);
181    }
182}
183impl PartialEq for Formula {
184    fn eq(&self, other: &Self) -> bool {
185        self.clauses == other.clauses
186    }
187}
188impl PartialOrd for Formula {
189    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
190        Some(self.cmp(other))
191    }
192}
193/// note: we rely on this ordering when building the dag
194impl Ord for Formula {
195    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
196        self.clauses
197            .len()
198            .cmp(&other.clauses.len())
199            .then_with(|| self.clauses.cmp(&other.clauses))
200    }
201}
202impl Display for Formula {
203    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
204        let clauses: String = self.clauses.iter().joined_by(", ");
205        write!(f, "{clauses}")
206    }
207}
208
209/// A clause c "subsumes" a clause d when d is a subset of c
210/// BUG: The comment seems to describe the opposite of the implementation
211fn subsumes(c: &Clause, d: &Clause) -> bool {
212    c.is_subset(d)
213}
214
215pub trait IntoUnion {
216    fn into_union(self, other: Self) -> Self;
217}
218impl IntoUnion for Clause {
219    fn into_union(self, other: Self) -> Self {
220        Clause {
221            literals: self.literals.into_union(other.literals),
222        }
223    }
224}
225impl<T: Clone + Ord> IntoUnion for BTreeSet<T> {
226    fn into_union(self, other: Self) -> Self {
227        self.union(&other).cloned().collect()
228    }
229}
230
231#[cfg(test)]
232mod tests {
233    use super::*;
234    use crate::ast::macros::*;
235    use pretty_assertions::assert_eq;
236
237    #[test]
238    fn normalize() {
239        let form = Formula::with_clauses([
240            Clause::with_literals([key!("a"), key!("b")]),
241            Clause::with_literals([key!("b")]),
242            Clause::with_literals([key!("a")]),
243            Clause::with_literals([key!("c"), key!("d")]),
244            Clause::with_literals([key!("a"), key!("c"), key!("d")]),
245            Clause::with_literals([key!("c"), key!("d")]),
246        ]);
247        assert_eq!(form.to_string(), "a, b, a b, c d, a c d");
248        assert_eq!(form.normalize().to_string(), "a, b, c d");
249    }
250}
ccs2/ast/formula.rs

ccs2/ast/
formula.rs
