Trait rsmt2::QueryExpr

pub trait QueryExpr<'kid, Parser: ParseSmt2 + 'static, Info, Expr: Expr2Smt<Info>>: Solver<'kid, Parser> + Query<'kid, Parser> {
    fn print_get_values(&mut self, exprs: &[Expr], info: &Info) -> Res<()> { ... }
}

Queries with expr printing.

Provided Methods

fn print_get_values(&mut self, exprs: &[Expr], info: &Info) -> Res<()>

Get-values command.

Implementors

• impl<'kid, Parser: ParseSmt2 + 'static, Info, Expr: Expr2Smt<Info>> QueryExpr<'kid, Parser, Info, Expr> for PlainSolver<'kid, Parser>
• impl<'kid, Parser: ParseSmt2 + 'static, Info, Expr: Expr2Smt<Info>> QueryExpr<'kid, Parser, Info, Expr> for TeeSolver<'kid, Parser>