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§
fn true_ptr(&self) -> Ptr
fn false_ptr(&self) -> Ptr
fn var(&'a self, label: VarLabel, polarity: bool) -> Ptr
Sourcefn eq(&'a self, a: Ptr, b: Ptr) -> bool
fn eq(&'a self, a: Ptr, b: Ptr) -> bool
Test for semantic equality (not pointer/structural equality)
fn and(&'a self, a: Ptr, b: Ptr) -> Ptr
fn negate(&'a self, f: Ptr) -> Ptr
Sourcefn compile_cnf(&'a self, cnf: &Cnf) -> Ptr
fn compile_cnf(&'a self, cnf: &Cnf) -> Ptr
directly compile a CNF
Provided Methods§
Sourcefn or(&'a self, a: Ptr, b: Ptr) -> Ptr
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
Sourcefn compose(&'a self, f: Ptr, lbl: VarLabel, g: Ptr) -> Ptr
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).
Sourcefn compile_logical_expr(&'a self, expr: &LogicalExpr) -> Ptr
fn compile_logical_expr(&'a self, expr: &LogicalExpr) -> Ptr
directly compile a logical expression
Sourcefn compile_plan(&'a self, expr: &BottomUpPlan) -> Ptr
fn compile_plan(&'a self, expr: &BottomUpPlan) -> Ptr
Compiles from a BottomUpPlan, which represents a deferred computation