Trait gf::smt::SolverModel

pub trait SolverModel {
    fn value(&mut self, expr: Expr) -> Option<ExprValue>;
}

⚪ A model generated for a satisfiable assertion set.

Required methods

fn value(&mut self, expr: Expr) -> Option<ExprValue>

Calculate value of an expression, if known.

Loading content...

Implementors

impl SolverModel for EmptySolverModel

fn value(&mut self, _: Expr) -> Option<ExprValue>

Loading content...