alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/buddy/src/reorder.c
Alexandre Duret-Lutz 1ffdd57383 [buddy] backport some fixes from upstream 
* src/fdd.c, src/imatrix.c, src/kernel.c, src/reorder.c: Here.
2015-03-11 23:45:00 +01:00

2321 lines
54 KiB
C
Raw Blame History

/*========================================================================
Copyright (C) 1996-2002 by Jorn Lind-Nielsen
All rights reserved
Permission is hereby granted, without written agreement and without
license or royalty fees, to use, reproduce, prepare derivative
works, distribute, and display this software and its documentation
for any purpose, provided that (1) the above copyright notice and
the following two paragraphs appear in all copies of the source code
and (2) redistributions, including without limitation binaries,
reproduce these notices in the supporting documentation. Substantial
modifications to this software may be copyrighted by their authors
and need not follow the licensing terms described here, provided
that the new terms are clearly indicated in all files where they apply.
IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
MODIFICATIONS.
========================================================================*/
/*************************************************************************
$Header: /Volumes/CVS/repository/spot/spot/buddy/src/reorder.c,v 1.2 2003/05/05 13:45:08 aduret Exp $
FILE: reorder.c
DESCR: BDD reordering functions
AUTH: Jorn Lind
DATE: (C) january 1998
*************************************************************************/
#include <stdlib.h>
#include <string.h>
#include <time.h>
#include <math.h>
#include <assert.h>
#include "kernel.h"
#include "bddtree.h"
#include "imatrix.h"
#include "prime.h"
/* IMPORTANT:
* The semantics of the "level" field in the BddNode struct changes during
* variable reordering in order to make a fast variable swap possible when
* two variables are independent. Instead of refering to the level of the node
* it refers to the *variable* !!!
*/
/* Change macros to reflect the above idea */
#define VAR(n) (bddnodes[n].level)
#define VARp(p) (p->level)
/* Avoid these - they are misleading! */
#undef LEVEL
#undef LEVELp
#define __USERESIZE /* FIXME */
/* Current auto reord. method and number of automatic reorderings left */
static int bddreordermethod;
static int bddreordertimes;
/* Flag for disabling reordering temporarily */
static int reorderdisabled;
/* Store for the variable relationships */
static BddTree *vartree;
static int blockid;
/* Store for the ref.cou. of the external roots */
static int *extroots;
static int extrootsize;
/* Level data */
typedef struct _levelData
{
int start; /* Start of this sub-table (entry in "bddnodes") */
int size; /* Size of this sub-table */
int maxsize; /* Max. allowed size of sub-table */
int nodenum; /* Number of nodes in this level */
} levelData;
static levelData *levels; /* Indexed by variable! */
/* Interaction matrix */
static imatrix *iactmtx;
/* Reordering information for the user */
static int verbose;
static bddinthandler reorder_handler;
static bddfilehandler reorder_filehandler;
static bddsizehandler reorder_nodenum;
/* Number of live nodes before and after a reordering session */
static int usednum_before;
static int usednum_after;
/* Kernel variables needed for reordering */
extern int bddfreepos;
extern int bddfreenum;
extern long int bddproduced;
/* Flag telling us when a node table resize is done */
static int resizedInMakenode;
/* New node hashing function for use with reordering */
#define NODEHASH(var,l,h) ((PAIR((l),(h))%levels[var].size)+levels[var].start)
/* Reordering prototypes */
static void blockdown(BddTree *);
static void addref_rec(int, char *);
static void reorder_gbc(void);
static void reorder_setLevellookup(void);
static int reorder_makenode(int, int, int);
static int reorder_varup(int);
static int reorder_vardown(int);
static int reorder_init(void);
static void reorder_done(void);
#define random(a) (rand() % (a))
/* For sorting the blocks according to some specific size value */
typedef struct s_sizePair
{
int val;
BddTree *block;
} sizePair;
/*************************************************************************
Initialize and shutdown
*************************************************************************/
void bdd_reorder_init(void)
{
reorderdisabled = 0;
vartree = NULL;
bdd_clrvarblocks();
bdd_reorder_hook(bdd_default_reohandler);
bdd_reorder_verbose(0);
bdd_autoreorder_times(BDD_REORDER_NONE, 0);
reorder_nodenum = bdd_getnodenum;
usednum_before = usednum_after = 0;
blockid = 0;
}
void bdd_reorder_done(void)
{
bddtree_del(vartree);
bdd_operator_reset();
vartree = NULL;
}
/*************************************************************************
Reordering heuristics
*************************************************************************/
/*=== Reorder using a sliding window of size 2 =========================*/
static BddTree *reorder_win2(BddTree *t)
{
BddTree *this=t, *first=t;
if (t == NULL)
return t;
if (verbose > 1)
printf("Win2 start: %d nodes\n", reorder_nodenum());
fflush(stdout);
while (this->next != NULL)
{
int best = reorder_nodenum();
blockdown(this);
if (best < reorder_nodenum())
{
blockdown(this->prev);
this = this->next;
}
else
if (first == this)
first = this->prev;
if (verbose > 1)
{
printf(".");
fflush(stdout);
}
}
if (verbose > 1)
printf("\nWin2 end: %d nodes\n", reorder_nodenum());
fflush(stdout);
return first;
}
static BddTree *reorder_win2ite(BddTree *t)
{
BddTree *this, *first=t;
int lastsize;
int c=1;
if (t == NULL)
return t;
if (verbose > 1)
printf("Win2ite start: %d nodes\n", reorder_nodenum());
do
{
lastsize = reorder_nodenum();
this = t;
while (this->next != NULL)
{
int best = reorder_nodenum();
blockdown(this);
if (best < reorder_nodenum())
{
blockdown(this->prev);
this = this->next;
}
else
if (first == this)
first = this->prev;
if (verbose > 1)
{
printf(".");
fflush(stdout);
}
}
if (verbose > 1)
printf(" %d nodes\n", reorder_nodenum());
c++;
}
while (reorder_nodenum() != lastsize);
return first;
}
/*=== Reorder using a sliding window of size 3 =========================*/
#define X(a)
static BddTree *reorder_swapwin3(BddTree *this, BddTree **first)
{
int setfirst = (this->prev == NULL ? 1 : 0);
BddTree *next = this;
int best = reorder_nodenum();
if (this->next->next == NULL) /* Only two blocks left -> win2 swap */
{
blockdown(this);
if (best < reorder_nodenum())
{
blockdown(this->prev);
next = this->next;
}
else
{
next = this;
if (setfirst)
*first = this->prev;
}
}
else /* Real win3 swap */
{
int pos = 0;
X(printf("%d: ", reorder_nodenum()));
blockdown(this); /* B A* C (4) */
X(printf("A"));
pos++;
if (best > reorder_nodenum())
{
X(printf("(%d)", reorder_nodenum()));
pos = 0;
best = reorder_nodenum();
}
blockdown(this); /* B C A* (3) */
X(printf("B"));
pos++;
if (best > reorder_nodenum())
{
X(printf("(%d)", reorder_nodenum()));
pos = 0;
best = reorder_nodenum();
}
this = this->prev->prev;
blockdown(this); /* C B* A (2) */
X(printf("C"));
pos++;
if (best > reorder_nodenum())
{
X(printf("(%d)", reorder_nodenum()));
pos = 0;
best = reorder_nodenum();
}
blockdown(this); /* C A B* (1) */
X(printf("D"));
pos++;
if (best > reorder_nodenum())
{
X(printf("(%d)", reorder_nodenum()));
pos = 0;
best = reorder_nodenum();
}
this = this->prev->prev;
blockdown(this); /* A C* B (0)*/
X(printf("E"));
pos++;
if (best > reorder_nodenum())
{
X(printf("(%d)", reorder_nodenum()));
pos = 0;
best = reorder_nodenum();
}
X(printf(" -> "));
if (pos >= 1) /* A C B -> C A* B */
{
this = this->prev;
blockdown(this);
next = this;
if (setfirst)
*first = this->prev;
X(printf("a(%d)", reorder_nodenum()));
}
if (pos >= 2) /* C A B -> C B A* */
{
blockdown(this);
next = this->prev;
if (setfirst)
*first = this->prev->prev;
X(printf("b(%d)", reorder_nodenum()));
}
if (pos >= 3) /* C B A -> B C* A */
{
this = this->prev->prev;
blockdown(this);
next = this;
if (setfirst)
*first = this->prev;
X(printf("c(%d)", reorder_nodenum()));
}
if (pos >= 4) /* B C A -> B A C* */
{
blockdown(this);
next = this->prev;
if (setfirst)
*first = this->prev->prev;
X(printf("d(%d)", reorder_nodenum()));
}
if (pos >= 5) /* B A C -> A B* C */
{
this = this->prev->prev;
blockdown(this);
next = this;
if (setfirst)
*first = this->prev;
X(printf("e(%d)", reorder_nodenum()));
}
X(printf("\n"));
}
return next;
}
static BddTree *reorder_win3(BddTree *t)
{
BddTree *this=t, *first=t;
if (t == NULL)
return t;
if (verbose > 1)
printf("Win3 start: %d nodes\n", reorder_nodenum());
fflush(stdout);
while (this->next != NULL)
{
this = reorder_swapwin3(this, &first);
if (verbose > 1)
{
printf(".");
fflush(stdout);
}
}
if (verbose > 1)
printf("\nWin3 end: %d nodes\n", reorder_nodenum());
fflush(stdout);
return first;
}
static BddTree *reorder_win3ite(BddTree *t)
{
BddTree *this, *first=t;
int lastsize;
if (t == NULL)
return t;
if (verbose > 1)
printf("Win3ite start: %d nodes\n", reorder_nodenum());
do
{
lastsize = reorder_nodenum();
this = first;
while (this->next != NULL && this->next->next != NULL)
{
this = reorder_swapwin3(this, &first);
if (verbose > 1)
{
printf(".");
fflush(stdout);
}
}
if (verbose > 1)
printf(" %d nodes\n", reorder_nodenum());
}
while (reorder_nodenum() != lastsize);
if (verbose > 1)
printf("Win3ite end: %d nodes\n", reorder_nodenum());
return first;
}
/*=== Reorder by sifting =============================================*/
/* Move a specific block up and down in the order and place at last in
the best position
*/
static void reorder_sift_bestpos(BddTree *blk, int middlePos)
{
int best = reorder_nodenum();
int maxAllowed;
int bestpos = 0;
int dirIsUp = 1;
int n;
if (bddmaxnodesize > 0)
maxAllowed = MIN(best/5+best, bddmaxnodesize-bddmaxnodeincrease-2);
else
maxAllowed = best/5+best;
/* Determine initial direction */
if (blk->pos > middlePos)
dirIsUp = 0;
/* Move block back and forth */
for (n=0 ; n<2 ; n++)
{
int first = 1;
if (dirIsUp)
{
while (blk->prev != NULL &&
(reorder_nodenum() <= maxAllowed || first))
{
first = 0;
blockdown(blk->prev);
bestpos--;
if (verbose > 1)
{
printf("-");
fflush(stdout);
}
if (reorder_nodenum() < best)
{
best = reorder_nodenum();
bestpos = 0;
if (bddmaxnodesize > 0)
maxAllowed = MIN(best/5+best,
bddmaxnodesize-bddmaxnodeincrease-2);
else
maxAllowed = best/5+best;
}
}
}
else
{
while (blk->next != NULL &&
(reorder_nodenum() <= maxAllowed || first))
{
first = 0;
blockdown(blk);
bestpos++;
if (verbose > 1)
{
printf("+");
fflush(stdout);
}
if (reorder_nodenum() < best)
{
best = reorder_nodenum();
bestpos = 0;
if (bddmaxnodesize > 0)
maxAllowed = MIN(best/5+best,
bddmaxnodesize-bddmaxnodeincrease-2);
else
maxAllowed = best/5+best;
}
}
}
if (reorder_nodenum() > maxAllowed && verbose > 1)
{
printf("!");
fflush(stdout);
}
dirIsUp = !dirIsUp;
}
/* Move to best pos */
while (bestpos < 0)
{
blockdown(blk);
bestpos++;
}
while (bestpos > 0)
{
blockdown(blk->prev);
bestpos--;
}
}
/* Go through all blocks in a specific sequence and find best
position for each of them
*/
static BddTree *reorder_sift_seq(BddTree *t, BddTree **seq, int num)
{
BddTree *this;
int n;
if (t == NULL)
return t;
for (n=0 ; n<num ; n++)
{
long c2, c1 = clock();
if (verbose > 1)
{
printf("Sift ");
if (reorder_filehandler)
reorder_filehandler(stdout, seq[n]->id);
else
printf("%d", seq[n]->id);
printf(": ");
}
reorder_sift_bestpos(seq[n], num/2);
if (verbose > 1)
printf("\n> %d nodes", reorder_nodenum());
c2 = clock();
if (verbose > 1)
printf(" (%.1f sec)\n", (float)(c2-c1)/CLOCKS_PER_SEC);
}
/* Find first block */
for (this=t ; this->prev != NULL ; this=this->prev)
/* nil */;
return this;
}
/* Compare function for sorting sifting sequence
*/
static int siftTestCmp(const void *aa, const void *bb)
{
const sizePair *a = (const sizePair*)aa;
const sizePair *b = (const sizePair*)bb;
if (a->val < b->val)
return -1;
if (a->val > b->val)
return 1;
return 0;
}
/* Find sifting sequence based on the number of nodes at each level
*/
static BddTree *reorder_sift(BddTree *t)
{
BddTree *this, **seq;
sizePair *p;
int n, num;
for (this=t,num=0 ; this!=NULL ; this=this->next)
this->pos = num++;
if ((p=NEW(sizePair,num)) == NULL)
return t;
if ((seq=NEW(BddTree*,num)) == NULL)
{
free(p);
return t;
}
for (this=t,n=0 ; this!=NULL ; this=this->next,n++)
{
int v;
/* Accumulate number of nodes for each block */
p[n].val = 0;
for (v=this->first ; v<=this->last ; v++)
p[n].val -= levels[v].nodenum;
p[n].block = this;
}
/* Sort according to the number of nodes at each level */
qsort(p, num, sizeof(sizePair), siftTestCmp);
/* Create sequence */
for (n=0 ; n<num ; n++)
seq[n] = p[n].block;
/* Do the sifting on this sequence */
t = reorder_sift_seq(t, seq, num);
free(seq);
free(p);
return t;
}
/* Do sifting iteratively until no more improvement can be found
*/
static BddTree *reorder_siftite(BddTree *t)
{
BddTree *first=t;
int lastsize;
int c=1;
if (t == NULL)
return t;
do
{
if (verbose > 1)
printf("Reorder %d\n", c++);
lastsize = reorder_nodenum();
first = reorder_sift(first);
}
while (reorder_nodenum() != lastsize);
return first;
}
/*=== Random reordering (mostly for debugging and test ) =============*/
static BddTree *reorder_random(BddTree *t)
{
BddTree *this;
BddTree **seq;
int n, num=0;
if (t == NULL)
return t;
for (this=t ; this!=NULL ; this=this->next)
num++;
seq = NEW(BddTree*,num);
for (this=t,num=0 ; this!=NULL ; this=this->next)
seq[num++] = this;
for (n=0 ; n<4*num ; n++)
{
int blk = random(num);
if (seq[blk]->next != NULL)
blockdown(seq[blk]);
}
/* Find first block */
for (this=t ; this->prev != NULL ; this=this->prev)
/* nil */;
free(seq);
if (verbose)
printf("Random order: %d nodes\n", reorder_nodenum());
return this;
}
/*************************************************************************
Swapping adjacent blocks
*************************************************************************/
static void blockdown(BddTree *left)
{
BddTree *right = left->next;
int n;
int leftsize = left->last - left->first;
int rightsize = right->last - right->first;
int leftstart = bddvar2level[left->seq[0]];
int *lseq = left->seq;
int *rseq = right->seq;
/* Move left past right */
while (bddvar2level[lseq[0]] < bddvar2level[rseq[rightsize]])
{
for (n=0 ; n<leftsize ; n++)
{
if (bddvar2level[lseq[n]]+1 != bddvar2level[lseq[n+1]]
&& bddvar2level[lseq[n]] < bddvar2level[rseq[rightsize]])
{
reorder_vardown(lseq[n]);
}
}
if (bddvar2level[lseq[leftsize]] < bddvar2level[rseq[rightsize]])
{
reorder_vardown(lseq[leftsize]);
}
}
/* Move right to where left started */
while (bddvar2level[rseq[0]] > leftstart)
{
for (n=rightsize ; n>0 ; n--)
{
if (bddvar2level[rseq[n]]-1 != bddvar2level[rseq[n-1]]
&& bddvar2level[rseq[n]] > leftstart)
{
reorder_varup(rseq[n]);
}
}
if (bddvar2level[rseq[0]] > leftstart)
reorder_varup(rseq[0]);
}
/* Swap left and right data in the order */
left->next = right->next;
right->prev = left->prev;
left->prev = right;
right->next = left;
if (right->prev != NULL)
right->prev->next = right;
if (left->next != NULL)
left->next->prev = left;
n = left->pos;
left->pos = right->pos;
right->pos = n;
}
/*************************************************************************
Kernel reordering routines
*************************************************************************/
/*=== Garbage collection for reordering ================================*/
/* Note: Node may be marked
*/
static void addref_rec(int r, char *dep)
{
if (r < 2)
return;
if (bddnodes[r].refcou == 0 || MARKED(r))
{
bddfreenum--;
/* Detect variable dependencies for the interaction matrix */
dep[VAR(r) & MARKHIDE] = 1;
/* Make sure the nodenum field is updated. Used in the initial GBC */
levels[VAR(r) & MARKHIDE].nodenum++;
addref_rec(LOW(r), dep);
addref_rec(HIGH(r), dep);
}
else
{
int n;
/* Update (from previously found) variable dependencies
* for the interaction matrix */
for (n=0 ; n<bddvarnum ; n++)
dep[n] |= imatrixDepends(iactmtx, VAR(r) & MARKHIDE, n);
}
INCREF(r);
}
static void addDependencies(char *dep)
{
int n,m;
for (n=0 ; n<bddvarnum ; n++)
{
for (m=n ; m<bddvarnum ; m++)
{
if (dep[n] && dep[m])
{
imatrixSet(iactmtx, n,m);
imatrixSet(iactmtx, m,n);
}
}
}
}
/* Make sure all nodes are recursively reference counted and store info about
nodes that are refcou. externally. This info is used at last to revert
to the standard GBC mode.
*/
static int mark_roots(void)
{
char *dep = NEW(char,bddvarnum);
int n;
for (n=2,extrootsize=0 ; n<bddnodesize ; n++)
{
/* This is where we go from .level to .var!
* - Do NOT use the LEVEL macro here. */
bddnodes[n].level = bddlevel2var[bddnodes[n].level];
if (bddnodes[n].refcou > 0)
{
SETMARK(n);
extrootsize++;
}
}
if ((extroots=(int*)(malloc(sizeof(int)*extrootsize))) == NULL)
{
free(dep);
return bdd_error(BDD_MEMORY);
}
iactmtx = imatrixNew(bddvarnum);
for (n=2,extrootsize=0 ; n<bddnodesize ; n++)
{
BddNode *node = &bddnodes[n];
if (MARKEDp(node))
{
UNMARKp(node);
extroots[extrootsize++] = n;
memset(dep,0,bddvarnum);
dep[VARp(node)] = 1;
levels[VARp(node)].nodenum++;
addref_rec(LOWp(node), dep);
addref_rec(HIGHp(node), dep);
addDependencies(dep);
}
}
/* Make sure the hash is empty. This saves a loop in the initial
GBC */
memset(bddhash, 0, bddnodesize*sizeof(*bddhash));
free(dep);
return 0;
}
/* Now that all nodes are recursively reference counted we must make sure
that the new hashing scheme is used AND that dead nodes are removed.
This is also a good time to create the interaction matrix.
*/
static void reorder_gbc(void)
{
int n;
bddfreepos = 0;
bddfreenum = 0;
/* No need to zero all hash fields - this is done in mark_roots */
for (n=bddnodesize-1 ; n>=2 ; n--)
{
register BddNode *node = &bddnodes[n];
if (node->refcou > 0)
{
register unsigned int hash;
hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
node->next = bddhash[hash];
bddhash[hash] = n;
}
else
{
LOWp(node) = -1;
node->next = bddfreepos;
bddfreepos = n;
bddfreenum++;
}
}
}
static void reorder_setLevellookup(void)
{
int n;
for (n=0 ; n<bddvarnum ; n++)
{
#ifdef USERESIZE
levels[n].maxsize = bddnodesize / bddvarnum;
levels[n].start = n * levels[n].maxsize;
levels[n].size = MIN(levels[n].maxsize, (levels[n].nodenum*5)/4);
#else
levels[n].maxsize = bddnodesize / bddvarnum;
levels[n].start = n * levels[n].maxsize;
levels[n].size = levels[n].maxsize;
#endif
if (levels[n].size >= 4)
levels[n].size = bdd_prime_lte(levels[n].size);
#if 0
printf("L%3d: start %d, size %d, nodes %d\n", n, levels[n].start,
levels[n].size, levels[n].nodenum);
#endif
}
}
static void reorder_rehashAll(void)
{
int n;
reorder_setLevellookup();
bddfreepos = 0;
memset(bddhash, 0, sizeof(*bddhash)*bddnodesize);
for (n=bddnodesize-1 ; n>=2 ; n--)
{
register BddNode *node = &bddnodes[n];
if (node->refcou > 0)
{
register unsigned int hash;
hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
node->next = bddhash[hash];
bddhash[hash] = n;
}
else
{
node->next = bddfreepos;
bddfreepos = n;
}
}
}
/*=== Unique table handling for reordering =============================*/
/* Note: rehashing must not take place during a makenode call. It is okay
to resize the table, but *not* to rehash it.
*/
static int reorder_makenode(int var, int low, int high)
{
register BddNode *node;
register unsigned int hash;
register int res;
#ifdef CACHESTATS
bddcachestats.uniqueAccess++;
#endif
/* Note: We know that low,high has a refcou greater than zero, so
there is no need to add reference *recursively* */
/* check whether childs are equal */
if (low == high)
{
INCREF(low);
return low;
}
/* Try to find an existing node of this kind */
hash = NODEHASH(var, low, high);
res = bddhash[hash];
while(res != 0)
{
if (LOW(res) == low && HIGH(res) == high)
{
#ifdef CACHESTATS
bddcachestats.uniqueHit++;
#endif
INCREF(res);
return res;
}
res = bddnodes[res].next;
#ifdef CACHESTATS
bddcachestats.uniqueChain++;
#endif
}
/* No existing node -> build one */
#ifdef CACHESTATS
bddcachestats.uniqueMiss++;
#endif
/* Any free nodes to use ? */
if (bddfreepos == 0)
{
if (bdderrorcond)
return 0;
/* Try to allocate more nodes - call noderesize without
* enabling rehashing.
* Note: if ever rehashing is allowed here, then remember to
* update local variable "hash" */
bdd_noderesize(0);
resizedInMakenode = 1;
/* Panic if that is not possible */
if (bddfreepos == 0)
{
bdd_error(BDD_NODENUM);
bdderrorcond = abs(BDD_NODENUM);
return 0;
}
}
/* Build new node */
res = bddfreepos;
bddfreepos = bddnodes[bddfreepos].next;
levels[var].nodenum++;
bddproduced++;
bddfreenum--;
node = &bddnodes[res];
VARp(node) = var;
LOWp(node) = low;
HIGHp(node) = high;
/* Insert node in hash chain */
node->next = bddhash[hash];
bddhash[hash] = res;
/* Make sure it is reference counted */
node->refcou = 1;
INCREF(LOWp(node));
INCREF(HIGHp(node));
return res;
}
/*=== Swapping two adjacent variables ==================================*/
/* Go through var 0 nodes. Move nodes that depends on var 1 to a separate
* chain (toBeProcessed) and let the rest stay in the table.
*/
static int reorder_downSimple(int var0)
{
int toBeProcessed = 0;
int var1 = bddlevel2var[bddvar2level[var0]+1];
int vl0 = levels[var0].start;
int size0 = levels[var0].size;
int n;
levels[var0].nodenum = 0;
for (n=0 ; n<size0 ; n++)
{
int r;
r = bddhash[n + vl0];
bddhash[n + vl0] = 0;
while (r != 0)
{
BddNode *node = &bddnodes[r];
int next = node->next;
if (VAR(LOWp(node)) != var1 && VAR(HIGHp(node)) != var1)
{
/* Node does not depend on next var, let it stay in the chain */
node->next = bddhash[n+vl0];
bddhash[n+vl0] = r;
levels[var0].nodenum++;
}
else
{
/* Node depends on next var - save it for later procesing */
node->next = toBeProcessed;
toBeProcessed = r;
#ifdef SWAPCOUNT
bddcachestats.swapCount++;
#endif
}
r = next;
}
}
return toBeProcessed;
}
/* Now process all the var 0 nodes that depends on var 1.
*
* It is extremely important that no rehashing is done inside the makenode
* calls, since this would destroy the toBeProcessed chain.
*/
static void reorder_swap(int toBeProcessed, int var0)
{
int var1 = bddlevel2var[bddvar2level[var0]+1];
while (toBeProcessed)
{
BddNode *node = &bddnodes[toBeProcessed];
int next = node->next;
int f0 = LOWp(node);
int f1 = HIGHp(node);
int f00, f01, f10, f11, hash;
/* Find the cofactors for the new nodes */
if (VAR(f0) == var1)
{
f00 = LOW(f0);
f01 = HIGH(f0);
}
else
f00 = f01 = f0;
if (VAR(f1) == var1)
{
f10 = LOW(f1);
f11 = HIGH(f1);
}
else
f10 = f11 = f1;
/* Note: makenode does refcou. */
f0 = reorder_makenode(var0, f00, f10);
f1 = reorder_makenode(var0, f01, f11);
node = &bddnodes[toBeProcessed]; /* Might change in makenode */
/* We know that the refcou of the grandchilds of this node
* is greater than one (these are f00...f11), so there is
* no need to do a recursive refcou decrease. It is also
* possible for the LOWp(node)/high nodes to come alive again,
* so deref. of the childs is delayed until the local GBC. */
DECREF(LOWp(node));
DECREF(HIGHp(node));
/* Update in-place */
VARp(node) = var1;
LOWp(node) = f0;
HIGHp(node) = f1;
levels[var1].nodenum++;
/* Rehash the node since it got new childs */
hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
node->next = bddhash[hash];
bddhash[hash] = toBeProcessed;
toBeProcessed = next;
}
}
/* Now go through the var 1 chains. The nodes live here have survived
* the call to reorder_swap() and may stay in the chain.
* The dead nodes are reclaimed.
*/
static void reorder_localGbc(int var0)
{
int var1 = bddlevel2var[bddvar2level[var0]+1];
int vl1 = levels[var1].start;
int size1 = levels[var1].size;
int n;
for (n=0 ; n<size1 ; n++)
{
int hash = n+vl1;
int r = bddhash[hash];
bddhash[hash] = 0;
while (r)
{
BddNode *node = &bddnodes[r];
int next = node->next;
if (node->refcou > 0)
{
node->next = bddhash[hash];
bddhash[hash] = r;
}
else
{
DECREF(LOWp(node));
DECREF(HIGHp(node));
LOWp(node) = -1;
node->next = bddfreepos;
bddfreepos = r;
levels[var1].nodenum--;
bddfreenum++;
}
r = next;
}
}
}
#ifdef USERESIZE
static void reorder_swapResize(int toBeProcessed, int var0)
{
int var1 = bddlevel2var[bddvar2level[var0]+1];
while (toBeProcessed)
{
BddNode *node = &bddnodes[toBeProcessed];
int next = node->next;
int f0 = LOWp(node);
int f1 = HIGHp(node);
int f00, f01, f10, f11;
/* Find the cofactors for the new nodes */
if (VAR(f0) == var1)
{
f00 = LOW(f0);
f01 = HIGH(f0);
}
else
f00 = f01 = f0;
if (VAR(f1) == var1)
{
f10 = LOW(f1);
f11 = HIGH(f1);
}
else
f10 = f11 = f1;
/* Note: makenode does refcou. */
f0 = reorder_makenode(var0, f00, f10);
f1 = reorder_makenode(var0, f01, f11);
node = &bddnodes[toBeProcessed]; /* Might change in makenode */
/* We know that the refcou of the grandchilds of this node
* is greater than one (these are f00...f11), so there is
* no need to do a recursive refcou decrease. It is also
* possible for the LOWp(node)/high nodes to come alive again,
* so deref. of the childs is delayed until the local GBC. */
DECREF(LOWp(node));
DECREF(HIGHp(node));
/* Update in-place */
VARp(node) = var1;
LOWp(node) = f0;
HIGHp(node) = f1;
levels[var1].nodenum++;
/* Do not rehash yet since we are going to resize the hash table */
toBeProcessed = next;
}
}
static void reorder_localGbcResize(int toBeProcessed, int var0)
{
int var1 = bddlevel2var[bddvar2level[var0]+1];
int vl1 = levels[var1].start;
int size1 = levels[var1].size;
int n;
for (n=0 ; n<size1 ; n++)
{
int hash = n+vl1;
int r = bddhash[hash];
bddhash[hash] = 0;
while (r)
{
BddNode *node = &bddnodes[r];
int next = node->next;
if (node->refcou > 0)
{
node->next = toBeProcessed;
toBeProcessed = r;
}
else
{
DECREF(LOWp(node));
DECREF(HIGHp(node));
LOWp(node) = -1;
node->next = bddfreepos;
bddfreepos = r;
levels[var1].nodenum--;
bddfreenum++;
}
r = next;
}
}
/* Resize */
if (levels[var1].nodenum < levels[var1].size)
levels[var1].size = MIN(levels[var1].maxsize, levels[var1].size/2);
else
levels[var1].size = MIN(levels[var1].maxsize, levels[var1].size*2);
if (levels[var1].size >= 4)
levels[var1].size = bdd_prime_lte(levels[var1].size);
/* Rehash the remaining live nodes */
while (toBeProcessed)
{
BddNode *node = &bddnodes[toBeProcessed];
int next = node->next;
int hash = NODEHASH(VARp(node), LOWp(node), HIGHp(node));
node->next = bddhash[hash];
bddhash[hash] = toBeProcessed;
toBeProcessed = next;
}
}
#endif /* USERESIZE */
static int reorder_varup(int var)
{
if (var < 0 || var >= bddvarnum)
return bdd_error(BDD_VAR);
if (bddvar2level[var] == 0)
return 0;
return reorder_vardown( bddlevel2var[bddvar2level[var]-1]);
}
#if 0
static void sanitycheck(void)
{
int n,v,r;
int cou=0;
for (v=0 ; v<bddvarnum ; v++)
{
int vcou=0;
for (n=0 ; n<levels[v].size ; n++)
{
r = bddhash[n+levels[v].start];
while (r)
{
assert(VAR(r) == v);
r = bddnodes[r].next;
cou++;
vcou++;
}
}
assert(vcou == levels[v].nodenum);
}
for (n=2 ; n<bddnodesize ; n++)
{
if (bddnodes[n].refcou > 0)
{
assert(LEVEL(n) < LEVEL(LOW(n)));
assert(LEVEL(n) < LEVEL(HIGH(n)));
cou--;
}
}
assert(cou == 0);
}
#endif
static int reorder_vardown(int var)
{
int n, level;
if (var < 0 || var >= bddvarnum)
return bdd_error(BDD_VAR);
if ((level=bddvar2level[var]) >= bddvarnum-1)
return 0;
resizedInMakenode = 0;
if (imatrixDepends(iactmtx, var, bddlevel2var[level+1]))
{
int toBeProcessed = reorder_downSimple(var);
#ifdef USERESIZE
levelData *l = &levels[var];
if (l->nodenum < (l->size)/3 ||
l->nodenum >= (l->size*3)/2 && l->size < l->maxsize)
{
reorder_swapResize(toBeProcessed, var);
reorder_localGbcResize(toBeProcessed, var);
}
else
#endif
{
reorder_swap(toBeProcessed, var);
reorder_localGbc(var);
}
}
/* Swap the var<->level tables */
n = bddlevel2var[level];
bddlevel2var[level] = bddlevel2var[level+1];
bddlevel2var[level+1] = n;
n = bddvar2level[var];
bddvar2level[var] = bddvar2level[ bddlevel2var[level] ];
bddvar2level[ bddlevel2var[level] ] = n;
/* Update all rename pairs */
bdd_pairs_vardown(level);
if (resizedInMakenode)
reorder_rehashAll();
return 0;
}
/*************************************************************************
User reordering interface
*************************************************************************/
/*
NAME {* bdd\_swapvar *}
SECTION {* reorder *}
SHORT {* Swap two BDD variables *}
PROTO {* int bdd_swapvar(int v1, int v2) *}
DESCR {* Use {\tt bdd\_swapvar} to swap the position (in the current
variable order) of the two BDD
variables {\tt v1} and {\tt v2}. There are no constraints on the
position of the two variables before the call. This function may
{\em not} be used together with user defined variable blocks.
The swap is done by a series of adjacent variable swaps and
requires the whole node table to be rehashed twice for each call
to {\tt bdd\_swapvar}. It should therefore not be used were
efficiency is a major concern. *}
RETURN {* Zero on succes and a negative error code otherwise. *}
ALSO {* bdd\_reorder, bdd\_addvarblock *}
*/
int bdd_swapvar(int v1, int v2)
{
int l1, l2;
/* Do not swap when variable-blocks are used */
if (vartree != NULL)
return bdd_error(BDD_VARBLK);
/* Don't bother swapping x with x */
if (v1 == v2)
return 0;
/* Make sure the variable exists */
if (v1 < 0 || v1 >= bddvarnum || v2 < 0 || v2 >= bddvarnum)
return bdd_error(BDD_VAR);
l1 = bddvar2level[v1];
l2 = bddvar2level[v2];
/* Make sure v1 is before v2 */
if (l1 > l2)
{
int tmp = v1;
v1 = v2;
v2 = tmp;
l1 = bddvar2level[v1];
l2 = bddvar2level[v2];
}
reorder_init();
/* Move v1 to v2's position */
while (bddvar2level[v1] < l2)
reorder_vardown(v1);
/* Move v2 to v1's position */
while (bddvar2level[v2] > l1)
reorder_varup(v2);
reorder_done();
return 0;
}
void bdd_default_reohandler(int prestate)
{
static long c1;
if (verbose > 0)
{
if (prestate)
{
printf("Start reordering\n");
c1 = clock();
}
else
{
long c2 = clock();
printf("End reordering. Went from %d to %d nodes (%.1f sec)\n",
usednum_before, usednum_after, (float)(c2-c1)/CLOCKS_PER_SEC);
}
}
}
/*
NAME {* bdd\_disable\_reorder *}
SECTION {* reorder *}
SHORT {* Disable automatic reordering *}
PROTO {* void bdd_disable_reorder(void) *}
DESCR {* Disables automatic reordering until {\tt bdd\_enable\_reorder}
is called. Reordering is enabled by default as soon as any variable
blocks have been defined. *}
ALSO {* bdd\_enable\_reorder *}
*/
void bdd_disable_reorder(void)
{
reorderdisabled = 1;
}
/*
NAME {* bdd\_enable\_reorder *}
SECTION {* reorder *}
SHORT {* Enables automatic reordering *}
PROTO {* void bdd_enable_reorder(void) *}
DESCR {* Re-enables reordering after a call to {\tt bdd\_disable\_reorder}. *}
ALSO {* bdd\_disable\_reorder *}
*/
void bdd_enable_reorder(void)
{
reorderdisabled = 0;
}
int bdd_reorder_ready(void)
{
if (bddreordermethod == BDD_REORDER_NONE || vartree == NULL ||
bddreordertimes == 0 || reorderdisabled)
return 0;
return 1;
}
void bdd_reorder_auto(void)
{
if (!bdd_reorder_ready())
return;
if (reorder_handler != NULL)
reorder_handler(1);
bdd_reorder(bddreordermethod);
bddreordertimes--;
if (reorder_handler != NULL)
reorder_handler(0);
}
static int reorder_init(void)
{
int n;
if ((levels=NEW(levelData,bddvarnum)) == NULL)
return -1;
for (n=0 ; n<bddvarnum ; n++)
{
levels[n].start = -1;
levels[n].size = 0;
levels[n].nodenum = 0;
}
/* First mark and recursive refcou. all roots and childs. Also do some
* setup here for both setLevellookup and reorder_gbc */
if (mark_roots() < 0)
return -1;
/* Initialize the hash tables */
reorder_setLevellookup();
/* Garbage collect and rehash to new scheme */
reorder_gbc();
return 0;
}
static void reorder_done(void)
{
int n;
for (n=0 ; n<extrootsize ; n++)
SETMARK(extroots[n]);
for (n=2 ; n<bddnodesize ; n++)
{
if (MARKED(n))
UNMARK(n);
else
bddnodes[n].refcou = 0;
/* This is where we go from .var to .level again!
* - Do NOT use the LEVEL macro here. */
bddnodes[n].level = bddvar2level[bddnodes[n].level];
}
#if 0
for (n=0 ; n<bddvarnum ; n++)
printf("%3d\n", bddlevel2var[n]);
printf("\n");
#endif
#if 0
for (n=0 ; n<bddvarnum ; n++)
printf("%3d: %4d nodes , %4d entries\n", n, levels[n].nodenum,
levels[n].size);
#endif
free(extroots);
free(levels);
imatrixDelete(iactmtx);
bdd_gbc();
}
static int varseqCmp(const void *aa, const void *bb)
{
int a = bddvar2level[*((const int*)aa)];
int b = bddvar2level[*((const int*)bb)];
if (a < b)
return -1;
if (a > b)
return 1;
return 0;
}
static BddTree *reorder_block(BddTree *t, int method)
{
BddTree *this;
if (t == NULL)
return NULL;
if (t->fixed == BDD_REORDER_FREE && t->nextlevel!=NULL)
{
switch(method)
{
case BDD_REORDER_WIN2:
t->nextlevel = reorder_win2(t->nextlevel);
break;
case BDD_REORDER_WIN2ITE:
t->nextlevel = reorder_win2ite(t->nextlevel);
break;
case BDD_REORDER_SIFT:
t->nextlevel = reorder_sift(t->nextlevel);
break;
case BDD_REORDER_SIFTITE:
t->nextlevel = reorder_siftite(t->nextlevel);
break;
case BDD_REORDER_WIN3:
t->nextlevel = reorder_win3(t->nextlevel);
break;
case BDD_REORDER_WIN3ITE:
t->nextlevel = reorder_win3ite(t->nextlevel);
break;
case BDD_REORDER_RANDOM:
t->nextlevel = reorder_random(t->nextlevel);
break;
}
}
for (this=t->nextlevel ; this ; this=this->next)
reorder_block(this, method);
if (t->seq != NULL)
qsort(t->seq, t->last-t->first+1, sizeof(int), varseqCmp);
return t;
}
/*
NAME {* bdd\_reorder *}
SECTION {* reorder *}
SHORT {* start dynamic reordering *}
PROTO {* void bdd_reorder(int method) *}
DESCR {* This function initiates dynamic reordering using the heuristic
defined by {\tt method}, which may be one of the following
\begin{description}
\item {\tt BDD\_REORDER\_WIN2}\\
Reordering using a sliding window of size 2. This algorithm
swaps two adjacent variable blocks and if this results in
more nodes then the two blocks are swapped back again.
Otherwise the result is kept in the variable order. This is
then repeated for all variable blocks.
\item {\tt BDD\_REORDER\_WIN2ITE}\\
The same as above but the process is repeated until no further
progress is done. Usually a fast and efficient method.
\item {\tt BDD\_REORDER\_WIN3}\\
The same as above but with a window size of 3.
\item {\tt BDD\_REORDER\_WIN2ITE}\\
The same as above but with a window size of 3.
\item {\tt BDD\_REORDER\_SIFT}\\
Reordering where each block is moved through all possible
positions. The best of these is then used as the new position.
Potentially a very slow but good method.
\item {\tt BDD\_REORDER\_SIFTITE}\\
The same as above but the process is repeated until no further
progress is done. Can be extremely slow.
\item {\tt BDD\_REORDER\_RANDOM}\\
Mostly used for debugging purpose, but may be usefull for
others. Selects a random position for each variable.
\end{description}
*}
ALSO {* bdd\_autoreorder, bdd\_reorder\_verbose, bdd\_addvarblock, bdd\_clrvarblocks *}
*/
void bdd_reorder(int method)
{
BddTree *top;
int savemethod = bddreordermethod;
int savetimes = bddreordertimes;
bddreordermethod = method;
bddreordertimes = 1;
if ((top=bddtree_new(-1)) == NULL)
return;
if (reorder_init() < 0)
return;
usednum_before = bddnodesize - bddfreenum;
top->first = 0;
top->last = bdd_varnum()-1;
top->fixed = 0;
top->next = NULL;
top->nextlevel = vartree;
reorder_block(top, method);
vartree = top->nextlevel;
free(top);
usednum_after = bddnodesize - bddfreenum;
reorder_done();
bddreordermethod = savemethod;
bddreordertimes = savetimes;
}
/*
NAME {* bdd\_reorder\_gain *}
SECTION {* reorder *}
SHORT {* Calculate the gain in size after a reordering *}
PROTO {* int bdd_reorder_gain(void) *}
DESCR {* Returns the gain in percent of the previous number of used
nodes. The value returned is
\[ (100 * (A - B)) / A \]
Where $A$ is previous number of used nodes and $B$ is current
number of used nodes.
*}
*/
int bdd_reorder_gain(void)
{
if (usednum_before == 0)
return 0;
return (100*(usednum_before - usednum_after)) / usednum_before;
}
/*
NAME {* bdd\_reorder\_hook *}
SECTION {* reorder *}
SHORT {* sets a handler for automatic reorderings *}
PROTO {* bddinthandler bdd_reorder_hook(bddinthandler handler) *}
DESCR {* Whenever automatic reordering is done, a check is done to see
if the user has supplied a handler for that event. If so then
it is called with the argument {\tt prestate} being 1 if the
handler is called immediately {\em before} reordering and
{\tt prestate} being 0 if it is called immediately after.
The default handler is
{\tt bdd\_default\_reohandler} which will print information
about the reordering.
A typical handler could look like this:
\begin{verbatim}
void reorderhandler(int prestate)
{
if (prestate)
printf("Start reordering");
else
printf("End reordering");
}
\end{verbatim} *}
RETURN {* The previous handler *}
ALSO {* bdd\_reorder, bdd\_autoreorder, bdd\_resize\_hook *}
*/
bddinthandler bdd_reorder_hook(bddinthandler handler)
{
bddinthandler tmp = reorder_handler;
reorder_handler = handler;
return tmp;
}
/*
NAME {* bdd\_blockfile\_hook *}
SECTION {* reorder *}
SHORT {* Specifies a printing callback handler *}
PROTO {* bddfilehandler bdd_blockfile_hook(bddfilehandler handler) *}
DESCR {* A printing callback handler is used to convert the variable
block identifiers into something readable by the end user. Use
{\tt bdd\_blockfile\_hook} to pass a handler to BuDDy. A typical
handler could look like this:
\begin{verbatim}
void printhandler(FILE *o, int block)
{
extern char **blocknames;
fprintf(o, "%s", blocknames[block]);
}
\end{verbatim}
\noindent
The handler is then called from {\tt bdd\_printorder} and
{\tt bdd\_reorder} (depending on the verbose level) with
the block numbers returned by {\tt bdd\_addvarblock} as arguments.
No default handler is supplied. The argument {\tt handler} may be
NULL if no handler is needed. *}
RETURN {* The old handler *}
ALSO {* bdd\_printorder *}
*/
bddfilehandler bdd_blockfile_hook(bddfilehandler handler)
{
bddfilehandler tmp = reorder_filehandler;
reorder_filehandler = handler;
return tmp;
}
/*
NAME {* bdd\_autoreorder *}
EXTRA {* bdd\_autoreorder\_times *}
SECTION {* reorder *}
SHORT {* enables automatic reordering *}
PROTO {* int bdd_autoreorder(int method)
int bdd_autoreorder_times(int method, int num) *}
DESCR {* Enables automatic reordering using {\tt method} as the reordering
method. If {\tt method} is {\tt BDD\_REORDER\_NONE} then
automatic reordering is disabled. Automatic
reordering is done every time the number of active nodes in the
node table has been doubled and works by interrupting the current
BDD operation, doing the reordering and the retrying the operation.
In the second form the argument {\tt num} specifies the allowed
number of reorderings. So if for example a "one shot" reordering
is needed, then the {\tt num} argument would be set to one.
Values for {\tt method} can be found under {\tt bdd\_reorder}.
*}
RETURN {* Returns the old value of {\tt method} *}
ALSO {* bdd\_reorder *}
*/
int bdd_autoreorder(int method)
{
int tmp = bddreordermethod;
bddreordermethod = method;
bddreordertimes = -1;
return tmp;
}
int bdd_autoreorder_times(int method, int num)
{
int tmp = bddreordermethod;
bddreordermethod = method;
bddreordertimes = num;
return tmp;
}
/*
NAME {* bdd\_var2level *}
SECTION {* reorder *}
SHORT {* Fetch the level of a specific BDD variable *}
PROTO {* int bdd_var2level(int var) *}
DESCR {* Returns the position of the variable {\tt var} in the current
variable order. *}
ALSO {* bdd\_reorder, bdd\_level2var *}
*/
int bdd_var2level(int var)
{
if (var < 0 || var >= bddvarnum)
return bdd_error(BDD_VAR);
return bddvar2level[var];
}
/*
NAME {* bdd\_level2var *}
SECTION {* reorder *}
SHORT {* Fetch the variable number of a specific level *}
PROTO {* int bdd_level2var(int level) *}
DESCR {* Returns the variable placed at position {\tt level} in the
current variable order. *}
ALSO {* bdd\_reorder, bdd\_var2level *}
*/
int bdd_level2var(int level)
{
if (level < 0 || level >= bddvarnum)
return bdd_error(BDD_VAR);
return bddlevel2var[level];
}
/*
NAME {* bdd\_getreorder\_times *}
SECTION {* reorder *}
SHORT {* Fetch the current number of allowed reorderings *}
PROTO {* int bdd_getreorder_times(void) *}
DESCR {* Returns the current number of allowed reorderings left. This
value can be defined by {\tt bdd\_autoreorder\_times}. *}
ALSO {* bdd\_reorder\_times, bdd\_getreorder\_method *}
*/
int bdd_getreorder_times(void)
{
return bddreordertimes;
}
/*
NAME {* bdd\_getreorder\_method *}
SECTION {* reorder *}
SHORT {* Fetch the current reorder method *}
PROTO {* int bdd_getreorder_method(void) *}
DESCR {* Returns the current reorder method as defined by
{\tt bdd\_autoreorder}. *}
ALSO {* bdd\_reorder, bdd\_getreorder\_times *}
*/
int bdd_getreorder_method(void)
{
return bddreordermethod;
}
/*
NAME {* bdd\_reorder\_verbose *}
SECTION {* reorder *}
SHORT {* enables verbose information about reorderings *}
PROTO {* int bdd_reorder_verbose(int v) *}
DESCR {* With {\tt bdd\_reorder\_verbose} it is possible to set the level
of information which should be printed during reordering. A value
of zero means no information, a value of one means some information
and any greater value will result in a lot of reordering
information. The default value is zero. *}
RETURN {* The old verbose level *}
ALSO {* bdd\_reorder *}
*/
int bdd_reorder_verbose(int v)
{
int tmp = verbose;
verbose = v;
return tmp;
}
/*
NAME {* bdd\_reorder\_probe *}
SECTION {* reorder *}
SHORT {* Define a handler for minimization of BDDs *}
PROTO {* bddsizehandler bdd_reorder_probe(bddsizehandler handler) *}
DESCR {* Reordering is typically done to minimize the global number of
BDD nodes in use, but it may in some cases be usefull to minimize
with respect to a specific BDD. With {\tt bdd\_reorder\_probe} it
is possible to define a callback function that calculates the
size of a specific BDD (or anything else in fact). This handler
will then be called by the reordering functions to get the current
size information. A typical handle could look like this:
\begin{verbatim}
int sizehandler(void)
{
extern BDD mybdd;
return bdd_nodecount(mybdd);
}
\end{verbatim}
No default handler is supplied. The argument {\tt handler} may be
NULL if no handler is needed. *}
*}
RETURN {* The old handler *}
ALSO {* bdd\_reorder *}
*/
bddsizehandler bdd_reorder_probe(bddsizehandler handler)
{
bddsizehandler old = reorder_nodenum;
if (handler == NULL)
return reorder_nodenum;
reorder_nodenum = handler;
return old;
}
/*
NAME {* bdd\_clrvarblocks *}
SECTION {* reorder *}
SHORT {* clears all variable blocks *}
PROTO {* void bdd_clrvarblocks(void) *}
DESCR {* Clears all the variable blocks that has been defined by calls
to bdd\_addvarblock. *}
ALSO {* bdd\_addvarblock *}
*/
void bdd_clrvarblocks(void)
{
bddtree_del(vartree);
vartree = NULL;
blockid = 0;
}
/*
NAME {* bdd\_addvarblock *}
EXTRA {* bdd\_intaddvarblock *}
SECTION {* reorder *}
SHORT {* adds a new variable block for reordering *}
PROTO {* int bdd_addvarblock(BDD var, int fixed)
int bdd_intaddvarblock(int first, int last, int fixed) *}
DESCR {* Creates a new variable block with the variables in the variable
set {\tt var}. The variables in {\tt var} must be contiguous.
In the second form the argument {\tt first} is the first variable
included in the block and {\tt last} is the last variable included
in the block. This order does not depend on current variable
order.
The variable blocks are ordered as a tree, with the largest
ranges at top and the smallest at the bottom. Example: Assume
the block 0-9 is added as the first block and then the block 0-6.
This yields the 0-9 block at the top, with the 0-6 block as a
child. If now the block 2-4 was added, it would become a child
of the 0-6 block. A block of 0-8 would be a child of the 0-9
block and have the 0-6 block as a child. Partially overlapping
blocks are not allowed.
The {\tt fixed} parameter sets the block to be fixed (no
reordering of its child blocks is allowed) or free, using
the constants {\tt BDD\_REORDER\_FIXED} and {\tt
BDD\_REORDER\_FREE}. Reordering is always done on the top
most blocks first and then recursively downwards.
The return value is an integer that can be used to identify
the block later on - with for example {\tt bdd\_blockfile\_hook}.
The values returned will be in the sequence $0,1,2,3,\ldots$.
*}
RETURN {* A non-negative identifier on success, otherwise a negative error code. *}
ALSO {* bdd\_varblockall, fdd\_intaddvarblock, bdd\_clrvarblocks *} */
int bdd_addvarblock(BDD b, int fixed)
{
BddTree *t;
int n, *v, size;
int first, last;
if ((n=bdd_scanset(b, &v, &size)) < 0)
return n;
if (size < 1)
return bdd_error(BDD_VARBLK);
first = last = v[0];
for (n=0 ; n<size ; n++)
{
if (v[n] < first)
first = v[n];
if (v[n] > last)
last = v[n];
}
if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == NULL)
return bdd_error(BDD_VARBLK);
vartree = t;
return blockid++;
}
int bdd_intaddvarblock(int first, int last, int fixed)
{
BddTree *t;
if (first < 0 || first >= bddvarnum || last < 0 || last >= bddvarnum)
return bdd_error(BDD_VAR);
if ((t=bddtree_addrange(vartree, first,last, fixed,blockid)) == NULL)
return bdd_error(BDD_VARBLK);
vartree = t;
return blockid++;
}
/*
NAME {* bdd\_varblockall *}
SECTION {* reorder *}
SHORT {* add a variable block for all variables *}
PROTO {* void bdd_varblockall(void) *}
DESCR {* Adds a variable block for all BDD variables declared so far.
Each block contains one variable only. More variable blocks
can be added later with the use of {\tt bdd\_addvarblock} --
in this case the tree of variable blocks will have the blocks
of single variables as the leafs. *}
ALSO {* bdd\_addvarblock, bdd\_intaddvarblock *}
*/
void bdd_varblockall(void)
{
int n;
for (n=0 ; n<bddvarnum ; n++)
bdd_intaddvarblock(n,n,1);
}
/*
NAME {* bdd\_printorder *}
SECTION {* reorder *}
SHORT {* prints the current order *}
PROTO {* void bdd_printorder(void)
bdd_fprint_order(FILE *f)*}
DESCR {* Prints an indented list of the variable blocks, showing the top
most blocks to the left and the lower blocks to the right.
Example:\\
\begin{verbatim}
2{
0
1
2}
3
4
\end{verbatim}
This shows 5 variable blocks. The first one added is block zero,
which is on the same level as block one. These two blocks are then
sub-blocks of block two and block two is on the same level as
block three and four. The numbers are the identifiers returned
from {\tt bdd\_addvarblock}. The block levels depends on the
variables included in the blocks.
*}
ALSO {* bdd\_reorder, bdd\_addvarblock *}
*/
void bdd_printorder(void)
{
bdd_fprintorder(stdout);
}
/*
NAME {* bdd\_setvarorder *}
SECTION {* reorder *}
SHORT {* set a specific variable order *}
PROTO {* void bdd_setvarorder(int *neworder) *}
DESCR {* This function sets the current variable order to be the one
defined by {\tt neworder}. The parameter {\tt neworder} is
interpreted as a sequence of variable indecies and the new
variable order is exactly this sequence. The array {\em must}
contain all the variables defined so far. If for instance the
current number of variables is 3 and {\tt neworder} contains
$[1,0,2]$ then the new variable order is $v_1 < v_0 < v_2$. *}
ALSO {* bdd\_reorder, bdd\_printorder *}
*/
void bdd_setvarorder(int *neworder)
{
int level;
/* Do not set order when variable-blocks are used */
if (vartree != NULL)
{
bdd_error(BDD_VARBLK);
return;
}
reorder_init();
for (level=0 ; level<bddvarnum ; level++)
{
int lowvar = neworder[level];
while (bddvar2level[lowvar] > level)
reorder_varup(lowvar);
}
reorder_done();
}
static void print_order_rec(FILE *o, BddTree *t, int level)
{
if (t == NULL)
return;
if (t->nextlevel)
{
fprintf(o, "%*s", level*3, "");
if (reorder_filehandler)
reorder_filehandler(o,t->id);
else
fprintf(o, "%3d", t->id);
fprintf(o, "{\n");
print_order_rec(o, t->nextlevel, level+1);
fprintf(o, "%*s", level*3, "");
if (reorder_filehandler)
reorder_filehandler(o,t->id);
else
fprintf(o, "%3d", t->id);
fprintf(o, "}\n");
print_order_rec(o, t->next, level);
}
else
{
fprintf(o, "%*s", level*3, "");
if (reorder_filehandler)
reorder_filehandler(o,t->id);
else
fprintf(o, "%3d", t->id);
fprintf(o, "\n");
print_order_rec(o, t->next, level);
}
}
void bdd_fprintorder(FILE *ofile)
{
print_order_rec(ofile, vartree, 0);
}
/* EOF */
Reference in a new issue View git blame Copy permalink