OKlibrary  0.2.1.6
PartialAssignments.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 5.7.2008 (Swansea) */
00002 /* Copyright 2008, 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/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/tests/BasicOperations.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Algebra/Lisp/Groupoids/BasicNotions.mac")$
00027 
00028 kill(f)$
00029 
00030 /* ****************************************
00031    * The notion of a "partial assignment" *
00032    ****************************************
00033 */
00034 
00035 okltest_pa_p(f) := block(
00036   assert(f({}) = true),
00037   okltest_c_p(f))$
00038 
00039 
00040 /* ***********************************
00041    * Enumerating partial assignments *
00042    ***********************************
00043 */
00044 
00045 okltest_all_pass(f) := (
00046   assert(f({}) = {{}}),
00047   assert(f({1}) = {{},{1},{-1}}),
00048   assert(f({1,2}) = {{},{-1},{1},{-2},{2},{-1,-2},{-1,2},{1,-2},{1,2}}),
00049   for n : 0 thru 3 do
00050     assert(length(f(setn(n))) = 3^n),
00051   true)$
00052 
00053 okltest_all_pass_l(f) := (
00054   assert(f([]) = [{}]),
00055   assert(f([1]) = [{},{-1},{1}]),
00056   assert(f([3,2]) = [{},{-2},{2},{-3},{-3,-2},{-3,2},{3},{3,-2},{3,2}]),
00057   assert(okltest_all_pass(buildq([f],lambda([V],setify(f(listify(V))))))),
00058   true)$
00059 
00060 okltest_all_pass_n(f) := block(
00061   assert(f({},-1) = {}),
00062   assert(f({1},-1) = {}),
00063   assert(f({},0) = {{}}),
00064   assert(f({1},0) = {{}}),
00065   assert(f({},1) = {}),
00066   assert(f({1},1) = {{-1},{1}}),
00067   for n : 0 thru 3 do
00068     assert(f(setn(n),n) = full_fcs(n)[2]),
00069   if oklib_test_level = 0 then return(true),
00070   block([oklib_test_level : oklib_test_level - 1],
00071     okltest_all_pass(buildq([f],lambda([V],apply(union,create_list(f(V,n),n,0,length(V))))))),
00072   true)$
00073 
00074 okltest_all_tass(f) := block(
00075   assert(f({}) = {{}}),
00076   assert(f({1}) = {{-1},{1}}),
00077   assert(f({1,2}) = {{-2,-1},{-2,1},{-1,2},{1,2}}),
00078   assert(f({2,4,6}) = {{-6,-4,-2},{-6,-4,2},{-6,4,-2},{-6,4,2},{6,-4,-2},{6,-4,2},{6,4,-2},{6,4,2}}),
00079   for n : 3 thru 5 do
00080     assert(length(f(setn(n))) = 2^n),
00081   true)$
00082 
00083 okltest_all_tass_l(f) := (
00084   assert(f([]) = [{}]),
00085   assert(f([1]) = [{-1},{1}]),
00086   assert(f([1,2]) = [{-1,-2},{-1,2},{1,-2},{1,2}]),
00087   assert(f({1,2}) = [{-1,-2},{1,-2},{-1,2},{1,2}]),
00088   assert(f({2,4,6}) = [{-6,-4,-2},{-6,-4,2},{-6,4,-2},{-6,4,2},{6,-4,-2},{6,-4,2},{6,4,-2},{6,4,2}]),
00089   assert(f([2,4,6]) = [{-2,-4,-6},{-2,-4,6},{-2,4,-6},{-2,4,6},{2,-4,-6},{2,-4,6},{2,4,-6},{2,4,6}]),
00090   assert(f([3,1]) = [{-3,-1},{-3,1},{3,-1},{3,1}]),
00091   assert(okltest_all_tass(buildq([f],lambda([V],setify(f(listify(V))))))),
00092   true)$
00093 
00094 
00095 /* ********************
00096    * Basic operations *
00097    ********************
00098 */
00099 
00100 okltest_var_pa(f) := (
00101   assert(f({}) = {}),
00102   assert(f({1}) = {1}),
00103   assert(f({1,-3,4,-5}) = {1,3,4,5}),
00104   true)$
00105 
00106 okltest_restr_c_pa(f) := (
00107   assert(f({},{}) = {}),
00108   assert(f({},{1}) = {}),
00109   assert(f({1},{1}) = {}),
00110   assert(f({-1},{1}) = {}),
00111   assert(f({2},{1}) = {2}),
00112   assert(f({-1,-2},{2}) = {-1}),
00113   true)$
00114 
00115 okltest_compo_pass(f) := (
00116   assert(f({},{}) = {}),
00117   assert(f({},{1}) = {1}),
00118   assert(f({1},{}) = {1}),
00119   assert(f({1},{-1}) = {-1}),
00120   assert(f({-1},{1}) = {1}),
00121   assert(f({1,2,3},{1,-2,-4}) = {1,-2,3,-4}),
00122   true)$
00123 
00124 /* ********************************
00125    * Applying partial assignments *
00126    ********************************
00127 */
00128 
00129 okltest_apply_pa_cs(f) := (
00130   assert(f({},{}) = {}),
00131   assert(f({},{{}}) = {{}}),
00132   assert(f({},{{1},{2}}) = {{1},{2}}),
00133   assert(f({3},{{1},{2}}) = {{1},{2}}),
00134   assert(f({1},{{1},{2}}) = {{2}}),
00135   assert(f({-1},{{1},{2}}) = {{},{2}}),
00136   assert(f({2},{{1},{2}}) = {{1}}),
00137   assert(f({-2},{{1},{2}}) = {{},{1}}),
00138   assert(f({1,2},{{1},{2}}) = {}),
00139   assert(f({-1,2},{{1},{2}}) = {{}}),
00140   assert(f({-1,-2},{{1},{2}}) = {{}}),
00141   true)$
00142 
00143 okltest_apply_pa_cl(f) := (
00144   assert(f({},[]) = []),
00145   assert(f({1,-2},[{},{1},{2},{-1,-2},{-1,3},{-2}]) = [{},{},{3}]),
00146   assert(okltest_apply_pa_cs(buildq([f],lambda([phi,F],cl2cs(f(phi,cs2cl(F))))))),
00147   true)$
00148 
00149 okltest_apply_pa_fcs(f) := (
00150   assert(f({},[{},{}]) = [{},{}]),
00151   assert(f({},[{},{{}}]) = [{},{{}}]),
00152   assert(f({},[{1},{}]) = [{1},{}]),
00153   assert(f({},[{1},{{}}]) = [{1},{{}}]),
00154   assert(f({1},[{},{}]) = [{},{}]),
00155   assert(f({1},[{},{{}}]) = [{},{{}}]),
00156   assert(f({1},[{1},{}]) = [{},{}]),
00157   assert(f({1},[{1},{{}}]) = [{},{{}}]),
00158   true)$
00159 
00160 okltest_apply_pa_ip_cl(f) := block([F],
00161   F : [],
00162   assert(f({},'F) = true),
00163   assert(F = []),
00164   F : [{1},{2},{-3},{1,-2},{2,3}],
00165   assert(f({-1,2,3},'F) = true),
00166   assert(F = [{},{},{}]),
00167   assert(okltest_apply_pa_cl(buildq([f],lambda([phi,F],(f(phi,'F),F))))),
00168   true)$
00169 
00170 
00171 /* ****************************************************
00172    * Analysing partial assignments for satisfyingness *
00173    ****************************************************
00174 */
00175 
00176 okltest_sat_pac_p(f) := (
00177   assert(f({},{}) = false),
00178   assert(f({1},{}) = false),
00179   assert(f({-1},{}) = false),
00180   assert(f({1},{2}) = false),
00181   assert(f({1},{1}) = true),
00182   assert(f({1},{-1}) = false),
00183   assert(f({1},{1,2}) = true),
00184   assert(f({1},{-1,2}) = false),
00185   true)$
00186 
00187 okltest_sat_pacs_p(f) := (
00188   assert(f({},{}) = true),
00189   assert(f({},{{}}) = false),
00190   assert(f({1},{}) = true),
00191   assert(f({1},{{-1}}) = false),
00192   assert(f({1},{{2}}) = false),
00193   true)$
00194 
00195 okltest_sat_paocs_p(f) := (
00196   assert(f({},[]) = true),
00197   assert(okltest_sat_pacs_p(buildq([f],lambda([phi,F],f(phi,cs2ocs(F)))))),
00198   true)$
00199 
00200 okltest_sat_pacl_p(f) := (
00201   assert(f({},[]) = true),
00202   assert(f({1},[{1,2},{1,3}]) = true),
00203   assert(okltest_sat_paocs_p(buildq([f],lambda([phi,F],f(phi,F))))),
00204   true)$
00205 
00206 okltest_sat_pafcs_p(f) := (
00207   assert(f({},[{},{}]) = true),
00208   assert(f({},[{1},{}]) = true),
00209   assert(f({},[{},{{}}]) = false),
00210   assert(f({1},[{1},{{1}}]) = true),
00211   assert(f({1},[{1},{{-1}}]) = false),
00212   assert(okltest_sat_pacs_p(buildq([f],lambda([phi,F],f(phi,cs2fcs(F)))))),
00213   true)$
00214 
00215 okltest_sat_paofcs_p(f) := (
00216   assert(f({},[[],[]]) = true),
00217   assert(okltest_sat_paocs_p(buildq([f],lambda([phi,F],f(phi,ocs2ofcs(F)))))),
00218   true)$
00219 
00220 okltest_sat_pafcl_p(f) := (
00221   assert(f({},[[],[]]) = true),
00222   assert(okltest_sat_paofcs_p(buildq([f],lambda([phi,FF],f(phi,FF))))),
00223   true)$
00224 
00225 okltest_sat_pa_cs(f) := (
00226   assert(f({},{}) = {}),
00227   assert(f({},{{}}) = {}),
00228   assert(f({},{{1}}) = {}),
00229   assert(f({1},{}) = {}),
00230   assert(f({1},{{}}) = {}),
00231   assert(f({1},{{2}}) = {}),
00232   assert(f({1},{{1}}) = {{1}}),
00233   assert(f({1},{{-1}}) = {}),
00234   assert(f({1,-2},{{},{1,2,3},{-1,3},{-2,3},{2,4}}) = {{1,2,3},{-2,3}}),
00235   true)$
00236 
00237 okltest_sat_pa_fcs(f) := (
00238   assert(f({},[{},{}]) = {}),
00239   assert(okltest_sat_pa_cs(buildq([f],lambda([phi,F],f(phi,cs2fcs(F)))))),
00240   true)$
00241 
00242 
00243 /* ************************************************
00244    * Analysing partial assignments for autarkness *
00245    ************************************************
00246 */
00247 
00248 okltest_waut_pacs_p(f) := (
00249   assert(f({},{}) = true),
00250   assert(f({},{{}}) = true),
00251   assert(f({},{{1}}) = true),
00252   assert(f({},{{1},{-1}}) = true),
00253   assert(f({1},{}) = true),
00254   assert(f({1},{{}}) = true),
00255   assert(f({1},{{2}}) = true),
00256   assert(f({1},{{1}}) = true),
00257   assert(f({1},{{-1}}) = false),
00258   assert(f({1},{{-1,2},{}}) = false),
00259   assert(f({1},{{1,2},{}}) = true),
00260   assert(f({1},{{-1,2},{2}}) = true),
00261   true)$
00262 
00263 okltest_aut_pacs_p(f) := (
00264   assert(f({},{}) = true),
00265   assert(f({},{{}}) = true),
00266   assert(f({},{{1}}) = true),
00267   assert(f({},{{1},{-1}}) = true),
00268   assert(f({1},{}) = true),
00269   assert(f({1},{{}}) = true),
00270   assert(f({1},{{2}}) = true),
00271   assert(f({1},{{1}}) = true),
00272   assert(f({1},{{-1}}) = false),
00273   assert(f({1},{{-1,2},{}}) = false),
00274   assert(f({1},{{1,2},{}}) = true),
00275   assert(f({1},{{-1,2},{2}}) = false),
00276   true)$
00277 
00278 okltest_aut_paocs_p(f) := (
00279   assert(f({},[]) = true),
00280   assert(okltest_aut_pacs_p(buildq([f],lambda([phi,F],f(phi,cs2ocs(F)))))),
00281   true)$
00282 
00283 okltest_aut_paofcs_p(f) := (
00284   assert(f({},[[],[]]) = true),
00285   assert(okltest_aut_paocs_p(buildq([f],lambda([phi,F],f(phi,ocs2fcl(F)))))),
00286   true)$
00287 
00288 
00289 /* ********************************************
00290    * Complete analysis of partial assignments *
00291    ********************************************
00292 */
00293 
00294 okltest_analyse_pa_cs(f) := (
00295   assert(f({},{}) = [{},{},{},{}]),
00296   assert(f({},{{}}) = [{},{{}},{},{}]),
00297   assert(f({},{{1},{}}) = [{},{{}},{{1}},{}]),
00298   assert(f({1},{}) = [{},{},{},{}]),
00299   assert(f({1},{{}}) = [{},{{}},{},{}]),
00300   assert(f({1},{{1},{-1},{},{2},{-1,2}}) = [{{1}},{{-1},{}},{{2}},{{-1,2}}]),
00301   true)$
00302 
00303 okltest_analyse_pa_fcs(f) := (
00304   assert(f({},[{},{}]) = [{},{},{},{}]),
00305   assert(okltest_analyse_pa_cs(buildq([f],lambda([phi,F],f(phi,cs2fcs(F)))))),
00306   true)$
00307 
00308 
00309 /* ************************************
00310    * All satisfying assignments bydef *
00311    ************************************
00312 */
00313 
00314 okltest_all_sattass_cs(f) := block(
00315   assert(f({},{}) = {{}}),
00316   okltest_all_tass(buildq([f],lambda([V],f({},V)))),
00317   assert(f({{}},{}) = {}),
00318   assert(f({{}},{1}) = {}),
00319   assert(f({{1}},{}) = {}),
00320   assert(f({{1}},{2}) = {}),
00321   assert(f({{1}},{1}) = {{1}}),
00322   assert(f({{1}},{1,2}) = {{1,2},{1,-2}}),
00323   assert(f({{-1},{1}},{1}) = {}),
00324   true)$
00325 
00326 okltest_all_sattass_ocs(f) := (
00327   assert(f([],[]) = [{}]),
00328   okltest_all_tass_l(buildq([f],lambda([V],f({},V)))),
00329   assert(f([{1,2},{2,3}],[4,2]) = [{-4,2},{4,2}]),
00330   assert(f([{1,2},{2,3}],[1]) = []),
00331   assert(okltest_all_sattass_cs(buildq([f],lambda([F,V],setify(f(cs2ocs(F),listify(V))))))),
00332   true)$
00333 
00334 okltest_all_sat_cs(f) := (
00335   assert(f({}) = {{}}),
00336   assert(f({{}}) = {}),
00337   assert(f({{1,2},{1,-2},{-1,2}}) = {{1,2}}),
00338   true)$
00339 
00340 okltest_all_sat_fcs(f) := (
00341   assert(f([{},{}]) = {{}}),
00342   assert(f([{1,2},{{-1}}]) = {{-1,2},{-1,-2}}),
00343   assert(okltest_all_sat_cs(buildq([f],lambda([F],f(cs2fcs(F)))))),
00344   true)$
00345 
00346 okltest_all_sat_ofcs(f) := (
00347   assert(f([[],[]]) = [{}]),
00348   assert(f([[2,1],[{-1}]]) = [{-2,-1},{2,-1}]),
00349   assert(okltest_all_sat_fcs(buildq([f],lambda([F],setify(f(fcs2ofcs(F))))))),
00350   true)$
00351 
00352 
00353 /* ***********************
00354    * All autarkies bydef *
00355    ***********************
00356 */
00357 
00358 okltest_all_aut_cs(f) := (
00359   assert(f({}) = {{}}),
00360   assert(f({{}}) = {{}}),
00361   assert(f({{1}}) = {{},{1}}),
00362   assert(f({{1},{-1}}) = {{}}),
00363   assert(f({{2},{-1,2}}) = {{},{2},{-1},{-1,2},{1,2}}),
00364   true)$
00365 
00366 okltest_all_aut_ocs(f) := (
00367   assert(f([]) = [{}]),
00368   assert(f([{1}]) = [{},{1}]),
00369   assert(f([{2,3},{-1,2}]) = [{},{-1},{3},{3,-1},{-2,3,-1},{2},{2,-1},{2,1},{2,-3},{2,-3,-1},{2,-3,1},{2,3},{2,3,-1},{2,3,1}]),
00370   assert(okltest_all_aut_cs(buildq([f],lambda([F],setify(f(cs2ocs(F))))))),
00371   true)$
00372 
00373 okltest_all_aut_ofcs(f) := (
00374   assert(f([[2,1],[]]) = [{},{-1},{1},{-2},{-2,-1},{-2,1},{2},{2,-1},{2,1}]),
00375   assert(okltest_all_aut_ocs(buildq([f],lambda([F],f(ocs2ofcs(F)))))),
00376   true)$
00377 
00378 okltest_autmon_cs(f) := block(
00379   if oklib_test_level = 0 then return(true),
00380   assert(okltest_all_aut_cs(buildq([f],lambda([F],
00381     block([M : f(F)], assert(mon_p(M)), M[1]))))),
00382   true)$
00383 
00384 okltest_autmon_ocs(f) := block(
00385   if oklib_test_level = 0 then return(true),
00386   assert(okltest_all_aut_ocs(buildq([f],lambda([F],
00387     block([M : f(F)], assert(mon_p([setify(M[1]),M[2],M[3]])), M[1]))))),
00388   true)$
00389 
00390