symbolic-sets 0.1.0

// -*- coding: utf-8 -*-
//-------------------------------------------------------------------------------------------------
// SPDX-FileCopyrightText: © 2024 Walland Heavy Research
// SPDX-License-Identifier: AGPL-3.0-only
//-------------------------------------------------------------------------------------------------

//! Sets stored in [Algebraic Normal Form] (ANF)
//!
//! In ANF, each set is stored as the symmetric difference of intersections (or in boolean terms,
//! as the XOR of ANDs).
//!
//! [Algebraic Normal Form]: https://en.wikipedia.org/wiki/Algebraic_normal_form

use std::collections::BTreeSet;
use std::fmt::Debug;
use std::fmt::Display;

use crate::Property;

/// A set of elements stored in algebraic normal form.
///
/// `P` defines properties that may be true or false for each possible element of the set.  A set
/// is then the XOR of zero or more clauses, each of which is the AND of one or more properties.
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct AnfSet<P> {
    negated: bool,
    clauses: BTreeSet<Clause<P>>,
}

/// A single clause in an ANF set. It is the intersection of one or more properties.
#[derive(Clone, Eq, Ord, PartialEq, PartialOrd)]
struct Clause<P> {
    properties: BTreeSet<P>,
}

impl<P> AnfSet<P> {
    /// Returns a set that contains no elements.
    pub fn empty() -> Self {
        Self {
            negated: false,
            clauses: BTreeSet::new(),
        }
    }

    /// Returns a set that contains every possible element.
    pub fn universe() -> Self {
        Self {
            negated: true,
            clauses: BTreeSet::new(),
        }
    }
}

impl<P> From<P> for AnfSet<P>
where
    P: Ord,
{
    fn from(property: P) -> Self {
        let mut clauses = BTreeSet::new();
        clauses.insert(property.into());
        Self {
            negated: false,
            clauses,
        }
    }
}

impl<P> From<P> for Clause<P>
where
    P: Ord,
{
    fn from(property: P) -> Self {
        let mut properties = BTreeSet::new();
        properties.insert(property);
        Self { properties }
    }
}

impl<P> AnfSet<P> {
    /// Returns whether the set contains no elements.
    pub fn is_empty(&self) -> bool {
        !self.negated && self.clauses.is_empty()
    }

    /// Returns whether the set includes the universe (the set containing all possible elements) as
    /// one of its clauses.  (In ANF terms, this is whether the set includes `1⊕...` as one of its
    /// terms.)
    pub fn includes_universe(&self) -> bool {
        self.negated
    }

    /// Returns an iterator of the clauses in the set.
    pub fn clauses(&self) -> impl Iterator<Item = impl Iterator<Item = &P>> + '_ {
        self.clauses.iter().map(|c| c.properties.iter())
    }

    /// Negates the set, so that it contains only those elements that it did not contain before the
    /// call.
    pub fn negate(&mut self) {
        self.negated = !self.negated;
    }
}

impl<P> AnfSet<P>
where
    P: Property,
{
    /// Returns whether the set contains a particular element.
    pub fn contains(&self, element: &P::Element) -> bool {
        let mut result = self.negated;
        for clause in &self.clauses {
            result = result != clause.properties.iter().all(|p| p.is_satisfied(element))
        }
        result
    }
}

impl<P> Debug for Clause<P>
where
    P: Debug,
{
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        // Special-case: Ignore the pretty-print alternate format if there's only one property.
        if self.properties.len() == 1 {
            return write!(
                f,
                "Clause({:?})",
                &self.properties.iter().next().expect("Inconsistent length")
            );
        }

        let mut tuple = f.debug_tuple("Clause");
        for property in &self.properties {
            tuple.field(property);
        }
        tuple.finish()
    }
}

impl<P> Display for AnfSet<P>
where
    P: Display,
{
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        let mut first = true;
        if self.negated {
            first = false;
            write!(f, "1")?;
        }
        for clause in &self.clauses {
            if first {
                first = false;
            } else {
                write!(f, " ⊕ ")?;
            }
            write!(f, "{}", clause)?;
        }
        if first {
            write!(f, "∅")?;
        }
        Ok(())
    }
}

impl<P> Display for Clause<P>
where
    P: Display,
{
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        let mut first = true;
        write!(f, "(")?;
        for property in &self.properties {
            if first {
                first = false;
            } else {
                write!(f, " ∩ ")?;
            }
            write!(f, "{}", property)?;
        }
        write!(f, ")")?;
        Ok(())
    }
}

impl<P> std::ops::BitAnd for AnfSet<P>
where
    P: Clone + Eq + Ord + Simplifiable,
{
    type Output = Self;

    fn bitand(self, rhs: Self) -> Self::Output {
        let lhs = self;
        let mut result = AnfSet::empty();

        // (0/1 ⊕ ...) ∩ (0/1 ⊕ ...) = (0/1 ∩ 0/1) ⊕ ...
        result.negated = lhs.negated && rhs.negated;

        // (1 ⊕ ...) ∩ (... ⊕ R₀ ⊕ R₁ ⊕ ...) = 1(... ⊕ R₀ ⊕ R₁ ⊕ ...) ⊕ ...
        //                                   = (... ⊕ R₀ ⊕ R₁ ⊕ ...) ⊕ ...
        if lhs.negated {
            for rc in &rhs.clauses {
                result.add_clause(rc.clone());
            }
        }

        // (... ⊕ L₀ ⊕ L₁ ⊕ ...) ∩ (1 ⊕ ...) = (... ⊕ L₀ ⊕ L₁ ⊕ ...)1 ⊕ ...
        //                                   = (... ⊕ L₀ ⊕ L₁ ⊕ ...) ⊕ ...
        if rhs.negated {
            for lc in &lhs.clauses {
                result.add_clause(lc.clone());
            }
        }

        // (... ⊕ L₀ ⊕ L₁ ⊕ ...) ∩ (... ⊕ R₀ ⊕ R₁ ⊕ ...) = ... ⊕ (L₀ ∩ R₀) ⊕ (L₀ ∩ R₁) ⊕ (L₁ ∩ R₀) ⊕ (L₁ ∩ R₁) ⊕ ...
        for lc in &lhs.clauses {
            for rc in &rhs.clauses {
                if let Some(ic) = lc.intersection(rc) {
                    result.add_clause(ic);
                }
            }
        }

        result
    }
}

impl<P> std::ops::BitAndAssign for AnfSet<P>
where
    P: Clone + Eq + Ord + Simplifiable,
{
    fn bitand_assign(&mut self, rhs: Self) {
        let lhs = std::mem::replace(self, AnfSet::empty());
        *self = lhs & rhs;
    }
}

impl<P> std::ops::BitOr for AnfSet<P>
where
    P: Clone + Eq + Ord + Simplifiable,
{
    type Output = Self;

    fn bitor(self, rhs: Self) -> Self::Output {
        // L ∪ R = L ⊕ R ⊕ (L ∩ R)
        let lhs = self;
        let mut result = AnfSet::empty();

        // negated?
        // lhs  rhs
        // --------
        //  0    0   (0⊕...) ⊕ (0⊕...) ⊕ (0⊕...)(0⊕...) → (0⊕0⊕0)... → 0...
        //  0    1   (0⊕...) ⊕ (1⊕...) ⊕ (0⊕...)(1⊕...) → (0⊕1⊕0)... → 1...
        //  1    0   (1⊕...) ⊕ (0⊕...) ⊕ (1⊕...)(0⊕...) → (1⊕0⊕0)... → 1...
        //  1    1   (1⊕...) ⊕ (1⊕...) ⊕ (1⊕...)(1⊕...) → (1⊕1⊕1)... → 1...
        result.negated = lhs.negated || rhs.negated;

        // L ∪ R = L ⊕ ...
        result.clauses = lhs.clauses.clone();

        // L ∪ R = ... ⊕ R ⊕ ...
        for rc in &rhs.clauses {
            result.add_clause(rc.clone());
        }

        // L ∪ R = ... ⊕ (L ∩ R)
        if lhs.negated {
            // (1 ⊕ ...) ∩ (R₀ ⊕ R₁ ⊕ ...) = 1(R₀ ⊕ R₁ ⊕ ...) ⊕ ...
            //                             = (R₀ ⊕ R₁ ⊕ ...) ⊕ ...
            for rc in &rhs.clauses {
                result.add_clause(rc.clone());
            }
        }
        if rhs.negated {
            // Ditto above
            for lc in &lhs.clauses {
                result.add_clause(lc.clone());
            }
        }
        for lc in &lhs.clauses {
            for rc in &rhs.clauses {
                if let Some(ic) = lc.intersection(rc) {
                    result.add_clause(ic);
                }
            }
        }

        result
    }
}

impl<P> std::ops::BitOrAssign for AnfSet<P>
where
    P: Clone + Eq + Ord + Simplifiable,
{
    fn bitor_assign(&mut self, rhs: Self) {
        let lhs = std::mem::replace(self, AnfSet::empty());
        *self = lhs | rhs;
    }
}

impl<P> std::ops::BitXor for AnfSet<P>
where
    P: Eq + Ord + Simplifiable,
{
    type Output = Self;

    fn bitxor(mut self, rhs: Self) -> Self::Output {
        self ^= rhs;
        self
    }
}

impl<P> std::ops::BitXorAssign for AnfSet<P>
where
    P: Eq + Ord + Simplifiable,
{
    fn bitxor_assign(&mut self, rhs: Self) {
        // Naively, the result is just the concatenation of each set's clause list, but we also
        // need to make sure that the result is simplified fully. Both lhs and rhs come in
        // simplified individually.  So we use use add_clause to add each of rhs's clauses one by
        // one, simplifying as much as we can each step.  Because
        // [Simplifiable.symmetric_difference] must be confluent, we should get the same result no
        // matter what order we process the clauses in.
        self.negated = self.negated != rhs.negated;
        for rc in rhs.clauses {
            self.add_clause(rc);
        }
    }
}

impl<P> std::ops::Not for AnfSet<P> {
    type Output = Self;

    fn not(mut self) -> Self::Output {
        self.negated = !self.negated;
        self
    }
}

impl<P> std::ops::Sub for AnfSet<P>
where
    P: Clone + Eq + Ord + Simplifiable,
{
    type Output = Self;

    fn sub(self, other: Self) -> Self::Output {
        self & !other
    }
}

impl<P> std::ops::SubAssign for AnfSet<P>
where
    P: Clone + Eq + Ord + Simplifiable,
{
    fn sub_assign(&mut self, other: Self) {
        *self &= !other;
    }
}

impl<P> AnfSet<P>
where
    P: Eq + Ord + Simplifiable,
{
    fn add_clause(&mut self, mut clause: Clause<P>) {
        let prev = std::mem::take(&mut self.clauses);
        let mut clauses = prev.into_iter();
        while let Some(lc) = clauses.next() {
            match lc.symmetric_difference(clause) {
                Simplification::Remove => {
                    // If two clauses cancel out via XOR, that does NOT cause the entire set to
                    // become ∅.  We need to keep whatever clauses have already been added to the
                    // result, and also need to copy over any later clauses that we hadn't
                    // processed yet.
                    self.clauses.extend(clauses);
                    return;
                }

                Simplification::Keep(lc, c) => {
                    // We couldn't simplify relative to lc, so add lc to the result.  Continue
                    // trying to simplify clause against the later clauses in the set.
                    self.clauses.insert(lc);
                    clause = c;
                }

                Simplification::Replace(c) => {
                    // We were able to simplify relative to lc.  Don't add it to the result yet;
                    // instead, try to simplify the result further against later clauses in s.
                    clause = c;
                }
            }
        }

        // If we fall through then we need to add clause to the clause list (either because we
        // couldn't simplify it with anything, or because we did without it canceling out).
        self.clauses.insert(clause);
    }
}

impl<P> Clause<P>
where
    P: Eq + Ord + Simplifiable,
{
    /// Returns the symmetric difference of two clauses.
    fn symmetric_difference(mut self, mut other: Clause<P>) -> Simplification<Clause<P>> {
        // If both clauses contain exactly the same set of properties, then they
        // cancel each other out.
        if self.properties == other.properties {
            return Simplification::Remove;
        }

        // If both clauses contain a single property, we use their
        // symmetric_difference implementation to simplify them.
        if self.properties.len() == 1 && other.properties.len() == 1 {
            let lp = self
                .properties
                .pop_first()
                .expect("Properties has length 1");
            let rp = other
                .properties
                .pop_first()
                .expect("Properties has length 1");
            return lp.symmetric_difference(rp).into();
        }

        // Otherwise we assume that they cannot be simplified further.
        Simplification::Keep(self, other)
    }

    /// Adds an additional property to a clause, simplifying it to retain the “pairwise simplified”
    /// invariant.  Returns None if the result is an empty clause.
    fn add_property(&mut self, mut property: P) -> Option<()> {
        let prev = std::mem::take(&mut self.properties);
        let properties = prev.into_iter();
        for lp in properties {
            match lp.intersection(property) {
                Simplification::Remove => {
                    // The intersection of any two properties being ∅ causes the whole
                    // clause to become ∅.
                    return None;
                }

                Simplification::Keep(lp, p) => {
                    // We couldn't simplify relative to lp, so add lp to the result.  Continue
                    // trying to simplify `property` against the later properties in the set.
                    self.properties.insert(lp);
                    property = p;
                }

                Simplification::Replace(p) => {
                    // We were able to simplify relative to lp.  Don't add it to the result yet;
                    // instead, try to simplify the result further against later properties in
                    // self.
                    property = p;
                }
            }
        }

        // If we fall through then we need to add `property` to the result (either because we
        // couldn't simplify it with anything, or because we did without it canceling out).
        self.properties.insert(property);
        Some(())
    }
}

impl<P> Clause<P>
where
    P: Clone + Eq + Ord + Simplifiable,
{
    /// Returns the intersection of two clauses, or None if the intersection is empty.
    fn intersection(&self, other: &Clause<P>) -> Option<Clause<P>> {
        // Naively, the result is just the concatenation of each clause's property list, but we
        // also need to make sure that the result is simplified fully. Both self and other come in
        // simplified individually.  So we start with a copy of self's properties, and then use
        // add_property to add each of other's properties one by one, simplifying as much as we can
        // each step.  Because [Simplifiable::intersection] must be confluent, we should get the
        // same result (modulo reordering) no matter what order we process the properties in.
        let mut result = self.clone();
        for rp in &other.properties {
            result.add_property(rp.clone())?;
        }
        Some(result)
    }
}

/// Defines how to simplify properties that are used for ANF sets.
///
/// Implementations must be:
///
///   - Symmetric: `p1.intersection(p2)` and `p2.intersection(p1)` must return the same result.
///     (Ditto for `symmetric_difference`)
///
///   - Confluent: Given any number of properties, calling `intersection` or `symmetric_difference`
///     on them in any order must produce an equivalent result.
pub trait Simplifiable: Sized {
    /// Determines whether the intersection of this property and another is empty; and if not,
    /// whether it can be represented by a different, simpler, property instance.
    ///
    /// If the two properties are disjoint, then their intersection is empty. In that case, return
    /// [`Remove`][Simplification::Remove].
    ///
    /// If the intersection is non-empty, and there is a simpler, single property instance that
    /// contains EXACTLY the same elements as the intersection, return
    /// [`Replace`][Simplification::Replace] containing the simplified property.  If not (that is,
    /// the two existing property instances are the best representation of their intersection),
    /// then return [`Keep`][Simplification::Keep].
    ///
    /// As a common case of the above, we will test ourselves whether the two properties are equal,
    /// in which case they will be replaced with a single copy of the property.  You do not have to
    /// test for that situation.
    fn intersection(self, other: Self) -> Simplification<Self>;

    /// Determines whether the symmetric difference of this property and another is empty; and if
    /// not, whether it can be represented by a different, simpler, property instance.
    ///
    /// If the two properties are equivalent, then their symmetric difference is empty. In that
    /// case, return [`Remove`][Simplification::Remove].
    ///
    /// If the symmetric difference is non-empty, and there is a simpler, single property instance
    /// that contains EXACTLY the same elements as the symmetric difference, return
    /// [`Replace`][Simplification::Replace] containing the simplified property.  If not (that is,
    /// the two existing property instances are the best representation of their symmetric
    /// difference), then return [`Keep`][Simplification::Keep].
    ///
    /// As a common case of the above, we will test ourselves whether the two properties are equal,
    /// in which case they will be removed.  You do not have to test for that situation.
    fn symmetric_difference(self, other: Self) -> Simplification<Self>;
}

/// Indicates what kind of result is returned from [`intersection`][Simplifiable::intersection] and
/// [`symmetric_difference`][Simplifiable::symmetric_difference].
pub enum Simplification<P> {
    /// Indicates that the two properties being simplified cancel each other out and should both be
    /// removed.
    Remove,
    /// Indicates that the two properties cannot be simplified, and should be kept as-is.
    Keep(P, P),
    /// Indicates that the two properties can be simplified, and should collectively be replaced
    /// with a different property.
    Replace(P),
}

impl<P> From<Simplification<P>> for Simplification<Clause<P>>
where
    P: Ord,
{
    fn from(p: Simplification<P>) -> Self {
        match p {
            Simplification::Remove => Simplification::Remove,
            Simplification::Keep(f1, f2) => Simplification::Keep(f1.into(), f2.into()),
            Simplification::Replace(f) => Simplification::Replace(f.into()),
        }
    }
}