libreda_logic/
traits.rs

1// SPDX-FileCopyrightText: 2022 Thomas Kramer <code@tkramer.ch>
2//
3// SPDX-License-Identifier: AGPL-3.0-or-later
4
5//! Abstractions for different representations of boolean formulas.
6//! Defines how different types of boolean functions/formulas can be accessed and manipulated.
7
8use std::hash::Hash;
9
10/// Trait used for identifier types.
11pub trait IdType:
12    Copy + Clone + PartialEq + Eq + Hash + PartialOrd + Ord + Send + Sync + 'static
13{
14}
15
16/// Blanket implementation.
17impl<T> IdType for T where
18    T: Copy + Clone + PartialEq + Eq + Hash + PartialOrd + Ord + Send + Sync + 'static
19{
20}
21
22/// Define the number of function arguments.
23pub trait NumInputs {
24    /// Get the number of inputs of the boolean function.
25    fn num_inputs(&self) -> usize;
26}
27
28/// Define the number of function outputs.
29pub trait NumOutputs {
30    /// Get the number of outputs of the boolean function.
31    fn num_outputs(&self) -> usize;
32}
33
34/// Generic ways to access and query a set of partially specified boolean formulas.
35pub trait PartialBooleanSystem: NumInputs + NumOutputs {
36    /// An identifier for an input of the boolean formula.
37    type LiteralId: IdType;
38    /// An identifier of an intermediate value or output.
39    type TermId: IdType;
40
41    /// Compute the value of the `term`.
42    /// The values of all needed literals must be defined by the `input_values` function.
43    /// Returns `None` if the value is not specified for the given inputs.
44    fn evaluate_term_partial(&self, term: &Self::TermId, input_values: &[bool]) -> Option<bool>;
45
46    //fn evaluate_term_partial_with_context(
47    //    &self,
48    //    term: &Self::TermId,
49    //    input_values: &impl Fn(Self::LiteralId) -> bool,
50    //) -> Option<bool>;
51}
52
53/// Define positions of input variables such that they can be
54/// adressed with an index.
55pub trait PositionalInputs: NumInputs {
56    /// ID type used for input variables.
57    type InputId: IdType;
58
59    /// Find the input variable at the given position.
60    /// Returns `None` if there's no variable at the position.
61    fn get_input_var(&self, position: usize) -> Option<Self::InputId>;
62
63    /// Find the first position of an input variable.
64    fn find_input_position(&self, input_id: &Self::InputId) -> Option<usize> {
65        (0..self.num_inputs()).find(|&i| self.get_input_var(i).as_ref() == Some(input_id))
66    }
67}
68
69/// A set of fully specified boolean formulas.
70pub trait BooleanSystem: PartialBooleanSystem {
71    /// Compute the value of the `term`.
72    /// The values of all needed literals must be defined by the `input_values` function.
73    fn evaluate_term(&self, term: &Self::TermId, input_values: &[bool]) -> bool;
74}
75
76/// Special case of a boolean system with exactly one output.
77pub trait PartialBooleanFunction: PartialBooleanSystem + StaticNumOutputs<1> {
78    /// Evaluate the boolean function with the given input values.
79    fn partial_eval(&self, input_values: &[bool]) -> Option<bool>;
80}
81
82/// Special case of a boolean system with exactly one output.
83pub trait BooleanFunction: PartialBooleanFunction {
84    /// Evaluate the boolean function with the given input values.
85    fn eval(&self, input_values: &[bool]) -> bool;
86}
87
88/// Number of inputs known at compile time.
89pub trait StaticNumInputs<const NUM_INPUTS: usize> {}
90
91/// Number of outputs known at compile time.
92pub trait StaticNumOutputs<const NUM_OUTPUTS: usize> {}
93
94/// Generic ways how a boolean system can be modified.
95pub trait BooleanSystemEdit: BooleanSystem {
96    // TODO
97}
98
99/// Marker trait for functions which are partially commutative.
100///
101/// Partially commutative means that the function inputs can be grouped into disjoint sets. Within each set of inputs, the inputs can be reordered
102/// without changing the function. Trivially, every function is partially commutative when grouping each input into it's own set.
103pub trait StaticPartialComutative<const NUM_INPUTS: usize> {
104    /// Set indices for each input.
105    ///
106    /// Example: A function `f` with `f(a, b, c, d) == f(b, a, c, d)` would have `COMMUTATIVE_INPUTS = [0, 0, 1, 2]`.
107    const COMMUTATIVE_INPUTS: [usize; NUM_INPUTS];
108}
109
110/// Marker trait for commutative functions.
111///
112/// Boolean systems implementing this trait are invariant under permutations of the inputs.
113pub trait StaticCommutative {}
114
115/// TODO
116pub trait ArithmeticProperties {
117    /// Check if the boolean function is commutative.
118    fn is_commutative(&self) -> bool;
119}
120
121/// Abstraction of logic values.
122pub trait LogicValue: Copy + Clone + PartialEq + Eq + Hash + 'static {
123    /// Get number of different values that this type can have.
124    fn num_values() -> usize;
125
126    /// List of possible logic values.
127    fn value(idx: usize) -> Self;
128
129    /// Additive neutral element.
130    fn zero() -> Self;
131
132    /// Multiplicative neutral element.
133    fn one() -> Self;
134}
135
136/// Binary logic operations for logic types such as `bool` or `Logic3`.
137pub trait LogicOps:
138    Sized + std::ops::Not + std::ops::BitAnd + std::ops::BitOr + std::ops::BitXor
139{
140}
141
142impl<T> LogicOps for T where
143    T: Sized + std::ops::Not + std::ops::BitAnd + std::ops::BitOr + std::ops::BitXor
144{
145}
libreda_logic/traits.rs

libreda_logic/
traits.rs
