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,
{ ... }
}
Expand description
An expression printable in the SMT-LIB 2 standard given some info.
Required Methods
Provided Methods
sourcefn to_smt_named<Sym>(self, name: Sym) -> NamedExpr<Sym, Self, Info>where
Sym: Sym2Smt,
Self: Sized,
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).