symbolic-sets 0.1.0

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

//! Supports writing property tests that exercise set implementations.
//!
//! To use the set types in this crate, you must define a type that implements the
//! [`Property`][crate::Property] trait.  This type must satisfy certain laws for the rest of the
//! set implementation to be valid.  For instance, a property used in an
//! [`AnfSet`] must also provide a [`Simplifiable`][crate::anf::Simplifiable] implementation that
//! is _symmetric_ and _confluent_.
//!
//! It's very important that your property implementation actually satisfies these laws, since the
//! correctness of the rest of the set code depends on it!  To validate this, it's useful to use
//! [_property-based testing_][prop tests] to validate all of the various [set laws][] that all
//! sets must satisfy.
//!
//! This can be very tedious, so we provide some macros that define a full suite of property test
//! functions for you.  The end result is a test block that looks something like:
//!
//! ``` ignore
//! #[cfg(test)]
//! mod tests {
//!   symbolic_sets::test_anf_set!(YourProperty);
//!   symbolic_sets::test_anf_set_with_elements!(YourProperty);
//! }
//! ```
//!
//! [prop tests]: https://en.wikipedia.org/wiki/QuickCheck
//! [set laws]: https://en.wikipedia.org/wiki/List_of_set_identities_and_relations

use std::fmt::Debug;

use proptest::prelude::*;
use proptest::sample::SizeRange;

use crate::anf::AnfSet;
use crate::anf::Simplifiable;

impl<P> Arbitrary for AnfSet<P>
where
    P: Arbitrary + Clone + Eq + Into<AnfSet<P>> + Ord + Simplifiable + 'static,
{
    type Parameters = SizeRange;
    type Strategy = BoxedStrategy<Self>;
    fn arbitrary_with(args: Self::Parameters) -> Self::Strategy {
        proptest::collection::vec(any::<P>(), args)
            .prop_map(|properties| {
                properties
                    .into_iter()
                    .map(|property| property.into())
                    .fold(Self::empty(), |a, b| a | b)
            })
            .boxed()
    }
}

/// Implemented by properties that can generate a random element in a property test.
pub trait ArbitraryElement: Sized {
    type Element;
    type Strategy: Strategy<Value = Self::Element>;

    /// Returns a [`Strategy`] that generates a random element from the set.
    fn arbitrary_element(set: &AnfSet<Self>) -> Self::Strategy;
}

/// Implements [`Arbitrary`] to generate a set and an element of that set in property tests.
#[derive(Debug)]
pub struct SetAndElement<S, E> {
    pub set: S,
    pub element: E,
}

impl<P, E> Arbitrary for SetAndElement<AnfSet<P>, E>
where
    P: ArbitraryElement<Element = E>,
    AnfSet<P>: Arbitrary<Parameters = SizeRange> + Clone + Debug + 'static,
    E: Debug,
{
    type Parameters = ();
    type Strategy = BoxedStrategy<Self>;

    fn arbitrary_with(_args: Self::Parameters) -> Self::Strategy {
        any_with::<AnfSet<P>>((1..10).into())
            .prop_filter("nonempty set", |set| !set.is_empty())
            .prop_flat_map(move |set| {
                let element = P::arbitrary_element(&set);
                (Just(set), element)
            })
            .prop_map(|(set, element)| SetAndElement { set, element })
            .boxed()
    }
}

// The macros implemented below use some items from other crates.  Instead of asking each
// downstream user of the macros to add dependencies on those crates, we re-export the necessary
// items here, so that the macros can refer to them via `$crate`.
#[doc(hidden)]
pub use indoc::indoc as __indoc;
#[doc(hidden)]
pub use proptest_attr_macro::proptest as __proptest;

/// Defines a full suite of property tests that exercise an [`AnfSet`] implementation.
///
/// You must implement the [`Arbitrary`][proptest::arbitrary::Arbitrary] trait for your
/// [`Property`][crate::Property] implementation.  We will generate random instances of your set
/// and verify that all of the typical set laws hold.
///
/// _All_ property implementations include this test suite.  If any of these tests fail, it
/// indicates that your properties are not written correctly.  (In particular, your
/// [`Simplifiable`][crate::anf::Simplifiable] methods might not be symmetric and confluent.)
///
/// The [`test_anf_set_with_elements`][crate::test_anf_set_with_elements] macro defines some
/// additional tests that are only valid if you can easily choose a random element.
#[macro_export]
macro_rules! test_anf_set {
    ($typ:ty) => {
        #[$crate::proptest::__proptest]
        fn complement_distributes_over_symmetric_difference(
            a: $crate::anf::AnfSet<$typ>,
            b: $crate::anf::AnfSet<$typ>,
        ) {
            // A ⊕ B == !A ⊕ !B
            let lhs = a.clone() ^ b.clone();
            let rhs = !a.clone() ^ !b.clone();
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    and set B
                      {}
                    A ⊕ B
                      {}
                    and !A ⊕ !B
                      {}
                    should be equal"},
                a, b, lhs, rhs,
            );
        }

        #[$crate::proptest::__proptest]
        fn difference_annhilates(a: $crate::anf::AnfSet<$typ>) {
            // A ⊕ A = ∅
            let diff = a.clone() - a.clone();
            assert!(
                diff.is_empty(),
                $crate::proptest::__indoc! {"
                    Given set
                      {}
                    A \\ A
                      {}
                    should be empty"},
                a,
                diff,
            );
        }

        #[$crate::proptest::__proptest]
        fn difference_has_unit(a: $crate::anf::AnfSet<$typ>) {
            // A \ ∅ = A
            let lhs = a.clone();
            let rhs = a.clone() - $crate::anf::AnfSet::empty();
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    A \\ ∅
                      {}
                    should be the same"},
                lhs, rhs,
            );
        }

        #[$crate::proptest::__proptest]
        fn difference_has_zero(a: $crate::anf::AnfSet<$typ>) {
            // A \ 1 = ∅
            let diff = a.clone() - $crate::anf::AnfSet::universe();
            assert!(
                diff.is_empty(),
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    A \\ 1
                      {}
                    should be empty"},
                a,
                diff,
            );
        }

        #[$crate::proptest::__proptest]
        fn intersection_has_unit(a: $crate::anf::AnfSet<$typ>) {
            // A ∩ 1 == A
            let intersection = a.clone() & $crate::anf::AnfSet::universe();
            assert_eq!(
                a, intersection,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    A ∩ 1
                      {}
                    should be the same"},
                a, intersection,
            );
        }

        #[$crate::proptest::__proptest]
        fn intersection_has_zero(a: $crate::anf::AnfSet<$typ>) {
            // A ∩ ∅ == ∅
            let intersection = a.clone() & $crate::anf::AnfSet::empty();
            assert!(
                intersection.is_empty(),
                $crate::proptest::__indoc! {"
                    Intersection with empty
                      of {}
                      with ∅
                      should be empty
                      got {}"},
                a,
                intersection,
            );
        }

        #[$crate::proptest::__proptest]
        fn intersection_is_idempotent(a: $crate::anf::AnfSet<$typ>) {
            // A ∩ A == A
            let lhs = a.clone() & a.clone();
            let rhs = a.clone();
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    A ∩ A
                      {}
                    should be same"},
                a, lhs,
            );
        }

        #[$crate::proptest::__proptest]
        fn intersection_is_symmetric(a: $crate::anf::AnfSet<$typ>, b: $crate::anf::AnfSet<$typ>) {
            // A ∩ B == B ∩ A
            let lhs = a.clone() & b.clone();
            let rhs = b.clone() & a.clone();
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    and set B
                      {}
                    A ∩ B
                      {}
                    and B ∩ A
                      {}
                    should be same"},
                a, b, lhs, rhs,
            );
        }

        #[$crate::proptest::__proptest]
        fn intersection_left_distributes_over_symmetric_difference(
            a: $crate::anf::AnfSet<$typ>,
            b: $crate::anf::AnfSet<$typ>,
            c: $crate::anf::AnfSet<$typ>,
        ) {
            // A ∩ (B ⊕ C) = (A ∩ B) ⊕ (A ∩ C)
            let lhs = a.clone() & (b.clone() ^ c.clone());
            let rhs = (a.clone() & b.clone()) ^ (a.clone() & c.clone());
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    set B
                      {}
                    and set C
                      {}
                    A ∩ (B ⊕ C)
                      {}
                    and (A ∩ B) ⊕ (A ∩ C)
                      {}
                    should be same"},
                a, b, c, lhs, rhs,
            );
        }

        #[$crate::proptest::__proptest]
        fn intersection_right_distributes_over_symmetric_difference(
            a: $crate::anf::AnfSet<$typ>,
            b: $crate::anf::AnfSet<$typ>,
            c: $crate::anf::AnfSet<$typ>,
        ) {
            // (A ⊕ B) ∩ C = (A ∩ C) ⊕ (B ∩ C)
            let lhs = (a.clone() ^ b.clone()) & c.clone();
            let rhs = (a.clone() & c.clone()) ^ (b.clone() & c.clone());
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    set B
                      {}
                    and set C
                      {}
                    (A ⊕ B) ∩ C
                      {}
                    and (A ∩ C) ⊕ (B ∩ C)
                      {}
                    should be same"},
                a, b, c, lhs, rhs,
            );
        }

        #[$crate::proptest::__proptest]
        fn intersection_with_complement_is_empty(a: $crate::anf::AnfSet<$typ>) {
            // A ∩ !A == ∅
            let negated = !a.clone();
            let intersection = a.clone() & negated.clone();
            assert!(
                intersection.is_empty(),
                $crate::proptest::__indoc! {"
                    Intersection with negation
                      of {}
                      with {}
                      should be empty
                      got {}"},
                a,
                negated,
                intersection,
            );
        }

        #[$crate::proptest::__proptest]
        fn symmetric_difference_annhilates(a: $crate::anf::AnfSet<$typ>) {
            // A ⊕ A = ∅
            let diff = a.clone() ^ a.clone();
            assert!(
                diff.is_empty(),
                $crate::proptest::__indoc! {"
                    Given set
                      {}
                    A ⊕ A
                      {}
                    should be empty"},
                a,
                diff,
            );
        }

        #[$crate::proptest::__proptest]
        fn symmetric_difference_has_unit(a: $crate::anf::AnfSet<$typ>) {
            // A ⊕ ∅ = A
            let diff = a.clone() ^ $crate::anf::AnfSet::empty();
            assert_eq!(
                a, diff,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    A ⊕ ∅
                      {}
                    should be the same"},
                a, diff,
            );
        }

        #[$crate::proptest::__proptest]
        fn symmetric_difference_is_union_minus_intersection(
            a: $crate::anf::AnfSet<$typ>,
            b: $crate::anf::AnfSet<$typ>,
        ) {
            // A ⊕ B = (A ∪ B) \ (A ∩ B)
            let lhs = a.clone() ^ b.clone();
            let rhs = (a.clone() | b.clone()) - (a.clone() & b.clone());
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    and set B
                      {}
                    A ⊕ B
                      {}
                    and (A ∪ B) \\ (A ∩ B)
                      {}
                    should be equal"},
                a, b, lhs, rhs,
            );
        }

        #[$crate::proptest::__proptest]
        fn symmetric_difference_is_union_of_differences(
            a: $crate::anf::AnfSet<$typ>,
            b: $crate::anf::AnfSet<$typ>,
        ) {
            // A ⊕ B = (A \ B) ∪ (B \ A)
            let lhs = a.clone() ^ b.clone();
            let rhs = (a.clone() - b.clone()) | (b.clone() - a.clone());
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    and set B
                      {}
                    A ⊕ B
                      {}
                    and (A \\ B) ∪ (B \\ A)
                      {}
                    should be equal"},
                a, b, lhs, rhs,
            );
        }

        #[$crate::proptest::__proptest]
        fn symmetric_difference_with_complement_is_universe(a: $crate::anf::AnfSet<$typ>) {
            // A ⊕ !A == 1
            let lhs = a.clone() ^ !a.clone();
            let rhs = $crate::anf::AnfSet::universe();
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    A ⊕ !A
                      {}
                    should be the universe"},
                a, lhs,
            );
        }

        #[$crate::proptest::__proptest]
        fn union_has_unit(a: $crate::anf::AnfSet<$typ>) {
            // A ∪ ∅ = A
            let union = a.clone() | $crate::anf::AnfSet::empty();
            assert_eq!(
                a, union,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    A ∪ ∅
                      {}
                    should be the same"},
                a, union,
            );
        }

        #[$crate::proptest::__proptest]
        fn union_is_idempotent(a: $crate::anf::AnfSet<$typ>) {
            // A ∪ A == A
            let lhs = a.clone() | a.clone();
            let rhs = a.clone();
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    A ∪ A
                      {}
                    should be same"},
                a, lhs,
            );
        }

        #[$crate::proptest::__proptest]
        fn union_is_symmetric(a: $crate::anf::AnfSet<$typ>, b: $crate::anf::AnfSet<$typ>) {
            // A ∪ B == B ∪ A
            let lhs = a.clone() | b.clone();
            let rhs = b.clone() | a.clone();
            assert_eq!(
                lhs, rhs,
                $crate::proptest::__indoc! {"
                    Given set A
                      {}
                    and set B
                      {}
                    A ∪ B
                      {}
                    and B ∪ A
                      {}
                    should be same"},
                a, b, lhs, rhs,
            );
        }
    };
}

/// Defines additional property tests for [`AnfSet`] implementations where you can easily choose a
/// random element from a set.
///
/// Because ANF sets are implemented via XOR, we cannot efficiently generate set elements by
/// generating elements of each clause and property — it would generate too many false positives
/// that would be thrown away by a [`prop_filter`][proptest::strategy::Strategy::prop_filter]. That
/// means you must use some other mechanism to generate random elements.  Signal that you can
/// do so by implementing the [`ArbitraryElement`] trait _for the set itself_ — that is, for
/// `AnfSet<YourProperty>`.
#[macro_export]
macro_rules! test_anf_set_with_elements {
    ($typ:ty) => {
        #[$crate::proptest::__proptest]
        fn difference_membership(
            a: $crate::proptest::SetAndElement<$crate::anf::AnfSet<$typ>, _>,
            b: $crate::anf::AnfSet<$typ>,
        ) {
            // e ∈ A ⇒ (e ∈ A\B ⇔ e ∉ B)
            let diff = a.set.clone() - b.clone();
            if b.contains(&a.element) {
                assert!(
                    !diff.contains(&a.element),
                    $crate::proptest::__indoc! {"
                        Difference {}
                          of {}
                          and {}
                          should not contain {}"},
                    diff,
                    a.set,
                    b,
                    a.element,
                );
            } else {
                assert!(
                    diff.contains(&a.element),
                    $crate::proptest::__indoc! {"
                        Difference {}
                          of {}
                          and {}
                          should contain {}"},
                    diff,
                    a.set,
                    b,
                    a.element,
                );
            }
        }

        #[$crate::proptest::__proptest]
        fn intersection_membership(
            a: $crate::proptest::SetAndElement<$crate::anf::AnfSet<$typ>, _>,
            b: $crate::anf::AnfSet<$typ>,
        ) {
            // e ∈ A ⇒ (e ∈ (A ∩ B) ⇔ e ∈ B)
            let intersection = a.set.clone() & b.clone();
            if b.contains(&a.element) {
                assert!(
                    intersection.contains(&a.element),
                    $crate::proptest::__indoc! {"
                        Intersection {}
                          of {}
                          and {}
                          should contain {}"},
                    intersection,
                    a.set,
                    b,
                    a.element,
                );
            } else {
                assert!(
                    !intersection.contains(&a.element),
                    $crate::proptest::__indoc! {"
                        Intersection {}
                          of {}
                          and {}
                          should not contain {}"},
                    intersection,
                    a.set,
                    b,
                    a.element,
                );
            }
        }

        #[$crate::proptest::__proptest]
        fn set_element_in_set(a: $crate::proptest::SetAndElement<$crate::anf::AnfSet<$typ>, _>) {
            assert!(
                a.set.contains(&a.element),
                $crate::proptest::__indoc! {"
                    Set {}
                      should contain {}"},
                a.set,
                a.element,
            );
        }

        #[$crate::proptest::__proptest]
        fn union_membership(
            a: $crate::proptest::SetAndElement<$crate::anf::AnfSet<$typ>, _>,
            b: $crate::anf::AnfSet<$typ>,
        ) {
            // e ∈ A ⇒ e ∈ (A ∪ B)
            let union = a.set.clone() | b.clone();
            assert!(
                union.contains(&a.element),
                $crate::proptest::__indoc! {"
                    Union {}
                      of {}
                      and {}
                      should contain {}"},
                union,
                a.set,
                b,
                a.element,
            );
        }

        #[$crate::proptest::__proptest]
        fn union_with_complement_is_universe(a: $crate::anf::AnfSet<$typ>) {
            // A ∪ !A == 1
            let negated = !a.clone();
            let union = a.clone() | negated.clone();
            let universe = $crate::anf::AnfSet::universe();
            assert_eq!(
                union, universe,
                $crate::proptest::__indoc! {"
                    Union with negation
                      of {}
                      with {}
                      should be the universe
                      got {}"},
                a, negated, union,
            );
        }
    };
}