Trait rsmt2::print::Expr2Smt

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

    fn to_smt_named<Sym>(self, name: Sym) -> NamedExpr<Sym, Self, Info>
    where
        Sym: Sym2Smt,
        Self: Sized,
    { ... }
    fn as_smt_named<Sym>(&self, name: Sym) -> NamedExpr<Sym, &Self, Info>
    where
        Sym: Sym2Smt,
        Self: Sized,
    { ... }
}

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

Required Methods

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

Prints an expression to a writer given some info.

Provided Methods

fn to_smt_named<Sym>(self, name: Sym) -> NamedExpr<Sym, Self, Info> where
    Sym: Sym2Smt,
    Self: Sized, 

Gives a name to an expression (owned version).

fn as_smt_named<Sym>(&self, name: Sym) -> NamedExpr<Sym, &Self, Info> where
    Sym: Sym2Smt,
    Self: Sized, 

Gives a name to an expression (borrowed version).

Implementations on Foreign Types

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

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

impl<T> Expr2Smt<T> for str

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

impl<T> Expr2Smt<T> for String

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

Implementors

impl Expr2Smt<()> for Const

impl Expr2Smt<()> for Expr

impl Expr2Smt<()> for Actlit

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

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

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

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

impl<Expr, Info> Expr2Smt<Info> for CondExpr<Expr> where
    Expr: Expr2Smt<Info>, 

impl<Sym, Expr, Info> Expr2Smt<Info> for NamedExpr<Sym, Expr, Info> where
    Sym: Sym2Smt<()>,
    Expr: Expr2Smt<Info>,