tclbdd

Check-in [e48d5c4b6a]
Login

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

Overview
Comment:support; beadcount; simplify; tests for simplify and unset
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:e48d5c4b6a52e18337339caf6fabda0cca6c0094
User & Date: kbk 2013-12-12 00:44:41
Context
2013-12-13
04:57
Fix beadcount - didn't work at all. Added loading of FDDD rows. check-in: 62023edbb8 user: kbk tags: trunk
2013-12-12
00:44
support; beadcount; simplify; tests for simplify and unset check-in: e48d5c4b6a user: kbk tags: trunk
2013-12-11
13:27
add profiler check-in: bcd84fa263 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

1981
1982
1983
1984
1985
1986
1987




































































































































































1988
1989
1990
1991
1992
1993
1994
    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 --







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







1981
1982
1983
1984
1985
1986
1987
1988
1989
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
2024
2025
2026
2027
2028
2029
2030
2031
2032
2033
2034
2035
2036
2037
2038
2039
2040
2041
2042
2043
2044
2045
2046
2047
2048
2049
2050
2051
2052
2053
2054
2055
2056
2057
2058
2059
2060
2061
2062
2063
2064
2065
2066
2067
2068
2069
2070
2071
2072
2073
2074
2075
2076
2077
2078
2079
2080
2081
2082
2083
2084
2085
2086
2087
2088
2089
2090
2091
2092
2093
2094
2095
2096
2097
2098
2099
2100
2101
2102
2103
2104
2105
2106
2107
2108
2109
2110
2111
2112
2113
2114
2115
2116
2117
2118
2119
2120
2121
2122
2123
2124
2125
2126
2127
2128
2129
2130
2131
2132
2133
2134
2135
2136
2137
2138
2139
2140
2141
2142
2143
2144
2145
2146
2147
2148
2149
2150
2151
2152
2153
2154
2155
2156
2157
2158
    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_Simplify --
 *
 *	Simplify a BDD with respect to a domain.
 *
 * Results:
 *	Returns the simplified BDD.
 *
 * This function is the 'Restrict' function of Coudert and Madre.
 * It works by pruning paths of the BDD outside the given domain.
 * It is guaranteed never to increase the size of the BDD.
 *
 *-----------------------------------------------------------------------------
 */

static BDD_BeadIndex
Simplify(
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_BeadIndex f,		/* BDD to simplify */
    BDD_BeadIndex domain)	/* Domain outside which values are
				 * irrelevant. */
{
    BDD_BeadIndex u[2];		/* Hash key */
    Tcl_HashEntry* entry;	/* Hash entry in the cache
				 * of partial results */
    int isNew;			/* Flag == 1 if the entry was created */
    BDD_BeadIndex result = ~(BDD_BeadIndex) 0;
				/* Simplified BDD */
    Bead* fPtr = sysPtr->beads + f;
    Bead* dPtr = sysPtr->beads + domain;
    BDD_VariableIndex fLevel = fPtr->level;
    BDD_VariableIndex dLevel = dPtr->level;
    BDD_BeadIndex low, high, temp;

    /*
     * Handle the trivial cases without resorting to the cache
     */
    if (domain == 1 || f <= 1) {
	++sysPtr->beads[f].refCount;
	return f;
    }
    if (domain == f) {
	++sysPtr->beads[1].refCount;
	return 1;
    }
    if (domain == 0) {
	++sysPtr->beads[0].refCount;
	return 0;
    }

    /*
     * Search the cache
     */
    u[0] = f;
    u[1] = domain;
    entry = Tcl_CreateHashEntry(&(sysPtr->simplifyCache), u, &isNew);
    if (!isNew) {
	result = (BDD_BeadIndex)Tcl_GetHashValue(entry);
	++sysPtr->beads[result].refCount;
	return result;
    }

    /*
     * Simplify when a common variable appears in domain and function
     */
    if (fLevel == dLevel) {
	/*
	 * Trim zero branches in the domain
	 */
	if (dPtr->low == 0) {
	    /* 
	     * The common variable has all zeroes in the low branch.
	     * Cast out the low branch and simplify the high.
	     */
	    result = Simplify(sysPtr, fPtr->high, dPtr->high);
	} else if (dPtr->high == 0) {
	    /*
	     * The common variable has all zeroes in the high branch.
	     * Cast out the high branch and simplify the low.
	     */
	    result = Simplify(sysPtr, fPtr->low, dPtr->low);
	} else {
	    /*
	     * The common variable has live branches in both
	     * directions. Simplify the high and low branches
	     * separately and conjoin them.
	     */
	    low = Simplify(sysPtr, fPtr->low, dPtr->low);
	    high = Simplify(sysPtr, fPtr->high, dPtr->high);
	    result = BDD_MakeBead(sysPtr, fLevel, low, high);
	    BDD_UnrefBead(sysPtr, low);
	    BDD_UnrefBead(sysPtr, high);
	}
    } else if (fLevel < dLevel) {
	/*
	 * The first variable in f is not constrained by the domain.
	 * Simplify its low and high branches, and make a bead testing
	 * the variable of f.
	 */
	low = Simplify(sysPtr, fPtr->low, domain);
	high = Simplify(sysPtr, fPtr->high, domain);
	result = BDD_MakeBead(sysPtr, fLevel, low, high);
	BDD_UnrefBead(sysPtr, low);
	BDD_UnrefBead(sysPtr, high);
    } else /* fLevel > dLevel */ {
	/* 
	 * The first variable in domain does not appear in
	 * f. Existentially quantify it away from domain, and simplify
	 * with respect to the broader domain
	 */
	/* sysPtr->applyOp = BDD_BINOP_OR; */
	temp = Apply(sysPtr, dPtr->low, dPtr->high);
	result = Simplify(sysPtr, f, temp);
	BDD_UnrefBead(sysPtr, temp);
    }
    ++sysPtr->beads[result].refCount;
    Tcl_SetHashValue(entry, (ClientData) result);
    return result;
}
BDD_BeadIndex
BDD_Simplify(
    BDD_System* sysPtr,		/* System of BDD's */
    BDD_BeadIndex f,		/* Function to simplify */
    BDD_BeadIndex domain)	/* Domain of interest */
{
    Tcl_HashSearch search;	/* Search for clearing the cache */
    Tcl_HashEntry* entryPtr;	/* Hash entyr for clearing the cache */
    BDD_BeadIndex result;	/* Return value */

    /*
     * Initialize caches of partial results
     */
    Tcl_InitCustomHashTable(&(sysPtr->applyCache),
			    TCL_CUSTOM_TYPE_KEYS, &Bead3KeyType);
    sysPtr->applyOp = BDD_BINOP_OR;
    Tcl_InitCustomHashTable(&(sysPtr->simplifyCache),
			    TCL_CUSTOM_TYPE_KEYS, &Bead2KeyType);

    /*
     * Compute the result
     */
    result = Simplify(sysPtr, f, domain);

    /*
     * Clear the caches
     */
    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->simplifyCache), &search);
	 entryPtr != NULL;
	 entryPtr = Tcl_NextHashEntry(&search)) {
	BDD_UnrefBead(sysPtr, (BDD_BeadIndex)Tcl_GetHashValue(entryPtr));
    }
    Tcl_DeleteHashTable(&(sysPtr->simplifyCache));

    return result;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Compose --

Changes to generic/bdd.h.

149
150
151
152
153
154
155


156
157
158
159
160
161
162
					 const BDD_ValueAssignment r[],
					 BDD_VariableIndex n);
extern BDDAPI BDD_BeadIndex BDD_Quantify(BDD_System* sysPtr,
					 BDD_Quantifier q,
					 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,







>
>







149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
					 const BDD_ValueAssignment r[],
					 BDD_VariableIndex n);
extern BDDAPI BDD_BeadIndex BDD_Quantify(BDD_System* sysPtr,
					 BDD_Quantifier q,
					 BDD_VariableIndex n,
					 const BDD_VariableIndex v[],
					 BDD_BeadIndex u);
extern BDDAPI BDD_BeadIndex BDD_Simplify(BDD_System* sysPtr, BDD_BeadIndex f,
					 BDD_BeadIndex domain);
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,

Changes to generic/bddInt.h.

68
69
70
71
72
73
74


75
76
77
78
79
80
81
    BDD_Quantifier quantifier;	/* Quantifier for BDD_Quantify */
    Tcl_HashTable quantifyCache;
				/* Cache of partial results for BDD_Quantify */
    Tcl_HashTable restrictCache; 
				/* Cache of partial results for BDD_Restrict */
    Tcl_HashTable satCountCache;
				/* Cache of partial results for BDD_SatCount */


};

/*
 * State of an AllSat computation
 */
typedef enum BDD_AllSatSEnum {
    BDD_ALLSAT_START,		/* Initial entry */







>
>







68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
    BDD_Quantifier quantifier;	/* Quantifier for BDD_Quantify */
    Tcl_HashTable quantifyCache;
				/* Cache of partial results for BDD_Quantify */
    Tcl_HashTable restrictCache; 
				/* Cache of partial results for BDD_Restrict */
    Tcl_HashTable satCountCache;
				/* Cache of partial results for BDD_SatCount */
    Tcl_HashTable simplifyCache;
				/* Cache of partial results for BDD_Simplify */
};

/*
 * State of an AllSat computation
 */
typedef enum BDD_AllSatSEnum {
    BDD_ALLSAT_START,		/* Initial entry */

Changes to generic/tclBdd.c.

147
148
149
150
151
152
153


154
155
156
157
158
159
160
...
285
286
287
288
289
290
291







292
293
294
295
296
297
298
...
343
344
345
346
347
348
349

350
351
352
353
354
355
356
....
1792
1793
1794
1795
1796
1797
1798

































































1799
1800
1801
1802
1803
1804
1805
				  int, Tcl_Obj* const[]);
static int BddSystemQuantifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemRestrictMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemSatcountMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);


static int BddSystemTernopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				 int, Tcl_Obj* const[]);
static int BddSystemUnsetMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int CloneBddSystemObject(Tcl_Interp*, ClientData, ClientData*);
static int CloneMethod(Tcl_Interp*, ClientData, ClientData*);
static void DeleteBddSystemData(BddSystemData*);
................................................................................
const static Tcl_MethodType BddSystemSatcountMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "satcount",			   /* name */
    BddSystemSatcountMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};







const static Tcl_MethodType BddSystemTernopMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "ternop",			   /* name */
    BddSystemTernopMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};				   /* common to all ternary operators */
................................................................................
    { "nor3",      &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
    { "oneof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_ONEOF },
    { "profile",   &BddSystemProfileMethodType,   NULL },
    { "restrict",  &BddSystemRestrictMethodType,  NULL },
    { "satcount",  &BddSystemSatcountMethodType,  NULL },

    { "twoof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_TWOOF },
    { "unset",     &BddSystemUnsetMethodType,     NULL },
    { "|",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_OR },
    { "|3",        &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_OR },
    { "~",         &BddSystemNegateMethodType,    NULL },
    { NULL,	   NULL,                          NULL }
};
................................................................................
    }
    mp_init(&satCount);
    BDD_SatCount(sdata->system, beadIndex, &satCount);
    Tcl_SetObjResult(interp, Tcl_NewBignumObj(&satCount));

    return TCL_OK;
}

































































 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemTernopMethod --
 *
 *	Computes a ternary operation among three expressions in a BDD system







>
>







 







>
>
>
>
>
>
>







 







>







 







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







147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
...
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
...
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
....
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
				  int, Tcl_Obj* const[]);
static int BddSystemQuantifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemRestrictMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemSatcountMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemSimplifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemTernopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				 int, Tcl_Obj* const[]);
static int BddSystemUnsetMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int CloneBddSystemObject(Tcl_Interp*, ClientData, ClientData*);
static int CloneMethod(Tcl_Interp*, ClientData, ClientData*);
static void DeleteBddSystemData(BddSystemData*);
................................................................................
const static Tcl_MethodType BddSystemSatcountMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "satcount",			   /* name */
    BddSystemSatcountMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemSimplifyMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "binop",			   /* name */
    BddSystemSimplifyMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};				   /* common to all ten binary operators */
const static Tcl_MethodType BddSystemTernopMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "ternop",			   /* name */
    BddSystemTernopMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};				   /* common to all ternary operators */
................................................................................
    { "nor3",      &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
    { "oneof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_ONEOF },
    { "profile",   &BddSystemProfileMethodType,   NULL },
    { "restrict",  &BddSystemRestrictMethodType,  NULL },
    { "satcount",  &BddSystemSatcountMethodType,  NULL },
    { "simplify",  &BddSystemSimplifyMethodType,  NULL },
    { "twoof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_TWOOF },
    { "unset",     &BddSystemUnsetMethodType,     NULL },
    { "|",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_OR },
    { "|3",        &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_OR },
    { "~",         &BddSystemNegateMethodType,    NULL },
    { NULL,	   NULL,                          NULL }
};
................................................................................
    }
    mp_init(&satCount);
    BDD_SatCount(sdata->system, beadIndex, &satCount);
    Tcl_SetObjResult(interp, Tcl_NewBignumObj(&satCount));

    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemSimplifyMethod --
 *
 *	Simplifies a BDD with a respect to a domain. (Coudert and Madre's
 *	Restrict function).
 *
 * Usage:
 *	$system simplify a f domain
 *
 * Parameters:
 *	OP - One of the binary operators nor, <, >, !=, ^, nand, &,
 *           ==, <=, >=, |
 *	a - Name of the result expression
 *	f - Name of the expression to simplify
 *	domain - Name of the expression describing the domain of interest
 *
 * Results:
 *	None
 *
 * Side effects:
 *	Assigns the given name to the result expression
 *
 *-----------------------------------------------------------------------------
 */

static int
BddSystemSimplifyMethod(
    ClientData clientData,	/* Operation to perform */
    Tcl_Interp* interp,		/* Tcl interpreter */
    Tcl_ObjectContext ctx,	/* Object context */
    int objc,			/* Parameter count */
    Tcl_Obj *const objv[])	/* Parameter vector */
{
    Tcl_Object thisObject = Tcl_ObjectContextObject(ctx);
				/* The current object */
    BddSystemData* sdata = (BddSystemData*)
	Tcl_ObjectGetMetadata(thisObject, &BddSystemDataType);
				/* The current system of expressions */
    int skipped = Tcl_ObjectContextSkippedArgs(ctx);
				/* The number of args used in method dispatch */
    BDD_BeadIndex beadIndexOpd1; /* The bead index of the first operand */
    BDD_BeadIndex beadIndexOpd2; /* The bead index of the second operand */
    BDD_BeadIndex beadIndexResult; /* The bead index of the result */

    /* Check syntax */

    if (objc != skipped+3) {
	Tcl_WrongNumArgs(interp, skipped, objv, "result function domain");
	return TCL_ERROR;
    }
    if (FindNamedExpression(interp, sdata, objv[skipped+1],
			    &beadIndexOpd1) != TCL_OK
	|| FindNamedExpression(interp, sdata, objv[skipped+2],
			       &beadIndexOpd2) != TCL_OK) {
	return TCL_ERROR;
    }
    beadIndexResult = BDD_Simplify(sdata->system, beadIndexOpd1,
				   beadIndexOpd2);
    SetNamedExpression(sdata, objv[skipped], beadIndexResult);
    BDD_UnrefBead(sdata->system, beadIndexResult);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemTernopMethod --
 *
 *	Computes a ternary operation among three expressions in a BDD system

Changes to library/tclbdd.tcl.

23
24
25
26
27
28
29






30






31
32
33
34
35
36
37
..
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
    export ===
    method satisfiable {exprName} {
	expr {[my beadindex $exprName] != 0}
    }
    method tautology {exprName} {
	expr {[my beadindex $exprname] == 1}
    }













}

proc bdd::Lexer {script} {
    set lexvals {\n ; ; ; ( ( ) ) = = ? ? : : nor NOR < < <= <=
	== == != != ^ ^ > > >= >= -> <= <- >= <-> == & & | | ~ ~ - - ! ~
	0 constant 1 constant}
    set line 0
................................................................................
	   | \s
	   | ;
	   | \(
	   | \)
	   | =
	   | \?
	   | :
	   | nor
	   | <
	   | <=
	   | ==
	   | !=
	   | >
	   | >=
	   | ->







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







 







<







23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
..
58
59
60
61
62
63
64

65
66
67
68
69
70
71
    export ===
    method satisfiable {exprName} {
	expr {[my beadindex $exprName] != 0}
    }
    method tautology {exprName} {
	expr {[my beadindex $exprname] == 1}
    }
    method support {exprName} {
	set i 0
	set result {}
	foreach k [my profile $exprName] {
	    if {$k != 0} {
		lappend result $i
	    }
	    incr i
	}
    }
    method beadcount {exprName} {
	tcl::mathop::+ [my profile $exprName]
    }
}

proc bdd::Lexer {script} {
    set lexvals {\n ; ; ; ( ( ) ) = = ? ? : : nor NOR < < <= <=
	== == != != ^ ^ > > >= >= -> <= <- >= <-> == & & | | ~ ~ - - ! ~
	0 constant 1 constant}
    set line 0
................................................................................
	   | \s
	   | ;
	   | \(
	   | \)
	   | =
	   | \?
	   | :

	   | <
	   | <=
	   | ==
	   | !=
	   | >
	   | >=
	   | ->

Added library/tclfdd.tcl.





























































































































































































































>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
#package require tclbdd 0.1

namespace eval fdd {
    namespace export domain interleave concatenate
}

proc fdd::domain {name width {endian littleendian}} {
    switch -exact -- $endian {
	littleendian {
	    set l {}
	    for {set i 0} {$i < $width} {incr i} {
		lappend l $name $i
	    }
	}
	bigendian {
	    set l {}
	    for {set i [expr {$width-1}]} {$i >= 0} {incr i -1} {
		lappend l $name $i
	    }
	}
	default {
	    return -code error -errorcode [list FDD BadEndian $endian] \
		"unknown endian \"$endian\": must be bigendian or littleendian"
	}
    }
    return [list [dict create $name $width] $l]
}

proc fdd::interleave {args} {
    set N 0
    set names {}
    set bits {}
    foreach domain $args {
	dict for {name width} [lindex $domain 0] {
	    if {[dict exists $names $name]} {
		return -code error -errorcode [list FDD DuplicateName $name] \
		    "domain named \"$name\" appears in multiple places"
	    }
	    incr N $width
	    dict set names $name $width
	    lappend bits [lindex $domain 1]
	}
    }
    set processed 0
    set scrambled {}
    while {$processed < $N} {
	set i 0
	foreach b $bits {
	    if {[llength $b] > 0} {
		lset bits $i [lassign $b name pos]
		lappend scrambled $name $pos
		incr processed
	    }
	    incr i
	}
    }
    return [list $names $scrambled]
}

proc fdd::concatenate {args} {
    set N 0
    set names {}
    set bits {}
    foreach domain $args {
	dict for {name width} [lindex $domain 0] {
	    if {[dict exists $names $name]} {
		return -code error -errorcode [list FDD DuplicateName $name] \
		    "domain named \"$name\" appears in multiple places"
	    }
	    incr N $width
	    dict set names $name $width
	}
	lappend bits [lindex $domain 1]
	puts "appended to bits: [lindex $domain 1] result=$bits"
    }
    puts "fdd::concatenate: bits: $bits"
    set scrambled {}
    foreach b $bits {
	lappend scrambled {*}$b
    }
    return [list $names $scrambled]
}

proc fdd::reader {sysName termName layout args} {
    set i 0
    foreach name $args {
	dict set cmdpos $name $i
	puts "$name appears at position $i"
	incr i
    }
    set result {}
    set p 0
    foreach {name bit} [lindex $layout 1] {
	if {[dict exists $cmdpos $name]} {
	    lappend result $p [dict get $cmdpos $name] $bit
	} else {
	    puts "$name does not appear"
	}
	incr p
    }
    set cmd [list $sysName load $termName $result]
    foreach name $args {
	append cmd " \$" $name
    }
    return $cmd
}



    

Changes to tests/bdd.test.

223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239











240
241
242
243
244
245
246
....
2681
2682
2683
2684
2685
2686
2687












































































































































2688
2689
2690
2691
2692
2693
2694
2695
....
2799
2800
2801
2802
2803
2804
2805
2806
2807
2808
2809
2810
2811
2812
2813
	list [sys dump !b] [sys dump !a] \
	    [sys unset !b] [sys unset !a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {{3 {1 1 0} 1 {2 1 1} 0 {2 0 0}} {2 {0 1 0} 1 {2 1 1} 0 {2 0 0}} {} {} 2}
}

test bdd-7.5 {nthvar - redundant var (tests duplicate BDD_MakeBead)} {
    -setup {bdd::system create sys}
    -body {
	sys notnthvar !a 0; sys notnthvar !b 1; sys notnthvar !c 0
	list [sys beadindex !a] [sys beadindex !b] [sys beadindex !c] \
	    [sys unset !a] [sys unset !b] [sys unset !c] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {2 3 2 {} {} {} 2}
}












test bdd-8.1 {negate - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys ~}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	    [sys unset result a1 a2 a4 a8 b1 b2 b4 b8 z1 z2 z4 z8] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {{1 2 3 2 3 4 2 3 4 2 2 2} {} 2}
}













































































































































test bdd-21.1 {eight queens} {*}{
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 64} {incr i} {
	    sys nthvar v$i $i; sys notnthvar !v$i $i
	}
    }
    -body {
................................................................................
	lreverse $sols

    }
    -cleanup {rename sys {}}
    -result {2 04752613 05726314 06357142 06471352 13572064 14602753 14630752 15063724 15720364 16257403 16470352 17502463 20647135 24170635 24175360 24603175 24730615 25147063 25160374 25164073 25307461 25317460 25703641 25704613 25713064 26174035 26175304 27360514 30471625 30475261 31475026 31625704 31625740 31640752 31746025 31750246 35041726 35716024 35720641 36074152 36271405 36415027 36420571 37025164 37046152 37420615 40357162 40731625 40752613 41357206 41362750 41506372 41703625 42057136 42061753 42736051 46027531 46031752 46137025 46152037 46152073 46302751 47302516 47306152 50417263 51602473 51603742 52064713 52073164 52074136 52460317 52470316 52613704 52617403 52630714 53047162 53174602 53602417 53607142 57130642 60275314 61307425 61520374 62057413 62714053 63147025 63175024 64205713 71306425 71420635 72051463 73025164}
}

test bdd-21.2 {verification of a full adder} {
    -setup {
	bdd::system create sys
	sys nthvar x 0; sys notnthvar !x 0
	sys nthvar y 1; sys notnthvar !y 1
	sys nthvar ci 2; sys notnthvar !ci 2
    }
    -body {







|









>
>
>
>
>
>
>
>
>
>
>







 







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







 







|







223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
....
2692
2693
2694
2695
2696
2697
2698
2699
2700
2701
2702
2703
2704
2705
2706
2707
2708
2709
2710
2711
2712
2713
2714
2715
2716
2717
2718
2719
2720
2721
2722
2723
2724
2725
2726
2727
2728
2729
2730
2731
2732
2733
2734
2735
2736
2737
2738
2739
2740
2741
2742
2743
2744
2745
2746
2747
2748
2749
2750
2751
2752
2753
2754
2755
2756
2757
2758
2759
2760
2761
2762
2763
2764
2765
2766
2767
2768
2769
2770
2771
2772
2773
2774
2775
2776
2777
2778
2779
2780
2781
2782
2783
2784
2785
2786
2787
2788
2789
2790
2791
2792
2793
2794
2795
2796
2797
2798
2799
2800
2801
2802
2803
2804
2805
2806
2807
2808
2809
2810
2811
2812
2813
2814
2815
2816
2817
2818
2819
2820
2821
2822
2823
2824
2825
2826
2827
2828
2829
2830
2831
2832
2833
2834
2835
2836
2837
2838
2839
2840
2841
2842
2843
2844
2845
2846
....
2950
2951
2952
2953
2954
2955
2956
2957
2958
2959
2960
2961
2962
2963
2964
	list [sys dump !b] [sys dump !a] \
	    [sys unset !b] [sys unset !a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {{3 {1 1 0} 1 {2 1 1} 0 {2 0 0}} {2 {0 1 0} 1 {2 1 1} 0 {2 0 0}} {} {} 2}
}

test bdd-7.5 {notnthvar - redundant var (tests duplicate BDD_MakeBead)} {
    -setup {bdd::system create sys}
    -body {
	sys notnthvar !a 0; sys notnthvar !b 1; sys notnthvar !c 0
	list [sys beadindex !a] [sys beadindex !b] [sys beadindex !c] \
	    [sys unset !a] [sys unset !b] [sys unset !c] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {2 3 2 {} {} {} 2}
}

test bdd-7.6 {unset} {*}{
    -setup {bdd::system create sys}
    -body {
	sys nthvar a 0
	sys unset a
	list [catch {sys := b a} result] $result $::errorCode [sys gc]
    }
    -cleanup {sys destroy}
    -result {1 {expression named "a" not found} {BDD ExprNotFound a} 2} 
}

test bdd-8.1 {negate - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys ~}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	    [sys unset result a1 a2 a4 a8 b1 b2 b4 b8 z1 z2 z4 z8] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {{1 2 3 2 3 4 2 3 4 2 2 2} {} 2}
}

test bdd-20.1 {simplify - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys simplify
    }
    -cleanup {
	sys destroy
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test bdd-20.2 {simplify - bad first expr} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 0; sys notnthvar !b 0
    }
    -body {list [catch {sys simplify c garbage b} result] $result $::errorCode}
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-20.3 {simplify - bad second expr} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 0; sys notnthvar !b 0
    }
    -body {list [catch {sys simplify c a garbage} result] $result $::errorCode}
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-20.4 {simplify - trivial cases} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 0; sys notnthvar !b 0
    }
    -body {
	set trouble {}
	foreach {f d r} {
	    0 0 0
	    0 b 0
	    0 1 0
	    1 0 1
	    1 b 1
	    1 1 1
	    a 0 0
	    a a 1
	    a 1 a
	} {
	    sys simplify z $f $d
	    if {[sys beadindex z] != [sys beadindex $r]} {
		lappend trouble "simplify $f wrt $d did not yield $r"
	    }
	}
	sys unset a b !a !b z
	lappend trouble [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result 2
}

test bdd-20.5 {simplify - example 1} {*}{
    -setup {
	bdd::system create sys
	sys nthvar v1 0
	sys nthvar v2 1
	sys nthvar v3 2; sys notnthvar !v3 2
	sys nthvar v4 3
    }
    -body {
	sys & shouldbe v1 v2
	sys & temp !v3 v4 
	sys ?: f v1 v2 temp
	sys unset temp
	sys | domain v1 v3
	sys simplify is f domain
	list [expr {[sys beadindex is] == [sys beadindex shouldbe]}] \
	    [sys unset v1 v2 v3 !v3 v4 f domain is shouldbe] \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test bdd-20.6 {simplify - no change to system} {*}{
    -setup {
	bdd::system create sys
	sys nthvar v1 0; sys notnthvar !v1 0
	sys nthvar v2 1; sys notnthvar !v2 1
	sys nthvar v3 2; sys notnthvar !v3 2
    }
    -body {
	sys ?: f v1 !v3 !v2
	sys | domain v2 !v3
	sys simplify is f domain
	list [expr {[sys beadindex is] == [sys beadindex f]}] \
	    [sys unset v1 !v1 v2 !v2 v3 !v3 f domain is] \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test bdd-20.7 {simplify changes variables} {*}{
    -setup {
	bdd::system create sys
	sys nthvar v1 0; sys notnthvar !v1 0
	sys nthvar v2 1; sys notnthvar !v2 1
	sys nthvar v3 2; sys notnthvar !v3 2
    }
    -body {
	sys ?: f v1 v3 !v2
	sys | domain !v1 v3
	sys | sb v1 !v2
	sys simplify is f domain
	list [expr {[sys beadindex is] == [sys beadindex sb]}] \
	    [sys unset v1 !v1 v2 !v2 v3 !v3 f domain is sb] \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test bdd-30.1 {eight queens} {*}{
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 64} {incr i} {
	    sys nthvar v$i $i; sys notnthvar !v$i $i
	}
    }
    -body {
................................................................................
	lreverse $sols

    }
    -cleanup {rename sys {}}
    -result {2 04752613 05726314 06357142 06471352 13572064 14602753 14630752 15063724 15720364 16257403 16470352 17502463 20647135 24170635 24175360 24603175 24730615 25147063 25160374 25164073 25307461 25317460 25703641 25704613 25713064 26174035 26175304 27360514 30471625 30475261 31475026 31625704 31625740 31640752 31746025 31750246 35041726 35716024 35720641 36074152 36271405 36415027 36420571 37025164 37046152 37420615 40357162 40731625 40752613 41357206 41362750 41506372 41703625 42057136 42061753 42736051 46027531 46031752 46137025 46152037 46152073 46302751 47302516 47306152 50417263 51602473 51603742 52064713 52073164 52074136 52460317 52470316 52613704 52617403 52630714 53047162 53174602 53602417 53607142 57130642 60275314 61307425 61520374 62057413 62714053 63147025 63175024 64205713 71306425 71420635 72051463 73025164}
}

test bdd-30.2 {verification of a full adder} {
    -setup {
	bdd::system create sys
	sys nthvar x 0; sys notnthvar !x 0
	sys nthvar y 1; sys notnthvar !y 1
	sys nthvar ci 2; sys notnthvar !ci 2
    }
    -body {