alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[buddy] introduce bdd_stable_cmp

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2021-06-10 17:59:38 +02:00
parent edfcd5b0d8
commit 9ed2682f67
2 changed files with 33 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
buddy/src/bddx.h
View file

@ -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; }

28
buddy/src/kernel.c
View file

@ -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