tclbdd

Check-in [74ad4ed7f0]
Login

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

Overview
Comment:Add test cases for low-level 'project' and fixed the bugs that were exposed
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:74ad4ed7f01d5adbdf30594fd8d4438a3ed03e8a
User & Date: kbk 2013-12-17 16:16:04
Context
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
15:53
Renamed the 'fdd' subpackage to 'fddd'. (Finite Domain Decision Diagram is correct.) Added the machinery to include it in the [package] mechanism. Added 'foreach_fullsat' to expand out truth tables for SAT terms, and added test cases for the same. Added 'fddd::support' method (no tests yet) to list the finite domain variables that appear in a query term. Added test cases for 'fddd::domain' and friends, and fixed the bugs that the test cases exposed. check-in: 80342a5576 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/tclBdd.c.

1809
1810
1811
1812
1813
1814
1815

1816

1817
1818
1819
1820
1821
1822
1823
....
1831
1832
1833
1834
1835
1836
1837









1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
				/* The number of args used in method dispatch */
    BDD_BeadIndex u;		/* Expression to quantify */
    int varc;			/* Number of variables to project away */
    Tcl_Obj** varv;		/* Indices of variables to project away */
    int vIndex;			/* Variable number from Tcl */
    BDD_VariableIndex* v;	/* Variables to quantify */
    BDD_BeadIndex result;	/* Result of the quantification */

    BDD_VariableIndex i;


    /* Check syntax */

    if (objc != skipped+3) {
	Tcl_WrongNumArgs(interp, skipped, objv, "name varList expr");
	return TCL_ERROR;
    }
................................................................................
    }
    v = ckalloc(varc * sizeof(BDD_VariableIndex));
    for (i = 0; i < varc; ++i) {
	if (Tcl_GetIntFromObj(interp, varv[i], &vIndex) != TCL_OK) {
	    ckfree(v);
	    return TCL_ERROR;
	}









	v[i] = (BDD_VariableIndex) vIndex;
	if (i > 0 && v[i] <= v[i-1]) {
	    Tcl_SetObjResult(interp, Tcl_NewStringObj("variables are not in "
						      "increasing order\n",
						      -1));
	    Tcl_SetErrorCode(interp, "BDD", "VarsOutOfOrder", NULL);
	    ckfree(v);
	    return TCL_ERROR;
	}
    }

    result =







>

>







 







>
>
>
>
>
>
>
>
>



|
<







1809
1810
1811
1812
1813
1814
1815
1816
1817
1818
1819
1820
1821
1822
1823
1824
1825
....
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
1852

1853
1854
1855
1856
1857
1858
1859
				/* The number of args used in method dispatch */
    BDD_BeadIndex u;		/* Expression to quantify */
    int varc;			/* Number of variables to project away */
    Tcl_Obj** varv;		/* Indices of variables to project away */
    int vIndex;			/* Variable number from Tcl */
    BDD_VariableIndex* v;	/* Variables to quantify */
    BDD_BeadIndex result;	/* Result of the quantification */
    Tcl_Obj* errorMessage;	/* Error message from this method */
    BDD_VariableIndex i;


    /* Check syntax */

    if (objc != skipped+3) {
	Tcl_WrongNumArgs(interp, skipped, objv, "name varList expr");
	return TCL_ERROR;
    }
................................................................................
    }
    v = ckalloc(varc * sizeof(BDD_VariableIndex));
    for (i = 0; i < varc; ++i) {
	if (Tcl_GetIntFromObj(interp, varv[i], &vIndex) != TCL_OK) {
	    ckfree(v);
	    return TCL_ERROR;
	}
	if (vIndex < 0) {
	    errorMessage =
		Tcl_ObjPrintf("expected nonnegative integer but got \"%s\"",
			      Tcl_GetString(varv[i]));
	    Tcl_SetObjResult(interp, errorMessage);
	    Tcl_SetErrorCode(interp, "BDD", "NegativeVarIndex", 
			     Tcl_GetString(varv[i]), NULL);
	    return TCL_ERROR;
	}
	v[i] = (BDD_VariableIndex) vIndex;
	if (i > 0 && v[i] <= v[i-1]) {
	    Tcl_SetObjResult(interp, Tcl_NewStringObj("variables are not in "
						      "increasing order", -1));

	    Tcl_SetErrorCode(interp, "BDD", "VarsOutOfOrder", NULL);
	    ckfree(v);
	    return TCL_ERROR;
	}
    }

    result =

Changes to tests/fddd.test.

354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375



























































































376
377
378
379
    -cleanup {
	rename rdr {}
	sys destroy
    }
    -result {{0 0 1 1 2 1 3 0} {0 1 1 0 2 1 3 1} {0 1 1 1 2 0 3 1} 2}
}

test fddd-5.1 {project - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys project
    }
    -cleanup {
	sys destroy
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}




























































































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







|














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




354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
    -cleanup {
	rename rdr {}
	sys destroy
    }
    -result {{0 0 1 1 2 1 3 0} {0 1 1 0 2 1 3 1} {0 1 1 1 2 0 3 1} 2}
}

test fddd-4.1 {project - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys project
    }
    -cleanup {
	sys destroy
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test fddd-4.2 {project - can't find expr} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys project x {} garbage} result] $result $::errorCode
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test fddd-4.3 {project - malformed list} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys project x \{ 1
    }
    -cleanup {
	sys destroy
    }
    -result {unmatched open brace in list}
    -returnCodes error
}

test fddd-4.4 {bad variable number} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys project x garbage 1
    }
    -cleanup {
	sys destroy
    }
    -result {expected integer but got "garbage"}
    -returnCodes error
}

test fddd-4.5 {bad variable number} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys project x {-2 -1} 1} result] $result $::errorCode
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected nonnegative integer but got "-2"} {BDD NegativeVarIndex -2}}
}

test fddd-4.6 {variable numbers out of sequence} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys project x {1 0} 1} result] $result $::errorCode
    }
    -cleanup {
	sys destroy
    }
    -result {1 {variables are not in increasing order} {BDD VarsOutOfOrder}}
}

test fddd-4.7 {project} {*}{
    -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 project ze {4 5} expr
	list [expr {[sys beadindex ze] == [sys beadindex ye]}] \
	    [sys unset ye ze term expr a b c d e f !e !f] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

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