tclbdd

Check-in [b11e4e2f87]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Added missing bddInt.h (whoops\!). Added code for AllSat - no Tcl support yet, so entirely untested.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:b11e4e2f8782fd7860b849db88ffe91d5af1e23a
User & Date: kennykb 2013-11-30 04:28:06
Context
2013-11-30
16:34
Add 8-queens example as a test. check-in: 2cbd4f3ba6 user: kennykb tags: trunk
04:28
Added missing bddInt.h (whoops\!). Added code for AllSat - no Tcl support yet, so entirely untested. check-in: b11e4e2f87 user: kennykb tags: trunk
01:30
add Restrict - no tests yet check-in: d889c00657 user: kennykb tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

1255
1256
1257
1258
1259
1260
1261
















































































































































































































1262
1263
1264
1265
1266
1267
1268
	mp_clear(v);
	ckfree(v);
	Tcl_SetHashValue(cleanup, NULL);
    }
    Tcl_DeleteHashTable(&hash);
    return status;
}
















































































































































































































 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Dump --
 *
 *	Formats a BDD as a Tcl dictionary for debugging.







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
	mp_clear(v);
	ckfree(v);
	Tcl_SetHashValue(cleanup, NULL);
    }
    Tcl_DeleteHashTable(&hash);
    return status;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_AllSatStart --
 *
 *	Begins a traversal of a BDD for all satisfying variable assignments
 *
 * Results:
 *	Returns a pointer to a state vector that manages the state
 *	of the traversal. The state vector must be passed to BDD_AllSatNext
 *	to retrieve each variable assignment, and to BDD_AllSatFinish
 *	at the end of the traversal or when the traversal is abandoned.
 *
 * It is a pointer smash to dispose of a BDD_System while traversing one of
 * its BDD's.
 *
 *-----------------------------------------------------------------------------
 */
BDD_AllSatState*
BDD_AllSatStart(
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_BeadIndex u)		/* BDD to traverse */
{

    /*
     * Allocate the state vector
     */
    BDD_AllSatState* stateVector =
	(BDD_AllSatState*) ckalloc(sizeof(BDD_AllSatState));
    BDD_VariableIndex nVars = BDD_GetVariableCount(sysPtr);

    /*
     * Allocate the stacks
     */
    stateVector->sysPtr = sysPtr;
    stateVector->uStack = (BDD_BeadIndex*)
	ckalloc(nVars * sizeof(BDD_BeadIndex));
    stateVector->sStack = (unsigned char*)
	ckalloc(nVars);
    stateVector->v = (BDD_ValueAssignment*)
	ckalloc(nVars * sizeof(BDD_ValueAssignment));

    /*
     * Store the initial state, in which the top of the expression
     * is on the stack and the stack depth is 1, with the first
     * action being to explore the expression's left hand side.
     */

    stateVector->uStack[0] = u;
    ++sysPtr->beads[u].refCount;
    stateVector->sStack[0] = BDD_ALLSAT_START;
    stateVector->depth = 1;

    return stateVector;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_AllSat_Next --
 *
 *	Retrieves the next satisfying assignment from an iterator over
 *	a BDD
 *
 * Results:
 *	Returns 1 if there was a satisfying assignment, 0 at the end of
 *	the iterator.
 *
 * Side effects:
 *	Stores the literals of the satisfying assignment in *v and 
 *	the count of the literals in *n.
 *
 * Irrelevant variables are omitted from the vector. The vector is
 * usable until the next call to BDD_AllSat_Next, or a call to BDD_AllSat_Finish
 *
 * It is necessary to call BDD_AllSat_Finish to dispose of the state
 * vector, even after this function has returned 0.
 *
 *-----------------------------------------------------------------------------
 */

int
BDD_AllSat_Next(
    BDD_AllSatState* stateVector,
				/* State vector from BDD_AllSat_Start */
    BDD_ValueAssignment **vPtr, /* OUTPUT: Vector of satisfying literals */
    BDD_VariableIndex *nPtr)	/* OUTPUT: Count of satisfying literals */
{
    BDD_System* sysPtr = stateVector->sysPtr;
				/* System of BDD's */
    BDD_VariableIndex depth = stateVector->depth;
				/* Depth of the stack */
    BDD_BeadIndex u;		/* Current bead */
    unsigned char s;		/* Current state */
	
    for (;;) {

	/*
	 * Initially, BDD_AllSat_Start will have pushed the starting
	 * bead and the BDD_ALLSAT_START state onto the stack, and this
	 * code will pop it again. After reporting a variable assignment
	 * and re-entering this procedure, the top of stack will be
	 * the last bead prior to the 1, and the BDD_ALLSAT_SECONDTRY
	 * or BDD_ALLSAT_RETURN according to whether the next action
	 * is to explore the bead's 'high' transition or to retreat to
	 * the bead's predecessor.
	 *
	 * We also arrive at this point from the bottom of the loop,
	 * in which case u designates the 0 leaf bead, and we want
	 * to unwind the stack in the same way.
	 */

	/*
	 * Pop the state off the stack
	 */
	do {
	    if (depth == 0) {
		/*
		 * When the entire stack is unwound, the BDD has been fully
		 * traversed.
		 */
		return 0;
	    }
	    --depth;
	    u = stateVector->uStack[depth];
	    s = stateVector->sStack[depth];

	    /*
	     * As long as the popped state is RETURN, keep discarding stack
	     * levels.
	     */
	} while (s == BDD_ALLSAT_RETURN);

	/*
	 * At this point, the state is either START, to begin traversing
	 * the diagram, or SECONDTRY, to explore the 'high' transition of
	 * a visited bead. If it's SECONDTRY, advance to the bead's 'high'
	 * transition.
	 */
	if (s == BDD_ALLSAT_SECONDTRY) {
	    stateVector->uStack[depth] = u;
	    stateVector->sStack[depth] = BDD_ALLSAT_RETURN;
	    stateVector->v[depth].var = sysPtr->beads[u].high;
	    stateVector->v[depth].value = 1;
	    ++depth;
	    u = sysPtr->beads[u].high;
	}

	/*
	 * Traverse the 'low' transitions on the current branch
	 * until reaching a terminal, stacking SECONDTRY along the way.
	 */
	while (u != 0) {
	    if (u == 1) {
		/*
		 * We've reached the 1 terminal. Return the satisfying
		 * assignment that we just found. We'll resume by unstacking
		 */
		stateVector->depth = depth;
		*vPtr = stateVector->v;
		*nPtr = depth;
		return 1;
	    }

	    /*
	     * Stack the current bead to restart from the 'high' transition,
	     * then advance to the 'low' transition.
	     */
	    stateVector->uStack[depth] = u;
	    stateVector->sStack[depth] = BDD_ALLSAT_SECONDTRY;
	    stateVector->v[depth].var = sysPtr->beads[u].level;
	    stateVector->v[depth].value = 0;
	    ++depth;
	    u = sysPtr->beads[u].low;
	}

	/* 
	 * We've reached the zero terminal. Return to the top of this
	 * function to unwind the stack to the next decision point.
	 */
    }
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_AllSat_Finish --
 *
 *	Terminates an exhaustive search for satisfying variable assigments
 *	in a BDD.
 *
 * Side effects:
 *	Frees the state vector and decrements the ref count of the start bead.
 *
 *-----------------------------------------------------------------------------
 */

void
BDD_AllSat_Finish(
    BDD_AllSatState* stateVector) /* State vector for tbe search */
{
    ckfree(stateVector->v);
    ckfree(stateVector->sStack);
    BDD_UnrefBead(stateVector->sysPtr, stateVector->uStack[0]);
    ckfree(stateVector->uStack);
    ckfree(stateVector);
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Dump --
 *
 *	Formats a BDD as a Tcl dictionary for debugging.

Changes to generic/bdd.h.

52
53
54
55
56
57
58

59
60
61
62
63
64
65
...
103
104
105
106
107
108
109






110
111
112
113
114
115
116
117
118
119
120
121
    BDD_BINOP_OR = 0xe,         /* 0    1   1   1  */ /* a | b */

    /* BDD_BINOP_TRUE = 0xf */

} BDD_BinOp;

typedef struct BDD_System BDD_System;


/* Type of a bead index */

typedef size_t BDD_BeadIndex;	/* Making this 'unsigned int'
				 * limits the size of a BDD system to
				 * 2**32 nodes but cuts the memory
				 * usage (and bus bandwidth) roughly in 
................................................................................
				      BDD_BeadIndex u1, BDD_BeadIndex u2);
extern BDDAPI BDD_BeadIndex BDD_Restrict(BDD_System* sysPtr,
					 BDD_BeadIndex u,
					 const BDD_ValueAssignment r[],
					 BDD_VariableIndex n);
extern BDDAPI int BDD_SatCount(BDD_System* sysPtr, BDD_BeadIndex x,
			       mp_int* count);






extern BDDAPI int BDD_Dump(Tcl_Interp*, Tcl_Obj*, BDD_System*, BDD_BeadIndex);
extern BDDAPI void BDD_DeleteSystem(BDD_System* sysPtr);


#endif /* not BDD_H_INCLUDED */

/*
 * Local Variables:
 * mode: c
 * c-basic-offset: 4
 * End:
 */







>







 







>
>
>
>
>
>












52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
...
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
    BDD_BINOP_OR = 0xe,         /* 0    1   1   1  */ /* a | b */

    /* BDD_BINOP_TRUE = 0xf */

} BDD_BinOp;

typedef struct BDD_System BDD_System;
typedef struct BDD_AllSatState BDD_AllSatState;

/* Type of a bead index */

typedef size_t BDD_BeadIndex;	/* Making this 'unsigned int'
				 * limits the size of a BDD system to
				 * 2**32 nodes but cuts the memory
				 * usage (and bus bandwidth) roughly in 
................................................................................
				      BDD_BeadIndex u1, BDD_BeadIndex u2);
extern BDDAPI BDD_BeadIndex BDD_Restrict(BDD_System* sysPtr,
					 BDD_BeadIndex u,
					 const BDD_ValueAssignment r[],
					 BDD_VariableIndex n);
extern BDDAPI int BDD_SatCount(BDD_System* sysPtr, BDD_BeadIndex x,
			       mp_int* count);
extern BDDAPI BDD_AllSatState* BDD_AllSatStart(BDD_System* sysPtr,
					       BDD_BeadIndex u);
extern BDDAPI int BDD_AllSatNext(BDD_AllSatState* state,
				 BDD_ValueAssignment** vPtr,
				 int* nPtr);
extern BDDAPI int BDD_AllSatFinish(BDD_AllSatState*);
extern BDDAPI int BDD_Dump(Tcl_Interp*, Tcl_Obj*, BDD_System*, BDD_BeadIndex);
extern BDDAPI void BDD_DeleteSystem(BDD_System* sysPtr);


#endif /* not BDD_H_INCLUDED */

/*
 * Local Variables:
 * mode: c
 * c-basic-offset: 4
 * End:
 */

Added generic/bddInt.h.

































































































































































































































































































































>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
#pragma once
#ifndef BDDINT_H_INCLUDED
#define BDDINT_H_INCLUDED 1

#include "bdd.h"

typedef struct Bead Bead;
typedef struct UIHash1 UIHash1;
typedef struct UIEntry1 UIEntry1;
typedef struct UIHash1MP UIHash1MP;
typedef struct UIEntry1MP UIEntry1MP;
typedef struct UIHash2 UIHash2;
typedef struct UIEntry2 UIEntry2;
typedef struct UIHash2 UIHash3;
typedef struct UIEntry2 UIEntry3;

/*
 * Structure that holds all the data for a system of Binary Decision Diagrams
 * (BDD's).
 *
 * The 'hashes' table is a special hash table whose implementation is in
 * the file 'bdd.c'.  It is an intrusive hash table: each Bead structure
 * is also a hash entry. The hash buckets are singly linked lists with
 * the 'next' entry designating, for each bucket, the next element in the
 * bucket.
 *
 * The reason that the 'hashes' table is handled specially is that it saves
 * an extra pointer per bead in an external hash table. Since every bead
 * is in the hash at all times, this turns out to be an important saving
 * in memory and time.
 */
struct BDD_System {
    Bead* beads;		/* Array of Bead structures holding the
				 * individual beads (shared among all BDD's). */
    BDD_BeadIndex beadsAlloc;	/* Number of elements allocated for the
				 * 'beads' array. */
    BDD_BeadIndex unusedBead;	/* Pointer to the most-recently used 
				 * free bead in the 'beads' array. This
				 * bead points to the least-recently-used,
				 * which in turn points to the next-least
				 * recently-used, and so on in a circular
				 * queue. */
    BDD_BeadIndex* hashes;	/* Array of indices for the first bead in each
				 * hash bucket. The hash table looks up beads
				 * by 'level', 'low' and 'high.*/
    BDD_BeadIndex hashSize;	/* Number of buckets in the hash table */
  
};

/*
 * State of an AllSat computation
 */
typedef enum BDD_AllSatSEnum {
    BDD_ALLSAT_START,		/* Initial entry */
    BDD_ALLSAT_SECONDTRY,	/* Did the low transition at this
				 * stack level, now try the high transition */
    BDD_ALLSAT_RETURN,		/* Did both transitions, retreat to the
				 * next earlier node */
} BDD_AllSatSEnum;

/*
 * Structure that manages the state of an AllSat computation
 */
struct BDD_AllSatState {
    BDD_System* sysPtr;		/* System of BDD's */
    BDD_BeadIndex* uStack;	/* Stack of beads from the root to the current
				 * point */
    unsigned char* sStack;	/* Stack of state at each bead */
    BDD_ValueAssignment* v;	/* Incomplete satisfying assignment */
    BDD_VariableIndex depth;	/* Stack depth of the three stacks */
};

/*
 * Structure that represents a single bead in a BDD 
 */
struct Bead {
    BDD_BeadIndex low;		/* Index of the next bead if the variable is
				 * false */
    BDD_BeadIndex high;		/* Index of the next bead if the variable is
				 * true */
    BDD_BeadIndex next;		/* Index of the next bead in the same
				 * hash bucket as this bead. */
    BDD_BeadIndex refCount;	/* Reference count of this bead */
    BDD_VariableIndex level;	/* Level in the diagram (in other words,
				 * the index of the variable being examined) */
};

/*
 * Structure that represents a hash table with a key comprising a single
 * unsigned integer and a value consisting of a single unsigned integer
 */
struct UIHash1 {
    UIEntry1MP* entries;	/* Array of hashtable entries */
    BDD_BeadIndex* hashes;	/* Array of heads of hash buckets */
    BDD_BeadIndex unusedEntry;	/* Index of the last unused entry */
    BDD_BeadIndex entriesAlloc;	/* Count of allocated entries */
    BDD_BeadIndex hashSize;	/* Count of allocated buckets */
};

/*
 * Structure that represents a single hash entry in a UIHash1
 */
struct UIEntry1 {
    BDD_BeadIndex key;		/* Key */
    BDD_BeadIndex next;		/* Next hash entry in the same bucket */
    BDD_BeadIndex value;	/* Value */
};

/*
 * Structure that represents a hash table with a key comprising a single
 * unsigned integer and a value consisting of a single mp_int
 */
struct UIHash1MP {
    UIEntry1MP* entries;	/* Array of hashtable entries */
    BDD_BeadIndex* hashes;	/* Array of heads of hash buckets */
    BDD_BeadIndex unusedEntry;	/* Index of the last unused entry */
    BDD_BeadIndex entriesAlloc;	/* Count of allocated entries */
    BDD_BeadIndex hashSize;	/* Count of allocated buckets */
};

/*
 * Structure that represents a single hash entry in a UIHash1MP
 */
struct UIEntry1MP {
    BDD_BeadIndex key;		/* Key */
    BDD_BeadIndex next;		/* Next hash entry in the same bucket */
    mp_int value;		/* Value */
};

/*
 * Structure that represents a hash table with a key comprising two
 * unsigned integers and a value consisting of a single one.
 */
struct UIHash2 {
    UIEntry2* entries;		/* Array of hashtable entries */
    BDD_BeadIndex* hashes;	/* Array of heads of hash buckets */
    BDD_BeadIndex unusedEntry;	/* Index of the last unused entry */
    BDD_BeadIndex entriesAlloc;	/* Count of allocated entries */
    BDD_BeadIndex hashSize;	/* Count of allocated buckets */
};

/*
 * Structure that represents a single hash entry in a UIHash2 
 */
struct UIEntry2 {
    BDD_BeadIndex key1;		/* First component of key */
    BDD_BeadIndex key2;		/* Second component of key */
    BDD_BeadIndex next;		/* Next hash entry in the same bucket */
    BDD_BeadIndex value;	/* Value */
};

#endif 


/*
 * Local Variables:
 * mode: c
 * c-basic-offset: 4
 * End:
 */