Struct rsmt2::PlainSolver
[−]
[src]
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>
[src]
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>
[src]
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>
[src]
fn parse<Out, F: Fn(&[u8], &Parser) -> (String, Res<Out>)>(
&mut self,
parser: F
) -> Res<Out>
&mut self,
parser: F
) -> Res<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 PlainSolver<'kid, Parser>
[src]
fn reset(&mut self) -> Res<()>
Resets the underlying solver. Restarts the kid process if no reset command is supported. Read more
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<()>
&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<()>
&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<()>
&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<()>
&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<()>
&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<()>
&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>
[src]
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,
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)>>
&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>
[src]
fn print_check_sat_assuming(
&mut self,
bool_vars: &[Ident],
info: &Info
) -> Res<()>
&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>
[src]
fn print_get_values(&mut self, exprs: &[Expr], info: &Info) -> Res<()>
Get-values command.