libreda-logic 0.0.3

// SPDX-FileCopyrightText: 2022 Thomas Kramer <code@tkramer.ch>
//
// SPDX-License-Identifier: AGPL-3.0-or-later

//! Abstractions for different representations of boolean formulas.
//! Defines how different types of boolean functions/formulas can be accessed and manipulated.

use std::hash::Hash;

/// Trait used for identifier types.
pub trait IdType:
    Copy + Clone + PartialEq + Eq + Hash + PartialOrd + Ord + Send + Sync + 'static
{
}

/// Blanket implementation.
impl<T> IdType for T where
    T: Copy + Clone + PartialEq + Eq + Hash + PartialOrd + Ord + Send + Sync + 'static
{
}

/// Define the number of function arguments.
pub trait NumInputs {
    /// Get the number of inputs of the boolean function.
    fn num_inputs(&self) -> usize;
}

/// Define the number of function outputs.
pub trait NumOutputs {
    /// Get the number of outputs of the boolean function.
    fn num_outputs(&self) -> usize;
}

/// Generic ways to access and query a set of partially specified boolean formulas.
pub trait PartialBooleanSystem: NumInputs + NumOutputs {
    /// An identifier for an input of the boolean formula.
    type LiteralId: IdType;
    /// An identifier of an intermediate value or output.
    type TermId: IdType;

    /// Compute the value of the `term`.
    /// The values of all needed literals must be defined by the `input_values` function.
    /// Returns `None` if the value is not specified for the given inputs.
    fn evaluate_term_partial(&self, term: &Self::TermId, input_values: &[bool]) -> Option<bool>;

    //fn evaluate_term_partial_with_context(
    //    &self,
    //    term: &Self::TermId,
    //    input_values: &impl Fn(Self::LiteralId) -> bool,
    //) -> Option<bool>;
}

/// Define positions of input variables such that they can be
/// adressed with an index.
pub trait PositionalInputs: NumInputs {
    /// ID type used for input variables.
    type InputId: IdType;

    /// Find the input variable at the given position.
    /// Returns `None` if there's no variable at the position.
    fn get_input_var(&self, position: usize) -> Option<Self::InputId>;

    /// Find the first position of an input variable.
    fn find_input_position(&self, input_id: &Self::InputId) -> Option<usize> {
        (0..self.num_inputs()).find(|&i| self.get_input_var(i).as_ref() == Some(input_id))
    }
}

/// A set of fully specified boolean formulas.
pub trait BooleanSystem: PartialBooleanSystem {
    /// Compute the value of the `term`.
    /// The values of all needed literals must be defined by the `input_values` function.
    fn evaluate_term(&self, term: &Self::TermId, input_values: &[bool]) -> bool;
}

/// Special case of a boolean system with exactly one output.
pub trait PartialBooleanFunction: PartialBooleanSystem + StaticNumOutputs<1> {
    /// Evaluate the boolean function with the given input values.
    fn partial_eval(&self, input_values: &[bool]) -> Option<bool>;
}

/// Special case of a boolean system with exactly one output.
pub trait BooleanFunction: PartialBooleanFunction {
    /// Evaluate the boolean function with the given input values.
    fn eval(&self, input_values: &[bool]) -> bool;
}

/// Number of inputs known at compile time.
pub trait StaticNumInputs<const NUM_INPUTS: usize> {}

/// Number of outputs known at compile time.
pub trait StaticNumOutputs<const NUM_OUTPUTS: usize> {}

/// Generic ways how a boolean system can be modified.
pub trait BooleanSystemEdit: BooleanSystem {
    // TODO
}

/// Marker trait for functions which are partially commutative.
///
/// Partially commutative means that the function inputs can be grouped into disjoint sets. Within each set of inputs, the inputs can be reordered
/// without changing the function. Trivially, every function is partially commutative when grouping each input into it's own set.
pub trait StaticPartialComutative<const NUM_INPUTS: usize> {
    /// Set indices for each input.
    ///
    /// Example: A function `f` with `f(a, b, c, d) == f(b, a, c, d)` would have `COMMUTATIVE_INPUTS = [0, 0, 1, 2]`.
    const COMMUTATIVE_INPUTS: [usize; NUM_INPUTS];
}

/// Marker trait for commutative functions.
///
/// Boolean systems implementing this trait are invariant under permutations of the inputs.
pub trait StaticCommutative {}

/// TODO
pub trait ArithmeticProperties {
    /// Check if the boolean function is commutative.
    fn is_commutative(&self) -> bool;
}

/// Abstraction of logic values.
pub trait LogicValue: Copy + Clone + PartialEq + Eq + Hash + 'static {
    /// Get number of different values that this type can have.
    fn num_values() -> usize;

    /// List of possible logic values.
    fn value(idx: usize) -> Self;

    /// Additive neutral element.
    fn zero() -> Self;

    /// Multiplicative neutral element.
    fn one() -> Self;
}

/// Binary logic operations for logic types such as `bool` or `Logic3`.
pub trait LogicOps:
    Sized + std::ops::Not + std::ops::BitAnd + std::ops::BitOr + std::ops::BitXor
{
}

impl<T> LogicOps for T where
    T: Sized + std::ops::Not + std::ops::BitAnd + std::ops::BitOr + std::ops::BitXor
{
}