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) -> UnitSmtRes { ... } fn check_sat_assuming(&mut self, idents: &[Ident], info: &Info) -> SmtRes<bool> { ... } }
Queries with ident printing.
Provided Methods
fn print_check_sat_assuming(&mut self, bool_vars: &[Ident], info: &Info) -> UnitSmtRes
Check-sat with assumptions command.
fn check_sat_assuming(&mut self, idents: &[Ident], info: &Info) -> SmtRes<bool>
Check-sat assuming command.