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 Side-by-Side Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

  1172   1172       BDD_System* sysPtr,		/* System of BDD's */
  1173   1173       BDD_BeadIndex u1,		/* Left operand */
  1174   1174       BDD_BeadIndex u2) 		/* Right operand */
  1175   1175   {
  1176   1176       BDD_BinOp op = sysPtr->applyOp;
  1177   1177   				/* Operation to apply */
  1178   1178       Bead* beads = sysPtr->beads; /* Bead table */
  1179         -    BDD_BeadIndex u[2];		/* Bead indices for left- and right-hand 
         1179  +    BDD_BeadIndex u[3];		/* Bead indices for left- and right-hand 
  1180   1180   				 * sides */
  1181   1181       Bead* u1Ptr = beads + u1;	/* Pointer to the left-hand bead */
  1182   1182       Bead* u2Ptr = beads + u2;	/* Pointer to the right-hand bead */
  1183   1183       BDD_VariableIndex level;	/* Level of the result */
  1184   1184       BDD_BeadIndex low1, high1;	/* Low and high transitions of the 
  1185   1185   				 * left-hand bead */
  1186   1186       BDD_BeadIndex low2, high2;	/* Low and high transitions of the
................................................................................
  1188   1188   
  1189   1189       BDD_BeadIndex l, h;	        /* Low and high transitions of the result */
  1190   1190       int newFlag;		/* Flag==1 if the output is a new bead */
  1191   1191       BDD_BeadIndex result;	/* Return value */
  1192   1192       Tcl_HashEntry* entry;	/* Pointer to the entry in the
  1193   1193   				 * cache of beads for this operation */
  1194   1194   
  1195         -    /* Check if the result is already hashed */
         1195  +    /* 
         1196  +     * Check if the result is already hashed. Note that the operator
         1197  +     * is included in the cache because relational joins have the cache
         1198  +     * active for AND and for OR (EXISTS) simultaneously */
  1196   1199   
  1197         -    u[0] = u1;
  1198         -    u[1] = u2;
         1200  +    u[0] = op;
         1201  +    u[1] = u1;
         1202  +    u[2] = u2;
  1199   1203       entry = Tcl_CreateHashEntry(&(sysPtr->applyCache), u, &newFlag);
  1200   1204       if (!newFlag) {
  1201   1205   	result = (BDD_BeadIndex) Tcl_GetHashValue(entry);
  1202   1206   	++sysPtr->beads[result].refCount;
  1203   1207       } else {
  1204   1208   
  1205   1209   	/*
................................................................................
  1264   1268       BDD_BinOp op,		/* Operation to apply */
  1265   1269       BDD_BeadIndex u1,		/* Left operand */
  1266   1270       BDD_BeadIndex u2) 		/* Right operand */
  1267   1271   {
  1268   1272       Tcl_HashSearch search;	/* Search for clearing the cache */
  1269   1273       Tcl_HashEntry* entryPtr;	/* Hash entyr for clearing the cache */
  1270   1274       Tcl_InitCustomHashTable(&(sysPtr->applyCache),
  1271         -			    TCL_CUSTOM_TYPE_KEYS, &Bead2KeyType);
         1275  +			    TCL_CUSTOM_TYPE_KEYS, &Bead3KeyType);
  1272   1276       sysPtr->applyOp = op;
  1273   1277       BDD_BeadIndex result = Apply(sysPtr, u1, u2);
  1274   1278       for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->applyCache), &search);
  1275   1279   	 entryPtr != NULL;
  1276   1280   	 entryPtr = Tcl_NextHashEntry(&search)) {
  1277   1281   	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
  1278   1282       }
................................................................................
  1691   1695   {
  1692   1696       Tcl_HashSearch search;	/* Search state for clearing the hash */
  1693   1697       Tcl_HashEntry* entryPtr;	/* Hash table entry to be cleared */
  1694   1698   
  1695   1699       BDD_BeadIndex r;		/* Return value */
  1696   1700   
  1697   1701       Tcl_InitCustomHashTable(&(sysPtr->applyCache),
  1698         -			    TCL_CUSTOM_TYPE_KEYS, &Bead2KeyType);
         1702  +			    TCL_CUSTOM_TYPE_KEYS, &Bead3KeyType);
  1699   1703       sysPtr->quantifier = q;
  1700   1704       Tcl_InitHashTable(&(sysPtr->quantifyCache), TCL_ONE_WORD_KEYS);
  1701   1705   
  1702   1706       r = Quantify(sysPtr, n, v, e);
  1703   1707   
  1704   1708       for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->quantifyCache), &search);
  1705   1709   	 entryPtr != NULL;