Trait rsmt2::print::Expr2Smt

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

An expression printable in the SMT Lib 2 standard given some info.

Required methods

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

Prints an expression to a writer given some info.

Loading content...

Implementations on Foreign Types

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

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

impl<T> Expr2Smt<T> for str

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

impl<T> Expr2Smt<T> for String

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

Loading content...

Implementors

impl Expr2Smt<()> for Const

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

impl Expr2Smt<()> for Expr

pub fn expr_to_smt2<Writer>(&self, w: &mut Writer, _: ()) -> SmtRes<()> where
    Writer: Write, 

impl Expr2Smt<()> for Actlit

pub fn expr_to_smt2<Writer>(&self, w: &mut Writer, _: ()) -> SmtRes<()> where
    Writer: Write, 

impl<'a> Expr2Smt<&'a Offset> for SExpr

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

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

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

impl<'a, 'b> Expr2Smt<()> for Unrolled<'a, &'b SExpr>

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

impl<'a, V: AsRef<Var>> Expr2Smt<()> for Unrolled<'a, V>

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

Loading content...