tclbdd

Check-in [bd3c0053ea]
Login

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

Overview
Comment:added != to datalog, and extended tclfddd to support it.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:bd3c0053ea93e24c101937db99e3048e1346d6cb
User & Date: kbk 2014-01-14 00:35:38
Context
2014-07-01
03:26
Begin writing a man page for tclbdd, and make some comments truthful check-in: 780b74afbb user: kbk tags: trunk
2014-01-14
00:35
added != to datalog, and extended tclfddd to support it. check-in: bd3c0053ea user: kbk tags: trunk
2014-01-10
13:52
Add prelude/postlude to code generation to reduce the temptation of global vars. Fix FDDD code gen for equalities, which was using the wrong namespace. check-in: 88561d8ac3 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to library/datalog.tcl.

184
185
186
187
188
189
190






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




250
251
252
253
254
255
256
...
400
401
402
403
404
405
406

407
408
409
410
411
412
413
414
...
678
679
680
681
682
683
684

685
686
687
688
689
690
691
692
...
740
741
742
743
744
745
746

747
748
749
750
751
752
753
754
...
966
967
968
969
970
971
972

973
974
975
976
977
978
979
980
981
...
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
....
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
....
1261
1262
1263
1264
1265
1266
1267




1268
1269
1270
1271
1272
1273
1274
    }

    equality	::=	variable = variable
    {
	list EQUALITY [list VARIABLE [lindex $_ 0]] \
	    [list VARIABLE [lindex $_ 2]]
    }







    # A predicate symbol is either a bare identifier or a quoted string

    predicate_symbol ::= IDENTIFIER			{}
    predicate_symbol ::= STRING				{}

    # A term is either a variable or a constant
................................................................................
}
proc bdd::datalog::prettyprint-subgoal {subgoal} {
    switch -exact [lindex $subgoal 0] {
	EQUALITY {
	    set s [prettyprint-variable [lindex $subgoal 1]]
	    append s = [prettyprint-variable [lindex $subgoal 2]]
	}




	NOT {
	    set s !
	    append s [prettyprint-literal [lindex $subgoal 1]]
	}
	LITERAL {
	    set s [prettyprint-literal $subgoal]
	}
................................................................................

	# Examine the subgoals on the right hand side

	set i 0
	foreach subgoal [lrange $rule 1 end] {
	    incr i
	    switch -exact -- [lindex $subgoal 0] {

		EQUALITY { 	# does not create a dependency
		    continue
		}
		LITERAL {
		    set dependency [lindex $subgoal 1]
		    set not 0
		}
		NOT {
................................................................................

    method rankComponentMembers {component loops} {
	set delta {}
	foreach rule $loops {
	    set lhPredicate [lindex $rule 0 1]
	    foreach subgoal [lrange $rule 1 end] {
		switch -exact -- [lindex $subgoal 0] {

		    EQUALITY {	# does not introduce a dependency
			continue
		    }
		    NOT {
			set rhPredicate [lindex $subgoal 1 1]
		    }
		    LITERAL {
			set rhPredicate [lindex $subgoal 1]
................................................................................
    # Results:
    #	Returns 2 if the rule depends on one of the predicates in negated
    #   form, 1, if the rule depends on one of the predicates only in
    #   non-negated form, 0 if the rule has no dependency on the predicates

    method subgoalDependsOn {subgoal predicates} {
	switch -exact -- [lindex $subgoal 0] {

	    EQUALITY {
		return 0
	    }
	    NOT {
		if {[my subgoalDependsOn [lindex $subgoal 1] $predicates]} {
		    return 2
		} else {
		    return 0
................................................................................
		lassign \
		    [my translateLiteral $db \
			 [lindex $subgoal 1] $dataSoFar $columnsSoFar] \
		    subgoalRelation subgoalColumns
		tailcall my translateSubgoalEnd $db ANTIJOIN \
		    $dataSoFar $columnsSoFar $subgoalRelation $subgoalColumns
	    }

	    EQUALITY {
		tailcall my translateEquality $db \
		    [lindex $subgoal 1] [lindex $subgoal 2] \
		    $dataSoFar $columnsSoFar
	    }
	    LITERAL {
		lassign \
		    [my translateLiteral \
			 $db $subgoal $dataSoFar $columnsSoFar] \
................................................................................
	    }
	    default {
		error "in translateSubgoal: can't happen"
	    }
	}
    }

    method translateEquality {db var1 var2 dataSoFar columnsSoFar} {
	set col1 [lindex $var1 1]
	set col2 [lindex $var2 1]
	set equality [my gensym #T]
	lappend intcode \
	    [list RELATION $equality [list $col1 $col2]] \
	    [list EQUALITY $equality $col1 $col2]
	if {$dataSoFar eq {}} {
	    return [list $equality [list $col1 $col2]]
	} else {
	    set joined [my gensym #T]
	    lappend columnsSoFar $col1 $col2
	    set columnsSoFar [lsort -dictionary -unique $columnsSoFar]
	    lappend intcode \
		[list RELATION $joined $columnsSoFar] \
................................................................................
	set prologue \n
	set body \n
	set epilogue \n

	set ind0 {    }
	set ind {    }

	#append body $ind {puts {Start evaluation!}} \n
	foreach instr $icode {
	    # append body $ind [list puts $instr] \n
	    switch -exact -- [lindex $instr 0] {
		RELATION {
		    $db relation [lindex $instr 1] {*}[lindex $instr 2]
		    append prologue $ind0 [$db set [lindex $instr 1] {}] \n
		    append epilogue $ind0 [$db set [lindex $instr 1] {}] \n
		}
		
................................................................................
		    set ind [string replace $ind end-3 end]
		    append body $ind "\}" \n
		}
		EQUALITY {
		    append body $ind \
			[$db equate {*}[lrange $instr 1 end]] \n
		}




		JOIN {
		    append body $ind \
			[$db join {*}[lrange $instr 1 end]] \n
		}
		LOAD {
		    # append body $ind # $instr \n
		    set relation [lindex $instr 1]







>
>
>
>
>
>







 







>
>
>
>







 







>
|







 







>
|







 







>
|







 







>
|
|







 







|





|
|







 







<

<







 







>
>
>
>







184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
...
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
...
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
...
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
...
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
...
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
...
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
....
1246
1247
1248
1249
1250
1251
1252

1253

1254
1255
1256
1257
1258
1259
1260
....
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
    }

    equality	::=	variable = variable
    {
	list EQUALITY [list VARIABLE [lindex $_ 0]] \
	    [list VARIABLE [lindex $_ 2]]
    }

    equality	::=	variable ! = variable
    {
	list INEQUALITY [list VARIABLE [lindex $_ 0]] \
	    [list VARIABLE [lindex $_ 3]]
    }

    # A predicate symbol is either a bare identifier or a quoted string

    predicate_symbol ::= IDENTIFIER			{}
    predicate_symbol ::= STRING				{}

    # A term is either a variable or a constant
................................................................................
}
proc bdd::datalog::prettyprint-subgoal {subgoal} {
    switch -exact [lindex $subgoal 0] {
	EQUALITY {
	    set s [prettyprint-variable [lindex $subgoal 1]]
	    append s = [prettyprint-variable [lindex $subgoal 2]]
	}
	INEQUALITY {
	    set s [prettyprint-variable [lindex $subgoal 1]]
	    append s != [prettyprint-variable [lindex $subgoal 2]]
	}
	NOT {
	    set s !
	    append s [prettyprint-literal [lindex $subgoal 1]]
	}
	LITERAL {
	    set s [prettyprint-literal $subgoal]
	}
................................................................................

	# Examine the subgoals on the right hand side

	set i 0
	foreach subgoal [lrange $rule 1 end] {
	    incr i
	    switch -exact -- [lindex $subgoal 0] {
		EQUALITY -
		INEQUALITY { 	# does not create a dependency
		    continue
		}
		LITERAL {
		    set dependency [lindex $subgoal 1]
		    set not 0
		}
		NOT {
................................................................................

    method rankComponentMembers {component loops} {
	set delta {}
	foreach rule $loops {
	    set lhPredicate [lindex $rule 0 1]
	    foreach subgoal [lrange $rule 1 end] {
		switch -exact -- [lindex $subgoal 0] {
		    EQUALITY - 
		    INEQUALITY {	# does not introduce a dependency
			continue
		    }
		    NOT {
			set rhPredicate [lindex $subgoal 1 1]
		    }
		    LITERAL {
			set rhPredicate [lindex $subgoal 1]
................................................................................
    # Results:
    #	Returns 2 if the rule depends on one of the predicates in negated
    #   form, 1, if the rule depends on one of the predicates only in
    #   non-negated form, 0 if the rule has no dependency on the predicates

    method subgoalDependsOn {subgoal predicates} {
	switch -exact -- [lindex $subgoal 0] {
	    EQUALITY -
	    INEQUALITY {
		return 0
	    }
	    NOT {
		if {[my subgoalDependsOn [lindex $subgoal 1] $predicates]} {
		    return 2
		} else {
		    return 0
................................................................................
		lassign \
		    [my translateLiteral $db \
			 [lindex $subgoal 1] $dataSoFar $columnsSoFar] \
		    subgoalRelation subgoalColumns
		tailcall my translateSubgoalEnd $db ANTIJOIN \
		    $dataSoFar $columnsSoFar $subgoalRelation $subgoalColumns
	    }
	    EQUALITY -
	    INEQUALITY {
		tailcall my translateEquality $db [lindex $subgoal 0] \
		    [lindex $subgoal 1] [lindex $subgoal 2] \
		    $dataSoFar $columnsSoFar
	    }
	    LITERAL {
		lassign \
		    [my translateLiteral \
			 $db $subgoal $dataSoFar $columnsSoFar] \
................................................................................
	    }
	    default {
		error "in translateSubgoal: can't happen"
	    }
	}
    }

    method translateEquality {db operation var1 var2 dataSoFar columnsSoFar} {
	set col1 [lindex $var1 1]
	set col2 [lindex $var2 1]
	set equality [my gensym #T]
	lappend intcode \
	    [list RELATION $equality [list $col1 $col2]] \
	    [list $operation $equality $col1 $col2]
	if {$columnsSoFar eq {}} {
	    return [list $equality [list $col1 $col2]]
	} else {
	    set joined [my gensym #T]
	    lappend columnsSoFar $col1 $col2
	    set columnsSoFar [lsort -dictionary -unique $columnsSoFar]
	    lappend intcode \
		[list RELATION $joined $columnsSoFar] \
................................................................................
	set prologue \n
	set body \n
	set epilogue \n

	set ind0 {    }
	set ind {    }


	foreach instr $icode {

	    switch -exact -- [lindex $instr 0] {
		RELATION {
		    $db relation [lindex $instr 1] {*}[lindex $instr 2]
		    append prologue $ind0 [$db set [lindex $instr 1] {}] \n
		    append epilogue $ind0 [$db set [lindex $instr 1] {}] \n
		}
		
................................................................................
		    set ind [string replace $ind end-3 end]
		    append body $ind "\}" \n
		}
		EQUALITY {
		    append body $ind \
			[$db equate {*}[lrange $instr 1 end]] \n
		}
		INEQUALITY {
		    append body $ind \
			[$db inequality {*}[lrange $instr 1 end]] \n
		}
		JOIN {
		    append body $ind \
			[$db join {*}[lrange $instr 1 end]] \n
		}
		LOAD {
		    # append body $ind # $instr \n
		    set relation [lindex $instr 1]

Changes to library/tclfddd.tcl.














1
2
3
4
5
6
7
...
646
647
648
649
650
651
652








































































653
654
655
656
657
658
659













package require tclbdd 0.1

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

#-----------------------------------------------------------------------------
................................................................................
    # a unit test.
    #
    # This method executes directly, rather than returning a code fragment

    method gc {} {
	return [sys gc]
    }









































































    # Method: join
    #
    #	Generates code to join a pair of relations
    #
    # Usage:
    #	$db join dest source1 source2
>
>
>
>
>
>
>
>
>
>
>
>
>







 







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







1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
...
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
# tclfddd.tcl --
#
#	Class definitions and Tcl-level methods for the bdd::fddd package:
#	Binary Decision Diagram (BDD) implementation of Finite Domain
#	Decision Diagrams (FDDD's).
#
# Copyright (c) 2014 by Kevin B. Kenny
#
# See the file "license.terms" for information on usage and redistribution
# of this file, and for a DISCLAIMER OF ALL WARRANTIES.
#
#------------------------------------------------------------------------------

package require tclbdd 0.1

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

#-----------------------------------------------------------------------------
................................................................................
    # a unit test.
    #
    # This method executes directly, rather than returning a code fragment

    method gc {} {
	return [sys gc]
    }

    # Method: inequality
    #
    #	Generates code for an inequality constraint 
    #
    # Usage:
    #	db inequality dest col1 col2
    #
    # Parameters:
    #	dest - Name of a relation that will contain one row for each
    #          value in its domain that has col1 != col2
    #   col1 - Name of the first column to compare
    #   col2 - Name of the second column to compare
    #
    # Results:
    #	Returns a fragment of code that creates the given relation.
    #
    # The destination relation must contain both col1 and col2 as columns.
    # The domains of col1 and col2 must have the same size.
    #
    # This method does not create the inequality relation; it returns a fragment
    # of code that does it.
    #
    # The time taken to create the inequality is highly variable. In the case
    # where the two columns' variables are interleaved, the time is linear
    # in the number of bits of the domains. In the case where they are
    # concatenated, both time and space are exponential in the number of
    # variables. Other orderings will give results between these two extremes.

    method inequality {dest col1 col2} {
	my relationMustExist $dest
	my columnMustExist $col1
	my columnMustExist $col2
	set destcolumns [dict get $m_relcolumns $dest]
	if {[lsearch -exact $destcolumns $col1] == -1} {
	    return -code error -errorcode \
		[list FDDD RelationDoesNotContainColumn $dest $col1] \
		"relation \"$dest\" does not contain column \"$col1\""
	}
	if {[lsearch -exact $destcolumns $col2] == -1} {
	    return -code error -errorcode \
		[list FDDD RelationDoesNotContainColumn $dest $col1] \
		"relation \"$dest\" does not contain column \"$col1\""
	}
	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"
	}

	# Sort the variables in descending order by the first column's
	# positions. This will keep them ordered well for the rename in
	# the easy cases.

	set vlist {}
	foreach v $vars1 v2 $vars2 {
	    lappend vlist $v $v2
	}
	set vlist [lsort -stride 2 -integer -index 0 -decreasing $vlist]
	set code [list [namespace which sys] := $dest 0]
	foreach {v v2} $vlist {
	    append code \; [list [namespace which sys] nthvar :a $v]
	    append code \; [list [namespace which sys] nthvar :b $v2]
	    append code \; [list [namespace which sys] != :t :a :b]
	    append code \; [list [namespace which sys] | $dest $dest :t]
	}
	append code \; [list [namespace which sys] unset :a :b :t]
	return $code
    }

    # Method: join
    #
    #	Generates code to join a pair of relations
    #
    # Usage:
    #	$db join dest source1 source2