OKlibrary  0.2.1.6
Statistics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 4.4.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2011, 2012 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/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/tests/HashMaps.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00028 
00029 kill(f)$
00030 
00031 /* ******************
00032    * Basic measures *
00033    ******************
00034 */
00035 
00036 okltest_nvar_cs(f) := (
00037   assert(f({}) = 0),
00038   assert(f({{}}) = 0),
00039   assert(f({{1},{-1},{2,3},{-2,-1}}) = 3),
00040   true)$
00041 
00042 okltest_nvar_ocs(f) := (
00043   assert(f([]) = 0),
00044   assert(f([{}]) = 0),
00045   assert(okltest_nvar_cs(buildq([f],lambda([F],f(cs2ocs(F)))))),
00046   true)$
00047 
00048 okltest_nvar_cl(f) := (
00049   assert(f([]) = 0),
00050   assert(f([{}]) = 0),
00051   assert(f([{1},{1},{},{-1},{}]) = 1),
00052   assert(okltest_nvar_ocs(f)),
00053   true)$
00054 
00055 
00056 okltest_nvar_fcs(f) := (
00057   assert(f([{},{}]) = 0),
00058   assert(f([{},{{}}]) = 0),
00059   assert(f([{1,2},{}]) = 2),
00060   assert(okltest_nvar_cs(buildq([f],lambda([F],f(cs2fcs(F)))))),
00061   true)$
00062 
00063 okltest_nvar_fcl(f) := (
00064   assert(okltest_nvar_fcs(buildq([f],lambda([FF],f(fcs2fcl(FF)))))),
00065   assert(f([[],[{},{}]]) = 0),
00066   true)$
00067 
00068 okltest_nvar_ofcs(f) := (
00069   assert(okltest_nvar_fcs(buildq([f],lambda([FF],f(fcs2ofcs(FF)))))),
00070   true)$
00071 
00072 okltest_ncl_fcs(f) := (
00073   /* XXX */
00074   true)$
00075 
00076 okltest_ncl_fcl(f) := (
00077   /* XXX */
00078   true)$
00079 
00080 okltest_ncl_cs(f) := (
00081   /* XXX */
00082   true)$
00083 
00084 okltest_ncl_cl(f) := (
00085   /* XXX */
00086   true)$
00087 
00088 okltest_nlitocc_cl(f) := (
00089   assert(f([]) = 0),
00090   assert(f([{}]) = 0),
00091   assert(f([{1},{-1}]) = 2),
00092   assert(f([{1},{},{1,2},{-2,3}]) = 5),
00093   assert(f([{},{1},{},{1},{1,2},{-2,3},{2,1}]) = 8),
00094   true)$
00095 
00096 okltest_nlitocc_cs(f) := (
00097   assert(f({}) = 0),
00098   assert(f({{}}) = 0),
00099   assert(f({{1},{-1}}) = 2),
00100   assert(f({{1},{},{1,2},{-2,3}}) = 5),
00101   true)$
00102 
00103 okltest_nlitocc_fcl(f) := (
00104   assert(f([[],[]]) = 0),
00105   assert(f([[1],[{},{1},{1},{-1},{}]]) = 3),
00106   assert(okltest_nlitocc_cl(buildq([f],lambda([F],f(cl2fcl(F))))) = true),
00107   true)$
00108 
00109 okltest_nlitocc_fcs(f) := block([x,y,z],
00110   assert(okltest_nlitocc_cs(buildq([f],lambda([F],f(cs2fcs(F))))) = true),
00111   assert(okltest_nlitocc_cs(buildq([f],lambda([F],f([union(var_cs(F),{x,y,z}),F])))) = true),
00112   true)$
00113 
00114 okltest_ncl_list_fcl(f) := (
00115   assert(f([[],[]]) = []),
00116   assert(f([[1,2,3],[]]) = []),
00117   assert(f([[],[{},{}]]) = [[0,2]]),
00118   assert(f([[1,3,5],[{},{}]]) = [[0,2]]),
00119   assert(okltest_ncl_list_fcs(buildq([f], lambda([FF],f(fcs2fcl(FF))))) = true),
00120   true)$
00121 
00122 okltest_ncl_list_fcs(f) := (
00123   assert(f([{},{}]) = []),
00124   assert(f([{},{{}}]) = [[0,1]]),
00125   assert(f([{1},{{},{1},{-1}}]) = [[0,1],[1,2]]),
00126   assert(f([{1},{{1},{-1}}]) = [[1,2]]),
00127   assert(f([{1,2},{{1},{-1,2},{1,-2}}]) = [[1,1],[2,2]]),
00128   for n : 0 thru 3 do
00129     assert(f(full_fcs(n)) = [[n,2^n]]),
00130   true)$
00131 
00132 okltest_ncl_list_cl(f) := (
00133   assert(okltest_ncl_list_fcl(buildq([f], lambda([FF],f(fcl2cl(FF))))) = true),
00134   true)$
00135 
00136 okltest_ncl_list_cs(f) := (
00137   assert(okltest_ncl_list_fcs(buildq([f], lambda([FF],f(fcs2cs(FF))))) = true),
00138   true)$
00139 
00140 okltest_max_rank_cs(f) := (
00141   assert(f({}) = -1),
00142   assert(f({{}}) = 0),
00143   assert(f({{1,2}}) = 2),
00144   assert(f({{1,2},{}}) = 2),
00145   assert(f({{1,2},{1},{-1,-2,-3}}) = 3),
00146   true)$
00147 
00148 okltest_max_rank_fcs(f) := block([x,y,z],
00149   assert(okltest_max_rank_cs(buildq([f],lambda([F],f(cs2fcs(F))))) = true),
00150   assert(okltest_max_rank_cs(buildq([f],lambda([F],f([union(var_cs(F),{x,y,z}),F])))) = true),
00151   true)$
00152 
00153 okltest_min_rank_cs(f) := (
00154   assert(f({}) = inf),
00155   assert(f({{}}) = 0),
00156   assert(f({{1,2}}) = 2),
00157   assert(f({{1,2},{}}) = 0),
00158   assert(f({{1,2},{1},{-1,-2,-3}}) = 1),
00159   true)$
00160 
00161 okltest_min_rank_fcs(f) := (
00162   assert(okltest_min_rank_cs(buildq([f],lambda([F],f(cs2fcs(F))))) = true),
00163   assert(okltest_min_rank_cs(buildq([f],lambda([F],f([union(var_cs(F),{x,y,z}),F])))) = true),
00164   true)$
00165 
00166 okltest_uniformcsp(f) := (
00167   /* XXX */
00168   true)$
00169 
00170 
00171 /* *******************
00172    * Literal degrees *
00173    *******************
00174 */
00175 
00176 okltest_literal_degree_cs(f) := block(
00177   assert(f({},1) = 0),
00178   assert(f({{}},1) = 0),
00179   assert(f({{1}},1) = 1),
00180   assert(f({{1}},-1) = 0),
00181   assert(f({{1}},2) = 0),
00182   assert(f({{1},{-1}},1) = 1),
00183   assert(f({{1},{-1}},-1) = 1),
00184   block([F : {{-3,-2,-1},{-3,1},{-2,3},{-1,2},{1,2,3}}],
00185     for i : 1 thru 3 do (
00186       assert(f(F,i) = 2),
00187       assert(f(F,-i) = 2)
00188   )),
00189   true)$
00190 
00191 okltest_literal_degrees_cs(f) := block(
00192   assert(eq_hmsm_p(f({}),{}) = true),
00193   assert(eq_hmsm_p(f({{}}),{}) = true),
00194   assert(eq_hmsm_p(f({{1}}),{[1,1]}) = true),
00195   assert(eq_hmsm_p(f({{1},{-1}}),{[1,1],[-1,1]}) = true),
00196   assert(eq_hmsm_p(f({{1},{-1},{}}),{[1,1],[-1,1]}) = true),
00197   assert(eq_hmsm_p(f({{1},{-1},{},{2,1}}),{[1,2],[-1,1],[2,1]}) = true),
00198   true)$
00199 
00200 okltest_literal_degrees_cl(f) := block(
00201   assert(hm2sm(f([])) = {}),
00202   assert(hm2sm(f([{}])) = {}),
00203   assert(hm2sm(f([{1},{1}])) = {[1,2]}),
00204   assert(okltest_literal_degrees_cs(buildq([f],lambda([F],f(cs2cl(F))))) = true),
00205   true)$
00206 
00207 okltest_literal_degrees_fcs(f) := block(
00208   assert(eq_hmsm_p(f([{},{}]),{}) = true),
00209   assert(eq_hmsm_p(f([{1},{}]),{[1,0],[-1,0]}) = true),
00210   assert(eq_hmsm_p(f([{1},{{}}]),{[1,0],[-1,0]}) = true),
00211   assert(eq_hmsm_p(f([{1},{{1}}]),{[1,1],[-1,0]}) = true),
00212   assert(eq_hmsm_p(f([{1},{{1},{-1}}]),{[1,1],[-1,1]}) = true),
00213   true)$
00214 
00215 okltest_ordered_literal_degrees_cs(f) := block(
00216   assert(f({}) = []),
00217   assert(f({{}}) = []),
00218   assert(f({{1}}) = [[1,1]]),
00219   assert(f({{-1}}) = [[-1,1]]),
00220   assert(f({{1},{-1}}) = [[-1,1],[1,1]]),
00221   assert(f({{1},{-1},{}}) = [[-1,1],[1,1]]),
00222   assert(f({{1,2},{-1},{-2},{-1,2}}) = [[-1,2],[2,2],[-2,1],[1,1]]),
00223   assert(f({{1,2},{1},{1,2,3}}) = [[1,3],[2,2],[3,1]]),
00224 true)$
00225 
00226 okltest_ordered_literal_degrees_fcs(f) := block(
00227   assert(f([{},{}]) = []),
00228   assert(f([{1},{}]) = [[-1,0],[1,0]]),
00229   assert(f([{},{{}}]) = []),
00230   assert(f([{1},{{}}]) = [[-1,0],[1,0]]),
00231   assert(f([{1},{{1}}]) = [[1,1],[-1,0]]),
00232   assert(f([{1,2},{{1}}]) = [[1,1],[-2,0],[-1,0],[2,0]]),
00233   assert(f([{1},{{-1}}]) = [[-1,1],[1,0]]),
00234   assert(f([{1},{{1},{-1}}]) = [[-1,1],[1,1]]),
00235   assert(f([{1},{{1},{-1},{}}]) = [[-1,1],[1,1]]),
00236   assert(f([{1,2},{{1,2},{-1},{-2},{-1,2}}]) = [[-1,2],[2,2],[-2,1],[1,1]]),
00237   assert(f([{1,2,3},{{1,2},{1},{1,2,3}}]) = [[1,3],[2,2],[3,1],[-3,0],[-2,0],[-1,0]]),
00238 true)$
00239 
00240 okltest_min_literal_degree_cs(f) := (
00241   assert(f({}) = inf),
00242   assert(f({{}}) = inf),
00243   assert(f({{1}}) = 1),
00244   assert(f({{1},{-1}}) = 1),
00245   assert(f({{1},{1,2}}) = 1),
00246   for n : 1 thru 3 do
00247     assert(f(full_fcs(n)[2]) = 2^(n-1)),
00248   true)$
00249 
00250 okltest_min_literal_degree_fcs(f) := (
00251   /* XXX */
00252   true)$
00253 
00254 okltest_max_literal_degree_cs(f) := (
00255   assert(f({}) = minf),
00256   assert(f({{}}) = minf),
00257   assert(f({{1}}) = 1),
00258   assert(f({{1},{-1}}) = 1),
00259   assert(f({{1},{1,2}}) = 2),
00260   for n : 1 thru 3 do
00261     assert(f(full_fcs(n)[2]) = 2^(n-1)),
00262   true)$
00263 
00264 okltest_max_literal_degree_fcs(f) := (
00265   /* XXX */
00266   true)$
00267 
00268 okltest_min_literal_degree_l_cs(f) := block(
00269   assert(f({}) = [inf,0]),
00270   assert(f({{}}) = [inf,0]),
00271   assert(f({{1}}) = [1,1]),
00272   assert(elementp(f({{1},{-1}}), {[1,1],[1,-1]}) = true),
00273   assert(f({{},{1},{1,2}}) = [1,2]),
00274   true)$
00275 
00276 okltest_max_literal_degree_l_cs(f) := block(
00277   assert(f({}) = [minf,0]),
00278   assert(f({{}}) = [minf,0]),
00279   assert(f({{1}}) = [1,1]),
00280   assert(elementp(f({{1},{-1}}), {[1,1],[1,-1]}) = true),
00281   assert(f({{},{1},{1,2}}) = [2,1]),
00282   true)$
00283 
00284 okltest_max_literal_degree_l_cl(f) := (
00285   assert(f([]) = [minf,0]),
00286   assert(f([{}]) = [minf,0]),
00287   assert(f([{-1},{-1},{2}]) = [2,-1]),
00288   assert(okltest_max_literal_degree_l_cs(buildq([f],lambda([F],f(cs2cl(F))))) = true),
00289   true)$
00290 
00291 okltest_literalregularcsp(f) := (
00292   /* XXX */
00293   true)$
00294 
00295 okltest_mean_literal_degree_fcs(f) := (
00296   /* XXX */
00297   true)$
00298 
00299 okltest_min_literal_frequency_cs(f) := (
00300   /* XXX */
00301   true)$
00302 
00303 okltest_max_literal_frequency_cs(f) := (
00304   /* XXX */
00305   true)$
00306 
00307 okltest_mean_literal_frequency_cs(f) := (
00308   /* XXX */
00309   true)$
00310 
00311 okltest_literal_degrees_list_fcs(f) := block(
00312   assert(f([{},{}]) = []),
00313   assert(f([{},{{}}]) = []),
00314   assert(f([{1,2},{}]) = [[0,4]]),
00315   assert(f([{1,2},{{}}]) = [[0,4]]),
00316   assert(f([{1},{{},{1}}]) = [[0,1],[1,1]]),
00317   assert(f([{1},{{},{1},{-1}}]) = [[1,2]]),
00318   assert(f([{1,2},{{},{1},{-1}}]) = [[0,2],[1,2]]),
00319   assert(f([setn(4),{{-4,-3},{-4,-1,2,3},{-4,1,2,3},{-3,-2,4},{-2,-1,3},{-2,1,3},{2,4}}]) = [[2,4],[3,3],[4,1]]),
00320   for n : 0 thru 3 do
00321     assert(f(full_fcs(n)) = if n=0 then [] else [[2^(n-1),2*n]]),
00322   true)$
00323 
00324 okltest_max_literal_degree_tb(f) := (
00325   /* XXX */
00326   true)$
00327 
00328 okltest_max_literal_degree_tb_l_cs(f) := (
00329   /* XXX */
00330   true)$
00331 
00332 
00333 /* ********************
00334    * Variable degrees *
00335    ********************
00336 */
00337 
00338 okltest_variable_degree_cs(f) := block(
00339   assert(f({},1) = 0),
00340   assert(f({{}},1) = 0),
00341   assert(f({{1}},1) = 1),
00342   assert(f({{1}},-1) = 0),
00343   assert(f({{1}},2) = 0),
00344   assert(f({{1},{-1}},1) = 2),
00345   block([F : {{-3,-2,-1},{-3,1},{-2,3},{-1,2},{1,2,3}}],
00346     for i : 1 thru 3 do
00347       assert(f(F,i) = 4)),
00348   true)$
00349 
00350 okltest_variable_degrees_cs(f) := block(
00351   assert(eq_hmsm_p(f({}),{}) = true),
00352   assert(eq_hmsm_p(f({{}}),{}) = true),
00353   assert(eq_hmsm_p(f({{1}}),{[1,1]}) = true),
00354   assert(eq_hmsm_p(f({{1},{-1}}),{[1,2]}) = true),
00355   assert(eq_hmsm_p(f({{1},{-1},{}}),{[1,2]}) = true),
00356   assert(eq_hmsm_p(f({{1},{-1},{},{2,1}}),{[1,3],[2,1]}) = true),
00357   true)$
00358 
00359 okltest_min_variable_degree_cs(f) := (
00360   assert(f({}) = inf),
00361   assert(f({{}}) = inf),
00362   assert(f({{1}}) = 1),
00363   assert(f({{1},{-1}}) = 2),
00364   assert(f({{1},{1,2}}) = 1),
00365   for n : 1 thru 3 do
00366     assert(f(full_fcs(n)[2]) = 2^n),
00367   true)$
00368 
00369 okltest_min_variable_degree_fcs(f) := (
00370   /* XXX */
00371   true)$
00372 
00373 okltest_min_variable_degree_v_cs(f) := (
00374   assert(f({}) = [inf,0]),
00375   assert(f({{}}) = [inf,0]),
00376   assert(f({{1},{}}) = [1,1]),
00377   assert(f({{-1},{}}) = [1,1]),
00378   assert(f({{1},{-2},{}}) = [1,1]),
00379   assert(f({{1},{-1},{2},{-2},{1,2}}) = [3,1]),
00380   assert(f({{2},{1},{-1}}) = [1,2]),
00381   true)$
00382 
00383 okltest_max_min_var_deg_cs(f) := (
00384   /* XXX */
00385   true)$
00386 
00387 okltest_max_variable_degree_fcs(f) := (
00388   /* XXX */
00389   true)$
00390 
00391 okltest_max_variable_degree_cs(f) := (
00392   assert(f({}) = minf),
00393   assert(f({{}}) = minf),
00394   assert(f({{1}}) = 1),
00395   assert(f({{1},{-1}}) = 2),
00396   assert(f({{1},{1,2}}) = 2),
00397   for n : 1 thru 3 do
00398     assert(f(full_fcs(n)[2]) = 2^n),
00399   true)$
00400 
00401 okltest_max_variable_degree_v_cs(f) := block(
00402   assert(f({}) = [minf,0]),
00403   assert(f({{}}) = [minf,0]),
00404   assert(f({{1}}) = [1,1]),
00405   assert(f({{1},{-1}}) = [2,1]),
00406   assert(f({{},{1},{1,2}}) = [2,1]),
00407   assert(f({{},{-1},{1,2}}) = [2,1]),
00408   true)$
00409 
00410 okltest_min_max_var_deg_cs(f) := (
00411   /* XXX */
00412   true)$
00413 
00414 okltest_variableregularcsp(f) := (
00415   /* XXX */
00416   true)$
00417 
00418 okltest_mean_variable_degree_cs(f) := (
00419   /* XXX */
00420   true)$
00421 
00422 okltest_min_variable_frequency_cs(f) := (
00423   /* XXX */
00424   true)$
00425 
00426 okltest_max_variable_frequency_cs(f) := (
00427   /* XXX */
00428   true)$
00429 
00430 okltest_mean_variable_frequency_cs(f) := (
00431   /* XXX */
00432   true)$
00433 
00434 okltest_variable_degrees_list_cs(f) := block(
00435   assert(f({}) = []),
00436   assert(f({{}}) = []),
00437   assert(f({{},{1}}) = [[1,1]]),
00438   assert(f({{},{1},{-1}}) = [[2,1]]),
00439   assert(f({{},{1},{-1}}) = [[2,1]]),
00440   assert(f({{-4,-3},{-4,-1,2,3},{-4,1,2,3},{-3,-2,4},{-2,-1,3},{-2,1,3},{2,4}}) = [[4,1],[5,1],[6,2]]),
00441   for n : 0 thru 3 do
00442     assert(f(full_fcs(n)[2]) = if n=0 then [] else [[2^n,n]]),
00443   true)$
00444 
00445 okltest_full_variables_cs(f) := (
00446   assert(f({{}}) = {}),
00447   assert(f({{1}}) = {1}),
00448   assert(f({{1},{-1}}) = {1}),
00449   assert(f({{1},{2}}) = {}),
00450   true)$
00451 
00452 okltest_full_variables_fcs(f) := block([X],
00453   assert(f([{},{}]) = {}),
00454   assert(f([X,{}]) = X),
00455   assert(okltest_full_variables_cs(buildq([f],lambda([F],f(cs2fcs(F))))) = true),
00456   true)$
00457 
00458 okltest_full_var_csp(f) := (
00459   assert(f({}) = false),
00460   assert(f({{}}) = false),
00461   assert(f({{1}}) = true),
00462   assert(f({{1},{-1}}) = true),
00463   assert(f({{1},{2}}) = false),
00464   true)$
00465 
00466 okltest_full_var_fcsp(f) := (
00467   assert(f([{},{}]) = false),
00468   assert(f([{1},{}]) = true),
00469   assert(okltest_full_var_csp(buildq([f],lambda([F],f(cs2fcs(F))))) = true),
00470   true)$
00471 
00472 okltest_singularpure_variables_cs(f) := (
00473   assert(f({}) = {}),
00474   assert(f({{}}) = {}),
00475   assert(f({{1}}) = {1}),
00476   assert(f({{-1}}) = {1}),
00477   assert(f({{1},{-1}}) = {1}),
00478   assert(f({{1,2}}) = {1,2}),
00479   assert(f({{1,2},{-1,2}}) = {1,2}),
00480   true)$
00481 
00482 okltest_singular_variables_cs(f) := (
00483   assert(f({}) = {}),
00484   assert(f({{}}) = {}),
00485   assert(f({{1}}) = {}),
00486   assert(f({{-1}}) = {}),
00487   assert(f({{1},{-1}}) = {1}),
00488   assert(f({{1,2}}) = {}),
00489   assert(f({{1,2},{-1,2}}) = {1}),
00490   assert(f({{1,2},{-1,2},{-2,1}}) = {1,2}),
00491   assert(f({{1,2},{-1,2},{-2,1},{-1,-2}}) = {}),
00492   true)$
00493 
00494 okltest_singular_variables_fcs(f) := (
00495   assert(f([{},{}]) = {}),
00496   assert(f([{},{{}}]) = {}),
00497   assert(f([{1},{}]) = {}),
00498   assert(f([{1},{{}}]) = {}),
00499   assert(f([{1},{{1}}]) = {}),
00500   assert(f([{1},{{1},{-1}}]) = {1}),
00501   assert(okltest_singular_variables_cs(buildq([f], lambda([F],f(cs2fcs(F))))) = true),
00502   true)$
00503 
00504 okltest_onesingular_variables_fcs(f) := (
00505   assert(f([{},{}]) = {}),
00506   assert(f([{},{{}}]) = {}),
00507   assert(f([{1},{}]) = {}),
00508   assert(f([{1},{{}}]) = {}),
00509   assert(f([{1},{{1}}]) = {}),
00510   assert(f([{1},{{1},{-1}}]) = {1}),
00511   assert(okltest_onesingular_variables_cs(buildq([f], lambda([F],f(cs2fcs(F))))) = true),
00512   true)$
00513 
00514 okltest_onesingular_variables_cs(f) := (
00515   assert(f({}) = {}),
00516   assert(f({{}}) = {}),
00517   assert(f({{1}}) = {}),
00518   assert(f({{-1}}) = {}),
00519   assert(f({{1},{-1}}) = {1}),
00520   assert(f({{1,2}}) = {}),
00521   assert(f({{1,2},{-1,2}}) = {1}),
00522   assert(f({{1,2},{-1,2},{-2,1}}) = {}),
00523   assert(f({{1,2},{-1,2},{-2,1},{-1,-2}}) = {}),
00524   assert(f({{1},{-1},{2},{-2},{3,4},{-3,-4},{5,6},{-5,6},{5,-6}}) = {1,2,3,4}),
00525   true)$
00526 
00527 okltest_nononesingular_variables_fcs(f) := (
00528   assert(f([{},{}]) = {}),
00529   assert(f([{},{{}}]) = {}),
00530   assert(f([{1},{}]) = {}),
00531   assert(f([{1},{{}}]) = {}),
00532   assert(f([{1},{{1}}]) = {}),
00533   assert(f([{1},{{1},{-1}}]) = {}),
00534   assert(f([{1,2},{{1},{-1,2},{-1,-2}}]) = {1}),
00535   assert(okltest_nononesingular_variables_cs(buildq([f], lambda([F],f(cs2fcs(F))))) = true),
00536   true)$
00537 
00538 okltest_nononesingular_variables_cs(f) := (
00539   assert(f({}) = {}),
00540   assert(f({{}}) = {}),
00541   assert(f({{1}}) = {}),
00542   assert(f({{-1}}) = {}),
00543   assert(f({{1},{-1}}) = {}),
00544   assert(f({{1,2}}) = {}),
00545   assert(f({{1,2},{-1,2}}) = {}),
00546   assert(f({{1,2},{-1,2},{-2,1}}) = {1,2}),
00547   assert(f({{1,2},{-1,2},{-2,1},{-1,-2}}) = {}),
00548   assert(f({{1},{-1},{2},{-2},{3,4},{-3,-4},{5,6},{-5,6},{5,-6}}) = {5,6}),
00549   true)$
00550 
00551 okltest_sortvar_prodocc_cs(f) := (
00552   assert(f({}) = []),
00553   assert(f({{}}) = []),
00554   assert(f({{1}}) = [1]),
00555   assert(f({{1},{-1},{2}}) = [2,1]),
00556   assert(f({{1,2},{-1,2},{1,-2}}) = [1,2]),
00557   assert(f({{1,2,3},{-1},{-2,-3},{-1,-2},{3}}) = [1,2,3]),
00558   assert(f({{1,2,3},{-1},{-2,-3},{-1,-2},{3},{2,3}}) = [1,3,2]),
00559   assert(f({{1,2,3},{-1},{-2,-3},{-1,-2},{3},{2,3},{-1,3}}) = [1,2,3]),
00560   assert(f({{1,2,3},{-1},{-2,-3},{-1,-2},{3},{2,3},{-1,3},{1}}) = [2,3,1]),
00561   true)$
00562 
00563 
00564 /* **********************
00565    * Numbers of clauses *
00566    **********************
00567 */
00568 
00569 okltest_nfcl_fcl(f) := (
00570   assert(f([[],[]]) = 0),
00571   assert(f([[],[{}]]) = 1),
00572   assert(f([[],[{},{}]]) = 2),
00573   assert(f([[1],[{}]]) = 0),
00574   assert(f([[1],[{1},{},{-1},{1},{},{-1}]]) = 4),
00575   assert(f([[1,2],[{1,2},{-1,2},{2}]]) = 2),
00576   assert(f([[1,2,3],[{1,2},{-1,2},{2}]]) = 0),
00577   assert(okltest_nfcl_cs(buildq([f], lambda([F], f(cs2fcl(F))))) = true),
00578   true)$
00579 
00580 okltest_nfcl_cs(f) := (
00581   assert(f({}) = 0),
00582   assert(f({{}}) = 1),
00583   assert(f({{1},{-1},{}}) = 2),
00584   assert(f({{1,2},{3},{-1},{1,2,3}}) = 1),
00585   true)$
00586 
00587 okltest_weighted_ncl_2n_cs(f) := (
00588   assert(f({}) = 0),
00589   assert(f({{}}) = 1),
00590   assert(f({{1}}) = 1/2),
00591   assert(f({{-1}}) = 1/2),
00592   assert(f({{1},{-1}}) = 1),
00593   assert(f({{1,2}}) = 1/4),
00594   assert(f({{1,2},{-1,2}}) = 1/2),
00595   assert(f({{1,2},{-1,2}, {1,-2}}) = 3/4),
00596   for k : 0 thru 5 do
00597     assert(f({setn(k)}) = 2^(-k)),
00598   assert(f({{},{1},{1,2}}) = 7/4),
00599   true)$
00600 
00601 okltest_weighted_ncl_2n_fcs(f) := (
00602   /* XXX */
00603   true)$
00604 
00605 
00606 /* **************************
00607    * Summarising statistics *
00608    **************************
00609 */
00610 
00611 okltest_statistics_cs(f)  := (
00612   assert(f({}) = [0,0,0,-1,inf]),
00613   assert(f({{}}) = [0,1,0,0,0]),
00614   assert(f({{1},{1,2},{-1,4},{2,-4,-1}}) = [3,4,8,3,1]),
00615   assert(okltest_nvar_cs(buildq([f],lambda([F],f(F)[1]))) = true),
00616   assert(okltest_ncl_cs(buildq([f],lambda([F],f(F)[2]))) = true),
00617   assert(okltest_nlitocc_cs(buildq([f],lambda([F],f(F)[3]))) = true),
00618   assert(okltest_max_rank_cs(buildq([f],lambda([F],f(F)[4]))) = true),
00619   assert(okltest_min_rank_cs(buildq([f],lambda([F],f(F)[5]))) = true),
00620   true)$
00621 
00622 okltest_statistics_fcs(f)  := (
00623   assert(okltest_statistics_cs(buildq([f],lambda([F],f(cs2fcs(F))))) = true),
00624   assert(f([{1},{}]) = [1,0,0,-1,inf]),
00625   assert(f([{2},{{}}]) = [1,1,0,0,0]),
00626   assert(okltest_nvar_fcs(buildq([f],lambda([F],f(F)[1]))) = true),
00627   assert(okltest_ncl_fcs(buildq([f],lambda([F],f(F)[2]))) = true),
00628   assert(okltest_nlitocc_fcs(buildq([f],lambda([F],f(F)[3]))) = true),
00629   assert(okltest_max_rank_fcs(buildq([f],lambda([F],f(F)[4]))) = true),
00630   assert(okltest_min_rank_fcs(buildq([f],lambda([F],f(F)[5]))) = true),
00631   true)$
00632 
00633 okltest_extended_statistics_fcs(f) := (
00634   assert(f([{},{}]) = [0,0,0,inf,-1,[],inf,minf,inf,minf]),
00635   assert(okltest_nvar_fcs(buildq([f],lambda([F],f(F)[1]))) = true),
00636   assert(okltest_ncl_fcs(buildq([f],lambda([F],f(F)[2]))) = true),
00637   assert(okltest_nlitocc_fcs(buildq([f],lambda([F],f(F)[3]))) = true),
00638   assert(okltest_min_rank_fcs(buildq([f],lambda([F],f(F)[4]))) = true),
00639   assert(okltest_max_rank_fcs(buildq([f],lambda([F],f(F)[5]))) = true),
00640   assert(okltest_ncl_list_fcs(buildq([f],lambda([F],f(F)[6]))) = true),
00641   assert(okltest_min_literal_degree_fcs(buildq([f],lambda([F],f(F)[7]))) = true),
00642   assert(okltest_max_literal_degree_fcs(buildq([f],lambda([F],f(F)[8]))) = true),
00643   assert(okltest_min_variable_degree_fcs(buildq([f],lambda([F],f(F)[9]))) = true),
00644   assert(okltest_max_variable_degree_fcs(buildq([f],lambda([F],f(F)[10]))) = true),
00645   true)$
00646