tclbdd

Check-in [b18569e814]
Login

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

Overview
Comment:Added tests for 'satisfiable'
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:b18569e814ab7e602a964f268c5ebc690452a7c8
User & Date: kbk 2013-12-21 17:52:08
Context
2013-12-21
21:51
Regularize and streamling FDDD database API. Begin commenting the FDDD database methods. check-in: baa39949c5 user: kbk tags: trunk
17:52
Added tests for 'satisfiable' check-in: b18569e814 user: kbk tags: trunk
17:47
Added tests for the convenience methods '===', 'tautology', 'support', 'beadcount' and fixed the bugs revealed. check-in: e6c6de79de user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to tests/bdd.test.

2940
2941
2942
2943
2944
2945
2946














































2947
2948
2949
2950
2951
2952
2953
2954
....
2955
2956
2957
2958
2959
2960
2961
2962
2963
2964
2965
2966
2967
2968
2969
2970
2971
2972
2973
2974
2975
2976
2977
2978
2979
2980
2981
2982
2983
....
2995
2996
2997
2998
2999
3000
3001
3002
3003
3004
3005
3006
3007
3008
3009
....
3010
3011
3012
3013
3014
3015
3016
3017
3018
3019
3020
3021
3022
3023
3024
3025
3026
3027
3028
3029
3030
3031
3032
3033
3034
3035
3036
3037
3038
....
3051
3052
3053
3054
3055
3056
3057
3058
3059
3060
3061
3062
3063
3064
3065
....
3066
3067
3068
3069
3070
3071
3072
3073
3074
3075
3076
3077
3078
3079
3080
....
3087
3088
3089
3090
3091
3092
3093
3094
3095
3096
3097
3098
3099
3100
3101
....
3105
3106
3107
3108
3109
3110
3111
3112
3113
3114
3115
3116
3117
3118
3119
....
3123
3124
3125
3126
3127
3128
3129
3130
3131
3132
3133
3134
3135
3136
3137
    }
    -cleanup {
	rename sys {}
    }
    -result {0 1 0 0 {} 2}
}















































test bdd-32.1 {support - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys support
    }
    -cleanup {
................................................................................
	sys destroy
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test bdd-32.2 {support - bad expr} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys support garbage} result] $result $::errorCode
    }
    -cleanup {
	sys destroy
    }
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-32.3 {support} {*}{
    -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 ^ d a b
	sys ^ e a c
................................................................................
    }
    -cleanup {
	rename sys {}
    }
    -result {{} {} 0 0 1 1 2 2 {0 1} {0 2} {1 2} {0 1 2} {} 2}
}

test bdd-33.1 {beadcount - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys beadcount
    }
    -cleanup {
................................................................................
	sys destroy
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test bdd-33.2 {beadcount - bad expr} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys beadcount garbage} result] $result $::errorCode
    }
    -cleanup {
	sys destroy
    }
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-33.3 {beadcount} {*}{
    -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 ^ d a b
	sys ^ e a c
................................................................................
    }
    -cleanup {
	rename sys {}
    }
    -result {0 0 1 1 1 1 1 1 3 3 3 5 {} 2}
}

test bdd-34.1 {foreach_fullsat} {*}{
    -body {
	set result {}
	bdd::foreach_fullsat s {6 3 0 7 4 1} {1 0 3 1 6 0 7 0} {
	    set val 0
	    foreach bit $s {
		set val [expr {($val << 1) | $bit}]
	    }
................................................................................
	    lappend result [expr {$val & 0x7}] [expr {$val >> 3}]
	}
	set result
    }
    -result {0 2 2 2 0 3 2 3}
}

test bdd-34.2 {foreach_fullsat - return} {*}{
    -setup {
	proc x {} {
	    bdd::foreach_fullsat s {6 3 0 7 4 1} {1 0 3 1 6 0 7 0} {
		set val 0
		foreach bit $s {
		    set val [expr {($val << 1) | $bit}]
		}
................................................................................
    }
    -cleanup {
	rename x {}
    }
    -result {0 2}
}

test bdd-34.3 {foreach_fullsat - break} {*}{
    -body {
	set result {}
	bdd::foreach_fullsat s {6 3 0 7 4 1} {1 0 3 1 6 0 7 0} {
	    set val 0
	    foreach bit $s {
		set val [expr {($val << 1) | $bit}]
	    }
................................................................................
	    lappend result [expr {$val & 0x7}] [expr {$val >> 3}]
	}
	set result
    }
    -result {0 2 2 2}
}

test bdd-34.4 {foreach_fullsat - continue} {*}{
    -body {
	set result {}
	bdd::foreach_fullsat s {6 3 0 7 4 1} {1 0 3 1 6 0 7 0} {
	    set val 0
	    foreach bit $s {
		set val [expr {($val << 1) | $bit}]
	    }
................................................................................
	    lappend result [expr {$val & 0x7}] [expr {$val >> 3}]
	}
	set result
    }
    -result {0 2 2 2 2 3}
}

test bdd-34.5 {foreach_fullsat - code 6} {*}{
    -body {
	set result {}
	list [catch {
	    bdd::foreach_fullsat s {6 3 0 7 4 1} {1 0 3 1 6 0 7 0} {
		set val 0
		foreach bit $s {
		    set val [expr {($val << 1) | $bit}]







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







 







|













|







 







|







 







|













|







 







|







 







|







 







|







 







|







 







|







2940
2941
2942
2943
2944
2945
2946
2947
2948
2949
2950
2951
2952
2953
2954
2955
2956
2957
2958
2959
2960
2961
2962
2963
2964
2965
2966
2967
2968
2969
2970
2971
2972
2973
2974
2975
2976
2977
2978
2979
2980
2981
2982
2983
2984
2985
2986
2987
2988
2989
2990
2991
2992
2993
2994
2995
2996
2997
2998
2999
3000
....
3001
3002
3003
3004
3005
3006
3007
3008
3009
3010
3011
3012
3013
3014
3015
3016
3017
3018
3019
3020
3021
3022
3023
3024
3025
3026
3027
3028
3029
....
3041
3042
3043
3044
3045
3046
3047
3048
3049
3050
3051
3052
3053
3054
3055
....
3056
3057
3058
3059
3060
3061
3062
3063
3064
3065
3066
3067
3068
3069
3070
3071
3072
3073
3074
3075
3076
3077
3078
3079
3080
3081
3082
3083
3084
....
3097
3098
3099
3100
3101
3102
3103
3104
3105
3106
3107
3108
3109
3110
3111
....
3112
3113
3114
3115
3116
3117
3118
3119
3120
3121
3122
3123
3124
3125
3126
....
3133
3134
3135
3136
3137
3138
3139
3140
3141
3142
3143
3144
3145
3146
3147
....
3151
3152
3153
3154
3155
3156
3157
3158
3159
3160
3161
3162
3163
3164
3165
....
3169
3170
3171
3172
3173
3174
3175
3176
3177
3178
3179
3180
3181
3182
3183
    }
    -cleanup {
	rename sys {}
    }
    -result {0 1 0 0 {} 2}
}

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

test bdd-32.2 {satisfiable - bad expr} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys satisfiable garbage} result] $result $::errorCode
    }
    -cleanup {
	sys destroy
    }
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-32.3 {satisfiable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
    }
    -body {
	list \
	    [sys satisfiable 0] [sys satisfiable 1] \
	    [sys satisfiable a] [sys satisfiable !a] \
	    [sys unset a !a] [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {0 1 1 1 {} 2}
}

test bdd-33.1 {support - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys support
    }
    -cleanup {
................................................................................
	sys destroy
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test bdd-33.2 {support - bad expr} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys support garbage} result] $result $::errorCode
    }
    -cleanup {
	sys destroy
    }
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-33.3 {support} {*}{
    -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 ^ d a b
	sys ^ e a c
................................................................................
    }
    -cleanup {
	rename sys {}
    }
    -result {{} {} 0 0 1 1 2 2 {0 1} {0 2} {1 2} {0 1 2} {} 2}
}

test bdd-34.1 {beadcount - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys beadcount
    }
    -cleanup {
................................................................................
	sys destroy
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test bdd-34.2 {beadcount - bad expr} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys beadcount garbage} result] $result $::errorCode
    }
    -cleanup {
	sys destroy
    }
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-34.3 {beadcount} {*}{
    -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 ^ d a b
	sys ^ e a c
................................................................................
    }
    -cleanup {
	rename sys {}
    }
    -result {0 0 1 1 1 1 1 1 3 3 3 5 {} 2}
}

test bdd-35.1 {foreach_fullsat} {*}{
    -body {
	set result {}
	bdd::foreach_fullsat s {6 3 0 7 4 1} {1 0 3 1 6 0 7 0} {
	    set val 0
	    foreach bit $s {
		set val [expr {($val << 1) | $bit}]
	    }
................................................................................
	    lappend result [expr {$val & 0x7}] [expr {$val >> 3}]
	}
	set result
    }
    -result {0 2 2 2 0 3 2 3}
}

test bdd-35.2 {foreach_fullsat - return} {*}{
    -setup {
	proc x {} {
	    bdd::foreach_fullsat s {6 3 0 7 4 1} {1 0 3 1 6 0 7 0} {
		set val 0
		foreach bit $s {
		    set val [expr {($val << 1) | $bit}]
		}
................................................................................
    }
    -cleanup {
	rename x {}
    }
    -result {0 2}
}

test bdd-35.3 {foreach_fullsat - break} {*}{
    -body {
	set result {}
	bdd::foreach_fullsat s {6 3 0 7 4 1} {1 0 3 1 6 0 7 0} {
	    set val 0
	    foreach bit $s {
		set val [expr {($val << 1) | $bit}]
	    }
................................................................................
	    lappend result [expr {$val & 0x7}] [expr {$val >> 3}]
	}
	set result
    }
    -result {0 2 2 2}
}

test bdd-35.4 {foreach_fullsat - continue} {*}{
    -body {
	set result {}
	bdd::foreach_fullsat s {6 3 0 7 4 1} {1 0 3 1 6 0 7 0} {
	    set val 0
	    foreach bit $s {
		set val [expr {($val << 1) | $bit}]
	    }
................................................................................
	    lappend result [expr {$val & 0x7}] [expr {$val >> 3}]
	}
	set result
    }
    -result {0 2 2 2 2 3}
}

test bdd-35.5 {foreach_fullsat - code 6} {*}{
    -body {
	set result {}
	list [catch {
	    bdd::foreach_fullsat s {6 3 0 7 4 1} {1 0 3 1 6 0 7 0} {
		set val 0
		foreach bit $s {
		    set val [expr {($val << 1) | $bit}]