From 23cbd39039c63c3a252b35be48d0fb8a1860a88c Mon Sep 17 00:00:00 2001 From: hal8174 Date: Sun, 3 Nov 2024 19:58:06 +0100 Subject: [PATCH] Generalize literals in epression and add helper function for expressions --- src/expr.rs | 46 ++++++++++++++---- src/expr/helper.rs | 118 +++++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 5 ++ src/mapping.rs | 25 +++++----- 4 files changed, 173 insertions(+), 21 deletions(-) create mode 100644 src/expr/helper.rs create mode 100644 src/lib.rs diff --git a/src/expr.rs b/src/expr.rs index 2a10559..443207f 100644 --- a/src/expr.rs +++ b/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> { - Literal(&'s str), - Not(Box>), - And(Vec>), - Or(Vec>), +pub enum Expr +where + L: Clone, +{ + Literal(L), + Not(Box>), + And(Vec>), + Or(Vec>), +} + +impl Expr +where + L: Clone, +{ + pub fn not(e: Expr) -> Expr { + Expr::Not(Box::new(e)) + } } #[derive(Debug)] @@ -91,8 +107,8 @@ impl<'s> Iterator for Tokanizer<'s> { } } -impl<'s> Expr<'s> { - fn parse_expr(tokanizer: &mut Tokanizer<'s>) -> Result> { +impl<'s> Expr<&'s str> { + fn parse_expr(tokanizer: &mut Tokanizer<'s>) -> Result> { 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 Expr +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 Expr +where + L: Clone + Eq + Hash, +{ + pub fn disjunctive_normal_form2(self, mapping: &mut Mapping) -> 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) { 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>, Mapping<'s>) { + pub fn cnf(self) -> (Vec>, Mapping) { let mut map = Mapping::new(); let mut cnf = Vec::new(); diff --git a/src/expr/helper.rs b/src/expr/helper.rs new file mode 100644 index 0000000..fd5006c --- /dev/null +++ b/src/expr/helper.rs @@ -0,0 +1,118 @@ +use super::Expr; + +impl Expr +where + L: Clone, +{ + pub fn to_expressions(s: &[L]) -> Vec> { + s.iter().map(|l| Expr::Literal(l.clone())).collect() + } + + pub fn less_than_two_of(s: &[Expr]) -> Expr { + 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]) -> Expr { + 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]) -> Expr { + Expr::Or(s.to_vec()) + } + + pub fn more_than_one_of(s: &[Expr]) -> Expr { + 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]) -> Expr { + 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]) -> Expr { + 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]) -> Expr { + Expr::And(vec![Expr::less_than_two_of(s), Expr::more_than_zero_of(s)]) + } + + pub fn exactly_two_of(s: &[Expr]) -> Expr { + Expr::not(Expr::Or(vec![ + Expr::less_than_two_of(s), + Expr::more_than_two_of(s), + ])) + } + + pub fn exactly_three_of(s: &[Expr]) -> Expr { + Expr::And(vec![ + Expr::not(Expr::more_than_three_of(s)), + Expr::not(Expr::less_than_three_of(s)), + ]) + } +} diff --git a/src/lib.rs b/src/lib.rs new file mode 100644 index 0000000..79f6fdb --- /dev/null +++ b/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; diff --git a/src/mapping.rs b/src/mapping.rs index f42337d..8b7546c 100644 --- a/src/mapping.rs +++ b/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> { - forward: HashMap<&'s str, Index>, - backward: Vec<&'s str>, +pub struct Mapping { + forward: HashMap, + backward: Vec, } -impl<'s> Mapping<'s> { +impl Mapping +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 { - if let Some(&i) = self.forward.get(str) { + pub fn forward(&mut self, l: L) -> Index { + if let Some(&i) = self.forward.get(&l) { i } else { let i = self.backward.len() as Index + 1; - self.forward.insert(str, i); - self.backward.push(str); + self.forward.insert(l.clone(), i); + self.backward.push(l); i } } - pub fn backward(&self, i: Index) -> &'s str { - self.backward[(i - 1) as usize] + pub fn backward(&self, i: Index) -> &L { + &self.backward[(i - 1) as usize] } }