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>( to_sort: impl IntoIterator<Item = &'a V> ) -> Selfwhere R: From<usize>, usize: From<R>, V: Ord + 'a,

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) -> Cwhere C: Index<usize> + 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

Converts to this type from the input type.

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

Converts to this type from the input type.