tclbdd

Check-in [f726758694]
Login

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

Overview
Comment:Revised caching in Quantify and Restrict, cleaned up commentary.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:f726758694308541f4b66c735a29b8b8bc9d729d
User & Date: kbk 2013-12-07 03:08:15
Context
2013-12-09
03:38
Finished and debugged implementation and test suite of 'compose', plus fixed several additional memory management bugs. check-in: fec3a9366b user: kbk tags: trunk
2013-12-07
03:08
Revised caching in Quantify and Restrict, cleaned up commentary. check-in: f726758694 user: kbk tags: trunk
2013-12-06
05:08
test ternary operators - add missing ternary OR check-in: 70e321ed7a user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
....
1274
1275
1276
1277
1278
1279
1280








1281
1282
1283
1284
1285
1286
1287
1288
1289
....
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
....
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
....
1518
1519
1520
1521
1522
1523
1524
1525
1526


1527
1528
1529
1530
1531
1532
1533
....
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
....
1605
1606
1607
1608
1609
1610
1611


1612

1613
1614

1615


1616

















































































1617



















1618
1619
1620
1621
1622
1623
1624

1625


1626

1627

1628
1629
1630
1631
1632
1633
1634
	 * 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 */
{
................................................................................
    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) {
................................................................................
 *
 * Results:
 *	Returns the restricted BDD. Refcount must be decremented by
 *	the caller when the caller is done with the BDD.
 *
 * Notes:
 *	The restrictions must be listed in ascending order by variable
 *	number.
 *
 *-----------------------------------------------------------------------------
 */
static BDD_BeadIndex
Restrict(
    Tcl_HashTable* H,		/* Hash table of precomputed values */
    BDD_System* sysPtr,		/* System of BDD's */
................................................................................
	++sysPtr->beads[u].refCount;
	return u;
    }

    /* Has this value been computed already? */

    entryPtr = Tcl_CreateHashEntry(H, u, &newFlag);
    if (newFlag) {
	Tcl_SetHashValue(entryPtr, 0);
    }
    BDD_BeadIndex cached = (BDD_BeadIndex) Tcl_GetHashValue(entryPtr);
    if (cached != 0) {
	++sysPtr->beads[cached].refCount;
	return cached;

    }

    /*
     * Value is not cached. Handle the first variable of the restriction
     */
    BDD_BeadIndex rvar = r[0].var;
    BDD_BeadIndex uvar = sysPtr->beads[u].level;










    if (rvar < uvar) {
	/*
	 * r[0] is an irrelevant variable in u
	 */
	result = Restrict(H, sysPtr, u, r+1, n-1);
    } else if (rvar == uvar) {
	/*
	 * r[0] appears in u. Bind it.
	 */
	if (r[0].value) {


	    result = Restrict(H, sysPtr, sysPtr->beads[u].high, r+1, n-1);
	} else {
	    result = Restrict(H, sysPtr, sysPtr->beads[u].low, r+1, n-1);



	}
    } else /* rvar > uvar */ {
	/*
	 * u's first variable is unrestricted. Apply the restriction to both
	 * successors of u, and make a bead for the restricted expression.
	 */
	l = Restrict(H, sysPtr, sysPtr->beads[u].low, r, n);
................................................................................
 *	Returns a BDD representing the quantified expression.
 *
 *-----------------------------------------------------------------------------
 */

static BDD_BeadIndex
Quantify(
    Tcl_HashTable* H,		/* Hash table of cached partial results */
    BDD_System* sysPtr,		/* Pointer to the system of BDD's */


    BDD_Quantifier q,		/* Quantifier to apply */
    const BDD_VariableIndex* v,	/* Variables to quantify */
    BDD_VariableIndex n,	/* Number of quantified variables */
    BDD_BeadIndex u)		/* Expression to quantify */
{
    BDD_BeadIndex l;		/* Low transition of the result */
    BDD_BeadIndex h;		/* High transition of the result */
................................................................................
	    r = u;
	    break;
	} else if (beadPtr->level < *v) {
	    /*
	     * The current variable in the expression is unquantified.
	     * Quantify the two subexpressions and make the result
	     */
	    l = Quantify(H, sysPtr, q, v, n, beadPtr->low);
	    h = Quantify(H, sysPtr, q, v, n, beadPtr->high);
	    r = BDD_MakeBead(sysPtr, beadPtr->level, l, h);
	    BDD_UnrefBead(sysPtr,h);
	    BDD_UnrefBead(sysPtr,l);
	    break;
	} else if (beadPtr->level == *v) {
	    /*
	     * The current variable in the expression is quantified.
	     * Quantify the two subexpressions with respect to the
	     * remaining variables and then apply the combining operation.
	     *
	     * Would it be advantageous to cache more aggressively here,
	     * rather than creating/destroying the hash table in BDD_Apply?
	     */
	    l = Quantify(H, sysPtr, q, v+1, n-1, beadPtr->low);
	    h = Quantify(H, sysPtr, q, v+1, n-1, beadPtr->high);
	    r = BDD_Apply(sysPtr, q, l, h);
	    BDD_UnrefBead(sysPtr,h);
	    BDD_UnrefBead(sysPtr,l);
	    break;
	} else {
	    /* 
	     * The current variable does not appear free in the expression,
	     * The quantification is trivially satisfied with respect to the
................................................................................
BDD_Quantify(
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_Quantifier q,		/* Quantifier to apply */
    const BDD_VariableIndex* v,	/* List of variables to quantify */
    BDD_VariableIndex n,	/* Number of variables to quantify */
    BDD_BeadIndex e)		/* Expression to quantify */
{


    Tcl_HashTable H;		/* Hash table to cache partial results */

    Tcl_HashSearch search;	/* Search state for clearing the hash */
    Tcl_HashEntry* entryPtr;	/* Hash table entry to be cleared */

    BDD_BeadIndex c;		/* Cached result */


    Tcl_InitHashTable(&H, TCL_ONE_WORD_KEYS);

















































































    BDD_BeadIndex r = Quantify(&H, sysPtr, q, v, n, e);



















    for (entryPtr = Tcl_FirstHashEntry(&H, &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	c = (BDD_BeadIndex) Tcl_GetHashValue(entryPtr);
	BDD_UnrefBead(sysPtr, c);
    }
    Tcl_DeleteHashTable(&H);

    return r;


	 

    

}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_SatCount --
 *







<







 







>
>
>
>
>
>
>
>

<







 







|







 







|
|
|
|
|
|
|
>







>
>
>
>
>
>
>
>
>
>









|
>
>


<
>
>
>







 







<

>
>







 







|
|









|
<
<
<
|
|
|







 







>
>
|
>


>
|
>
>

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



<
|


>
|
>
>
|
>
|
>







1198
1199
1200
1201
1202
1203
1204

1205
1206
1207
1208
1209
1210
1211
....
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288

1289
1290
1291
1292
1293
1294
1295
....
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
....
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
1499
1500
1501
1502
....
1539
1540
1541
1542
1543
1544
1545

1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
....
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595



1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
....
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
1643
1644
1645
1646
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
1675
1676
1677
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729
1730
1731
1732
1733
1734
1735
1736
1737
1738
1739
1740
1741
1742
1743
1744
1745

1746
1747
1748
1749
1750
1751
1752
1753
1754
1755
1756
1757
1758
1759
1760
1761
1762
1763
	 * 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 */
{
................................................................................
    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 if (op == BDD_TERNOP_IFTHENELSE && u2 == u3) {
	/*
	 * Special case - if the op is IFTHENELSE, and both the IF and
	 * ELSE cases are the same bead, we can prune the search.
	 * (This case is here because it helps performance in Compose)
	 */
	result = u2;
	++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) {
................................................................................
 *
 * Results:
 *	Returns the restricted BDD. Refcount must be decremented by
 *	the caller when the caller is done with the BDD.
 *
 * Notes:
 *	The restrictions must be listed in ascending order by variable
 *	number. The values of r[].value must be Boolean constants.
 *
 *-----------------------------------------------------------------------------
 */
static BDD_BeadIndex
Restrict(
    Tcl_HashTable* H,		/* Hash table of precomputed values */
    BDD_System* sysPtr,		/* System of BDD's */
................................................................................
	++sysPtr->beads[u].refCount;
	return u;
    }

    /* Has this value been computed already? */

    entryPtr = Tcl_CreateHashEntry(H, u, &newFlag);
    if (!newFlag) {
	result = (BDD_BeadIndex)(size_t)Tcl_GetHashValue(entryPtr);
	if (result != !(BDD_BeadIndex)0) {
	    ++sysPtr->beads[result].refCount;
	    return result;
	}
    } else {
	Tcl_SetHashValue(entryPtr, ~(BDD_BeadIndex)0);
    }

    /*
     * Value is not cached. Handle the first variable of the restriction
     */
    BDD_BeadIndex rvar = r[0].var;
    BDD_BeadIndex uvar = sysPtr->beads[u].level;
    if (n > 1) {
	/*
	 * Consistency check on variable ordering.
	 */
	BDD_BeadIndex nextvar = r[1].var;
	if (nextvar <= rvar) {
	    Tcl_Panic("variables %lu and %lu in BDD_Restrict are out of order.",
		      rvar, nextvar);
	}
    }
    if (rvar < uvar) {
	/*
	 * r[0] is an irrelevant variable in u
	 */
	result = Restrict(H, sysPtr, u, r+1, n-1);
    } else if (rvar == uvar) {
	/*
	 * r[0] appears in u. Bind it.
	 */
	if (r[0].value == 0) {
	    result = Restrict(H, sysPtr, sysPtr->beads[u].low, r+1, n-1);
	} else if (r[0].value == 1) {
	    result = Restrict(H, sysPtr, sysPtr->beads[u].high, r+1, n-1);
	} else {

	    Tcl_Panic("BDD_Restrict called with non-constant value for "
		      "variable %lu\n", rvar);
	    result = 0;		/* silence compiler warnings */
	}
    } else /* rvar > uvar */ {
	/*
	 * u's first variable is unrestricted. Apply the restriction to both
	 * successors of u, and make a bead for the restricted expression.
	 */
	l = Restrict(H, sysPtr, sysPtr->beads[u].low, r, n);
................................................................................
 *	Returns a BDD representing the quantified expression.
 *
 *-----------------------------------------------------------------------------
 */

static BDD_BeadIndex
Quantify(

    BDD_System* sysPtr,		/* Pointer to the system of BDD's */
    Tcl_HashTable* G,	        /* Cached partial results of Apply */
    Tcl_HashTable* H,		/* Cached partial results of Quantify */
    BDD_Quantifier q,		/* Quantifier to apply */
    const BDD_VariableIndex* v,	/* Variables to quantify */
    BDD_VariableIndex n,	/* Number of quantified variables */
    BDD_BeadIndex u)		/* Expression to quantify */
{
    BDD_BeadIndex l;		/* Low transition of the result */
    BDD_BeadIndex h;		/* High transition of the result */
................................................................................
	    r = u;
	    break;
	} else if (beadPtr->level < *v) {
	    /*
	     * The current variable in the expression is unquantified.
	     * Quantify the two subexpressions and make the result
	     */
	    l = Quantify(sysPtr, G, H, q, v, n, beadPtr->low);
	    h = Quantify(sysPtr, G, H, q, v, n, beadPtr->high);
	    r = BDD_MakeBead(sysPtr, beadPtr->level, l, h);
	    BDD_UnrefBead(sysPtr,h);
	    BDD_UnrefBead(sysPtr,l);
	    break;
	} else if (beadPtr->level == *v) {
	    /*
	     * The current variable in the expression is quantified.
	     * Quantify the two subexpressions with respect to the
	     * remaining variables and then apply the combining operation.
	     */



	    l = Quantify(sysPtr, G, H, q, v+1, n-1, beadPtr->low);
	    h = Quantify(sysPtr, G, H, q, v+1, n-1, beadPtr->high);
	    r = Apply(sysPtr, G, q, l, h);
	    BDD_UnrefBead(sysPtr,h);
	    BDD_UnrefBead(sysPtr,l);
	    break;
	} else {
	    /* 
	     * The current variable does not appear free in the expression,
	     * The quantification is trivially satisfied with respect to the
................................................................................
BDD_Quantify(
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_Quantifier q,		/* Quantifier to apply */
    const BDD_VariableIndex* v,	/* List of variables to quantify */
    BDD_VariableIndex n,	/* Number of variables to quantify */
    BDD_BeadIndex e)		/* Expression to quantify */
{
    Tcl_HashTable G;	        /* Hash table to cache partial results
				 * of Apply */
    Tcl_HashTable H;		/* Hash table to cache partial results
				 * of Quantify */
    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(&G, TCL_CUSTOM_TYPE_KEYS, &Bead2KeyType);
    Tcl_InitHashTable(&H, TCL_ONE_WORD_KEYS);

    r = Quantify(sysPtr, &G, &H, q, v, n, e);

    for (entryPtr = Tcl_FirstHashEntry(&H, &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&H);
    for (entryPtr = Tcl_FirstHashEntry(&G, &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&G);

    return r;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Compose --
 *
 *	Computes a BDD representing an input BDD with a selection of variables
 *	replaced simultaneously with other expressions.
 *
 * Results:
 *	Returns the composed BDD.
 *
 * This procedure performs simultaneous composition. The result is
 * different from consecutive composition calls on the individual variables:
 *
 * compose(x1&x2&x3, (x1->x2,x2->x3,x3->x1)) == (x2&x3&x1)
 * compose(x1&x2&x3, x1->x2) == x2&x2&x3 == x2&x3
 * compose(x2&x3, x2->x3) == x3&x3 == x3
 * compose(x3, x3->x1) == x1
 *
 * If all the variables need to be replaced with constants, then Restrict
 * is much faster than Compose at generating the replaced BDD.
 *
 *-----------------------------------------------------------------------------
 */

static BDD_BeadIndex
Compose(
    BDD_System* sysPtr,		/* System of BDD's */
    Tcl_HashTable* G,		/* Hash table to cache partial results 
				 * of Apply3 */
    Tcl_HashTable* H,		/* Hash table to cache partial results
				 * of Compose */
    BDD_BeadIndex u,		/* Input BDD */
    BDD_VariableIndex n,	/* Number of variables in the vector */
    BDD_BeadIndex r[n])		/* Replacement terms for variables
				 * 0..n */
{
    BDD_BeadIndex result;	/* Return value */
    int newFlag;
    Tcl_HashEntry* entryPtr = Tcl_CreateHashEntry(H, (ClientData)u, &newFlag);
    Bead* uPtr = sysPtr->beads + u;
    BDD_VariableIndex level = uPtr->level;
    BDD_BeadIndex low = uPtr->low;
    BDD_BeadIndex high = uPtr->high;
    if (!newFlag) {
	result = (BDD_BeadIndex) (size_t) Tcl_GetHashValue(entryPtr);
	++sysPtr->beads[result].refCount;
	return result;
    } else if (sysPtr->beads[u].level >= n) {
	result = u;
	++sysPtr->beads[result].refCount;
    } else {
	low = Compose(sysPtr, G, H, low, n, r);
	high = Compose(sysPtr, G, H, high, n, r);
	result = Apply3(sysPtr, G, BDD_TERNOP_IFTHENELSE, r[level], low, high);
	BDD_UnrefBead(sysPtr, low);
	BDD_UnrefBead(sysPtr, high);
    }
    Tcl_SetHashValue(entryPtr, (ClientData) result);
    ++sysPtr->beads[result].refCount;
    return result;
}
BDD_BeadIndex
BDD_Compose(
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_BeadIndex u,		/* BDD to compose */
    BDD_VariableIndex n,	/* Number of leading variables specified */
    BDD_BeadIndex replacements[])
				/* Replacement values for first n variables */
{
    Tcl_HashTable G;		/* Partial results for Apply3 */
    Tcl_HashTable H;		/* Partial results for Compose */

    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(&G, TCL_CUSTOM_TYPE_KEYS, &Bead3KeyType);
    Tcl_InitHashTable(&H, TCL_ONE_WORD_KEYS);

    r = Compose(sysPtr, &G, &H, u, n, replacements);

    for (entryPtr = Tcl_FirstHashEntry(&H, &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {

	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&H);
    for (entryPtr = Tcl_FirstHashEntry(&G, &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&G);

    return r;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_SatCount --
 *

Changes to generic/bdd.h.

103
104
105
106
107
108
109
110
111
112
113
114
115



116
117
118
119
120
121
122
...
145
146
147
148
149
150
151




152
153
154
155
156
157
158
typedef unsigned int BDD_VariableIndex;
				/* Since the size of BDD's often is
				 * exponential in the number of variables,
				 * it's hard to imagine more than 
				 * an 'unsigned int' worth. */

/*
 * Value assignment: used in making conjunctions and restrictions,
 * and in reporting out satisfying expressions.
 */
typedef struct BDD_ValueAssignment {
    BDD_VariableIndex var;	/* Variable */
    int value;			/* Boolean value */



} BDD_ValueAssignment;

#define BDDAPI /* TODO: work out the export gubbins */

extern BDDAPI BDD_System* BDD_NewSystem(BDD_BeadIndex n);
extern BDDAPI void BDD_SetVariableCount(BDD_System* sysPtr,
					BDD_VariableIndex n);
................................................................................
					 const BDD_ValueAssignment r[],
					 BDD_VariableIndex n);
extern BDDAPI BDD_BeadIndex BDD_Quantify(BDD_System* sysPtr,
					 BDD_Quantifier q,
					 const BDD_VariableIndex v[],
					 BDD_VariableIndex n,
					 BDD_BeadIndex u);




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,
				 BDD_VariableIndex* nPtr);







|




|
>
>
>







 







>
>
>
>







103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
...
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
typedef unsigned int BDD_VariableIndex;
				/* Since the size of BDD's often is
				 * exponential in the number of variables,
				 * it's hard to imagine more than 
				 * an 'unsigned int' worth. */

/*
 * Value assignment: used in making conjunctions, compositions and restrictions,
 * and in reporting out satisfying expressions.
 */
typedef struct BDD_ValueAssignment {
    BDD_VariableIndex var;	/* Variable */
    BDD_BeadIndex value;	/* Boolean value. Must be constant for
				 * conjunctions and restrictions.
				 * Will be constant for satisfying assignments.
				 * May be an arbitrary bead for compositions. */
} BDD_ValueAssignment;

#define BDDAPI /* TODO: work out the export gubbins */

extern BDDAPI BDD_System* BDD_NewSystem(BDD_BeadIndex n);
extern BDDAPI void BDD_SetVariableCount(BDD_System* sysPtr,
					BDD_VariableIndex n);
................................................................................
					 const BDD_ValueAssignment r[],
					 BDD_VariableIndex n);
extern BDDAPI BDD_BeadIndex BDD_Quantify(BDD_System* sysPtr,
					 BDD_Quantifier q,
					 const BDD_VariableIndex v[],
					 BDD_VariableIndex n,
					 BDD_BeadIndex u);
extern BDDAPI BDD_BeadIndex BDD_Compose(BDD_System* sysPtr,
					BDD_BeadIndex u,
					BDD_VariableIndex nVars,
					BDD_BeadIndex replacements[]);
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,
				 BDD_VariableIndex* nPtr);