OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 27.3.2008 (Swansea) */
00002 /* Copyright 2008, 2010, 2011, 2012, 2013 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/Generators.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/LinearEquations.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00028 
00029 kill(f)$
00030 
00031 
00032 /* ***************************
00033    * Single resolution steps *
00034    ***************************
00035 */
00036 
00037 okltest_resolvable(f) := (
00038   assert(f({},{}) = false),
00039   assert(f({1},{}) = false),
00040   assert(f({},{1}) = false),
00041   assert(f({1},{-1}) = true),
00042   assert(f({1,-2,3},{1,2,4}) = true),
00043   assert(f({1,2},{2,3,4}) = false),
00044   true)$
00045 
00046 okltest_resolution_literal(f) := (
00047   assert(f({1},{-1}) = 1),
00048   assert(f({1,2,-3},{2,3,-4}) = -3),
00049   true)$
00050 
00051 okltest_resolvable_p(f) := (
00052   assert(f({},{}) = []),
00053   assert(f({1},{}) = []),
00054   assert(f({},{1}) = []),
00055   assert(f({1},{-1}) = [1]),
00056   assert(f({1,-2,3},{1,2,4}) = [-2]),
00057   assert(f({1,2},{2,3,4}) = []),
00058   true)$
00059 
00060 okltest_two_subsumption_resolvent_p(f) := (
00061   assert(f({},{}) = []),
00062   assert(f({1},{-1}) = [{}]),
00063   assert(f({1},{-1,2}) = []),
00064   assert(f({1},{2}) = []),
00065   assert(f({1,2},{-1,2}) = [{2}]),
00066   assert(f({1,2},{-1,-2}) = []),
00067   true)$
00068 
00069 
00070 /* *************************
00071    * Adding all resolvents *
00072    *************************
00073 */
00074 
00075 okltest_resolvable_cs(f) := (
00076   assert(f({}) = {}),
00077   assert(f({{}}) = {}),
00078   assert(f({{1}}) = {}),
00079   assert(f({{1},{-1}}) = {{{1},{-1}}}),
00080   assert(f({{1},{-1},{}}) = {{{1},{-1}}}),
00081   assert(f({{1,2},{-1,2},{-1,-2}}) = {{{1,2},{-1,2}},{{-1,2},{-1,-2}}}),
00082   for n : 0 thru 4 do block([F : full_fcs(n)[2]],
00083     assert(length(f(F)) = 2^n * n / 2)),
00084   true)$
00085 
00086 okltest_two_subsumption_resolvable_cs(f) := (
00087   assert(f({}) = {}),
00088   assert(f({{}}) = {}),
00089   assert(f({{1}}) = {}),
00090   assert(f({{1},{-1}}) = {{{1},{-1}}}),
00091   assert(f({{1},{-1},{}}) = {{{1},{-1}}}),
00092   assert(f({{1,2},{-1,2},{-1,-2}}) = {{{1,2},{-1,2}},{{-1,2},{-1,-2}}}),
00093   assert(f({{1,2},{-1,2},{-1,-2},{1}}) = {{{1,2},{-1,2}},{{-1,2},{-1,-2}}}),
00094   for n : 0 thru 4 do block([F : full_fcs(n)[2]],
00095     assert(length(f(F)) = 2^n * n / 2)),
00096   true)$
00097 
00098 okltest_two_subsumption_resolvents_rem_cs(f) := (
00099   assert(f({}) = [{},{}]),
00100   assert(f({{}}) = [{},{{}}]),
00101   assert(f({{1}}) = [{},{{1}}]),
00102   assert(f({{1},{-1}}) = [{{}},{}]),
00103   assert(f({{1,2},{1,-2}}) = [{{1}},{}]),
00104   assert(f({{1,2},{-1,-2}}) = [{},{{1,2},{-1,-2}}]),
00105   true)$
00106 
00107 
00108 /* *****************
00109    * DP resolution *
00110    *****************
00111 */
00112 
00113 okltest_dp_operator(f) := (
00114   assert(f({},1) = {}),
00115   assert(f({{}},1) = {{}}),
00116   assert(f({{1}},1) = {}),
00117   assert(f({{1}},2) = {{1}}),
00118   assert(f({{1},{-1}},1) = {{}}),
00119   assert(f({{1},{-1}},2) = {{1},{-1}}),
00120   block([n : 4, F],
00121     F : full_fcs(n)[2],
00122     for v : n thru 1 step -1 do (
00123       F : f(F,v),
00124       assert(F = full_fcs(v-1)[2]))),
00125   true)$
00126 
00127 okltest_dp_operator_fcs(f) := (
00128   assert(f([{},{}],1) = [{},{}]),
00129   assert(f([{},{{}}],1) = [{},{{}}]),
00130   assert(f([{1},{}],1) = [{},{}]),
00131   assert(f([{1},{{}}],1) = [{},{{}}]),
00132   assert(f([{2},{}],1) = [{2},{}]),
00133   assert(f([{2},{{}}],1) = [{2},{{}}]),
00134   assert(okltest_dp_operator(buildq([f], lambda([F,v], fcs2cs(f(cs2fcs(F),v))))) = true),
00135   true)$
00136 
00137 okltest_distribution_min_dp(f) := block(
00138   assert(f([{},{}]) = [[0,1]]),
00139   assert(f([{},{{}}]) = [[1,1]]),
00140   assert(f([{1},{}]) = [[0,1]]),
00141   assert(f([{1},{{}}]) = [[2,1]]),
00142   assert(f([{1},{{1}}]) = [[1,1]]),
00143   assert(f([{1},{{1},{-1}}]) = [[3,1]]),
00144   assert(f([{1},{{},{1},{-1}}]) = [[4,1]]),
00145   assert(f([{1,2},{{1,2},{-1,2},{-1,-2}}]) = [[4,2]]),
00146   assert(f([{1,2},{{1},{1,2},{-1,2},{-1,-2}}]) = [[7,2]]),
00147   for n : 0 thru if oklib_test_level=0 then 3 else 4 do
00148    block([FF : full_fcs(n)],
00149     assert(f(FF) = [[2^(n+1)-1,n!]])),
00150   true)$
00151 
00152 
00153 /* ****************************
00154    * Width-bounded resolution *
00155    ****************************
00156 */
00157 
00158 okltest_kresolvable(f) := (
00159   assert(f({},{},0) = false),
00160   assert(f({1},{-1},0) = false),
00161   assert(f({1},{-1},1) = true),
00162   assert(f({1},{-1,2},1) = true),
00163   assert(f({1,2},{-1},1) = true),
00164   assert(f({1,2},{-1,2},1) = false),
00165   assert(f({1,2},{-1,2},2) = true),
00166   assert(f({1,2,3},{-1,2},2) = true),
00167   assert(f({1,2},{-1,2,3},2) = true),
00168   true)$
00169 
00170 okltest_kresolvable_s(f) := (
00171   assert(okltest_kresolvable(buildq([f], lambda([C,D,k], f({C,D},k)))) = true),
00172   assert(f({},0) = false),
00173   assert(f({{1}},0) = false),
00174   assert(f({{1},{}},0) = false),
00175   assert(f({{1},{-1}},0) = false),
00176   assert(f({{1},{-1}},1) = true),
00177   assert(f({{1},{-1,2}},1) = true),
00178   assert(f({{1,2},{-1,2}},1) = false),
00179   assert(f({{1,2},{-1,2}},2) = true),
00180   assert(f({{1,2,3},{-1,2}},2) = true),
00181   true)$
00182 
00183 okltest_kresolvable_cs(f) := (
00184   assert(f({},0) = {}),
00185   assert(f({{1}},0) = {}),
00186   assert(f({{1},{-1}},0) = {}),
00187   assert(f({{1},{-1}},1) = {{{1},{-1}}}),
00188   assert(f({{1},{-1},{-1,2}},1) = {{{1},{-1}},{{1},{-1,2}}}),
00189   assert(f({{1},{1,2},{-1},{-1,2}},1) = {{{1},{-1}},{{1},{-1,2}},{{1,2},{-1}}}),
00190   true)$
00191 
00192 okltest_kresolvents_cs(f) := (
00193   assert(f({},0) = {}),
00194   assert(f({{1}},0) = {}),
00195   assert(f({{1},{-1}},0) = {}),
00196   assert(f({{1},{-1}},1) = {{}}),
00197   assert(f({{1},{-1},{-1,2}},1) = {{},{2}}),
00198   assert(f({{1},{1,2},{-1},{-1,2}},1) = {{},{2}}),
00199   assert(f({{1},{1,2,4},{-1},{-1,2,3}},1) = {{},{2,4},{2,3}}),
00200   assert(f({{1},{1,2,4},{-1},{-1,2,3}},2) = {{},{2,4},{2,3}}),
00201   assert(f({{1},{1,2,4},{-1},{-1,2,3}},3) = {{},{2,4},{2,3},{2,3,4}}),
00202   true)$
00203 
00204 okltest_add_kresolvents_cs(f) := (
00205   assert(f({},0) = {}),
00206   assert(f({{1}},0) = {{1}}),
00207   assert(f({{1},{-1}},0) = {{1},{-1}}),
00208   assert(f({{1},{-1}},1) = {{},{1},{-1}}),
00209   assert(f({{1},{-1},{-1,2}},1) = {{},{2},{1},{-1},{-1,2}}),
00210   assert(f({{1},{1,2},{-1},{-1,2}},1) = {{},{2},{1},{1,2},{-1},{-1,2}}),
00211   assert(f({{1},{1,2,4},{-1},{-1,2,3}},1) = {{},{2,4},{2,3},{1},{1,2,4},{-1},{-1,2,3}}),
00212   assert(f({{1},{1,2,4},{-1},{-1,2,3}},2) = {{},{2,4},{2,3},{1},{1,2,4},{-1},{-1,2,3}}),
00213   assert(f({{1},{1,2,4},{-1},{-1,2,3}},3) = {{},{2,4},{2,3},{2,3,4},{1},{1,2,4},{-1},{-1,2,3}}),
00214   true)$
00215 
00216 okltest_kresolution_closure_cs(f) := (
00217   assert(f({},0) = [{},[0]]),
00218   assert(f({},1) = [{},[0]]),
00219   assert(f({{}},0) = [{{}},[1]]),
00220   assert(f({{}},1) = [{{}},[1]]),
00221   assert(f({{1}},0) = [{{1}},[1]]),
00222   assert(f({{1}},1) = [{{1}},[1]]),
00223   assert(f({{1},{-1}},0) = [{{1},{-1}},[2]]),
00224   assert(f({{1},{-1}},1) = [{{},{1},{-1}},[2,3]]),
00225   for n : 1 thru 5 do block([N:setn(n), NN:singletons(setmn(-n,-1))],
00226     assert(f(adjoin(N,NN),1)[1] = union(NN,powerset(N)))),
00227   assert(f({{1,2},{-1,2}},1) = [{{1,2},{-1,2}},[2]]),
00228   assert(f({{1,2},{-1,2}},2) = [{{1,2},{-1,2},{2}},[2,3]]),
00229   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}},2) = [{{1,2},{-1,2},{1,-2},{-1,-2},{1},{-1},{2},{-2},{}},[4,8,9]]),
00230   assert(f({{1,2,3},{-1,2,3}},2) = [{{1,2,3},{-1,2,3}},[2]]),
00231   assert(f({{1,2,3},{-1,2,3}},3) = [{{1,2,3},{-1,2,3},{2,3}},[2,3]]),
00232   true)$
00233 
00234 okltest_min_add_kresolvents_cs(f) := (
00235   assert(f({},0) = {}),
00236   assert(f({{1}},0) = {{1}}),
00237   assert(f({{1},{-1}},0) = {{1},{-1}}),
00238   assert(f({{1},{-1}},1) = {{}}),
00239   assert(f({{1},{-1},{-1,2}},1) = {{}}),
00240   assert(f({{1},{1,2},{-1},{-1,2}},1) = {{}}),
00241   assert(f({{1},{1,2,4},{-1},{-1,2,3}},1) = {{}}),
00242   assert(f({{1},{1,2,4},{-1},{-1,2,3}},2) = {{}}),
00243   assert(f({{1},{1,2,4},{-1},{-1,2,3}},3) = {{}}),
00244   assert(f({{1,2},{2,3}},2) = {{1,2},{2,3}}),
00245   assert(f({{1,2},{-2,3}},2) = {{1,2},{-2,3},{1,3}}),
00246   true)$
00247 
00248 okltest_min_kresolution_closure_cs(f) := (
00249   assert(f({},0) = [{},[0]]),
00250   assert(f({},1) = [{},[0]]),
00251   assert(f({{}},0) = [{{}},[1]]),
00252   assert(f({{}},1) = [{{}},[1]]),
00253   assert(f({{1}},0) = [{{1}},[1]]),
00254   assert(f({{1}},1) = [{{1}},[1]]),
00255   assert(f({{1},{-1}},0) = [{{1},{-1}},[2]]),
00256   assert(f({{1},{-1}},1) = [{{}},[2,1]]),
00257   for n : 1 thru 5 do block([N:setn(n), NN:singletons(setmn(-n,-1))],
00258     assert(f(adjoin(N,NN),1)[1] = {{}})),
00259   assert(f({{1,2},{-1,2}},1) = [{{1,2},{-1,2}},[2]]),
00260   assert(f({{1,2},{-1,2}},2) = [{{2}},[2,1]]),
00261   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}},2) = [{{}},[4,4,1]]),
00262   assert(f({{1,2,3},{-1,2,3}},2) = [{{1,2,3},{-1,2,3}},[2]]),
00263   assert(f({{1,2,3},{-1,2,3}},3) = [{{2,3}},[2,1]]),
00264   true)$
00265 
00266 okltest_bresolvable(f) := (
00267   assert(f({},{},0) = false),
00268   assert(f({1},{-1},0) = false),
00269   assert(f({1},{-1},1) = true),
00270   assert(f({1},{-1,2},1) = false),
00271   assert(f({1},{-1,2},2) = true),
00272   assert(f({1,2},{-2},1) = false),
00273   assert(f({1,2},{-2},2) = true),
00274   true)$
00275 
00276 okltest_bresolvable_s(f) := (
00277   assert(f({},0) = false),
00278   assert(f({{}},0) = false),
00279   assert(f({{},{1}},1) = false),
00280   assert(f({{1},{-1}},1) = true),
00281   assert(okltest_bresolvable(buildq([f], lambda([C,D,k], f({C,D},k)))) = true),
00282   true)$
00283 
00284 okltest_bresolvable_cs(f) := (
00285   assert(f({},0) = {}),
00286   assert(f({{1}},0) = {}),
00287   assert(f({{1},{-1}},0) = {}),
00288   assert(f({{1},{-1}},1) = {{{1},{-1}}}),
00289   assert(f({{1},{-1},{-1,2}},1) = {{{1},{-1}}}),
00290   assert(f({{1},{1,2},{-1},{-1,2}},1) = {{{1},{-1}}}),
00291   assert(f({{1,2},{-2,3},{-3}},1) = {}),
00292   assert(f({{1,2},{-2,3},{-3}},2) = {{{1,2},{-2,3}},{{-2,3},{-3}}}),
00293   assert(f({{1,2},{-2,3},{-3},{1,2,3}},2) = {{{1,2},{-2,3}},{{-2,3},{-3}}}),
00294   true)$
00295 
00296 okltest_bresolvents_cs(f) := (
00297   assert(f({},0) = {}),
00298   assert(f({{1}},0) = {}),
00299   assert(f({{1},{-1}},0) = {}),
00300   assert(f({{1},{-1}},1) = {{}}),
00301   assert(f({{1},{-1},{-1,2}},1) = {{}}),
00302   assert(f({{1},{1,2},{-1},{-1,2}},1) = {{}}),
00303   assert(f({{1,2},{-2,3},{-3}},1) = {}),
00304   assert(f({{1,2},{-2,3},{-3}},2) = {{1,3},{-2}}),
00305   assert(f({{1,2},{-2,3},{-3},{1,2,3}},2) = {{1,3},{-2}}),
00306   true)$
00307 
00308 okltest_add_bresolvents_cs(f) := (
00309   assert(f({},0) = {}),
00310   assert(f({{1}},0) = {{1}}),
00311   assert(f({{1},{-1}},0) = {{1},{-1}}),
00312   assert(f({{1},{-1}},1) = {{},{1},{-1}}),
00313   assert(f({{1},{-1},{-1,2}},1) = {{},{1},{-1},{-1,2}}),
00314   assert(f({{1},{1,2},{-1},{-1,2}},1) = {{},{1},{1,2},{-1},{-1,2}}),
00315   assert(f({{1},{1,2,4},{-1},{-1,2,3}},1) = {{},{1},{1,2,4},{-1},{-1,2,3}}),
00316   assert(f({{1},{1,2,4},{-1},{-1,2,3}},2) = {{},{1},{1,2,4},{-1},{-1,2,3}}),
00317   assert(f({{1},{1,2,4},{-1},{-1,2,3}},3) = {{},{2,4},{2,3},{2,3,4},{1},{1,2,4},{-1},{-1,2,3}}),
00318   true)$
00319 
00320 okltest_bresolution_closure_cs(f) := (
00321   assert(f({},0) = [{},[0]]),
00322   assert(f({},1) = [{},[0]]),
00323   assert(f({{}},0) = [{{}},[1]]),
00324   assert(f({{}},1) = [{{}},[1]]),
00325   assert(f({{1}},0) = [{{1}},[1]]),
00326   assert(f({{1}},1) = [{{1}},[1]]),
00327   assert(f({{1},{-1}},0) = [{{1},{-1}},[2]]),
00328   assert(f({{1},{-1}},1) = [{{},{1},{-1}},[2,3]]),
00329   for n : 2 thru 5 do block([N:setn(n), NN:singletons(setmn(-n,-1)), F],
00330     F : adjoin(N,NN),
00331     assert(f(F,1)[1] = F),
00332     assert(f(F,n-1)[1] = F),
00333     assert(f(F,n)[1] = union(NN,powerset(N)))
00334   ),
00335   assert(f({{1,2},{-1,2}},1) = [{{1,2},{-1,2}},[2]]),
00336   assert(f({{1,2},{-1,2}},2) = [{{1,2},{-1,2},{2}},[2,3]]),
00337   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}},2) = [{{1,2},{-1,2},{1,-2},{-1,-2},{1},{-1},{2},{-2},{}},[4,8,9]]),
00338   assert(f({{1,2,3},{-1,2,3}},2) = [{{1,2,3},{-1,2,3}},[2]]),
00339   assert(f({{1,2,3},{-1,2,3}},3) = [{{1,2,3},{-1,2,3},{2,3}},[2,3]]),
00340   for n : 1 thru cokltl(3,5) do block([F : full_cs(n)],
00341     assert(f(F,n-1)[1] = F),
00342     assert(f(F,n)[1] = all_pass(setn(n)))
00343   ),
00344   true)$
00345 
00346 okltest_min_add_bresolvents_cs(f) := (
00347   assert(f({},0) = {}),
00348   assert(f({{1}},0) = {{1}}),
00349   assert(f({{1},{-1}},0) = {{1},{-1}}),
00350   assert(f({{1},{-1}},1) = {{}}),
00351   assert(f({{1},{-1},{-1,2}},1) = {{}}),
00352   assert(f({{1},{1,2},{-1},{-1,2}},1) = {{}}),
00353   assert(f({{1},{1,2,4},{-1},{-1,2,3}},1) = {{}}),
00354   assert(f({{1},{1,2,4},{-1},{-1,2,3}},2) = {{}}),
00355   assert(f({{1},{1,2,4},{-1},{-1,2,3}},3) = {{}}),
00356   assert(f({{1,2},{2,3}},2) = {{1,2},{2,3}}),
00357   assert(f({{1,2},{-2,3}},2) = {{1,2},{-2,3},{1,3}}),
00358   assert(f({{1,2,3},{-1,2}},2) = {{1,2,3},{-1,2}}),
00359   assert(f({{1,2,3},{-1,2}},3) = {{2,3},{-1,2}}),
00360   true)$
00361 
00362 okltest_min_bresolution_closure_cs(f) := (
00363   assert(f({},0) = [{},[0]]),
00364   assert(f({},1) = [{},[0]]),
00365   assert(f({{}},0) = [{{}},[1]]),
00366   assert(f({{}},1) = [{{}},[1]]),
00367   assert(f({{1}},0) = [{{1}},[1]]),
00368   assert(f({{1}},1) = [{{1}},[1]]),
00369   assert(f({{1},{-1}},0) = [{{1},{-1}},[2]]),
00370   assert(f({{1},{-1}},1) = [{{}},[2,1]]),
00371   for n : 2 thru 5 do block([N:setn(n), NN:singletons(setmn(-n,-1)), F],
00372     F : adjoin(N,NN),
00373     assert(f(F,1)[1] = F),
00374     assert(f(F,n-1)[1] = F),
00375     assert(f(F,n)[1] = {{}})
00376   ),
00377   assert(f({{1,2},{-1,2}},1) = [{{1,2},{-1,2}},[2]]),
00378   assert(f({{1,2},{-1,2}},2) = [{{2}},[2,1]]),
00379   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}},2) = [{{}},[4,4,1]]),
00380   assert(f({{1,2,3},{-1,2,3}},2) = [{{1,2,3},{-1,2,3}},[2]]),
00381   assert(f({{1,2,3},{-1,2,3}},3) = [{{2,3}},[2,1]]),
00382   for n : 1 thru cokltl(3,5) do block([F : full_cs(n)],
00383     assert(f(F,n-1)[1] = F),
00384     assert(f(F,n)[1] = {{}})
00385   ),
00386   true)$
00387 
00388 
00389 /* *******************
00390    * Blocked clauses *
00391    *******************
00392 */
00393 
00394 okltest_blocking_literal_p(f) := block(
00395   assert(f({{1}},{1},1)),
00396   assert(not(f({},{},1))),
00397   assert(not(f({{}},{},1))),
00398   assert(not(f({{1},{-1}},{1},1))),
00399   assert(f({{1,2},{1,-2,-3},{-1,3}},{1,-2,-3},1)),
00400   assert(f({{1,2},{1,-2,-3},{-1,3}},{1,-2,-3},-3)),
00401   assert(not(f({{1,2},{1,-2,-3},{-1,3}},{1,-2,-3},3))),
00402   true)$
00403 
00404 okltest_blocked_cs_p(f) := block(
00405   assert(f({{1}},{1})),
00406   assert(not(f({},{}))),
00407   assert(not(f({{}},{}))),
00408   assert(not(f({{1},{-1}},{1}))),
00409   assert(f({{1,2},{1,-2,-3},{-1,3}},{1,-2,-3})),
00410   assert(f({{1,2},{1,-2,-3},{-1,3}},{1,-2,-3})),
00411   for i : 1 thru 3 do block([F : full_cs(i)],
00412     for C in F do assert(not(f(F,C)))),
00413   for i : 1 thru 3 do block([F : setify(even_parity_cl(i))],
00414     for C in F do assert(f(F,C))),
00415   true)$
00416 
00417 okltest_elim_blocked_cs(f) := block(
00418   assert(f({}) = {}),
00419   assert(f({{}}) = {{}}),
00420   assert(f({{1}}) = {}),
00421   assert(f({{1},{-1}}) = {{1},{-1}}),
00422   assert(f({{1,2},{1,-2,-3},{-1,3}}) = {}),
00423   for i : 1 thru 3 do block([F : full_cs(i)],
00424     assert(f(F) = F)),
00425   for i : 1 thru 3 do block([F : setify(even_parity_cl(i))],
00426     assert(f(F) = {})),
00427   true)$
00428 
00429 okltest_elim_blockedk_cs(f) := (
00430   assert(okltest_elim_blocked_cs(buildq([f], lambda([F], f(F,inf)))) = true),
00431   assert(f({{1}},0) = {{1}}),
00432   assert(f({{1}},1) = {}),
00433   assert(f({{1,2},{1,-2,-3},{-1,3}},2) = {{1,-2,-3}}),
00434   true)$
00435 
00436 okltest_blocked_extension_cs_p(f) := block(
00437   assert(f({},{})),
00438   assert(f({{1}},{{1}})),
00439   assert(f({{1}},{})),
00440   assert(not(f({{-1}},{{1}}))),
00441   for i : 1 thru 3 do block([F : full_cs(i)],
00442     assert(f(F,F))),
00443   for i : 1 thru 3 do block([F : setify(even_parity_cl(i))],
00444     assert(f(F,{})),
00445     assert(not(f(F,setify(odd_parity_cl(i)))))),
00446   true)$
00447