[−][src]Struct z3::DatatypeBuilder
Build a datatype sort.
Example:
// Like Rust's Option<int> type let option_int = DatatypeBuilder::new(&ctx, "OptionInt") .variant("None", vec![]) .variant( "Some", vec![("value", DatatypeAccessor::Sort(Sort::int(&ctx)))], ) .finish(); // Assert x.is_none() let x = Datatype::new_const(&ctx, "x", &option_int.sort); solver.assert(&option_int.variants[0].tester.apply(&[&x.into()]).as_bool().unwrap()); // Assert y == Some(3) let y = Datatype::new_const(&ctx, "y", &option_int.sort); let value = option_int.variants[1].constructor.apply(&[&Int::from_i64(&ctx, 3).into()]); solver.assert(&y._eq(&value.as_datatype().unwrap())); assert_eq!(solver.check(), SatResult::Sat); let model = solver.get_model().unwrap();; // Get the value out of Some(3) let ast = option_int.variants[1].accessors[0].apply(&[&y.into()]); assert_eq!(3, model.eval(&ast.as_int().unwrap()).unwrap().as_i64().unwrap());
Implementations
impl<'ctx> DatatypeBuilder<'ctx>
[src]
pub fn new<S: Into<Symbol>>(ctx: &'ctx Context, name: S) -> Self
[src]
pub fn variant(
self,
name: &str,
fields: Vec<(&str, DatatypeAccessor<'ctx>)>
) -> Self
[src]
self,
name: &str,
fields: Vec<(&str, DatatypeAccessor<'ctx>)>
) -> Self
pub fn finish(self) -> DatatypeSort<'ctx>
[src]
Trait Implementations
Auto Trait Implementations
impl<'ctx> RefUnwindSafe for DatatypeBuilder<'ctx>
impl<'ctx> !Send for DatatypeBuilder<'ctx>
impl<'ctx> !Sync for DatatypeBuilder<'ctx>
impl<'ctx> Unpin for DatatypeBuilder<'ctx>
impl<'ctx> UnwindSafe for DatatypeBuilder<'ctx>
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,
pub 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.
pub 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>,