tclbdd

Check-in [33b0644fb3]
Login

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

Overview
Comment:Flesh out BDD_ApplyAndQuantify. Needs Tcl wrapper.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:33b0644fb384cc488aec1df432cdd245d44e085f
User & Date: kbk 2013-12-10 13:32:35
Context
2013-12-11
02:34
Added GarbageCollect for memory debugging Modified all tests to gc at the end and report # of nodes in use for leak checking. Added Tcl binding for ApplyAndQuantify Modified unset to take an arbitrary number of names. check-in: 7771be216c user: kbk tags: trunk
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
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
....
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
....
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
    Tcl_DeleteHashTable(&(sysPtr->quantifyCache));
    for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->applyCache), &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&(sysPtr->applyCache));

    return r;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_ApplyAndQuantify --
................................................................................
	    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;
	    }
................................................................................
		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







<







 







>
>
>

<
<
>










>
>
>







 







>
>










>
>











|







>


<
<
<






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







1713
1714
1715
1716
1717
1718
1719

1720
1721
1722
1723
1724
1725
1726
....
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
....
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
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
    Tcl_DeleteHashTable(&(sysPtr->quantifyCache));
    for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->applyCache), &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&(sysPtr->applyCache));

    return r;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_ApplyAndQuantify --
................................................................................
	    result = temp;
	} else {
	    result = Quantify(sysPtr, n, v, temp);
	    --sysPtr->beads[temp].refCount;
	}
    } else {

	/*
	 * Not an easy case. Iterate over the quantified variables
	 */
	for (;;) {


	    if (n == 0) {
		/*
		 * 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;
	    } 

	    /*
	     * Split both expressions at the current variable
	     */
	    if (level1 == level) {
		low1 = beadPtr1->low;
		high1 = beadPtr1->high;
	    } else {
		low1 = u1;
		high1 = u1;
	    }
................................................................................
		low2 = u2;
		high2 = u2;
	    }

	    if (level < *v) {
		/*
		 * The current variable in the expression is unquantified.
		 * Recurse into the subexpressions, and recombine with
		 * a simple IF-THEN_ELSE
		 */
		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.
		 * Recurse into the subexpressions at the next variable,
		 * and combine by applying the quantifier.
		 */
		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



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

    return result;
}
BDD_BeadIndex
BDD_ApplyAndQuantify(
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_Quantifier q,		/* Quantifier (EXISTS or FORALL */
    BDD_VariableIndex n,	/* Number of quantified variables */
    const BDD_VariableIndex v[],
				/* Quantified variables */
    BDD_BinOp op,		/* Operator to apply */
    BDD_BeadIndex u1,		/* Left subexpression */
    BDD_BeadIndex u2)		/* Right subexpression */
{
    BDD_BeadIndex result;	/* Result of the combined operation */
    Tcl_HashSearch search;	/* Search for clearing caches */
    Tcl_HashEntry* entryPtr;	/* Hash entry in cache being cleared */
    Tcl_InitCustomHashTable(&(sysPtr->applyCache), 
			    TCL_CUSTOM_TYPE_KEYS, &Bead3KeyType);
    Tcl_InitCustomHashTable(&(sysPtr->appquantCache),
			    TCL_CUSTOM_TYPE_KEYS, &Bead2KeyType);
    Tcl_InitHashTable(&(sysPtr->quantifyCache), TCL_ONE_WORD_KEYS);
    sysPtr->quantifier = q;
    sysPtr->appquantOp = op;

    result = ApplyAndQuantify(sysPtr, n, v, u1, u2);
    
    for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->quantifyCache), &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&(sysPtr->quantifyCache));
    for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->applyCache), &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&(sysPtr->applyCache));
    for (entryPtr = Tcl_FirstHashEntry(&(sysPtr->appquantCache), &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&(sysPtr->appquantCache));
    return result;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Compose --
 *
 *	Computes a BDD representing an input BDD with a selection of variables

Changes to generic/bdd.h.

152
153
154
155
156
157
158







159
160
161
162
163
164
165
					 BDD_VariableIndex n,
					 const BDD_VariableIndex v[],
					 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);







>
>
>
>
>
>
>







152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
					 BDD_VariableIndex n,
					 const BDD_VariableIndex v[],
					 BDD_BeadIndex u);
extern BDDAPI BDD_BeadIndex BDD_Compose(BDD_System* sysPtr,
					BDD_BeadIndex u,
					BDD_VariableIndex nVars,
					BDD_BeadIndex replacements[]);
extern BDDAPI BDD_BeadIndex BDD_ApplyAndQuantify(BDD_System* sysPtr, 
						 BDD_Quantifier q,
						 BDD_VariableIndex n,
						 const BDD_VariableIndex v[],
						 BDD_BinOp op,
						 BDD_BeadIndex u1, 
						 BDD_BeadIndex u2);
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);