pub struct Comprehension { /* private fields */ }
Expand description
A comprehension.
Implementations§
Source§impl Comprehension
impl Comprehension
pub fn domain_of(&self) -> Option<Domain>
Sourcepub fn expand_simple(
self,
symtab: &mut SymbolTable,
) -> Result<Vec<Expression>, SolverError>
pub fn expand_simple( self, symtab: &mut SymbolTable, ) -> Result<Vec<Expression>, SolverError>
Expands the comprehension using Minion, returning the resulting expressions.
This method performs simple pruning of the induction variables: an expression is returned
for each assignment to the induction variables that satisfy the static guards of the
comprehension. If the comprehension is inside an associative-commutative operation, use
[expand_ac
] instead, as this performs further pruning of “uninteresting” return values.
If successful, this modifies the symbol table given to add aux-variables needed inside the expanded expressions.
Sourcepub fn expand_ac(
self,
symtab: &mut SymbolTable,
ac_operator: ACOperatorKind,
) -> Result<Vec<Expression>, SolverError>
pub fn expand_ac( self, symtab: &mut SymbolTable, ac_operator: ACOperatorKind, ) -> Result<Vec<Expression>, SolverError>
Expands the comprehension using Minion, returning the resulting expressions.
This method is only suitable for comprehensions inside an AC operator. The AC operator that
contains this comprehension should be passed into the ac_operator
argument.
This method performs additional pruning of “uninteresting” values, only possible when the comprehension is inside an AC operator.
If successful, this modifies the symbol table given to add aux-variables needed inside the expanded expressions.
pub fn return_expression(self) -> Expression
pub fn replace_return_expression(&mut self, new_expr: Expression)
Sourcepub fn add_induction_guard(&mut self, guard: Expression) -> bool
pub fn add_induction_guard(&mut self, guard: Expression) -> bool
Adds a guard to the comprehension. Returns false if the guard does not only reference induction variables.
Sourcepub fn is_induction_guard(&self, expr: &Expression) -> bool
pub fn is_induction_guard(&self, expr: &Expression) -> bool
True iff expr only references induction variables.
Trait Implementations§
Source§impl Biplate<Comprehension> for Comprehension
impl Biplate<Comprehension> for Comprehension
Source§fn biplate(
&self,
) -> (Tree<Comprehension>, Box<dyn Fn(Tree<Comprehension>) -> Comprehension>)
fn biplate( &self, ) -> (Tree<Comprehension>, Box<dyn Fn(Tree<Comprehension>) -> Comprehension>)
§fn with_children_bi(&self, children: VecDeque<To>) -> Self
fn with_children_bi(&self, children: VecDeque<To>) -> Self
§fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
Uniplate::descend
] Read more§fn universe_bi(&self) -> VecDeque<To>
fn universe_bi(&self) -> VecDeque<To>
§fn children_bi(&self) -> VecDeque<To>
fn children_bi(&self) -> VecDeque<To>
§fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
§fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
§fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
Source§impl Biplate<Comprehension> for Expression
impl Biplate<Comprehension> for Expression
Source§fn biplate(
&self,
) -> (Tree<Comprehension>, Box<dyn Fn(Tree<Comprehension>) -> Expression>)
fn biplate( &self, ) -> (Tree<Comprehension>, Box<dyn Fn(Tree<Comprehension>) -> Expression>)
§fn with_children_bi(&self, children: VecDeque<To>) -> Self
fn with_children_bi(&self, children: VecDeque<To>) -> Self
§fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
Uniplate::descend
] Read more§fn universe_bi(&self) -> VecDeque<To>
fn universe_bi(&self) -> VecDeque<To>
§fn children_bi(&self) -> VecDeque<To>
fn children_bi(&self) -> VecDeque<To>
§fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
§fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
§fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
Source§impl Biplate<Comprehension> for SubModel
impl Biplate<Comprehension> for SubModel
Source§fn biplate(
&self,
) -> (Tree<Comprehension>, Box<dyn Fn(Tree<Comprehension>) -> Self>)
fn biplate( &self, ) -> (Tree<Comprehension>, Box<dyn Fn(Tree<Comprehension>) -> Self>)
§fn with_children_bi(&self, children: VecDeque<To>) -> Self
fn with_children_bi(&self, children: VecDeque<To>) -> Self
§fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
Uniplate::descend
] Read more§fn universe_bi(&self) -> VecDeque<To>
fn universe_bi(&self) -> VecDeque<To>
§fn children_bi(&self) -> VecDeque<To>
fn children_bi(&self) -> VecDeque<To>
§fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
§fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
§fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
Source§impl Biplate<Comprehension> for SymbolTable
impl Biplate<Comprehension> for SymbolTable
Source§fn biplate(
&self,
) -> (Tree<Comprehension>, Box<dyn Fn(Tree<Comprehension>) -> Self>)
fn biplate( &self, ) -> (Tree<Comprehension>, Box<dyn Fn(Tree<Comprehension>) -> Self>)
§fn with_children_bi(&self, children: VecDeque<To>) -> Self
fn with_children_bi(&self, children: VecDeque<To>) -> Self
§fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
Uniplate::descend
] Read more§fn universe_bi(&self) -> VecDeque<To>
fn universe_bi(&self) -> VecDeque<To>
§fn children_bi(&self) -> VecDeque<To>
fn children_bi(&self) -> VecDeque<To>
§fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
§fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
§fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
Source§impl Biplate<Expression> for Comprehension
impl Biplate<Expression> for Comprehension
Source§fn biplate(
&self,
) -> (Tree<Expression>, Box<dyn Fn(Tree<Expression>) -> Comprehension>)
fn biplate( &self, ) -> (Tree<Expression>, Box<dyn Fn(Tree<Expression>) -> Comprehension>)
§fn with_children_bi(&self, children: VecDeque<To>) -> Self
fn with_children_bi(&self, children: VecDeque<To>) -> Self
§fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
Uniplate::descend
] Read more§fn universe_bi(&self) -> VecDeque<To>
fn universe_bi(&self) -> VecDeque<To>
§fn children_bi(&self) -> VecDeque<To>
fn children_bi(&self) -> VecDeque<To>
§fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
§fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
§fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
Source§impl Biplate<SubModel> for Comprehension
impl Biplate<SubModel> for Comprehension
Source§fn biplate(
&self,
) -> (Tree<SubModel>, Box<dyn Fn(Tree<SubModel>) -> Comprehension>)
fn biplate( &self, ) -> (Tree<SubModel>, Box<dyn Fn(Tree<SubModel>) -> Comprehension>)
§fn with_children_bi(&self, children: VecDeque<To>) -> Self
fn with_children_bi(&self, children: VecDeque<To>) -> Self
§fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self
Uniplate::descend
] Read more§fn universe_bi(&self) -> VecDeque<To>
fn universe_bi(&self) -> VecDeque<To>
§fn children_bi(&self) -> VecDeque<To>
fn children_bi(&self) -> VecDeque<To>
§fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self
§fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
§fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>
Source§impl Clone for Comprehension
impl Clone for Comprehension
Source§fn clone(&self) -> Comprehension
fn clone(&self) -> Comprehension
1.0.0 · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source
. Read moreSource§impl Debug for Comprehension
impl Debug for Comprehension
Source§impl<'de> Deserialize<'de> for Comprehension
impl<'de> Deserialize<'de> for Comprehension
Source§fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
Source§impl Display for Comprehension
impl Display for Comprehension
Source§impl PartialEq for Comprehension
impl PartialEq for Comprehension
Source§impl Serialize for Comprehension
impl Serialize for Comprehension
Source§impl Uniplate for Comprehension
impl Uniplate for Comprehension
Source§fn uniplate(
&self,
) -> (Tree<Comprehension>, Box<dyn Fn(Tree<Comprehension>) -> Comprehension>)
fn uniplate( &self, ) -> (Tree<Comprehension>, Box<dyn Fn(Tree<Comprehension>) -> Comprehension>)
Uniplate
. Read more§fn descend(&self, op: &impl Fn(Self) -> Self) -> Self
fn descend(&self, op: &impl Fn(Self) -> Self) -> Self
§fn universe(&self) -> VecDeque<Self>
fn universe(&self) -> VecDeque<Self>
§fn with_children(&self, children: VecDeque<Self>) -> Self
fn with_children(&self, children: VecDeque<Self>) -> Self
§fn transform(&self, f: &impl Fn(Self) -> Self) -> Self
fn transform(&self, f: &impl Fn(Self) -> Self) -> Self
§fn rewrite(&self, f: &impl Fn(Self) -> Option<Self>) -> Self
fn rewrite(&self, f: &impl Fn(Self) -> Option<Self>) -> Self
§fn cata<T>(&self, op: &impl Fn(Self, VecDeque<T>) -> T) -> T
fn cata<T>(&self, op: &impl Fn(Self, VecDeque<T>) -> T) -> T
impl Eq for Comprehension
impl StructuralPartialEq for Comprehension
Auto Trait Implementations§
impl Freeze for Comprehension
impl !RefUnwindSafe for Comprehension
impl !Send for Comprehension
impl !Sync for Comprehension
impl Unpin for Comprehension
impl !UnwindSafe for Comprehension
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
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
§impl<T> Instrument for T
impl<T> Instrument for T
§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
self
into a Left
variant of Either<Self, Self>
if into_left
is true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
self
into a Left
variant of Either<Self, Self>
if into_left(&self)
returns true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read more§impl<T> WithSubscriber for T
impl<T> WithSubscriber for T
§fn with_subscriber<S>(self, subscriber: S) -> WithDispatch<Self>where
S: Into<Dispatch>,
fn with_subscriber<S>(self, subscriber: S) -> WithDispatch<Self>where
S: Into<Dispatch>,
§fn with_current_subscriber(self) -> WithDispatch<Self>
fn with_current_subscriber(self) -> WithDispatch<Self>
impl<T> DeserializeOwned for Twhere
T: for<'de> Deserialize<'de>,
Layout§
Note: Most layout information is completely unstable and may even differ between compilations. The only exception is types with certain repr(...)
attributes. Please see the Rust Reference's “Type Layout” chapter for details on type layout guarantees.
Size: 56 bytes