[−][src]Struct sspds::smt::state_helpers::SmtCompositionState
- composition state smt gen helper type
- what do we need?
-
- composition state sort name
-
- composition state constructor name
-
- composition state accessor names
-
- composition state sort definition
-
- composition state accessor helpers
-
- overwrite/copy-on-write helper
- for that we need...
-
- composition name
-
- SmtPackageState values for each instance
- (declare-datatype State_right-pkey ( (mk-state-right-pkey (state-right-pkey-pk (Array Int String)) (state-right-pkey-sk (Array Int String)) (state-right-pkey-id (Array String Int)) (state-right-pkey-ctr Int) (state-right-pkey-rand RandState))))
Implementations
impl<'a> SmtCompositionState<'a>[src]
pub fn new(
comp_name: &'a str,
substate_names: Vec<&'a str>
) -> SmtCompositionState<'a>[src]
comp_name: &'a str,
substate_names: Vec<&'a str>
) -> SmtCompositionState<'a>
pub fn smt_sort(&self) -> SmtExpr[src]
pub fn smt_constructor(&self) -> SmtExpr[src]
pub fn smt_accessor(&self, inst_name: &str) -> SmtExpr[src]
pub fn smt_access(&self, inst_name: &str, term: SmtExpr) -> SmtExpr[src]
pub fn smt_declare_datatype(&self) -> SmtExpr[src]
pub fn smt_set(&self, target: &str, new: &SmtExpr, body: SmtExpr) -> SmtExpr[src]
Auto Trait Implementations
impl<'a> RefUnwindSafe for SmtCompositionState<'a>
impl<'a> Send for SmtCompositionState<'a>
impl<'a> Sync for SmtCompositionState<'a>
impl<'a> Unpin for SmtCompositionState<'a>
impl<'a> UnwindSafe for SmtCompositionState<'a>
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized, [src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized, [src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized, [src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T[src]
impl<T> From<T> for T[src]
impl<T, U> Into<U> for T where
U: From<T>, [src]
U: From<T>,
impl<T, U> TryFrom<U> for T where
U: Into<T>, [src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>, [src]
U: TryFrom<T>,