[−][src]Struct sspds::smt::state_helpers::SmtPackageState
packages state smt gen helper type
what do we need?
- state type name ✅
- state type definition ✅
- state type constructor name ✅
- state type accessors ✅
- overwrite/copy-on-write helper ✅
for that we need...
- composition name
- package instance name
- state variables
Implementations
impl<'a> SmtPackageState<'a>[src]
comp = mod_prf_game inst = multi_key
pub fn new(
comp_name: &'a str,
inst_name: &'a str,
state: Vec<(String, Type)>
) -> SmtPackageState<'a>[src]
comp_name: &'a str,
inst_name: &'a str,
state: Vec<(String, Type)>
) -> SmtPackageState<'a>
pub fn smt_constructor(&self) -> SmtExpr[src]
pub fn smt_sort(&self) -> SmtExpr[src]
pub fn smt_accessor(&self, id: &str) -> SmtExpr[src]
pub fn smt_access(&self, id: &str, term: SmtExpr) -> SmtExpr[src]
pub fn smt_declare_datatype(&self) -> SmtExpr[src]
pub fn smt_set(&self, id: &str, new: &SmtExpr) -> SmtExpr[src]
Auto Trait Implementations
impl<'a> RefUnwindSafe for SmtPackageState<'a>
impl<'a> Send for SmtPackageState<'a>
impl<'a> Sync for SmtPackageState<'a>
impl<'a> Unpin for SmtPackageState<'a>
impl<'a> UnwindSafe for SmtPackageState<'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>,