Trait BottomUpBuilder

Source
pub trait BottomUpBuilder<'a, Ptr> {
Show 16 methods // Required methods fn true_ptr(&self) -> Ptr; fn false_ptr(&self) -> Ptr; fn var(&'a self, label: VarLabel, polarity: bool) -> Ptr; fn eq(&'a self, a: Ptr, b: Ptr) -> bool; fn and(&'a self, a: Ptr, b: Ptr) -> Ptr; fn negate(&'a self, f: Ptr) -> Ptr; fn ite(&'a self, f: Ptr, g: Ptr, h: Ptr) -> Ptr; fn iff(&'a self, a: Ptr, b: Ptr) -> Ptr; fn xor(&'a self, a: Ptr, b: Ptr) -> Ptr; fn exists(&'a self, f: Ptr, v: VarLabel) -> Ptr; fn condition(&'a self, a: Ptr, v: VarLabel, value: bool) -> Ptr; fn compile_cnf(&'a self, cnf: &Cnf) -> Ptr; // Provided methods fn or(&'a self, a: Ptr, b: Ptr) -> Ptr { ... } fn compose(&'a self, f: Ptr, lbl: VarLabel, g: Ptr) -> Ptr { ... } fn compile_logical_expr(&'a self, expr: &LogicalExpr) -> Ptr { ... } fn compile_plan(&'a self, expr: &BottomUpPlan) -> Ptr { ... }
}

Required Methods§

Source

fn true_ptr(&self) -> Ptr

Source

fn false_ptr(&self) -> Ptr

Source

fn var(&'a self, label: VarLabel, polarity: bool) -> Ptr

Source

fn eq(&'a self, a: Ptr, b: Ptr) -> bool

Test for semantic equality (not pointer/structural equality)

Source

fn and(&'a self, a: Ptr, b: Ptr) -> Ptr

Source

fn negate(&'a self, f: Ptr) -> Ptr

Source

fn ite(&'a self, f: Ptr, g: Ptr, h: Ptr) -> Ptr

if f then g else h

Source

fn iff(&'a self, a: Ptr, b: Ptr) -> Ptr

if and only if (i.e., Boolean equality)

Source

fn xor(&'a self, a: Ptr, b: Ptr) -> Ptr

logical exclusive-or

Source

fn exists(&'a self, f: Ptr, v: VarLabel) -> Ptr

existentially quantifies v out of f

Source

fn condition(&'a self, a: Ptr, v: VarLabel, value: bool) -> Ptr

conditions f | v = value

Source

fn compile_cnf(&'a self, cnf: &Cnf) -> Ptr

directly compile a CNF

Provided Methods§

Source

fn or(&'a self, a: Ptr, b: Ptr) -> Ptr

Compute the Boolean function f || g by default, or is defined using de morgan’s law as and

Source

fn compose(&'a self, f: Ptr, lbl: VarLabel, g: Ptr) -> Ptr

compose g into f for variable v I.e., computes the logical function (exists v. (g <=> v) /\ f).

Source

fn compile_logical_expr(&'a self, expr: &LogicalExpr) -> Ptr

directly compile a logical expression

Source

fn compile_plan(&'a self, expr: &BottomUpPlan) -> Ptr

Compiles from a BottomUpPlan, which represents a deferred computation

Implementors§

Source§

impl<'a, T> BottomUpBuilder<'a, BddPtr<'a>> for T
where T: BddBuilder<'a>,

Source§

impl<'a, T> BottomUpBuilder<'a, SddPtr<'a>> for T
where T: SddBuilder<'a>,