[−][src]Struct isla_lib::smt::Solver
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>
[src]
pub fn new(ctx: &'ctx Context) -> Self
[src]
pub fn fresh(&mut self) -> Sym
[src]
pub fn get_enum(&mut self, size: usize) -> usize
[src]
pub fn length(&mut self, v: Sym) -> Option<u32>
[src]
pub fn is_bitvector(&mut self, v: Sym) -> bool
[src]
pub fn add(&mut self, def: Def)
[src]
pub fn declare_const(&mut self, ty: Ty) -> Sym
[src]
pub fn define_const(&mut self, exp: Exp) -> Sym
[src]
pub fn assert_eq(&mut self, lhs: Exp, rhs: Exp)
[src]
pub fn cycle_count(&mut self)
[src]
pub fn get_cycle_count(&self) -> i128
[src]
pub fn add_event(&mut self, event: Event<B>)
[src]
pub fn from_checkpoint(
ctx: &'ctx Context,
Checkpoint { num: num, next_var: next_var, trace: trace }: Checkpoint<B>
) -> Self
[src]
ctx: &'ctx Context,
Checkpoint { num: num, next_var: next_var, trace: trace }: Checkpoint<B>
) -> Self
pub fn check_sat_with(&mut self, exp: &Exp) -> SmtResult
[src]
pub fn trace(&self) -> &Trace<B>
[src]
pub fn check_sat(&mut self) -> SmtResult
[src]
Trait Implementations
Auto Trait Implementations
impl<'ctx, B> RefUnwindSafe for Solver<'ctx, B> where
B: RefUnwindSafe,
B: RefUnwindSafe,
impl<'ctx, B> !Send for Solver<'ctx, B>
impl<'ctx, B> !Sync for Solver<'ctx, B>
impl<'ctx, B> Unpin for Solver<'ctx, B> where
B: Unpin,
B: Unpin,
impl<'ctx, B> UnwindSafe for Solver<'ctx, B> where
B: RefUnwindSafe + UnwindSafe,
B: RefUnwindSafe + UnwindSafe,
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> Same<T> for T
type Output = T
Should always be Self
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,