OKlibrary  0.2.1.6
MinVarDegrees.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 16.4.2011 (Guangzhou) */
00002 /* Copyright 2011, 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 
00021 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/MinVarDegrees.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/tests/MinVarDegrees.mac")$
00023 
00024 /* **************************
00025    * Number of full clauses *
00026    **************************
00027 */
00028 
00029 okltest_fullclauses_dmu_lb1(fullclauses_dmu_lb1);
00030 okltest_index_Sma_S2_rec(index_Sma_S2_rec);
00031 
00032 okltest_Sma_S2_replica(Sma_S2_replica);
00033 
00034 okltest_fullclauses_dmu_lb1_gen(fullclauses_dmu_lb1_gen);
00035 
00036 okltest_Sma_S2_list(lambda([n], if n=0 then [] else cons(0,create_list(fullclauses_dmu_lb1[k],k,1,n-1))));
00037 okltest_Sma_S2_list(lambda([n], create_list(Sma_S2_bydef(k),k,0,n-1)));
00038 okltest_Sma_S2_list(Sma_S2_list);
00039 
00040 okltest_Sma_bydef(Sma_bydef);
00041 okltest_Sma_start(Sma_start);
00042 okltest_Sma_list(Sma_list);
00043 
00044 okltest_Sma_replica(Sma_replica);
00045 
00046 /* ***************************
00047    * Maximal min-var-degrees *
00048    ***************************
00049 */
00050 
00051 okltest_order_deficiency(order_deficiency);
00052 
00053 /* **************************************
00054    * (Generalised) non-Mersenne numbers *
00055    **************************************
00056 */
00057 
00058 okltest_nonmersenne_rec(nonmersenne_rec);
00059 okltest_nonmersenne_law(nonmersenne_law);
00060 okltest_nonmersenne_lb(nonmersenne_lb);
00061 okltest_nonmersenne_ub(nonmersenne_ub);
00062 
00063 okltest_nonmersenne_dary_jump0(nonmersenne_dary_jump0);
00064 okltest_nonmersenne_dary_rec(nonmersenne_dary_rec);
00065 
00066 okltest_analyse_nonmersenne_rec(analyse_nonmersenne_rec);
00067 
00068 okltest_index_nonmersenne_rec(index_nonmersenne_rec);
00069 okltest_nonmersenne_law(nonmersenne_rec2);
00070 
00071 okltest_step_nonmersenne_rec(step_nonmersenne_rec);
00072 
00073 okltest_nonmersenne_rec(nonmersenne_rec3);
00074 
00075 okltest_possible_degree_pairs_nm(possible_degree_pairs_nm);
00076 okltest_possible_degree_pairs_gen(possible_degree_pairs_gen);
00077 
00078 okltest_nonmersenne_op(nonmersenne_op);
00079 
00080 okltest_nonmersenne_gen_rec(nonmersenne_gen_rec);
00081 
00082 okltest_epoche_nonmersenne_gen(epoche_nonmersenne_gen);
00083 
00084 okltest_nonmersenne_inf_rec(nonmersenne_inf_rec);
00085 
00086 okltest_nonmersenne_level(nonmersenne_level);
00087 
00088 okltest_nonmersenne_law(nonmersenne_law2);
00089 
00090 okltest_nonmersenne_inf_rec(nonmersenne_inf_law);
00091