tclbdd

Check-in [baa39949c5]
Login

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

Overview
Comment:Regularize and streamling FDDD database API. Begin commenting the FDDD database methods.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:baa39949c5407d02835a5c11bcdf7ec91bab6874
User & Date: kbk 2013-12-21 21:51:46
Context
2013-12-23
03:18
Major code cleanup and commentary in tclfddd.tcl. check-in: ba20005fb0 user: kbk tags: trunk
2013-12-21
21:51
Regularize and streamling FDDD database API. Begin commenting the FDDD database methods. check-in: baa39949c5 user: kbk tags: trunk
17:52
Added tests for 'satisfiable' check-in: b18569e814 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to examples/loadProgram.tcl.

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
..
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
	incr bound $bound
    }
    return $bits
}

# Calculates 'reads', 'writes' and 'seq'

proc pass2 {program vars labels} {
    set i 0
    foreach insn $program {
	if {[regexp {^(_[[:alnum:]_]+):$} [lindex $insn 0] label]} {
	    set insn [lrange $insn[set insn {}] 1 end]
	}
	if {[lindex $insn 1] eq {:=}} {
	    lappend writes $i [dict get $vars [lindex $insn 0]]
	    set insn [lrange $insn[set insn {}] 2 end]
	}
	foreach token $insn {
	    if {[regexp {^[[:alpha:]][[:alnum:]_]*$} $token]} {
		lappend reads $i [dict get $vars $token]
	    }
	}
	if {[lindex $insn 0] eq {*GOTO}} {
	    lappend seq $i [dict get $labels [lindex $insn 1]]
	} elseif {[lindex $insn 0] eq {*IF} && [lindex $insn 2] eq {*GOTO}} {
	    lappend seq $i [dict get $labels [lindex $insn 3]] $i [expr {$i+1}]

	} else {
	    lappend seq $i [expr {$i+1}]
	}
	incr i
    }
    return [list $reads $writes $seq]
}
    
proc analyzeProgram {program db} {
    # pass 1 - find variables, resolve labels, calculate domain sizes
    lassign [pass1 $program] vars labels
    set stbits [fdbits [llength $program]]
    set vbits [fdbits [dict size $vars]]
................................................................................
		  [bdd::fddd::domain st2 $stbits bigendian] \
		  [bdd::fddd::domain st3 $stbits bigendian]]]
    
    $db relation reads st v
    $db relation writes st v
    $db relation seq st st2

    # pass 2 - discover 'reads', 'writes', 'seq' relations
    lassign [pass2 $program $vars $labels] reads writes seq

    # TODO - Load incrementally in pass 2
    
    $db load reads $reads
    $db load writes $writes
    $db load seq $seq

    # Return the variable dictionary, since it is not readily recoverable

    return $vars
}







|






|




|



|

|
>

|



|







 







|
|
|
|
|
|
<
<





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
..
90
91
92
93
94
95
96
97
98
99
100
101
102


103
104
105
106
107
	incr bound $bound
    }
    return $bits
}

# Calculates 'reads', 'writes' and 'seq'

proc pass2 {db program vars labels} {
    set i 0
    foreach insn $program {
	if {[regexp {^(_[[:alnum:]_]+):$} [lindex $insn 0] label]} {
	    set insn [lrange $insn[set insn {}] 1 end]
	}
	if {[lindex $insn 1] eq {:=}} {
	    loadWrites $i [dict get $vars [lindex $insn 0]]
	    set insn [lrange $insn[set insn {}] 2 end]
	}
	foreach token $insn {
	    if {[regexp {^[[:alpha:]][[:alnum:]_]*$} $token]} {
		loadReads $i [dict get $vars $token]
	    }
	}
	if {[lindex $insn 0] eq {*GOTO}} {
	    loadSeq $i [dict get $labels [lindex $insn 1]]
	} elseif {[lindex $insn 0] eq {*IF} && [lindex $insn 2] eq {*GOTO}} {
	    loadSeq $i [dict get $labels [lindex $insn 3]] 
	    loadSeq $i [expr {$i+1}]
	} else {
	    loadSeq $i [expr {$i+1}]
	}
	incr i
    }
    return
}
    
proc analyzeProgram {program db} {
    # pass 1 - find variables, resolve labels, calculate domain sizes
    lassign [pass1 $program] vars labels
    set stbits [fdbits [llength $program]]
    set vbits [fdbits [dict size $vars]]
................................................................................
		  [bdd::fddd::domain st2 $stbits bigendian] \
		  [bdd::fddd::domain st3 $stbits bigendian]]]
    
    $db relation reads st v
    $db relation writes st v
    $db relation seq st st2

    interp alias {} loadReads {} {*}[$db loader reads]
    interp alias {} loadWrites {} {*}[$db loader writes]
    interp alias {} loadSeq {} {*}[$db loader seq]

    # pass 2 - discover 'reads', 'writes', 'seq' relations
    pass2 db $program $vars $labels



    # Return the variable dictionary, since it is not readily recoverable

    return $vars
}

Changes to examples/reach.tcl.

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

db relation flowspast v st st2
db relation flowspast' v st st2
db relation reaches v st st2

# Reachability: code that might be generated by a Datalog compiler

proc reachability {db} [subst {

    ### input: reads(st,v)
    ### input: writes(st,v)
    ### input: seq(st,st2)
    ### output: flowspast(v,st,st2)
    ### output: reaches(v,st,st2)

    ### flowspast(v,st,st2) :- seq(st,st2)
    
    [db set t10 _]
    [db join flowspast seq t10]; 		profile \$db flowspast

    ### flowspast(v,st,st2) :- flowspast(v,st,st3),
    ###                        !writes(st3,v),
    ###                        flowspast(v,st3,st2)

    [db replace t11 writes st3 st]; # invariant code hoisted out of loop
    [db set flowspast' {}]
    while {!\[\$db === flowspast flowspast'\]} {
	[db set flowspast' flowspast]
	[db replace t12 flowspast st3 st2];	profile \$db t12
	[db antijoin t13 t12 t11]; 		profile \$db t13
	[db replace t14 flowspast st3 st];	profile \$db t14
	[db join t15 t13 t14];			profile \$db t15
	[db project t16 t15];			profile \$db t16
	[db union flowspast flowspast' t16];	profile \$db flowspast
    }

    ### reaches(v,st,st2) :- writes(st,v),
    ###                      flowspast(v,st,st2),
    ###                      reads(st2,v)

    [db join t17 writes flowspast]; 		profile \$db t17
    [db replace t18 reads st2 st]; 		profile \$db t18
    [db join reaches t17 t18];			profile \$db reaches

}]

#############################################################################

# DATALOG QUERY: reaches(_,_,i)?

db relation q1 st2
db relation q1result v st st2 
proc query1 {db i} [subst {
    [db set q1 {}]
    \$db load q1 \[list \$i\]
    [db join q1result reaches q1]
}]

#############################################################################

# DATALOG QUERY: reaches(_,i,_)?

db relation q2 st
db relation q2result v st st2 
proc query2 {db i} [subst {
    [db set q2 {}]
    \$db load q2 \[list \$i\]
    [db join q2result reaches q2]
}]

#############################################################################

# Report on reachability analysis

reachability db

puts [format {%-16s %2s  %-32s %-16s} PRODUCERS {} INSTRUCTIONS CONSUMERS]
set i 0
foreach stmt $program {

    query1 db $i
    set flowsto {}
    db enumerate result q1result {
	lappend flowsto \
	    [lindex $vars [expr {2*[dict get $result v]}]] \
	    [dict get $result st]
    }

    query2 db $i
    set flowsfrom {}
    db enumerate result q2result {
	lappend flowsfrom \
	    [lindex $vars [expr {2*[dict get $result v]}]] \
	    [dict get $result st2]
    }








|










|







|

|
|
|
|
|
|






|
|
|









|

|









|

|







|





|







|







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

db relation flowspast v st st2
db relation flowspast' v st st2
db relation reaches v st st2

# Reachability: code that might be generated by a Datalog compiler

proc reachability {} [subst {

    ### input: reads(st,v)
    ### input: writes(st,v)
    ### input: seq(st,st2)
    ### output: flowspast(v,st,st2)
    ### output: reaches(v,st,st2)

    ### flowspast(v,st,st2) :- seq(st,st2)
    
    [db set t10 _]
    [db join flowspast seq t10]; 		profile db flowspast

    ### flowspast(v,st,st2) :- flowspast(v,st,st3),
    ###                        !writes(st3,v),
    ###                        flowspast(v,st3,st2)

    [db replace t11 writes st3 st]; # invariant code hoisted out of loop
    [db set flowspast' {}]
    while {!\[[db === flowspast flowspast']\]} {
	[db set flowspast' flowspast]
	[db replace t12 flowspast st3 st2];	profile db t12
	[db antijoin t13 t12 t11]; 		profile db t13
	[db replace t14 flowspast st3 st];	profile db t14
	[db join t15 t13 t14];			profile db t15
	[db project t16 t15];			profile db t16
	[db union flowspast flowspast' t16];	profile db flowspast
    }

    ### reaches(v,st,st2) :- writes(st,v),
    ###                      flowspast(v,st,st2),
    ###                      reads(st2,v)

    [db join t17 writes flowspast]; 		profile db t17
    [db replace t18 reads st2 st]; 		profile db t18
    [db join reaches t17 t18];			profile db reaches

}]

#############################################################################

# DATALOG QUERY: reaches(_,_,i)?

db relation q1 st2
db relation q1result v st st2 
proc query1 {i} [subst {
    [db set q1 {}]
    [db loader q1] \$i
    [db join q1result reaches q1]
}]

#############################################################################

# DATALOG QUERY: reaches(_,i,_)?

db relation q2 st
db relation q2result v st st2 
proc query2 {i} [subst {
    [db set q2 {}]
    [db loader q2] \$i
    [db join q2result reaches q2]
}]

#############################################################################

# Report on reachability analysis

reachability

puts [format {%-16s %2s  %-32s %-16s} PRODUCERS {} INSTRUCTIONS CONSUMERS]
set i 0
foreach stmt $program {

    query1 $i
    set flowsto {}
    db enumerate result q1result {
	lappend flowsto \
	    [lindex $vars [expr {2*[dict get $result v]}]] \
	    [dict get $result st]
    }

    query2 $i
    set flowsfrom {}
    db enumerate result q2result {
	lappend flowsfrom \
	    [lindex $vars [expr {2*[dict get $result v]}]] \
	    [dict get $result st2]
    }

Changes to library/tclfddd.tcl.

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
...
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
...
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
...
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
...
501
502
503
504
505
506
507













































































































508
509
510
511
512
513
514
...
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
636
637
638
639
    set chain {}
    foreach b $bits {
	lappend chain {*}$b
    }
    return [list [Invert $chain] $chain]
}

# bdd::fddd::reader --
#
#	Makes a call to the BDD engine to construct a term 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.
#
# Results:
#	Returns a command prefix for a command that will create a
#	named term containing a 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}
#
# and r set to:
#   sys load reads {0 1 2 1 1 1 2 1 0 3 0 0 5 0 1 7 0 2 9 0 3 11 0 4}
#
# which (when two additional args are catenated on the end), asks the BDD
# system "construct a term 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
    foreach {name bit} [lindex $layout 1] {
	if {[dict exists $cmdpos $name]} {
	    lappend result $p [dict get $cmdpos $name] $bit
	}
	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:
................................................................................
    set haveVar {}
    foreach bit [$sysName support $relationName] {
	dict set haveVar [lindex $layout 1 [expr {2 * $bit}]] {}
    }
    return [dict keys $haveVar]
}









oo::class create bdd::fddd::database {













    variable m_columns m_relcolumns m_variables





    constructor {layout} {
	#puts "LAYOUT: $layout"



	if {[llength $layout] != 2} {
	    if {[string length $layout] > 40} {
		set elayout [string range $layout 0 39]...
	    } else {
		set elayout $layout
	    }
	    return -code error -errorcode [list FDDD NotLayout $layout] \
		"expected a domain layout but found \"$elayout\""
	}



	lassign $layout m_columns m_variables



	set m_relcolumns {}




	bdd::system create [namespace current]::sys
    }

    # TODO - Check domain consistency?
    method === {rel1 rel2} {

	return [sys === $rel1 $rel2]
    }

    export ===









    method Varlist {relation} {
	#puts "What are the variables for $relation?"
	set retval {}
	foreach col [dict get $m_relcolumns $relation] {
	    #puts "$col has variables [dict get $m_columns $col]"
	    lappend retval {*}[dict get $m_columns $col]
	}
	return $retval
    }

    method columns {} {
	return [dict keys $m_columns]




















    }
















































    method set {dest source} {
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
	if {![dict exists $m_relcolumns $source]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $source] \
		"relation \"$source\" is not defined in this database"
	}





	if {[dict get $m_relcolumns $dest]
	    ne [dict get $m_relcolumns $source]} {



	    return -code error \
		-errorcode [list FDDD WrongColumns $dest $source] \
		"relations \"$dest\" and \"$source\" have different columns"


	}
	return [list [namespace which sys] negate $dest $source]
    }
    method antijoin {dest source1 source2} {
	# TODO typecheck
	return [list [namespace which sys] > $dest $source1 $source2]
    }

    # TODO - How can this be streamlined?











































    method enumerate {dictvar relation script} {
	upvar 1 $dictvar valdict


	if {![dict exists $m_relcolumns $relation]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $relation] \
		"relation \"$relation\" is not defined in this database"
	}



	sys foreach_sat satterm $relation {
	    #puts "expand a term of $relation with variables [my Varlist $relation]"
	    bdd::foreach_fullsat vars [my Varlist $relation] $satterm {
		#puts "and values $vars"


		set i 0
		set valdict {}
		foreach column [dict get $m_relcolumns $relation] {
		    set varsForColumn [dict get $m_columns $column]
		    set value 0
		    for {set j 0} {$j < [llength $varsForColumn]} {incr j} {
			set value [expr {$value | ([lindex $vars $i] << $j)}]
			incr i
		    }
		    dict set valdict $column $value
		}


		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
................................................................................
		    continue
		}
	    }
	}
	return
    }














    method forget_relation {name} {

	sys unset $name
	dict unset m_relcolumns $name

	return
    }

    method gc {} {
	return [sys gc]
    }

    method equate {dest col1 col2} {
	if {![dict exists $m_columns $col1]} {
	    return -code error -errorcode [list FDDD NoSuchColumn $col1] \
		"no such column: \"$col1\""












	}
	if {![dict exists $m_columns $col2]} {
	    return -code error -errorcode [list FDDD NoSuchColumn $col2] \
		"no such column: \"$col2\""
	}
	set vars1 [dict get $m_columns $col1]
	set vars2 [dict get $m_columns $col2]
	if {[llength $vars1] != [llength $vars2]} {

	    return -code error \
		-errorcode [list FDDD EquateWrongDomains $col1 $col2] \
		"cannot equate domains \"$col1\" and \"$col2\":\
                 sizes do not match"
	}
	# TODO - Typecheck $dest and sort one list in decreasing order by var#
	sys := $dest 1
	foreach v $vars1 v2 $vars2 {
	    sys nthvar _a $v
	    sys nthvar _b $v2
	    sys == temp _a _b
	    sys & $dest $dest temp
	}
	sys unset temp _a _b
    }



























    method join {dest source1 source2} {
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
................................................................................
		-errorcode [list FDDD BadJoin $destcolumns $destcolumns_sb] \
		"result of the join has columns $destcolumns but the\
                 target relation has columns $destcolumns_sb"
	}
	return [list [namespace which sys] & $dest $source1 $source2]
    }

    method load {name list} {
	if {![dict exists $m_relcolumns $name]} {

	    return -code error \
		-errorcode [list FDDD RelationNotDefined $name] \
		"relation \"$name\" is not defined in this database"
	}


	set nColumns [llength [dict get $m_relcolumns $name]]
	if {[llength $list] % $nColumns != 0} {

	    return -code error \
		-errorcode [list FDDD WrongListLength $nColumns] \
		"list must have a multiple of $nColumns values"
	}

	set reader [bdd::fddd::reader [namespace current]::sys \
			$name [list $m_columns $m_variables] \
			{*}[dict get $m_relcolumns $name]]
	set nCM1 [expr {$nColumns - 1}]

	while {[llength $list] > 0} {
	    {*}$reader {*}[lrange $list 0 $nCM1]
	    set list [lreplace ${list}[set list {}] 0 $nCM1]
	}
	return
    }

    method profile {relation} {
	if {![dict exists $m_relcolumns $relation]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $relation] \
		"relation \"$relation\" is not defined in this database"
	}
	sys profile $relation



    }













    method project {dest source} {
	# columns to project away are determined by dest and source
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
................................................................................
		-errorcode [list FDDD ProjectColumnMissing {*}[dict keys $want]]\
		"columns missing from source relation: [dict keys $want]"
	}
	return [list [namespace which sys] project $dest \
		    [lsort -integer $discards] $source]
	return
    }














































































































    method relation {name args} {
	if {[dict exists $m_relcolumns $name]} {
	    return -code error \
		-errorcode [list FDDD RelationAlreadyDefined $name] \
		"relation \"$name\" is already defined in this database"
	}
................................................................................
	    }
	    lappend fromvars {*}$fv
	    lappend tovars {*}[lrange $tv 0 [expr {[llength $fv] - 1}]]
	}
	return [list [namespace which sys] replace $dest $fromvars $tovars $source]
    }
	    
    method set {dest source} {
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
	if {$source eq {}} {
	    set source 0
	} elseif {$source eq {_}} {
	    set source 1
	} else {
	    if {![dict exists $m_relcolumns $source]} {
		return -code error \
		    -errorcode [list FDDD RelationNotDefined $source] \
		    "relation \"$source\" is not defined in this database"
	    }
	    if {[dict get $m_relcolumns $dest]
		ne [dict get $m_relcolumns $source]} {
		return -code error \
		    -errorcode [list FDDD WrongColumns $dest $source] \
		    "relations \"$dest\" and \"$source\" have different columns"
	    }
	}
	return [list [namespace which sys] := $dest $source]
    }

    method union {dest source1 source2} {
	# TODO typecheck
	return [list [namespace which sys] | $dest $source1 $source2]
    }
}

package provide tclbdd::fddd 0.1







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







 







>
>
>
>
>
>
>
>


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


>
>
>
>

<
>
>
>









>
>
>

>
>
>

>
>
>
>



|
<
>
|
<
>
|
>
|
>
>
>
>
>
>
>

<


<





<
<
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|
>
>
>
>
>
|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|





|

|
|

>
>
>
>
>
|
|
>
>
>

|
<
>
>

<
|
<
<



<
>
|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>


>
>





>
>
>

<

<
>
>











>
>







 







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



|
<
<
|
<
<
<
<
>
>
>
>
>
>
>
>
>
>
>
>
|
<
<
<
<
<
<
<
>
|
<
<
<
|
<
<
<
<
<
<
<
|
<
<
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







 







|
<
>
|
|
<
<
>
>
|
<
>
|
|
|
<
>
|
|
|
<
>
|
|
<
|
<
<
<
|





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







 







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







 







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








175
176
177
178
179
180
181
182































































183
184
185
186
187
188
189
...
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
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
...
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
...
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
...
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
...
847
848
849
850
851
852
853

























854
855
856
857
858
859
860
861
    set chain {}
    foreach b $bits {
	lappend chain {*}$b
    }
    return [list [Invert $chain] $chain]
}

if 0 { # this needs to be a method of the database
































































# bdd::fddd::support --
#
#	Makes a call to the BDD engine to determine the support of a relation
#	in a finite domain
#
# Usage:
................................................................................
    set haveVar {}
    foreach bit [$sysName support $relationName] {
	dict set haveVar [lindex $layout 1 [expr {2 * $bit}]] {}
    }
    return [dict keys $haveVar]
}

}

# Class: bdd::fddd::database
#
#	Class that represents a database containing relations whose
#       columns belong to finite domains. The database is held in a
#	system of Binary Decision Diagrams (BDD's).

oo::class create bdd::fddd::database {

    # m_columns is a dictionary whose keys are columns and whose values are
    #           lists of BDD variables that represent the column values.
    #
    # m_relcolumns is a dictionary whose keys are the relations known to
    #              the database and whose values are lists of columns that
    #              participate in the relations.
    #
    # m_variables is a list of alternating column names and bit positions.
    #             Variable number i in the BDD system represents
    #             the 2**[lindex $m_variables [expr {2*$i+1}]] bit of
    #	          the column whose name is [lindex $m_variables [expr {2*$i}]]
    
    variable m_columns m_relcolumns m_variables

    # The constructor accepts aes its sole parameter a domain layout
    # that is computed by some series of calls to bdd::fddd::domain,
    # bdd::fddd::interleave and bdd::fddd::concatenate.

    constructor {layout} {

	
	# Make sure that the layout contains two sublists

	if {[llength $layout] != 2} {
	    if {[string length $layout] > 40} {
		set elayout [string range $layout 0 39]...
	    } else {
		set elayout $layout
	    }
	    return -code error -errorcode [list FDDD NotLayout $layout] \
		"expected a domain layout but found \"$elayout\""
	}

	# Unpack the sublists into 'm_columns' and 'm_variables'

	lassign $layout m_columns m_variables

	# There are no relations defined yet.

	set m_relcolumns {}

	# Create the underlying system of BDD's in the current object's
	# namespace.

	bdd::system create [namespace current]::sys
    }

    # Private method: Varlist

    #	
    #	Enumerates the BDD variables that make up a relation.

    #
    # Usage:
    #	$db Varlist $relation
    #
    # Parameters:
    #	relation - Name of the relation being processed.
    #
    # Results:
    # 	Returns a list of the BDD variables for all the columns of the
    #	relation.

    method Varlist {relation} {

	set retval {}
	foreach col [dict get $m_relcolumns $relation] {

	    lappend retval {*}[dict get $m_columns $col]
	}
	return $retval
    }



    # Method: ===
    #
    #	Generates code to test whether two relations are equal: that is,
    #	contain exactly the same rows.
    #
    # Usage:
    #	$db === $rel1 $rel2
    #
    # Parameters:
    #	rel1 - First relation to test
    #   rel2 - Second relation to test
    #
    # Results:
    #	Returns a command that will evaluate to 1 if the relations
    #   are equal and 0 if they are not.
    #
    # This method does not perform the test directly: it generates
    # code to perform the test.
    #
    # The test executes in constant time.

    method === {rel1 rel2} {
	if {![dict exists $m_relcolumns $rel1]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $rel1] \
		"relation \"$rel1\" is not defined in this database"
	}
	if {![dict exists $m_relcolumns $rel2]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $rel2] \
		"relation \"$rel2\" is not defined in this database"
	}
	if {[dict get $m_relcolumns $rel1]
	    ne [dict get $m_relcolumns $rel2]} {
	    return -code error \
		-errorcode [list FDDD WrongColumns $rel1 $rel2] \
		"relations \"$rel1\" and \"$rel2\" have different columns"
	}
	return [list [namespace which sys] === $rel1 $rel2]
    }
    export ===

    # Method: antijoin
    #
    #	Generates code to antijoin a pair of relations
    #
    # Usage:
    #	$db antijoin dest source1 source2
    #
    # Results:
    #	Returns a fragment of code that will perform the antijoin.
    #
    # The result of the antijoin is the set of rows that are
    # members of the $source relation but not members of the $dest
    # relation. This is well defined for any two relations: if either
    # relation contains excess columns, the other relation is presumed
    # to contain tuples with every possible value in those columns.
    # Of course, the excess columns may be projected away before or
    # after the antijoin. Most commonly, the columns of $source2 will
    # all appear in $source1.
    #
    # The result will have the union of the columns of the two inputs.
    #
    # This method does not perform the copy directly: it generates
    # code to perform the copy.
    #
    # The antijoin executes in time proportional to the size of the
    # source1 BDD.

    method antijoin {dest source1 source2} {
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
	if {![dict exists $m_relcolumns $source1]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $source1] \
		"relation \"$source1\" is not defined in this database"
	}
	if {![dict exists $m_relcolumns $source2]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $source2] \
		"relation \"$source2\" is not defined in this database"
	}
	set destcolumns [dict get $m_relcolumns $source1]
	lappend destcolumns {*}[dict get $m_relcolumns $source2]
	set destcolumns [lsort -ascii -unique $destcolumns]
	set destcolumns_sb [dict get $m_relcolumns $dest]
	if {$destcolumns ne $destcolumns_sb} {
	    return -code error \
		-errorcode [list FDDD BadJoin $destcolumns $destcolumns_sb] \

		"result of the antijoin has columns $destcolumns but the\
                 target relation has columns $destcolumns_sb"
	}




	return [list [namespace which sys] > $dest $source1 $source2]
    }


    # Method: columns
    #
    #	Enumerates all columns in the database
    #
    # Usage:
    #	$db columns
    #
    # Results:
    #	Returns a list of the column names that are known to the databsae.

    method columns {} {
	return [dict keys $m_columns]
    }

    # Method: enumerate
    #
    #	Iterates over all the tuples in a relation
    #
    # Usage:
    #	$db enumerate dictvar relation { script }
    #
    # Parameters:
    #	dictvar - Variable that will receive a dictionary whose keys
    #		  are column names are whose values are the values in
    #		  the given columns
    #	relation - Name of the relation to iterate over
    #   script -   Script to execute on each tuple.
    #
    # Results:
    #	None.
    #
    # This call iterates over the given relation. For each row that is
    # found, the given variable is set to a dictionary containing the rows
    # values, and the given script is evaluated.
    #
    # If evaluating the script causes an error, the iteration is terminated.
    # If the script performs a return, the return has its natural meaning.
    # If the script performs a break or continue, the iteration is
    # terminated (for a break) or recommences with the next tuple
    # (for a continue).
    # [return -code 6] is synonymous with [break]
    # Any other nonstandard status code terminates the iteration.

    method enumerate {dictvar relation script} {
	upvar 1 $dictvar valdict

	# Make sure the relation exists
	if {![dict exists $m_relcolumns $relation]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $relation] \
		"relation \"$relation\" is not defined in this database"
	}

	# Iterate over the relation, getting SAT terms. Iterate over
	# the variable assignments that satisfy the terms.
	sys foreach_sat satterm $relation {

	    bdd::foreach_fullsat vars [my Varlist $relation] $satterm {


		# Iterate over the columns and populate the dictionary
		set i 0
		set valdict {}
		foreach column [dict get $m_relcolumns $relation] {
		    set varsForColumn [dict get $m_columns $column]
		    set value 0
		    for {set j 0} {$j < [llength $varsForColumn]} {incr j} {
			set value [expr {$value | ([lindex $vars $i] << $j)}]
			incr i
		    }
		    dict set valdict $column $value
		}

		# Evaluate the script and handle the status returns
		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
................................................................................
		    continue
		}
	    }
	}
	return
    }

    # Method: forget
    #
    #	Removes relations from the database
    #
    # Usage:
    #	db forget ?relation...?
    #
    # Parameters:
    #	relation... - Names of relations to remove
    #
    # Results:
    #	None.

    method forget_relation {args} {
	foreach name $args {
	    sys unset $name
	    dict unset m_relcolumns $name
	}
	return
    }

    # Method: gc


    #




    #	Garbage collects the database
    #
    # Usage:
    #	$db gc
    #
    # Results:
    #	Returns the number of beads in the BDD system after garbage collection
    #
    # This method should not ordinarily be called; the incremental garbage
    # collector is faster than the mark and sweep done by this call. This call
    # exists for leak checking, making sure that all beads are reclaimed after
    # a unit test.








    method gc {} {
	return [sys gc]



    }










    # Method: join
    #
    #	Generates code to join a pair of relations
    #
    # Usage:
    #	$db join dest source1 source2
    #
    # Results:
    #	Returns a fragment of code that will perform the join.
    #
    # The result of the join is the set of rows that are
    # members of the $source relation but not members of the $dest
    # relation. This is well defined for any two relations: if either
    # relation contains excess columns, the other relation is presumed
    # to contain tuples with every possible value in those columns.
    # Of course, the excess columns may be projected away before or
    # after the join. Most commonly, the columns of $source2 will
    # all appear in $source1.
    #
    # The result will have the union of the columns of the two inputs.
    #
    # This method does not perform the copy directly: it generates
    # code to perform the copy.
    #
    # The join executes in time proportional to the size of the
    # source1 BDD.

    method join {dest source1 source2} {
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
................................................................................
		-errorcode [list FDDD BadJoin $destcolumns $destcolumns_sb] \
		"result of the join has columns $destcolumns but the\
                 target relation has columns $destcolumns_sb"
	}
	return [list [namespace which sys] & $dest $source1 $source2]
    }

    # Method: loader

    #
    #	Generates code to call the BDD engine to construct a term 
    #   corresponding to a tuple in a finite domain.


    #
    # Usage:
    #	$db loader relation

    #
    # Parameters:
    #   db - Name of the database
    #   relation - Name of the relation being loaded

    #
    # Results:
    #	Returns a command prefix for a command that will add a tuple
    #	to the given relation.

    #
    # To the prefix should be appended the values of the columns,
    # in [lsort -ascii] order by the colun names.





    method loader {relation} {
	if {![dict exists $m_relcolumns $relation]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $relation] \
		"relation \"$relation\" is not defined in this database"
	}
	set i 0
	foreach column [dict get $m_relcolumns $relation] {
	    dict set cmdpos $column $i
	    incr i
	}
	set result {}
	set p 0
	foreach {column bit} $m_variables {
	    if {[dict exists $cmdpos $column]} {
		lappend result $p [dict get $cmdpos $column] $bit
	    }
	    incr p
	}
	set cmd [list [namespace which sys] load $relation $result]
	return $cmd
    }


    method project {dest source} {
	# columns to project away are determined by dest and source
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
................................................................................
		-errorcode [list FDDD ProjectColumnMissing {*}[dict keys $want]]\
		"columns missing from source relation: [dict keys $want]"
	}
	return [list [namespace which sys] project $dest \
		    [lsort -integer $discards] $source]
	return
    }

    # Method: set
    #
    #	Generates code to copy one relation to another
    #
    # Usage:
    #	$db set $dest $source
    #
    # Parameters:
    #	dest   - Name of the output relation
    #	source - Name of the input relation
    #
    # Results:
    #	Returns a command that will make the first relation a copy of
    #	the second.
    #
    # The source may be one of the special values:
    #	{} - (The empty string) - generates a relation with no rows.
    #	_  - generates a relation containin every combination of column
    #        values.
    #
    # This method does not perform the copy directly: it generates
    # code to perform the copy.
    #
    # The copy executes in constant time.

    method set {dest source} {
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
	if {$source eq {}} {
	    set source 0
	} elseif {$source eq {_}} {
	    set source 1
	} else {
	    if {![dict exists $m_relcolumns $source]} {
		return -code error \
		    -errorcode [list FDDD RelationNotDefined $source] \
		    "relation \"$source\" is not defined in this database"
	    }
	    if {[dict get $m_relcolumns $dest]
		ne [dict get $m_relcolumns $source]} {
		return -code error \
		    -errorcode [list FDDD WrongColumns $dest $source] \
		    "relations \"$dest\" and \"$source\" have different columns"
	    }
	}
	return [list [namespace which sys] := $dest $source]
    }

    method equate {dest col1 col2} {
	if {![dict exists $m_columns $col1]} {
	    return -code error -errorcode [list FDDD NoSuchColumn $col1] \
		"no such column: \"$col1\""
	}
	if {![dict exists $m_columns $col2]} {
	    return -code error -errorcode [list FDDD NoSuchColumn $col2] \
		"no such column: \"$col2\""
	}
	set vars1 [dict get $m_columns $col1]
	set vars2 [dict get $m_columns $col2]
	if {[llength $vars1] != [llength $vars2]} {
	    return -code error \
		-errorcode [list FDDD EquateWrongDomains $col1 $col2] \
		"cannot equate domains \"$col1\" and \"$col2\":\
                 sizes do not match"
	}
	# TODO - Typecheck $dest and sort one list in decreasing order by var#
	sys := $dest 1
	foreach v $vars1 v2 $vars2 {
	    sys nthvar _a $v
	    sys nthvar _b $v2
	    sys == temp _a _b
	    sys & $dest $dest temp
	}
	sys unset temp _a _b
    }

    method load {name list} {
	if {![dict exists $m_relcolumns $name]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $name] \
		"relation \"$name\" is not defined in this database"
	}
	set nColumns [llength [dict get $m_relcolumns $name]]
	if {[llength $list] % $nColumns != 0} {
	    return -code error \
		-errorcode [list FDDD WrongListLength $nColumns] \
		"list must have a multiple of $nColumns values"
	}
	set reader [my loader $name]
	set nCM1 [expr {$nColumns - 1}]
	while {[llength $list] > 0} {
	    {*}$reader {*}[lrange $list 0 $nCM1]
	    set list [lreplace ${list}[set list {}] 0 $nCM1]
	}
	return
    }

    method profile {relation} {
	if {![dict exists $m_relcolumns $relation]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $relation] \
		"relation \"$relation\" is not defined in this database"
	}
	sys profile $relation
    }

    method relation {name args} {
	if {[dict exists $m_relcolumns $name]} {
	    return -code error \
		-errorcode [list FDDD RelationAlreadyDefined $name] \
		"relation \"$name\" is already defined in this database"
	}
................................................................................
	    }
	    lappend fromvars {*}$fv
	    lappend tovars {*}[lrange $tv 0 [expr {[llength $fv] - 1}]]
	}
	return [list [namespace which sys] replace $dest $fromvars $tovars $source]
    }
	    


























    method union {dest source1 source2} {
	# TODO typecheck
	return [list [namespace which sys] | $dest $source1 $source2]
    }
}

package provide tclbdd::fddd 0.1

Changes to tests/fddd.test.

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
...
618
619
620
621
622
623
624

625
626
627
628
629
630
631
632
		 [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} {*}{

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







>







 







>







 







>








303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
...
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
...
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
		 [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]]
    }
................................................................................
	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]]
    }
................................................................................
	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: