tclbdd

Check-in [d66431592d]
Login

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

Overview
Comment:Removed abuse of the word 'minterm': the terms being discussed were not minimal
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:d66431592d77b1a634c2e24c74cbd12c79922e9a
User & Date: kbk 2013-12-17 18:42:54
Context
2013-12-18
16:06
Added 'replace' method to bdd::system in support of relational algebra. Fixed a typo in '===' method that caused it to fail always check-in: db99db21ba user: kbk tags: trunk
2013-12-17
18:42
Removed abuse of the word 'minterm': the terms being discussed were not minimal check-in: d66431592d user: kbk tags: trunk
16:16
Add test cases for low-level 'project' and fixed the bugs that were exposed check-in: 74ad4ed7f0 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/tclBdd.c.

1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
....
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
....
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
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * 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
................................................................................
    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 */
................................................................................
						  "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;
	}
	if (varIndex >= lastVarIndex || varIndex < 0) {
	    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;
	}
	lastVarIndex = varIndex;
	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) {
	    temp = BDD_MakeBead(sdata->system, (BDD_VariableIndex) varIndex,
				(BDD_BeadIndex) 0, minterm);
	} else {
	    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) {
	relation = 0;
	BDD_IncrBeadRefCount(sdata->system, relation);
    } else {
	relation = (BDD_BeadIndex) Tcl_GetHashValue(entryPtr);
    }
    temp = relation;
    relation = BDD_Apply(sdata->system, BDD_BINOP_OR, relation, minterm);
    BDD_UnrefBead(sdata->system, temp);
    BDD_UnrefBead(sdata->system, minterm);
    Tcl_SetHashValue(entryPtr, relation);

    return TCL_OK;
    
}
 
/*







|







 







|







 







|

|
|








|







|









|







|





|




|


|

|
|




|










|

|







1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
....
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
....
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
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDDSystemLoadMethod --
 *
 *	OR's a term 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
................................................................................
    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 term;		/* Term 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 */
................................................................................
						  "elements", -1));
	Tcl_SetErrorCode(interp, "BDD", "DescNotMultipleOf3", NULL);
	ckfree(paramv);
	return TCL_ERROR;
    }

    /*
     * Convert the given integer values to a term
     */
    term = 1;
    BDD_IncrBeadRefCount(sdata->system, term);
    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, term);
	    ckfree(paramv);
	    return TCL_ERROR;
	}
	if (varIndex >= lastVarIndex || varIndex < 0) {
	    Tcl_SetObjResult(interp, Tcl_NewStringObj("variables are not in "
						      "increasing order", -1));
	    Tcl_SetErrorCode(interp, "BDD", "VarsOutOfOrder", NULL);
	    BDD_UnrefBead(sdata->system, term);
	    ckfree(paramv);
	    return TCL_ERROR;
	}
	lastVarIndex = varIndex;
	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, term);
	    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, term);
	    ckfree(paramv);
	    return TCL_ERROR;
	}

	/*
	 * Make a literal for the current bit and AND it with the term
	 * under construction.
	 */
	if ((paramv[paramIndex] >> bitPos) & 1) {
	    temp = BDD_MakeBead(sdata->system, (BDD_VariableIndex) varIndex,
				(BDD_BeadIndex) 0, term);
	} else {
	    temp = BDD_MakeBead(sdata->system, (BDD_VariableIndex) varIndex,
				term, 0);
	}
	BDD_UnrefBead(sdata->system, term);
	term = temp;
    }
    ckfree(paramv);

    /*
     * OR the term into the named relation, creating the empty
     * relation if necessary.
     */
    entryPtr = Tcl_CreateHashEntry(sdata->expressions, name, &newFlag);
    if (newFlag) {
	relation = 0;
	BDD_IncrBeadRefCount(sdata->system, relation);
    } else {
	relation = (BDD_BeadIndex) Tcl_GetHashValue(entryPtr);
    }
    temp = relation;
    relation = BDD_Apply(sdata->system, BDD_BINOP_OR, relation, term);
    BDD_UnrefBead(sdata->system, temp);
    BDD_UnrefBead(sdata->system, term);
    Tcl_SetHashValue(entryPtr, relation);

    return TCL_OK;
    
}
 
/*

Changes to library/tclfddd.tcl.

153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
...
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
	lappend chain {*}$b
    }
    return [list $names $chain]
}

# bdd::fddd::reader --
#
#	Makes a call to the BDD engine to construct a minterm corresponding
#	to a tuple in a finite domain.
#
# Usage:
#	bdd::fddd::reader sysName termName layout domain ?domain...?
#
# Parameters:
#	sysName - Name of the system of BDD's
................................................................................
#    {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 bdd::fddd::reader {sysName termName layout args} {
    set i 0







|







 







|







153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
...
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
	lappend chain {*}$b
    }
    return [list $names $chain]
}

# bdd::fddd::reader --
#
#	Makes a call to the BDD engine to construct a term corresponding
#	to a tuple in a finite domain.
#
# Usage:
#	bdd::fddd::reader sysName termName layout domain ?domain...?
#
# Parameters:
#	sysName - Name of the system of BDD's
................................................................................
#    {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 term 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 bdd::fddd::reader {sysName termName layout args} {
    set i 0

Changes to tests/fddd.test.

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
...
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
#
#       Tests for Finite Domain Decision Diagrams (FDDD's)
#
# Copyright (c) 2013 by Kevin B. Kenny.

package require tclbdd::fddd

test fddd-1.1 {load minterm - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys load
    }
    -cleanup {
................................................................................
	rename sys {}
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test fddd-1.2 {load minterm - bad integer} {*}{
    -setup {
	bdd::system create sys
    } 
    -body {
	sys load x {} garbage
    } 
    -cleanup {
	rename sys {}
    }
    -result {expected integer but got "garbage"}
    -returnCodes error
}

test fddd-1.3 {load minterm - ill-formed list} {
    -setup {
	bdd::system create sys
    }
    -body {
	sys load x \{ 
    }
    -cleanup {
	rename sys {}
    }
    -result {unmatched open brace in list}
    -returnCodes error
}

test fddd-1.4 {load minterm - wrong list size} {
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys load x {1 2}} result] $result $::errorCode
    }
    -cleanup {
................................................................................
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test fddd-1.12 {load multiple minterms} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	set result {}
	for {set i 0} {$i < 3} {incr i} {
	    set j [expr {($i + 1) % 4}]







|







 







|













|













|







 







|







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
...
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
#
#       Tests for Finite Domain Decision Diagrams (FDDD's)
#
# Copyright (c) 2013 by Kevin B. Kenny.

package require tclbdd::fddd

test fddd-1.1 {load term - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys load
    }
    -cleanup {
................................................................................
	rename sys {}
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test fddd-1.2 {load term - bad integer} {*}{
    -setup {
	bdd::system create sys
    } 
    -body {
	sys load x {} garbage
    } 
    -cleanup {
	rename sys {}
    }
    -result {expected integer but got "garbage"}
    -returnCodes error
}

test fddd-1.3 {load term - ill-formed list} {
    -setup {
	bdd::system create sys
    }
    -body {
	sys load x \{ 
    }
    -cleanup {
	rename sys {}
    }
    -result {unmatched open brace in list}
    -returnCodes error
}

test fddd-1.4 {load term - wrong list size} {
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys load x {1 2}} result] $result $::errorCode
    }
    -cleanup {
................................................................................
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test fddd-1.12 {load multiple terms} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	set result {}
	for {set i 0} {$i < 3} {incr i} {
	    set j [expr {($i + 1) % 4}]