Trait SmtModel

pub trait SmtModel<'ctx, S: SmtSolver<'ctx>>: Debug {
    // Required method
    fn get_const_interp(&self, name: &S::BV) -> Option<S::BV>;
}

Model for satisfied assertions.

Required Methods

fn get_const_interp(&self, name: &S::BV) -> Option<S::BV>

Obtain the value for a constant in the model.

Implementors

impl<'ctx> SmtModel<'ctx, Z3Solver<'ctx>> for Model<'ctx>

impl<'ctx, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtModel<'ctx, CachedSolver<'ctx, S, C>> for CacheModel<'ctx, S>