Trait rsmt2::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.

Implementations on Foreign Types

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

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, 

Implementors

impl Sym2Smt<()> for Actlit

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

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