Trait rsmt2::QueryExprInfo

pub trait QueryExprInfo<'kid, Parser: ParseSmt2 + 'static, Expr: Expr2Smt<Parser::I>>: Solver<'kid, Parser> + QueryExpr<'kid, Parser, Parser::I, Expr> {
    fn get_values(
        &mut self, 
        exprs: &[Expr], 
        info: &Parser::I
    ) -> Res<Vec<(Parser::Expr, Parser::Value)>> { ... }
}

Queries with expr printing and related print/parse information.

Provided Methods

fn get_values(
    &mut self,
    exprs: &[Expr],
    info: &Parser::I
) -> Res<Vec<(Parser::Expr, Parser::Value)>>

Get-values command.

Implementors

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