tclbdd

Check-in [7fff8b5c6a]
Login

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

Overview
Comment:Added quantifiers - no tests yet.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:7fff8b5c6afac223c663be799ed1c516704ac4cc
User & Date: kbk 2013-12-03 04:24:19
Context
2013-12-04
06:01
Gave up on the unique quantifier and expunged it from the code. Added hard tests for exists and forall; now need tests of the glue surrounding them. check-in: 232f5ceef1 user: kbk tags: trunk
2013-12-03
04:24
Added quantifiers - no tests yet. check-in: 7fff8b5c6a user: kbk tags: trunk
2013-12-02
01:25
foreach_sat test cases check-in: e966ffd735 user: kennykb tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

1153
1154
1155
1156
1157
1158
1159





































































































































1160
1161
1162
1163
1164
1165
1166
    Tcl_HashTable H;		/* Cache of partial results */
    BDD_BeadIndex result;	/* Bead index of the result */
    Tcl_InitHashTable(&H, TCL_ONE_WORD_KEYS);
    result = Restrict(&H, sysPtr, u, r, n);
    Tcl_DeleteHashTable(&H);
    return result;
}





































































































































 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_SatCount --
 *
 *	Counts the number of variable assignments that satisfy the expression







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







1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
    Tcl_HashTable H;		/* Cache of partial results */
    BDD_BeadIndex result;	/* Bead index of the result */
    Tcl_InitHashTable(&H, TCL_ONE_WORD_KEYS);
    result = Restrict(&H, sysPtr, u, r, n);
    Tcl_DeleteHashTable(&H);
    return result;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_Quantify --
 *
 *	Apply an existential, unique, or universal quantifier to a BDD.
 *
 * Results:
 *	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 */
    BDD_BeadIndex r;		/* Return value */
    int newFlag;		/* Flag == 1 iff the result was not cached */
    Tcl_HashEntry* entryPtr;	/* Pointer to the hash entry for
				 * a cached result */

    /* Check for a cached result */
    entryPtr = Tcl_CreateHashEntry(H, (ClientData) u, &newFlag);
    if (!newFlag) {
	r = (BDD_BeadIndex) Tcl_GetHashValue(entryPtr);
	++sysPtr->beads[r].refCount;
	return r;
    }

    for (;;) {
	Bead* beadPtr = sysPtr->beads + u;
	if (v == 0) {
	    /*
	     * No variables remain to quantify. Simply return the expression
	     * itself.
	     */
	    ++beadPtr->refCount;
	    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 if (q == BDD_QUANT_UNIQUE) {
	    /* 
	     * There is a quantified variable that does not appear free in
	     * the expression.
	     *
	     * If the quantifier is UNIQUE, then either value of the variable
	     * will satisfy the expression equally, and no unique solution
	     * is possible.
	     */
	    r = 0;
	    ++sysPtr->beads[r].refCount;
	    break;
	} else {
	    /* 
	     * The current variable does not appear free in the expression,
	     * and the quantifier is EXISTS or FORALL. The quantification is
	     * trivially satisfied with respect to the variable in question.
	     * Advance to the next variable.
	     */
	    ++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.
     */
    ++sysPtr->beads[r].refCount;
    Tcl_SetHashValue(entryPtr, (ClientData) r);
    return r;
}
BDD_BeadIndex
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 --
 *
 *	Counts the number of variable assignments that satisfy the expression

Changes to generic/bdd.h.

51
52
53
54
55
56
57









58
59
60
61
62
63
64
...
102
103
104
105
106
107
108





109
110
111
112
113
114
115

    BDD_BINOP_OR = 0xe,         /* 0    1   1   1  */ /* a | b */

    /* BDD_BINOP_TRUE = 0xf */

} BDD_BinOp;










typedef struct BDD_System BDD_System;
typedef struct BDD_AllSatState BDD_AllSatState;

/* Type of a bead index */

typedef size_t BDD_BeadIndex;	/* Making this 'unsigned int'
				 * limits the size of a BDD system to
................................................................................
extern BDDAPI BDD_BeadIndex BDD_Negate(BDD_System* sysPtr, BDD_BeadIndex u);
extern BDDAPI BDD_BeadIndex BDD_Apply(BDD_System* sysPtr, BDD_BinOp op,
				      BDD_BeadIndex u1, BDD_BeadIndex u2);
extern BDDAPI BDD_BeadIndex BDD_Restrict(BDD_System* sysPtr,
					 BDD_BeadIndex u,
					 const BDD_ValueAssignment r[],
					 BDD_VariableIndex n);





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);







>
>
>
>
>
>
>
>
>







 







>
>
>
>
>







51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
...
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129

    BDD_BINOP_OR = 0xe,         /* 0    1   1   1  */ /* a | b */

    /* BDD_BINOP_TRUE = 0xf */

} BDD_BinOp;

/*
 * Quantifiers for use with BDD's
 */
typedef enum BDD_Quantifier {
    BDD_QUANT_FORALL = BDD_BINOP_AND,
    BDD_QUANT_EXISTS = BDD_BINOP_OR,
    BDD_QUANT_UNIQUE = BDD_BINOP_XOR,
} BDD_Quantifier;

typedef struct BDD_System BDD_System;
typedef struct BDD_AllSatState BDD_AllSatState;

/* Type of a bead index */

typedef size_t BDD_BeadIndex;	/* Making this 'unsigned int'
				 * limits the size of a BDD system to
................................................................................
extern BDDAPI BDD_BeadIndex BDD_Negate(BDD_System* sysPtr, BDD_BeadIndex u);
extern BDDAPI BDD_BeadIndex BDD_Apply(BDD_System* sysPtr, BDD_BinOp op,
				      BDD_BeadIndex u1, BDD_BeadIndex u2);
extern BDDAPI BDD_BeadIndex BDD_Restrict(BDD_System* sysPtr,
					 BDD_BeadIndex u,
					 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);

Changes to generic/tclBdd.c.

93
94
95
96
97
98
99

100
101
102
103
104
105
106
...
116
117
118
119
120
121
122


123
124
125
126
127
128
129
...
206
207
208
209
210
211
212







213
214
215
216
217
218
219
...
245
246
247
248
249
250
251




252
253
254
255
256
257
258
259


260
261
262
263
264
265
266
....
1049
1050
1051
1052
1053
1054
1055

































































































1056
1057
1058
1059
1060
1061
1062
....
1479
1480
1481
1482
1483
1484
1485

























1486
1487
1488
1489
1490
1491
1492
static Tcl_HashEntry* FindHashEntryForNamedExpression(Tcl_Interp*,
						      BddSystemData*,
						      Tcl_Obj*);
static int FindNamedExpression(Tcl_Interp*, BddSystemData*, Tcl_Obj*,
			       BDD_BeadIndex*);
static int UnsetNamedExpression(Tcl_Interp*, BddSystemData*, Tcl_Obj*);
static int CompareValueAssignments(const void* a, const void* b);

static void DeletePerInterpData(PerInterpData*);
static int BddSystemConstructor(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int BddSystemBeadindexMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				    int, Tcl_Obj* const[]);
static int BddSystemBinopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
................................................................................
static int ForeachSatPost(ClientData data[4], Tcl_Interp*, int);
static int BddSystemNegateMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				 int, Tcl_Obj* const[]);
static int BddSystemNotnthvarMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				    int, Tcl_Obj* const[]);
static int BddSystemNthvarMethod(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 BddSystemUnsetMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int CloneBddSystemObject(Tcl_Interp*, ClientData, ClientData*);
................................................................................
};
const static Tcl_MethodType BddSystemNthvarMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "nthvar",			   /* name */
    BddSystemNthvarMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */







};
const static Tcl_MethodType BddSystemRestrictMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "restrict",			   /* name */
    BddSystemRestrictMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
................................................................................
    { "<=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LE },
    { "==",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_EQ },
    { ">",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GT },
    { ">=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GE },
    { "^",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_XOR },
    { "beadindex", &BddSystemBeadindexMethodType, NULL },
    { "dump",      &BddSystemDumpMethodType,      NULL },




    { "foreach_sat",
                   &BddSystemForeachSatMethodType,NULL },
    { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
    { "restrict",  &BddSystemRestrictMethodType,  NULL },
    { "satcount",  &BddSystemSatcountMethodType,  NULL },


    { "unset",     &BddSystemUnsetMethodType,     NULL },
    { "|",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_OR },
    { "~",         &BddSystemNegateMethodType,    NULL },
    { NULL,	   NULL,                         NULL }
};
 
/*
................................................................................
    BDD_UnrefBead(sdata->system, beadIndex);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *

































































































 * BddSystemRestrictMethod --
 *
 *	Computes a BDD restricted to a particular set of variable values
 *
 * Usage:
 *	$system restrict name expr r1 r2 ...
 *
................................................................................
{
    const BDD_ValueAssignment* aPtr = (const BDD_ValueAssignment*) a;
    const BDD_ValueAssignment* bPtr = (const BDD_ValueAssignment*) b;
    if (aPtr->var < bPtr->var) return -1;
    else if (aPtr->var > bPtr->var) return 1;
    else return 0;
}

























 
/*
 *-----------------------------------------------------------------------------
 *
 * DeleteBddSystemData --
 *
 *	Final cleanup when a system of BDD's is deleted







>







 







>
>







 







>
>
>
>
>
>
>







 







>
>
>
>








>
>







 







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







 







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







93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
...
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
...
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
...
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
....
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
....
1592
1593
1594
1595
1596
1597
1598
1599
1600
1601
1602
1603
1604
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
static Tcl_HashEntry* FindHashEntryForNamedExpression(Tcl_Interp*,
						      BddSystemData*,
						      Tcl_Obj*);
static int FindNamedExpression(Tcl_Interp*, BddSystemData*, Tcl_Obj*,
			       BDD_BeadIndex*);
static int UnsetNamedExpression(Tcl_Interp*, BddSystemData*, Tcl_Obj*);
static int CompareValueAssignments(const void* a, const void* b);
static int CompareVariableIndices(const void* a, const void* b);
static void DeletePerInterpData(PerInterpData*);
static int BddSystemConstructor(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int BddSystemBeadindexMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				    int, Tcl_Obj* const[]);
static int BddSystemBinopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
................................................................................
static int ForeachSatPost(ClientData data[4], Tcl_Interp*, int);
static int BddSystemNegateMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				 int, Tcl_Obj* const[]);
static int BddSystemNotnthvarMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				    int, Tcl_Obj* const[]);
static int BddSystemNthvarMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				 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 BddSystemUnsetMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int CloneBddSystemObject(Tcl_Interp*, ClientData, ClientData*);
................................................................................
};
const static Tcl_MethodType BddSystemNthvarMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "nthvar",			   /* name */
    BddSystemNthvarMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemQuantifyMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "quantify",			   /* name */
    BddSystemQuantifyMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemRestrictMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "restrict",			   /* name */
    BddSystemRestrictMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
................................................................................
    { "<=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LE },
    { "==",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_EQ },
    { ">",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GT },
    { ">=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GE },
    { "^",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_XOR },
    { "beadindex", &BddSystemBeadindexMethodType, NULL },
    { "dump",      &BddSystemDumpMethodType,      NULL },
    { "exists",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_EXISTS },
    { "forall",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_FORALL },
    { "foreach_sat",
                   &BddSystemForeachSatMethodType,NULL },
    { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
    { "restrict",  &BddSystemRestrictMethodType,  NULL },
    { "satcount",  &BddSystemSatcountMethodType,  NULL },
    { "unique",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_UNIQUE },
    { "unset",     &BddSystemUnsetMethodType,     NULL },
    { "|",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_OR },
    { "~",         &BddSystemNegateMethodType,    NULL },
    { NULL,	   NULL,                         NULL }
};
 
/*
................................................................................
    BDD_UnrefBead(sdata->system, beadIndex);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemQuantifyMethod --
 *
 *	Quantifies a BDD with respect to a particular set of variables.
 *
 * Usage:
 *	$system exists $name $vars $expr
 *	$system forall $name $vars $expr
 *	$system unique $name $vars $expr
 *
 * Parameters:
 *	system - System of BDD's
 *	name - Name to assign to the resulting expression.
 *	vars - List of literals that must be un-negated variable names
 *	expr - Expression to quantify.
 *
 * Results:
 *	Returns a standard Tcl result
 *
 * Side effects:
 *	Creates the named expression if successful
 *
 *-----------------------------------------------------------------------------
 */
static int
BddSystemQuantifyMethod(
    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 */
{
    BDD_Quantifier q = (BDD_Quantifier) clientData;
				/* The quantifier to apply */
    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 u;		/* Expression to quantify */
    int varc;			/* Count of variable names supplied */
    Tcl_Obj** varv;		/* List of variable names supplied */
    BDD_BeadIndex literalIndex;	/* Index of the current variable as a BDD */
    BDD_VariableIndex* v;	/* Variables to quantify */
    BDD_ValueAssignment a;	/* Current quantified variable */
    Tcl_Obj* errorMessage;	/* Error message of a failed execution */
    BDD_BeadIndex result;	/* Result of the quantification */
    BDD_VariableIndex i;

    /* Check syntax */

    if (objc != skipped+3) {
	Tcl_WrongNumArgs(interp, skipped, objv, "name vars expr");
	return TCL_ERROR;
    }
    if (FindNamedExpression(interp, sdata, objv[skipped+2],
			    &u) != TCL_OK) {
	return TCL_ERROR;
    }
    if (Tcl_ListObjGetElements(interp, objv[skipped+1],
			       &varc, &varv) != TCL_OK) {
	return TCL_ERROR;
    }
    v = ckalloc(varc);
    for (i = 0; i < varc; ++i) {
	if (FindNamedExpression(interp, sdata, varv[i],
				&literalIndex) != TCL_OK) {
	    ckfree(v);
	    return TCL_ERROR;
	}
	if (!BDD_Literal(sdata->system, literalIndex, &a)
	    || (a.value == 0)) {
	    errorMessage = Tcl_ObjPrintf("%s is not a variable",
					 Tcl_GetString(varv[i]));
	    Tcl_SetObjResult(interp, errorMessage);
	    Tcl_SetErrorCode(interp, "BDD", "NotVariable",
			     Tcl_GetString(varv[i]), NULL);
	    ckfree(v);
	    return TCL_ERROR;
	}	    
    }

    /*
     * Order the literals
     */
    qsort(v, varc, sizeof(BDD_VariableIndex), CompareVariableIndices);

    result = BDD_Quantify(sdata->system, q, v, varc, u);
    SetNamedExpression(sdata, objv[skipped], result);
    BDD_UnrefBead(sdata->system, result);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemRestrictMethod --
 *
 *	Computes a BDD restricted to a particular set of variable values
 *
 * Usage:
 *	$system restrict name expr r1 r2 ...
 *
................................................................................
{
    const BDD_ValueAssignment* aPtr = (const BDD_ValueAssignment*) a;
    const BDD_ValueAssignment* bPtr = (const BDD_ValueAssignment*) b;
    if (aPtr->var < bPtr->var) return -1;
    else if (aPtr->var > bPtr->var) return 1;
    else return 0;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * CompareVariableIndices --
 *
 *	Callback for 'qsort' to compare	variable indices.
 *
 * Results:
 *	Returns -1 if a < b; 0 if a == b, 1 if a > b.
 *
 *-----------------------------------------------------------------------------
 */

static int
CompareVariableIndices(
    const void* a,		/* Pointer to first assignment */
    const void* b)		/* Pointer to second assignment */
{
    const BDD_VariableIndex* aPtr = (const BDD_VariableIndex*) a;
    const BDD_VariableIndex* bPtr = (const BDD_VariableIndex*) b;
    if (*aPtr<*bPtr) return -1;
    else if (*aPtr>*bPtr) return 1;
    else return 0;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * DeleteBddSystemData --
 *
 *	Final cleanup when a system of BDD's is deleted