rsdd/builder/
mod.rs

1//! Contains the core datastructures for constructing and maintaining decision
2//! diagrams.
3
4pub mod cache;
5
6pub mod bdd;
7pub mod decision_nnf;
8pub mod sdd;
9
10use crate::{
11    plan::BottomUpPlan,
12    repr::{Cnf, LogicalExpr, VarLabel},
13};
14
15pub trait BottomUpBuilder<'a, Ptr> {
16    // constants --- can elide the input lifetimes
17    fn true_ptr(&self) -> Ptr;
18    fn false_ptr(&self) -> Ptr;
19
20    fn var(&'a self, label: VarLabel, polarity: bool) -> Ptr;
21
22    // primitive operations
23
24    /// Test for *semantic equality* (not pointer/structural equality)
25    fn eq(&'a self, a: Ptr, b: Ptr) -> bool;
26
27    fn and(&'a self, a: Ptr, b: Ptr) -> Ptr;
28
29    /// Compute the Boolean function `f || g`
30    /// by default, or is defined using de morgan's law as and
31    fn or(&'a self, a: Ptr, b: Ptr) -> Ptr {
32        self.negate(self.and(self.negate(a), self.negate(b)))
33    }
34    fn negate(&'a self, f: Ptr) -> Ptr;
35
36    /// if f then g else h
37    fn ite(&'a self, f: Ptr, g: Ptr, h: Ptr) -> Ptr;
38
39    /// if and only if (i.e., Boolean equality)
40    fn iff(&'a self, a: Ptr, b: Ptr) -> Ptr;
41
42    /// logical exclusive-or
43    fn xor(&'a self, a: Ptr, b: Ptr) -> Ptr;
44
45    /// existentially quantifies `v` out of `f`
46    fn exists(&'a self, f: Ptr, v: VarLabel) -> Ptr;
47
48    /// conditions f | v = value
49    fn condition(&'a self, a: Ptr, v: VarLabel, value: bool) -> Ptr;
50
51    /// compose g into f for variable v
52    /// I.e., computes the logical function (exists v. (g <=> v) /\ f).
53    fn compose(&'a self, f: Ptr, lbl: VarLabel, g: Ptr) -> Ptr {
54        // TODO this can be optimized with a specialized implementation to make
55        // it a single traversal
56        let var = self.var(lbl, true);
57        let iff = self.iff(var, g);
58        let a = self.and(iff, f);
59
60        self.exists(a, lbl)
61    }
62
63    // compilation
64
65    /// directly compile a CNF
66    fn compile_cnf(&'a self, cnf: &Cnf) -> Ptr;
67
68    /// directly compile a logical expression
69    fn compile_logical_expr(&'a self, expr: &LogicalExpr) -> Ptr {
70        match &expr {
71            LogicalExpr::Literal(lbl, polarity) => self.var(VarLabel::new(*lbl as u64), *polarity),
72            LogicalExpr::And(ref l, ref r) => {
73                let r1 = self.compile_logical_expr(l);
74                let r2 = self.compile_logical_expr(r);
75                self.and(r1, r2)
76            }
77            LogicalExpr::Or(ref l, ref r) => {
78                let r1 = self.compile_logical_expr(l);
79                let r2 = self.compile_logical_expr(r);
80                self.or(r1, r2)
81            }
82            LogicalExpr::Not(ref e) => self.negate(self.compile_logical_expr(e)),
83            LogicalExpr::Iff(ref l, ref r) => {
84                let r1 = self.compile_logical_expr(l);
85                let r2 = self.compile_logical_expr(r);
86                self.iff(r1, r2)
87            }
88            LogicalExpr::Xor(ref l, ref r) => {
89                let r1 = self.compile_logical_expr(l);
90                let r2 = self.compile_logical_expr(r);
91                self.xor(r1, r2)
92            }
93            LogicalExpr::Ite {
94                ref guard,
95                ref thn,
96                ref els,
97            } => {
98                let g = self.compile_logical_expr(guard);
99                let t = self.compile_logical_expr(thn);
100                let e = self.compile_logical_expr(els);
101                self.ite(g, t, e)
102            }
103        }
104    }
105
106    /// Compiles from a BottomUpPlan, which represents a deferred computation
107    fn compile_plan(&'a self, expr: &BottomUpPlan) -> Ptr {
108        match &expr {
109            BottomUpPlan::Literal(var, polarity) => self.var(*var, *polarity),
110            BottomUpPlan::And(ref l, ref r) => {
111                let r1 = self.compile_plan(l);
112                let r2 = self.compile_plan(r);
113                self.and(r1, r2)
114            }
115            BottomUpPlan::Or(ref l, ref r) => {
116                let r1 = self.compile_plan(l);
117                let r2 = self.compile_plan(r);
118                self.or(r1, r2)
119            }
120            BottomUpPlan::Iff(ref l, ref r) => {
121                let r1 = self.compile_plan(l);
122                let r2 = self.compile_plan(r);
123                self.iff(r1, r2)
124            }
125            BottomUpPlan::Ite(ref f, ref g, ref h) => {
126                let f = self.compile_plan(f);
127                let g = self.compile_plan(g);
128                let h = self.compile_plan(h);
129                self.ite(f, g, h)
130            }
131            BottomUpPlan::Not(ref f) => {
132                let f = self.compile_plan(f);
133                self.negate(f)
134            }
135            BottomUpPlan::ConstTrue => self.true_ptr(),
136            BottomUpPlan::ConstFalse => self.false_ptr(),
137        }
138    }
139}
140
141pub trait TopDownBuilder<'a, Ptr> {
142    fn var(&'a self, label: VarLabel, polarity: bool) -> Ptr;
143
144    /// conditions f | v = value
145    fn condition(&'a self, a: Ptr, v: VarLabel, value: bool) -> Ptr;
146}
rsdd/builder/mod.rs

rsdd/builder/
mod.rs
