Struct rsmt2::NamedExpr

pub struct NamedExpr<Sym, Expr> { /* fields omitted */ }

Wraps an expression and a symbol. Symbol is understood as the name of the expression.

use rsmt2::prelude::*;
let mut conf = SmtConf::default_z3();
conf.unsat_cores();

let mut solver = Solver::new(conf, ()).unwrap();
solver.declare_const("n", "Int").unwrap();
solver.declare_const("m", "Int").unwrap();

solver.assert("true").unwrap();

let e_1 = "(> n 7)";
let label_e_1 = "e_1";
let named = NamedExpr::new(label_e_1, e_1);
solver.assert(&named).unwrap();

let e_2 = "(and (> m n) (< m 7))";
let label_e_2 = "e_2";
let named = NamedExpr::new(label_e_2, e_2);
solver.assert(&named).unwrap();

assert!(!solver.check_sat().unwrap());
let core: Vec<String> = solver.get_unsat_core().unwrap();
assert_eq!(core, vec![label_e_1, label_e_2]);

Implementations

impl<Sym, Expr> NamedExpr<Sym, Expr>

pub fn new(sym: Sym, expr: Expr) -> Self

Constructor.

Trait Implementations

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

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

Prints an expression to a writer given some info.