tclbdd

Check-in [80342a5576]
Login

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

Overview
Comment:Renamed the 'fdd' subpackage to 'fddd'. (Finite Domain Decision Diagram is correct.) Added the machinery to include it in the [package] mechanism. Added 'foreach_fullsat' to expand out truth tables for SAT terms, and added test cases for the same. Added 'fddd::support' method (no tests yet) to list the finite domain variables that appear in a query term. Added test cases for 'fddd::domain' and friends, and fixed the bugs that the test cases exposed.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:80342a5576bdea1518d0dcdae8d7cb889a8de27b
User & Date: kbk 2013-12-17 15:53:04
Context
2013-12-17
16:16
Add test cases for low-level 'project' and fixed the bugs that were exposed check-in: 74ad4ed7f0 user: kbk tags: trunk
15:53
Renamed the 'fdd' subpackage to 'fddd'. (Finite Domain Decision Diagram is correct.) Added the machinery to include it in the [package] mechanism. Added 'foreach_fullsat' to expand out truth tables for SAT terms, and added test cases for the same. Added 'fddd::support' method (no tests yet) to list the finite domain variables that appear in a query term. Added test cases for 'fddd::domain' and friends, and fixed the bugs that the test cases exposed. check-in: 80342a5576 user: kbk tags: trunk
2013-12-14
23:20
correct name of 'fdd' package to 'fddd'. Add 'project' method to bdd base code - no driver nor tests yet. check-in: 444573ad82 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to Makefile.in.

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
	    echo "Installing $$i"; \
	    $(INSTALL_DATA) $$i $(DESTDIR)$(mandir)/mann ; \
	done

test: binaries libraries
	$(TCLSH) `@CYGPATH@ $(srcdir)/tests/all.tcl` $(TESTFLAGS) \
		-load "package ifneeded ${PACKAGE_NAME} ${PACKAGE_VERSION}\
	                [list source `@CYGPATH@ $(srcdir)/library/tclbdd.tcl`]\;[list load `@CYGPATH@ $(PKG_LIB_FILE)` $(PACKAGE_NAME)]"



shell: binaries libraries
	@$(TCLSH) $(SCRIPT)

gdb:
	$(TCLSH_ENV) gdb $(TCLSH_PROG) $(SCRIPT)

................................................................................
VALGRINDARGS =	--tool=memcheck --num-callers=8 --leak-resolution=high \
		--leak-check=yes --show-reachable=yes -v

valgrind: binaries libraries
	$(TCLSH_ENV) valgrind $(VALGRINDARGS) $(TCLSH_PROG) \
		`@CYGPATH@ $(srcdir)/tests/all.tcl` $(TESTFLAGS) \
		-load "package ifneeded ${PACKAGE_NAME} ${PACKAGE_VERSION}\
	                [list source `@CYGPATH@ $(srcdir)/library/tclbdd.tcl`]\;[list load `@CYGPATH@ ./$(PKG_LIB_FILE)` $(PACKAGE_NAME)]"



valgrindshell: binaries libraries
	$(TCLSH_ENV) valgrind $(VALGRINDARGS) $(TCLSH_PROG) $(SCRIPT)

depend:

#========================================================================







|
>
>







 







|
>
>







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
	    echo "Installing $$i"; \
	    $(INSTALL_DATA) $$i $(DESTDIR)$(mandir)/mann ; \
	done

test: binaries libraries
	$(TCLSH) `@CYGPATH@ $(srcdir)/tests/all.tcl` $(TESTFLAGS) \
		-load "package ifneeded ${PACKAGE_NAME} ${PACKAGE_VERSION}\
	                [list source `@CYGPATH@ $(srcdir)/library/tclbdd.tcl`]\;[list load `@CYGPATH@ ./$(PKG_LIB_FILE)` $(PACKAGE_NAME)]" \
		-load "package ifneeded ${PACKAGE_NAME}::tclfddd ${PACKAGE_VERSION}\
		    [list source `@CYGPATH@ $(srcdir)/library/tclfddd.tcl`]"

shell: binaries libraries
	@$(TCLSH) $(SCRIPT)

gdb:
	$(TCLSH_ENV) gdb $(TCLSH_PROG) $(SCRIPT)

................................................................................
VALGRINDARGS =	--tool=memcheck --num-callers=8 --leak-resolution=high \
		--leak-check=yes --show-reachable=yes -v

valgrind: binaries libraries
	$(TCLSH_ENV) valgrind $(VALGRINDARGS) $(TCLSH_PROG) \
		`@CYGPATH@ $(srcdir)/tests/all.tcl` $(TESTFLAGS) \
		-load "package ifneeded ${PACKAGE_NAME} ${PACKAGE_VERSION}\
	                [list source `@CYGPATH@ $(srcdir)/library/tclbdd.tcl`]\;[list load `@CYGPATH@ ./$(PKG_LIB_FILE)` $(PACKAGE_NAME)]" \
		-load "package ifneeded ${PACKAGE_NAME}::tclfddd ${PACKAGE_VERSION}\
		    [list source `@CYGPATH@ $(srcdir)/library/tclfddd.tcl`]"

valgrindshell: binaries libraries
	$(TCLSH_ENV) valgrind $(VALGRINDARGS) $(TCLSH_PROG) $(SCRIPT)

depend:

#========================================================================

Changes to library/tclbdd.tcl.

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
# of this file, and for a DISCLAIMER OF ALL WARRANTIES.
#
#------------------------------------------------------------------------------

package require grammar::aycock;	# TEMP - Build parser in advance!
package require grammar::aycock::runtime



namespace eval bdd {

    namespace export system
}






















oo::class create bdd::system {























    method === {exprName1 exprName2} {
	expr {[my beadindex $exprName1] == [my beadindex exprName2]}
    }
    export ===















    method satisfiable {exprName} {
	expr {[my beadindex $exprName] != 0}
    }
















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


















    method support {exprName} {
	set i 0
	set result {}
	foreach k [my profile $exprName] {
	    if {$k != 0} {
		lappend result $i
	    }
	    incr i
	}
    }















    method beadcount {exprName} {
	tcl::mathop::+ {*}[my profile $exprName]
    }
}



































































































































proc bdd::Lexer {script} {
    set lexvals {\n ; ; ; ( ( ) ) = = ? ? : : nor NOR < < <= <=
	== == != != ^ ^ > > >= >= -> <= <- >= <-> == & & | | ~ ~ - - ! ~
	0 constant 1 constant}
    set line 0
    set cpos -1







>
>

>
|
|
>
>
>

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

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




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



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



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










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




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







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
# of this file, and for a DISCLAIMER OF ALL WARRANTIES.
#
#------------------------------------------------------------------------------

package require grammar::aycock;	# TEMP - Build parser in advance!
package require grammar::aycock::runtime

# The 'bdd' namespace contains the entirety of the package

namespace eval bdd {

    namespace export foreach_fullsat system

    # The _fullsat namespace contains coroutines for 'foreach_fullsat'
    # calls in progress.
    namespace eval _fullsat {}

    # The _seq variable is a sequence number for generating unique names
    variable _seq 0
}

# bdd::system --
#
#	Represents a system of BDD's.
#
# Constructed by:
#	bdd::system new
#	bdd::system create NAME
#
# Parameters:
#	name -- Name of the system of BDD's.
#
# The system object supports a great many methods, most of which are
# written in C. Refer to 'generic/tclBdd.c' to find them.

oo::class create bdd::system {

    # Method: ===
    #
    #	Determines whether two BDD's are identical.
    #
    # Usage:
    #	$system === $exprName1 $exprName2
    #
    # Parameters:
    #	system - System of BDD's
    #	exprName1 - Name of the first expression (BDD) to compare
    #   exprName2 - Name of the second expression (BDD) to compare
    #
    # Results:
    #	Returns 1 if the BDD's are identical, 0 otherwise
    #
    # By the canonicity lemma, two BDD's return the same output on all
    # inputs if and only if they are identical.
    #
    # This method is distinguished from == in that == returns a BDD
    # specifying the conditions under which two BDDs give the same
    # output, while === tests whether they give the same output always.

    method === {exprName1 exprName2} {
	expr {[my beadindex $exprName1] == [my beadindex exprName2]}
    }
    export ===

    # Method: satisfiable
    #
    #	Determines whether a BDD representing a Boolean formula is satisfiable
    #
    # Usage:
    #	$system satisfiable $exprName
    #
    # Parameters:
    #	system - System of BDD's
    #   exprName - Name of the expression to test
    #
    # Results:
    #	Returns 1 if the expression is satisfiable, 0 otherwise.

    method satisfiable {exprName} {
	expr {[my beadindex $exprName] != 0}
    }

    # Method: tautology
    #
    #	Determines whether a BDD representing a Boolean formula is 
    #	a tautology - that is, true for all inputs.
    #
    # Usage:
    #	$system tautology $exprName
    #
    # Parameters:
    #	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
    #
    # Usage:
    #	$system support $exprName
    #
    # Parameters:
    #	system - System of BDD's
    #   exprName - Name of the expression to test
    #
    # Results:
    #	Returns a list of integer indices of the variables whose values
    #   can affect the value of the expression. The expression does not
    #   depend on variables not listed in the result.

    method support {exprName} {
	set i 0
	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:
    #	$system beadcount $exprName
    #
    # Parameters:
    #	system - System of BDD's
    #   exprName - Name of the expression to test
    #
    # Results:
    #	Returns the number of beads in the BDD for the given expression.

    method beadcount {exprName} {
	tcl::mathop::+ {*}[my profile $exprName]
    }
}

# bdd::foreach_fullsat --
#
#	Expands a term produced by the 'foreach_sat' method on
#	the 'bdd::system' object to list all combinations of a certain
#	set of variables.
#
# Usage:
#	bdd::foreach_fullsat v varList satterm script
#
# Parameters:
#	v - Name of a variable that will hold a list of values of
#	    the variables in a BDD.
#	varList - List of the integer indices of the variables of
#	          interest. All variables of the BDD must appear in
#		  varList, or else foreach_fullsat will execute
#		  redundant calls.
#	satterm - Term produced by the 'foreach_sat' method. The term
#		  will be represented as a dictionary whose keys are
#		  variable indices and whose values are the Boolean values.
#	script - Script that will be executed once per satisfying combination,
#		 with $v set to a list of Boolean values corresponding to the
#		 variable indices in $varList.
#
# Results:
#	None.
#
# Notes:
#	Within the script, 'break', 'continue' and 'return' have their
#	natural meaning. 'return -level 0 -code 6' may also be useful: it
#	translates to causing the 'foreach_fullsat' construct to return
#	with the 'break' return code. Since 'foreach_fullsat' is normally
#	nested directly inside 'foreach_sat', this return causes both
#	loops to break at once.

proc bdd::foreach_fullsat {v varlist satterm script} {
    variable _seq
    upvar 1 $v var
    set coro [coroutine [namespace current]::_fullsat::[incr _seq] \
		  [namespace which ExpandedSatLauncher] $varlist $satterm]
    try {
	while {[llength [set var [$coro]]] != 0} {
	    try {
		uplevel 1 $script
	    } on error {message options} {
		dict incr $options -level 1
		return -options $options $message
	    } on return {retval options} {
		dict incr $options -level 1
		return -options $options $retval
	    } on break {} {
		break
	    } on continue {} {
		continue
	    } on 6 {} {
		return -code break
	    }
	}
    } finally {
	if {[namespace which $coro] ne {}} {
	    rename $coro {}
	}
    }
}

# bdd::ExpandedSatLauncher --
#
#	Launches a coroutine for expanding a SAT term
#
# Parameters:
#	varList - list of numeric variable indices
#	term - Term to expand
#
# Results:
#	The immediate result is the name of the coroutine.
#	Further results are the rows in the term's truth table.
#	The final result, once all truth table rows are yielded, is the
#	empty list. Upon returning this result, the coroutine terminates.

proc bdd::ExpandedSatLauncher {varlist term} {
    yield [info coroutine]
    ExpandedSat $varlist $term {}
    return {}
}

# bdd::ExpandedSat --
#
#	Recursively expands a SAT term's truth table.
#
# Parameters:
#	varList - List of variables to include in the truth table
#	term - SAT term to expand
#	prefix - Truth table row for variables already expanded.
#
# Results:
#	Yields rows in the truth table. Returns without a result to the
#	caller once the expansion is done.

proc bdd::ExpandedSat {varlist term prefix} {

    # If no variables remain to expand, yield the current truth table row

    if {[llength $varlist] == 0} {
	yield $prefix
	return
    }

    # Pull off one variable to expand

    set restvars [lassign $varlist var]
    if {[dict exists $term $var]} {

	# The term value depends on the variable: make the truth assignment
	# and expand the remaining variables.

	lappend prefix [dict get $term $var]
	ExpandedSat $restvars $term $prefix
    } else {

	# The term value does not depend on the variable. Generate truth
	# table rows for both values of the variable.

	lappend prefix 0
	ExpandedSat $restvars $term $prefix
	lset prefix end 1
	ExpandedSat $restvars $term $prefix

    }
    return
}

proc bdd::Lexer {script} {
    set lexvals {\n ; ; ; ( ( ) ) = = ? ? : : nor NOR < < <= <=
	== == != != ^ ^ > > >= >= -> <= <- >= <-> == & & | | ~ ~ - - ! ~
	0 constant 1 constant}
    set line 0
    set cpos -1

Changes to library/tclfddd.tcl.

1
2
3
4
5
6
7
8
9
10
11
..
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
..
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
..
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
...
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
...
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
...
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
...
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
...
215
216
217
218
219
220
221
























222
#package require tclbdd 0.1

namespace eval fddd {
    namespace export domain interleave concatenate
}

#-----------------------------------------------------------------------------
#
# The next few procedures are for working with domain descriptions, which
# describe a finite, multivalued domain within a BDD. A domain description
# consists of two parts:
................................................................................
#	    represent values in the given domains. The list appears in
#	    order by variable index. It consists of alternating domain
#	    names and bit positions in values in the domain (with
#	    position zero being the least significant bit).
#
#-----------------------------------------------------------------------------

# fddd::domain --
#
#	Defines a new finite domain
#
# Usage:
#	fddd::domain name width ?endian?
#
# Parameters:
#	name - Name of the domain
#	width - Log base 2 of the number of distinct values.
#	endian - 'littleendian' (default) if the values are to be
#		 encoded in BDD's with the least significant bit first.
#		 'bigendian' if they are to be encoded with the most
#		 significant bit first
#
# Results:
#	Returns a domain description.

proc fddd::domain {name width {endian littleendian}} {
    switch -exact -- $endian {
	littleendian {
	    set l {}
	    for {set i 0} {$i < $width} {incr i} {
		lappend l $name $i
	    }
	}
................................................................................
	    return -code error -errorcode [list FDDD BadEndian $endian] \
		"unknown endian \"$endian\": must be bigendian or littleendian"
	}
    }
    return [list [dict create $name $width] $l]
}

# fddd::interleave --
#
#	Interleaves some number of finite domains so that their bit positions
#	in a BDD alternate.
#
# Usage:
#	fddd::interleave ?description...?
#
# Parameters:
#	Zero or more domain descriptions whose bits are to be interleaved.
#	All domains in the descriptions must be distinct.
#
# Results:
#	Returns a domain description of the interleaved domains.
................................................................................
# Errors:
#	{FDDD DuplicateName $name} if any domain is not distinct
#
# The domains are interleaved by taking one bit from the first domain,
# one from the second, and so on. If they are of differing length, then
# the process ceases taking bits from the shorter ones when they run out.

proc fddd::interleave {args} {
    set N 0
    set names {}
    set bits {}
    foreach domain $args {
	dict for {name width} [lindex $domain 0] {
	    if {[dict exists $names $name]} {
		return -code error -errorcode [list FDDD DuplicateName $name] \
		    "domain named \"$name\" appears in multiple places"
	    }
	    incr N $width
	    dict set names $name $width

	    lappend bits [lindex $domain 1]
	}
    }
    set processed 0
    set scrambled {}
    while {$processed < $N} {
	set i 0
	foreach b $bits {
	    if {[llength $b] > 0} {
................................................................................
	    }
	    incr i
	}
    }
    return [list $names $scrambled]
}

# fddd::concatenate --
#
#	Concatenates the descriptions of a set of finite domains
#
# Usage:
#	fddd::concatenate ?description...?
#
# Parameters:
#	Zero or more finite domain descriptions.
#
# Results:
#	Returns a description with the bits of the domains concatenated
#	together.
#
# Errors:
#	{FDDD DuplicateName $name} if any domain is not distinct

proc fddd::concatenate {args} {
    set N 0
    set names {}
    set bits {}
    foreach domain $args {
	dict for {name width} [lindex $domain 0] {
	    if {[dict exists $names $name]} {
		return -code error -errorcode [list FDDD DuplicateName $name] \
................................................................................
    set chain {}
    foreach b $bits {
	lappend chain {*}$b
    }
    return [list $names $chain]
}

# fddd::reader --
#
#	Makes a call to the BDD engine to construct a minterm corresponding
#	to a tuple in a finite domain.
#
# Usage:
#	fddd::reader sysName termName layout domain ?domain...?
#
# Parameters:
#	sysName - Name of the system of BDD's
#	termName - Name of the term to be constructed
#	layout - Description of the finite domain
#	domain - One or more domain names, in the order in which values
#	         will appear in an input tuple.
................................................................................
#
# To the prefix should be appended the values of the domain elements,
# in the order in which their domains appeared on this command.
#
# Example:
#
# set desc \
#     [fddd::concatenate \
#         [fddd::domain var 3 bigendian] \
#         [fddd::interleave \
#             [fddd::domain stmt 5] [fddd::domain stmt2 5]]]
#  set r [fddd::reader sys reads $desc stmt var]
#
# leaves desc set to:
#
#    {var 3 stmt 5 stmt2 5} 
#    {var 2 var 1 var 0 stmt 0 stmt2 0 stmt 1 stmt2 1 stmt 2 stmt2 2 
#     stmt 3 stmt2 3 stmt 4 stmt2 4}
#
................................................................................
# which (when two additional args are catenated on the end), asks the BDD
# system "construct a minterm named 'reads', where variable zero is set from
# parameter 1, the 2**2 bit, variable 1 from parameter 1 the 2**1 bit,
# variable 2 from parameter 1 the 2**0 bit, variable 3 from parameter 0 the
# 2**0 bit, variable 5 from parameter 0 the 2**1 bit ... variable 11 from
# parameter 0 the 2**4 bit."

proc fddd::reader {sysName termName layout args} {
    set i 0
    foreach name $args {
	dict set cmdpos $name $i
	incr i
    }
    set result {}
    set p 0
................................................................................
	}
	incr p
    }
    set cmd [list $sysName load $termName $result]
    return $cmd
}

























package provide tclfddd  0.1
|

|
|







 







|




|












|







 







|





|







 







|











>
|
|







 







|




|











|







 







|





|







 







|
|
|
|
|







 







|







 







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|
1
2
3
4
5
6
7
8
9
10
11
..
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
..
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
..
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
...
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
...
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
...
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
...
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
...
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
package require tclbdd 0.1

namespace eval bdd::fddd {
    namespace export concatenate domain interleave reader support
}

#-----------------------------------------------------------------------------
#
# The next few procedures are for working with domain descriptions, which
# describe a finite, multivalued domain within a BDD. A domain description
# consists of two parts:
................................................................................
#	    represent values in the given domains. The list appears in
#	    order by variable index. It consists of alternating domain
#	    names and bit positions in values in the domain (with
#	    position zero being the least significant bit).
#
#-----------------------------------------------------------------------------

# bdd::fddd::domain --
#
#	Defines a new finite domain
#
# Usage:
#	bdd::fddd::domain name width ?endian?
#
# Parameters:
#	name - Name of the domain
#	width - Log base 2 of the number of distinct values.
#	endian - 'littleendian' (default) if the values are to be
#		 encoded in BDD's with the least significant bit first.
#		 'bigendian' if they are to be encoded with the most
#		 significant bit first
#
# Results:
#	Returns a domain description.

proc bdd::fddd::domain {name width {endian littleendian}} {
    switch -exact -- $endian {
	littleendian {
	    set l {}
	    for {set i 0} {$i < $width} {incr i} {
		lappend l $name $i
	    }
	}
................................................................................
	    return -code error -errorcode [list FDDD BadEndian $endian] \
		"unknown endian \"$endian\": must be bigendian or littleendian"
	}
    }
    return [list [dict create $name $width] $l]
}

# bdd::bdd::fddd::interleave --
#
#	Interleaves some number of finite domains so that their bit positions
#	in a BDD alternate.
#
# Usage:
#	bdd::fddd::interleave ?description...?
#
# Parameters:
#	Zero or more domain descriptions whose bits are to be interleaved.
#	All domains in the descriptions must be distinct.
#
# Results:
#	Returns a domain description of the interleaved domains.
................................................................................
# Errors:
#	{FDDD DuplicateName $name} if any domain is not distinct
#
# The domains are interleaved by taking one bit from the first domain,
# one from the second, and so on. If they are of differing length, then
# the process ceases taking bits from the shorter ones when they run out.

proc bdd::fddd::interleave {args} {
    set N 0
    set names {}
    set bits {}
    foreach domain $args {
	dict for {name width} [lindex $domain 0] {
	    if {[dict exists $names $name]} {
		return -code error -errorcode [list FDDD DuplicateName $name] \
		    "domain named \"$name\" appears in multiple places"
	    }
	    incr N $width
	    dict set names $name $width
	}
	lappend bits [lindex $domain 1]

    }
    set processed 0
    set scrambled {}
    while {$processed < $N} {
	set i 0
	foreach b $bits {
	    if {[llength $b] > 0} {
................................................................................
	    }
	    incr i
	}
    }
    return [list $names $scrambled]
}

# bdd::fddd::concatenate --
#
#	Concatenates the descriptions of a set of finite domains
#
# Usage:
#	bdd::fddd::concatenate ?description...?
#
# Parameters:
#	Zero or more finite domain descriptions.
#
# Results:
#	Returns a description with the bits of the domains concatenated
#	together.
#
# Errors:
#	{FDDD DuplicateName $name} if any domain is not distinct

proc bdd::fddd::concatenate {args} {
    set N 0
    set names {}
    set bits {}
    foreach domain $args {
	dict for {name width} [lindex $domain 0] {
	    if {[dict exists $names $name]} {
		return -code error -errorcode [list FDDD DuplicateName $name] \
................................................................................
    set chain {}
    foreach b $bits {
	lappend chain {*}$b
    }
    return [list $names $chain]
}

# bdd::fddd::reader --
#
#	Makes a call to the BDD engine to construct a minterm corresponding
#	to a tuple in a finite domain.
#
# Usage:
#	bdd::fddd::reader sysName termName layout domain ?domain...?
#
# Parameters:
#	sysName - Name of the system of BDD's
#	termName - Name of the term to be constructed
#	layout - Description of the finite domain
#	domain - One or more domain names, in the order in which values
#	         will appear in an input tuple.
................................................................................
#
# To the prefix should be appended the values of the domain elements,
# in the order in which their domains appeared on this command.
#
# Example:
#
# set desc \
#     [bdd::fddd::concatenate \
#         [bdd::fddd::domain var 3 bigendian] \
#         [bdd::fddd::interleave \
#             [bdd::fddd::domain stmt 5] [bdd::fddd::domain stmt2 5]]]
#  set r [bdd::fddd::reader sys reads $desc stmt var]
#
# leaves desc set to:
#
#    {var 3 stmt 5 stmt2 5} 
#    {var 2 var 1 var 0 stmt 0 stmt2 0 stmt 1 stmt2 1 stmt 2 stmt2 2 
#     stmt 3 stmt2 3 stmt 4 stmt2 4}
#
................................................................................
# which (when two additional args are catenated on the end), asks the BDD
# system "construct a minterm named 'reads', where variable zero is set from
# parameter 1, the 2**2 bit, variable 1 from parameter 1 the 2**1 bit,
# variable 2 from parameter 1 the 2**0 bit, variable 3 from parameter 0 the
# 2**0 bit, variable 5 from parameter 0 the 2**1 bit ... variable 11 from
# parameter 0 the 2**4 bit."

proc bdd::fddd::reader {sysName termName layout args} {
    set i 0
    foreach name $args {
	dict set cmdpos $name $i
	incr i
    }
    set result {}
    set p 0
................................................................................
	}
	incr p
    }
    set cmd [list $sysName load $termName $result]
    return $cmd
}

# bdd::fddd::support --
#
#	Makes a call to the BDD engine to determine the support of a relation
#	in a finite domain
#
# Usage:
#	bdd::fddd::support sysName relationName layout
#
# Parameters:
#	sysName - Name of the system of BDD's
#	relationName - Name of the relation to be analyzed
#	layout - Description of the finite domain
#
# Results:
#	Returns the names of variables on which the relation depends.

proc bdd::fddd::support {sysName relationName layout} {
    set haveVar {}
    foreach bit [$sysName support $relationName] {
	dict set haveVar [lindex $layout 1 [expr {2 * $bit}]] {}
    }
    return [dict keys $haveVar]
}

package provide tclbdd::fddd 0.1

Changes to pkgIndex.tcl.in.

1
2
3
4
5
6


#
# Tcl package index file
#
package ifneeded @PACKAGE_NAME@ @PACKAGE_VERSION@ \
    "[list source [file join $dir @PACKAGE_NAME@.tcl]]\;\
     [list load [file join $dir @PKG_LIB_FILE@] @PACKAGE_NAME@]"








>
>
1
2
3
4
5
6
7
8
#
# Tcl package index file
#
package ifneeded @PACKAGE_NAME@ @PACKAGE_VERSION@ \
    "[list source [file join $dir @PACKAGE_NAME@.tcl]]\;\
     [list load [file join $dir @PKG_LIB_FILE@] @PACKAGE_NAME@]"
package ifneeded @PACKAGE_NAME@::fddd @PACKAGE_VERSION@ \
    [list source [file join $dir tclfddd.tcl]]

Changes to tests/bdd.test.

2832
2833
2834
2835
2836
2837
2838



























































































2839
2840
2841
2842
2843
2844
2845
2846
....
2950
2951
2952
2953
2954
2955
2956
2957
2958
2959
2960
2961
2962
2963
2964
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}




























































































test bdd-30.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
	}
    }
    -body {
................................................................................
	lreverse $sols

    }
    -cleanup {rename sys {}}
    -result {2 04752613 05726314 06357142 06471352 13572064 14602753 14630752 15063724 15720364 16257403 16470352 17502463 20647135 24170635 24175360 24603175 24730615 25147063 25160374 25164073 25307461 25317460 25703641 25704613 25713064 26174035 26175304 27360514 30471625 30475261 31475026 31625704 31625740 31640752 31746025 31750246 35041726 35716024 35720641 36074152 36271405 36415027 36420571 37025164 37046152 37420615 40357162 40731625 40752613 41357206 41362750 41506372 41703625 42057136 42061753 42736051 46027531 46031752 46137025 46152037 46152073 46302751 47302516 47306152 50417263 51602473 51603742 52064713 52073164 52074136 52460317 52470316 52613704 52617403 52630714 53047162 53174602 53602417 53607142 57130642 60275314 61307425 61520374 62057413 62714053 63147025 63175024 64205713 71306425 71420635 72051463 73025164}
}

test bdd-30.2 {verification of a full adder} {
    -setup {
	bdd::system create sys
	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 {







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







 







|







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
....
3041
3042
3043
3044
3045
3046
3047
3048
3049
3050
3051
3052
3053
3054
3055
    }
    -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 {
		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}]
		}
		return [list [expr {$val & 0x7}] [expr {$val >> 3}]]
	    }
	}
    }
    -body {
	x
    }
    -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}]
	    }
	    if {$s eq {0 1 1 0 0 0}} {
		break
	    }
	    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}]
	    }
	    if {$s eq {0 1 1 0 0 0}} {
		continue
	    }
	    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}]
		}
		if {$s eq {0 1 1 0 0 0}} {
		    return -level 0 -code 6
		}
		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
	}
    }
    -body {
................................................................................
	lreverse $sols

    }
    -cleanup {rename sys {}}
    -result {2 04752613 05726314 06357142 06471352 13572064 14602753 14630752 15063724 15720364 16257403 16470352 17502463 20647135 24170635 24175360 24603175 24730615 25147063 25160374 25164073 25307461 25317460 25703641 25704613 25713064 26174035 26175304 27360514 30471625 30475261 31475026 31625704 31625740 31640752 31746025 31750246 35041726 35716024 35720641 36074152 36271405 36415027 36420571 37025164 37046152 37420615 40357162 40731625 40752613 41357206 41362750 41506372 41703625 42057136 42061753 42736051 46027531 46031752 46137025 46152037 46152073 46302751 47302516 47306152 50417263 51602473 51603742 52064713 52073164 52074136 52460317 52470316 52613704 52617403 52630714 53047162 53174602 53602417 53607142 57130642 60275314 61307425 61520374 62057413 62714053 63147025 63175024 64205713 71306425 71420635 72051463 73025164}
}

test bdd-40.2 {verification of a full adder} {
    -setup {
	bdd::system create sys
	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 {

Changes to tests/fddd.test.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
...
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
...
193
194
195
196
197
198
199
200















































































































































































201
202
203
204
# bdd.test --
#
#       Tests for Finite Domain Decision Diagrams (FDDD's)
#
# Copyright (c) 2013 by Kevin B. Kenny.

package require tclbdd

test fddd-1.1 {load minterm - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys load
................................................................................
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test fdd-1.13 {load multiple minterms} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	set result {}
	for {set i 0} {$i < 3} {incr i} {
	    set j [expr {($i + 1) % 4}]
................................................................................
	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}
}
















































































































































































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






|







 







|







 








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




1
2
3
4
5
6
7
8
9
10
11
12
13
14
...
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
...
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
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
# bdd.test --
#
#       Tests for Finite Domain Decision Diagrams (FDDD's)
#
# Copyright (c) 2013 by Kevin B. Kenny.

package require tclbdd::fddd

test fddd-1.1 {load minterm - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys load
................................................................................
    }
    -cleanup {
	sys destroy
    }
    -result {1 {} 2}
}

test fddd-1.12 {load multiple minterms} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	set result {}
	for {set i 0} {$i < 3} {incr i} {
	    set j [expr {($i + 1) % 4}]
................................................................................
	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 3} {a 0 a 1 a 2}} {{b 3} {b 0 b 1 b 2}} {{c 3} {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 3 b 3} {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 3 b 3 c 3} {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 4 b 3 c 2} {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 3 b 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 3 b 3 c 3 d 3} {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 3 b 3 c 3 d 3} {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} {*}{
    -setup {
	bdd::system create sys
	set layout \
	    [bdd::fddd::concatenate \
		 [bdd::fddd::domain a 2] \
		 [bdd::fddd::domain b 2]]
    }
    -body {
	interp alias {} rdr {} {*}[bdd::fddd::reader sys x $layout a]
	rdr 1
	rdr 2
	set result {}
	sys foreach_sat s x {
	    lappend result $s
	}
	sys unset x
	lappend result [sys gc]
	set result
    }
    -cleanup {
	rename rdr {}
	sys destroy
    }
    -result {{0 0 1 1} {0 1 1 0} 2}
}

test fddd-3.2 {reader - 2 columns} {
    -setup {
	bdd::system create sys
	set layout \
	    [bdd::fddd::concatenate \
		 [bdd::fddd::domain a 2 bigendian] \
		 [bdd::fddd::domain b 2 bigendian]]
    }
    -body {
	interp alias {} rdr {} {*}[bdd::fddd::reader sys x $layout a b]
	rdr 1 2
	rdr 2 3
	rdr 3 1
	set result {}
	sys foreach_sat s x {
	    lappend result $s
	}
	sys unset x
	lappend result [sys gc]
	set result
    }
    -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-5.1 {project - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
	sys project
    }
    -cleanup {
	sys destroy
    }
    -result {wrong # args: *}
    -match glob
    -returnCodes error
}

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