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>