symbolic_sets_integers/

lib.rs

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

//! Provides examples and test cases for the [`symbolic-sets`][symbolic_sets] crate.

use std::fmt::Debug;
use std::fmt::Display;

use bitvec::BitArr;
use symbolic_sets::anf::AnfSet;
use symbolic_sets::anf::Simplifiable;
use symbolic_sets::anf::Simplification;
use symbolic_sets::Property;

// Note: ARRAY_SIZE isn't that large, so we could easily implement these sets exhaustively using a
// bitvec.  But we are purposefully doing it via a variety of different Property implementations to
// test that the ANF logic works as expected.

/// The number of elements that can be stored in a test set
const ARRAY_SIZE: usize = 1024;

/// An [`AnfSet`] that can store integers up to a certain size
pub type TestSet = AnfSet<TestProperty>;

/// A [`BitArray`][bitvec::array::BitArray] that can exhaustively store all of the integers in a
/// test set.
pub type TestArray = BitArr!(for ARRAY_SIZE);

/// An extension trait that adds useful methods to a [`TestSet`].
pub trait TestSetExt {
    /// Returns an exhaustive list of all of the elements in a test set as a [`TestArray`].
    fn to_array(&self) -> TestArray;

    /// Returns a test set containing only a single integer.
    fn only(element: u16) -> TestSet;

    /// Returns a test set containing all even integers.
    fn is_even() -> TestSet;

    /// Returns a test set containing all integers greater than a particular value.
    fn greater_than(element: u16) -> TestSet;
}

impl TestSetExt for TestSet {
    fn to_array(&self) -> TestArray {
        let mut result = TestArray::ZERO;
        if self.includes_universe() {
            result = !result;
        }
        for clause in self.clauses() {
            let mut clause_bits = !TestArray::ZERO;
            for property in clause {
                clause_bits &= property.to_array();
            }
            result ^= clause_bits;
        }
        result
    }

    fn only(element: u16) -> TestSet {
        TestProperty::from(SingleNumber(element)).into()
    }

    fn is_even() -> TestSet {
        TestProperty::from(IsEven).into()
    }

    fn greater_than(element: u16) -> TestSet {
        TestProperty::from(GreaterThan(element)).into()
    }
}

#[doc(hidden)]
#[derive(Clone, Eq, Ord, PartialEq, PartialOrd)]
pub enum TestProperty {
    SingleNumber(SingleNumber),
    IsEven(IsEven),
    GreaterThan(GreaterThan),
}

impl TestProperty {
    fn to_array(&self) -> TestArray {
        match self {
            TestProperty::SingleNumber(prop) => prop.to_array(),
            TestProperty::IsEven(prop) => prop.to_array(),
            TestProperty::GreaterThan(prop) => prop.to_array(),
        }
    }

    fn contains(&self, element: u16) -> bool {
        match self {
            TestProperty::SingleNumber(prop) => prop.is_satisfied(element),
            TestProperty::IsEven(prop) => prop.is_satisfied(element),
            TestProperty::GreaterThan(prop) => prop.is_satisfied(element),
        }
    }
}

impl Debug for TestProperty {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            TestProperty::SingleNumber(prop) => write!(f, "{:?}", prop),
            TestProperty::IsEven(prop) => write!(f, "{:?}", prop),
            TestProperty::GreaterThan(prop) => write!(f, "{:?}", prop),
        }
    }
}

impl Display for TestProperty {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            TestProperty::SingleNumber(prop) => write!(f, "{}", prop),
            TestProperty::IsEven(prop) => write!(f, "{}", prop),
            TestProperty::GreaterThan(prop) => write!(f, "{}", prop),
        }
    }
}

impl Property for TestProperty {
    type Element = u16;

    fn is_satisfied(&self, element: &u16) -> bool {
        self.contains(*element)
    }
}

impl Simplifiable for TestProperty {
    fn intersection(self, other: Self) -> Simplification<Self> {
        if self < other {
            self.intersection_ordered(other)
        } else {
            other.intersection_ordered(self)
        }
    }

    fn symmetric_difference(self, other: Self) -> Simplification<Self> {
        if self < other {
            self.symmetric_difference_ordered(other)
        } else {
            other.symmetric_difference_ordered(self)
        }
    }
}

impl TestProperty {
    fn intersection_ordered(self, other: Self) -> Simplification<Self> {
        match self {
            TestProperty::SingleNumber(prop) => prop.intersection_ordered(other),
            TestProperty::IsEven(prop) => prop.intersection_ordered(other),
            TestProperty::GreaterThan(prop) => prop.intersection_ordered(other),
        }
    }

    fn symmetric_difference_ordered(self, other: Self) -> Simplification<Self> {
        match self {
            TestProperty::SingleNumber(prop) => prop.symmetric_difference_ordered(other),
            TestProperty::IsEven(prop) => prop.symmetric_difference_ordered(other),
            TestProperty::GreaterThan(prop) => prop.symmetric_difference_ordered(other),
        }
    }
}

//-------------------------------------------------------------------------------------------------
// Property: Equals a single number

#[doc(hidden)]
#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
pub struct SingleNumber(u16);

impl From<SingleNumber> for TestProperty {
    fn from(prop: SingleNumber) -> TestProperty {
        TestProperty::SingleNumber(prop)
    }
}

impl SingleNumber {
    fn to_array(self) -> TestArray {
        let mut result = TestArray::ZERO;
        result.set(self.0 as usize, true);
        result
    }

    fn is_satisfied(self, element: u16) -> bool {
        self.0 == element
    }

    fn intersection_ordered(self, other: TestProperty) -> Simplification<TestProperty> {
        // This handles all other property types correctly:
        if other.contains(self.0) {
            // (i ∩ A) == i where i ∈ A
            return Simplification::Replace(self.into());
        }
        // (i ∩ A) == ∅ where i ∉ A
        Simplification::Remove
    }

    fn symmetric_difference_ordered(self, other: TestProperty) -> Simplification<TestProperty> {
        // (i ⊕ i) has already been handled by the caller
        // (i ⊕ j) cannot be simplified
        // (i ⊕ even) cannot be simplified
        // (i ⊕ >j) cannot be simplified
        Simplification::Keep(self.into(), other)
    }
}

impl Display for SingleNumber {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}

//-------------------------------------------------------------------------------------------------
// Property: Number is even

#[doc(hidden)]
#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
pub struct IsEven;

impl From<IsEven> for TestProperty {
    fn from(prop: IsEven) -> TestProperty {
        TestProperty::IsEven(prop)
    }
}

impl IsEven {
    fn to_array(self) -> TestArray {
        let mut result = TestArray::ZERO;
        for i in (0..ARRAY_SIZE).step_by(2) {
            result.set(i, true);
        }
        result
    }

    fn is_satisfied(self, element: u16) -> bool {
        (element % 2) == 0
    }

    fn intersection_ordered(self, other: TestProperty) -> Simplification<TestProperty> {
        // (even ∩ i) is out of order and will be called reversed
        // (even ∩ even) has already been handled by the caller
        // (even ∩ >i) can't be simplified
        Simplification::Keep(self.into(), other)
    }

    fn symmetric_difference_ordered(self, other: TestProperty) -> Simplification<TestProperty> {
        // (even ⊕ i) is out of order and will be called reversed
        // (even ⊕ even) has already been handled by the caller
        // (even ⊕ >i) can't be simplified
        Simplification::Keep(self.into(), other)
    }
}

impl Display for IsEven {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "even")
    }
}

//-------------------------------------------------------------------------------------------------
// Property: Greater than

#[doc(hidden)]
#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
pub struct GreaterThan(u16);

impl From<GreaterThan> for TestProperty {
    fn from(prop: GreaterThan) -> TestProperty {
        TestProperty::GreaterThan(prop)
    }
}

impl GreaterThan {
    fn to_array(self) -> TestArray {
        let mut result = TestArray::ZERO;
        for i in (self.0 as usize + 1)..ARRAY_SIZE {
            result.set(i, true);
        }
        result
    }

    fn is_satisfied(self, element: u16) -> bool {
        element > self.0
    }

    fn intersection_ordered(self, other: TestProperty) -> Simplification<TestProperty> {
        // (>i ∩ j) is out of order and will be called reversed
        // (>i ∩ even) is out of order and will be called reversed
        // (>i ∩ >i) has already been handled by the caller

        match other {
            TestProperty::GreaterThan(other) => {
                // (>i ∩ >j) == >max(i,j)
                if self.0 > other.0 {
                    Simplification::Replace(self.into())
                } else {
                    Simplification::Replace(other.into())
                }
            }

            _ => Simplification::Remove,
        }
    }

    fn symmetric_difference_ordered(self, other: TestProperty) -> Simplification<TestProperty> {
        // (>i ⊕ j) is out of order and will be called reversed
        // (>i ⊕ even) is out of order and will be called reversed
        // (>i ⊕ >i) has already been handled by the caller
        // (>i ⊕ >j) cannot be simplified
        Simplification::Keep(self.into(), other)
    }
}

impl Display for GreaterThan {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, ">{}", self.0)
    }
}

//-------------------------------------------------------------------------------------------------
// Tests

mod proptest_support {
    use super::*;

    use std::ops::Range;

    use proptest::prelude::*;
    use proptest::strategy::Map;
    use symbolic_sets::proptest::ArbitraryElement;

    impl Arbitrary for SingleNumber {
        type Parameters = ();
        type Strategy = Map<Range<u16>, fn(u16) -> SingleNumber>;
        fn arbitrary_with(_args: Self::Parameters) -> Self::Strategy {
            (0..ARRAY_SIZE as u16).prop_map(SingleNumber)
        }
    }

    impl Arbitrary for IsEven {
        type Parameters = ();
        type Strategy = Just<IsEven>;
        fn arbitrary_with(_args: Self::Parameters) -> Self::Strategy {
            Just(IsEven)
        }
    }

    impl Arbitrary for GreaterThan {
        type Parameters = ();
        type Strategy = Map<Range<u16>, fn(u16) -> GreaterThan>;
        fn arbitrary_with(_args: Self::Parameters) -> Self::Strategy {
            (0..ARRAY_SIZE as u16).prop_map(GreaterThan)
        }
    }

    impl Arbitrary for TestProperty {
        type Parameters = ();
        type Strategy = BoxedStrategy<TestProperty>;
        fn arbitrary_with(_args: Self::Parameters) -> Self::Strategy {
            prop_oneof![
                any::<SingleNumber>().prop_map_into(), //
                any::<IsEven>().prop_map_into(),
                any::<GreaterThan>().prop_map_into(),
            ]
            .boxed()
        }
    }

    impl ArbitraryElement for TestProperty {
        type Element = u16;
        type Strategy = BoxedStrategy<u16>;
        fn arbitrary_element(set: &TestSet) -> Self::Strategy {
            let elements = set.to_array();
            let size = elements.count_ones();
            (0..size)
                .prop_map(move |idx| {
                    elements
                        .iter_ones()
                        .nth(idx)
                        .expect("Index should be valid") as u16
                })
                .boxed()
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    symbolic_sets::test_anf_set!(TestProperty);
    symbolic_sets::test_anf_set_with_elements!(TestProperty);
}