Generalize literals in epression and add helper function for expressions

src/expr.rs

@@ -1,3 +1,5 @@
+use std::hash::Hash;
+
 use crate::{
     dpll::Index,
     mapping::Mapping,
@@ -5,12 +7,26 @@ use crate::{
 };
 use miette::{miette, Context, Result};
 
+pub mod helper;
+
 #[derive(Debug, Clone)]
-pub enum Expr<'s> {
+pub enum Expr<L>
-    Literal(&'s str),
+where
-    Not(Box<Expr<'s>>),
+    L: Clone,
-    And(Vec<Expr<'s>>),
+{
-    Or(Vec<Expr<'s>>),
+    Literal(L),
+    Not(Box<Expr<L>>),
+    And(Vec<Expr<L>>),
+    Or(Vec<Expr<L>>),
+}
+
+impl<L> Expr<L>
+where
+    L: Clone,
+{
+    pub fn not(e: Expr<L>) -> Expr<L> {
+        Expr::Not(Box::new(e))
+    }
 }
 
 #[derive(Debug)]
@@ -91,8 +107,8 @@ impl<'s> Iterator for Tokanizer<'s> {
     }
 }
 
-impl<'s> Expr<'s> {
+impl<'s> Expr<&'s str> {
-    fn parse_expr(tokanizer: &mut Tokanizer<'s>) -> Result<Expr<'s>> {
+    fn parse_expr(tokanizer: &mut Tokanizer<'s>) -> Result<Expr<&'s str>> {
         if let Some(token) = tokanizer.next().transpose()? {
             match token {
                 Token::Literal(l) => Ok(Expr::Literal(l)),
@@ -173,7 +189,12 @@ impl<'s> Expr<'s> {
             Ok(Expr::And(v))
         }
     }
+}
 
+impl<L> Expr<L>
+where
+    L: Clone,
+{
     pub fn disjunctive_normal_form(self) -> Self {
         // dbg!(&self);
         match self {
@@ -245,8 +266,13 @@ impl<'s> Expr<'s> {
             ),
         }
     }
+}
 
-    pub fn disjunctive_normal_form2(self, mapping: &mut Mapping<'s>) -> NormalForm {
+impl<L> Expr<L>
+where
+    L: Clone + Eq + Hash,
+{
+    pub fn disjunctive_normal_form2(self, mapping: &mut Mapping<L>) -> NormalForm {
         match self {
             Expr::Literal(l) => {
                 let mut n = NormalForm::new();
@@ -371,7 +397,7 @@ impl<'s> Expr<'s> {
         }
     }
 
-    pub fn cnf_normal_form(self) -> (NormalForm, Mapping<'s>) {
+    pub fn cnf_normal_form(self) -> (NormalForm, Mapping<L>) {
         let mut mapping = Mapping::new();
 
         let mut cnf = Expr::Not(Box::new(self)).disjunctive_normal_form2(&mut mapping);
@@ -381,7 +407,7 @@ impl<'s> Expr<'s> {
         (cnf, mapping)
     }
 
-    pub fn cnf(self) -> (Vec<Vec<Index>>, Mapping<'s>) {
+    pub fn cnf(self) -> (Vec<Vec<Index>>, Mapping<L>) {
         let mut map = Mapping::new();
 
         let mut cnf = Vec::new();

src/expr/helper.rs

@@ -0,0 +1,118 @@
+use super::Expr;
+
+impl<L> Expr<L>
+where
+    L: Clone,
+{
+    pub fn to_expressions(s: &[L]) -> Vec<Expr<L>> {
+        s.iter().map(|l| Expr::Literal(l.clone())).collect()
+    }
+
+    pub fn less_than_two_of(s: &[Expr<L>]) -> Expr<L> {
+        assert!(s.len() > 1);
+        let mut and = Vec::new();
+
+        for i in 0..s.len() {
+            for j in 0..i {
+                and.push(Expr::not(Expr::And(vec![s[i].clone(), s[j].clone()])));
+            }
+        }
+
+        Expr::And(and)
+    }
+
+    pub fn less_than_three_of(s: &[Expr<L>]) -> Expr<L> {
+        assert!(s.len() > 2);
+        let mut and = Vec::new();
+
+        for i in 0..s.len() {
+            for j in 0..i {
+                for k in 0..j {
+                    and.push(Expr::not(Expr::And(vec![
+                        s[i].clone(),
+                        s[j].clone(),
+                        s[k].clone(),
+                    ])));
+                }
+            }
+        }
+
+        Expr::And(and)
+    }
+
+    pub fn more_than_zero_of(s: &[Expr<L>]) -> Expr<L> {
+        Expr::Or(s.to_vec())
+    }
+
+    pub fn more_than_one_of(s: &[Expr<L>]) -> Expr<L> {
+        assert!(s.len() > 1);
+        let mut or = Vec::new();
+
+        for i in 0..s.len() {
+            for j in 0..i {
+                or.push(Expr::And(vec![s[i].clone(), s[j].clone()]));
+            }
+        }
+
+        Expr::Or(or)
+    }
+
+    pub fn more_than_two_of(s: &[Expr<L>]) -> Expr<L> {
+        assert!(s.len() > 2);
+        let mut or = Vec::new();
+
+        for i in 0..s.len() {
+            for j in 0..i {
+                for k in 0..j {
+                    or.push(Expr::And(vec![s[i].clone(), s[j].clone(), s[k].clone()]));
+                }
+            }
+        }
+
+        Expr::Or(or)
+    }
+
+    pub fn more_than_three_of(s: &[Expr<L>]) -> Expr<L> {
+        assert!(!s.is_empty());
+        if s.len() < 4 {
+            Expr::And(vec![s[0].clone(), Expr::not(s[0].clone())])
+        } else {
+            let mut or = Vec::new();
+
+            for i in 0..s.len() {
+                for j in 0..i {
+                    for k in 0..j {
+                        for l in 0..k {
+                            or.push(Expr::And(vec![
+                                s[i].clone(),
+                                s[j].clone(),
+                                s[k].clone(),
+                                s[l].clone(),
+                            ]));
+                        }
+                    }
+                }
+            }
+
+            Expr::Or(or)
+        }
+    }
+
+    pub fn exactly_one_of(s: &[Expr<L>]) -> Expr<L> {
+        Expr::And(vec![Expr::less_than_two_of(s), Expr::more_than_zero_of(s)])
+    }
+
+    pub fn exactly_two_of(s: &[Expr<L>]) -> Expr<L> {
+        Expr::not(Expr::Or(vec![
+            Expr::less_than_two_of(s),
+            Expr::more_than_two_of(s),
+        ]))
+    }
+
+    pub fn exactly_three_of(s: &[Expr<L>]) -> Expr<L> {
+        Expr::And(vec![
+            Expr::not(Expr::more_than_three_of(s)),
+            Expr::not(Expr::less_than_three_of(s)),
+        ])
+    }
+}

src/lib.rs

@@ -0,0 +1,5 @@
+pub mod dpll;
+pub mod dpll_normal_form;
+pub mod expr;
+pub mod mapping;
+pub mod normal_form;

src/mapping.rs

@@ -1,14 +1,17 @@
-use std::collections::HashMap;
+use std::{collections::HashMap, hash::Hash};
 
 use crate::dpll::Index;
 
 #[derive(Debug, Clone)]
-pub struct Mapping<'s> {
+pub struct Mapping<L> {
-    forward: HashMap<&'s str, Index>,
+    forward: HashMap<L, Index>,
-    backward: Vec<&'s str>,
+    backward: Vec<L>,
 }
 
-impl<'s> Mapping<'s> {
+impl<L> Mapping<L>
+where
+    L: Eq + Hash + Clone,
+{
     pub fn new() -> Self {
         Self {
             forward: HashMap::new(),
@@ -16,18 +19,18 @@ impl<'s> Mapping<'s> {
         }
     }
 
-    pub fn forward(&mut self, str: &'s str) -> Index {
+    pub fn forward(&mut self, l: L) -> Index {
-        if let Some(&i) = self.forward.get(str) {
+        if let Some(&i) = self.forward.get(&l) {
             i
         } else {
             let i = self.backward.len() as Index + 1;
-            self.forward.insert(str, i);
+            self.forward.insert(l.clone(), i);
-            self.backward.push(str);
+            self.backward.push(l);
             i
         }
     }
 
-    pub fn backward(&self, i: Index) -> &'s str {
+    pub fn backward(&self, i: Index) -> &L {
-        self.backward[(i - 1) as usize]
+        &self.backward[(i - 1) as usize]
     }
 }