Struct z3::Sort

pub struct Sort<'ctx> { /* fields omitted */ }

Sorts represent the various ‘types’ of Asts.

Implementations

impl<'ctx> Sort<'ctx>

pub fn uninterpreted(ctx: &'ctx Context, name: Symbol) -> Sort<'ctx>

pub fn bool(ctx: &Context) -> Sort<'_>

pub fn int(ctx: &Context) -> Sort<'_>

pub fn real(ctx: &Context) -> Sort<'_>

pub fn float(ctx: &Context, ebits: u32, sbits: u32) -> Sort<'_>

pub fn float32(ctx: &Context) -> Sort<'_>

pub fn double(ctx: &Context) -> Sort<'_>

pub fn string(ctx: &'ctx Context) -> Sort<'ctx>

pub fn bitvector(ctx: &Context, sz: u32) -> Sort<'_>

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>

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

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.

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.

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());

pub fn array_domain(&self) -> Option<Sort<'_>>

Return the Sort of the domain for Arrays 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());

pub fn array_range(&self) -> Option<Sort<'_>>

Return the Sort of the range for Arrays 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());

Trait Implementations

impl<'ctx> Clone for Sort<'ctx>

fn clone(&self) -> Self

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'ctx> Debug for Sort<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Display for Sort<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Drop for Sort<'ctx>

fn drop(&mut self)

Executes the destructor for this type.

impl<'ctx> PartialEq<Sort<'ctx>> for Sort<'ctx>

fn eq(&self, other: &Sort<'ctx>) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=.

impl<'ctx> Eq for Sort<'ctx>