tclbdd

Check-in [2cbd4f3ba6]
Login

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

Overview
Comment:Add 8-queens example as a test.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:2cbd4f3ba636b5f1ce707741c0542f9d5855398f
User & Date: kennykb 2013-11-30 16:34:15
Context
2013-11-30
17:38
add circuit verification example check-in: 1513a7c798 user: kennykb tags: trunk
16:34
Add 8-queens example as a test. check-in: 2cbd4f3ba6 user: kennykb tags: trunk
04:28
Added missing bddInt.h (whoops\!). Added code for AllSat - no Tcl support yet, so entirely untested. check-in: b11e4e2f87 user: kennykb tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to tests/bdd.test.

829
830
831
832
833
834
835
































































































836
837
838
839
840
841
842
	list [dict size [sys dump r0]] [format %llx [sys satcount r0]]
    }
    -cleanup {
	rename sys {}
    }
    -result {257 80000000000000000000000000000000}
}

































































































test bdd-13.n {restrict - reduce to constant} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2







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







829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
	list [dict size [sys dump r0]] [format %llx [sys satcount r0]]
    }
    -cleanup {
	rename sys {}
    }
    -result {257 80000000000000000000000000000000}
}

test bdd-12.12 {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 {

	set result {}

	sys constant solution 1

	# iterate through the cells

	for {set row 0} {$row < 8} {incr row} {
	    sys constant thisRowC 1
	    for {set col 7} {$col >= 0} {incr col -1} {
		sys constant cellC 1
		set q1 v[expr {8* $row + $col}]

		# queen here <= no other queen in the same column

		sys constant columnC 1
		for {set col2 7} {$col2 >= 0} {incr col2 -1} {
		    if {$col2 != $col} {
			set q2 v[expr {8 * $row + $col2}]
			sys & columnC columnC !$q2
		    }
		}
		sys <= columnC $q1 columnC
		sys & cellC cellC columnC
		
		# queen here <= no other queen in the same row

		sys constant rowC 1
		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
		    if {$row2 != $row} {
			set q2 v[expr {8 * $row2 + $col}]
			sys & rowC rowC !$q2
		    }
		}
		sys <= rowC $q1 rowC
		sys & cellC cellC rowC

		# queen here <= no other queen in the same diagonal

		sys constant diag1C 1
		sys constant diag2C 1
		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
		    if {$row2 != $row} {
			set col2 [expr {$col + $row2 - $row}]
			if {$col2 >= 0 && $col2 < 8} {
			    set q2 v[expr {8 * $row2 + $col2}]
			    sys & diag1C diag1C !$q2
			}
			set col2 [expr {$col + $row - $row2}]
			if {$col2 >= 0 && $col2 < 8} {
			    set q2 v[expr {8 * $row2 + $col2}]
			    sys & diag2C diag2C !$q2
			}
		    }
		}
		sys <= diag1C $q1 diag1C
		sys & cellC cellC diag1C

		sys <= diag2C $q1 diag2C
		sys & cellC cellC diag2C

		# accumulate into the constraint set for the row

		sys & thisRowC thisRowC cellC
	    }

	    # accumulate all constraints for a row into the solution

	    sys & solution solution thisRowC
	}
		
	# at least one queen in each column
	for {set col 0} {$col < 8} {incr col} {
	    sys constant columnC 0
	    for {set row 0} {$row < 8} {incr row} {
		set q v[expr {8*$row + $col}]
		sys | columnC columnC $q
	    }
	    sys & solution solution columnC
	}

	sys satcount solution

    }
    -cleanup {rename sys {}}
    -result 92
}

test bdd-13.n {restrict - reduce to constant} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2