Struct z3::DatatypeBuilder [−][src]
pub struct DatatypeBuilder<'ctx> { /* fields omitted */ }
Expand description
Build a custom 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]).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)]); 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]); assert_eq!(3, model.eval(&ast.as_int().unwrap(), true).unwrap().as_i64().unwrap());
Implementations
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>