DNF

rsprocess/src/boolean.rs

@@ -29,6 +29,42 @@ impl BooleanFunction {
                 bf1.evaluate(assignments) || bf2.evaluate(assignments),
         }
     }
+
+    pub fn remove_literals(&self) -> Self {
+        match self {
+            | Self::False => Self::False,
+            | Self::True => Self::True,
+            | Self::Not(bf) => match &**bf {
+                | Self::False => Self::True,
+                | Self::True => Self::False,
+                | Self::Not(bf) => bf.remove_literals(),
+                | _ => bf.remove_literals(),
+            },
+            | Self::Variable(i) => Self::Variable(*i),
+            | Self::And(bf1, bf2) => match (&**bf1, &**bf2) {
+                | (Self::False, _) => Self::False,
+                | (_, Self::False) => Self::False,
+                | (Self::True, Self::True) => Self::True,
+                | (Self::True, bf) => bf.remove_literals(),
+                | (bf, Self::True) => bf.remove_literals(),
+                | (bf1, bf2) => Self::And(
+                    Box::new(bf1.remove_literals()),
+                    Box::new(bf2.remove_literals()),
+                ),
+            },
+            | Self::Or(bf1, bf2) => match (&**bf1, &**bf2) {
+                | (Self::True, _) => Self::True,
+                | (_, Self::True) => Self::True,
+                | (Self::False, Self::False) => Self::False,
+                | (Self::False, bf) => bf.remove_literals(),
+                | (bf, Self::False) => bf.remove_literals(),
+                | (bf1, bf2) => Self::Or(
+                    Box::new(bf1.remove_literals()),
+                    Box::new(bf2.remove_literals()),
+                ),
+            },
+        }
+    }
 }
 
 impl PrintableWithTranslator for BooleanFunction {
@@ -60,6 +96,10 @@ impl PrintableWithTranslator for BooleanFunction {
     }
 }
 
+// -----------------------------------------------------------------------------
+// CNF
+// -----------------------------------------------------------------------------
+
 #[derive(
     Default, Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize,
 )]
@@ -267,6 +307,221 @@ impl CNFBooleanFunction {
     }
 }
 
+// -----------------------------------------------------------------------------
+// DNF
+// -----------------------------------------------------------------------------
+
+#[derive(
+    Default, Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize,
+)]
+pub enum DNFLiteral {
+    #[default]
+    False,
+    True,
+    Variable {
+        positive: bool,
+        variable: IdType,
+    },
+}
+
+impl std::ops::Not for DNFLiteral {
+    type Output = DNFLiteral;
+
+    fn not(self) -> Self::Output {
+        match self {
+            | Self::False => Self::True,
+            | Self::True => Self::False,
+            | Self::Variable { positive, variable } => Self::Variable {
+                positive: !positive,
+                variable,
+            },
+        }
+    }
+}
+
+impl DNFLiteral {
+    pub fn evaluate(&self, assignments: &BTreeMap<IdType, bool>) -> bool {
+        match self {
+            | Self::False => false,
+            | Self::True => true,
+            | Self::Variable { positive, variable } =>
+                if *positive {
+                    *assignments.get(variable).unwrap_or(&false)
+                } else {
+                    !*assignments.get(variable).unwrap_or(&false)
+                },
+        }
+    }
+}
+
+impl PrintableWithTranslator for DNFLiteral {
+    fn print(
+        &self,
+        f: &mut std::fmt::Formatter,
+        translator: &crate::translator::Translator,
+    ) -> std::fmt::Result {
+        use DNFLiteral::*;
+        match self {
+            | False => write!(f, "F"),
+            | True => write!(f, "T"),
+            | Variable { positive, variable } =>
+                if *positive {
+                    write!(f, "{}", Formatter::from(translator, variable))
+                } else {
+                    write!(f, "-{}", Formatter::from(translator, variable))
+                },
+        }
+    }
+}
+
+#[derive(Default, Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+// first vec is Or, second in And
+pub struct DNFBooleanFunction {
+    pub formula: Vec<Vec<DNFLiteral>>,
+}
+
+impl PrintableWithTranslator for DNFBooleanFunction {
+    fn print(
+        &self,
+        f: &mut std::fmt::Formatter,
+        translator: &crate::translator::Translator,
+    ) -> std::fmt::Result {
+        let mut it = self.formula.iter().peekable();
+        while let Some(or_formula) = it.next() {
+            let mut or_it = or_formula.iter().peekable();
+            write!(f, "(")?;
+            while let Some(or) = or_it.next() {
+                if or_it.peek().is_none() {
+                    write!(f, "{}", Formatter::from(translator, or))?;
+                } else {
+                    write!(f, "{} ^ ", Formatter::from(translator, or))?;
+                }
+            }
+            if it.peek().is_none() {
+                write!(f, ")")?;
+            } else {
+                writeln!(f, ") v")?;
+            }
+        }
+        Ok(())
+    }
+}
+
+impl From<BooleanFunction> for DNFBooleanFunction {
+    fn from(source: BooleanFunction) -> Self {
+        fn morgan(source: DNFBooleanFunction) -> DNFBooleanFunction {
+            let temp: Vec<Vec<_>> = source
+                .formula
+                .into_iter()
+                .map(|f| f.into_iter().map(|l| !l).collect())
+                .collect();
+
+            let lenghts: Vec<usize> = temp.iter().map(|f| f.len()).collect();
+            let mut position = vec![0; temp.len()];
+
+            let add_one = |position: &mut Vec<usize>| -> bool {
+                let mut location: usize = 0;
+                loop {
+                    if location >= position.len() {
+                        return true;
+                    }
+                    position[location] += 1;
+                    if position[location] >= lenghts[location] {
+                        position[location] = 0;
+                    } else {
+                        return false;
+                    }
+                    location += 1;
+                }
+            };
+
+            let mut ret_val = vec![];
+            loop {
+                ret_val.push(
+                    position
+                        .iter()
+                        .enumerate()
+                        .map(|(pos, p)| temp[pos][*p])
+                        .collect(),
+                );
+
+                if add_one(&mut position) {
+                    break;
+                }
+            }
+            DNFBooleanFunction { formula: ret_val }
+        }
+
+        fn helper_normalize(source: BooleanFunction) -> DNFBooleanFunction {
+            match &source {
+                | BooleanFunction::False => DNFBooleanFunction {
+                    formula: vec![vec![DNFLiteral::False]],
+                },
+                | BooleanFunction::True => DNFBooleanFunction {
+                    formula: vec![vec![DNFLiteral::True]],
+                },
+                | BooleanFunction::Variable(v) => DNFBooleanFunction {
+                    formula: vec![vec![DNFLiteral::Variable {
+                        positive: true,
+                        variable: *v,
+                    }]],
+                },
+                | BooleanFunction::And(n1, n2) => {
+                    let n1 = helper_normalize(*n1.clone());
+                    let n2 = helper_normalize(*n2.clone());
+
+                    let mut formulas = vec![];
+                    for formula1 in n1.formula {
+                        for formula2 in &n2.formula {
+                            formulas.push(
+                                formula1
+                                    .iter()
+                                    .chain(formula2.iter())
+                                    .cloned()
+                                    .collect(),
+                            );
+                        }
+                    }
+                    DNFBooleanFunction { formula: formulas }
+                },
+                | BooleanFunction::Or(n1, n2) => {
+                    let n1 = helper_normalize(*n1.clone());
+                    let n2 = helper_normalize(*n2.clone());
+
+                    DNFBooleanFunction {
+                        formula: n1
+                            .formula
+                            .into_iter()
+                            .chain(n2.formula)
+                            .collect(),
+                    }
+                },
+                | BooleanFunction::Not(n) => {
+                    if let BooleanFunction::Not(n) = &**n {
+                        helper_normalize(*n.clone())
+                    } else {
+                        morgan(helper_normalize(*n.clone()))
+                    }
+                },
+            }
+        }
+
+        helper_normalize(source)
+    }
+}
+
+impl DNFBooleanFunction {
+    pub fn evaluate(&self, assignments: &BTreeMap<IdType, bool>) -> bool {
+        self.formula
+            .iter()
+            .any(|or_f| or_f.iter().all(|l| l.evaluate(assignments)))
+    }
+}
+
+// -----------------------------------------------------------------------------
+// Boolean Networks
+// -----------------------------------------------------------------------------
+
 #[derive(Default, Clone, PartialEq, Eq, Serialize, Deserialize)]
 pub struct BooleanNetwork {
     initial_state: BTreeMap<IdType, bool>,

rsprocess/src/boolean_test.rs

@@ -1,6 +1,9 @@
 use std::collections::BTreeMap;
 
-use crate::boolean::{BooleanFunction, CNFBooleanFunction, CNFLiteral};
+use crate::boolean::{
+    BooleanFunction, CNFBooleanFunction, CNFLiteral, DNFBooleanFunction,
+    DNFLiteral,
+};
 use crate::element::IdType;
 
 macro_rules! cnfl {
@@ -15,6 +18,18 @@ macro_rules! cnfl {
     };
 }
 
+macro_rules! dnfl {
+    ($i:ident) => {
+        DNFLiteral::$i
+    };
+    ($p:literal, $i:literal) => {
+        DNFLiteral::Variable {
+            positive: $p,
+            variable: $i,
+        }
+    };
+}
+
 macro_rules! boolean {
     (False) => (BooleanFunction::False);
     (True) => (BooleanFunction::True);
@@ -34,8 +49,15 @@ macro_rules! boolean {
     );
 }
 
+// -----------------------------------------------------------------------------
+// Tests
+// -----------------------------------------------------------------------------
+
+// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+// CNF
+
 #[test]
-fn boolean_1() {
+fn cnf_1() {
     let bf = boolean!(False);
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -43,7 +65,7 @@ fn boolean_1() {
 }
 
 #[test]
-fn boolean_2() {
+fn cnf_2() {
     let bf = boolean!(True);
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -51,7 +73,7 @@ fn boolean_2() {
 }
 
 #[test]
-fn boolean_3() {
+fn cnf_3() {
     let bf = boolean!(Variable(1));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -59,7 +81,7 @@ fn boolean_3() {
 }
 
 #[test]
-fn boolean_4() {
+fn cnf_4() {
     let bf = boolean!(Not(True));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -67,7 +89,7 @@ fn boolean_4() {
 }
 
 #[test]
-fn boolean_5() {
+fn cnf_5() {
     let bf = boolean!(Not(False));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -75,7 +97,7 @@ fn boolean_5() {
 }
 
 #[test]
-fn boolean_6() {
+fn cnf_6() {
     let bf = boolean!(Not(False));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -83,7 +105,7 @@ fn boolean_6() {
 }
 
 #[test]
-fn boolean_7() {
+fn cnf_7() {
     let bf = boolean!(Not(Not(False)));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -91,7 +113,7 @@ fn boolean_7() {
 }
 
 #[test]
-fn boolean_8() {
+fn cnf_8() {
     let bf = boolean!(Not(Not(True)));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -99,7 +121,7 @@ fn boolean_8() {
 }
 
 #[test]
-fn boolean_9() {
+fn cnf_9() {
     let bf = boolean!(Not(Variable(0)));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -107,7 +129,7 @@ fn boolean_9() {
 }
 
 #[test]
-fn boolean_10() {
+fn cnf_10() {
     let bf = boolean!(Not(Not(Variable(0))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -115,7 +137,7 @@ fn boolean_10() {
 }
 
 #[test]
-fn boolean_11() {
+fn cnf_11() {
     let bf = boolean!(And((True), (True)));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -123,7 +145,7 @@ fn boolean_11() {
 }
 
 #[test]
-fn boolean_12() {
+fn cnf_12() {
     let bf = boolean!(And((True), (False)));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -131,7 +153,7 @@ fn boolean_12() {
 }
 
 #[test]
-fn boolean_13() {
+fn cnf_13() {
     let bf = boolean!(And((Variable(0)), (False)));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -139,7 +161,7 @@ fn boolean_13() {
 }
 
 #[test]
-fn boolean_14() {
+fn cnf_14() {
     let bf = boolean!(And((Not(Variable(0))), (False)));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -147,7 +169,7 @@ fn boolean_14() {
 }
 
 #[test]
-fn boolean_15() {
+fn cnf_15() {
     let bf = boolean!(And((Not(Variable(0))), (Not(Not(Variable(1))))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -155,7 +177,7 @@ fn boolean_15() {
 }
 
 #[test]
-fn boolean_16() {
+fn cnf_16() {
     let bf = boolean!(And((And((True), (True))), (Not(Not(Variable(1))))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -165,7 +187,7 @@ fn boolean_16() {
 }
 
 #[test]
-fn boolean_17() {
+fn cnf_17() {
     let bf = boolean!(Not(And((False), (False))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -173,7 +195,7 @@ fn boolean_17() {
 }
 
 #[test]
-fn boolean_18() {
+fn cnf_18() {
     let bf = boolean!(Not(And((False), (True))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -181,7 +203,7 @@ fn boolean_18() {
 }
 
 #[test]
-fn boolean_19() {
+fn cnf_19() {
     let bf = boolean!(Not(And((False), (Not(True)))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -189,7 +211,7 @@ fn boolean_19() {
 }
 
 #[test]
-fn boolean_20() {
+fn cnf_20() {
     let bf = boolean!(Not(And((Variable(0)), (Not(True)))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -197,7 +219,7 @@ fn boolean_20() {
 }
 
 #[test]
-fn boolean_21() {
+fn cnf_21() {
     let bf = boolean!(Not(And((Variable(0)), (Not(And((True), (False)))))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -208,7 +230,7 @@ fn boolean_21() {
 }
 
 #[test]
-fn boolean_22() {
+fn cnf_22() {
     let bf = boolean!(And(
         (Or((Variable(0)), (Or((Not(Variable(1))), (Variable(2)))))),
         (Or((Not(Variable(3))), (Or((Variable(4)), (Variable(5))))))
@@ -222,7 +244,7 @@ fn boolean_22() {
 }
 
 #[test]
-fn boolean_23() {
+fn cnf_23() {
     let bf = boolean!(And((Or((Variable(0)), (Variable(1)))), (Variable(2))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -232,7 +254,7 @@ fn boolean_23() {
 }
 
 #[test]
-fn boolean_24() {
+fn cnf_24() {
     let bf = boolean!(Or((Variable(0)), (Variable(1))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -240,7 +262,7 @@ fn boolean_24() {
 }
 
 #[test]
-fn boolean_25() {
+fn cnf_25() {
     let bf = boolean!(Or((Variable(0)), (Or((Variable(1)), (Variable(2))))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -252,7 +274,7 @@ fn boolean_25() {
 }
 
 #[test]
-fn boolean_26() {
+fn cnf_26() {
     let bf = boolean!(Or(
         (Variable(0)),
         (Or((Variable(1)), (Or((Variable(2)), (Variable(3))))))
@@ -268,7 +290,7 @@ fn boolean_26() {
 }
 
 #[test]
-fn boolean_27() {
+fn cnf_27() {
     let bf = boolean!(Or(
         (Variable(0)),
         (Or(
@@ -288,7 +310,7 @@ fn boolean_27() {
 }
 
 #[test]
-fn boolean_28() {
+fn cnf_28() {
     let bf = boolean!(Or((Not(Variable(0))), (Variable(1))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -296,7 +318,7 @@ fn boolean_28() {
 }
 
 #[test]
-fn boolean_29() {
+fn cnf_29() {
     let bf = boolean!(Or((Not(Variable(0))), (Not(Not(Variable(1))))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -304,7 +326,7 @@ fn boolean_29() {
 }
 
 #[test]
-fn boolean_30() {
+fn cnf_30() {
     let bf = boolean!(Not(Or((False), (False))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -312,7 +334,7 @@ fn boolean_30() {
 }
 
 #[test]
-fn boolean_31() {
+fn cnf_31() {
     let bf = boolean!(Not(Or((False), (True))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -320,7 +342,7 @@ fn boolean_31() {
 }
 
 #[test]
-fn boolean_32() {
+fn cnf_32() {
     let bf = boolean!(Not(Or((Variable(0)), (Not(Or((True), (False)))))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -334,7 +356,7 @@ fn boolean_32() {
 }
 
 #[test]
-fn boolean_33() {
+fn cnf_33() {
     let bf = boolean!(Not(Or((Variable(0)), (Not(And((True), (False)))))));
     let cnf: CNFBooleanFunction = bf.into();
 
@@ -348,7 +370,7 @@ fn boolean_33() {
 }
 
 #[test]
-fn boolean_34() {
+fn cnf_34() {
     let bf = boolean!(Or(
         (And((Variable(0)), (Variable(1)))),
         (Or(
@@ -388,7 +410,7 @@ fn boolean_34() {
 }
 
 #[test]
-fn boolean_35() {
+fn cnf_35() {
     let bf = boolean!(Or(
         (And(
             (And(
@@ -418,3 +440,400 @@ fn boolean_35() {
         assert_eq!(cnf.evaluate(assignment), res);
     }
 }
+
+// %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+// DNF
+
+#[test]
+fn dnf_1() {
+    let bf = boolean!(False);
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(False)]]);
+}
+
+#[test]
+fn dnf_2() {
+    let bf = boolean!(True);
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True)]]);
+}
+
+#[test]
+fn dnf_3() {
+    let bf = boolean!(Variable(1));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(true, 1)]]);
+}
+
+#[test]
+fn dnf_4() {
+    let bf = boolean!(Not(True));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(False)]]);
+}
+
+#[test]
+fn dnf_5() {
+    let bf = boolean!(Not(False));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True)]]);
+}
+
+#[test]
+fn dnf_6() {
+    let bf = boolean!(Not(False));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True)]]);
+}
+
+#[test]
+fn dnf_7() {
+    let bf = boolean!(Not(Not(False)));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(False)]]);
+}
+
+#[test]
+fn dnf_8() {
+    let bf = boolean!(Not(Not(True)));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True)]]);
+}
+
+#[test]
+fn dnf_9() {
+    let bf = boolean!(Not(Variable(0)));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(false, 0)]]);
+}
+
+#[test]
+fn dnf_10() {
+    let bf = boolean!(Not(Not(Variable(0))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(true, 0)]]);
+}
+
+#[test]
+fn dnf_11() {
+    let bf = boolean!(And((True), (True)));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True), dnfl!(True)]]);
+}
+
+#[test]
+fn dnf_12() {
+    let bf = boolean!(And((True), (False)));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True), dnfl!(False)]]);
+}
+
+#[test]
+fn dnf_13() {
+    let bf = boolean!(And((Variable(0)), (False)));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(true, 0), dnfl!(False)]]);
+}
+
+#[test]
+fn dnf_14() {
+    let bf = boolean!(And((Not(Variable(0))), (False)));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(false, 0), dnfl!(False)]]);
+}
+
+#[test]
+fn dnf_15() {
+    let bf = boolean!(And((Not(Variable(0))), (Not(Not(Variable(1))))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(false, 0), dnfl!(true, 1)]]);
+}
+
+#[test]
+fn dnf_16() {
+    let bf = boolean!(And((And((True), (True))), (Not(Not(Variable(1))))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True), dnfl!(True), dnfl!(true, 1)]]);
+}
+
+#[test]
+fn dnf_17() {
+    let bf = boolean!(Not(And((False), (False))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True)], [dnfl!(True)]]);
+}
+
+#[test]
+fn dnf_18() {
+    let bf = boolean!(Not(And((False), (True))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True)], [dnfl!(False)]]);
+}
+
+#[test]
+fn dnf_19() {
+    let bf = boolean!(Not(And((False), (Not(True)))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True)], [dnfl!(True)]]);
+}
+
+#[test]
+fn dnf_20() {
+    let bf = boolean!(Not(And((Variable(0)), (Not(True)))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(false, 0)], [dnfl!(True)]]);
+}
+
+#[test]
+fn dnf_21() {
+    let bf = boolean!(Not(And((Variable(0)), (Not(And((True), (False)))))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    let assignments = BTreeMap::from([(0, false)]);
+
+    assert!(cnf.evaluate(&assignments));
+
+    let assignments = BTreeMap::from([(0, true)]);
+
+    assert!(!cnf.evaluate(&assignments));
+}
+
+#[test]
+fn dnf_22() {
+    let bf = boolean!(And(
+        (Or((Variable(0)), (Or((Not(Variable(1))), (Variable(2)))))),
+        (Or((Not(Variable(3))), (Or((Variable(4)), (Variable(5))))))
+    ));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    let assignments: Vec<BTreeMap<IdType, bool>> = (0_u32..128)
+        .map(|p| {
+            BTreeMap::from_iter(
+                (0..8)
+                    .map(|pos| (pos, p >> pos & 1 == 1))
+                    .collect::<Vec<_>>(),
+            )
+        })
+        .collect();
+
+    let correct_results = [
+        true, true, false, true, true, true, true, true, false, false, false,
+        false, false, false, false, false, true, true, false, true, true,
+        true, true, true, true, true, false, true, true, true, true, true,
+        true, true, false, true, true, true, true, true, true, true, false,
+        true, true, true, true, true, true, true, false, true, true, true,
+        true, true, true, true, false, true, true, true, true, true
+    ];
+
+    for (assignment, res) in assignments.iter().zip(correct_results) {
+        assert_eq!(cnf.evaluate(assignment), res);
+    }
+}
+
+#[test]
+fn dnf_23() {
+    let bf = boolean!(And((Or((Variable(0)), (Variable(1)))), (Variable(2))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [vec![dnfl!(true, 0), dnfl!(true, 2)],
+                             vec![dnfl!(true, 1), dnfl!(true, 2)]]);
+}
+
+#[test]
+fn dnf_24() {
+    let bf = boolean!(Or((Variable(0)), (Variable(1))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(true, 0)], [dnfl!(true, 1)]]);
+}
+
+#[test]
+fn dnf_25() {
+    let bf = boolean!(Or((Variable(0)), (Or((Variable(1)), (Variable(2))))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(true, 0)],[dnfl!(true, 1)],[dnfl!(true, 2)]]);
+}
+
+#[test]
+fn dnf_26() {
+    let bf = boolean!(Or(
+        (Variable(0)),
+        (Or((Variable(1)), (Or((Variable(2)), (Variable(3))))))
+    ));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [
+        [dnfl!(true, 0)],
+        [dnfl!(true, 1)],
+        [dnfl!(true, 2)],
+        [dnfl!(true, 3)]
+    ]);
+}
+
+#[test]
+fn dnf_27() {
+    let bf = boolean!(Or(
+        (Variable(0)),
+        (Or(
+            (Or((Variable(1)), (Variable(2)))),
+            (Or((Variable(3)), (Variable(4))))
+        ))
+    ));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [
+        [dnfl!(true, 0)],
+        [dnfl!(true, 1)],
+        [dnfl!(true, 2)],
+        [dnfl!(true, 3)],
+        [dnfl!(true, 4)],
+    ]);
+}
+
+#[test]
+fn dnf_28() {
+    let bf = boolean!(Or((Not(Variable(0))), (Variable(1))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(false, 0)], [dnfl!(true, 1)]]);
+}
+
+#[test]
+fn dnf_29() {
+    let bf = boolean!(Or((Not(Variable(0))), (Not(Not(Variable(1))))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(false, 0)], [dnfl!(true, 1)]]);
+}
+
+#[test]
+fn dnf_30() {
+    let bf = boolean!(Not(Or((False), (False))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True), dnfl!(True)]]);
+}
+
+#[test]
+fn dnf_31() {
+    let bf = boolean!(Not(Or((False), (True))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(True), dnfl!(False)]]);
+}
+
+#[test]
+fn dnf_32() {
+    let bf = boolean!(Not(Or((Variable(0)), (Not(Or((True), (False)))))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    assert_eq!(cnf.formula, [[dnfl!(false, 0), dnfl!(True)],
+                             [dnfl!(false, 0), dnfl!(False)]]);
+}
+
+#[test]
+fn dnf_33() {
+    let bf = boolean!(Not(Or((Variable(0)), (Not(And((True), (False)))))));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    let assignments = BTreeMap::from([(0, false)]);
+
+    assert!(!cnf.evaluate(&assignments));
+
+    let assignments = BTreeMap::from([(0, true)]);
+
+    assert!(!cnf.evaluate(&assignments));
+}
+
+#[test]
+fn dnf_34() {
+    let bf = boolean!(Or(
+        (And((Variable(0)), (Variable(1)))),
+        (Or(
+            (Or((Variable(2)), (Not(Variable(3))))),
+            (Not(And((And((Variable(4)), (Not(Variable(5))))), (Variable(6)))))
+        ))
+    ));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    let assignments: Vec<BTreeMap<IdType, bool>> = (0_u32..128)
+        .map(|p| {
+            BTreeMap::from_iter(
+                (0..8)
+                    .map(|pos| (pos, p >> pos & 1 == 1))
+                    .collect::<Vec<_>>(),
+            )
+        })
+        .collect();
+
+    let correct_results = [
+        true, true, true, true, true, true, true, true, true, true, true, true,
+        true, true, true, true, true, true, true, true, true, true, true, true,
+        true, true, true, true, true, true, true, true, true, true, true, true,
+        true, true, true, true, true, true, true, true, true, true, true, true,
+        true, true, true, true, true, true, true, true, true, true, true, true,
+        true, true, true, true, true, true, true, true, true, true, true, true,
+        true, true, true, true, true, true, true, true, true, true, true, true,
+        true, true, true, true, false, false, false, true, true, true, true,
+        true, true, true, true, true, true, true, true, true, true, true, true,
+        true, true, true, true, true, true, true, true, true, true, true, true,
+        true, true, true, true, true, true, true, true, true,
+    ];
+
+    for (assignment, res) in assignments.iter().zip(correct_results) {
+        assert_eq!(cnf.evaluate(assignment), res);
+    }
+}
+
+#[test]
+fn dnf_35() {
+    let bf = boolean!(Or(
+        (And(
+            (And(
+                (Or((Variable(0)), (Or((Variable(1)), (Variable(2)))))),
+                (Or((And((Variable(0)), (Not(Variable(1))))), (Variable(2))))
+            )),
+            (Not(Variable(2)))
+        )),
+        (And((Variable(2)), (Not(Or((Variable(0)), (Variable(1)))))))
+    ));
+    let cnf: DNFBooleanFunction = bf.into();
+
+    let assignments: Vec<BTreeMap<IdType, bool>> = (0_u32..8)
+        .map(|p| {
+            BTreeMap::from_iter(
+                (0..3)
+                    .map(|pos| (pos, p >> pos & 1 == 1))
+                    .collect::<Vec<_>>(),
+            )
+        })
+        .collect();
+
+    let correct_results =
+        [false, true, false, false, true, false, false, false];
+
+    for (assignment, res) in assignments.iter().zip(correct_results) {
+        assert_eq!(cnf.evaluate(assignment), res);
+    }
+}