tclbdd

Check-in [db99db21ba]
Login

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

Overview
Comment:Added 'replace' method to bdd::system in support of relational algebra. Fixed a typo in '===' method that caused it to fail always
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:db99db21baffc83eb5d4a94237e6aec7d7e595da
User & Date: kbk 2013-12-18 16:06:37
Context
2013-12-18
18:54
Make finite domain descriptions contain inverted lists of the variable numbers for each column. check-in: 8077309f9f user: kbk tags: trunk
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
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/tclBdd.c.

148
149
150
151
152
153
154


155
156
157
158
159
160
161
...
291
292
293
294
295
296
297







298
299
300
301
302
303
304
...
371
372
373
374
375
376
377

378
379
380
381
382
383
384
....
1773
1774
1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
....
1963
1964
1965
1966
1967
1968
1969




















































































































































1970
1971
1972
1973
1974
1975
1976
				 int, Tcl_Obj* const[]);
static int BddSystemProfileMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				  int, Tcl_Obj* const[]);
static int BddSystemProjectMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				  int, Tcl_Obj* const[]);
static int BddSystemQuantifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);


static int BddSystemRestrictMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemSatcountMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemSimplifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemTernopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
................................................................................
};
const static Tcl_MethodType BddSystemQuantifyMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "quantify",			   /* name */
    BddSystemQuantifyMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */







};
const static Tcl_MethodType BddSystemRestrictMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "restrict",			   /* name */
    BddSystemRestrictMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
................................................................................
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "nor3",      &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
    { "oneof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_ONEOF },
    { "profile",   &BddSystemProfileMethodType,   NULL },
    { "project",   &BddSystemProjectMethodType,   NULL },

    { "restrict",  &BddSystemRestrictMethodType,  NULL },
    { "satcount",  &BddSystemSatcountMethodType,  NULL },
    { "simplify",  &BddSystemSimplifyMethodType,  NULL },
    { "twoof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_TWOOF },
    { "unset",     &BddSystemUnsetMethodType,     NULL },
    { "|",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_OR },
    { "|3",        &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_OR },
................................................................................
 *
 * Usage:
 *	$system project result vars expr
 *
 * Parameters:
 *	system - System of BDD's
 *	result - Name of a BDD that will receive the result
 *	var - List of integers giving positions of variables to project away.
 *	expr - Expression to simplify
 *
 * Results:
 *	Returns a standard Tcl result
 *
 * Side effects:
 *	Creates the named expression if successful
................................................................................
    result = BDD_Quantify(sdata->system, q, varc, v, u);

    ckfree(v);
    SetNamedExpression(sdata, objv[skipped], result);
    BDD_UnrefBead(sdata->system, result);
    return TCL_OK;
}




















































































































































 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemRestrictMethod --
 *
 *	Computes a BDD restricted to a particular set of variable values







>
>







 







>
>
>
>
>
>
>







 







>







 







|







 







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







148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
...
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
...
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
....
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
....
1973
1974
1975
1976
1977
1978
1979
1980
1981
1982
1983
1984
1985
1986
1987
1988
1989
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
2024
2025
2026
2027
2028
2029
2030
2031
2032
2033
2034
2035
2036
2037
2038
2039
2040
2041
2042
2043
2044
2045
2046
2047
2048
2049
2050
2051
2052
2053
2054
2055
2056
2057
2058
2059
2060
2061
2062
2063
2064
2065
2066
2067
2068
2069
2070
2071
2072
2073
2074
2075
2076
2077
2078
2079
2080
2081
2082
2083
2084
2085
2086
2087
2088
2089
2090
2091
2092
2093
2094
2095
2096
2097
2098
2099
2100
2101
2102
2103
2104
2105
2106
2107
2108
2109
2110
2111
2112
2113
2114
2115
2116
2117
2118
2119
2120
2121
2122
2123
2124
2125
2126
2127
2128
2129
2130
2131
2132
2133
2134
				 int, Tcl_Obj* const[]);
static int BddSystemProfileMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				  int, Tcl_Obj* const[]);
static int BddSystemProjectMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				  int, Tcl_Obj* const[]);
static int BddSystemQuantifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemReplaceMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				  int, Tcl_Obj* const[]);
static int BddSystemRestrictMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemSatcountMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemSimplifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemTernopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
................................................................................
};
const static Tcl_MethodType BddSystemQuantifyMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "quantify",			   /* name */
    BddSystemQuantifyMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemReplaceMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "replace",			   /* name */
    BddSystemReplaceMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemRestrictMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "restrict",			   /* name */
    BddSystemRestrictMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
................................................................................
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "nor3",      &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
    { "oneof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_ONEOF },
    { "profile",   &BddSystemProfileMethodType,   NULL },
    { "project",   &BddSystemProjectMethodType,   NULL },
    { "replace",   &BddSystemReplaceMethodType,   NULL },
    { "restrict",  &BddSystemRestrictMethodType,  NULL },
    { "satcount",  &BddSystemSatcountMethodType,  NULL },
    { "simplify",  &BddSystemSimplifyMethodType,  NULL },
    { "twoof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_TWOOF },
    { "unset",     &BddSystemUnsetMethodType,     NULL },
    { "|",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_OR },
    { "|3",        &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_OR },
................................................................................
 *
 * Usage:
 *	$system project result vars expr
 *
 * Parameters:
 *	system - System of BDD's
 *	result - Name of a BDD that will receive the result
 *	vars - List of integers giving positions of variables to project away.
 *	expr - Expression to simplify
 *
 * Results:
 *	Returns a standard Tcl result
 *
 * Side effects:
 *	Creates the named expression if successful
................................................................................
    result = BDD_Quantify(sdata->system, q, varc, v, u);

    ckfree(v);
    SetNamedExpression(sdata, objv[skipped], result);
    BDD_UnrefBead(sdata->system, result);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemReplaceMethod --
 *
 *	Replaces a set of variables in a BDD with other variables.
 *
 * Usage:
 *	$system project result vars vars2 expr
 *
 * Parameters:
 *	system - System of BDD's
 *	result - Name of a BDD that will receive the result
 *	vars - List of integers giving positions of variables to replace
 *	vars2 - List of integers giving positions of variables that will
 *              replace vars. The two lists must have the same length.
 *	expr - Expression to rewrite
 *
 * Results:
 *	Returns a standard Tcl result
 *
 * Side effects:
 *	Creates the named expression if successful
 *
 * This is the same operation as existential quantification. It is provided
 * for the convenience of Finite Domain Decision Diagrams, where it exists
 * as the relational 'project' operator.
 *
 *-----------------------------------------------------------------------------
 */
static int
BddSystemReplaceMethod(
    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 */
    BDD_BeadIndex u;		/* Expression to quantify */
    int varc;			/* Number of variables to replace */
    Tcl_Obj** varv;		/* Indices of variables to replace */
    int vIndex;			/* Variable number from Tcl */
    int var2c;			/* Number of replacement variables */
    Tcl_Obj** var2v;		/* Indices of replacement variables */
    int v2Index;		/* Variable number of a replacement */
    BDD_VariableIndex totalv;	/* Number of variables in the BDD system */
    BDD_VariableIndex replacedv = 0;
				/* Count of variables that have replacements */
    BDD_BeadIndex* replacements;/* Description of the variable replacement
				 * to be performed. */
    BDD_BeadIndex result;	/* Result of the quantification */
    Tcl_Obj* errorMessage;	/* Error message from this method */
    int retval = TCL_ERROR;	/* Return value from this method */
    BDD_VariableIndex i;


    /* Check syntax */

    if (objc != skipped+4) {
	Tcl_WrongNumArgs(interp, skipped, objv, "name vars vars2 expr");
	return TCL_ERROR;
    }
    if (FindNamedExpression(interp, sdata, objv[skipped+3],
			    &u) != TCL_OK
	|| Tcl_ListObjGetElements(interp, objv[skipped+1],
				  &varc, &varv) != TCL_OK
	|| Tcl_ListObjGetElements(interp, objv[skipped+2],
				  &var2c, &var2v) != TCL_OK) {
	return TCL_ERROR;
    }
    if (varc != var2c) {
	Tcl_SetObjResult(interp, Tcl_NewStringObj("variable list and "
						  "replacement list have "
						  "different lengths", -1));
	Tcl_SetErrorCode(interp, "BDD", "WrongListLengths", NULL);
	return TCL_ERROR;
    }

    /*
     * Allocate space for replacement description, and initialize the
     * description to replace all variables with themselves.
     */

    totalv = BDD_GetVariableCount(sdata->system);
    replacements = ckalloc(totalv * sizeof(BDD_BeadIndex));
    for (i = 0; i < totalv; ++i) {
	replacements[i] = BDD_MakeBead(sdata->system, i, 0, 1);
    }

    for (i = 0; i < varc; ++i) {
	if (Tcl_GetIntFromObj(interp, varv[i], &vIndex) != TCL_OK
	    || Tcl_GetIntFromObj(interp, var2v[i], &v2Index) != TCL_OK) {
	    goto cleanup;
	}
	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);
	    goto cleanup;
	}
	if (v2Index < 0) {
	    errorMessage =
		Tcl_ObjPrintf("expected nonnegative integer but got \"%s\"",
			      Tcl_GetString(var2v[i]));
	    Tcl_SetObjResult(interp, errorMessage);
	    Tcl_SetErrorCode(interp, "BDD", "NegativeVarIndex", 
			     Tcl_GetString(var2v[i]), NULL);
	    goto cleanup;
	}
	if (vIndex >= totalv) {
	    /*
	     * Silently ignore requests to replace a nonexistent variable
	     */
	    continue;
	}
	
	result = BDD_MakeBead(sdata->system, (BDD_VariableIndex) v2Index,
			      0, 1);
	BDD_UnrefBead(sdata->system, replacements[vIndex]);
	replacements[vIndex] = result;
	if (vIndex >= replacedv) {
	    replacedv = vIndex + 1;
	}
    }

    retval = TCL_OK;
    result = BDD_Compose(sdata->system, u, replacedv, replacements);
    SetNamedExpression(sdata, objv[skipped], result);
    BDD_UnrefBead(sdata->system, result);

 cleanup:
    for (i = 0; i < totalv; ++i) {
	BDD_UnrefBead(sdata->system, replacements[i]);
    }
    ckfree(replacements);
    return retval;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemRestrictMethod --
 *
 *	Computes a BDD restricted to a particular set of variable values

Changes to library/tclbdd.tcl.

61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
    # inputs if and only if they are identical.
    #
    # This method is distinguished from == in that == returns a BDD
    # specifying the conditions under which two BDDs give the same
    # output, while === tests whether they give the same output always.

    method === {exprName1 exprName2} {
	expr {[my beadindex $exprName1] == [my beadindex exprName2]}
    }
    export ===

    # Method: satisfiable
    #
    #	Determines whether a BDD representing a Boolean formula is satisfiable
    #







|







61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
    # inputs if and only if they are identical.
    #
    # This method is distinguished from == in that == returns a BDD
    # specifying the conditions under which two BDDs give the same
    # output, while === tests whether they give the same output always.

    method === {exprName1 exprName2} {
	expr {[my beadindex $exprName1] == [my beadindex $exprName2]}
    }
    export ===

    # Method: satisfiable
    #
    #	Determines whether a BDD representing a Boolean formula is satisfiable
    #

Changes to tests/fddd.test.

459
460
461
462
463
464
465
466




































































































































467
468
469
470
	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:








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




459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
	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}
}

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

test fddd-5.2 {replace - missing expression} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys replace y {} {} garbage} result] $result $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expression named "garbage" not found} {BDD ExprNotFound garbage} 2}
}

test fddd-5.3 {replace - malformed first list} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys replace y \{ {} 0} result] $result [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {unmatched open brace in list} 2}
}

test fddd-5.4 {replace - malformed second list} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys replace y {} \{ 0} result] $result [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {unmatched open brace in list} 2}
}

test fddd-5.5 {replace - different list lengths} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys replace y {} {1} 0} result] $result $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {variable list and replacement list have different lengths} {BDD WrongListLengths} 2}
}

test fddd-5.6 {replace - bad integer in first list} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys replace y garbage 0 0} result] $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test fddd-5.7 {replace - bad integer in second list} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys replace y 0 garbage 0} result] $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test fddd-5.8 {replace - nonexistent var to replace} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys < c a b
    }
    -body {
	sys replace y 7 0 c
	list [sys === y c] [sys unset a b c y] [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test fddd-5.9 {replace} {
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys < c a b
	sys > d a b
    }
    -body {
	sys replace y {1 0} {0 1} c
	list [sys === y d] [sys unset a b c d y] [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

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