tclbdd

Check-in [1ff84c529c]
Login

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

Overview
Comment:Add test cases for Restrict and fix the bugs exposed thereby.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:1ff84c529c285c2e06471e6af8d3085faaaa1961
User & Date: kennykb 2013-12-01 01:09:08
Context
2013-12-01
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
01:09
Add test cases for Restrict and fix the bugs exposed thereby. check-in: 1ff84c529c user: kennykb tags: trunk
2013-11-30
17:50
remove dribble from bdd-12.13 check-in: 8f7b52fae4 user: kennykb tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/tclBdd.c.

918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
...
953
954
955
956
957
958
959
960
961
962
963
964

965
966
967
968
969
970
971
972
973
974
975
				/* 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 expr;		/* The expression to restrict */
    BDD_VariableIndex nRestrictions;
				/* How many restrictions? */
    BDD_ValueAssignment* restrictions;
    int i;
    BDD_VariableIndex j;
    BDD_BeadIndex literalIndex;
    Tcl_Obj* errorMessage;
    BDD_BeadIndex result;
    
    /* Check syntax */
................................................................................
		return TCL_ERROR;
	    }
	    if (!BDD_Literal(sdata->system, literalIndex, restrictions+j)) {
		errorMessage = Tcl_ObjPrintf("%s is not a literal",
					     Tcl_GetString(objv[i]));
		Tcl_SetObjResult(interp, errorMessage);
		Tcl_SetErrorCode(interp, "BDD", "NotLiteral",
				 Tcl_GetString(objv[i]));
		ckfree(restrictions);
		return TCL_ERROR;
	    }
	}

	result = BDD_Restrict(sdata->system, expr, restrictions, nRestrictions);
	SetNamedExpression(sdata, objv[skipped], result);
	BDD_UnrefBead(sdata->system, result);
    }
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemSatcountMethod --







|

|







 







|




>
|
|
|
<







918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
...
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968

969
970
971
972
973
974
975
				/* 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 expr;		/* The expression to restrict */
    BDD_VariableIndex nRestrictions = 0;
				/* How many restrictions? */
    BDD_ValueAssignment* restrictions = NULL;
    int i;
    BDD_VariableIndex j;
    BDD_BeadIndex literalIndex;
    Tcl_Obj* errorMessage;
    BDD_BeadIndex result;
    
    /* Check syntax */
................................................................................
		return TCL_ERROR;
	    }
	    if (!BDD_Literal(sdata->system, literalIndex, restrictions+j)) {
		errorMessage = Tcl_ObjPrintf("%s is not a literal",
					     Tcl_GetString(objv[i]));
		Tcl_SetObjResult(interp, errorMessage);
		Tcl_SetErrorCode(interp, "BDD", "NotLiteral",
				 Tcl_GetString(objv[i]), NULL);
		ckfree(restrictions);
		return TCL_ERROR;
	    }
	}
    }
    result = BDD_Restrict(sdata->system, expr, restrictions, nRestrictions);
    SetNamedExpression(sdata, objv[skipped], result);
    BDD_UnrefBead(sdata->system, result);

    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemSatcountMethod --

Changes to tests/bdd.test.

988
989
990
991
992
993
994






995












































































































996
997
998
999
1000
1001
1002
1003
....
1008
1009
1010
1011
1012
1013
1014


































1015
1016
1017
1018
1019
1020
1021
	list [expr {[sys beadindex co] == [sys beadindex spec_co]}] \
	    [expr {[sys beadindex z] == [sys beadindex spec_z]}]
    }
    -cleanup {rename sys {}}
    -result {1 1}
}
		



















































































































test bdd-13.n {restrict - reduce to constant} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
    }
    -body {
................................................................................
	sys beadindex r2
    }
    -cleanup {
	rename sys {}
    }
    -result 1
}



































cleanupTests
return

# Local Variables:
# mode: tcl
# End:







>
>
>
>
>
>
|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|







 







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







988
989
990
991
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
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
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
....
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
	list [expr {[sys beadindex co] == [sys beadindex spec_co]}] \
	    [expr {[sys beadindex z] == [sys beadindex spec_z]}]
    }
    -cleanup {rename sys {}}
    -result {1 1}
}
		
test bdd-13.1 {restrict - wrong # args} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
    }
    -body {
	sys restrict r1
    }
    -cleanup {
	rename sys {}
    }
    -returnCodes error
    -match glob
    -result {wrong # args: *}
}

test bdd-13.2 {restrict - can't find expr to restrict} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
    }
    -body {list [catch {sys restrict r1 garbage} result] $result $::errorCode}
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-13.3 {restrict - can't find second expression} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {list [catch {sys restrict r1 r2 garbage} result] \
	       $result $::errorCode}
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-13.4 {restrict - not a literal} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {list [catch {sys restrict r1 c r2} result] \
	       $result $::errorCode}
    -cleanup {rename sys {}}
    -result \
	{1 {r2 is not a literal} {BDD NotLiteral r2}}
}

test bdd-13.5 {restrict - do nothing gracefully} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2
	expr {[sys beadindex r1] == [sys beadindex r2]}
    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-13.6 {restrict by literal} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2 !b
	sys ^ r3 a c 
	expr {[sys beadindex r1] == [sys beadindex r3]}
    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-13.7 {restrict by two literals} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2 a c
	expr {[sys beadindex r1] == [sys beadindex b]}
    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-13.8 {restrict - reduce to constant} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
    }
    -body {
................................................................................
	sys beadindex r2
    }
    -cleanup {
	rename sys {}
    }
    -result 1
}

test bdd-13.10 {restrict zero} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 0 a c
	sys beadindex r1
    }
    -cleanup {rename sys {}}
    -result 0
}

test bdd-13.11 {restrict one} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 1 a c
	sys beadindex r1
    }
    -cleanup {rename sys {}}
    -result 1
}

cleanupTests
return

# Local Variables:
# mode: tcl
# End: