Struct SuggestionSolver 

pub struct SuggestionSolver<T: Types> {
    session: Z3Subprocess,
    env: ConstraintGlobalEnv<T>,
}

Fields

session: Z3Subprocess

env: ConstraintGlobalEnv<T>

Implementations

impl<T: Types> SuggestionSolver<T>

pub fn new( global_consts: &[ConstDecl<T>], funs: &[FunDef<T>], datatype_decls: Vec<DataDecl<T>>, ) -> Result<Self, SuggestionSolverError>

pub(crate) fn check_validity( &mut self, constraint: &FlatConstraint<T>, ) -> Result<bool, SuggestionSolverError>

pub(crate) fn qe_and_simplify( &mut self, constraint: &FlatConstraint<T>, binder_consts: &[ConstDecl<T>], ) -> Result<Expr<T>, SuggestionSolverError>

fn qe_and_simplify_in_context( session: &mut Z3Subprocess, env: &ConstraintGlobalEnv<T>, locals: &ConstraintLocalEnv<'_, T>, assumptions: &[String], body: &str, implication: &str, ) -> Result<Expr<T>, SuggestionSolverError>