Trait gf::smt::SolverInstance

pub trait SolverInstance: Sized {
    type Model: SolverModel;
    fn assert(&mut self, expr: Expr);
    fn solve(self) -> SolverResult<Self>;
}

⚪ An SMT solver instance.

Associated Types

type Model: SolverModel

Model implementation type.

Loading content...

Required methods

fn assert(&mut self, expr: Expr)

Assert an expression.

fn solve(self) -> SolverResult<Self>

Check whether the current assertion set is satisfiable and return the model.

Loading content...

Implementors

Loading content...