Type Alias SMTSolver 

pub type SMTSolver = Context;

Interface to interact with SMT solver

This type is an alias for the easy_smt::Context type. See easy-smt for more information.

Aliased Type

pub struct SMTSolver { /* private fields */ }

Trait Implementations

impl SMTSolverContext for SMTSolver

fn get_smt_solver_mut(&mut self) -> &mut SMTSolver

Get a mutable reference to the SMT solver associated with this context

fn get_smt_solver(&self) -> &SMTSolver

Get the SMT solver associated with this context

fn assert_and_check_expr( &mut self, expr: SMTExpr, ) -> Result<SMTSolution, SMTSolverError>

Check the satisfiability of the given SMTExpr