From a32ccd649db3771f87d833e83b59e2fa4eeff836 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 20 Oct 2016 20:59:28 +0200
Subject: [PATCH] [buddy] slight optimization of bdd_implies

* src/bddop.c: Avoid the first recursion when it is obvious that the
second will fail.
---
 buddy/src/bddop.c | 21 ++++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c
index 74ae5bce1..82bd45d80 100644
--- a/buddy/src/bddop.c
+++ b/buddy/src/bddop.c
@@ -931,15 +931,30 @@ int bdd_implies(BDD l, BDD r)
 
   if (LEVEL(l) == LEVEL(r))
     {
-      res = bdd_implies(LOW(l), LOW(r)) && bdd_implies(HIGH(l), HIGH(r));
+      int hl = HIGH(l);
+      int hr = HIGH(r);
+      // Avoid the recursion if the second implication will trivially
+      // fail.
+      if ((ISONE(hl) || ISZERO(hr)) && (hl != hr))
+        res = 0;
+      else
+        res = bdd_implies(LOW(l), LOW(r)) && bdd_implies(hl, hr);
     }
   else if (LEVEL(l) < LEVEL(r))
     {
-      res = bdd_implies(LOW(l), r) && bdd_implies(HIGH(l), r);
+      int hl = HIGH(l);
+      if (ISONE(hl) && (hl != r))
+        res = 0;
+      else
+        res = bdd_implies(LOW(l), r) && bdd_implies(HIGH(l), r);
     }
   else /* LEVEL(l) > LEVEL(r) */
     {
-      res = bdd_implies(l, LOW(r)) && bdd_implies(l, HIGH(r));
+      int hr = HIGH(r);
+      if (ISZERO(hr) && (hr != r))
+        res = 0;
+      else
+        res = bdd_implies(l, LOW(r)) && bdd_implies(l, HIGH(r));
     }
 
   entry->i.a = l;