Trait rsmt2::QueryIdent
[−]
[src]
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<()>
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.