Trait SmtModelRef

pub trait SmtModelRef<'ctx, S: SmtSolver<'ctx>>: Debug {
    // Required method
    fn to_model(&self) -> Option<S::Model>;
}

Reference to SmtModel.

Required Methods

fn to_model(&self) -> Option<S::Model>

Convert the reference into an owned model.

Implementors

impl<'ctx> SmtModelRef<'ctx, Z3Solver<'ctx>> for ModelRef<'_, 'ctx>

impl<'r, 'ctx, S: SmtSolver<'ctx> + 'r + 'ctx, C: SolverCache> SmtModelRef<'ctx, CachedSolver<'ctx, S, C>> for CacheModelRef<'r, 'ctx, S>