tclbdd

Check-in [40788f090a]
Login

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

Overview
Comment:Added Apply3 for ternary operators - no tests yet. Modified Apply to prune subtrees more aggressively - now recognizes operations that will evaluate to constant 1, constant 0 and either of the input arguments. Modified to maintain refcounts of partial applications that are cached. Added test cases for quantified formulas, and plugged a memory leak.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:40788f090aa250b21d3c82245eb26458c275c478
User & Date: kbk 2013-12-06 03:15:23
Context
2013-12-06
05:08
test ternary operators - add missing ternary OR check-in: 70e321ed7a user: kbk tags: trunk
03:15
Added Apply3 for ternary operators - no tests yet. Modified Apply to prune subtrees more aggressively - now recognizes operations that will evaluate to constant 1, constant 0 and either of the input arguments. Modified to maintain refcounts of partial applications that are cached. Added test cases for quantified formulas, and plugged a memory leak. check-in: 40788f090a user: kbk tags: trunk
2013-12-05
03:16
Fix several miscellaneous packaging and coding issues identified by dgp and aku check-in: a87110a479 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

27
28
29
30
31
32
33



34
35
36
37
38
39
40
..
63
64
65
66
67
68
69






















70
71
72
73
74
75
76
...
261
262
263
264
265
266
267













































































268
269
270
271
272
273
274
...
995
996
997
998
999
1000
1001



1002
1003
1004
1005
1006
1007
1008








1009
1010











1011
1012


















1013





1014



1015
1016
1017
1018
1019
1020
1021
1022



1023
1024
1025
1026
1027
1028



1029
1030
1031
1032
1033
1034



1035
1036
1037
1038




1039

1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050


1051
1052





1053
1054



















































































































































































1055
1056
1057
1058
1059
1060
1061
 * Static functions defined in this file
 */
static void AddToHash(BDD_System*, BDD_BeadIndex);
				/* Add a bead to the system hash */
static unsigned int Bead2HashKeyProc(Tcl_HashTable*, void*);
static int Bead2HashKeyComparator(void*, Tcl_HashEntry*);
static Tcl_HashEntry* Bead2HashEntryAlloc(Tcl_HashTable*, void*);



static int FindInHash(BDD_System*, BDD_VariableIndex, BDD_BeadIndex,
		      BDD_BeadIndex high);
				/* Find a bead in the system hash */
static unsigned int HashPair(BDD_BeadIndex, BDD_BeadIndex);
				/* Hashcode for a pair of integers */
static unsigned int HashTriple(BDD_VariableIndex, BDD_BeadIndex,
				BDD_BeadIndex);
................................................................................
    TCL_HASH_KEY_TYPE_VERSION,	/* version */
    0,				/* flags */
    Bead2HashKeyProc,		/* hash procedure */
    Bead2HashKeyComparator,	/* comparator */
    Bead2HashEntryAlloc,	/* allocator */
    NULL			/* standard deallocator */
};






















/*
 *-----------------------------------------------------------------------------
 *
 * Log2HashTableSize --
 *
 *	Computes the number of bits to use in a hash bucket index
 *	when the index is expected to vary between 0 and n-1
................................................................................
				 - sizeof(entryPtr->key)
				 + 2 * sizeof(BDD_BeadIndex));
    BDD_BeadIndex* outBeads = (BDD_BeadIndex*) &(entryPtr->key.oneWordValue);
    outBeads[0] = beads[0];
    outBeads[1] = beads[1];
    return entryPtr;
}













































































 
/*
 *-----------------------------------------------------------------------------
 *
 * AddToHash --
 *
 *	Adds a bead to the hash table.
................................................................................
				 * right-hand bead*/

    BDD_BeadIndex l, h;	        /* Low and high transitions of the result */
    int newFlag;		/* Flag==1 if the output is a new bead */
    BDD_BeadIndex result;	/* Return value */
    Tcl_HashEntry* entry;	/* Pointer to the entry in the
				 * cache of beads for this operation */




    u[0] = u1;
    u[1] = u2;
    entry = Tcl_CreateHashEntry(G, u, &newFlag);
    if (!newFlag) {
	result = (BDD_BeadIndex) Tcl_GetHashValue(entry);
	++sysPtr->beads[result].refCount;








    } else if (u1 <= 1 && u2 <= 1) {
	unsigned int i = ((unsigned int)u1 << 1) + (unsigned int)u2;











	result = ((op>>i) & 1);
	++sysPtr->beads[result].refCount;


















    } else {





	if (u1Ptr->level == u2Ptr->level) {



	    level = u1Ptr->level;
	    low1 = u1Ptr->low;
	    high1 = u1Ptr->high;
	    low2 = u2Ptr->low;
	    high2 = u2Ptr->high;
	    l = Apply(sysPtr, G, op, low1, low2);
	    h = Apply(sysPtr, G, op, high1, high2);
	} else if (u1Ptr->level < u2Ptr->level) {



	    level = u1Ptr->level;
	    low1 = u1Ptr->low;
	    high1 = u1Ptr->high;
	    l = Apply(sysPtr, G, op, low1, u2);
	    h = Apply(sysPtr, G, op, high1, u2);
	} else /* u1Ptr->level > u2Ptr->level */ {



	    level = u2Ptr->level;
	    low2 = u2Ptr->low;
	    high2 = u2Ptr->high;
	    l = Apply(sysPtr, G, op, u1, low2);
	    h = Apply(sysPtr, G, op, u1, high2);
	}



	result = BDD_MakeBead(sysPtr, level, l, h);
	BDD_UnrefBead(sysPtr, l);
	BDD_UnrefBead(sysPtr, h);
    }




    Tcl_SetHashValue(entry, result);

    return result;
}

BDD_BeadIndex
BDD_Apply(
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_BinOp op,		/* Operation to apply */
    BDD_BeadIndex u1,		/* Left operand */
    BDD_BeadIndex u2) 		/* Right operand */
{
    Tcl_HashTable G;


    Tcl_InitCustomHashTable(&G, TCL_CUSTOM_TYPE_KEYS, &Bead2KeyType);
    BDD_BeadIndex entry = Apply(sysPtr, &G, op, u1, u2);





    Tcl_DeleteHashTable(&G);
    return entry;



















































































































































































}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Restrict --
 *







>
>
>







 







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







 







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







 







>
>
>







>
>
>
>
>
>
>
>
|
<
>
>
>
>
>
>
>
>
>
>
>
|
|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|
>
>
>
>
>
|
>
>
>
|
|
|
|
|
|
|
|
>
>
>
|
|
|
|
|
|
>
>
>
|
|
|
|
|
|
>
>
>
|
|
|
|
>
>
>
>
|
>










|
>
>

|
>
>
>
>
>

|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
..
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
...
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
....
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122

1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
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
 * Static functions defined in this file
 */
static void AddToHash(BDD_System*, BDD_BeadIndex);
				/* Add a bead to the system hash */
static unsigned int Bead2HashKeyProc(Tcl_HashTable*, void*);
static int Bead2HashKeyComparator(void*, Tcl_HashEntry*);
static Tcl_HashEntry* Bead2HashEntryAlloc(Tcl_HashTable*, void*);
static unsigned int Bead3HashKeyProc(Tcl_HashTable*, void*);
static int Bead3HashKeyComparator(void*, Tcl_HashEntry*);
static Tcl_HashEntry* Bead3HashEntryAlloc(Tcl_HashTable*, void*);
static int FindInHash(BDD_System*, BDD_VariableIndex, BDD_BeadIndex,
		      BDD_BeadIndex high);
				/* Find a bead in the system hash */
static unsigned int HashPair(BDD_BeadIndex, BDD_BeadIndex);
				/* Hashcode for a pair of integers */
static unsigned int HashTriple(BDD_VariableIndex, BDD_BeadIndex,
				BDD_BeadIndex);
................................................................................
    TCL_HASH_KEY_TYPE_VERSION,	/* version */
    0,				/* flags */
    Bead2HashKeyProc,		/* hash procedure */
    Bead2HashKeyComparator,	/* comparator */
    Bead2HashEntryAlloc,	/* allocator */
    NULL			/* standard deallocator */
};

/*
 * Hash entry type for an object indexed by three bead indices
 */
typedef struct Bead3HashEntry {
    Tcl_HashEntry parent;	/* Based on the Tcl_HashEntry */
    BDD_BeadIndex beads[3];	/* The two bead indices */
} Bead3HashEntry;

/*
 * Hash key type for an object indexed by two bead indices
 */

Tcl_HashKeyType Bead3KeyType = {
    TCL_HASH_KEY_TYPE_VERSION,	/* version */
    0,				/* flags */
    Bead3HashKeyProc,		/* hash procedure */
    Bead3HashKeyComparator,	/* comparator */
    Bead3HashEntryAlloc,	/* allocator */
    NULL			/* standard deallocator */
};
 
/*
 *-----------------------------------------------------------------------------
 *
 * Log2HashTableSize --
 *
 *	Computes the number of bits to use in a hash bucket index
 *	when the index is expected to vary between 0 and n-1
................................................................................
				 - sizeof(entryPtr->key)
				 + 2 * sizeof(BDD_BeadIndex));
    BDD_BeadIndex* outBeads = (BDD_BeadIndex*) &(entryPtr->key.oneWordValue);
    outBeads[0] = beads[0];
    outBeads[1] = beads[1];
    return entryPtr;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * Bead3HashKeyProc --
 *
 *	Compute a hashcode from a triple of bead indices
 *
 * Results:
 *	Returns the computed hashcode.
 */

static unsigned int
Bead3HashKeyProc(
    Tcl_HashTable* hashTable,	/* Hash table being processed */
    void* key)			/* Key */
{
    BDD_BeadIndex* beads = (BDD_BeadIndex*) key;
    return HashTriple(beads[0], beads[1], beads[2]);
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * Bead3HashKeyComparator --
 *
 *	Compares the keys in a hash table indexed by two bead indices
 *
 * Results:
 *	Returns 1 if the keys are equal, 0 otherwise.
 *
 *-----------------------------------------------------------------------------
 */

static int
Bead3HashKeyComparator(
    void* key1VPtr,		/* Pointer to the first key */
    Tcl_HashEntry* entryPtr)
				/* Pointer to a hash entry containing the
				 * second key */
{
    BDD_BeadIndex* key1Ptr = (BDD_BeadIndex*) key1VPtr;
    BDD_BeadIndex* key2Ptr = (BDD_BeadIndex*) &(entryPtr->key.oneWordValue);
;
    return (key1Ptr[0] == key2Ptr[0]
	    && key1Ptr[1] == key2Ptr[1]
	    && key1Ptr[2] == key2Ptr[2]);
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * Bead3HashEntryAlloc --
 *
 *	Allocates a hash entry containing two BDD_BeadIndex keys
 *
 * Results:
 *	Returns the allocated entry
 *
 *-----------------------------------------------------------------------------
 */
static Tcl_HashEntry*
Bead3HashEntryAlloc(
    Tcl_HashTable* tablePtr,	/* Hash table */
    void* keyPtr		/* Key */
) {
    BDD_BeadIndex* beads = (BDD_BeadIndex*) keyPtr;
    Tcl_HashEntry* entryPtr =
	(Tcl_HashEntry*) ckalloc(sizeof(Tcl_HashEntry)
				 - sizeof(entryPtr->key)
				 + 3 * sizeof(BDD_BeadIndex));
    BDD_BeadIndex* outBeads = (BDD_BeadIndex*) &(entryPtr->key.oneWordValue);
    outBeads[0] = beads[0];
    outBeads[1] = beads[1];
    outBeads[2] = beads[2];
    return entryPtr;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * AddToHash --
 *
 *	Adds a bead to the hash table.
................................................................................
				 * right-hand bead*/

    BDD_BeadIndex l, h;	        /* Low and high transitions of the result */
    int newFlag;		/* Flag==1 if the output is a new bead */
    BDD_BeadIndex result;	/* Return value */
    Tcl_HashEntry* entry;	/* Pointer to the entry in the
				 * cache of beads for this operation */
    BDD_BinOp opmask;		/* Mask of relevant bits for this operation */

    /* Check if the result is already hashed */

    u[0] = u1;
    u[1] = u2;
    entry = Tcl_CreateHashEntry(G, u, &newFlag);
    if (!newFlag) {
	result = (BDD_BeadIndex) Tcl_GetHashValue(entry);
	++sysPtr->beads[result].refCount;
    } else {

	/* 
	 * Check if the result is constant or a copy of one of the operands
	 */
	opmask = 0xF;
	if (u1 == 0) {
	    opmask &= 0x3;
	} else if (u1 == 1) {

	    opmask &= 0xC;
	}
	if (u2 == 0) {
	    opmask &= 0x5;
	} else if (u2 == 1) {
	    opmask &= 0xA;
	}
	if ((op & opmask) == 0) {
	    /* 
	     * Result is constant zero 
	     */
	    result = 0;
	    ++sysPtr->beads[result].refCount;
	} else if ((op & opmask) == opmask) {
	    /* 
	     * Result is constant one 
	     */
	    result = 1;
	    ++sysPtr->beads[result].refCount;
	} else if ((op & opmask) == (0xC & opmask)) {
	    /*
	     * Result is the left operand
	     */
	    result = u1;
	    ++sysPtr->beads[result].refCount;
	} else if ((op & opmask) == (0xA & opmask)) {
	    /*
	     * Result is the right operand
	     */
	    result = u2;
	    ++sysPtr->beads[result].refCount;
	} else {
	    
	    /*
	     * Result is not constant. Apply recursively to the subexpression
	     * with the earlier top variable.
	     */
	    if (u1Ptr->level == u2Ptr->level) {
		/*
		 * Both subexpressions have the same top variable
		 */
		level = u1Ptr->level;
		low1 = u1Ptr->low;
		high1 = u1Ptr->high;
		low2 = u2Ptr->low;
		high2 = u2Ptr->high;
		l = Apply(sysPtr, G, op, low1, low2);
		h = Apply(sysPtr, G, op, high1, high2);
	    } else if (u1Ptr->level < u2Ptr->level) {
		/*
		 * Apply first to the left-hand operand
		 */
		level = u1Ptr->level;
		low1 = u1Ptr->low;
		high1 = u1Ptr->high;
		l = Apply(sysPtr, G, op, low1, u2);
		h = Apply(sysPtr, G, op, high1, u2);
	    } else /* u1Ptr->level > u2Ptr->level */ {
		/*
		 * Apply first to the right-hand operand
		 */
		level = u2Ptr->level;
		low2 = u2Ptr->low;
		high2 = u2Ptr->high;
		l = Apply(sysPtr, G, op, u1, low2);
		h = Apply(sysPtr, G, op, u1, high2);
	    }
	    /*
	     * Compose the subexpressions
	     */
	    result = BDD_MakeBead(sysPtr, level, l, h);
	    BDD_UnrefBead(sysPtr, l);
	    BDD_UnrefBead(sysPtr, h);
	}
	/*
	 * Cache the result
	 */
	++sysPtr->beads[result].refCount;
	Tcl_SetHashValue(entry, result);
    }
    return result;
}

BDD_BeadIndex
BDD_Apply(
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_BinOp op,		/* Operation to apply */
    BDD_BeadIndex u1,		/* Left operand */
    BDD_BeadIndex u2) 		/* Right operand */
{
    Tcl_HashTable G;		/* Cache of partial results */
    Tcl_HashSearch search;	/* Search for clearing the cache */
    Tcl_HashEntry* entryPtr;	/* Hash entyr for clearing the cache */
    Tcl_InitCustomHashTable(&G, TCL_CUSTOM_TYPE_KEYS, &Bead2KeyType);
    BDD_BeadIndex result = Apply(sysPtr, &G, op, u1, u2);
    for (entryPtr = Tcl_FirstHashEntry(&G, &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&G);
    return result;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Apply3 --
 *
 *	Applies a Boolean operator among three BDD's.
 *
 * Results:
 *	Returns the resulting BDD.
 *
 * Side effects:
 *	Resulting BDD has a ref count of one plus any previously extant
 *	references. Caller should decrement the ref count when done.
 *
 *-----------------------------------------------------------------------------
 */

static BDD_BeadIndex
Apply3(
    BDD_System* sysPtr,		/* System of BDD's */
    Tcl_HashTable* G,		/* Hash table of partial results */
    BDD_TernOp op,		/* Operation to apply */
    BDD_BeadIndex u1,		/* First operand */
    BDD_BeadIndex u2,		/* Second operand */
    BDD_BeadIndex u3) 		/* Third operand */
{
    Bead* beads = sysPtr->beads; /* Bead table */
    BDD_BeadIndex u[3];		 /* Bead indices for left- and right-hand 
				  * sides */
    Bead* u1Ptr = beads + u1;	/* Pointer to the left-hand bead */
    Bead* u2Ptr = beads + u2;	/* Pointer to the right-hand bead */
    Bead* u3Ptr = beads + u3;	/* Pointer to the right-hand bead */
    BDD_VariableIndex level;	/* Level of the result */
    BDD_BeadIndex low1, high1;	/* Low and high transitions of the first bead */
    BDD_BeadIndex low2, high2;	/* Low and high transitions of the
				 * second bead */
    BDD_BeadIndex low3, high3;	/* Low and high transitions of the third bead */
    BDD_BeadIndex l, h;	        /* Low and high transitions of the result */
    int newFlag;		/* Flag==1 if the output is a new bead */
    BDD_BeadIndex result;	/* Return value */
    Tcl_HashEntry* entry;	/* Pointer to the entry in the
				 * cache of beads for this operation */
    BDD_TernOp opmask;		/* Mask of relevant bits for this operation */
    BDD_TernOp opfiltered;	/* Operation masked with 'opmask' */

    /* Check if the result is already hashed */

    u[0] = u1;
    u[1] = u2;
    u[2] = u3;
    entry = Tcl_CreateHashEntry(G, u, &newFlag);
    if (!newFlag) {
	result = (BDD_BeadIndex) Tcl_GetHashValue(entry);
	++sysPtr->beads[result].refCount;
    } else {

	/* 
	 * Check if the result is constant or equal to one of the operands
	 */
	opmask = 0xFF;
	if (u1 == 0) {
	    opmask &= 0x0F;
	} else if (u1 == 1) {
	    opmask &= 0xF0;
	}
	if (u2 == 0) {
	    opmask &= 0x33;
	} else if (u2 == 1) {
	    opmask &= 0xCC;
	}
	if (u3 == 0) {
	    opmask &= 0x55;
	} else if (u3 == 1) {
	    opmask &= 0xAA;
	}
	opfiltered = op & opmask;
	if (opfiltered == 0) {
	    /* 
	     * Result is constant zero 
	     */
	    result = 0;
	    ++sysPtr->beads[result].refCount;
	} else if (opfiltered == opmask) {
	    /* 
	     * Result is constant one 
	     */
	    result = 1;
	    ++sysPtr->beads[result].refCount;
	} else if (opfiltered == (0xF0 & opmask)) {
	    /*
	     * Result is the first operand
	     */
	    result = u1;
	    ++sysPtr->beads[result].refCount;
	} else if (opfiltered == (0xCC & opmask)) {
	    /*
	     * Result is the second operand
	     */
	    result = u2;
	    ++sysPtr->beads[result].refCount;
	} else if (opfiltered == (0xAA & opmask)) {
	    /*
	     * Result is the third operand
	     */
	    result = u3;
	    ++sysPtr->beads[result].refCount;
	} else {
	    /*
	     * Result is not constant. Find the top variable
	     */
	    level = u1Ptr->level;
	    if (u2Ptr->level < level) level = u2Ptr->level;
	    if (u3Ptr->level < level) level = u3Ptr->level;
	    /*
	     * Split the expressions at the top variable
	     */
	    if (u1Ptr->level > level) {
		low1 = u1;
		high1 = u1;
	    } else {
		low1 = u1Ptr->low;
		high1 = u1Ptr->high;
	    }
	    if (u2Ptr->level > level) {
		low2 = u2;
		high2 = u2;
	    } else {
		low2 = u2Ptr->low;
		high2 = u2Ptr->high;
	    }
	    if (u3Ptr->level > level) {
		low3 = u3;
		high3 = u3;
	    } else {
		low3 = u3Ptr->low;
		high3 = u3Ptr->high;
	    }
	    /*
	     * Compute the two branches from the top variable
	     */
	    l = Apply3(sysPtr, G, op, low1, low2, low3);
	    h = Apply3(sysPtr, G, op, high1, high2, high3);
	    /*
	     * Compose the subexpressions
	     */
	    result = BDD_MakeBead(sysPtr, level, l, h);
	    BDD_UnrefBead(sysPtr, l);
	    BDD_UnrefBead(sysPtr, h);
	}
	/*
	 * Cache the result
	 */
	++sysPtr->beads[result].refCount;
	Tcl_SetHashValue(entry, result);
    }
    return result;
}
BDD_BeadIndex
BDD_Apply3(
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_TernOp op,		/* Operation to apply */
    BDD_BeadIndex u1,		/* First operand */
    BDD_BeadIndex u2, 		/* Second operand */
    BDD_BeadIndex u3)		/* Third operand */
{
    Tcl_HashTable G;		/* Cache of partial results */
    Tcl_HashSearch search;	/* Search for clearing the cache */
    Tcl_HashEntry* entryPtr;	/* Hash entyr for clearing the cache */
    Tcl_InitCustomHashTable(&G, TCL_CUSTOM_TYPE_KEYS, &Bead3KeyType);
    BDD_BeadIndex result = Apply3(sysPtr, &G, op, u1, u2, u3);
    for (entryPtr = Tcl_FirstHashEntry(&G, &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&G);
    return result;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Restrict --
 *

Changes to generic/bdd.h.

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
...
131
132
133
134
135
136
137



138
139
140
141
142
143
144
 *	There are 2**2**3 = 256 possible operations. This is merely
 * a selection of the most useful ones.
 */
typedef enum BDD_TernOp {
    BDD_TERNOP_NOR = 0x01,	/* Logical NOR of three variables */
    BDD_TERNOP_ONEOF = 0x16,	/* Exactly one of three variables TRUE */
    BDD_TERNOP_TWOOF = 0x68,	/* Exactly two of three variables TRUE */
    BDD_TERNOP_XNOR = 0x69,	/* Exclusive NOR: zero or two variables TRUE */
    BDD_TERNOP_DIFFER = 0x7E,	/* At least one variable differs from
				* the other two. */
    BDD_TERNOP_NAND = 0x7F,	/* Logical NAND of three variables */
    BDD_TERNOP_AND = 0x80,	/* Logical AND of three variables */
    BDD_TERNOP_CONCUR = 0x81,	/* All three variables agree */


    BDD_TERNOP_XOR = 0x96,	/* Exclusive OR: one or three variables TRUE */
    BDD_TERNOP_IFTHENELSE = 0xCA, 
				/* a ? b : c */
    BDD_TERNOP_MAJORITY = 0xE8,	/* Majority rule: at least two of three.


				 * This is also the carry bit of a full
				 * adder */
    BDD_TERNOP_OR = 0xFE,	/* Logical OR of three variables */
} BDD_TernOp;

/*
 * Quantifiers for use with BDD's
 */
typedef enum BDD_Quantifier {
    BDD_QUANT_FORALL = BDD_BINOP_AND,

    BDD_QUANT_EXISTS = BDD_BINOP_OR,
} BDD_Quantifier;

typedef struct BDD_System BDD_System;
typedef struct BDD_AllSatState BDD_AllSatState;

/* Type of a bead index */

................................................................................
extern BDDAPI BDD_BeadIndex BDD_NotNthVariable(BDD_System* sysPtr,
					       BDD_VariableIndex n);
extern BDDAPI int BDD_Literal(BDD_System* sysPtr, BDD_BeadIndex expr,
			      BDD_ValueAssignment* assignPtr);
extern BDDAPI BDD_BeadIndex BDD_Negate(BDD_System* sysPtr, BDD_BeadIndex u);
extern BDDAPI BDD_BeadIndex BDD_Apply(BDD_System* sysPtr, BDD_BinOp op,
				      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 BDD_BeadIndex BDD_Quantify(BDD_System* sysPtr,
					 BDD_Quantifier q,
					 const BDD_VariableIndex v[],







|
|
<



>
>

|
<
|
>
>
|
<







|
>
|







 







>
>
>







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
...
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
 *	There are 2**2**3 = 256 possible operations. This is merely
 * a selection of the most useful ones.
 */
typedef enum BDD_TernOp {
    BDD_TERNOP_NOR = 0x01,	/* Logical NOR of three variables */
    BDD_TERNOP_ONEOF = 0x16,	/* Exactly one of three variables TRUE */
    BDD_TERNOP_TWOOF = 0x68,	/* Exactly two of three variables TRUE */
    BDD_TERNOP_EVEN = 0x69,	/* Exclusive NOR: zero or two variables TRUE */
    BDD_TERNOP_DIFFER = 0x7E,	/* 1 or 2 variables TRUE - disagreement. */

    BDD_TERNOP_NAND = 0x7F,	/* Logical NAND of three variables */
    BDD_TERNOP_AND = 0x80,	/* Logical AND of three variables */
    BDD_TERNOP_CONCUR = 0x81,	/* All three variables agree */
    BDD_TERNOP_BORROW = 0x8E,	/* Borrow bit of a full subtractor */
                                /* -(a-b-c) < 0 */
    BDD_TERNOP_XOR = 0x96,	/* Exclusive OR: one or three variables TRUE */
    BDD_TERNOP_IFTHENELSE = 0xCA, /* a ? b : c */

    BDD_TERNOP_MEDIAN = 0xE8,	/* Majority rule: at least two of three. */
				/* This function is the median of the three */
				/* variables. This function is also the */
				/* carry bit of a full adder: (a+b+c) > 1 */

    BDD_TERNOP_OR = 0xFE,	/* Logical OR of three variables */
} BDD_TernOp;

/*
 * Quantifiers for use with BDD's
 */
typedef enum BDD_Quantifier {
    BDD_QUANT_FORALL = BDD_BINOP_AND, /* Universal quantification */
    /* BDD_QUANT_UNIQUE - BDD_BINOP_XOR, Unique quantification is not working */
    BDD_QUANT_EXISTS = BDD_BINOP_OR,  /* Existential quantification */
} BDD_Quantifier;

typedef struct BDD_System BDD_System;
typedef struct BDD_AllSatState BDD_AllSatState;

/* Type of a bead index */

................................................................................
extern BDDAPI BDD_BeadIndex BDD_NotNthVariable(BDD_System* sysPtr,
					       BDD_VariableIndex n);
extern BDDAPI int BDD_Literal(BDD_System* sysPtr, BDD_BeadIndex expr,
			      BDD_ValueAssignment* assignPtr);
extern BDDAPI BDD_BeadIndex BDD_Negate(BDD_System* sysPtr, BDD_BeadIndex u);
extern BDDAPI BDD_BeadIndex BDD_Apply(BDD_System* sysPtr, BDD_BinOp op,
				      BDD_BeadIndex u1, BDD_BeadIndex u2);
extern BDDAPI BDD_BeadIndex BDD_Apply3(BDD_System* sysPtr, BDD_TernOp op,
				       BDD_BeadIndex u1, BDD_BeadIndex u2,
				       BDD_BeadIndex u3);
extern BDDAPI BDD_BeadIndex BDD_Restrict(BDD_System* sysPtr,
					 BDD_BeadIndex u,
					 const BDD_ValueAssignment r[],
					 BDD_VariableIndex n);
extern BDDAPI BDD_BeadIndex BDD_Quantify(BDD_System* sysPtr,
					 BDD_Quantifier q,
					 const BDD_VariableIndex v[],

Changes to generic/tclBdd.c.

123
124
125
126
127
128
129


130
131
132
133
134
135
136
...
231
232
233
234
235
236
237







238
239
240
241
242
243
244
...
246
247
248
249
250
251
252

253
254
255
256
257
258
259



260



261

262
263
264
265
266
267

268

269

270
271

272
273

274
275
276
277
278
279
280
281
282
283
284
....
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
....
1155
1156
1157
1158
1159
1160
1161



1162


1163
1164
1165
1166
1167
1168
1169
....
1312
1313
1314
1315
1316
1317
1318





































































1319
1320
1321
1322
1323
1324
1325
				 int, Tcl_Obj* const[]);
static int BddSystemQuantifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemRestrictMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemSatcountMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);


static int BddSystemUnsetMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int CloneBddSystemObject(Tcl_Interp*, ClientData, ClientData*);
static int CloneMethod(Tcl_Interp*, ClientData, ClientData*);
static void DeleteBddSystemData(BddSystemData*);
static void DeleteBddSystemObject(ClientData);
static void DeleteMethod(ClientData);
................................................................................
const static Tcl_MethodType BddSystemSatcountMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "satcount",			   /* name */
    BddSystemSatcountMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};







const static Tcl_MethodType BddSystemUnsetMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "unset",			   /* name */
    BddSystemUnsetMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
................................................................................
/*
 * Method table for the BDD system object
 */

MethodTableRow systemMethodTable[] = {
    { "!=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NE },
    { "&",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_AND },

    { ":=",        &BddSystemCopyMethodType,      NULL },
    { "<",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LT },
    { "<=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LE },
    { "==",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_EQ },
    { ">",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GT },
    { ">=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GE },
    { "^",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_XOR },



    { "beadindex", &BddSystemBeadindexMethodType, NULL },



    { "dump",      &BddSystemDumpMethodType,      NULL },

    { "exists",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_EXISTS },
    { "forall",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_FORALL },
    { "foreach_sat",
                   &BddSystemForeachSatMethodType,NULL },

    { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },

    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },

    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },

    { "restrict",  &BddSystemRestrictMethodType,  NULL },
    { "satcount",  &BddSystemSatcountMethodType,  NULL },

    { "unset",     &BddSystemUnsetMethodType,     NULL },
    { "|",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_OR },
    { "~",         &BddSystemNegateMethodType,    NULL },
    { NULL,	   NULL,                         NULL }
};
 
/*
 *-----------------------------------------------------------------------------
 *
 * Tclbdd_Init --
 *
................................................................................
 * BddSystemQuantifyMethod --
 *
 *	Quantifies a BDD with respect to a particular set of variables.
 *
 * Usage:
 *	$system exists $name $vars $expr
 *	$system forall $name $vars $expr
 *	$system unique $name $vars $expr
 *
 * Parameters:
 *	system - System of BDD's
 *	name - Name to assign to the resulting expression.
 *	vars - List of literals that must be un-negated variable names
 *	expr - Expression to quantify.
 *
................................................................................
    }

    /*
     * Order the literals
     */
    qsort(v, varc, sizeof(BDD_VariableIndex), CompareVariableIndices);




    result = BDD_Quantify(sdata->system, q, v, varc, u);


    SetNamedExpression(sdata, objv[skipped], result);
    BDD_UnrefBead(sdata->system, result);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
................................................................................
    }
    mp_init(&satCount);
    BDD_SatCount(sdata->system, beadIndex, &satCount);
    Tcl_SetObjResult(interp, Tcl_NewBignumObj(&satCount));

    return TCL_OK;
}





































































 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemUnsetMethod --
 *
 *	Forgets a named expression







>
>







 







>
>
>
>
>
>
>







 







>







>
>
>

>
>
>

>






>

>

>


>


>



|







 







|







 







>
>
>

>
>







 







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







123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
...
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
...
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
....
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
....
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
....
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
				 int, Tcl_Obj* const[]);
static int BddSystemQuantifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemRestrictMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemSatcountMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemTernopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				 int, Tcl_Obj* const[]);
static int BddSystemUnsetMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int CloneBddSystemObject(Tcl_Interp*, ClientData, ClientData*);
static int CloneMethod(Tcl_Interp*, ClientData, ClientData*);
static void DeleteBddSystemData(BddSystemData*);
static void DeleteBddSystemObject(ClientData);
static void DeleteMethod(ClientData);
................................................................................
const static Tcl_MethodType BddSystemSatcountMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "satcount",			   /* name */
    BddSystemSatcountMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemTernopMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "ternop",			   /* name */
    BddSystemTernopMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};				   /* common to all ternary operators */
const static Tcl_MethodType BddSystemUnsetMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "unset",			   /* name */
    BddSystemUnsetMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
................................................................................
/*
 * Method table for the BDD system object
 */

MethodTableRow systemMethodTable[] = {
    { "!=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NE },
    { "&",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_AND },
    { "&3",        &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_AND },
    { ":=",        &BddSystemCopyMethodType,      NULL },
    { "<",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LT },
    { "<=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LE },
    { "==",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_EQ },
    { ">",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GT },
    { ">=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GE },
    { "^",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_XOR },
    { "^3",        &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_XOR },
    { "?:",        &BddSystemTernopMethodType,    
                                           (ClientData) BDD_TERNOP_IFTHENELSE },
    { "beadindex", &BddSystemBeadindexMethodType, NULL },
    { "borrow",    &BddSystemTernopMethodType, (ClientData) BDD_TERNOP_BORROW },
    { "concur3",   &BddSystemTernopMethodType, (ClientData) BDD_TERNOP_CONCUR },
    { "differ3",   &BddSystemTernopMethodType, (ClientData) BDD_TERNOP_DIFFER },
    { "dump",      &BddSystemDumpMethodType,      NULL },
    { "even3",     &BddSystemTernopMethodType,   (ClientData) BDD_TERNOP_EVEN },
    { "exists",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_EXISTS },
    { "forall",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_FORALL },
    { "foreach_sat",
                   &BddSystemForeachSatMethodType,NULL },
    { "median" ,   &BddSystemTernopMethodType, (ClientData) BDD_TERNOP_MEDIAN },
    { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },
    { "nand3",     &BddSystemTernopMethodType,   (ClientData) BDD_TERNOP_NAND },
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "nor3",      &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
    { "oneof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_ONEOF },
    { "restrict",  &BddSystemRestrictMethodType,  NULL },
    { "satcount",  &BddSystemSatcountMethodType,  NULL },
    { "twoof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_TWOOF },
    { "unset",     &BddSystemUnsetMethodType,     NULL },
    { "|",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_OR },
    { "~",         &BddSystemNegateMethodType,    NULL },
    { NULL,	   NULL,                          NULL }
};
 
/*
 *-----------------------------------------------------------------------------
 *
 * Tclbdd_Init --
 *
................................................................................
 * BddSystemQuantifyMethod --
 *
 *	Quantifies a BDD with respect to a particular set of variables.
 *
 * Usage:
 *	$system exists $name $vars $expr
 *	$system forall $name $vars $expr
 *	$system unique $name $vars $expr  (NOT YET IMPLEMENTED)
 *
 * Parameters:
 *	system - System of BDD's
 *	name - Name to assign to the resulting expression.
 *	vars - List of literals that must be un-negated variable names
 *	expr - Expression to quantify.
 *
................................................................................
    }

    /*
     * Order the literals
     */
    qsort(v, varc, sizeof(BDD_VariableIndex), CompareVariableIndices);

    /*
     * Quantify the formula
     */
    result = BDD_Quantify(sdata->system, q, v, varc, u);

    ckfree(v);
    SetNamedExpression(sdata, objv[skipped], result);
    BDD_UnrefBead(sdata->system, result);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
................................................................................
    }
    mp_init(&satCount);
    BDD_SatCount(sdata->system, beadIndex, &satCount);
    Tcl_SetObjResult(interp, Tcl_NewBignumObj(&satCount));

    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemTernopMethod --
 *
 *	Computes a ternary operation among three expressions in a BDD system
 *	and assigns it a name
 *
 * Usage:
 *	$system OP a b c d
 *
 * Parameters:
 *	OP - One of the ternary operators
 *	a - Name of the result expression
 *	b - Name of the first operand
 *	c - Name of the second operand
 *	d - Name of the third operand
 *
 * Results:
 *	None
 *
 * Side effects:
 *	Assigns the given name to the result expression
 *
 *-----------------------------------------------------------------------------
 */

static int
BddSystemTernopMethod(
    ClientData clientData,	/* Operation to perform */
    Tcl_Interp* interp,		/* Tcl interpreter */
    Tcl_ObjectContext ctx,	/* Object context */
    int objc,			/* Parameter count */
    Tcl_Obj *const objv[])	/* Parameter vector */
{
    Tcl_Object thisObject = Tcl_ObjectContextObject(ctx);
				/* The current object */
    BddSystemData* sdata = (BddSystemData*)
	Tcl_ObjectGetMetadata(thisObject, &BddSystemDataType);
				/* The current system of expressions */
    int skipped = Tcl_ObjectContextSkippedArgs(ctx);
				/* The number of args used in method dispatch */
    BDD_BeadIndex beadIndexOpd1; /* The bead index of the first operand */
    BDD_BeadIndex beadIndexOpd2; /* The bead index of the second operand */
    BDD_BeadIndex beadIndexOpd3; /* The bead index of the third operand */
    BDD_BeadIndex beadIndexResult; /* The bead index of the result */

    /* Check syntax */

    if (objc != skipped+4) {
	Tcl_WrongNumArgs(interp, skipped, objv,
			 "result operand1 operand2 operand3");
	return TCL_ERROR;
    }
    if (FindNamedExpression(interp, sdata, objv[skipped+1],
			    &beadIndexOpd1) != TCL_OK
	|| FindNamedExpression(interp, sdata, objv[skipped+2],
			       &beadIndexOpd2) != TCL_OK
	|| FindNamedExpression(interp, sdata, objv[skipped+3],
			       &beadIndexOpd3) != TCL_OK) {
	return TCL_ERROR;
    }
    beadIndexResult = BDD_Apply3(sdata->system, (BDD_TernOp) (size_t)clientData,
				 beadIndexOpd1, beadIndexOpd2, beadIndexOpd3);
    SetNamedExpression(sdata, objv[skipped], beadIndexResult);
    BDD_UnrefBead(sdata->system, beadIndexResult);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemUnsetMethod --
 *
 *	Forgets a named expression

Changes to tests/bdd.test.

1218
1219
1220
1221
1222
1223
1224










































































































































































































































































1225
1226
1227
1228
1229
1230
1231
1232
....
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
....
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
    }
    -cleanup {
	rename sys {}
    }
    -result {6 testing}
}











































































































































































































































































test bdd-15.n {existential quantifier} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	sys nthvar e 4; sys notnthvar !e 4
	sys nthvar f 5; sys notnthvar !f 5
	sys & expr !e !f; sys & expr expr a
	sys & term !e  f; sys & term term b; sys | expr expr term
................................................................................
	sys exists ze {e f} expr
	expr {[sys beadindex ze] == [sys beadindex ye]}
    }
    -cleanup {rename sys {}}
    -result {1}
}

test bdd-15.n {universal quantifier} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	sys nthvar e 4; sys notnthvar !e 4
	sys nthvar f 5; sys notnthvar !f 5
	sys & expr !e !f; sys & expr expr a
	sys & term !e  f; sys & term term b; sys | expr expr term
................................................................................
	sys & yu yu d
	sys forall zu {e f} expr
	expr {[sys beadindex zu] == [sys beadindex yu]}
    }
    -cleanup {rename sys {}}
    -result {1}
}
    

test bdd-21.1 {eight queens} {*}{
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 64} {incr i} {
	    sys nthvar v$i $i; sys notnthvar !v$i $i
	}







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|







 







|







 







<







1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
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
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
....
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
....
1527
1528
1529
1530
1531
1532
1533

1534
1535
1536
1537
1538
1539
1540
    }
    -cleanup {
	rename sys {}
    }
    -result {6 testing}
}

test bdd-15.1.1 {quantifiers - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys exists
    }
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
    -result {wrong # args: *}
}

test bdd-15.1.2 {quantifiers - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys forall
    }
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
    -result {wrong # args: *}
}

test bdd-15.2.1 {quantifiers - bad expression} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys exists x {} garbage} result] $result $::errorCode
    }
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-15.2.2 {quantifiers - bad expression} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys forall x {} garbage} result] $result $::errorCode
    }
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-15.3.1 {quantifiers - ill-formed list} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys exists x \{ 1
    }
    -cleanup {
	rename sys {}
    }
    -returnCodes error
    -result {unmatched open brace in list}
}

test bdd-15.3.2 {quantifiers - ill-formed list} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys forall x \{ 1
    }
    -cleanup {
	rename sys {}
    }
    -returnCodes error
    -result {unmatched open brace in list}
}

test bdd-15.4.1 {quantifiers - bad variable} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys exists x {garbage} 1} result] $result $::errorCode
    }
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-15.4.2 {quantifiers - bad variable} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys forall x {garbage} 1} result] $result $::errorCode
    }
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-15.5.1 {quantifiers - bad variable} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys exists x {1} 1} result] $result $::errorCode
    }
    -cleanup {rename sys {}}
    -result \
	{1 {1 is not a variable} {BDD NotVariable 1}}
}

test bdd-15.5.2 {quantifiers - bad variable} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys forall x {1} 1} result] $result $::errorCode
    }
    -cleanup {rename sys {}}
    -result \
	{1 {1 is not a variable} {BDD NotVariable 1}}
}

test bdd-15.6.1 {quantifiers - bad variable} {*}{
    -setup {
	bdd::system create sys
	sys notnthvar !a 0
    }
    -body {
	list [catch {sys exists x !a 1} result] $result $::errorCode
    }
    -cleanup {rename sys {}}
    -result \
	{1 {!a is not a variable} {BDD NotVariable !a}}
}

test bdd-15.6.2 {quantifiers - bad variable} {*}{
    -setup {
	bdd::system create sys
	sys notnthvar !a 0
    }
    -body {
	list [catch {sys forall x !a 1} result] $result $::errorCode
    }
    -cleanup {rename sys {}}
    -result \
	{1 {!a is not a variable} {BDD NotVariable !a}}
}

test bdd-15.7.1 {quantifiers - bad variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys ^ c a b
    }
    -body {
	list [catch {sys exists x c 1} result] $result $::errorCode
    }
    -cleanup {rename sys {}}
    -result {1 {c is not a variable} {BDD NotVariable c}}
}

test bdd-15.7.2 {quantifiers - bad variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys ^ c a b
    }
    -body {
	list [catch {sys forall x c 1} result] $result $::errorCode
    }
    -cleanup {rename sys {}}
    -result {1 {c is not a variable} {BDD NotVariable c}}
}

test bdd-15.8.1 {quantifiers - do nothing gracefully} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys ^ c a b
    }
    -body {
	set result {}
	foreach ex {0 1 a b c} {
	    sys exists z {} $ex
	    lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	}
	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1}
}

test bdd-15.8.2 {quantifiers - do nothing gracefully} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys ^ c a b
    }
    -body {
	set result {}
	foreach ex {0 1 a b c} {
	    sys forall z {} $ex
	    lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	}
	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1}
}

test bdd-15.9.1 {quantifiers - irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
	sys nthvar q 2
	sys nthvar b 3
	sys nthvar r 4
	sys ^ c a b
    }
    -body {
	set result {}
	foreach v {p q r} {
	    foreach ex {0 1 a b c} {
		sys exists z $v $ex
		lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	    }
	}
	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1 1 1 1 1 1 1 1 1 1 1}
}

test bdd-15.9.2 {quantifiers - irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
	sys nthvar q 2
	sys nthvar b 3
	sys nthvar r 4
	sys ^ c a b
    }
    -body {
	set result {}
	foreach v {p q r} {
	    foreach ex {0 1 a b c} {
		sys forall z $v $ex
		lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	    }
	}
	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1 1 1 1 1 1 1 1 1 1 1}
}

test bdd-15.10 {existential quantifier} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	sys nthvar e 4; sys notnthvar !e 4
	sys nthvar f 5; sys notnthvar !f 5
	sys & expr !e !f; sys & expr expr a
	sys & term !e  f; sys & term term b; sys | expr expr term
................................................................................
	sys exists ze {e f} expr
	expr {[sys beadindex ze] == [sys beadindex ye]}
    }
    -cleanup {rename sys {}}
    -result {1}
}

test bdd-15.11 {universal quantifier} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	sys nthvar e 4; sys notnthvar !e 4
	sys nthvar f 5; sys notnthvar !f 5
	sys & expr !e !f; sys & expr expr a
	sys & term !e  f; sys & term term b; sys | expr expr term
................................................................................
	sys & yu yu d
	sys forall zu {e f} expr
	expr {[sys beadindex zu] == [sys beadindex yu]}
    }
    -cleanup {rename sys {}}
    -result {1}
}


test bdd-21.1 {eight queens} {*}{
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 64} {incr i} {
	    sys nthvar v$i $i; sys notnthvar !v$i $i
	}