tclbdd

Check-in [62023edbb8]
Login

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

Overview
Comment:Fix beadcount - didn't work at all. Added loading of FDDD rows.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:62023edbb87aff0740a663e16224dc87f2b8f67f
User & Date: kbk 2013-12-13 04:57:36
Context
2013-12-13
20:22
Remove dribble from minterm loader. Fix variables-out-of-order check in minterm loader. Add minterm loader test vectors. check-in: 3194251647 user: kbk tags: trunk
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
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/tclBdd.c.

10
11
12
13
14
15
16

17
18
19
20
21
22
23
...
133
134
135
136
137
138
139


140
141
142
143
144
145
146
...
235
236
237
238
239
240
241







242
243
244
245
246
247
248
...
341
342
343
344
345
346
347

348
349
350
351
352
353
354
....
1303
1304
1305
1306
1307
1308
1309
















































































































































































































1310
1311
1312
1313
1314
1315
1316
 *
 *-----------------------------------------------------------------------------
 */

#include <tcl.h>
#include <tclOO.h>
#include <tclTomMath.h>


#include "tclBddInt.h"

/*
 * Objects to create within the literal pool
 */

................................................................................
				     int, Tcl_Obj *const[]);
static int ForeachSatPre(Tcl_Interp* interp, BddSystemData*,
			 Tcl_Obj* varName, Tcl_Obj* script,
			 BDD_AllSatState* stateVector);
static int ForeachSatPost(ClientData data[4], Tcl_Interp*, int);
static int BddSystemGCMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
			     int, Tcl_Obj *const[]);


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 BddSystemProfileMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
................................................................................
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemGCMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "gc",			   /* name */
    BddSystemGCMethod,		   /* callProc */







    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemNegateMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "negate",			   /* name */
    BddSystemNegateMethod,	   /* callProc */
................................................................................
    { "exists",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_EXISTS },
    { "forall",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_FORALL },
    { "foreach_sat",
                   &BddSystemForeachSatMethodType,NULL },
    { "gc",        &BddSystemGCMethodType,        NULL },

    { "median" ,   &BddSystemTernopMethodType, (ClientData) BDD_TERNOP_MEDIAN },
    { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },
    { "nand3",     &BddSystemTernopMethodType,   (ClientData) BDD_TERNOP_NAND },
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "nor3",      &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
................................................................................
    }

    beadCount = BDD_GarbageCollect(sdata->system);

    Tcl_SetObjResult(interp, Tcl_NewWideIntObj(beadCount));
    return TCL_OK;
}
















































































































































































































 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemNegateMethod --
 *
 *	Computes the negation of a named expression in a system of







>







 







>
>







 







>
>
>
>
>
>
>







 







>







 







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







10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
...
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
...
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
...
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
....
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
 *
 *-----------------------------------------------------------------------------
 */

#include <tcl.h>
#include <tclOO.h>
#include <tclTomMath.h>
#include <limits.h>

#include "tclBddInt.h"

/*
 * Objects to create within the literal pool
 */

................................................................................
				     int, Tcl_Obj *const[]);
static int ForeachSatPre(Tcl_Interp* interp, BddSystemData*,
			 Tcl_Obj* varName, Tcl_Obj* script,
			 BDD_AllSatState* stateVector);
static int ForeachSatPost(ClientData data[4], Tcl_Interp*, int);
static int BddSystemGCMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
			     int, Tcl_Obj *const[]);
static int BddSystemLoadMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
			       int, Tcl_Obj* const[]);
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 BddSystemProfileMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
................................................................................
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemGCMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "gc",			   /* name */
    BddSystemGCMethod,		   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemLoadMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "load",			   /* name */
    BddSystemLoadMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemNegateMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "negate",			   /* name */
    BddSystemNegateMethod,	   /* callProc */
................................................................................
    { "exists",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_EXISTS },
    { "forall",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_FORALL },
    { "foreach_sat",
                   &BddSystemForeachSatMethodType,NULL },
    { "gc",        &BddSystemGCMethodType,        NULL },
    { "load",      &BddSystemLoadMethodType,      NULL },
    { "median" ,   &BddSystemTernopMethodType, (ClientData) BDD_TERNOP_MEDIAN },
    { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },
    { "nand3",     &BddSystemTernopMethodType,   (ClientData) BDD_TERNOP_NAND },
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "nor3",      &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
................................................................................
    }

    beadCount = BDD_GarbageCollect(sdata->system);

    Tcl_SetObjResult(interp, Tcl_NewWideIntObj(beadCount));
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDDSystemLoadMethod --
 *
 *	OR's a minterm representing a tuple in a finite domain into a
 *	BDD representing a relation.
 *
 * Usage:
 *	$system load relation description value ?value ...?
 *
 * Parameters:
 *	system - System of BDD's
 *	relation - Name of the BDD representing the relation. The BDD
 *	           need not yet exist; if it does not, it will be initially
 *		   created as the constant 0.
 *	description - List describing the mapping of bits in the values to
 *		      variables in the BDD.
 *	value... - Integer values in the finite domain of the columns of
 *		   the relation.
 *
 * Results:
 *	Returns a standard Tcl result, empty on success or with an
 *	error message on failure.
 *
 * Side effects:
 *	An AND-term is constructed from the bit values and the term is OR-ed
 *	into the relation under construction.
 *
 * The description is a list whose length is a multiple of three.
 * Element 3*n is the level number of a variable in the BDD. Element
 * 3*n+1 is the index of a value within the 'value' parameters to this
 * method. Element 3*n+2 is the bit position (0 -> 1, 1 -> 2, 2 -> 4, 4-> 8
 * and so on) of the bit in the value that gives the value of the variable.
 * The variables MUST be listed in increasing order.
 *
 *-----------------------------------------------------------------------------
 */

static int
BddSystemLoadMethod(
    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 */
    Tcl_Obj* name;		/* Name of the named relation */
    int paramc = objc-skipped-2;
				/* Number of supplied parameters */
    Tcl_WideInt* paramv;	/* Vector of integer parameters */
    int descc;			/* Count of elements in the description list */
    Tcl_Obj** descv;		/* Description list */
    int i;
    BDD_BeadIndex minterm;	/* Minterm under construction */
    BDD_BeadIndex relation;	/* Relation under construction */
    BDD_BeadIndex temp;
    int lastVarIndex = INT_MAX;	/* Variable index from the last trip */
    int varIndex;		/* Variable index */
    int paramIndex;		/* Parameter index */
    int bitPos;			/* Bit position within the value */
    Tcl_HashEntry* entryPtr;	/* Hash entry holding the named relation */
    int newFlag;		/* Flag == 1 if the relation is newly created */

    /*
     * check param count
     */
    if (objc < skipped+2) {
	Tcl_WrongNumArgs(interp, skipped, objv, 
			 "relation description ?value...?");
	return TCL_ERROR;
    }
    name = objv[skipped];

    /*
     * Get parameter values
     */
    fprintf(stderr, "loading %s: parse param values\n", Tcl_GetString(name));
    paramv = ckalloc(paramc * sizeof(Tcl_WideInt));
    for (i = 0; i < paramc; ++i) {
	fprintf(stderr, "        %s: param %d\n", Tcl_GetString(name), i);
	if (Tcl_GetWideIntFromObj(interp, objv[skipped+2+i],
				  paramv+i) != TCL_OK) {
	    ckfree(paramv);
	    return TCL_ERROR;
	}
	fprintf(stderr, "        %s: value = %ld\n",
		Tcl_GetString(name), paramv[i]);
    }

    /*
     * Unpack description
     */
    if (Tcl_ListObjGetElements(interp, objv[skipped+1],
			       &descc, &descv) != TCL_OK) {
	ckfree(paramv);
	return TCL_ERROR;
    }
    fprintf(stderr, "loading %s: %d elements in description vector\n",
	    Tcl_GetString(name), descc);
    if (descc % 3 != 0) {
	Tcl_SetObjResult(interp, Tcl_NewStringObj("description list must have "
						  "a multiple of 3 "
						  "elements", -1));
	Tcl_SetErrorCode(interp, "BDD DescNotMultipleOf3", NULL);
	ckfree(paramv);
	return TCL_ERROR;
    }

    /*
     * Convert the given integer values to a minterm
     */
    minterm = 1;
    BDD_IncrBeadRefCount(sdata->system, minterm);
    for (i = descc; i > 0; ) {
	i -= 3;
	/*
	 * Unpack the description for the current bit
	 */
	if (Tcl_GetIntFromObj(interp, descv[i], &varIndex) != TCL_OK
	    || Tcl_GetIntFromObj(interp, descv[i+1], &paramIndex) != TCL_OK
	    || Tcl_GetIntFromObj(interp, descv[i+2], &bitPos) != TCL_OK) {
	    BDD_UnrefBead(sdata->system, minterm);
	    ckfree(paramv);
	    return TCL_ERROR;
	}
	fprintf(stderr, "loading %s: var=%d param=%d (bit %d)\n",
		Tcl_GetString(name), varIndex, paramIndex, bitPos);
	if (varIndex >= lastVarIndex) {
	    Tcl_SetObjResult(interp, Tcl_NewStringObj("variables are not in "
						      "increasing order", -1));
	    Tcl_SetErrorCode(interp, "BDD", "VarsOutOfOrder", NULL);
	    BDD_UnrefBead(sdata->system, minterm);
	    ckfree(paramv);
	    return TCL_ERROR;
	}
	if (paramIndex >= paramc || paramIndex < 0) {
	    Tcl_SetObjResult(interp, Tcl_NewStringObj("description refers to a "
						      "nonexistent "
						      "parameter", -1));
	    Tcl_SetErrorCode(interp, "BDD", "NonexistentParam", NULL);
	    BDD_UnrefBead(sdata->system, minterm);
	    ckfree(paramv);
	    return TCL_ERROR;
	}
	if (bitPos >= CHAR_BIT * sizeof(Tcl_WideInt) || bitPos < 0) {
	    Tcl_SetObjResult(interp, Tcl_NewStringObj("bad bit index in "
						      "description", -1));
	    Tcl_SetErrorCode(interp, "BDD", "BadBitIndex", NULL);
	    BDD_UnrefBead(sdata->system, minterm);
	    ckfree(paramv);
	    return TCL_ERROR;
	}

	/*
	 * Make a literal for the current bit and AND it with the minterm
	 * under construction.
	 */
	if ((paramv[paramIndex] >> bitPos) & 1) {
	    fprintf(stderr, "        %s: make bead (%u, %lu, %lu)\n",
		    Tcl_GetString(name),
		    (BDD_VariableIndex) varIndex, (BDD_BeadIndex) 0, minterm);
	    temp = BDD_MakeBead(sdata->system, (BDD_VariableIndex) varIndex,
				(BDD_BeadIndex) 0, minterm);
	} else {
	    fprintf(stderr, "        %s: make bead (%u, %lu, %lu)\n",
		    Tcl_GetString(name),
		    (BDD_VariableIndex) varIndex, minterm, (BDD_BeadIndex) 0);
	    temp = BDD_MakeBead(sdata->system, (BDD_VariableIndex) varIndex,
				minterm, 0);
	}
	BDD_UnrefBead(sdata->system, minterm);
	minterm = temp;
    }
    ckfree(paramv);

    /*
     * OR the minterm into the named relation, creating the empty
     * relation if necessary.
     */
    entryPtr = Tcl_CreateHashEntry(sdata->expressions, name, &newFlag);
    if (newFlag) {
	fprintf(stderr, "start a new (empty) relation %s\n",
		Tcl_GetString(name));
	relation = 0;
	BDD_IncrBeadRefCount(sdata->system, relation);
    } else {
	relation = (BDD_BeadIndex) Tcl_GetHashValue(entryPtr);
    }
    temp = relation;
    fprintf(stderr, "OR the minterm into %s\n", Tcl_GetString(name));
    relation = BDD_Apply(sdata->system, BDD_BINOP_OR, relation, minterm);
    BDD_UnrefBead(sdata->system, temp);
    BDD_UnrefBead(sdata->system, minterm);
    Tcl_SetHashValue(entryPtr, relation);
    fprintf(stderr, "Done loading a row of %s\n", Tcl_GetString(name));

    return TCL_OK;
    
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemNegateMethod --
 *
 *	Computes the negation of a named expression in a system of

Changes to library/tclbdd.tcl.

34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
	    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}







|







34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
	    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}

Changes to library/tclfdd.tcl.

1
2
3
4
5




































6
7
8
9
10
11
12
..
22
23
24
25
26
27
28






















29
30
31
32
33
34
35
..
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
................................................................................
	    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]} {
................................................................................
	    }
	    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
}



    





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







 







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







 







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







 







<

<
<
>

|

|


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




<







<
<




<
<
<



|
<
<
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
..
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
...
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
...
142
143
144
145
146
147
148

149


150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207

208
209
210
211
212
213
214


215
216
217
218



219
220
221
222


#package require tclbdd 0.1

namespace eval fdd {
    namespace export domain interleave concatenate
}

#-----------------------------------------------------------------------------
#
# The next few procedures are for working with domain descriptions, which
# describe a finite, multivalued domain within a BDD. A domain description
# consists of two parts:
#	    
#	(1) A dictionary whose keys are domain names and whose values
#	    are the number of bits used to encode values in the given
#	    domains.
#
#	(2) A list that gives the layout of BDD variables that
#	    represent values in the given domains. The list appears in
#	    order by variable index. It consists of alternating domain
#	    names and bit positions in values in the domain (with
#	    position zero being the least significant bit).
#
#-----------------------------------------------------------------------------

# fdd::domain --
#
#	Defines a new finite domain
#
# Usage:
#	fdd::domain name width ?endian?
#
# Parameters:
#	name - Name of the domain
#	width - Log base 2 of the number of distinct values.
#	endian - 'littleendian' (default) if the values are to be
#		 encoded in BDD's with the least significant bit first.
#		 'bigendian' if they are to be encoded with the most
#		 significant bit first
#
# Results:
#	Returns a domain description.

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
................................................................................
	    return -code error -errorcode [list FDD BadEndian $endian] \
		"unknown endian \"$endian\": must be bigendian or littleendian"
	}
    }
    return [list [dict create $name $width] $l]
}

# fdd::interleave --
#
#	Interleaves some number of finite domains so that their bit positions
#	in a BDD alternate.
#
# Usage:
#	fdd::interleave ?description...?
#
# Parameters:
#	Zero or more domain descriptions whose bits are to be interleaved.
#	All domains in the descriptions must be distinct.
#
# Results:
#	Returns a domain description of the interleaved domains.
#
# Errors:
#	{FDD DuplicateName $name} if any domain is not distinct
#
# The domains are interleaved by taking one bit from the first domain,
# one from the second, and so on. If they are of differing length, then
# the process ceases taking bits from the shorter ones when they run out.

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]} {
................................................................................
	    }
	    incr i
	}
    }
    return [list $names $scrambled]
}

# fdd::concatenate --
#
#	Concatenates the descriptions of a set of finite domains
#
# Usage:
#	fdd::concatenate ?description...?
#
# Parameters:
#	Zero or more finite domain descriptions.
#
# Results:
#	Returns a description with the bits of the domains concatenated
#	together.
#
# Errors:
#	{FDD DuplicateName $name} if any domain is not distinct

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]

    }


    set chain {}
    foreach b $bits {
	lappend chain {*}$b
    }
    return [list $names $chain]
}

# fdd::reader --
#
#	Makes a call to the BDD engine to construct a minterm corresponding
#	to a tuple in a finite domain.
#
# Usage:
#	fdd::reader sysName termName layout domain ?domain...?
#
# Parameters:
#	sysName - Name of the system of BDD's
#	termName - Name of the term to be constructed
#	layout - Description of the finite domain
#	domain - One or more domain names, in the order in which values
#	         will appear in an input tuple.
#
# Results:
#	Returns a command prefix for a command that will create a
#	named term containing a tuple. 
#
# To the prefix should be appended the values of the domain elements,
# in the order in which their domains appeared on this command.
#
# Example:
#
# set desc \
#     [fdd::concatenate \
#         [fdd::domain var 3 bigendian] \
#         [fdd::interleave \
#             [fdd::domain stmt 5] [fdd::domain stmt2 5]]]
#  set r [fdd::reader sys reads $desc stmt var]
#
# leaves desc set to:
#
#    {var 3 stmt 5 stmt2 5} 
#    {var 2 var 1 var 0 stmt 0 stmt2 0 stmt 1 stmt2 1 stmt 2 stmt2 2 
#     stmt 3 stmt2 3 stmt 4 stmt2 4}
#
# and r set to:
#   sys load reads {0 1 2 1 1 1 2 1 0 3 0 0 5 0 1 7 0 2 9 0 3 11 0 4}
#
# which (when two additional args are catenated on the end), asks the BDD
# system "construct a minterm named 'reads', where variable zero is set from
# parameter 1, the 2**2 bit, variable 1 from parameter 1 the 2**1 bit,
# variable 2 from parameter 1 the 2**0 bit, variable 3 from parameter 0 the
# 2**0 bit, variable 5 from parameter 0 the 2**1 bit ... variable 11 from
# parameter 0 the 2**4 bit."

proc fdd::reader {sysName termName layout args} {
    set i 0
    foreach name $args {
	dict set cmdpos $name $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


	}
	incr p
    }
    set cmd [list $sysName load $termName $result]



    return $cmd
}

package provide tclfdd 0.1