From 9ed2682f6741953276395843efa8615ce819c571 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 10 Jun 2021 17:59:38 +0200
Subject: [PATCH] [buddy] introduce bdd_stable_cmp

* src/bddx.h, misc/bddlt.hh (bdd_stable_cmp): Define this
new function, based on some code that was implemented in Spot, but was
unnecessarily doing reference counting.
---
 buddy/src/bddx.h   |  7 ++++++-
 buddy/src/kernel.c | 28 +++++++++++++++++++++++++++-
 2 files changed, 33 insertions(+), 2 deletions(-)

diff --git a/buddy/src/bddx.h b/buddy/src/bddx.h
index 6ac521939..4deef3497 100644
--- a/buddy/src/bddx.h
+++ b/buddy/src/bddx.h
@@ -1,5 +1,5 @@
 /*========================================================================
-	       Copyright (C) 1996-2003 by Jorn Lind-Nielsen
+	       Copyright (C) 1996-2003, 2021 by Jorn Lind-Nielsen
 			    All rights reserved
 
     Permission is hereby granted, without written agreement and without
@@ -335,6 +335,7 @@ BUDDY_API int      bdd_setbddpair(bddPair*, int, BDD);
 BUDDY_API int      bdd_setbddpairs(bddPair*, int*, BDD*, int);
 BUDDY_API void     bdd_resetpair(bddPair *);
 BUDDY_API void     bdd_freepair(bddPair*);
+BUDDY_API int      bdd_stable_cmp(BDD, BDD);
 
   /* In bddop.c */
 
@@ -593,6 +594,7 @@ protected:
    friend bdd      bdd_makesetpp(int *, int);
    friend int      bdd_setbddpair(bddPair*, int, const bdd &);
    friend int      bdd_setbddpairs(bddPair*, int*, const bdd *, int);
+   friend int      bdd_stable_cmp(const bdd&, const bdd&);
    friend bdd      bdd_from_int(int i);
    friend bdd      bdd_buildcube(int, int, const bdd *);
    friend bdd      bdd_ibuildcubepp(int, int, int *);
@@ -742,6 +744,9 @@ inline bdd bdd_makesetpp(int *v, int n)
 inline int bdd_setbddpair(bddPair *p, int ov, const bdd &nv)
 { return bdd_setbddpair(p,ov,nv.root); }
 
+inline int bdd_stable_cmp(const bdd&l, const bdd& r)
+{ return bdd_stable_cmp(l.root, r.root); }
+
 inline bdd bdd_from_int(int i)
 { return i; }
 
diff --git a/buddy/src/kernel.c b/buddy/src/kernel.c
index 2cef6db0e..96d95c284 100644
--- a/buddy/src/kernel.c
+++ b/buddy/src/kernel.c
@@ -1,5 +1,5 @@
 /*========================================================================
-	       Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+	       Copyright (C) 1996-2002, 2021 by Jorn Lind-Nielsen
 			    All rights reserved
 
     Permission is hereby granted, without written agreement and without
@@ -1018,6 +1018,32 @@ BDD bdd_high(BDD root)
 }
 
 
+int bdd_stable_cmp(BDD left, BDD right)
+{
+  for (;;)
+    {
+      if (left == right || ISCONST(left) || ISCONST(right))
+        return left - right;
+      int vl = bddlevel2var[LEVEL(left)];
+      int vr = bddlevel2var[LEVEL(right)];
+      if (vl != vr)
+        return vr - vl;
+      // We check the high side before low, this way
+      //  !a&b comes before a&!b and a&b
+      BDD dl = HIGH(left);
+      BDD dr = HIGH(right);
+      if (dl != dr)
+        {
+          left = dl;
+          right = dr;
+        }
+      else
+        {
+          left = LOW(left);
+          right = LOW(right);
+        }
+    }
+}
 
 /*************************************************************************
   Garbage collection and node referencing