tclbdd

Check-in [61ca0d0495]
Login

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

Overview
Comment:Added operator to the key of 'applyCache' so that multiple applications can be in flight at once.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:61ca0d04953414fd130d192d3cc924e2029b012a
User & Date: kbk 2013-12-10 12:33:07
Context
2013-12-10
13:19
Flesh out ApplyAndQuantify. Needs the outer layers. check-in: bdc21889cb user: kbk tags: trunk
12:33
Added operator to the key of 'applyCache' so that multiple applications can be in flight at once. check-in: 61ca0d0495 user: kbk tags: trunk
12:25
Broke off the easy cases from Apply (to be used in ApplyAndQuantify) check-in: 3016cbe3d8 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
....
1188
1189
1190
1191
1192
1193
1194

1195


1196
1197
1198

1199
1200
1201
1202
1203
1204
1205
....
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
....
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_BeadIndex u1,		/* Left operand */
    BDD_BeadIndex u2) 		/* Right operand */
{
    BDD_BinOp op = sysPtr->applyOp;
				/* Operation to apply */
    Bead* beads = sysPtr->beads; /* Bead table */
    BDD_BeadIndex u[2];		/* 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 */
    BDD_VariableIndex level;	/* Level of the result */
    BDD_BeadIndex low1, high1;	/* Low and high transitions of the 
				 * left-hand bead */
    BDD_BeadIndex low2, high2;	/* Low and high transitions of the
................................................................................

    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 */


    /* Check if the result is already hashed */



    u[0] = u1;
    u[1] = u2;

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

	/*
................................................................................
    BDD_BinOp op,		/* Operation to apply */
    BDD_BeadIndex u1,		/* Left operand */
    BDD_BeadIndex u2) 		/* Right operand */
{
    Tcl_HashSearch search;	/* Search for clearing the cache */
    Tcl_HashEntry* entryPtr;	/* Hash entyr for clearing the cache */
    Tcl_InitCustomHashTable(&(sysPtr->applyCache),
			    TCL_CUSTOM_TYPE_KEYS, &Bead2KeyType);
    sysPtr->applyOp = op;
    BDD_BeadIndex result = Apply(sysPtr, u1, u2);
    for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->applyCache), &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
................................................................................
{
    Tcl_HashSearch search;	/* Search state for clearing the hash */
    Tcl_HashEntry* entryPtr;	/* Hash table entry to be cleared */

    BDD_BeadIndex r;		/* Return value */

    Tcl_InitCustomHashTable(&(sysPtr->applyCache),
			    TCL_CUSTOM_TYPE_KEYS, &Bead2KeyType);
    sysPtr->quantifier = q;
    Tcl_InitHashTable(&(sysPtr->quantifyCache), TCL_ONE_WORD_KEYS);

    r = Quantify(sysPtr, n, v, e);

    for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->quantifyCache), &search);
	 entryPtr != NULL;







|







 







>
|
>
>

|
|
>







 







|







 







|







1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
....
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
....
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
....
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_BeadIndex u1,		/* Left operand */
    BDD_BeadIndex u2) 		/* Right operand */
{
    BDD_BinOp op = sysPtr->applyOp;
				/* Operation to apply */
    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 */
    BDD_VariableIndex level;	/* Level of the result */
    BDD_BeadIndex low1, high1;	/* Low and high transitions of the 
				 * left-hand bead */
    BDD_BeadIndex low2, high2;	/* Low and high transitions of the
................................................................................

    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 */

    /* 
     * Check if the result is already hashed. Note that the operator
     * is included in the cache because relational joins have the cache
     * active for AND and for OR (EXISTS) simultaneously */

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

	/*
................................................................................
    BDD_BinOp op,		/* Operation to apply */
    BDD_BeadIndex u1,		/* Left operand */
    BDD_BeadIndex u2) 		/* Right operand */
{
    Tcl_HashSearch search;	/* Search for clearing the cache */
    Tcl_HashEntry* entryPtr;	/* Hash entyr for clearing the cache */
    Tcl_InitCustomHashTable(&(sysPtr->applyCache),
			    TCL_CUSTOM_TYPE_KEYS, &Bead3KeyType);
    sysPtr->applyOp = op;
    BDD_BeadIndex result = Apply(sysPtr, u1, u2);
    for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->applyCache), &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
................................................................................
{
    Tcl_HashSearch search;	/* Search state for clearing the hash */
    Tcl_HashEntry* entryPtr;	/* Hash table entry to be cleared */

    BDD_BeadIndex r;		/* Return value */

    Tcl_InitCustomHashTable(&(sysPtr->applyCache),
			    TCL_CUSTOM_TYPE_KEYS, &Bead3KeyType);
    sysPtr->quantifier = q;
    Tcl_InitHashTable(&(sysPtr->quantifyCache), TCL_ONE_WORD_KEYS);

    r = Quantify(sysPtr, n, v, e);

    for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->quantifyCache), &search);
	 entryPtr != NULL;