tclbdd

Check-in [3194251647]
Login

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

Overview
Comment:Remove dribble from minterm loader. Fix variables-out-of-order check in minterm loader. Add minterm loader test vectors.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:3194251647b3003e2e7ad27e78f3f5e7fa590638
User & Date: kbk 2013-12-13 20:22:09
Context
2013-12-14
23:20
correct name of 'fdd' package to 'fddd'. Add 'project' method to bdd base code - no driver nor tests yet. check-in: 444573ad82 user: kbk tags: trunk
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
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/tclBdd.c.

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
....
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464

1465
1466
1467
1468
1469
1470
1471
....
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
	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
     */
................................................................................
	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);
................................................................................
	}

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







<


<





<
<










<
<




|







 







<
<
|







>







 







<
<
<



<
<
<







 







<
<






<




<







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
....
1442
1443
1444
1445
1446
1447
1448


1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
....
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
	return TCL_ERROR;
    }
    name = objv[skipped];

    /*
     * Get parameter values
     */

    paramv = ckalloc(paramc * sizeof(Tcl_WideInt));
    for (i = 0; i < paramc; ++i) {

	if (Tcl_GetWideIntFromObj(interp, objv[skipped+2+i],
				  paramv+i) != TCL_OK) {
	    ckfree(paramv);
	    return TCL_ERROR;
	}


    }

    /*
     * Unpack description
     */
    if (Tcl_ListObjGetElements(interp, objv[skipped+1],
			       &descc, &descv) != TCL_OK) {
	ckfree(paramv);
	return TCL_ERROR;
    }


    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
     */
................................................................................
	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);
................................................................................
	}

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

Added tests/fddd.test.

























































































































































































































































































































































































































>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
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
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
# bdd.test --
#
#       Tests for Finite Domain Decision Diagrams (FDDD's)
#
# Copyright (c) 2013 by Kevin B. Kenny.

package require tclbdd

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 {
	rename sys {}
    }
    -result {1 {description list must have a multiple of 3 elements} {BDD DescNotMultipleOf3}}
}

test fddd-1.5 {load - bad integer - also check bead leak} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {garbage 0 0 1 0 1} 0} result] \
	    $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test fddd-1.6 {load - bad integer - also check bead leak} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 garbage 0 1 0 1} 0} result] \
	    $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test fddd-1.7 {load - bad integer - also check bead leak} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 0 garbage 1 0 1} 0} result] \
	    $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test fddd-1.8 {load - nonincreasing var indices} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {1 0 0 1 0 1} 0} result] \
	    $result \
	    $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {variables are not in increasing order} {BDD VarsOutOfOrder} 2}
}

test fddd-1.9 {load - nonexistent param} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 1 0 1 0 1} 0} result] \
	    $result \
	    $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {description refers to a nonexistent parameter} {BDD NonexistentParam} 2}
}

test fddd-1.10 {load - bad bit index} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 0 65 1 0 1} 0} result] \
	    $result \
	    $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {bad bit index in description} {BDD BadBitIndex} 2}
}

test fddd-1.11 {load - do nothing gracefully} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys load x {}
	list [sys beadindex x] [sys unset x] [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test fdd-1.13 {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}]
	    sys load x {0 0 0 3 1 1 5 1 0 7 0 1} $i $j
	}
	sys foreach_sat s x {
	    lappend result $s
	}
	sys unset x
	lappend result [sys gc]
	set result
    }
    -cleanup {
	sys destroy
    }
    -result {{0 0 3 0 5 1 7 0} {0 0 3 1 5 1 7 1} {0 1 3 1 5 0 7 0} 2}
}

# Local Variables:
# mode: tcl
# c-basic-offset: 4
# End: