Struct Model

pub struct Model<'ctx, B> { /* private fields */ }

Interface for extracting information from Z3 models.

Model generation should be turned on in advance. This is currently Z3’s default, but it’s best to make sure:

let mut cfg = Config::new();
cfg.set_param_value("model", "true");
let ctx = Context::new(cfg);
let mut solver = Solver::<B64>::new(&ctx);
solver.add(DeclareConst(x, Ty::BitVec(4)));
solver.add(Assert(Bvsgt(Box::new(Var(x)), Box::new(Bits(vec![false,false,true,false])))));
assert!(solver.check_sat() == SmtResult::Sat);
let mut model = Model::new(&solver);
let var0 = model.get_var(x).unwrap().unwrap();

Implementations

impl<'ctx, B: BV> Model<'ctx, B>

pub fn new(solver: &'ctx Solver<'ctx, B>) -> Self

pub fn get_var(&mut self, var: Sym) -> Result<Option<Exp>, ExecError>

pub fn get_exp(&mut self, exp: &Exp) -> Result<Option<Exp>, ExecError>

Trait Implementations

impl<'ctx, B> Debug for Model<'ctx, B>

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

Formats the value using the given formatter.

impl<'ctx, B> Drop for Model<'ctx, B>

fn drop(&mut self)

Executes the destructor for this type.