tclbdd

Check-in [1c92997d04]
Login

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

Overview
Comment:Refactor tests so that fddd tests do not test functions that depend only on the core BDD library
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:1c92997d041bbf70027bc5f7546aab865027af42
User & Date: kbk 2014-08-02 21:24:23
Context
2014-08-02
23:48
Add more FDDD tests, clean up whitespace in tests, and fix bugs exposed in testing. check-in: 22d056d9e0 user: kbk tags: trunk
21:24
Refactor tests so that fddd tests do not test functions that depend only on the core BDD library check-in: 1c92997d04 user: kbk tags: trunk
21:23
Add leading comment so as not to confuse 'man' check-in: 668a835e53 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to tests/bdd.test.

29
30
31
32
33
34
35


36
37
38
39
40
41
42
..
49
50
51
52
53
54
55


56
57
58
59
60
61
62
..
80
81
82
83
84
85
86



87
88
89
90
91
92
93
...
104
105
106
107
108
109
110


111
112
113
114
115
116
117
...
127
128
129
130
131
132
133


134
135
136
137
138
139
140
...
184
185
186
187
188
189
190


191
192
193
194
195
196
197
...
244
245
246
247
248
249
250


251
252
253
254
255
256
257
...
316
317
318
319
320
321
322


323
324
325
326
327
328
329
...
588
589
590
591
592
593
594


595
596
597
598
599
600
601
...
618
619
620
621
622
623
624


625
626
627
628
629
630
631
...
735
736
737
738
739
740
741


742
743
744
745
746
747
748
...
895
896
897
898
899
900
901


902
903
904
905
906
907
908
....
1095
1096
1097
1098
1099
1100
1101


1102
1103
1104
1105
1106
1107
1108
....
1343
1344
1345
1346
1347
1348
1349




1350
1351
1352
1353
1354
1355
1356
....
1665
1666
1667
1668
1669
1670
1671


1672
1673
1674
1675
1676
1677
1678
....
2084
2085
2086
2087
2088
2089
2090


2091
2092
2093
2094
2095
2096
2097
....
2397
2398
2399
2400
2401
2402
2403


2404
2405
2406
2407
2408
2409
2410
....
2559
2560
2561
2562
2563
2564
2565


2566
2567
2568
2569
2570
2571
2572
....
2691
2692
2693
2694
2695
2696
2697


2698
2699
2700
2701
2702
2703
2704
....
2831
2832
2833
2834
2835
2836
2837
















































































































































































































































































































































































































































































2838
2839
2840
2841
2842
2843
2844
....
2893
2894
2895
2896
2897
2898
2899


2900
2901
2902
2903
2904
2905
2906
....
2939
2940
2941
2942
2943
2944
2945


2946
2947
2948
2949
2950
2951
2952
....
2985
2986
2987
2988
2989
2990
2991


2992
2993
2994
2995
2996
2997
2998
....
3040
3041
3042
3043
3044
3045
3046


3047
3048
3049
3050
3051
3052
3053
....
3096
3097
3098
3099
3100
3101
3102


3103
3104
3105
3106
3107
3108
3109
....
3188
3189
3190
3191
3192
3193
3194




3195
3196
3197
3198
3199
3200
3201
    set root [lindex $dump 0]
    set result {}
    for {set i 0} {$i < (1<<$nvars)} {incr i} {
	append result [evdump $dump $nvars $root $i 0]
    }
    return $result
}



test bdd-1.0 {simple create/delete} {
    set s [bdd::system new]
    rename $s {}
} {}

test bdd-1.1 {create with nonstandard size} {
................................................................................
    -result {wrong # args*}
}
test bdd-1.3 {size not an integer} {*}{
    -body {rename [bdd::system new garbage] {}}
    -returnCodes error
    -result {expected integer but got "garbage"}
}



test bdd-2.1 {beadindex wrong # args} {*}{
    -setup {bdd::system create sys}
    -body {sys beadindex}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
test bdd-2.4 {expression not found} {*}{
    -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
................................................................................

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}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................

test bdd-5.3 {dump - leaf 1} {*}{
    -setup {bdd::system create sys}
    -body {sys dump 1}
    -cleanup {rename sys {}}
    -result {1 {0 1 1}}
}



test bdd-6.1 {nthvar - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys nthvar}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	list [sys beadindex a] [sys beadindex b] [sys beadindex c] \
	    [sys unset a] [sys unset b] [sys unset c] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {2 3 2 {} {} {} 2}
}



test bdd-7.1 {notnthvar - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys notnthvar}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	sys nthvar a 0
	sys unset a
	list [catch {sys := b a} result] $result $::errorCode [sys gc]
    }
    -cleanup {sys destroy}
    -result {1 {expression named "a" not found} {BDD ExprNotFound a} 2} 
}



test bdd-8.1 {negate - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys ~}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	sys ~ b !a; 
	list [expr {[sys beadindex b] == [sys beadindex a]}] \
	    [sys unset b] [sys unset !a] [sys unset a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} {} {} 2}
}



test bdd-9.1 {binop - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys nand}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {1110 1101 1011 0111 2}
}



test bdd-10.1 {syllogism in the mode of barbara} {
    -setup {
	bdd::system create sys
	sys nthvar man(x) 0
	sys nthvar mortal(x) 1
	sys nthvar socrates(x) 2
................................................................................
	    [sys unset test2 test1 test0 conclusion conjunct minor major \
		 socrates(x) mortal(x) man(x)] \
	    [sys gc]
    } 
    -cleanup {rename sys {}}
    -result {0 0 1 10110001 {} 2}
}



test bdd-11.1 {demorgan} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
................................................................................
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {
	rename sys {}
   }
}



test bdd-12.1 {satcount - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys satcount}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	lappend result [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {257 80000000000000000000000000000000 2}
}



test bdd-13.1 {restrict - wrong # args} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
................................................................................
	list [sys beadindex r1] \
	    [sys unset r1 r2 c b a !c !b !a] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}



test bdd-14.1 {foreach_sat - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys foreach_sat
................................................................................
	lappend result [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {6 testing 2}
}





test bdd-15.1.1 {quantifiers - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys exists
................................................................................
	list [expr {[sys beadindex zu] == [sys beadindex yu]}] \
	    [sys unset zu yu expr term e !e f !f a b c d] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}



foreach operation {
    &3 ^3 ?: borrow concur3 differ3 even3 median nand3 nor3 oneof3 twoof3 |3
} {
    test bdd-16.1-$operation "$operation - wrong # args" {*}{
	-setup {
	    bdd::system create sys
................................................................................
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z y !p !q !r p q r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}



test bdd-17.1 {compose - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys compose
................................................................................
	list [expr {[sys beadindex z] == [sys beadindex y]}] \
	    [sys unset x y z t u a b c d] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}



test bdd-18.1 {appquant - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys exists_&
................................................................................
		    [sys gc]
	    }
	    -cleanup {rename sys {}}
	    -result {1 {} 2}
	}
    }
}



test bdd-19.1 {profile - wrong # args} {*}{
    -setup {bdd::system create sys}
    -body {sys profile}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	list [sys profile result] \
	    [sys unset result a1 a2 a4 a8 b1 b2 b4 b8 z1 z2 z4 z8] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {{1 2 3 2 3 4 2 3 4 2 2 2} {} 2}
}



test bdd-20.1 {simplify - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys simplify
................................................................................
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

















































































































































































































































































































































































































































































test bdd-30.1 {=== - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys ===
................................................................................
    }
    -cleanup {
	sys destroy
    }
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}



test bdd-31.1 {tautology - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys tautology
................................................................................
	    [sys unset a !a] [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {0 1 0 0 {} 2}
}



test bdd-32.1 {satisfiable - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys satisfiable
................................................................................
	    [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
................................................................................
	    [sys unset a !a b !b c !c d e f g] [sys gc]
    }
    -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
................................................................................
	    [sys unset a !a b !b c !c d e f g] [sys gc]
    }
    -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 {
................................................................................
		lappend result [expr {$val & 0x7}] [expr {$val >> 3}]
	    }
	} v] $v $result
    }
    -result {3 {} {0 2 2 2}}
}
	    




test bdd-40.1 {eight queens} {*}{
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 64} {incr i} {
	    sys nthvar v$i $i; sys notnthvar !v$i $i
	}
    }







>
>







 







>
>







 







>
>
>







 







>
>







 







>
>







 







>
>







 







>
>







 







>
>







 







>
>







 







>
>







 







>
>







 







>
>







 







>
>







 







>
>
>
>







 







>
>







 







>
>







 







>
>







 







>
>







 







>
>







 







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







 







>
>







 







>
>







 







>
>







 







>
>







 







>
>







 







>
>
>
>







29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
..
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
..
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
...
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
...
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
...
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
...
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
...
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
...
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
...
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
...
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
...
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
....
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
....
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
....
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
....
2117
2118
2119
2120
2121
2122
2123
2124
2125
2126
2127
2128
2129
2130
2131
2132
....
2432
2433
2434
2435
2436
2437
2438
2439
2440
2441
2442
2443
2444
2445
2446
2447
....
2596
2597
2598
2599
2600
2601
2602
2603
2604
2605
2606
2607
2608
2609
2610
2611
....
2730
2731
2732
2733
2734
2735
2736
2737
2738
2739
2740
2741
2742
2743
2744
2745
....
2872
2873
2874
2875
2876
2877
2878
2879
2880
2881
2882
2883
2884
2885
2886
2887
2888
2889
2890
2891
2892
2893
2894
2895
2896
2897
2898
2899
2900
2901
2902
2903
2904
2905
2906
2907
2908
2909
2910
2911
2912
2913
2914
2915
2916
2917
2918
2919
2920
2921
2922
2923
2924
2925
2926
2927
2928
2929
2930
2931
2932
2933
2934
2935
2936
2937
2938
2939
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
3030
3031
3032
3033
3034
3035
3036
3037
3038
3039
3040
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
3085
3086
3087
3088
3089
3090
3091
3092
3093
3094
3095
3096
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
3127
3128
3129
3130
3131
3132
3133
3134
3135
3136
3137
3138
3139
3140
3141
3142
3143
3144
3145
3146
3147
3148
3149
3150
3151
3152
3153
3154
3155
3156
3157
3158
3159
3160
3161
3162
3163
3164
3165
3166
3167
3168
3169
3170
3171
3172
3173
3174
3175
3176
3177
3178
3179
3180
3181
3182
3183
3184
3185
3186
3187
3188
3189
3190
3191
3192
3193
3194
3195
3196
3197
3198
3199
3200
3201
3202
3203
3204
3205
3206
3207
3208
3209
3210
3211
3212
3213
3214
3215
3216
3217
3218
3219
3220
3221
3222
3223
3224
3225
3226
3227
3228
3229
3230
3231
3232
3233
3234
3235
3236
3237
3238
3239
3240
3241
3242
3243
3244
3245
3246
3247
3248
3249
3250
3251
3252
3253
3254
3255
3256
3257
3258
3259
3260
3261
3262
3263
3264
3265
3266
3267
3268
3269
3270
3271
3272
3273
3274
3275
3276
3277
3278
3279
3280
3281
3282
3283
3284
3285
3286
3287
3288
3289
3290
3291
3292
3293
3294
3295
3296
3297
3298
3299
3300
3301
3302
3303
3304
3305
3306
3307
3308
3309
3310
3311
3312
3313
3314
3315
3316
3317
3318
3319
3320
3321
3322
3323
3324
3325
3326
3327
3328
3329
3330
3331
3332
3333
3334
3335
3336
3337
3338
3339
3340
3341
3342
3343
3344
3345
3346
3347
3348
3349
....
3398
3399
3400
3401
3402
3403
3404
3405
3406
3407
3408
3409
3410
3411
3412
3413
....
3446
3447
3448
3449
3450
3451
3452
3453
3454
3455
3456
3457
3458
3459
3460
3461
....
3494
3495
3496
3497
3498
3499
3500
3501
3502
3503
3504
3505
3506
3507
3508
3509
....
3551
3552
3553
3554
3555
3556
3557
3558
3559
3560
3561
3562
3563
3564
3565
3566
....
3609
3610
3611
3612
3613
3614
3615
3616
3617
3618
3619
3620
3621
3622
3623
3624
....
3703
3704
3705
3706
3707
3708
3709
3710
3711
3712
3713
3714
3715
3716
3717
3718
3719
3720
    set root [lindex $dump 0]
    set result {}
    for {set i 0} {$i < (1<<$nvars)} {incr i} {
	append result [evdump $dump $nvars $root $i 0]
    }
    return $result
}

# bdd-1 - new and delete of bdd's

test bdd-1.0 {simple create/delete} {
    set s [bdd::system new]
    rename $s {}
} {}

test bdd-1.1 {create with nonstandard size} {
................................................................................
    -result {wrong # args*}
}
test bdd-1.3 {size not an integer} {*}{
    -body {rename [bdd::system new garbage] {}}
    -returnCodes error
    -result {expected integer but got "garbage"}
}

# bdd-2 - beadindex

test bdd-2.1 {beadindex wrong # args} {*}{
    -setup {bdd::system create sys}
    -body {sys beadindex}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
test bdd-2.4 {expression not found} {*}{
    -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}}
}

# bdd-3 - obsolete
# bdd-4 - :=

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

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

# bdd-5 - dump

test bdd-5.1 {dump - wrong # args} {*}{
    -setup {bdd::system create sys}
    -body {sys dump}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................

test bdd-5.3 {dump - leaf 1} {*}{
    -setup {bdd::system create sys}
    -body {sys dump 1}
    -cleanup {rename sys {}}
    -result {1 {0 1 1}}
}

# bdd-6 - nthvar

test bdd-6.1 {nthvar - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys nthvar}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	list [sys beadindex a] [sys beadindex b] [sys beadindex c] \
	    [sys unset a] [sys unset b] [sys unset c] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {2 3 2 {} {} {} 2}
}

# bdd-7 - notnthvar

test bdd-7.1 {notnthvar - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys notnthvar}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	sys nthvar a 0
	sys unset a
	list [catch {sys := b a} result] $result $::errorCode [sys gc]
    }
    -cleanup {sys destroy}
    -result {1 {expression named "a" not found} {BDD ExprNotFound a} 2} 
}

# bdd-8 - negate (~)

test bdd-8.1 {negate - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys ~}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	sys ~ b !a; 
	list [expr {[sys beadindex b] == [sys beadindex a]}] \
	    [sys unset b] [sys unset !a] [sys unset a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} {} {} 2}
}

# bdd-9 - binary operators

test bdd-9.1 {binop - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys nand}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {1110 1101 1011 0111 2}
}

# bdd-10 - demo

test bdd-10.1 {syllogism in the mode of barbara} {
    -setup {
	bdd::system create sys
	sys nthvar man(x) 0
	sys nthvar mortal(x) 1
	sys nthvar socrates(x) 2
................................................................................
	    [sys unset test2 test1 test0 conclusion conjunct minor major \
		 socrates(x) mortal(x) man(x)] \
	    [sys gc]
    } 
    -cleanup {rename sys {}}
    -result {0 0 1 10110001 {} 2}
}

# bdd-11 - test with DeMorgan's Laws

test bdd-11.1 {demorgan} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
................................................................................
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {
	rename sys {}
   }
}

# bdd-12 - satcount

test bdd-12.1 {satcount - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys satcount}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	lappend result [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {257 80000000000000000000000000000000 2}
}

# bdd-13 - restrict

test bdd-13.1 {restrict - wrong # args} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
................................................................................
	list [sys beadindex r1] \
	    [sys unset r1 r2 c b a !c !b !a] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

# bdd-14 - foreach_sat

test bdd-14.1 {foreach_sat - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys foreach_sat
................................................................................
	lappend result [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {6 testing 2}
}

# bdd-15 - quantifiers
#   15.x.1 - exists
#   15.x.2 - forall

test bdd-15.1.1 {quantifiers - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys exists
................................................................................
	list [expr {[sys beadindex zu] == [sys beadindex yu]}] \
	    [sys unset zu yu expr term e !e f !f a b c d] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

# bdd-16 - ternary operations

foreach operation {
    &3 ^3 ?: borrow concur3 differ3 even3 median nand3 nor3 oneof3 twoof3 |3
} {
    test bdd-16.1-$operation "$operation - wrong # args" {*}{
	-setup {
	    bdd::system create sys
................................................................................
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z y !p !q !r p q r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

# bdd-17 - compose

test bdd-17.1 {compose - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys compose
................................................................................
	list [expr {[sys beadindex z] == [sys beadindex y]}] \
	    [sys unset x y z t u a b c d] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

# bdd-18 - apply and quantify

test bdd-18.1 {appquant - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys exists_&
................................................................................
		    [sys gc]
	    }
	    -cleanup {rename sys {}}
	    -result {1 {} 2}
	}
    }
}

# bdd-19 - profile

test bdd-19.1 {profile - wrong # args} {*}{
    -setup {bdd::system create sys}
    -body {sys profile}
    -cleanup {rename sys {}}
    -returnCodes error
    -match glob
................................................................................
	list [sys profile result] \
	    [sys unset result a1 a2 a4 a8 b1 b2 b4 b8 z1 z2 z4 z8] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {{1 2 3 2 3 4 2 3 4 2 2 2} {} 2}
}

# bdd-20 - simplify

test bdd-20.1 {simplify - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys simplify
................................................................................
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

# bddd-21 - load

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

test bdd-21.2 {load term - bad integer} {*}{
    -setup {
	bdd::system create sys
    } 
    -body {
	sys load x {} garbage
    } 
    -cleanup {
	rename sys {}
    }
    -result {expected integer but got "garbage"}
    -returnCodes error
}

test bdd-21.3 {load term - ill-formed list} {
    -setup {
	bdd::system create sys
    }
    -body {
	sys load x \{ 
    }
    -cleanup {
	rename sys {}
    }
    -result {unmatched open brace in list}
    -returnCodes error
}

test bdd-21.4 {load term - wrong list size} {
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys load x {1 2}} result] $result $::errorCode
    }
    -cleanup {
	rename sys {}
    }
    -result {1 {description list must have a multiple of 3 elements} {BDD DescNotMultipleOf3}}
}

test bdd-21.5 {load - bad integer - also check bead leak} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {garbage 0 0 1 0 1} 0} result] \
	    $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test bdd-21.6 {load - bad integer - also check bead leak} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 garbage 0 1 0 1} 0} result] \
	    $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test bdd-21.7 {load - bad integer - also check bead leak} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 0 garbage 1 0 1} 0} result] \
	    $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test bdd-21.8 {load - nonincreasing var indices} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {1 0 0 1 0 1} 0} result] \
	    $result \
	    $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {variables are not in increasing order} {BDD VarsOutOfOrder} 2}
}

test bdd-21.9 {load - nonexistent param} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 1 0 1 0 1} 0} result] \
	    $result \
	    $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {description refers to a nonexistent parameter} {BDD NonexistentParam} 2}
}

test bdd-21.10 {load - bad bit index} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 0 65 1 0 1} 0} result] \
	    $result \
	    $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {bad bit index in description} {BDD BadBitIndex} 2}
}

test bdd-21.11 {load - do nothing gracefully} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys load x {}
	list [sys beadindex x] [sys unset x] [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test bdd-21.12 {load multiple terms} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	set result {}
	for {set i 0} {$i < 3} {incr i} {
	    set j [expr {($i + 1) % 4}]
	    sys load x {0 0 0 3 1 1 5 1 0 7 0 1} $i $j
	}
	sys foreach_sat s x {
	    lappend result $s
	}
	sys unset x
	lappend result [sys gc]
	set result
    }
    -cleanup {
	sys destroy
    }
    -result {{0 0 3 0 5 1 7 0} {0 0 3 1 5 1 7 1} {0 1 3 1 5 0 7 0} 2}
}

# bdd-22 - project

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

test bdd-22.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 bdd-22.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 bdd-22.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 bdd-22.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 bdd-22.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 bdd-22.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}
}

test bdd-22.8 {project with unused variable} {*}{
    -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 42} 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}
}

# bdd-23 - replace

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

test bdd-23.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 bdd-23.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 bdd-23.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 bdd-23.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 bdd-23.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 bdd-23.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 bdd-23.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 bdd-23.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}
}

# bdd-24-29 - available

# bdd-30 - ===

test bdd-30.1 {=== - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys ===
................................................................................
    }
    -cleanup {
	sys destroy
    }
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

# bdd-31 - tautology

test bdd-31.1 {tautology - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys tautology
................................................................................
	    [sys unset a !a] [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {0 1 0 0 {} 2}
}

# bdd-32 - satisfiable

test bdd-32.1 {satisfiable - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys satisfiable
................................................................................
	    [sys unset a !a] [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {0 1 1 1 {} 2}
}

# bdd-33 - support

test bdd-33.1 {support - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys support
................................................................................
	    [sys unset a !a b !b c !c d e f g] [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {{} {} 0 0 1 1 2 2 {0 1} {0 2} {1 2} {0 1 2} {} 2}
}

# bdd-34 - beadcount

test bdd-34.1 {beadcount - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys beadcount
................................................................................
	    [sys unset a !a b !b c !c d e f g] [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {0 0 1 1 1 1 1 1 3 3 3 5 {} 2}
}

# bdd-35 - foreach_fullsat

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 {
................................................................................
		lappend result [expr {$val & 0x7}] [expr {$val >> 3}]
	    }
	} v] $v $result
    }
    -result {3 {} {0 2 2 2}}
}
	    
# bdd-36-39 available

# bdd-40 - demos: eight queens, circuit verification,

test bdd-40.1 {eight queens} {*}{
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 64} {incr i} {
	    sys nthvar v$i $i; sys notnthvar !v$i $i
	}
    }

Changes to tests/fddd.test.

5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
...
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
...
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
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
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
# Copyright (c) 2013 by Kevin B. Kenny.

package require tcltest 2
namespace import -force ::tcltest::*
tcltest::loadTestedCommands
package require tclbdd::fddd

test fddd-1.1 {load term - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys load
    }
    -cleanup {
	rename sys {}
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test fddd-1.2 {load term - bad integer} {*}{
    -setup {
	bdd::system create sys
    } 
    -body {
	sys load x {} garbage
    } 
    -cleanup {
	rename sys {}
    }
    -result {expected integer but got "garbage"}
    -returnCodes error
}

test fddd-1.3 {load term - ill-formed list} {
    -setup {
	bdd::system create sys
    }
    -body {
	sys load x \{ 
    }
    -cleanup {
	rename sys {}
    }
    -result {unmatched open brace in list}
    -returnCodes error
}

test fddd-1.4 {load term - wrong list size} {
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys load x {1 2}} result] $result $::errorCode
    }
    -cleanup {
	rename sys {}
    }
    -result {1 {description list must have a multiple of 3 elements} {BDD DescNotMultipleOf3}}
}

test fddd-1.5 {load - bad integer - also check bead leak} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {garbage 0 0 1 0 1} 0} result] \
	    $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test fddd-1.6 {load - bad integer - also check bead leak} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 garbage 0 1 0 1} 0} result] \
	    $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test fddd-1.7 {load - bad integer - also check bead leak} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 0 garbage 1 0 1} 0} result] \
	    $result \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {expected integer but got "garbage"} 2}
}

test fddd-1.8 {load - nonincreasing var indices} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {1 0 0 1 0 1} 0} result] \
	    $result \
	    $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {variables are not in increasing order} {BDD VarsOutOfOrder} 2}
}

test fddd-1.9 {load - nonexistent param} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 1 0 1 0 1} 0} result] \
	    $result \
	    $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {description refers to a nonexistent parameter} {BDD NonexistentParam} 2}
}

test fddd-1.10 {load - bad bit index} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list \
	    [catch {sys load x {0 0 65 1 0 1} 0} result] \
	    $result \
	    $::errorCode \
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {bad bit index in description} {BDD BadBitIndex} 2}
}

test fddd-1.11 {load - do nothing gracefully} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys load x {}
	list [sys beadindex x] [sys unset x] [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test fddd-1.12 {load multiple terms} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	set result {}
	for {set i 0} {$i < 3} {incr i} {
	    set j [expr {($i + 1) % 4}]
	    sys load x {0 0 0 3 1 1 5 1 0 7 0 1} $i $j
	}
	sys foreach_sat s x {
	    lappend result $s
	}
	sys unset x
	lappend result [sys gc]
	set result
    }
    -cleanup {
	sys destroy
    }
    -result {{0 0 3 0 5 1 7 0} {0 0 3 1 5 1 7 1} {0 1 3 1 5 0 7 0} 2}
}

test fddd-2.1 {domain - wrong # args} {*}{
    -body {
	bdd::fddd::domain
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test fddd-2.2 {domain - bigendian default, littleendian available} {*}{
    -body {
	list \
	    [bdd::fddd::domain a 3] \
	    [bdd::fddd::domain b 3 littleendian] \
	    [bdd::fddd::domain c 3 bigendian]
    }
    -result {{{a {0 1 2}} {a 0 a 1 a 2}} {{b {0 1 2}} {b 0 b 1 b 2}} {{c {2 1 0}} {c 2 c 1 c 0}}}
}

test fddd-2.3 {interleave - duplicated domains} {*}{
    -body {
	list [catch {
	    bdd::fddd::interleave \
		[bdd::fddd::domain a 3] \
		[bdd::fddd::domain a 3]
	} result] $result $::errorCode
    }
    -result {1 {domain named "a" appears in multiple places} {FDDD DuplicateName a}}
}

test fddd-2.4 {interleave - two domains} {*}{
    -body {
	bdd::fddd::interleave \
	    [bdd::fddd::domain a 3] \
	    [bdd::fddd::domain b 3]
    }
    -result {{a {0 2 4} b {1 3 5}} {a 0 b 0 a 1 b 1 a 2 b 2}}
}

test fddd-2.5 {interleave - three domains} {*}{
    -body {
	bdd::fddd::interleave \
	    [bdd::fddd::domain a 3] \
	    [bdd::fddd::domain b 3 bigendian] \
	    [bdd::fddd::domain c 3]
    }
    -result {{a {0 3 6} b {7 4 1} c {2 5 8}} {a 0 b 2 c 0 a 1 b 1 c 1 a 2 b 0 c 2}}
}

test fddd-2.6 {interleave - domains of unequal lengths} {*}{
    -body {
	bdd::fddd::interleave \
	    [bdd::fddd::domain a 4] \
	    [bdd::fddd::domain b 3 bigendian] \
	    [bdd::fddd::domain c 2]
    }
    -result {{a {0 3 6 8} b {7 4 1} c {2 5}} {a 0 b 2 c 0 a 1 b 1 c 1 a 2 b 0 a 3}}
}

test fddd-2.7 {concatenate - duplicated domains} {*}{
    -body {
	list [catch {
	    bdd::fddd::concatenate \
		[bdd::fddd::domain a 3] \
		[bdd::fddd::domain a 3]
	} result] $result $::errorCode
    }
    -result {1 {domain named "a" appears in multiple places} {FDDD DuplicateName a}}
}

test fddd-2.8 {concatenate - two domains} {*}{
    -body {
	bdd::fddd::concatenate \
	    [bdd::fddd::domain a 3] \
	    [bdd::fddd::domain b 3 bigendian]
    }
    -result {{a {0 1 2} b {5 4 3}} {a 0 a 1 a 2 b 2 b 1 b 0}}
}

test fddd-2.9 {concatenate of interleaved} {*}{
    -body {
	bdd::fddd::concatenate \
	    [bdd::fddd::interleave \
		 [bdd::fddd::domain a 3] \
		 [bdd::fddd::domain b 3]] \
	    [bdd::fddd::interleave \
		 [bdd::fddd::domain c 3] \
		 [bdd::fddd::domain d 3]]
    }
    -result {{a {0 2 4} b {1 3 5} c {6 8 10} d {7 9 11}} {a 0 b 0 a 1 b 1 a 2 b 2 c 0 d 0 c 1 d 1 c 2 d 2}}
}

test fddd-2.10 {interleave of concatenated} {*}{
    -body {
	bdd::fddd::interleave \
	    [bdd::fddd::concatenate \
		 [bdd::fddd::domain a 3] \
		 [bdd::fddd::domain b 3]] \
	    [bdd::fddd::concatenate \
		 [bdd::fddd::domain c 3] \
		 [bdd::fddd::domain d 3]]
    }
    -result {{a {0 2 4} c {1 3 5} b {6 8 10} d {7 9 11}} {a 0 c 0 a 1 c 1 a 2 c 2 b 0 d 0 b 1 d 1 b 2 d 2}}
}

test fddd-3.1 {reader - 1 column} {*}{
    -constraints obsolete
    -setup {
	bdd::system create sys
	set layout \
	    [bdd::fddd::concatenate \
		 [bdd::fddd::domain a 2] \
		 [bdd::fddd::domain b 2]]
................................................................................
    -cleanup {
	rename rdr {}
	sys destroy
    }
    -result {{0 0 1 1} {0 1 1 0} 2}
}

test fddd-3.2 {reader - 2 columns} {
    -constraints obsolete
    -setup {
	bdd::system create sys
	set layout \
	    [bdd::fddd::concatenate \
		 [bdd::fddd::domain a 2 bigendian] \
		 [bdd::fddd::domain b 2 bigendian]]
................................................................................
    }
    -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}
}

test fddd-4.8 {project with unused variable} {*}{
    -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 42} 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}
}

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}
}


cleanupTests
return

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







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








|









|










|








|









|









|










|








|












|












|







 







|







 








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







5
6
7
8
9
10
11
































































































































































































12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
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
...
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
...
166
167
168
169
170
171
172
173







































































































































































































































































174
175
176
177
178
179
180
# Copyright (c) 2013 by Kevin B. Kenny.

package require tcltest 2
namespace import -force ::tcltest::*
tcltest::loadTestedCommands
package require tclbdd::fddd

































































































































































































test fddd-1.1 {domain - wrong # args} {*}{
    -body {
	bdd::fddd::domain
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

test fddd-1.2 {domain - bigendian default, littleendian available} {*}{
    -body {
	list \
	    [bdd::fddd::domain a 3] \
	    [bdd::fddd::domain b 3 littleendian] \
	    [bdd::fddd::domain c 3 bigendian]
    }
    -result {{{a {0 1 2}} {a 0 a 1 a 2}} {{b {0 1 2}} {b 0 b 1 b 2}} {{c {2 1 0}} {c 2 c 1 c 0}}}
}

test fddd-1.3 {interleave - duplicated domains} {*}{
    -body {
	list [catch {
	    bdd::fddd::interleave \
		[bdd::fddd::domain a 3] \
		[bdd::fddd::domain a 3]
	} result] $result $::errorCode
    }
    -result {1 {domain named "a" appears in multiple places} {FDDD DuplicateName a}}
}

test fddd-1.4 {interleave - two domains} {*}{
    -body {
	bdd::fddd::interleave \
	    [bdd::fddd::domain a 3] \
	    [bdd::fddd::domain b 3]
    }
    -result {{a {0 2 4} b {1 3 5}} {a 0 b 0 a 1 b 1 a 2 b 2}}
}

test fddd-1.5 {interleave - three domains} {*}{
    -body {
	bdd::fddd::interleave \
	    [bdd::fddd::domain a 3] \
	    [bdd::fddd::domain b 3 bigendian] \
	    [bdd::fddd::domain c 3]
    }
    -result {{a {0 3 6} b {7 4 1} c {2 5 8}} {a 0 b 2 c 0 a 1 b 1 c 1 a 2 b 0 c 2}}
}

test fddd-1.6 {interleave - domains of unequal lengths} {*}{
    -body {
	bdd::fddd::interleave \
	    [bdd::fddd::domain a 4] \
	    [bdd::fddd::domain b 3 bigendian] \
	    [bdd::fddd::domain c 2]
    }
    -result {{a {0 3 6 8} b {7 4 1} c {2 5}} {a 0 b 2 c 0 a 1 b 1 c 1 a 2 b 0 a 3}}
}

test fddd-1.7 {concatenate - duplicated domains} {*}{
    -body {
	list [catch {
	    bdd::fddd::concatenate \
		[bdd::fddd::domain a 3] \
		[bdd::fddd::domain a 3]
	} result] $result $::errorCode
    }
    -result {1 {domain named "a" appears in multiple places} {FDDD DuplicateName a}}
}

test fddd-1.8 {concatenate - two domains} {*}{
    -body {
	bdd::fddd::concatenate \
	    [bdd::fddd::domain a 3] \
	    [bdd::fddd::domain b 3 bigendian]
    }
    -result {{a {0 1 2} b {5 4 3}} {a 0 a 1 a 2 b 2 b 1 b 0}}
}

test fddd-1.9 {concatenate of interleaved} {*}{
    -body {
	bdd::fddd::concatenate \
	    [bdd::fddd::interleave \
		 [bdd::fddd::domain a 3] \
		 [bdd::fddd::domain b 3]] \
	    [bdd::fddd::interleave \
		 [bdd::fddd::domain c 3] \
		 [bdd::fddd::domain d 3]]
    }
    -result {{a {0 2 4} b {1 3 5} c {6 8 10} d {7 9 11}} {a 0 b 0 a 1 b 1 a 2 b 2 c 0 d 0 c 1 d 1 c 2 d 2}}
}

test fddd-1.10 {interleave of concatenated} {*}{
    -body {
	bdd::fddd::interleave \
	    [bdd::fddd::concatenate \
		 [bdd::fddd::domain a 3] \
		 [bdd::fddd::domain b 3]] \
	    [bdd::fddd::concatenate \
		 [bdd::fddd::domain c 3] \
		 [bdd::fddd::domain d 3]]
    }
    -result {{a {0 2 4} c {1 3 5} b {6 8 10} d {7 9 11}} {a 0 c 0 a 1 c 1 a 2 c 2 b 0 d 0 b 1 d 1 b 2 d 2}}
}

test fddd-2.1 {reader - 1 column} {*}{
    -constraints obsolete
    -setup {
	bdd::system create sys
	set layout \
	    [bdd::fddd::concatenate \
		 [bdd::fddd::domain a 2] \
		 [bdd::fddd::domain b 2]]
................................................................................
    -cleanup {
	rename rdr {}
	sys destroy
    }
    -result {{0 0 1 1} {0 1 1 0} 2}
}

test fddd-2.2 {reader - 2 columns} {
    -constraints obsolete
    -setup {
	bdd::system create sys
	set layout \
	    [bdd::fddd::concatenate \
		 [bdd::fddd::domain a 2 bigendian] \
		 [bdd::fddd::domain b 2 bigendian]]
................................................................................
    }
    -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}
}








































































































































































































































































cleanupTests
return

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