Struct Solver 

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

The Solver type handles all interaction with Z3. It mimics interacting with Z3 via the subset of the SMTLIB 2.0 format we care about.

For example:

let cfg = Config::new();
let ctx = Context::new(cfg);
let mut solver = Solver::<B64>::new(&ctx);
// (declare-const v0 Bool)
solver.add(DeclareConst(x, Ty::Bool));
// (assert v0)
solver.add(Assert(Var(x)));
// (check-sat)
assert!(solver.check_sat() == SmtResult::Sat)

The other thing the Solver type does is maintain a trace of interactions with Z3, which can be checkpointed and replayed by another solver. This Checkpoint type is safe to be sent between threads.

For example:

let point = {
    let cfg = Config::new();
    let ctx = Context::new(cfg);
    let mut solver = Solver::<B64>::new(&ctx);
    solver.add(DeclareConst(x, Ty::Bool));
    solver.add(Assert(Var(x)));
    solver.add(Assert(Not(Box::new(Var(x)))));
    checkpoint(&mut solver)
};
let cfg = Config::new();
let ctx = Context::new(cfg);
let mut solver = Solver::from_checkpoint(&ctx, point);
assert!(solver.check_sat() == SmtResult::Unsat);

Implementations

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

pub fn new(ctx: &'ctx Context) -> Self

pub fn fresh(&mut self) -> Sym

pub fn get_enum(&mut self, size: usize) -> usize

pub fn length(&mut self, v: Sym) -> Option<u32>

pub fn is_bitvector(&mut self, v: Sym) -> bool

pub fn add(&mut self, def: Def)

pub fn declare_const(&mut self, ty: Ty) -> Sym

pub fn define_const(&mut self, exp: Exp) -> Sym

pub fn assert_eq(&mut self, lhs: Exp, rhs: Exp)

pub fn cycle_count(&mut self)

pub fn get_cycle_count(&self) -> i128

pub fn add_event(&mut self, event: Event<B>)

pub fn from_checkpoint(ctx: &'ctx Context, _: Checkpoint<B>) -> Self

pub fn check_sat_with(&mut self, exp: &Exp) -> SmtResult

pub fn trace(&self) -> &Trace<B>

pub fn check_sat(&mut self) -> SmtResult

pub fn dump_solver(&mut self, filename: &str)

pub fn dump_solver_with(&mut self, filename: &str, exp: &Exp)

pub fn exp_to_str(&mut self, exp: &Exp) -> String

Trait Implementations

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

fn drop(&mut self)

Executes the destructor for this type.