OKlibrary  0.2.1.6
InverseSingularDP.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 14.6.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 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/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/DP-Reductions.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Symmetries/Symmetries.mac")$
00028 
00029 kill(f)$
00030 
00031 /* ********************************
00032    * Performing single extensions *
00033    ********************************
00034 */
00035 
00036 okltest_new_var_fcs(f) := (
00037   assert(f([{},{}]) = 1),
00038   assert(f([{},{{}}]) = 1),
00039   assert(f([{1},{}]) = 2),
00040   assert(f([{3},{{}}]) = 4),
00041   true)$
00042 
00043 okltest_random_sublist(f) := (
00044   assert(f({},0) = []),
00045   assert(f({},1) = []),
00046   assert(f(setn(10),0) = []),
00047   assert(f(setn(10),1) = create_list(i,i,1,10)),
00048   assert(subsetp(setify(f(create_list(i,i,1,10),0.5)), setn(10)) = true),
00049   true)$
00050 
00051 okltest_basic_inverse_singulardp_fcs(f) := block([FF],
00052   FF : [{},{{}}],
00053   assert(f(FF,{{}},0,0) = true),
00054   assert(FF = [{1},{{1},{-1}}]),
00055   assert(f(FF,{{1}},0,0) = true),
00056   assert(FF = [{1,2},{{2},{1,-2},{-1}}]),
00057   assert(f(FF,{{2},{-1}},1,1) = true),
00058   assert(FF = [{1,2,3},{{3},{2,-3},{-1,-3},{1,-2}}]),
00059   assert(f(FF,{{2,-3},{-1,-3}},1,0) = true),
00060   assert(FF = [setn(4), {{4,-3},{-4,2},{-4,-1},{3},{1,-2}}]),
00061   assert(f(FF,{{-4,2},{-4,-1}},1,1) = true),
00062   assert(FF = [setn(5), {{5,-4},{-5,-4,2},{-5,-4,-1},{4,-3},{3},{1,-2}}]),
00063   assert(f(FF,{{5,-4},{-5,-4,3}},0.5,0.5) = true),
00064   FF : full_fcs(3),
00065   assert(f(FF,{{1,2,3},{1,2,-3}},0.5,0.5) = true),
00066   assert(cs_to_fcs(sdp_reduction_cs(FF[2])) = full_fcs(3)),
00067   true)$
00068 
00069 okltest_pre_hitting_extension_fcs_p(f) := (
00070   assert(f([{},{}], {}) = false),
00071   assert(f([{},{}], {{}}) = false),
00072   assert(f([{},{{}}], {}) = false),
00073   assert(f([{},{{}}], {{}}) = true),
00074   assert(f([{1},{{1},{-1}}], {}) = false),
00075   assert(f([{1},{{1},{-1}}], {2}) = false),
00076   assert(f([{1},{{1},{-1}}], {{1}}) = true),
00077   assert(f([{1},{{1},{-1}}], {{1},{-1}}) = true),
00078   assert(f([{1,2},{{1},{2}}], {{1}}) = false),
00079   assert(f([{1,2},{{1},{2}}], {{1},{2}}) = true),
00080   /* XXX */
00081   true)$
00082 
00083 okltest_hitting_extension_fcs_p(f) := (
00084   assert(f([{},{}], {}) = false),
00085   assert(f([{},{}], {{}}) = false),
00086   assert(f([{},{{}}], {}) = false),
00087   assert(f([{},{{}}], {{}}) = true),
00088   assert(f([{1},{{1},{-1}}], {}) = false),
00089   assert(f([{1},{{1},{-1}}], {2}) = false),
00090   assert(f([{1},{{1},{-1}}], {{1}}) = true),
00091   assert(f([{1},{{1},{-1}}], {{1},{-1}}) = true),
00092   assert(f([{1,2},{{1},{2}}], {{1}}) = false),
00093   assert(f([{1,2},{{1},{2}}], {{1},{2}}) = false),
00094   /* XXX */
00095   true)$
00096 
00097 okltest_all_pre_hitting_extensions_fcs(f) := (
00098   assert(f([{},{}]) = {}),
00099   assert(f([{},{{}}]) = { [{1},{{1},{-1}}] }),
00100   assert(f([{1},{{1}}]) = { [{1,2},{{1,-2},{1,2}}] }),
00101   assert(f([{1},{{1},{}}]) = { [{1,2},{{1,-2},{-2},{2}}] }),
00102   assert(f([{1},{{1},{-1}}]) = { [{1,2}, {{1,-2},{1,2},{-1}}], [{1,2}, {{-1,-2},{-1,2},{1}}], [{1,2},{{1,-2},{-1,-2},{2}}] }),
00103   assert(f([{1,2,3}, {{1,3},{2,3},{-3}}]) = { [{1,2,3,4}, {{1,3,-4},{2,3,-4},{-3,-4},{4}}], [{1,2,3,4}, {{1,3,-4},{2,3,-4},{3,4},{-3}}], [{1,2,3,4},{{-3,-4},{-3,4},{1,3},{2,3}}] }),
00104   true)$
00105 
00106 okltest_hittingdivisor_extension_cs(f) := (
00107   assert(f({{}},{{}}) = {{}}),
00108   assert(f({{1}},{{1}}) = {{1}}),
00109   assert(f({{1},{-1}}, {{1}}) = {{1}}),
00110   assert(f({{1},{2}},{{1}}) = {{1},{2}}),
00111   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}},{{1,2}}) = {{1,2}}),
00112   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}},{{1,2},{-1,-2}}) = {{1,2},{-1,2},{1,-2},{-1,-2}}),
00113   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}},{{1,2},{-1,2}}) = {{1,2},{-1,2}}),
00114   assert(okltest_pre_hitting_extension_fcs_p(buildq([f], lambda([FF,G], subsetp(G,FF[2]) and not emptyp(G) and is(f(FF[2],G) = G)))) = true),
00115   true)$
00116 
00117 
00118 /* ********************************
00119    * Performing random extensions *
00120    ********************************
00121 */
00122 
00123 okltest_random_subset_si(f) := (
00124   assert(f({},0,0) = {}),
00125   assert(f({},0,1) = {}),
00126   assert(f({},1,0) = false),
00127   assert(f({{1}},1,0) = {{1}}),
00128   assert(f({{1}},1,1) = {{1}}),
00129   assert(f({{1}},1,2) = false),
00130   assert(f({{1}},2,0) = false),
00131   assert(f({{1}},0,10) = {}),
00132   assert(f({{1},{2}},2,0) = {{1},{2}}),
00133   assert(f({{1},{2}},2,1) = false),
00134   true)$
00135 
00136 okltest_si_inverse_singulardp_fcs(f) := block([FF],
00137   FF : [{},{{}}],
00138   assert(f(FF,0,0,1,1) = false),
00139   assert(FF = [{},{{}}]),
00140   assert(f(FF,0,0,0,1) = true),
00141   assert(FF = [{1},{{-1},{1}}]),
00142   assert(f(FF,0,0,2,1) = false),
00143   assert(FF = [{1},{{-1},{1}}]),
00144   assert(f(FF,1,1,0,2) = true),
00145   assert(FF = [{1,2},{{2},{-1,-2},{1,-2}}]),
00146   assert(f(FF,1,1,1,3) = false),
00147   assert(f(FF,0.5,0.5,1,2) = true),
00148   true)$
00149 
00150 okltest_it_si_inverse_singulardp_fcs(f) := block([FF],
00151   FF : [{},{{}}],
00152   assert(f(FF,1,1,0,1,0) = 0),
00153   assert(FF =  [{},{{}}]),
00154   okltest_si_inverse_singulardp_fcs(buildq([f],
00155     lambda([FF,p,q,a,b],is(f(FF,p,q,a,b,1)=1)))),
00156   assert(f(FF,1,1,0,1,2) = 2),
00157   assert(FF[1] = {1,2}),
00158   assert(is_isomorphic_btr_cs(FF[2],{{1,2},{1,-2},{-1}})),
00159   FF : [{},{}],
00160   assert(f(FF,0,0,0,1,1) = 0),
00161   assert(FF =  [{},{}]),
00162   true)$
00163