generic TruthTable

Author: tsionyx

examples/truth_table.rs

@@ -1,11 +1,11 @@
 //! Print truth tables for all the binary functions.
 #![allow(clippy::wildcard_imports)]
 
-use prop_logic::{connective::*, two_powers, CheckedArray};
+use prop_logic::{connective::*, two_powers, CheckedArray, TruthTabled as _};
 
 fn print_stat<const ARITY: usize>(f: &dyn StoredBoolFn<ARITY>)
 where
-    TruthTable<ARITY>: std::fmt::Display,
+    FixedTruthTable<ARITY>: std::fmt::Display,
     two_powers::D: CheckedArray<ARITY>,
 {
     print!("{}", f.notation());

src/connective/functions/binary/and.rs

@@ -128,18 +128,16 @@ where
 
 #[cfg(test)]
 mod tests {
+    use crate::truth_table::TruthTabled;
+
     use super::{
-        super::super::{
-            super::{EquivalentBoolFn, InitFn as _},
-            ternary::Ternary,
-            LogicalIdentity, Truth,
-        },
+        super::super::{super::InitFn as _, ternary::Ternary, LogicalIdentity, Truth},
         *,
     };
 
     #[test]
     fn any_equivalences() {
-        assert!(<Truth as EquivalentBoolFn<0>>::is_equivalent(
+        assert!(<Truth as TruthTabled<0>>::is_equivalent(
             &Truth,
             &ConjunctionAny::init()
         ));

src/connective/functions/binary/or.rs

@@ -127,18 +127,16 @@ where
 
 #[cfg(test)]
 mod tests {
+    use crate::truth_table::TruthTabled;
+
     use super::{
-        super::super::{
-            super::{EquivalentBoolFn, InitFn as _},
-            ternary::Ternary,
-            Falsity, LogicalIdentity,
-        },
+        super::super::{super::InitFn as _, ternary::Ternary, Falsity, LogicalIdentity},
         *,
     };
 
     #[test]
     fn any_equivalences() {
-        assert!(<Falsity as EquivalentBoolFn<0>>::is_equivalent(
+        assert!(<Falsity as TruthTabled<0>>::is_equivalent(
             &Falsity,
             &DisjunctionAny::init()
         ));

src/connective/functions/binary/xnor.rs

@@ -169,22 +169,20 @@ where
 
 #[cfg(test)]
 mod tests {
+    use crate::truth_table::TruthTabled;
+
     use super::{
-        super::super::{
-            super::{EquivalentBoolFn, InitFn as _},
-            ternary::Ternary,
-            Truth,
-        },
+        super::super::{super::InitFn as _, ternary::Ternary, Truth},
         *,
     };
 
     #[test]
     fn any_equivalences() {
-        assert!(<Truth as EquivalentBoolFn<0>>::is_equivalent(
+        assert!(<Truth as TruthTabled<0>>::is_equivalent(
             &Truth,
             &AllEquivalent::init()
         ));
-        assert!(<Truth as EquivalentBoolFn<1>>::is_equivalent(
+        assert!(<Truth as TruthTabled<1>>::is_equivalent(
             &Truth,
             &AllEquivalent::init()
         ));

src/connective/functions/binary/xor.rs

@@ -139,18 +139,16 @@ where
 
 #[cfg(test)]
 mod tests {
+    use crate::truth_table::TruthTabled;
+
     use super::{
-        super::super::{
-            super::{EquivalentBoolFn, InitFn as _},
-            ternary::Ternary,
-            Falsity, LogicalIdentity,
-        },
+        super::super::{super::InitFn as _, ternary::Ternary, Falsity, LogicalIdentity},
         *,
     };
 
     #[test]
     fn any_equivalences() {
-        assert!(<Falsity as EquivalentBoolFn<0>>::is_equivalent(
+        assert!(<Falsity as TruthTabled<0>>::is_equivalent(
             &Falsity,
             &ExclusiveDisjunctionAny::init()
         ));

src/connective/functions/ternary.rs

@@ -1,7 +1,9 @@
 //! Generic ternary function as the composition of two binary functions.
 //!
 //! <https://en.wikipedia.org/wiki/Ternary_operation>
-use super::super::{ops::Associativity as _, EquivalentBoolFn, Evaluable, TruthFn};
+use crate::truth_table::TruthTabled;
+
+use super::super::{ops::Associativity, Evaluable, TruthFn};
 
 #[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Default)]
 /// Wrapper for a ternary boolean function which applies
@@ -21,8 +23,8 @@ impl<const LEFT: bool, Op1, Op2> Ternary<LEFT, Op1, Op2> {
 impl<const LEFT: bool, E, Op1, Op2> TruthFn<3, E> for Ternary<LEFT, Op1, Op2>
 where
     E: Evaluable + Clone, // TODO: try to get rid of this `Clone` requirement
-    Op1: TruthFn<2, E> + EquivalentBoolFn<2>,
-    Op2: TruthFn<2, E> + EquivalentBoolFn<2>,
+    Op1: TruthFn<2, E> + TruthTabled<2> + Associativity,
+    Op2: TruthFn<2, E> + TruthTabled<2, TT = <Op1 as TruthTabled<2>>::TT> + Associativity,
 {
     fn fold(&self, values: [E; 3]) -> Result<E, [E; 3]> {
         let try_fold = |left| {

src/connective/mod.rs

@@ -21,8 +21,8 @@ pub use self::{
     priority::{Prioritized, Priority},
     properties::{is_basis, is_complete, BoolFnExt},
     storage::{AllFunctions, StoredBoolFn, BINARY_FUNCTIONS, NULLARY_FUNCTIONS, UNARY_FUNCTIONS},
-    traits::{BoolFn, Connective, EquivalentBoolFn, InitFn, TruthFn, TruthFnConnector},
-    truth_table::TruthTable,
+    traits::{BoolFn, Connective, InitFn, TruthFn, TruthFnConnector},
+    truth_table::FixedTruthTable,
 };
 
 #[allow(path_statements, clippy::no_effect)]
@@ -70,6 +70,8 @@ mod tests {
         F: TruthFn<ARITY, Formula<()>> + BoolFn<ARITY>,
         two_powers::D: CheckedArray<ARITY>,
     {
+        use crate::truth_table::TruthTabled as _;
+
         let truth_table = f.get_truth_table().into_iter();
         let eval_variants = truth_table.map(|(assignment, eval)| {
             let formulas = assignment

src/connective/ops.rs

@@ -1,8 +1,10 @@
 //! Unary operations and properties of the [`BoolFn`]-s.
 use std::{collections::HashMap as Map, ops::Not};
 
+use crate::truth_table::TruthTabled as _;
+
 #[allow(clippy::wildcard_imports)]
-use super::{functions::*, ternary::Ternary, BoolFn, EquivalentBoolFn as _, InitFn as _};
+use super::{functions::*, ternary::Ternary, BoolFn, InitFn as _};
 
 /// Easily convert a `BoolFn` into its counterpart in terms
 /// of switching all the bits in its truth table.
@@ -161,6 +163,8 @@ where
     F: BoolFn<2>,
 {
     fn is_commutative(&self) -> bool {
+        use crate::truth_table::TruthTabled as _;
+
         let table: Map<_, _> = self.get_truth_table().into_iter().collect();
 
         table.iter().all(|(args, val)| {
@@ -196,7 +200,11 @@ where
 mod tests {
     use std::collections::HashMap;
 
-    use crate::{arity::two_powers, utils::dependent_array::CheckedArray};
+    use crate::{
+        arity::two_powers,
+        truth_table::{TruthTable as _, TruthTabled as _},
+        utils::dependent_array::CheckedArray,
+    };
 
     use super::{super::InitFn, *};
 
@@ -206,8 +214,8 @@ mod tests {
         N::Not: BoolFn<ARITY> + InitFn,
         two_powers::D: CheckedArray<ARITY>,
     {
-        let table = N::init().get_truth_table().into_values();
-        let table_neg = N::Not::init().get_truth_table().into_values();
+        let table = N::init().get_truth_table().values();
+        let table_neg = N::Not::init().get_truth_table().values();
 
         dbg!(std::any::type_name::<N>());
         dbg!(std::any::type_name::<N::Not>());
@@ -222,8 +230,8 @@ mod tests {
         N2: BoolFn<ARITY>,
         two_powers::D: CheckedArray<ARITY>,
     {
-        let table = x.get_truth_table().into_values();
-        let table_neg = (!x).get_truth_table().into_values();
+        let table = x.get_truth_table().values();
+        let table_neg = (!x).get_truth_table().values();
 
         dbg!(std::any::type_name::<N>());
         for (x, y) in table.into_iter().zip(table_neg) {

src/connective/ordering.rs

@@ -1,10 +1,11 @@
 use std::cmp::Ordering;
 
 #[allow(clippy::wildcard_imports)]
-use super::{functions::*, truth_table, BoolFn, InitFn as _};
+use super::{functions::*, BoolFn, InitFn as _};
 
 use crate::{
     arity::two_powers::D,
+    truth_table::{TruthTable as _, TruthTabled as _},
     utils::{cartesian_diag, dependent_array::CheckedArray},
 };
 
@@ -18,10 +19,9 @@ where
     Op1: BoolFn<ARITY> + Default,
     Op2: BoolFn<ARITY> + Default,
     D: CheckedArray<ARITY>,
-    <D as CheckedArray<ARITY>>::Array<truth_table::Row<ARITY>>: Clone,
 {
-    let op1_truth_table = Op1::init().get_truth_table().into_values();
-    let op2_truth_table = Op2::init().get_truth_table().into_values();
+    let op1_truth_table = Op1::init().get_truth_table().values();
+    let op2_truth_table = Op2::init().get_truth_table().values();
 
     let mut set_ordering = Ordering::Equal;
     for (&val1, &val2) in op1_truth_table.iter().zip(&op2_truth_table) {

src/connective/properties.rs

@@ -6,14 +6,15 @@ use super::BoolFn;
 
 use crate::{
     arity::two_powers,
+    truth_table::TruthTabled as _,
     utils::{
         dependent_array::{CheckedArray, Discriminant as _},
         upcast::UpcastFrom,
     },
 };
 
 /// Defines the important properies of a [`BoolFn`]
-/// based on its [`TruthTable`][crate::connective::TruthTable].
+/// based on its [`TruthTable`][crate::truth_table::TruthTable].
 ///
 /// The most important of the properies are the includeness
 /// of a boolean function in some of the

src/connective/storage.rs

@@ -68,6 +68,8 @@ pub const BINARY_FUNCTIONS: AllFunctions<2> = CheckedStorage::new([
 
 #[cfg(test)]
 mod tests_ordering {
+    use crate::truth_table::TruthTabled as _;
+
     use super::*;
 
     #[test]

src/connective/traits.rs

@@ -1,17 +1,6 @@
-use std::{collections::BTreeMap as Map, iter};
+use crate::utils::{operation::Operation, upcast::UpcastFrom};
 
-use itertools::Itertools as _;
-
-use crate::{
-    arity::two_powers,
-    utils::{dependent_array::CheckedArray, operation::Operation, upcast::UpcastFrom},
-};
-
-use super::{
-    evaluation::Evaluable,
-    notation::FunctionNotation,
-    truth_table::{Row, TruthTable},
-};
+use super::{evaluation::Evaluable, notation::FunctionNotation};
 
 #[auto_impl::auto_impl(&, Box)]
 /// Enables the ability to combine propositional [`Evaluable`] into a single one.
@@ -61,73 +50,9 @@ where
 }
 
 /// Special case of [`TruthFn`] dealing with plain `bool` values.
-pub trait BoolFn<const ARITY: usize>: TruthFn<ARITY, bool> {
-    /// Generate a [truth table](https://en.wikipedia.org/wiki/Truth_table)
-    /// for a [`BoolFn`] as the **key** (boolean arguments)-**value** (function result)
-    /// ordered map.
-    fn get_truth_table(&self) -> TruthTable<ARITY>
-    where
-        two_powers::D: CheckedArray<ARITY>;
-}
+pub trait BoolFn<const ARITY: usize>: TruthFn<ARITY, bool> {}
 
-/// Use [`TruthTable`] to determine if two functions are equivalent.
-///
-/// Separated from the [parent trait][BoolFn] to allow for the latter
-/// to be dyn-compatible.
-pub trait EquivalentBoolFn<const ARITY: usize>: BoolFn<ARITY> {
-    /// Checks whether the two functions are equivalent.
-    fn is_equivalent<Rhs>(&self, other: &Rhs) -> bool
-    where
-        Rhs: BoolFn<ARITY>;
-}
-
-impl<const ARITY: usize, F> EquivalentBoolFn<ARITY> for F
-where
-    F: BoolFn<ARITY>,
-    two_powers::D: CheckedArray<ARITY>,
-{
-    fn is_equivalent<Rhs>(&self, other: &Rhs) -> bool
-    where
-        Rhs: BoolFn<ARITY>,
-    {
-        self.get_truth_table().into_values() == other.get_truth_table().into_values()
-    }
-}
-
-impl<const ARITY: usize, T> BoolFn<ARITY> for T
-where
-    T: TruthFn<ARITY, bool>,
-{
-    fn get_truth_table(&self) -> TruthTable<ARITY>
-    where
-        two_powers::D: CheckedArray<ARITY>,
-    {
-        let table: Map<_, _> = iter::repeat([false, true])
-            .take(ARITY)
-            .multi_cartesian_product()
-            .map(|assignment| {
-                let assignment = assignment
-                    .try_into()
-                    .expect("The array size is guaranteed by Itertools::multi_cartesian_product");
-                (assignment, self.compose(assignment))
-            })
-            .collect();
-
-        let table = if ARITY == 0 {
-            assert!(table.is_empty());
-            let dummy_empty_array = [false; ARITY];
-            let row: Row<ARITY> = (dummy_empty_array, self.compose(dummy_empty_array));
-            vec![row]
-        } else {
-            table.into_iter().collect()
-        };
-
-        assert_eq!(table.len(), 1 << ARITY);
-        table
-            .try_into()
-            .map_or_else(|_| panic!("Size checked before"), TruthTable::new)
-    }
-}
+impl<const ARITY: usize, T> BoolFn<ARITY> for T where T: TruthFn<ARITY, bool> {}
 
 #[auto_impl::auto_impl(&, Box)]
 /// A [logical constant](https://en.wikipedia.org/wiki/Logical_constant)