Trait rsmt2_zz::print::Sym2Smt

pub trait Sym2Smt<Info> {
    fn sym_to_smt2<Writer>(&self, w: &mut Writer, i: Info) -> SmtRes<()>
    where
        Writer: Write;
}

A symbol printable in the SMT Lib 2 standard given some info.

Required methods

fn sym_to_smt2<Writer>(&self, w: &mut Writer, i: Info) -> SmtRes<()> where
    Writer: Write, 

Prints a symbol to a writer given some info.

Loading content...

Implementations on Foreign Types

impl<'a, T: ?Sized, Info> Sym2Smt<Info> for &'a T where
    T: Sym2Smt<Info>, 

fn sym_to_smt2<Writer>(&self, writer: &mut Writer, info: Info) -> SmtRes<()> where
    Writer: Write, 

impl<T> Sym2Smt<T> for str

fn sym_to_smt2<Writer>(&self, writer: &mut Writer, _: T) -> SmtRes<()> where
    Writer: Write, 

impl<T> Sym2Smt<T> for String

fn sym_to_smt2<Writer>(&self, writer: &mut Writer, _: T) -> SmtRes<()> where
    Writer: Write, 

Loading content...

Implementors

impl<'a> Sym2Smt<&'a Offset> for Var

fn sym_to_smt2<Writer: Write>(
    &self,
    writer: &mut Writer,
    off: &'a Offset
) -> SmtRes<()>

impl<'a, 'b> Sym2Smt<()> for Unrolled<'a, &'b Var>

fn sym_to_smt2<Writer: Write>(&self, writer: &mut Writer, _: ()) -> SmtRes<()>

Loading content...