Struct stateright::RewritePlan

pub struct RewritePlan<R, S> { /* private fields */ }

A RewritePlan<R> is derived from a data structure instance and indicates how values of type R (short for “rewritten”) should be rewritten. When that plan is recursively applied via Rewrite, the resulting data structure instance will be behaviorally equivalent to the original data structure under a symmetry equivalence relation, enabling symmetry reduction.

Typically the RewritePlan would be constructed by an implementation of Representative for Model::State.

Implementations

impl<R, S> RewritePlan<R, S>

pub fn rewrite(&self, x: &R) -> R

Applies the rewrite plan to a value of type R

pub fn get_state(&self) -> &S

Returns the state. Useful for debugging

pub fn new(s: S, f: fn(_: &R, _: &S) -> R) -> Self

Creates a new rewrite plan from a given state and function

impl<R> RewritePlan<R, DenseNatMap<R, R>> where
    R: From<usize> + Copy,
    usize: From<R>, 

pub fn from_values_to_sort<'a, V: 'a>(
    to_sort: impl IntoIterator<Item = &'a V>
) -> Self where
    R: From<usize>,
    usize: From<R>,
    V: Ord, 

Constructs a RewritePlan by sorting values in a specified iterator. Favor using the RewritePlan::new constructor over this one as it provides additional type safety.

pub fn reindex<C>(&self, indexed: &C) -> C where
    C: Index<usize>,
    C: FromIterator<C::Output>,
    C::Output: Rewrite<R> + Sized, 

Permutes the elements of a Vec-like collection whose indices correspond with the indices of the Vec-like that was used to construct this RewritePlan.

Trait Implementations

impl<R, S> Debug for RewritePlan<R, S> where
    S: Debug, 

fn fmt(&self, fmt: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<R, V> From<&'_ DenseNatMap<R, V>> for RewritePlan<R, DenseNatMap<R, R>> where
    R: From<usize> + Copy,
    usize: From<R>,
    V: Ord, 

fn from(s: &DenseNatMap<R, V>) -> Self

Performs the conversion.

impl<R, V> From<DenseNatMap<R, V>> for RewritePlan<R, DenseNatMap<R, R>> where
    R: From<usize> + Copy,
    usize: From<R>,
    V: Ord, 

fn from(s: DenseNatMap<R, V>) -> Self

Performs the conversion.