Enum boogie_backend::boogie_wrapper::ModelValue
source · pub enum ModelValue {
Literal(String),
List(Vec<ModelValue>),
Map(BTreeMap<ModelValue, ModelValue>),
}
Expand description
Represents a model value.
Variants§
Implementations§
source§impl ModelValue
impl ModelValue
sourcepub fn pretty_or_raw(
&self,
wrapper: &BoogieWrapper<'_>,
model: &Model,
ty: &Type
) -> RcDoc<'static, ()>
pub fn pretty_or_raw( &self, wrapper: &BoogieWrapper<'_>, model: &Model, ty: &Type ) -> RcDoc<'static, ()>
Pretty prints the given model value which has given type. If printing fails, falls back to print the debug value.
sourcepub fn pretty(
&self,
wrapper: &BoogieWrapper<'_>,
model: &Model,
ty: &Type
) -> Option<RcDoc<'static, ()>>
pub fn pretty( &self, wrapper: &BoogieWrapper<'_>, model: &Model, ty: &Type ) -> Option<RcDoc<'static, ()>>
Pretty prints the given model value which has given type.
sourcepub fn pretty_vec_or_struct_body(
entries: Vec<RcDoc<'static, ()>>
) -> RcDoc<'static, ()>
pub fn pretty_vec_or_struct_body( entries: Vec<RcDoc<'static, ()>> ) -> RcDoc<'static, ()>
Pretty prints the body of a struct or vector, enclosed in braces.
sourcepub fn pretty_vector(
&self,
wrapper: &BoogieWrapper<'_>,
model: &Model,
param: &Type
) -> Option<RcDoc<'static, ()>>
pub fn pretty_vector( &self, wrapper: &BoogieWrapper<'_>, model: &Model, param: &Type ) -> Option<RcDoc<'static, ()>>
Pretty prints a vector.
sourcepub fn pretty_struct(
&self,
wrapper: &BoogieWrapper<'_>,
model: &Model,
module_id: ModuleId,
struct_id: StructId,
inst: &[Type]
) -> Option<RcDoc<'static, ()>>
pub fn pretty_struct( &self, wrapper: &BoogieWrapper<'_>, model: &Model, module_id: ModuleId, struct_id: StructId, inst: &[Type] ) -> Option<RcDoc<'static, ()>>
Pretty prints a struct.
Trait Implementations§
source§impl Clone for ModelValue
impl Clone for ModelValue
source§fn clone(&self) -> ModelValue
fn clone(&self) -> ModelValue
Returns a copy of the value. Read more
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source
. Read moresource§impl Debug for ModelValue
impl Debug for ModelValue
source§impl Hash for ModelValue
impl Hash for ModelValue
source§impl Ord for ModelValue
impl Ord for ModelValue
source§fn cmp(&self, other: &ModelValue) -> Ordering
fn cmp(&self, other: &ModelValue) -> Ordering
1.21.0 · source§fn max(self, other: Self) -> Selfwhere
Self: Sized,
fn max(self, other: Self) -> Selfwhere Self: Sized,
Compares and returns the maximum of two values. Read more
source§impl PartialEq<ModelValue> for ModelValue
impl PartialEq<ModelValue> for ModelValue
source§fn eq(&self, other: &ModelValue) -> bool
fn eq(&self, other: &ModelValue) -> bool
This method tests for
self
and other
values to be equal, and is used
by ==
.source§impl PartialOrd<ModelValue> for ModelValue
impl PartialOrd<ModelValue> for ModelValue
source§fn partial_cmp(&self, other: &ModelValue) -> Option<Ordering>
fn partial_cmp(&self, other: &ModelValue) -> Option<Ordering>
1.0.0 · source§fn le(&self, other: &Rhs) -> bool
fn le(&self, other: &Rhs) -> bool
This method tests less than or equal to (for
self
and other
) and is used by the <=
operator. Read moreimpl Eq for ModelValue
impl StructuralEq for ModelValue
impl StructuralPartialEq for ModelValue
Auto Trait Implementations§
impl RefUnwindSafe for ModelValue
impl Send for ModelValue
impl Sync for ModelValue
impl Unpin for ModelValue
impl UnwindSafe for ModelValue
Blanket Implementations§
source§impl<Q, K> Equivalent<K> for Qwhere
Q: Eq + ?Sized,
K: Borrow<Q> + ?Sized,
impl<Q, K> Equivalent<K> for Qwhere Q: Eq + ?Sized, K: Borrow<Q> + ?Sized,
source§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Compare self to
key
and return true
if they are equal.