OKlibrary  0.2.1.6
uhit_def.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 1.5.2008 (Guangzhou) */
00002 /* Copyright 2008, 2009, 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/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Symmetries/Symmetries.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00030 
00031 
00032 kill(f)$
00033 
00034 
00035 okltest_uhit_def(f) := block([list_def : f[0,"info"]],
00036   assert(listp(list_def) = true),
00037   assert(emptyp(list_def) = false),
00038   for k in list_def do block([info,status_def,minn,maxn,list_n],
00039     assert(k >= 1),
00040     info : f[k,"info"],
00041     assert(listp(info) = true),
00042     assert(length(info) = 4),
00043     status_def : info[1],
00044     assert(elementp(status_def,{true,false,unknown}) = true),
00045     minn : info[2], maxn : info[3],
00046     assert(minn <= maxn),
00047     list_n : info[4],
00048     assert(listp(list_n) = true),
00049     assert(emptyp(list_n) = false),
00050     for p in list_n do block([LF,n,status],
00051       assert(listp(p) = true),
00052       assert(length(p) = 2),
00053       [n,status] : p,
00054       if status_def=true then
00055         assert(status = true)
00056       else
00057         assert(elementp(status,{true,false,unknown}) = true),
00058       assert(minn <= n),
00059       assert(n <= maxn),
00060       LF : f[k,n],
00061       assert(listp(LF) = true),
00062       assert(emptyp(LF) = false),
00063       if oklib_test_level >= 1 then
00064         for F in LF do block([check : check_hitting_nsing_def(F)],
00065           assert(listp(check) = true),
00066           assert(length(check) = 1),
00067           assert(check[1] = k),
00068           assert(nvar_cs(F) = n)
00069         ),
00070       if oklib_test_level >= 1 then
00071         assert(length(representatives_cs(setify(LF))) = length(LF))
00072     )
00073   ),
00074   true)$
00075 
00076 /* *************************************
00077    * Bounds on the deficiency and on n *
00078    *************************************
00079 */
00080 
00081 okltest_max_def_uhit_n(f) := (
00082   assert(f(0) = 1),
00083   assert(f(1) = 1),
00084   assert(f(2) = 2),
00085   assert(f(3) = 5),
00086   assert(f(4) = 12),
00087   assert(f(5) = 27),
00088   true)$
00089 
00090 okltest_min_n_uhit_def(f) := (
00091   assert(f(1) = 0),
00092   assert(f(2) = 2),
00093   for k : 3 thru if oklib_test_level=0 then 3 else 10 do block([n : f(k)],
00094     assert(max_def_uhit_n(n) >= k),
00095     assert(max_def_uhit_n(n-1) < k)
00096   ),
00097   true)$
00098 
00099 
00100 /* ***************************
00101    * Accessing the catalogue *
00102    ***************************
00103 */
00104 
00105 okltest_all_uhit_def(f) := (
00106   assert(f(1) = [{{}}]),
00107   assert(f(2) = [{{-1,-2},{-1,2},{1,-2},{1,2}}, {{1,2,3},{-1,-2,-3},{-1,2},{-2,3},{-3,1}}]),
00108   true)$
00109 
00110 okltest_collect_uhit_n(f) := (
00111   assert(f(0,0,0) = {}),
00112   assert(f(0,0,1) = { {{}} }),
00113   assert(f(0,0,2) = { {{}} }),
00114   assert(f(0,1,2) = { {{}} }),
00115   assert(f(0,2,2) = {}),
00116   assert(f(1,0,0) = {}),
00117   assert(f(1,0,1) = {}),
00118   assert(f(1,0,2) = {}),
00119   assert(f(2,0,1) = {}),
00120   assert(f(2,2,2) = { {{-1,-2},{-1,2},{1,-2},{1,2}} }),
00121   assert(f(2,2,10) = { {{-1,-2},{-1,2},{1,-2},{1,2}} }),
00122   assert(f(3,2,2) = { {{1,2,3},{-1,-2,-3},{-1,2},{-2,3},{-3,1}} }),
00123   true)$
00124 
00125 okltest_uhit_n_data(f) := block([L : f()],
00126   assert(length(L[1]) = length(L[2])),
00127   assert(length(L[2]) = length(L[3])),
00128   assert(take_l(12,L[1]) = create_list(i,i,0,11)),
00129   /* XXX */
00130   true)$
00131 
00132 okltest_uhit_n(f) := (
00133   assert(take_elements(6,f(-1,true)) = create_list(k,k,0,5)),
00134   assert(take_elements(6,f(-1,false)) = create_list(k,k,0,5)),
00135   assert(f(0,true) = true),
00136   assert(length(f(0,false)) = 1),
00137   assert(f(1,true) = true),
00138   assert(length(f(1,false)) = 0),
00139   assert(f(2,true) = true),
00140   assert(length(f(2,false)) = 1),
00141   assert(f(3,true) = true),
00142   assert(length(f(3,false)) = 6),
00143   assert(f(4,true) = true),
00144   assert(length(f(4,false)) = 368),
00145   true)$
00146 
00147 
00148 /* ****************************
00149    * Evaluating the catalogue *
00150    ****************************
00151 */
00152 
00153 okltest_classify_candidates_uhit_def(f) := block(
00154   assert(f([]) = []),
00155   assert(f([{}]) = [false]),
00156   assert(f([{{1}}]) = [false]),
00157   if oklib_test_level = 0 then return(true),
00158   assert(f([{},{{}},{{1}},{{1},{-1}},full_fcs(2)[2],full_fcs(3)[2],full_fcs(8)[2]]) = [false,[[1,0],1],false,false,[[2,2],1],[[5,3],1],[[248,8],"new"]]),
00159   true)$
00160 
00161 okltest_analyse_isorepo_defset_mvd(f) := block([h,FF1,FF2],
00162   h : sm2hm({}),
00163   assert(f(h) = []),
00164   manage_repository_isomorphism_types([{},{{}}],h),
00165   assert(f(h) = [[1,{}]]),
00166   if oklib_test_level = 0 then return(true),
00167   manage_repository_isomorphism_types(full_fcs(2),h),
00168   assert(f(h) = [[1,{}],[2,{}]]),
00169   manage_repository_isomorphism_types(full_fcs(3),h),
00170   assert(f(h) = [[1,{}],[2,{}],[5,{}]]),
00171   FF1 : full_fcs(6),
00172   manage_repository_isomorphism_types(FF1,h),
00173   assert(f(h) = [[1,{}],[2,{}],[5,{}],[58,{}]]),
00174   FF2 : full_fcs(8),
00175   manage_repository_isomorphism_types(FF2,h),
00176   assert(f(h) = [[1,{}],[2,{}],[5,{}],[58,{}],[248,{FF2[2]}]]),
00177   true)$
00178 
00179 /* ****************************
00180    * Completing the catalogue *
00181    ****************************
00182 */
00183 
00184