Trait rsmt2::internals::SolverBasic [−] [src]

pub trait SolverBasic<'kid, Parser: ParseSmt2 + 'static> {
    fn fetch(&mut self) -> Res<()>;
    fn write<F: Fn(&mut Write) -> Res<()>>(&mut self, f: F) -> Res<()>;
    fn comment(&mut self, txt: &str) -> Res<()>;
    fn as_ref(&self) -> &[u8];
    fn parser(&self) -> &Parser;
    fn solver(&mut self) -> &mut PlainSolver<'kid, Parser>;
}

Most basic function needed to provide SMT-LIB commands.

Required Methods

`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, txt: &str) -> Res<()>`

Writes comments. Ignored for PlainSolver.

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

The bytes of the buffer.

`fn parser(&self) -> &Parser`

The parser.

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

The plain solver.

Implementors

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