tclbdd

Check-in [bdc21889cb]
Login

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

Overview
Comment:Flesh out ApplyAndQuantify. Needs the outer layers.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:bdc21889cbeea34f6d25486e1fc0a65fe04abce3
User & Date: kbk 2013-12-10 13:19:13
Context
2013-12-10
13:32
Flesh out BDD_ApplyAndQuantify. Needs Tcl wrapper. check-in: 33b0644fb3 user: kbk tags: trunk
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
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

1740
1741
1742
1743
1744
1745
1746
1747
1748
1749
1750
1751
1752
1753
1754
1755
1756
1757
1758
1759
1760
1761
1762


1763
1764
1765
1766
1767
1768

1769



1770


1771

1772
1773
1774

1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
1811
1812
1813
1814
1815
1816
1817
1818
1819
1820
1821
1822
1823
1824
1825
1826
1827
1828
1829
1830
1831
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
1852
1853
1854
1855
1856
1857
1858
1859
1860
1861
1862
1863
1864
1865
1866
1867
1868
1869
1870
1871
1872
1873
1874
1875
1876
1877
1878
1879
1880
1881
1882
1883
1884
1885
1886
1887
1888
1889
1890
1891
1892
1893
1894
1895
1896
1897
1898
1899
1900
1901
1902
1903
1904
1905
1906
1907
1908
1909
....
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
 *
 * Combining the two operations into a single call saves one complete
 * traversal of the functions.
 *
 *-----------------------------------------------------------------------------
 */

#if 0 /* This needs work - and it's a performance hack that
       * might not be needed? */
static BDD_BeadIndex
ApplyAndQuantify(
    BDD_System* sysPtr,	 	/* System of BDD's */
    Tcl_HashTable* F,		/* Partial results of Quantify */
    Tcl_HashTable* G,	 	/* Partial results of Quantify */
    Tcl_HashTable* H,	 	/* Partial results of Apply */
    Tcl_HashTable* J,		/* Final partial results of ApplyAndQuantify */
    BDD_Quantifier q,	 	/* Quantifier to apply */
    BDD_VariableIndex n,	/* Number of variables to quantify */
    const BDD_VariableIndex* v,	/* Variables to quantify */
    BDD_BinOp op,		/* Operation to apply */
    BDD_BeadIndex u1,		/* Left operand */
    BDD_BeadIndex u2)		/* Right operand */
{


    BDD_BeadIndex u[2];	        /* Hash key */
    Tcl_HashEntry* entry;       /* Cached partial result */
    int newFlag;	        /* Flag whether cached result was found */
    BDD_BinOp opmask;		/* Mask for matching the operator */
    BDD_BeadIndex temp;
    BDD_BeadIndex result = ~(BDD_BeadIndex) 0;

    Bead* beadPtr1, * beadPtr2;	/* Left and right operands */



    BDD_VariableIndex level1, level2;


				/* Left and right variables */

    BDD_VariableIndex level;	/* Lowest variable of the two operands */
    BDD_BeadIndex l, h;		/* Left and right operands for recursive
				 * ApplyAndQuantify */


    /* Check if the result is already hashed */

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

    /* 
     * Check if the result of the operation 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;
	
	/*
	 * Also check for special cases where both operands are
	 * identical.
	 */
    } else if ((op == BDD_BINOP_AND || op == BDD_BINOP_OR) && (u1 == u2)) {
	result = u2;
	++sysPtr->beads[result].refCount;
    } else if ((op == BDD_BINOP_XOR
		|| op == BDD_BINOP_LT
		|| op == BDD_BINOP_GT) && (u1 == u2)) {
	result = 0;
	++sysPtr->beads[result].refCount;
    } else if ((op == BDD_BINOP_EQ
		|| op == BDD_BINOP_LE
		|| op == BDD_BINOP_GE) && (u1 == u2)) {
	result = 1;
	++sysPtr->beads[result].refCount;
    }

    /*
     * If we've eliminated either operand, finish by doing the quantification
     * on the other operand. If we've reduced the expression to a constant,
     * just cache and return the result.
     */

    if (result != ~(BDD_BeadIndex) 0) {
	if (result > 1) {
	    temp = result;
	    result = Quantify(sysPtr, F, G, q, n, v, temp);
	    BDD_UnrefBead(sysPtr,temp);
	}
    } else {

	beadPtr1 = sysPtr->beads + u1;
	beadPtr2 = sysPtr->beads + u2;
	level1 = beadPtr1->level;
	level2 = beadPtr2->level;
	if (n == 0 || (level1 > v[n-1] && level2 > v[n-1])) {
	    /*
	     * We've run out of variables to quantify
	     */
	    result = Apply(sysPtr, u1, u2);
	} else if (level1 < level2) {
	    level = level1;
	    l = ApplyAndQuantify(sysPtr, F, G, J, q, n, v, op,
				 beadPtr1->low, u2);
	    h = ApplyAndQuantify(sysPtr, F, G, J, q, n, v, op,
				 beadPtr1->high, u2);
	} else if (level1 == level2) {
	    level = level1;
	    l = ApplyAndQuantify(sysPtr, F, G, H, J, q, n, v, op,
				 beadPtr1->low, beadPtr2->high);
	    h = ApplyAndQuantify(sysPtr, F, G, H, J, q, n, v, op,
				 beadPtr1->high, beadPtr2->high);
	} else /* level1 > level2 */ {
	    level = level2;
	    l = ApplyAndQuantify(sysPtr, F, G, H, J, q, n, v, op,
				 u1, beadPtr2->high);
	    h = ApplyAndQuantify(sysPtr, F, G, H, J, q, n, v, op,
				 u1, beadPtr2->high);
	}
	if (level < v[0]) {
	    
	    /* FIXME FINISH THIS */
	}

    }

    /* Cache the result */
    Tcl_SetHashValue(entry, (ClientData) result);
    ++sysPtr->beads[result].refCount;

    return result;
}
#endif
		 
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Compose --
 *
 *	Computes a BDD representing an input BDD with a selection of variables
................................................................................
 *
 * 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.
 *
 *-----------------------------------------------------------------------------
 */








<
<



<
<
<
<
<


<



>
>



<


>
|
>
>
>
|
>
>
|
>
|


>





|








|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<





<
<







 







|







1740
1741
1742
1743
1744
1745
1746


1747
1748
1749





1750
1751

1752
1753
1754
1755
1756
1757
1758
1759

1760
1761
1762
1763
1764
1765
1766
1767
1768
1769
1770
1771
1772
1773
1774
1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
1811
1812
1813
1814
1815
1816
1817
1818
1819
1820
1821
1822
1823
1824
1825
1826
1827
1828
1829
1830
1831
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
1852
1853
1854
1855
1856
1857
1858
1859
1860
1861
1862
1863
1864
1865
1866
1867
1868




























1869
1870
1871
1872
1873


1874
1875
1876
1877
1878
1879
1880
....
1885
1886
1887
1888
1889
1890
1891
1892
1893
1894
1895
1896
1897
1898
1899
 *
 * Combining the two operations into a single call saves one complete
 * traversal of the functions.
 *
 *-----------------------------------------------------------------------------
 */



static BDD_BeadIndex
ApplyAndQuantify(
    BDD_System* sysPtr,	 	/* System of BDD's */





    BDD_VariableIndex n,	/* Number of variables to quantify */
    const BDD_VariableIndex* v,	/* Variables to quantify */

    BDD_BeadIndex u1,		/* Left operand */
    BDD_BeadIndex u2)		/* Right operand */
{
    BDD_BinOp op = sysPtr->appquantOp;
				/* Operation to apply */
    BDD_BeadIndex u[2];	        /* Hash key */
    Tcl_HashEntry* entry;       /* Cached partial result */
    int newFlag;	        /* Flag whether cached result was found */

    BDD_BeadIndex temp;
    BDD_BeadIndex result = ~(BDD_BeadIndex) 0;
    
    Bead* beadPtr1 = sysPtr->beads + u1;
				/* Left operand */
    Bead* beadPtr2 = sysPtr->beads + u2;
				/* Right operand */
    BDD_VariableIndex level1 = beadPtr1->level;
				/* Left variable */
    BDD_VariableIndex level2 = beadPtr2->level;
				/* Right variable */
    BDD_VariableIndex level = (level1 < level2) ? level1 : level2;	
				/* Lowest variable of the two operands */
    BDD_BeadIndex l, h;		/* Left and right operands for recursive
				 * ApplyAndQuantify */
    BDD_BeadIndex low1, low2, high1, high2;

    /* Check if the result is already hashed */

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

    /* 
     * Check if the result of the operation is constant or a copy
     * of one of the operands. If it is, we're done with application
     * and can switch to a simple Quantify.
     */
    if (ApplyEasyCases(op, u1, u2, &temp)) {
	++sysPtr->beads[temp].refCount;
	if (temp <= 1) {
	    result = temp;
	} else {
	    result = Quantify(sysPtr, n, v, temp);
	    --sysPtr->beads[temp].refCount;
	}
    } else {

	for (;;) {

	    if (n == 0 || (level1 > v[n-1] && level2 > v[n-1])) {
		/*
		 * We've run out of variables to quantify. Switch to a simple 
		 * Apply operation.
		 * FIXME This is wrong for UNIQUE quantification
		 */
		sysPtr->applyOp = sysPtr->appquantOp;
		result = Apply(sysPtr, u1, u2);
		break;
	    } 

	    if (level1 == level) {
		low1 = beadPtr1->low;
		high1 = beadPtr1->high;
	    } else {
		low1 = u1;
		high1 = u1;
	    }
	    if (level2 == level) {
		low2 = beadPtr2->low;
		high2 = beadPtr2->high;
	    } else {
		low2 = u2;
		high2 = u2;
	    }

	    if (level < *v) {
		/*
		 * The current variable in the expression is unquantified.
		 */
		l = ApplyAndQuantify(sysPtr, n, v, low1, low2);
		h = ApplyAndQuantify(sysPtr, n, v, high1, high2);
		result = BDD_MakeBead(sysPtr, level, l, h);
		BDD_UnrefBead(sysPtr, l);
		BDD_UnrefBead(sysPtr, h);
		
	    } else if (level == *v) {
		/*
		 * The current variable in the expression is quantified.
		 */
		l = ApplyAndQuantify(sysPtr, n-1, v+1, low1, low2);
		h = ApplyAndQuantify(sysPtr, n-1, v+1, high1, high2);
		sysPtr->applyOp = sysPtr->quantifier;
		result = Apply(sysPtr, l, h);
		BDD_UnrefBead(sysPtr, l);
		BDD_UnrefBead(sysPtr, h);
		
	    } else {
		/*
		 * The current variable in the quantifier is unused.
		 * Advance to the next one
		 * FIXME This is wrong for a UNIQUE quantifier
		 */
		++v;
		--n;
	    }
	}
    }
    /*
     * Cache and return the result
     * It is possible for an outer quantification to destroy the
     * result altogether, so make sure that the refcount tracks the
     * cache entry.
     */




























    Tcl_SetHashValue(entry, (ClientData) result);
    ++sysPtr->beads[result].refCount;

    return result;
}


 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Compose --
 *
 *	Computes a BDD representing an input BDD with a selection of variables
................................................................................
 *
 * 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
x * 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.
 *
 *-----------------------------------------------------------------------------
 */

Changes to generic/bddInt.h.

37
38
39
40
41
42
43




44
45
46
47
48
49
50
    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 */

    Tcl_HashTable applyCache;	/* Cache of partial results for BDD_Apply */
    BDD_BinOp applyOp;		/* Operator for BDD_Apply */




    Tcl_HashTable apply3Cache;	/* Cache of partial results for BDD_Apply3 */
    BDD_TernOp apply3Op;	/* Operator for BDD_Apply3 */
    Tcl_HashTable composeCache;	/* Cache of partial results for BDD_Compose */
    BDD_VariableIndex composeCount;
				/* Number of variables being substituted
				 * in BDD_Compose */
    BDD_BeadIndex* composeReplacements;







>
>
>
>







37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
    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 */

    Tcl_HashTable applyCache;	/* Cache of partial results for BDD_Apply */
    BDD_BinOp applyOp;		/* Operator for BDD_Apply */
    Tcl_HashTable appquantCache;
				/* Cache of partial results for
				 * BDD_ApplyAndQuantify */
    BDD_BinOp appquantOp;	/* Operator for BDD_ApplyAndQuantify */
    Tcl_HashTable apply3Cache;	/* Cache of partial results for BDD_Apply3 */
    BDD_TernOp apply3Op;	/* Operator for BDD_Apply3 */
    Tcl_HashTable composeCache;	/* Cache of partial results for BDD_Compose */
    BDD_VariableIndex composeCount;
				/* Number of variables being substituted
				 * in BDD_Compose */
    BDD_BeadIndex* composeReplacements;