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

assert!(model.eval(&eq).unwrap().as_bool().unwrap().as_bool().unwrap());

pub fn kind(&self) -> SortKind

Trait Implementations

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> Eq for Sort<'ctx>

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 ==.

#[must_use]fn ne(&self, other: &Rhs) -> bool

This method tests for !=.