pub struct Sort<'ctx> { /* private fields */ }
Expand description
Sorts represent the various ‘types’ of Ast
s.
Implementations§
source§impl<'ctx> Sort<'ctx>
impl<'ctx> Sort<'ctx>
pub fn uninterpreted(ctx: &'ctx Context, name: Symbol) -> Sort<'ctx>
pub fn bool(ctx: &'ctx Context) -> Sort<'ctx>
pub fn int(ctx: &'ctx Context) -> Sort<'ctx>
pub fn real(ctx: &'ctx Context) -> Sort<'ctx>
pub fn float(ctx: &'ctx Context, ebits: u32, sbits: u32) -> Sort<'ctx>
pub fn float32(ctx: &'ctx Context) -> Sort<'ctx>
pub fn double(ctx: &'ctx Context) -> Sort<'ctx>
pub fn string(ctx: &'ctx Context) -> Sort<'ctx>
pub fn bitvector(ctx: &'ctx Context, sz: u32) -> Sort<'ctx>
pub fn array( ctx: &'ctx Context, domain: &Sort<'ctx>, range: &Sort<'ctx> ) -> Sort<'ctx>
pub fn set(ctx: &'ctx Context, elt: &Sort<'ctx>) -> Sort<'ctx>
sourcepub fn enumeration(
ctx: &'ctx Context,
name: Symbol,
enum_names: &[Symbol]
) -> (Sort<'ctx>, Vec<FuncDecl<'ctx>>, Vec<FuncDecl<'ctx>>)
pub fn enumeration( ctx: &'ctx Context, name: Symbol, enum_names: &[Symbol] ) -> (Sort<'ctx>, Vec<FuncDecl<'ctx>>, Vec<FuncDecl<'ctx>>)
Create an enumeration sort.
Creates a Z3 enumeration sort with the given name
.
The enum variants will have the names in enum_names
.
Three things are returned:
- the created
Sort
, - constants to create the variants,
- and testers to check if a value is equal to a variant.
Examples
let (colors, color_consts, color_testers) = Sort::enumeration(
&ctx,
"Color".into(),
&[
"Red".into(),
"Green".into(),
"Blue".into(),
],
);
let red_const = color_consts[0].apply(&[]);
let red_tester = &color_testers[0];
let eq = red_tester.apply(&[&red_const]);
assert_eq!(solver.check(), SatResult::Sat);
let model = solver.get_model().unwrap();;
assert!(model.eval(&eq, true).unwrap().as_bool().unwrap().as_bool().unwrap());
pub fn kind(&self) -> SortKind
sourcepub fn float_exponent_size(&self) -> Option<u32>
pub fn float_exponent_size(&self) -> Option<u32>
Returns Some(e)
where e
is the number of exponent bits if the sort
is a FloatingPoint
and None
otherwise.
sourcepub fn float_significand_size(&self) -> Option<u32>
pub fn float_significand_size(&self) -> Option<u32>
Returns Some(s)
where s
is the number of significand bits if the sort
is a FloatingPoint
and None
otherwise.
sourcepub fn is_array(&self) -> bool
pub fn is_array(&self) -> bool
Return if this Sort is for an Array
or a Set
.
Examples
let bool_sort = Sort::bool(&ctx);
let int_sort = Sort::int(&ctx);
let array_sort = Sort::array(&ctx, &int_sort, &bool_sort);
let set_sort = Sort::set(&ctx, &int_sort);
assert!(array_sort.is_array());
assert!(set_sort.is_array());
assert!(!int_sort.is_array());
assert!(!bool_sort.is_array());
sourcepub fn array_domain(&self) -> Option<Sort<'_>>
pub fn array_domain(&self) -> Option<Sort<'_>>
Return the Sort
of the domain for Array
s of this Sort
.
If this Sort
is an Array
or Set
, it has a domain sort, so return it.
If this is not an Array
or Set
Sort
, return None
.
Examples
let bool_sort = Sort::bool(&ctx);
let int_sort = Sort::int(&ctx);
let array_sort = Sort::array(&ctx, &int_sort, &bool_sort);
let set_sort = Sort::set(&ctx, &int_sort);
assert_eq!(array_sort.array_domain().unwrap(), int_sort);
assert_eq!(set_sort.array_domain().unwrap(), int_sort);
assert!(int_sort.array_domain().is_none());
assert!(bool_sort.array_domain().is_none());
sourcepub fn array_range(&self) -> Option<Sort<'_>>
pub fn array_range(&self) -> Option<Sort<'_>>
Return the Sort
of the range for Array
s of this Sort
.
If this Sort
is an Array
it has a range sort, so return it.
If this Sort
is a Set
, it has an implied range sort of Bool
.
If this is not an Array
or Set
Sort
, return None
.
Examples
let bool_sort = Sort::bool(&ctx);
let int_sort = Sort::int(&ctx);
let array_sort = Sort::array(&ctx, &int_sort, &bool_sort);
let set_sort = Sort::set(&ctx, &int_sort);
assert_eq!(array_sort.array_range().unwrap(), bool_sort);
assert_eq!(set_sort.array_range().unwrap(), bool_sort);
assert!(int_sort.array_range().is_none());
assert!(bool_sort.array_range().is_none());