tclbdd

Check-in [f7a47671e9]
Login

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

Overview
Comment:Added ===, tautology, satisfiable methods (no tests yet). Replaced 'constant' and 'copy' with a single ':=' method.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:f7a47671e987522b20074340a26eef2efc5fed97
User & Date: kennykb 2013-12-01 23:26:26
Context
2013-12-01
23:27
Removed pure-Tcl superclass for bdd: not sure where I was going with that. check-in: af2be65f95 user: kennykb tags: trunk
23:26
Added ===, tautology, satisfiable methods (no tests yet). Replaced 'constant' and 'copy' with a single ':=' method. check-in: f7a47671e9 user: kennykb tags: trunk
23:14
Implemented foreach_sat (no tests yet). Fixed a bug where restrict cannot handle variables out of sequence, and added a test case for same. Made the 8-queens example use foreach_sat to enumerate the solutions. check-in: 5b78565cad user: kennykb tags: trunk
Changes
Hide Diffs Unified Diffs Show Whitespace Changes Patch

Changes to generic/tclBdd.c.

100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
...
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
...
245
246
247
248
249
250
251

252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
...
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
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
static void DeletePerInterpData(PerInterpData*);
static int BddSystemConstructor(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int BddSystemBeadindexMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				    int, Tcl_Obj* const[]);
static int BddSystemBinopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int BddSystemConstantMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemCopyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
			       int, Tcl_Obj* const[]);
static int BddSystemDumpMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
			       int, Tcl_Obj* const[]);
static int BddSystemForeachSatMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				     int, Tcl_Obj *const[]);
static int ForeachSatPre(Tcl_Interp* interp, BddSystemData*,
................................................................................
const static Tcl_MethodType BddSystemBinopMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "binop",			   /* name */
    BddSystemBinopMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};				   /* common to all ten binary operators */
const static Tcl_MethodType BddSystemConstantMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "constant",			   /* name */
    BddSystemConstantMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemCopyMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "copy",			   /* name */
    BddSystemCopyMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
................................................................................
/*
 * Method table for the BDD system object
 */

MethodTableRow systemMethodTable[] = {
    { "!=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NE },
    { "&",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_AND },

    { "<",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LT },
    { "<=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LE },
    { "==",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_EQ },
    { ">",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GT },
    { ">=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GE },
    { "^",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_XOR },
    { "beadindex", &BddSystemBeadindexMethodType, NULL },
    { "constant",  &BddSystemConstantMethodType,  NULL },
    { "copy",      &BddSystemCopyMethodType,      NULL },
    { "dump",      &BddSystemDumpMethodType,      NULL },
    { "foreach_sat",
                   &BddSystemForeachSatMethodType,NULL },
    { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
................................................................................
    }
    beadIndexResult = BDD_Apply(sdata->system, (BDD_BinOp) (size_t)clientData,
				beadIndexOpd1, beadIndexOpd2);
    SetNamedExpression(sdata, objv[skipped], beadIndexResult);
    BDD_UnrefBead(sdata->system, beadIndexResult);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemConstantMethod --
 *
 *	Computes a constant expression in a system of BDD's and assigns
 *	it a name
 *
 * Usage:
 *	$system constant name value
 *
 * Parameters:
 *	name - The name to assign
 *	value - The Boolean value to give it
 *
 * Results:
 *	None
 *
 * Side effects:
 *	Assigns the given value to the name
 *
 *-----------------------------------------------------------------------------
 */

static int
BddSystemConstantMethod(
    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 */
    int boolval;		/* Boolean value */

    /* Check syntax */

    if (objc != skipped+2) {
	Tcl_WrongNumArgs(interp, skipped, objv, "name value");
	return TCL_ERROR;
    }
    if (Tcl_GetBooleanFromObj(interp, objv[skipped+1], &boolval) != TCL_OK) {
	return TCL_ERROR;
    }
    SetNamedExpression(sdata, objv[skipped], (BDD_BeadIndex) boolval);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemCopyMethod --
 *
 *	Copies a named expression in a system of BDD's and assigns







<
<







 







<
<
<
<
<
<
<







 







>







<
<







 







<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<







100
101
102
103
104
105
106


107
108
109
110
111
112
113
...
165
166
167
168
169
170
171







172
173
174
175
176
177
178
...
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250


251
252
253
254
255
256
257
...
543
544
545
546
547
548
549






















































550
551
552
553
554
555
556
static void DeletePerInterpData(PerInterpData*);
static int BddSystemConstructor(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int BddSystemBeadindexMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				    int, Tcl_Obj* const[]);
static int BddSystemBinopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);


static int BddSystemCopyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
			       int, Tcl_Obj* const[]);
static int BddSystemDumpMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
			       int, Tcl_Obj* const[]);
static int BddSystemForeachSatMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				     int, Tcl_Obj *const[]);
static int ForeachSatPre(Tcl_Interp* interp, BddSystemData*,
................................................................................
const static Tcl_MethodType BddSystemBinopMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "binop",			   /* name */
    BddSystemBinopMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};				   /* common to all ten binary operators */







const static Tcl_MethodType BddSystemCopyMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "copy",			   /* name */
    BddSystemCopyMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
................................................................................
/*
 * Method table for the BDD system object
 */

MethodTableRow systemMethodTable[] = {
    { "!=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NE },
    { "&",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_AND },
    { ":=",        &BddSystemCopyMethodType,      NULL },
    { "<",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LT },
    { "<=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LE },
    { "==",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_EQ },
    { ">",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GT },
    { ">=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GE },
    { "^",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_XOR },
    { "beadindex", &BddSystemBeadindexMethodType, NULL },


    { "dump",      &BddSystemDumpMethodType,      NULL },
    { "foreach_sat",
                   &BddSystemForeachSatMethodType,NULL },
    { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
................................................................................
    }
    beadIndexResult = BDD_Apply(sdata->system, (BDD_BinOp) (size_t)clientData,
				beadIndexOpd1, beadIndexOpd2);
    SetNamedExpression(sdata, objv[skipped], beadIndexResult);
    BDD_UnrefBead(sdata->system, beadIndexResult);
    return TCL_OK;
}






















































 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemCopyMethod --
 *
 *	Copies a named expression in a system of BDD's and assigns

Changes to library/tclbdd.tcl.

10
11
12
13
14
15
16
17
18
19
20
21
22


23







#------------------------------------------------------------------------------

namespace eval bdd {
    namespace export system
}

oo::class create bdd::SystemInt {
    variable beadseq
    constructor args {
    }
}
oo::class create bdd::system {
    superclass ::bdd::SystemInt


}














<





>
>
|
>
>
>
>
>
>
>
10
11
12
13
14
15
16

17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
#------------------------------------------------------------------------------

namespace eval bdd {
    namespace export system
}

oo::class create bdd::SystemInt {

    constructor args {
    }
}
oo::class create bdd::system {
    superclass ::bdd::SystemInt
    method === {exprName1 exprName2} {
	expr {[my beadindex $exprName1] == [my beadindex exprName2]}
    }
    method satisfiable {exprName} {
	expr {[my beadindex $exprName] != 0}
    }
    method tautology {exprName} {
	expr {[my beadindex $exprname] == 1}
    }
}

Changes to tests/bdd.test.

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
...
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
....
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
....
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
....
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
    -setup {bdd::system create sys}
    -body {list [catch {sys beadindex garbage} result] $result $::errorCode}
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-3.1 {constant - wrong # args} {*}{
    -setup {bdd::system create sys}
    -body {sys constant}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
    -result {wrong # args: *}
}

test bdd-3.2 {constant - bad value} {*}{
    -setup {bdd::system create sys}
    -body {sys constant rubbish garbage}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
    -result {expected boolean value but got "garbage"}
}

test bdd-3.3 {constant 0} {*}{
    -setup {bdd::system create sys}
    -body {sys constant zero false; sys beadindex zero}
    -cleanup {rename sys {}}
    -result 0
}

test bdd-3.4 {constant 1} {*}{
    -setup {bdd::system create sys}
    -body {sys constant one true; sys beadindex one}
    -cleanup {rename sys {}}
    -result 1
}

test bdd-4.1 {copy - wrong # args} {*}{
    -setup {bdd::system create sys; sys constant one true}
    -body {sys copy}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
    -result {wrong # args: *}
}

test bdd-4.2 {copy - can't find expr} {*}{
    -setup {bdd::system create sys; sys constant one true}
    -body {list [catch {sys copy yes garbage} result] $result $::errorCode}
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-4.3 {copy} {*}{
    -setup {bdd::system create sys; sys constant one true}
    -body {sys copy yes one; sys beadindex yes}
    -cleanup {rename sys {}}
    -result 1
}

test bdd-5.1 {dump - wrong # args} {*}{
    -setup {bdd::system create sys}
    -body {sys dump}
................................................................................
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 128} {incr i} {
	    sys nthvar v$i $i
	}
    }
    -body {
	sys copy r0 0
	for {set i 0} {$i < 128} {incr i 2} {
	    sys ^ r0 r0 v$i
	}
	for {set i 1} {$i < 128} {incr i 2} {
	    sys ^ r0 r0 v$i
	}
	list [dict size [sys dump r0]] [format %llx [sys satcount r0]]
................................................................................
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 64} {incr i} {
	    sys nthvar v$i $i; sys notnthvar !v$i $i
	}
    }
    -body {
	sys copy solution 1

	# iterate through the cells

	for {set row 0} {$row < 8} {incr row} {
	    sys copy thisRowC 1
	    for {set col 7} {$col >= 0} {incr col -1} {
		sys copy cellC 1
		set q1 v[expr {8* $row + $col}]

		# queen here <= no other queen in the same column

		sys copy columnC 1
		for {set col2 7} {$col2 >= 0} {incr col2 -1} {
		    if {$col2 != $col} {
			set q2 v[expr {8 * $row + $col2}]
			sys & columnC columnC !$q2
		    }
		}
		sys <= columnC $q1 columnC
		sys & cellC cellC columnC
		
		# queen here <= no other queen in the same row

		sys copy rowC 1
		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
		    if {$row2 != $row} {
			set q2 v[expr {8 * $row2 + $col}]
			sys & rowC rowC !$q2
		    }
		}
		sys <= rowC $q1 rowC
		sys & cellC cellC rowC

		# queen here <= no other queen in the same diagonal

		sys copy diag1C 1
		sys copy diag2C 1
		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
		    if {$row2 != $row} {
			set col2 [expr {$col + $row2 - $row}]
			if {$col2 >= 0 && $col2 < 8} {
			    set q2 v[expr {8 * $row2 + $col2}]
			    sys & diag1C diag1C !$q2
			}
................................................................................
	    # accumulate all constraints for a row into the solution

	    sys & solution solution thisRowC
	}
		
	# at least one queen in each column
	for {set col 0} {$col < 8} {incr col} {
	    sys copy columnC 0
	    for {set row 0} {$row < 8} {incr row} {
		set q v[expr {8*$row + $col}]
		sys | columnC columnC $q
	    }
	    sys & solution solution columnC
	}
	sys foreach_sat A solution {
................................................................................
	sys nthvar x 0; sys notnthvar !x 0
	sys nthvar y 1; sys notnthvar !y 1
	sys nthvar ci 2; sys notnthvar !ci 2
    }
    -body {

	# specification is a truth table
	sys copy spec_co 0
	sys copy spec_z 0
	foreach {x y ci co z} {
	    0 0 0 0 0
	    0 0 1 0 1
	    0 1 0 0 1
	    0 1 1 1 0

	    1 0 0 0 1







|

|






<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
|
|
|





|
|
|







 







|







 







|




|

|




|











|











|
|







 







|







 







|
|







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
...
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
...
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
....
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
....
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
    -setup {bdd::system create sys}
    -body {list [catch {sys beadindex garbage} result] $result $::errorCode}
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

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

































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

test bdd-4.3 {:=} {*}{
    -setup {bdd::system create sys}
    -body {sys := yes 1; sys beadindex yes}
    -cleanup {rename sys {}}
    -result 1
}

test bdd-5.1 {dump - wrong # args} {*}{
    -setup {bdd::system create sys}
    -body {sys dump}
................................................................................
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 128} {incr i} {
	    sys nthvar v$i $i
	}
    }
    -body {
	sys := r0 0
	for {set i 0} {$i < 128} {incr i 2} {
	    sys ^ r0 r0 v$i
	}
	for {set i 1} {$i < 128} {incr i 2} {
	    sys ^ r0 r0 v$i
	}
	list [dict size [sys dump r0]] [format %llx [sys satcount r0]]
................................................................................
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 64} {incr i} {
	    sys nthvar v$i $i; sys notnthvar !v$i $i
	}
    }
    -body {
	sys := solution 1

	# iterate through the cells

	for {set row 0} {$row < 8} {incr row} {
	    sys := thisRowC 1
	    for {set col 7} {$col >= 0} {incr col -1} {
		sys := cellC 1
		set q1 v[expr {8* $row + $col}]

		# queen here <= no other queen in the same column

		sys := columnC 1
		for {set col2 7} {$col2 >= 0} {incr col2 -1} {
		    if {$col2 != $col} {
			set q2 v[expr {8 * $row + $col2}]
			sys & columnC columnC !$q2
		    }
		}
		sys <= columnC $q1 columnC
		sys & cellC cellC columnC
		
		# queen here <= no other queen in the same row

		sys := rowC 1
		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
		    if {$row2 != $row} {
			set q2 v[expr {8 * $row2 + $col}]
			sys & rowC rowC !$q2
		    }
		}
		sys <= rowC $q1 rowC
		sys & cellC cellC rowC

		# queen here <= no other queen in the same diagonal

		sys := diag1C 1
		sys := diag2C 1
		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
		    if {$row2 != $row} {
			set col2 [expr {$col + $row2 - $row}]
			if {$col2 >= 0 && $col2 < 8} {
			    set q2 v[expr {8 * $row2 + $col2}]
			    sys & diag1C diag1C !$q2
			}
................................................................................
	    # accumulate all constraints for a row into the solution

	    sys & solution solution thisRowC
	}
		
	# at least one queen in each column
	for {set col 0} {$col < 8} {incr col} {
	    sys := columnC 0
	    for {set row 0} {$row < 8} {incr row} {
		set q v[expr {8*$row + $col}]
		sys | columnC columnC $q
	    }
	    sys & solution solution columnC
	}
	sys foreach_sat A solution {
................................................................................
	sys nthvar x 0; sys notnthvar !x 0
	sys nthvar y 1; sys notnthvar !y 1
	sys nthvar ci 2; sys notnthvar !ci 2
    }
    -body {

	# specification is a truth table
	sys := spec_co 0
	sys := spec_z 0
	foreach {x y ci co z} {
	    0 0 0 0 0
	    0 0 1 0 1
	    0 1 0 0 1
	    0 1 1 1 0

	    1 0 0 0 1