Struct Sort 

pub struct Sort { /* private fields */ }

Sorts represent the various ‘types’ of Asts.

Implementations

impl Sort

pub fn get_z3_sort(&self) -> Z3_sort

pub fn uninterpreted(name: Symbol) -> Sort

pub fn bool() -> Sort

pub fn int() -> Sort

pub fn real() -> Sort

pub fn float(ebits: u32, sbits: u32) -> Sort

pub fn float32() -> Sort

pub fn double() -> Sort

pub fn string() -> Sort

pub fn bitvector(sz: u32) -> Sort

pub fn array(domain: &Sort, range: &Sort) -> Sort

pub fn set(elt: &Sort) -> Sort

pub fn seq(elt: &Sort) -> Sort

pub fn enumeration( name: Symbol, enum_names: &[Symbol], ) -> (Sort, Vec<FuncDecl>, Vec<FuncDecl>)

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(
    "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();
let int_sort = Sort::int();
let array_sort = Sort::array(&int_sort, &bool_sort);
let set_sort = Sort::set(&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();
let int_sort = Sort::int();
let array_sort = Sort::array(&int_sort, &bool_sort);
let set_sort = Sort::set(&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();
let int_sort = Sort::int();
let array_sort = Sort::array(&int_sort, &bool_sort);
let set_sort = Sort::set(&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 Clone for Sort

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Sort

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

Formats the value using the given formatter.

impl Display for Sort

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

Formats the value using the given formatter.

impl Drop for Sort

fn drop(&mut self)

Executes the destructor for this type.

impl PartialEq for Sort

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Sort