Struct rsmt2::TeeSolver
[−]
[src]
pub struct TeeSolver<'kid, Parser: ParseSmt2 + 'static> { // some fields omitted }
Wrapper around a PlainSolver
logging IOs to a file.
Methods
impl<'kid, Parser: ParseSmt2 + 'static> TeeSolver<'kid, Parser>
[src]
fn conf(&self) -> &SolverConf
Configuration of the solver.
Trait Implementations
impl<'kid, Parser: ParseSmt2 + 'static> SolverBasic<'kid, Parser> for TeeSolver<'kid, Parser>
[src]
fn fetch(&mut self) -> UnitSmtRes
Fetches data.
fn write<F: Fn(&mut Write) -> UnitSmtRes>(&mut self, f: F) -> UnitSmtRes
Applies a function to the writer on the solver's stdin.
fn comment(&mut self, txt: &str) -> UnitSmtRes
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 TeeSolver<'kid, Parser>
[src]
fn parse<Out, F: Fn(&[u8], &Parser) -> (String, SmtRes<Out>)>(&mut self, parser: F) -> SmtRes<Out>
Fetchs data, applies a parser (passes the internal parser) and returns its result. Read more
impl<'kid, Parser: ParseSmt2 + 'static> Solver<'kid, Parser> for TeeSolver<'kid, Parser>
[src]
fn reset(&mut self) -> UnitSmtRes
Resets the underlying solver. Restarts the kid process if no reset command is supported. Read more
fn set_logic(&mut self, logic: &Logic) -> UnitSmtRes
Sets the logic.
fn set_option<Value: Display>(&mut self, option: &str, value: Value) -> UnitSmtRes
Set option command.
fn interactive_mode(&mut self) -> UnitSmtRes
Activates interactive mode.
fn print_success(&mut self) -> UnitSmtRes
Activates print success.
fn produce_unsat_core(&mut self) -> UnitSmtRes
Activates unsat core production.
fn exit(&mut self) -> UnitSmtRes
Shuts the solver down.
fn push(&mut self, n: &u8) -> UnitSmtRes
Pushes n
layers on the assertion stack.
fn pop(&mut self, n: &u8) -> UnitSmtRes
Pops n
layers off the assertion stack.
fn reset_assertions(&mut self) -> UnitSmtRes
Resets the assertions in the solver.
fn declare_sort<Sort: Sort2Smt>(&mut self, sort: &Sort, arity: &u8) -> UnitSmtRes
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) -> UnitSmtRes
Defines a new sort.
fn declare_fun<Sort: Sort2Smt, I, Sym: Sym2Smt<I>>(&mut self, symbol: &Sym, args: &[Sort], out: &Sort, info: &I) -> UnitSmtRes
Declares a new function symbol.
fn declare_const<Sort: Sort2Smt, I, Sym: Sym2Smt<I>>(&mut self, symbol: &Sym, out_sort: &Sort, info: &I) -> UnitSmtRes
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) -> UnitSmtRes
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) -> UnitSmtRes
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) -> UnitSmtRes
Defines a new recursive function.
fn assert<I, Expr: Expr2Smt<I>>(&mut self, expr: &Expr, info: &I) -> UnitSmtRes
Asserts an expression with some print information.
fn get_info(&mut self, flag: &str) -> UnitSmtRes
Get info command.
fn get_option(&mut self, option: &str) -> UnitSmtRes
Get option command.
fn set_info(&mut self, attribute: &str) -> UnitSmtRes
Set info command.
fn echo(&mut self, text: &str) -> UnitSmtRes
Echo command.
fn parse_success(&mut self) -> SmtRes<()>
Parse success.
impl<'kid, Parser: ParseSmt2 + 'static> Query<'kid, Parser> for TeeSolver<'kid, Parser>
[src]
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.
impl<'kid, Parser: ParseSmt2 + 'static, Info, Ident: Sym2Smt<Info>> QueryIdent<'kid, Parser, Info, Ident> for TeeSolver<'kid, Parser>
[src]
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.
impl<'kid, Parser: ParseSmt2 + 'static, Info, Expr: Expr2Smt<Info>> QueryExpr<'kid, Parser, Info, Expr> for TeeSolver<'kid, Parser>
[src]
fn print_get_values(&mut self, exprs: &[Expr], info: &Info) -> UnitSmtRes
Get-values command.