tclbdd

Check-in [232f5ceef1]
Login

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

Overview
Comment: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.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:232f5ceef1567539c8d98be3282c2d27442b1b8c
User & Date: kbk 2013-12-04 06:01:00
Original Comment: Gave up on the unique quantifier and expunged it from the code. Added hard tests for exists and forall; now need tests of the glus surrounding them.
Context
2013-12-05
03:08
Add a first whack at a Boolean expression parser check-in: d459b6ae38 user: kbk tags: trunk
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
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
....
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
	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;
................................................................................
	     */
	    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;
	}
    }
    
    /*







|







 







<
<
<
<
<
<
<
<
<
<
<
<



<
|
|







1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
....
1227
1228
1229
1230
1231
1232
1233












1234
1235
1236

1237
1238
1239
1240
1241
1242
1243
1244
1245
	r = (BDD_BeadIndex) Tcl_GetHashValue(entryPtr);
	++sysPtr->beads[r].refCount;
	return r;
    }

    for (;;) {
	Bead* beadPtr = sysPtr->beads + u;
	if (n == 0) {
	    /*
	     * No variables remain to quantify. Simply return the expression
	     * itself.
	     */
	    ++beadPtr->refCount;
	    r = u;
	    break;
................................................................................
	     */
	    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
	     * variable in question. Advance to the next variable.
	     */
	    ++v;
	    --n;
	}
    }
    
    /*

Changes to generic/bdd.h.

57
58
59
60
61
62
63
64
65
66
67
68
69
70
71

/*
 * 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 */








<







57
58
59
60
61
62
63

64
65
66
67
68
69
70

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

} BDD_Quantifier;

typedef struct BDD_System BDD_System;
typedef struct BDD_AllSatState BDD_AllSatState;

/* Type of a bead index */

Changes to generic/tclBdd.c.

267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
....
1146
1147
1148
1149
1150
1151
1152

1153
1154
1155
1156
1157
1158
1159
                   &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 }
};
 
/*
................................................................................
					 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);








<
<







 







>







267
268
269
270
271
272
273


274
275
276
277
278
279
280
....
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
                   &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 }
};
 
/*
................................................................................
					 Tcl_GetString(varv[i]));
	    Tcl_SetObjResult(interp, errorMessage);
	    Tcl_SetErrorCode(interp, "BDD", "NotVariable",
			     Tcl_GetString(varv[i]), NULL);
	    ckfree(v);
	    return TCL_ERROR;
	}	    
	v[i] = a.var;
    }

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

Changes to tests/bdd.test.

1217
1218
1219
1220
1221
1222
1223













































1224
1225
1226
1227
1228
1229
1230
	    $result
    }
    -cleanup {
	rename sys {}
    }
    -result {6 testing}
}














































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
	}







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







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
	    $result
    }
    -cleanup {
	rename sys {}
    }
    -result {6 testing}
}

test bdd-15.n {existential quantifier} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	sys nthvar e 4; sys notnthvar !e 4
	sys nthvar f 5; sys notnthvar !f 5
	sys & expr !e !f; sys & expr expr a
	sys & term !e  f; sys & term term b; sys | expr expr term
	sys & term  e !f; sys & term term c; sys | expr expr term
	sys & term  e  f; sys & term term d; sys | expr expr term
    }
    -body {
	sys | ye a b
	sys | ye ye c
	sys | ye ye d
	sys exists ze {e f} expr
	expr {[sys beadindex ze] == [sys beadindex ye]}
    }
    -cleanup {rename sys {}}
    -result {1}
}

test bdd-15.n {universal quantifier} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	sys nthvar e 4; sys notnthvar !e 4
	sys nthvar f 5; sys notnthvar !f 5
	sys & expr !e !f; sys & expr expr a
	sys & term !e  f; sys & term term b; sys | expr expr term
	sys & term  e !f; sys & term term c; sys | expr expr term
	sys & term  e  f; sys & term term d; sys | expr expr term
    }
    -body {
	sys & yu a b
	sys & yu yu c
	sys & yu yu d
	sys forall zu {e f} expr
	expr {[sys beadindex zu] == [sys beadindex yu]}
    }
    -cleanup {rename sys {}}
    -result {1}
}
    

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
	}