OKlibrary  0.2.1.6
NonBoolean.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 17.4.2009 (Swansea) */
00002 /* Copyright 2009, 2011 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/ClauseSets/NonBoolean.mac")$
00024 
00025 kill(f)$
00026 
00027 
00028 /* **************************
00029    * Variables and literals *
00030    **************************
00031 */
00032 
00033 okltest_nbl_p(f) := block([v,e],
00034   assert(f(1) = false),
00035   assert(f([1]) = false),
00036   assert(f([1,2]) = true),
00037   assert(f([v,e]) = true),
00038   assert(f([1,2,3]) = false),
00039   true)$
00040 
00041 okltest_var_nbl(f) := block([x,y],
00042   assert(f([x,y]) = x),
00043   true)$
00044 
00045 okltest_val_nbl(f) := block([x,y],
00046   assert(f([x,y]) = y),
00047   true)$
00048 
00049 okltest_snbl_p(f) := block([x,y,z],
00050   assert(f(1) = false),
00051   assert(f([]) = false),
00052   assert(f([x,y,z]) = false),
00053   assert(f([x,y,-1]) = true),
00054   assert(f([x,y,1]) = true),
00055   true)$
00056 
00057 okltest_var_snbl(f) := block([x,y,z],
00058   assert(f([x,y,z]) = x),
00059   true)$
00060 
00061 okltest_val_snbl(f) := block([x,y,z],
00062   assert(f([x,y,z]) = y),
00063   true)$
00064 
00065 okltest_sgn_snbl(f) := block([x,y,z],
00066   assert(f([x,y,z]) = z),
00067   true)$
00068 
00069 okltest_pl_p(f) := block([x,y],
00070   assert(f(0) = false),
00071   assert(f([]) = false),
00072   assert(f([x,y]) = false),
00073   assert(f([x,{}]) = true),
00074   true)$
00075 
00076 okltest_var_pl(f) := block([x,y],
00077   assert(f([x,y]) = x),
00078   true)$
00079 
00080 okltest_val_pl(f) := block([x,y],
00081   assert(f([x,y]) = y),
00082   true)$
00083 
00084 okltest_spl_p(f) := block([x,y,z],
00085   assert(f(0) = false),
00086   assert(f([]) = false),
00087   assert(f([x,y,z]) = false),
00088   assert(f([x,{},z]) = false),
00089   assert(f([x,{},1]) = true),
00090   assert(f([x,{},-1]) = true),
00091   true)$
00092 
00093 okltest_var_spl(f) := block([x,y,z],
00094   assert(f([x,y,z]) = x),
00095   true)$
00096 
00097 okltest_val_spl(f) := block([x,y,z],
00098   assert(f([x,y,z]) = y),
00099   true)$
00100 
00101 okltest_sgn_spl(f) := block([x,y,z],
00102   assert(f([x,y,z]) = z),
00103   true)$
00104 
00105 
00106 /* ***********
00107    * Clauses *
00108    ***********
00109 */
00110 
00111 okltest_nbc_p(f) := block([x,y],
00112   assert(f(0) = false),
00113   assert(f({x}) = false),
00114   assert(f({}) = true),
00115   assert(f({[x,y]}) = true),
00116   assert(f({[x,y],[x,1]}) = false),
00117   assert(f({[x,y],[1,x]}) = true),
00118   true)$
00119 
00120 okltest_var_nbc(f) := (
00121   assert(f({}) = {}),
00122   assert(f({[1,2],[2,2],[3,1]}) = {1,2,3}),
00123   true)$
00124 
00125 okltest_val_nbc(f) := block(
00126   assert(f({}) = {}),
00127   assert(f({[1,2],[2,2],[3,1]}) = {1,2}),
00128   true)$
00129 
00130 okltest_snbc_p(f) := block([x,y],
00131   assert(f(0) = false),
00132   assert(f({[x,y]}) = false),
00133   assert(f({}) = true),
00134   assert(f({[x,y,1]}) = true),
00135   assert(f({[x,y,-1]}) = true),
00136   assert(f({[x,y,1],[x,z,-1]}) = false),
00137   assert(f({[x,y,1],[y,x,1],[z,z,-1]}) = true),
00138   true)$
00139 
00140 okltest_var_snbc(f) := (
00141   assert(f({}) = {}),
00142   assert(f({[1,2,1],[2,2,-1],[3,1,1]}) = {1,2,3}),
00143   true)$
00144 
00145 okltest_val_snbc(f) := (
00146   assert(f({}) = {}),
00147   assert(f({[1,2,1],[2,2,1],[3,1,1]}) = {1,2}),
00148   true)$
00149 
00150 okltest_sgn_snbc(f) := (
00151   assert(f({}) = {}),
00152   assert(f({[1,2,1],[2,2,1],[3,1,1]}) = {1}),
00153   assert(f({[1,2,1],[2,2,-1],[3,1,1]}) = {1,-1}),
00154   true)$
00155 
00156 
00157 /* ***************
00158    * Clause-sets *
00159    ***************
00160 */
00161 
00162 okltest_nbcs_p(f) := block([x,y],
00163   assert(f(0) = false),
00164   assert(f({0}) = false),
00165   assert(f({}) = true),
00166   assert(f({{}}) = true),
00167   assert(f({{[x,y]}}) = true),
00168   assert(f({{[x,y,x]}}) = false),
00169   /* XXX */
00170   true)$
00171 
00172 okltest_var_nbcs(f) := (
00173   assert(f({}) = {}),
00174   assert(f({{}}) = {}),
00175   assert(f({{[1,5]}}) = {1}),
00176   assert(f({{[1,5],[2,6]},{[1,7],[3,8]}}) = {1,2,3}),
00177   true)$
00178 
00179 okltest_val_nbcs(f) := (
00180   assert(f({}) = {}),
00181   assert(f({{}}) = {}),
00182   assert(f({{[1,5]}}) = {5}),
00183   assert(f({{[1,5],[2,6]},{[1,6],[3,7]}}) = {5,6,7}),
00184   true)$
00185 
00186 okltest_lit_nbcs(f) := (
00187   assert(f({}) = {}),
00188   assert(f({{}}) = {}),
00189   assert(f({{[1,5]}}) = {[1,5]}),
00190   assert(f({{[1,5],[2,6]},{[1,7],[3,8]}}) = {[1,5],[2,6],[1,7],[3,8]}),
00191   true)$
00192 
00193 okltest_snbcs_p(f) := block([x,y],
00194   assert(f(0) = false),
00195   assert(f({0}) = false),
00196   assert(f({}) = true),
00197   assert(f({{}}) = true),
00198   assert(f({{[x,y,1]}}) = true),
00199   assert(f({{[x,y,x]}}) = false),
00200   true)$
00201 
00202 okltest_var_snbcs(f) := (
00203   assert(f({}) = {}),
00204   assert(f({{}}) = {}),
00205   assert(f({{[1,5,1]}}) = {1}),
00206   assert(f({{[1,5,1],[2,6,-1]},{[1,7,1],[3,8,-1]}}) = {1,2,3}),
00207   true)$
00208 
00209 okltest_val_snbcs(f) := (
00210   assert(f({}) = {}),
00211   assert(f({{}}) = {}),
00212   assert(f({{[1,5,1]}}) = {5}),
00213   assert(f({{[1,5,1],[2,6,1]},{[1,6,-1],[3,7,-1]}}) = {5,6,7}),
00214   true)$
00215 
00216 okltest_sgn_snbcs(f) := (
00217   assert(f({}) = {}),
00218   assert(f({{}}) = {}),
00219   assert(f({{[1,5,1]}}) = {1}),
00220   assert(f({{[1,5,1],[2,6,1]},{[1,6,-1],[3,7,-1]}}) = {1,-1}),
00221   true)$
00222 
00223 okltest_lit_snbcs(f) := (
00224   assert(f({}) = {}),
00225   assert(f({{}}) = {}),
00226   assert(f({{[1,5,1]}}) = {[1,5,1]}),
00227   assert(f({{[1,5,1],[2,6,-1]},{[1,7,-1],[3,8,1]}}) = {[1,5,1],[2,6,-1],[1,7,-1],[3,8,1]}),
00228   true)$
00229 
00230 okltest_nbcl_p(f) := block([x,y],
00231   assert(f(0) = false),
00232   assert(f([0]) = false),
00233   assert(f([]) = true),
00234   assert(f([{}]) = true),
00235   assert(f([{[x,y]}]) = true),
00236   assert(f([{[x,y,x]}]) = false),
00237   /* XXX */
00238   true)$
00239 
00240 okltest_var_nbcl(f) := (
00241   assert(f([]) = {}),
00242   assert(f([{}]) = {}),
00243   assert(f([{[1,5]}]) = {1}),
00244   assert(f([{[1,5],[2,6]},{[1,7],[3,8]}]) = {1,2,3}),
00245   true)$
00246 
00247 okltest_val_nbcl(f) := (
00248   assert(f([]) = {}),
00249   assert(f([{}]) = {}),
00250   assert(f([{[1,5]}]) = {5}),
00251   assert(f([{[1,5],[2,6]},{[1,6],[3,7]}]) = {5,6,7}),
00252   true)$
00253 
00254 okltest_lit_nbcl(f) := (
00255   assert(f([]) = {}),
00256   assert(f([{}]) = {}),
00257   assert(f([{[1,5]}]) = {[1,5]}),
00258   assert(f([{[1,5],[2,6]},{[1,7],[3,8]}]) = {[1,5],[2,6],[1,7],[3,8]}),
00259   true)$
00260 
00261 okltest_snbcl_p(f) := block([x,y,z],
00262   assert(f(0) = false),
00263   assert(f([0]) = false),
00264   assert(f([]) = true),
00265   assert(f([{}]) = true),
00266   assert(f([{[x,y,1]}]) = true),
00267   assert(f([{[x,y,x]}]) = false),
00268   assert(f([{[x,y,1],[x,z,-1]}]) = false),
00269   assert(f([{[x,y,1],[y,z,-1]}]) = true),
00270   true)$
00271 
00272 okltest_var_snbcl(f) := block(
00273   assert(f([]) = {}),
00274   assert(f([{}]) = {}),
00275   assert(f([{[1,5,1]}]) = {1}),
00276   assert(f([{[1,5,1],[2,6,1]},{[1,7,1],[3,8,-1]}]) = {1,2,3}),
00277   true)$
00278 
00279 okltest_val_snbcl(f) := block(
00280   assert(f([]) = {}),
00281   assert(f([{}]) = {}),
00282   assert(f([{[1,5,-1]}]) = {5}),
00283   assert(f([{[1,5,1],[2,6,1]},{[1,6,1],[3,7,-1]}]) = {5,6,7}),
00284   true)$
00285 
00286 okltest_sgn_snbcl(f) := (
00287   assert(f([]) = {}),
00288   assert(f([{}]) = {}),
00289   assert(f([{[1,5,-1]}]) = {-1}),
00290   assert(f([{[1,5,1],[2,6,1]},{[1,6,1],[3,7,-1]}]) = {1,-1}),
00291   true)$
00292 
00293 okltest_lit_snbcl(f) := block(
00294   assert(f([]) = {}),
00295   assert(f([{}]) = {}),
00296   assert(f([{[1,5,1]}]) = {[1,5,1]}),
00297   assert(f([{[1,5,-1],[2,6,-1]},{[1,7,-1],[3,8,1]}]) = {[1,5,-1],[2,6,-1],[1,7,-1],[3,8,1]}),
00298   true)$
00299 
00300 okltest_nbfcs_p(f) := (
00301   assert(f(0) = false).
00302   assert(f([0]) = false),
00303   assert(f([0,0]) = false),
00304   assert(f([{},{}]) = true),
00305   assert(f([{},{{}}]) = true),
00306   assert(f([{1},{{[1,5]}}]) = true),
00307   assert(f([{1},{{[2,1]}}]) = false),
00308   /* XXX */
00309   true)$
00310 
00311 okltest_var_nbfcs(f) := (
00312   assert(f([{},{}]) = {}),
00313   assert(f([{},{{}}]) = {}),
00314   assert(f([{1},{}]) = {1}),
00315   assert(f([{1},{{}}]) = {1}),
00316   assert(f([{1,2},{{[1,5]}}]) = {1,2}),
00317   true)$
00318 
00319 okltest_val_nbfcs(f) := (
00320   assert(f([{},{}]) = {}),
00321   assert(f([{},{{}}]) = {}),
00322   assert(f([{1},{}]) = {}),
00323   assert(f([{1},{{}}]) = {}),
00324   assert(f([{1,2},{{[1,5]}}]) = {5}),
00325   assert(f([{1,3,5},{{[1,11],[3,22]},{[5,11],[3,33]}}]) = {11,22,33}),
00326   true)$
00327 
00328 okltest_lit_nbfcs(f) := (
00329   assert(f([{},{}]) = {}),
00330   assert(f([{},{{}}]) = {}),
00331   assert(okltest_lit_nbcs(buildq([f], lambda([F], f(nbcs2nbfcs(F))))) = true),
00332   true)$
00333 
00334 okltest_snbfcs_p(f) := (
00335   assert(f(0) = false).
00336   assert(f([0]) = false),
00337   assert(f([0,0]) = false),
00338   assert(f([{},{}]) = true),
00339   assert(f([{},{{}}]) = true),
00340   assert(f([{1},{{[1,5,1]}}]) = true),
00341   assert(f([{1},{{[2,1,-1]}}]) = false),
00342   assert(f([{1,2},{{[1,-77,-1],[1,88,1]}}]) = false),
00343   assert(f([{1,2},{{[1,-77,-1],[2,88,1]}}]) = true),
00344   true)$
00345 
00346 okltest_var_snbfcs(f) := (
00347   assert(f([{},{}]) = {}),
00348   assert(f([{},{{}}]) = {}),
00349   assert(f([{1},{}]) = {1}),
00350   assert(f([{1},{{}}]) = {1}),
00351   assert(f([{1,2},{{[1,5,1]}}]) = {1,2}),
00352   true)$
00353 
00354 okltest_val_snbfcs(f) := (
00355   assert(f([{},{}]) = {}),
00356   assert(f([{},{{}}]) = {}),
00357   assert(f([{1},{}]) = {}),
00358   assert(f([{1},{{}}]) = {}),
00359   assert(f([{1,2},{{[1,5,-1]}}]) = {5}),
00360   assert(f([{1,3,5},{{[1,11,1],[3,22,-1]},{[5,11,1],[3,33,-1]}}]) = {11,22,33}),
00361   true)$
00362 
00363 okltest_sgn_snbfcs(f) := (
00364   assert(f([{},{}]) = {}),
00365   assert(f([{},{{}}]) = {}),
00366   assert(f([{1},{}]) = {}),
00367   assert(f([{1},{{}}]) = {}),
00368   assert(f([{1,2},{{[1,5,-1]}}]) = {-1}),
00369   assert(f([{1,3,5},{{[1,11,1],[3,22,-1]},{[5,11,1],[3,33,-1]}}]) = {1,-1}),
00370   true)$
00371 
00372 okltest_lit_snbfcs(f) := (
00373   assert(f([{},{}]) = {}),
00374   assert(f([{},{{}}]) = {}),
00375   assert(okltest_lit_snbcs(buildq([f], lambda([F], f(snbcs2snbfcs(F))))) = true),
00376   true)$
00377 
00378 okltest_nbfcl_p(f) := (
00379   assert(f(0) = false).
00380   assert(f([0]) = false),
00381   assert(f([0,0]) = false),
00382   assert(f([{},[]]) = false),
00383   assert(f([[],{}]) = false),
00384   assert(f([[],[]]) = true),
00385   assert(f([[],[{}]]) = true),
00386   assert(f([[1],[{[1,5]}]]) = true),
00387   assert(f([[1],[{[2,1]}]]) = false),
00388   assert(f([[1,2],[{[1,10],[2,11]}]]) = true),
00389   assert(f([[1,2,2],[{[1,10],[2,11]}]]) = false),
00390   /* XXX */
00391   true)$
00392 
00393 okltest_var_nbfcl(f) := (
00394   assert(f([[],[]]) = []),
00395   assert(f([[],[{}]]) = []),
00396   assert(f([[1],[]]) = [1]),
00397   assert(f([[1],[{}]]) = [1]),
00398   assert(f([[1,2],[{[1,5]}]]) = [1,2]),
00399   assert(f([[2,1],[{[1,5]}]]) = [2,1]),
00400   assert(okltest_var_nbfcs(buildq([f],lambda([FF],setify(f(nbfcs2nbfcl(FF)))))) = true),
00401   true)$
00402 
00403 okltest_val_nbfcl(f) := (
00404   assert(f([[],[]]) = {}),
00405   assert(f([[],[{}]]) = {}),
00406   assert(f([[1],[]]) = {}),
00407   assert(f([[1],[{}]]) = {}),
00408   assert(f([[1,2],[{[1,5]}]]) = {5}),
00409   assert(f([[1,3,5],[{[1,11],[3,22]},{[5,11],[3,33]}]]) = {11,22,33}),
00410   assert(okltest_val_nbfcs(buildq([f],lambda([FF],f(nbfcs2nbfcl(FF))))) = true),
00411   true)$
00412 
00413 okltest_lit_nbfcl(f) := (
00414   assert(f([[],[]]) = {}),
00415   assert(f([[],[{}]]) = {}),
00416   assert(okltest_lit_nbcl(buildq([f], lambda([F], f(nbcl2nbfcl(F))))) = true),
00417   true)$
00418 
00419 okltest_snbfcl_p(f) := (
00420   assert(f(0) = false).
00421   assert(f([0]) = false),
00422   assert(f([0,0]) = false),
00423   assert(f([{},[]]) = false),
00424   assert(f([[],{}]) = false),
00425   assert(f([[],[]]) = true),
00426   assert(f([[],[{}]]) = true),
00427   assert(f([[1],[{[1,5,1]}]]) = true),
00428   assert(f([[1],[{[2,1,1]}]]) = false),
00429   assert(f([[1,2],[{[1,10,-1],[2,11,-1]}]]) = true),
00430   assert(f([[1,2,2],[{[1,10,1],[2,11,1]}]]) = false),
00431   /* XXX */
00432   true)$
00433 
00434 okltest_var_snbfcl(f) := (
00435   assert(f([[],[]]) = {}),
00436   assert(f([[],[{}]]) = {}),
00437   assert(f([[1],[]]) = {1}),
00438   assert(f([[1],[{}]]) = {1}),
00439   assert(f([[1,2],[{[1,5,-1]}]]) = {1,2}),
00440   assert(okltest_var_snbfcs(buildq([f],lambda([FF],f(snbfcs2snbfcl(FF))))) = true),
00441   true)$
00442 
00443 okltest_val_snbfcl(f) := (
00444   assert(f([[],[]]) = {}),
00445   assert(f([[],[{}]]) = {}),
00446   assert(f([[1],[]]) = {}),
00447   assert(f([[1],[{}]]) = {}),
00448   assert(f([[1,2],[{[1,5,1]}]]) = {5}),
00449   assert(f([[1,3,5],[{[1,11,-1],[3,22,1]},{[5,11,1],[3,33,-1]}]]) = {11,22,33}),
00450   assert(okltest_val_snbfcs(buildq([f],lambda([FF],f(snbfcs2snbfcl(FF))))) = true),
00451   true)$
00452 
00453 okltest_sgn_snbfcl(f) := (
00454   assert(f([[],[]]) = {}),
00455   assert(f([[],[{}]]) = {}),
00456   assert(f([[1],[]]) = {}),
00457   assert(f([[1],[{}]]) = {}),
00458   assert(f([[1,2],[{[1,5,1]}]]) = {1}),
00459   assert(f([[1,3,5],[{[1,11,-1],[3,22,1]},{[5,11,1],[3,33,-1]}]]) = {1,-1}),
00460   assert(okltest_sgn_snbfcs(buildq([f],lambda([FF],f(snbfcs2snbfcl(FF))))) = true),
00461   true)$
00462 
00463 okltest_lit_snbfcl(f) := (
00464   assert(f([[],[]]) = {}),
00465   assert(f([[],[{}]]) = {}),
00466   assert(okltest_lit_snbcl(buildq([f], lambda([F], f(snbcl2snbfcl(F))))) = true),
00467   true)$
00468 
00469 okltest_nbfcsud_p(f) := (
00470   assert(f(0) = false),
00471   assert(f([]) = false),
00472   assert(f([0,0,0]) = false),
00473   assert(f([{},{},{}]) = true),
00474   assert(f([{1},{},{10}]) = true),
00475   assert(f([{1},{{}},{10}]) = true),
00476   assert(f([{1},{{[2,10]}},{10}]) = false),
00477   assert(f([{1},{{[1,11]}},{10}]) = false),
00478   assert(f([{1},{{[1,10]}},{10}]) = true),
00479   /* XXX */
00480   true)$
00481 
00482 okltest_snbfcsud_p(f) := (
00483   assert(f(0) = false),
00484   assert(f([]) = false),
00485   assert(f([0,0,0]) = false),
00486   assert(f([{},{},{}]) = true),
00487   assert(f([{1},{},{10}]) = true),
00488   assert(f([{1},{{}},{10}]) = true),
00489   assert(f([{1},{{[2,10,1]}},{10}]) = false),
00490   assert(f([{1},{{[1,11,-1]}},{10}]) = false),
00491   assert(f([{1},{{[1,10]}},{10}]) = false),
00492   assert(f([{1,2},{{[2,10,1]},{[1,11,-1]}},{10}]) = false),
00493   assert(f([{1,2},{{[2,10,1]},{[1,11,-1]}},{10,11}]) = true),
00494   true)$
00495 
00496 okltest_nbfclud_p(f) := block(
00497   assert(f(0) = false),
00498   assert(f([]) = false),
00499   assert(f([0,0,0]) = false),
00500   assert(f([[],[],[]]) = true),
00501   assert(f([[1],[],[10]]) = true),
00502   assert(f([[1],[{}],[10]]) = true),
00503   assert(f([[1],[{[2,10]}],[10]]) = false),
00504   assert(f([[1],[{[1,11]}],[10]]) = false),
00505   assert(f([[1],[{[1,10]}],[10]]) = true),
00506   assert(f([[1,2],[{[1,10]}],[10,11]]) = true),
00507   assert(f([[1,2,1],[{[1,10]}],[10,11]]) = false),
00508   assert(f([[1,2],[{[1,10]}],[10,11,11]]) = false),
00509   /* XXX */
00510   true)$
00511 
00512 okltest_snbfclud_p(f) := block(
00513   assert(f(0) = false),
00514   assert(f([]) = false),
00515   assert(f([0,0,0]) = false),
00516   assert(f([[],[],[]]) = true),
00517   assert(f([[1],[],[10]]) = true),
00518   assert(f([[1],[{}],[10]]) = true),
00519   assert(f([[1],[{[2,10,1]}],[10]]) = false),
00520   assert(f([[1],[{[1,11,1]}],[10]]) = false),
00521   assert(f([[1],[{[1,10,1]}],[10]]) = true),
00522   assert(f([[1,2],[{[1,10,-1]}],[10,11]]) = true),
00523   assert(f([[1,2,1],[{[1,10,1]}],[10,11]]) = false),
00524   assert(f([[1,2],[{[1,10,1]}],[10,11,11]]) = false),
00525   assert(f([[1,2],[{[1,10,1]},{[2,12,-1]}],[10,11,12]]) = true),
00526   true)$
00527 
00528 okltest_nbfcsfd_p(f) := block([D],
00529   assert(f(0) = false),
00530   assert(f([]) = false),
00531   assert(f([0,0,0]) = false),
00532   assert(f([{},{},{}]) = true),
00533   assert(f([{1},{},D]) = true),
00534   assert(f([{1},{{[1,10]}},D]) = false),
00535   assert(f([{1},{{[1,10]}},lambda([x],11)]) = false),
00536   assert(f([{1},{{[1,10]}},lambda([x],10)]) = false),
00537   assert(f([{1},{{[1,10]}},lambda([x],{10})]) = true),
00538   /* XXX */
00539   true)$
00540 
00541 okltest_snbfcsfd_p(f) := block([D],
00542   assert(f(0) = false),
00543   assert(f([]) = false),
00544   assert(f([0,0,0]) = false),
00545   assert(f([{},{},{}]) = true),
00546   assert(f([{1},{},D]) = true),
00547   assert(f([{1},{{[1,10]}},D]) = false),
00548   assert(f([{1},{{[1,10]}},lambda([x],11)]) = false),
00549   assert(f([{1},{{[1,10]}},lambda([x],10)]) = false),
00550   assert(f([{1},{{[1,10]}},lambda([x],{10})]) = false),
00551   assert(f([{1},{{[1,10,1]}},lambda([x],{10})]) = true),
00552   assert(f([{1,2},{{[1,77,1],[2,88,-1]}},lambda([x],{77})]) = false),
00553   assert(f([{1,2},{{[1,77,1],[2,88,-1]}},lambda([x],if x=1 then {77} else {88})]) = true),
00554   true)$
00555 
00556 okltest_nbfclfd_p(f) := block([D],
00557   assert(f(0) = false),
00558   assert(f([]) = false),
00559   assert(f([0,0,0]) = false),
00560   assert(f([[],[],[]]) = true),
00561   assert(f([[1],[],D]) = true),
00562   assert(f([[1],[{[1,10]}],D]) = false),
00563   assert(f([[1],[{[1,10]}],lambda([x],11)]) = false),
00564   assert(f([[1],[{[1,10]}],lambda([x],10)]) = false),
00565   assert(f([[1],[{[1,10]}],lambda([x],{10})]) = false),
00566   assert(f([[1],[{[1,10]}],lambda([x],[10])]) = true),
00567   /* XXX */
00568   true)$
00569 
00570 okltest_snbfclfd_p(f) := block([D],
00571   assert(f(0) = false),
00572   assert(f([]) = false),
00573   assert(f([0,0,0]) = false),
00574   assert(f([[],[],[]]) = true),
00575   assert(f([[1],[],D]) = true),
00576   assert(f([[1],[{[1,10,1]}],D]) = false),
00577   assert(f([[1],[{[1,10,-1]}],lambda([x],11)]) = false),
00578   assert(f([[1],[{[1,10,1]}],lambda([x],10)]) = false),
00579   assert(f([[1],[{[1,10,1]}],lambda([x],{10})]) = false),
00580   assert(f([[1],[{[1,10,1]}],lambda([x],[10])]) = true),
00581   assert(f([[1,2],[{[1,77,1],[2,88,-1]}],lambda([x],[77])]) = false),
00582   assert(f([[1,2],[{[1,77,1],[2,88,-1]}],lambda([x],if x=1 then [77] else [88])]) = true),
00583   true)$
00584 
00585 okltest_nbfcsfd_equalp(f) := block(
00586   /* XXX */
00587   true)$
00588 
00589 
00590 /* ***************
00591    * Conversions *
00592    ***************
00593 */
00594 
00595 okltest_nbcs2nbcl(f) := (
00596   assert(f({}) = []),
00597   assert(f({{}}) = [{}]),
00598   /* XXX */
00599   true)$
00600 
00601 okltest_nbcl2nbcs(f) := (
00602   assert(f([]) = {}),
00603   assert(f([{}]) = {{}}),
00604   /* XXX */
00605   true)$
00606 
00607 okltest_nbfcs2nbfcl(f) := (
00608   assert(f([{},{}]) = [[],[]]),
00609   assert(f([{},{{}}]) = [[],[{}]]),
00610   /* XXX */
00611   true)$
00612 
00613 okltest_snbfcs2snbfcl(f) := (
00614   assert(f([{},{}]) = [[],[]]),
00615   assert(f([{},{{}}]) = [[],[{}]]),
00616   /* XXX */
00617   true)$
00618 
00619 okltest_nbfcl2nbfcs(f) := (
00620   assert(f([[],[]]) = [{},{}]),
00621   assert(f([[],[{}]]) = [{},{{}}]),
00622   /* XXX */
00623   true)$
00624 
00625 okltest_snbfcl2snbfcs(f) := (
00626   assert(f([[],[]]) = [{},{}]),
00627   assert(f([[],[{}]]) = [{},{{}}]),
00628   /* XXX */
00629   true)$
00630 
00631 okltest_nbfcs2nbcs(f) := block([A,B],
00632   assert(f([A,B]) = B),
00633   /* XXX */
00634   true)$
00635 
00636 okltest_nbfcl2nbcl(f) := block([A,B],
00637   assert(f([A,B]) = B),
00638   /* XXX */
00639   true)$
00640 
00641 okltest_nbfcsud2nbfclud(f) := (
00642   assert(f([{},{},{}]) = [[],[],[]]),
00643   assert(f([{1,2,3},{{}},{10,11,12}]) = [[1,2,3],[{}],[10,11,12]]),
00644   /* XXX */
00645   true)$
00646 
00647 okltest_nbfclud2nbfcsud(f) := (
00648   assert(f([[],[],[]]) = [{},{},{}]),
00649   assert(f([[1,2,3],[{}],[10,11,12]]) = [{1,2,3},{{}},{10,11,12}]),
00650   /* XXX */
00651   true)$
00652 
00653 okltest_nbfcsfd2nbfclfd(f) := block([D],
00654   assert(nbfcsfd_equalp(f([{},{},D]), [[],[],D]) = true),
00655   assert(nbfcsfd_equalp(f([{1,2,3},{{}},D]), [[1,2,3],[{}],D]) = true),
00656   assert(nbfcsfd_equalp(f([{1,5},{},lambda([x],{1,2})]), [[1,5],[],lambda([x],[1,2])]) = true),
00657   /* XXX */
00658   true)$
00659 
00660 okltest_snbfcsfd2snbfclfd(f) := block([D],
00661   assert(nbfcsfd_equalp(f([{},{},D]), [[],[],D]) = true),
00662   assert(nbfcsfd_equalp(f([{1,2,3},{{}},D]), [[1,2,3],[{}],D]) = true),
00663   assert(nbfcsfd_equalp(f([{1,5},{},lambda([x],{1,2})]), [[1,5],[],lambda([x],[1,2])]) = true),
00664   /* XXX */
00665   true)$
00666 
00667 okltest_nbfclfd2nbfcsfd(f) := block([D],
00668   assert(nbfcsfd_equalp(f([[],[],D]), [{},{},D])),
00669   assert(nbfcsfd_equalp(f([[1,2,3],[{}],lambda([x],[x])]), [{1,2,3},{{}},lambda([x],{x})])),
00670   /* XXX */
00671   true)$
00672 
00673 okltest_snbfclfd2snbfcsfd(f) := block([D],
00674   assert(nbfcsfd_equalp(f([[],[],D]), [{},{},D])),
00675   assert(nbfcsfd_equalp(f([[1,2,3],[{}],lambda([x],[x])]), [{1,2,3},{{}},lambda([x],{x})])),
00676   /* XXX */
00677   true)$
00678 
00679 okltest_nbcs2nbfcs(f) := (
00680   assert(f({}) = [{},{}]),
00681   assert(f({{}}) = [{},{{}}]),
00682   assert(f({{[1,10]}}) = [{1},{{[1,10]}}]),
00683   /* XXX */
00684   true)$
00685 
00686 okltest_snbcs2snbfcs(f) := (
00687   assert(f({}) = [{},{}]),
00688   assert(f({{}}) = [{},{{}}]),
00689   assert(f({{[1,10,-1]}}) = [{1},{{[1,10,-1]}}]),
00690   /* XXX */
00691   true)$
00692 
00693 okltest_nbcl2nbfcl(f) := (
00694   assert(f([]) = [[],[]]),
00695   assert(f([{}]) = [[],[{}]]),
00696   assert(f([{[1,10]}]) = [[1],[{[1,10]}]]),
00697   assert(f([{[2,10],[3,11]},{[1,20]}]) = [[1,2,3],[{[2,10],[3,11]},{[1,20]}]]),
00698   /* XXX */
00699   true)$
00700 
00701 okltest_snbcl2snbfcl(f) := (
00702   assert(f([]) = [[],[]]),
00703   assert(f([{}]) = [[],[{}]]),
00704   assert(f([{[1,10]}]) = [[1],[{[1,10]}]]),
00705   assert(f([{[2,10,1],[3,11,-1]},{[1,20,1]}]) = [[1,2,3],[{[2,10,1],[3,11,-1]},{[1,20,1]}]]),
00706   /* XXX */
00707   true)$
00708 
00709 okltest_nbfcs2nbfcsud(f) := (
00710   assert(f([{},{}]) = [{},{},{}]),
00711   assert(f([{},{{}}]) = [{},{{}},{}]),
00712   assert(f([{1,3},{{[1,10],[3,30]}}]) = [{1,3},{{[1,10],[3,30]}},{10,30}]),
00713   /* XXX */
00714   true)$
00715 
00716 okltest_nbfcl2nbfclud(f) := (
00717   assert(f([[],[]]) = [[],[],[]]),
00718   assert(f([[],[{}]]) = [[],[{}],[]]),
00719   assert(f([[3,1],[{[1,30],[3,10]}]]) = [[3,1],[{[1,30],[3,10]}],[10,30]]),
00720   /* XXX */
00721   true)$
00722 
00723 okltest_nbfcsud2nbfcsfd(f) := block([D],
00724   assert(nbfcsfd_equalp(f([{},{},{}]), [{},{},D]) = true),
00725   assert(nbfcsfd_equalp(f([{},{{}},{}]), [{},{{}},D])),
00726   /* XXX */
00727   true)$
00728 
00729 okltest_snbfcsud2snbfcsfd(f) := block([D],
00730   assert(nbfcsfd_equalp(f([{},{},{}]), [{},{},D]) = true),
00731   assert(nbfcsfd_equalp(f([{},{{}},{}]), [{},{{}},D])),
00732   /* XXX */
00733   true)$
00734 
00735 okltest_nbfclud2nbfclfd(f) := block([D],
00736   assert(nbfcsfd_equalp(f([[],[],[]]), [[],[],D]) = true),
00737   assert(nbfcsfd_equalp(f([[1,3,2],[{[1,77]},{[1,88]},{[2,33]}],[33,77,88]]), [[1,3,2],[{[1,77]},{[1,88]},{[2,33]}],lambda([v],[33,77,88])]) = true),
00738   /* XXX */
00739   true)$
00740 
00741 okltest_snbfclud2snbfclfd(f) := block([D],
00742   assert(nbfcsfd_equalp(f([[],[],[]]), [[],[],D]) = true),
00743   assert(nbfcsfd_equalp(f([[1,3,2],[{[1,77,1]},{[1,88,-1]},{[2,33,1]}],[33,77,88]]), [[1,3,2],[{[1,77,1]},{[1,88,-1]},{[2,33,1]}],lambda([v],[33,77,88])]) = true),
00744   /* XXX */
00745   true)$
00746 
00747