Struct rsmt2::PlainSolver

pub struct PlainSolver<'kid, Parser: ParseSmt2 + 'static> { /* fields omitted */ }

Plain solver, as opposed to TeeSolver which logs IOs.

Methods

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

fn mk(kid: &'kid mut Kid, parser: Parser) -> Res<Self>

Creates a plain solver.

fn tee(self, file: File) -> TeeSolver<'kid, Parser>

Wraps a solver to log IOs to a file.

fn conf(&self) -> &SolverConf

Configuration of the solver.

Trait Implementations

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

fn fetch(&mut self) -> Res<()>

Fetches data.

fn write<F: Fn(&mut Write) -> Res<()>>(&mut self, f: F) -> Res<()>

Applies a function to the writer on the solver's stdin.

fn comment(&mut self, _: &str) -> Res<()>

Writes comments. Ignored for PlainSolver.

fn parser(&self) -> &Parser

The parser.

fn as_ref(&self) -> &[u8]

The bytes of the buffer.

fn solver(&mut self) -> &mut PlainSolver<'kid, Parser>

The plain solver.

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

fn parse<Out, F: Fn(&[u8], &Parser) -> (String, Res<Out>)>(&mut self,
                                                           parser: F)
                                                           -> Res<Out>

Fetchs data, applies a parser (passes the internal parser) and returns its result.

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

fn reset(&mut self) -> Res<()>

Resets the underlying solver. Restarts the kid process if no reset command is supported.

fn set_logic(&mut self, logic: &Logic) -> Res<()>

Sets the logic.

fn set_option<Value: Display>(&mut self, option: &str, value: Value) -> Res<()>

Set option command.

fn interactive_mode(&mut self) -> Res<()>

Activates interactive mode.

fn print_success(&mut self) -> Res<()>

Activates print success.

fn produce_unsat_core(&mut self) -> Res<()>

Activates unsat core production.

fn exit(&mut self) -> Res<()>

Shuts the solver down.

fn push(&mut self, n: &u8) -> Res<()>

Pushes n layers on the assertion stack.

fn pop(&mut self, n: &u8) -> Res<()>

Pops n layers off the assertion stack.

fn reset_assertions(&mut self) -> Res<()>

Resets the assertions in the solver.

fn declare_sort<Sort: Sort2Smt>(&mut self, sort: &Sort, arity: &u8) -> Res<()>

Declares a new sort.

fn define_sort<Sort: Sort2Smt, I, Expr1: Expr2Smt<I>, Expr2: Expr2Smt<I>>(&mut self,
                                                                          sort: &Sort,
                                                                          args: &[Expr1],
                                                                          body: &Expr2,
                                                                          info: &I)
                                                                          -> Res<()>

Defines a new sort.

fn declare_fun<Sort: Sort2Smt, I, Sym: Sym2Smt<I>>(&mut self,
                                                   symbol: &Sym,
                                                   args: &[Sort],
                                                   out: &Sort,
                                                   info: &I)
                                                   -> Res<()>

Declares a new function symbol.

fn declare_const<Sort: Sort2Smt, I, Sym: Sym2Smt<I>>(&mut self,
                                                     symbol: &Sym,
                                                     out_sort: &Sort,
                                                     info: &I)
                                                     -> Res<()>

Declares a new constant.

fn define_fun<I, Sort: Sort2Smt, Sym1: Sym2Smt<I>, Sym2: Sym2Smt<I>, Expr: Expr2Smt<I>>(&mut self,
                                                                                        symbol: &Sym1,
                                                                                        args: &[(Sym2, Sort)],
                                                                                        out: &Sort,
                                                                                        body: &Expr,
                                                                                        info: &I)
                                                                                        -> Res<()>

Defines a new function symbol.

fn define_funs_rec<I, Sort: Sort2Smt, Sym: Sym2Smt<I>, Expr: Expr2Smt<I>>(&mut self,
                                                                          funs: &[(Sym, &[(Sym, Sort)], Sort, Expr)],
                                                                          info: &I)
                                                                          -> Res<()>

Defines some new (possibily mutually) recursive functions.

fn define_fun_rec<I, Sort: Sort2Smt, Sym: Sym2Smt<I>, Expr: Expr2Smt<I>>(&mut self,
                                                                         symbol: &Sym,
                                                                         args: &[(Sym, Sort)],
                                                                         out: &Sort,
                                                                         body: &Expr,
                                                                         info: &I)
                                                                         -> Res<()>

Defines a new recursive function.

fn assert<I, Expr: Expr2Smt<I>>(&mut self, expr: &Expr, info: &I) -> Res<()>

Asserts an expression with some print information.

fn get_info(&mut self, flag: &str) -> Res<()>

Get info command.

fn get_option(&mut self, option: &str) -> Res<()>

Get option command.

fn set_info(&mut self, attribute: &str) -> Res<()>

Set info command.

fn echo(&mut self, text: &str) -> Res<()>

Echo command.

fn parse_success(&mut self) -> Res<()>

Parse success.

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

fn print_check_sat(&mut self) -> Res<()>

Check-sat command.

fn parse_check_sat(&mut self) -> Res<bool>

Parse the result of a check-sat.

fn check_sat(&mut self) -> Res<bool>

Check-sat command.

fn print_get_model(&mut self) -> Res<()>

Get-model command.

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

Parse the result of a get-model.

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

Get-model command.

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

Parse the result of a get-values.

fn print_get_assertions(&mut self) -> Res<()>

Get-assertions command.

fn print_get_assignment(&mut self) -> Res<()>

Get-assignment command.

fn print_get_unsat_assumptions(&mut self) -> Res<()>

Get-unsat-assumptions command.

fn print_get_proof(&mut self) -> Res<()>

Get-proop command.

fn print_get_unsat_core(&mut self) -> Res<()>

Get-unsat-core command.

impl<'kid, Parser: ParseSmt2 + 'static, Info, Ident: Sym2Smt<Info>> QueryIdent<'kid, Parser, Info, Ident> for PlainSolver<'kid, Parser>

fn print_check_sat_assuming(&mut self,
                            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.

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

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

Get-values command.

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

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

Get-values command.