WIP: Rewriting rules

src/formula/general/equivalences/identity.rs

@@ -0,0 +1,23 @@
+use crate::connective::Evaluable;
+
+use super::{Formula, RewritingRule};
+
+#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Default)]
+/// Conjunction with the tautology preserves the term.
+pub struct ConjunctionWithTruth;
+
+impl<T> RewritingRule<T> for ConjunctionWithTruth {
+    fn minimize(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
+        if let Formula::And(f1, f2) = formula {
+            if f1.is_tautology() {
+                Ok(*f2)
+            } else if f2.is_tautology() {
+                Ok(*f1)
+            } else {
+                Err(Formula::And(f1, f2))
+            }
+        } else {
+            Err(formula)
+        }
+    }
+}

src/formula/general/equivalences/mod.rs

@@ -0,0 +1,54 @@
+//! The rules to convert a [`Formula`] to the equivalent one
+//! by using common equivalence laws.
+//!
+//! <https://en.wikipedia.org/wiki/Logical_equivalence>
+
+use super::formula::Formula;
+
+mod identity;
+
+/// Represent the logical law to convert a [`Formula`]
+/// to the equivalent one.
+pub trait RewritingRule<T> {
+    /// Apply the rule returning the (possibly unchanged) new [`Formula`].
+    ///
+    /// Specifying the `minimize` flag ensures the [`Formula`]'s size will not increase,
+    /// i.e. the rule will not be applied if it creates longer [`Formula`].
+    fn apply(&self, formula: Formula<T>, minimize: bool) -> Formula<T> {
+        if minimize {
+            self.minimize(formula)
+        } else {
+            self.reduce(formula)
+        }
+        .unwrap_or_else(|original| original)
+    }
+
+    /// Try to apply the rule to the [`Formula`], if applicable.
+    ///
+    /// The rule is applicable if the necessary structure is found in the [`Formula`].
+    /// For only-shortening rules, the implementation should be the same
+    /// as for the [`minimize`][Self::minimize].
+    ///
+    /// # Errors
+    /// If the rule cannot be applied for the given [`Formula`]
+    /// return the [`Err`] variant containing original [`Formula`].
+    fn reduce(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
+        self.minimize(formula)
+    }
+
+    /// Try to apply the rule to the [`Formula`], if applicable.
+    ///
+    /// The rule is applicable if the necessary structure is found,
+    /// and if the rule will not introduce more connective,
+    /// but rather reduce the original ones.
+    ///
+    /// For example, the [De Morgan's laws](https://en.wikipedia.org/wiki/De_Morgan%27s_laws)
+    /// cannot minimize the [`Formula`] in the general case, but convert it to different form.
+    ///
+    /// # Errors
+    /// If the rule cannot be applied for the given [`Formula`]
+    /// return the [`Err`] variant containing original [`Formula`].
+    fn minimize(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>>;
+}
+
+// TODO: compose normal forms using the combination of specific rules for every kind of NF.

src/formula/general/mod.rs

@@ -1,4 +1,5 @@
 pub mod connective;
+pub mod equivalences;
 mod eval;
 pub mod formula;
 mod ops;

src/formula/mod.rs

@@ -16,6 +16,7 @@ pub use self::{
     eval::Valuation,
     general::{
         connective::{AnyConnective, DynConnective},
+        equivalences,
         formula::Formula,
     },
     lit::{Lit, Literal},