Trait rsmt2::Query [−] [src]

pub trait Query<'kid, Parser: ParseSmt2 + 'static>: Solver<'kid, Parser> {
    fn print_check_sat(&mut self) -> UnitSmtRes { ... }
    fn parse_check_sat(&mut self) -> SmtRes<bool> { ... }
    fn check_sat(&mut self) -> SmtRes<bool> { ... }
    fn print_get_model(&mut self) -> UnitSmtRes { ... }
    fn parse_get_model<'a>(&'a mut self) -> SmtRes<Vec<(Parser::Ident, Parser::Value)>> where Parser: 'a { ... }
    fn get_model(&mut self) -> SmtRes<Vec<(Parser::Ident, Parser::Value)>> { ... }
    fn parse_get_values(&mut self, info: &Parser::I) -> SmtRes<Vec<(Parser::Expr, Parser::Value)>> { ... }
    fn print_get_assertions(&mut self) -> UnitSmtRes { ... }
    fn print_get_assignment(&mut self) -> UnitSmtRes { ... }
    fn print_get_unsat_assumptions(&mut self) -> UnitSmtRes { ... }
    fn print_get_proof(&mut self) -> UnitSmtRes { ... }
    fn print_get_unsat_core(&mut self) -> UnitSmtRes { ... }
}

Prints queries.

Provided Methods

`fn print_check_sat(&mut self) -> UnitSmtRes`

Check-sat command.

`fn parse_check_sat(&mut self) -> SmtRes<bool>`

Parse the result of a check-sat.

`fn check_sat(&mut self) -> SmtRes<bool>`

Check-sat command.

`fn print_get_model(&mut self) -> UnitSmtRes`

Get-model command.

`fn parse_get_model<'a>(&'a mut self) -> SmtRes<Vec<(Parser::Ident, Parser::Value)>> where Parser: 'a`

Parse the result of a get-model.

`fn get_model(&mut self) -> SmtRes<Vec<(Parser::Ident, Parser::Value)>>`

Get-model command.

`fn parse_get_values(&mut self, info: &Parser::I) -> SmtRes<Vec<(Parser::Expr, Parser::Value)>>`

Parse the result of a get-values.

`fn print_get_assertions(&mut self) -> UnitSmtRes`

Get-assertions command.

`fn print_get_assignment(&mut self) -> UnitSmtRes`

Get-assignment command.

`fn print_get_unsat_assumptions(&mut self) -> UnitSmtRes`

Get-unsat-assumptions command.

`fn print_get_proof(&mut self) -> UnitSmtRes`

Get-proop command.

`fn print_get_unsat_core(&mut self) -> UnitSmtRes`

Get-unsat-core command.

Implementors

impl<'kid, Parser: ParseSmt2 + 'static> Query<'kid, Parser> for PlainSolver<'kid, Parser>
impl<'kid, Parser: ParseSmt2 + 'static> Query<'kid, Parser> for TeeSolver<'kid, Parser>