OKlibrary  0.2.1.6
Sudoku.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 7.10.2009 (Swansea) */
00002 /* Copyright 2009 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Sudoku.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00025 
00026 kill(f)$
00027 
00028 
00029 /* *************
00030    * Variables *
00031    *************
00032 */
00033 
00034 okltest_var_sdk(f) := (
00035   assert(f(0) = []),
00036   assert(f(1) = [sdk(1,1,1)]),
00037   assert(f(2) = block([N : 2^2], create_list(sdk(i,j,k), i,1,N, j,1,N, k,1,N))),
00038   true)$
00039 
00040 okltest_standardise_sdk(f) := (
00041   for p : 0 thru 2 do
00042     assert(f(var_sdk(p),p) = create_list(i,i,1,(p^2)^3)),
00043   true)$
00044 
00045 okltest_invstandardise_sdk(f) := (
00046   for p : 1 thru 2 do
00047     assert(map(lambda([n],f(n,p)),create_list(i,i,1,(p^2)^3)) = var_sdk(p)),
00048   true)$
00049 
00050 
00051 /* *************************
00052    * The basic translation *
00053    *************************
00054 */
00055 
00056 okltest_sdk_different_rows_cl(f) := (
00057   assert(f(0) = []),
00058   assert(f(1) = []),
00059   /* XXX */
00060   true)$
00061 
00062 okltest_sdk_different_columns_cl(f) := (
00063 
00064   true)$
00065 
00066 okltest_sdk_positions_box(f) := (
00067 
00068   true)$
00069 
00070 okltest_sdk_different_boxes_cl(f) := (
00071 
00072   true)$
00073 
00074 okltest_sdk_all_fields_cl(f) := (
00075 
00076   true)$
00077 
00078 okltest_weak_sdk_fcl(f) := (
00079 
00080   true)$
00081 
00082 
00083 /* **************************
00084    * Additional constraints *
00085    **************************
00086 */
00087 
00088 okltest_sdk_all_rows(f) := (
00089 
00090   true)$
00091 
00092 okltest_sdk_all_columns(f) := (
00093 
00094   true)$
00095 
00096 okltest_sdk_all_boxes(f) := (
00097 
00098   true)$
00099 
00100 okltest_dual_weak_sdk(f) := (
00101 
00102   true)$
00103 
00104 okltest_strong_sdk(f) := (
00105 
00106   true)$
00107 
00108 /* ************
00109    * Measures *
00110    ************
00111 */
00112 
00113 okltest_nvar_sdk(f) := (
00114   for p : 0 thru if oklib_test_level=0 then 2 else 3 do (
00115     assert(f(p) = nvar_fcl(weak_sdk_fcl(p))),
00116     assert(f(p) = nvar_fcl(dual_weak_sdk_fcl(p))),
00117     assert(f(p) = nvar_fcl(strong_sdk_fcl(p)))
00118   ),
00119   true)$
00120 
00121 okltest_ncl_list_weak_sdk_fcl(f) := (
00122   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00123     assert(f(p) = ncl_list_fcl(weak_sdk_fcl(p))),
00124   true)$
00125 
00126 okltest_ncl_list_weak_sdk_fcs(f) := (
00127   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00128     assert(f(p) = ncl_list_fcs(weak_sdk_fcs(p))),
00129   true)$
00130 
00131 okltest_ncl_list_dual_weak_sdk_fcl(f) := (
00132 for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00133     assert(f(p) = ncl_list_fcl(dual_weak_sdk_fcl(p))),
00134   true)$
00135 
00136 okltest_ncl_list_dual_weak_sdk_fcs(f) := (
00137 for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00138     assert(f(p) = ncl_list_fcs(dual_weak_sdk_fcs(p))),
00139   true)$
00140 
00141 okltest_ncl_list_strong_sdk_fcl(f) := (
00142   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00143     assert(f(p) = ncl_list_fcl(strong_sdk_fcl(p))),
00144   true)$
00145 
00146 okltest_ncl_list_strong_sdk_fcs(f) := (
00147   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00148     assert(f(p) = ncl_list_fcs(strong_sdk_fcs(p))),
00149   true)$
00150 
00151 okltest_ncl_weak_sdk_fcl(f) := (
00152   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00153     assert(f(p) = ncl_fcl(weak_sdk_fcl(p))),
00154   true)$
00155 
00156 okltest_ncl_weak_sdk_fcs(f) := (
00157   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00158     assert(f(p) = ncl_fcs(weak_sdk_fcs(p))),
00159   true)$
00160 
00161 okltest_ncl_dual_weak_sdk_fcl(f) := (
00162   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00163     assert(f(p) = ncl_fcl(dual_weak_sdk_fcl(p))),
00164   true)$
00165 
00166 okltest_ncl_dual_weak_sdk_fcs(f) := (
00167   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00168     assert(f(p) = ncl_fcs(dual_weak_sdk_fcs(p))),
00169   true)$
00170 
00171 okltest_ncl_strong_sdk_fcl(f) := (
00172   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00173     assert(f(p) = ncl_fcl(strong_sdk_fcl(p))),
00174   true)$
00175 
00176 okltest_ncl_strong_sdk_fcs(f) := (
00177   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00178     assert(f(p) = ncl_fcs(strong_sdk_fcs(p))),
00179   true)$
00180 
00181 okltest_nlitocc_weak_sdk_fcl(f) := (
00182   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00183     assert(f(p) = nlitocc_fcl(weak_sdk_fcl(p))),
00184   true)$
00185 
00186 okltest_nlitocc_weak_sdk_fcs(f) := (
00187   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00188     assert(f(p) = nlitocc_fcs(weak_sdk_fcs(p))),
00189   true)$
00190 
00191 okltest_nlitocc_dual_weak_sdk_fcl(f) := (
00192   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00193     assert(f(p) = nlitocc_fcl(dual_weak_sdk_fcl(p))),
00194   true)$
00195 
00196 okltest_nlitocc_dual_weak_sdk_fcs(f) := (
00197   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00198     assert(f(p) = nlitocc_fcs(dual_weak_sdk_fcs(p))),
00199   true)$
00200 
00201 okltest_nlitocc_strong_sdk_fcl(f) := (
00202   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00203     assert(f(p) = nlitocc_fcl(strong_sdk_fcl(p))),
00204   true)$
00205 
00206 okltest_nlitocc_strong_sdk_fcs(f) := (
00207   for p : 0 thru if oklib_test_level=0 then 2 else 3 do
00208     assert(f(p) = nlitocc_fcs(strong_sdk_fcs(p))),
00209   true)$
00210 
00211 
00212 /* ********************
00213    * Creating puzzles *
00214    ********************
00215 */
00216 
00217 okltest_sdk_fields_stdcl(f) := (
00218   assert(f([],0) = []),
00219   assert(f([[1,1,1]],1) = [{1}]),
00220   assert(f([[1,1,1]],2) = [{1}]),
00221   assert(f([[1,1,1],[4,4,4]],2) = [{1},{64}]),
00222   assert(f([[9,9,9],[1,1,1]],3) = [{729},{1}]),
00223   true)$
00224 
00225