Trait rsmt2::to_smt::Sym2Smt

pub trait Sym2Smt<Info> {
    fn sym_to_smt2<Writer>(&self, _: &mut Writer, _: 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, _: &mut Writer, _: Info) -> SmtRes<()> where
    Writer: Write, 

Prints a symbol to a writer given some info.

Implementations on Foreign Types

impl<'a, T> Sym2Smt<T> for &'a str

fn sym_to_smt2<Writer>(&self, writer: &mut Writer, _: T) -> 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<'a> Sym2Smt<&'a Offset> for Var
• impl<'a, 'b> Sym2Smt<()> for Unrolled<'a, &'b Var>