[−][src]Struct z3::DatatypeBuilder
Build a datatype sort.
Example:
// Like Rust's Option<int> type let option_int = DatatypeBuilder::new(&ctx) .variant("None", &[]) .variant("Some", &[("value", &Sort::int(&ctx))]) .finish("OptionInt"); // 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(); // 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(ctx: &'ctx Context) -> Self
[src]
pub fn variant(self, name: &str, fields: &[(&str, &Sort)]) -> Self
[src]
pub fn finish(self, name: impl Into<Symbol>) -> 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,
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>,