OKlibrary  0.2.1.6
RBases.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 28.12.2009 (Swansea) */
00002 /* Copyright 2009, 2010, 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/Reductions/UnitClausePropagation.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/Basics.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/tests/Basics.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/GeneralisedUCP.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/tests/Cores.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00031 
00032 kill(f)$
00033 
00034 
00035 /* *****************
00036    * Basic notions *
00037    *****************
00038 */
00039 
00040 okltest_rgen0_p_cs(f) := block([r],
00041   assert(f({},{},r) = true),
00042   assert(f({},{{}},identity) = false),
00043   assert(f({{}},{{}},identity) = true),
00044   assert(f({{}},{{},{1}},identity) = true),
00045   assert(f({{}},{},r) = true),
00046   assert(f({{}},{},r) = true),
00047   assert(f({{}},{{1}},identity) = true),
00048   assert(f({{1},{-1}},{},r) = true),
00049   assert(f({{1},{-1}},{{}},identity) = false),
00050   assert(f({{1},{-1}},{{}},ucp_0_cs) = true),
00051   assert(f({{1},{-1}},{{2}},identity) = false),
00052   assert(f({{1},{-1}},{{2}},ucp_0_cs) = true),
00053   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}},{{}},ucp_0_cs) = false),
00054   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}},{{}},generalised_ucp2) = true),
00055   true)$
00056 
00057 okltest_rgen0_p_cl(f) := block([r,r1],
00058   assert(f([],[],r) = true),
00059   assert(f([{1}],[],r) = true),
00060   assert(f([{1,2},{-1}],[{2}],identity) = false),
00061   r1 : lambda([F], cs2cl(ucp_0_cs(cl2cs(F)))),
00062   assert(f([{1,2},{-1}],[{2}],r1) = true),
00063   assert(okltest_rgen0_p_cs(buildq([f], lambda([G,F,r_], f(cs2cl(G), cs2cl(F), buildq([r_], lambda([H], cs2cl(r_(cl2cs(H))))))))) = true),
00064   true)$
00065 
00066 okltest_rgen_p_cs(f) := (
00067 
00068   true)$
00069 
00070 okltest_rbase_p_cs(f) := (
00071 
00072   true)$
00073 
00074 okltest_all_rbases_bydef(f) := (
00075 
00076   true)$
00077 
00078 
00079 /* ************
00080    * Sampling *
00081    ************
00082 */
00083 
00084 okltest_rand_rbase_cs(f) := block(
00085  [S, R, fr, F0,res0,core0,add0, s : make_random_state(false)],
00086   assert(f({},ucp_0_cs) = {}),
00087   assert(f({{}},ucp_0_cs) = {{}}),
00088   for n : 0 thru 5 do block([F : setify(create_list({i},i,1,n))],
00089     assert(f(F,ucp_0_cs) = F)),
00090   assert(f({{},{1}},ucp_0_cs) = {{}}),
00091   assert(f({{1},{-1},{2}},ucp_0_cs) = {{1},{-1}}),
00092   set_random(0),
00093   assert(f({{1},{-1},{2},{-2}},ucp_0_cs) =  {{1},{-1}}),
00094   set_random(1),
00095   assert(f({{1},{-1},{2},{-2}},ucp_0_cs) =  {{2},{-2}}),
00096   assert(f({{1,2,3},{-1,3,4},{2,3,4}},ucp_0_cs) = {{1,2,3},{-1,3,4}}),
00097   assert(f({{1,2,3},{-1,3,4},{2,3,4},{3,-4,5},{2,3,5}},ucp_0_cs) = {{1,2,3},{-1,3,4},{3,-4,5}}),
00098   assert(f({{1,2,3},{2,-3,4},{1,2,4},{5,-6,7},{-4,5,6},{-4,5,7},{1,2,5,7}},ucp_0_cs) = {{1,2,3},{2,-3,4},{5,-6,7},{-4,5,6}}),
00099   core0 : {{1,2,-3,7},{1,2,3,7},{-1,7},{4,5,-6,-7},{4,5,6,-7},{-5,-7}},
00100   add0 : {{2,7,8},{4,-7,8},{2,4,8}},
00101   F0 : union(core0,add0),
00102   for n : 0 thru 15 do block([res0],
00103     set_random(n),
00104     res0 : f(F0,ucp_0_cs),
00105     assert(subsetp(core0,res0) = true),
00106     assert(setdifference(res0,core0) = if elementp(n,{0,2,3,10}) then {{2,4,8}} elseif elementp(n,{1,4,5,6,7,9,11,12,13,14}) then {{4,-7,8}} elseif elementp(n,{8,15}) then {{2,7,8}})
00107   ),
00108   assert(f(F0,weakest_reduction_cs) = F0),
00109   assert(okltest_subsumption_elimination_cs(buildq([f], lambda([F], f(F,weakest_reduction_cs)))) = true),
00110   assert(okltest_subsumption_elimination_cs(buildq([f], lambda([F], f(F,generalised_ucp0_cs)))) = true),
00111   S : dll_simplest_first_shortest_clause,
00112   R : buildq([S],lambda([F], strongest_reduction_cs(F,S))),
00113   assert(f(F0,R) = core0),
00114   fr : buildq([f,R],lambda([F], f(F,R))),
00115   assert(okltest_some_irr_cs(fr) = true),
00116   /* XXX */
00117   set_random_state(s),
00118   true)$
00119