Trait SMTSolverContext

Source

pub trait SMTSolverContext {
    // Required methods
    fn get_smt_solver_mut(&mut self) -> &mut SMTSolver;
    fn get_smt_solver(&self) -> &SMTSolver;

    // Provided method
    fn assert_and_check_expr(
        &mut self,
        expr: SMTExpr,
    ) -> Result<SMTSolution, SMTSolverError> { ... }
}

Expand description

Trait indicating that the a type holds an SMTSolver

This trait should be implemented by any type that holds an SMT solver, i.e. a [easy_smt::Context] object. Implementing this trait will enable the type to encode SMT expressions and check their satisfiability using the SMT solver.