Trait rsmt2::QueryIdent

pub trait QueryIdent<'kid, Parser: ParseSmt2 + 'static, Info, Ident: Sym2Smt<Info>>: Solver<'kid, Parser> + Query<'kid, Parser> {
    fn print_check_sat_assuming(&mut self,
                                bool_vars: &[Ident],
                                info: &Info)
                                -> Res<()> { ... }
    fn check_sat_assuming(&mut self, idents: &[Ident], info: &Info) -> Res<bool> { ... }
}

Queries with ident printing.

Provided Methods

fn print_check_sat_assuming(&mut self,
                            bool_vars: &[Ident],
                            info: &Info)
                            -> Res<()>

Check-sat with assumptions command.

fn check_sat_assuming(&mut self, idents: &[Ident], info: &Info) -> Res<bool>

Check-sat assuming command.

Implementors

• impl<'kid, Parser: ParseSmt2 + 'static, Info, Ident: Sym2Smt<Info>> QueryIdent<'kid, Parser, Info, Ident> for PlainSolver<'kid, Parser>
• impl<'kid, Parser: ParseSmt2 + 'static, Info, Ident: Sym2Smt<Info>> QueryIdent<'kid, Parser, Info, Ident> for TeeSolver<'kid, Parser>