Struct Model

pub struct Model<'st> { /* private fields */ }

A Model contains the values of all named constants returned through Solver::check_sat_with_model or by calling Solver::get_model.

The two most common usages of Model is to:

• Extract values for constants using Model::eval.
• Print out the produced model using println!("{model}").

Implementations

impl<'st> Model<'st>

pub fn eval<T: Sorted<'st>>(&self, x: Const<'st, T>) -> Option<T::Inner>

where T::Inner: From<STerm<'st>>,

Extract the value of a constant. Returns None if the value was not part of the model, which occurs if the constant was not part of any expression asserted.

let x = Int::new_const(&st, "x");
solver.assert(x._eq(12))?;
let model = solver.check_sat_with_model()?.expect_sat()?;
match model.eval(x) {
    Some(x) => println!("This is the value of x: {x}"),
    None => panic!("Oh no! This should never happen, as x was part of an assert"),
}

Trait Implementations

impl Debug for Model<'_>

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

Formats the value using the given formatter.

impl Display for Model<'_>

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

Formats the value using the given formatter.