Struct stateright::RewritePlan
source · pub struct RewritePlan<R, S> { /* private fields */ }
Expand description
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§
source§impl<R, S> RewritePlan<R, S>
impl<R, S> RewritePlan<R, S>
source§impl<R> RewritePlan<R, DenseNatMap<R, R>>where
R: From<usize> + Copy,
usize: From<R>,
impl<R> RewritePlan<R, DenseNatMap<R, R>>where R: From<usize> + Copy, usize: From<R>,
sourcepub fn from_values_to_sort<'a, V>(
to_sort: impl IntoIterator<Item = &'a V>
) -> Selfwhere
R: From<usize>,
usize: From<R>,
V: Ord + 'a,
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.
Trait Implementations§
source§impl<R, S> Debug for RewritePlan<R, S>where
S: Debug,
impl<R, S> Debug for RewritePlan<R, S>where S: Debug,
source§impl<R, V> From<&DenseNatMap<R, V>> for RewritePlan<R, DenseNatMap<R, R>>where
R: From<usize> + Copy,
usize: From<R>,
V: Ord,
impl<R, V> From<&DenseNatMap<R, V>> for RewritePlan<R, DenseNatMap<R, R>>where R: From<usize> + Copy, usize: From<R>, V: Ord,
source§fn from(s: &DenseNatMap<R, V>) -> Self
fn from(s: &DenseNatMap<R, V>) -> Self
Converts to this type from the input type.
source§impl<R, V> From<DenseNatMap<R, V>> for RewritePlan<R, DenseNatMap<R, R>>where
R: From<usize> + Copy,
usize: From<R>,
V: Ord,
impl<R, V> From<DenseNatMap<R, V>> for RewritePlan<R, DenseNatMap<R, R>>where R: From<usize> + Copy, usize: From<R>, V: Ord,
source§fn from(s: DenseNatMap<R, V>) -> Self
fn from(s: DenseNatMap<R, V>) -> Self
Converts to this type from the input type.
Auto Trait Implementations§
impl<R, S> RefUnwindSafe for RewritePlan<R, S>where S: RefUnwindSafe,
impl<R, S> Send for RewritePlan<R, S>where S: Send,
impl<R, S> Sync for RewritePlan<R, S>where S: Sync,
impl<R, S> Unpin for RewritePlan<R, S>where S: Unpin,
impl<R, S> UnwindSafe for RewritePlan<R, S>where S: UnwindSafe,
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more