Merge pull request #43 from timbeurskens/or-operator-optimization

Or operator optimization

Author: timbeurskens

Cargo.lock

@@ -1,6 +1,6 @@
 [package]
 name = "rsbdd"
-version = "0.9.2"
+version = "0.9.3"
 edition = "2021"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

Cargo.toml

@@ -260,6 +260,40 @@ impl<S: BDDSymbol> BDDEnv<S> {
         }
     }
 
+    // disjunction
+    pub fn or(&self, a: Rc<BDD<S>>, b: Rc<BDD<S>>) -> Rc<BDD<S>> {
+        // self.not(self.nor(a, b))
+
+        match (a.as_ref(), b.as_ref()) {
+            (&BDD::True, _) | (_, &BDD::True) => self.mk_const(true),
+            (&BDD::False, _) => Rc::clone(&b),
+            (_, &BDD::False) => Rc::clone(&a),
+            // todo:
+            (&BDD::Choice(ref at, ref va, ref af), &BDD::Choice(_, ref vb, _)) if va < vb => self
+                .mk_choice(
+                    self.or(Rc::clone(at), Rc::clone(&b)),
+                    va.clone(),
+                    self.or(Rc::clone(af), Rc::clone(&b)),
+                ),
+            (&BDD::Choice(_, ref va, _), &BDD::Choice(ref bt, ref vb, ref bf)) if vb < va => self
+                .mk_choice(
+                    self.or(Rc::clone(bt), Rc::clone(&a)),
+                    vb.clone(),
+                    self.or(Rc::clone(bf), Rc::clone(&a)),
+                ),
+            (&BDD::Choice(ref at, ref va, ref af), &BDD::Choice(ref bt, ref vb, ref bf))
+                if va == vb =>
+            {
+                self.mk_choice(
+                    self.or(Rc::clone(at), Rc::clone(bt)),
+                    va.clone(),
+                    self.or(Rc::clone(af), Rc::clone(bf)),
+                )
+            }
+            _ => panic!("unsupported match: {:?} {:?}", a, b),
+        }
+    }
+
     pub fn not(&self, a: Rc<BDD<S>>) -> Rc<BDD<S>> {
         match *a.as_ref() {
             BDD::False => self.mk_const(true),
@@ -290,11 +324,6 @@ impl<S: BDDSymbol> BDDEnv<S> {
         )
     }
 
-    // disjunction
-    pub fn or(&self, a: Rc<BDD<S>>, b: Rc<BDD<S>>) -> Rc<BDD<S>> {
-        self.not(self.nor(a, b))
-    }
-
     // exclusive disjunction
     pub fn xor(&self, a: Rc<BDD<S>>, b: Rc<BDD<S>>) -> Rc<BDD<S>> {
         self.or(