Trait rsmt2::Solver [−] [src]

pub trait Solver<'kid, Parser: ParseSmt2 + 'static>: SolverPrims<'kid, Parser> {
    fn reset(&mut self) -> UnitSmtRes { ... }
    fn set_logic(&mut self, logic: &Logic) -> UnitSmtRes { ... }
    fn set_option<Value: Display>(&mut self, option: &str, value: Value) -> UnitSmtRes { ... }
    fn interactive_mode(&mut self) -> UnitSmtRes { ... }
    fn print_success(&mut self) -> UnitSmtRes { ... }
    fn produce_unsat_core(&mut self) -> UnitSmtRes { ... }
    fn exit(&mut self) -> UnitSmtRes { ... }
    fn push(&mut self, n: &u8) -> UnitSmtRes { ... }
    fn pop(&mut self, n: &u8) -> UnitSmtRes { ... }
    fn reset_assertions(&mut self) -> UnitSmtRes { ... }
    fn declare_sort<Sort: Sort2Smt>(&mut self, sort: &Sort, arity: &u8) -> UnitSmtRes { ... }
    fn define_sort<Sort: Sort2Smt, I, Expr1: Expr2Smt<I>, Expr2: Expr2Smt<I>>(&mut self, sort: &Sort, args: &[Expr1], body: &Expr2, info: &I) -> UnitSmtRes { ... }
    fn declare_fun<Sort: Sort2Smt, I, Sym: Sym2Smt<I>>(&mut self, symbol: &Sym, args: &[Sort], out: &Sort, info: &I) -> UnitSmtRes { ... }
    fn declare_const<Sort: Sort2Smt, I, Sym: Sym2Smt<I>>(&mut self, symbol: &Sym, out_sort: &Sort, info: &I) -> UnitSmtRes { ... }
    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 { ... }
    fn define_funs_rec<I, Sort: Sort2Smt, Sym: Sym2Smt<I>, Expr: Expr2Smt<I>>(&mut self, funs: &[(Sym, &[(Sym, Sort)], Sort, Expr)], info: &I) -> UnitSmtRes { ... }
    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 { ... }
    fn assert<I, Expr: Expr2Smt<I>>(&mut self, expr: &Expr, info: &I) -> UnitSmtRes { ... }
    fn get_info(&mut self, flag: &str) -> UnitSmtRes { ... }
    fn get_option(&mut self, option: &str) -> UnitSmtRes { ... }
    fn set_info(&mut self, attribute: &str) -> UnitSmtRes { ... }
    fn echo(&mut self, text: &str) -> UnitSmtRes { ... }
    fn parse_success(&mut self) -> SmtRes<()> { ... }
}

Provides SMT-LIB commands that are not queries.

Provided Methods

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

Sets the logic.

Set option command.

Activates interactive mode.

Activates print success.

Activates unsat core production.

Shuts the solver down.

Pushes n layers on the assertion stack.

Pops n layers off the assertion stack.

Resets the assertions in the solver.

Declares a new sort.

Defines a new sort.

Declares a new function symbol.

Declares a new constant.

Defines a new function symbol.

Defines some new (possibily mutually) recursive functions.

Defines a new recursive function.

Asserts an expression with some print information.

Get info command.

Get option command.

Set info command.

Echo command.

Parse success.

Implementors