tclbdd

Check-in [e6c6de79de]
Login

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

Overview
Comment:Added tests for the convenience methods '===', 'tautology', 'support', 'beadcount' and fixed the bugs revealed.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:e6c6de79def50389328070168f713f4fccb41c6c
User & Date: kbk 2013-12-21 17:47:50
Context
2013-12-21
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
16:41
add missing loadscript.tcl.in from last commit check-in: 9c7232598c user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to library/tclbdd.tcl.

99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
...
128
129
130
131
132
133
134

135
136
137
138
139
140
141
    #	system - System of BDD's
    #   exprName - Name of the expression to test
    #
    # Results:
    #	Returns 1 if the expression is a tautology, 0 otherwise.

    method tautology {exprName} {
	expr {[my beadindex $exprname] == 1}
    }

    # Method: support
    #
    #	Returns the indices of variables upon which a BDD representing
    #	a Boolean formula depends
    #
................................................................................
	set result {}
	foreach k [my profile $exprName] {
	    if {$k != 0} {
		lappend result $i
	    }
	    incr i
	}

    }

    # Method: beadcount
    #
    #	Returns the number of beads in a BDD.
    #
    # Usage:







|







 







>







99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
...
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
    #	system - System of BDD's
    #   exprName - Name of the expression to test
    #
    # Results:
    #	Returns 1 if the expression is a tautology, 0 otherwise.

    method tautology {exprName} {
	expr {[my beadindex $exprName] == 1}
    }

    # Method: support
    #
    #	Returns the indices of variables upon which a BDD representing
    #	a Boolean formula depends
    #
................................................................................
	set result {}
	foreach k [my profile $exprName] {
	    if {$k != 0} {
		lappend result $i
	    }
	    incr i
	}
	return $result
    }

    # Method: beadcount
    #
    #	Returns the number of beads in a BDD.
    #
    # Usage:

Changes to tests/bdd.test.

2831
2832
2833
2834
2835
2836
2837



























































































































































































































2838
2839
2840
2841
2842
2843
2844
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 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 {







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







2831
2832
2833
2834
2835
2836
2837
2838
2839
2840
2841
2842
2843
2844
2845
2846
2847
2848
2849
2850
2851
2852
2853
2854
2855
2856
2857
2858
2859
2860
2861
2862
2863
2864
2865
2866
2867
2868
2869
2870
2871
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
	    [sys gc]
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

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

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

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

test bdd-30.4 {=== - bad second arg} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	list [catch {sys === garbage 0} result] $result $::errorCode
    }
    -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
    }
    -cleanup {
	sys destroy
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

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

test bdd-31.3 {tautology} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
    }
    -body {
	list \
	    [sys tautology 0] [sys tautology 1] \
	    [sys tautology a] [sys tautology !a] \
	    [sys unset a !a] [sys gc]
    }
    -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
	sys ^ f b c
	sys ^3 g a b c
    }
    -body {
	list \
	    [sys support 0] [sys support 1] \
	    [sys support a] [sys support !a] \
	    [sys support b] [sys support !b] \
	    [sys support c] [sys support !c] \
	    [sys support d] [sys support e] [sys support f] [sys support g] \
	    [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-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
	sys ^ f b c
	sys ^3 g a b c
    }
    -body {
	list \
	    [sys beadcount 0] [sys beadcount 1] \
	    [sys beadcount a] [sys beadcount !a] \
	    [sys beadcount b] [sys beadcount !b] \
	    [sys beadcount c] [sys beadcount !c] \
	    [sys beadcount d] [sys beadcount e] \
	    [sys beadcount f] [sys beadcount g] \
	    [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-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 {