Trait rsmt2::Solver
[−]
[src]
pub trait Solver<'kid, Parser: ParseSmt2 + 'static>: SolverPrims<'kid, Parser> { fn reset(&mut self) -> Res<()> { ... } fn set_logic(&mut self, logic: &Logic) -> Res<()> { ... } fn set_option<Value: Display>(
&mut self,
option: &str,
value: Value
) -> Res<()> { ... } fn interactive_mode(&mut self) -> Res<()> { ... } fn print_success(&mut self) -> Res<()> { ... } fn produce_unsat_core(&mut self) -> Res<()> { ... } fn exit(&mut self) -> Res<()> { ... } fn push(&mut self, n: &u8) -> Res<()> { ... } fn pop(&mut self, n: &u8) -> Res<()> { ... } fn reset_assertions(&mut self) -> Res<()> { ... } fn declare_sort<Sort: Sort2Smt>(
&mut self,
sort: &Sort,
arity: &u8
) -> Res<()> { ... } fn define_sort<Sort: Sort2Smt, I, Expr1: Expr2Smt<I>, Expr2: Expr2Smt<I>>(
&mut self,
sort: &Sort,
args: &[Expr1],
body: &Expr2,
info: &I
) -> Res<()> { ... } fn declare_fun<Sort: Sort2Smt, I, Sym: Sym2Smt<I>>(
&mut self,
symbol: &Sym,
args: &[Sort],
out: &Sort,
info: &I
) -> Res<()> { ... } fn declare_const<Sort: Sort2Smt, I, Sym: Sym2Smt<I>>(
&mut self,
symbol: &Sym,
out_sort: &Sort,
info: &I
) -> Res<()> { ... } 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<()> { ... } fn define_funs_rec<I, Sort: Sort2Smt, Sym: Sym2Smt<I>, Expr: Expr2Smt<I>>(
&mut self,
funs: &[(Sym, &[(Sym, Sort)], Sort, Expr)],
info: &I
) -> Res<()> { ... } 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<()> { ... } fn assert<I, Expr: Expr2Smt<I>>(&mut self, expr: &Expr, info: &I) -> Res<()> { ... } fn get_info(&mut self, flag: &str) -> Res<()> { ... } fn get_option(&mut self, option: &str) -> Res<()> { ... } fn set_info(&mut self, attribute: &str) -> Res<()> { ... } fn echo(&mut self, text: &str) -> Res<()> { ... } fn parse_success(&mut self) -> Res<()> { ... } }
Provides SMT-LIB commands that are not queries.
Provided Methods
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<()>
&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.
Implementors
impl<'kid, Parser: ParseSmt2 + 'static> Solver<'kid, Parser> for PlainSolver<'kid, Parser>
impl<'kid, Parser: ParseSmt2 + 'static> Solver<'kid, Parser> for TeeSolver<'kid, Parser>