pub struct NamedExpr<Sym, Expr, Info> { /* private fields */ }
Expand description
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
Trait Implementations
sourceimpl<Sym, Expr, Info> Expr2Smt<Info> for NamedExpr<Sym, Expr, Info>where
Sym: Sym2Smt<()>,
Expr: Expr2Smt<Info>,
impl<Sym, Expr, Info> Expr2Smt<Info> for NamedExpr<Sym, Expr, Info>where
Sym: Sym2Smt<()>,
Expr: Expr2Smt<Info>,
Auto Trait Implementations
impl<Sym, Expr, Info> RefUnwindSafe for NamedExpr<Sym, Expr, Info>where
Expr: RefUnwindSafe,
Info: RefUnwindSafe,
Sym: RefUnwindSafe,
impl<Sym, Expr, Info> Send for NamedExpr<Sym, Expr, Info>where
Expr: Send,
Info: Send,
Sym: Send,
impl<Sym, Expr, Info> Sync for NamedExpr<Sym, Expr, Info>where
Expr: Sync,
Info: Sync,
Sym: Sync,
impl<Sym, Expr, Info> Unpin for NamedExpr<Sym, Expr, Info>where
Expr: Unpin,
Info: Unpin,
Sym: Unpin,
impl<Sym, Expr, Info> UnwindSafe for NamedExpr<Sym, Expr, Info>where
Expr: UnwindSafe,
Info: UnwindSafe,
Sym: UnwindSafe,
Blanket Implementations
sourceimpl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more