OKlibrary  0.2.1.6
VanderWaerdenProblems.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 20.9.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010 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/Generators/RamseyTheory/VanderWaerdenProblems.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/tests/VanderWaerdenProblems.mac")$
00023 
00024 /* **************************************************
00025    * Arithmetic progressions in the natural numbers *
00026    **************************************************
00027 */
00028 
00029 okltest_vanderwaerden2_fcl(vanderwaerden2_fcl);
00030 okltest_vanderwaerden2_fcs(vanderwaerden2_fcs);
00031 okltest_vanderwaerden2nd_fcl(vanderwaerden2nd_fcl);
00032 okltest_vanderwaerden2nd_fcs(vanderwaerden2nd_fcs);
00033 
00034 okltest_pd_vanderwaerden2nd_fcl(pd_vanderwaerden2nd_fcl);
00035 okltest_pd_vanderwaerden2nd_fcs(pd_vanderwaerden2nd_fcs);
00036 
00037 okltest_vanderwaerden_nbfclud(vanderwaerden_nbfclud);
00038 okltest_vanderwaerden_nbfcsud(vanderwaerden_nbfcsud);
00039 
00040 /* ****************************************
00041    * Translation into boolean clause-sets *
00042    ****************************************
00043 */
00044 
00045 okltest_vanderwaerden_aloamo_fcl(vanderwaerden_aloamo_fcl);
00046 okltest_vanderwaerden_aloamo_fcs(vanderwaerden_aloamo_fcs);
00047 
00048 okltest_vanderwaerden_aloamo_stdfcl(vanderwaerden_aloamo_stdfcl);
00049 okltest_vanderwaerden_aloamo_stdfcs(vanderwaerden_aloamo_stdfcs);
00050 
00051 okltest_standardise_vanderwaerden_aloamo(standardise_vanderwaerden_aloamo);
00052 okltest_invstandardise_vanderwaerden_aloamo(invstandardise_vanderwaerden_aloamo);
00053 
00054 /* ************************
00055    * Statistics functions *
00056    ************************
00057 */
00058 
00059 okltest_nvar_vanderwaerden2(nvar_vanderwaerden2);
00060 okltest_nvar_vanderwaerden2nd(nvar_vanderwaerden2nd);
00061 okltest_nvar_vanderwaerden(nvar_vanderwaerden);
00062 okltest_nvar_vanderwaerden_aloamo(nvar_vanderwaerden_aloamo);
00063 
00064 okltest_ncl_vanderwaerden2_cs(ncl_vanderwaerden2_cs);
00065 okltest_ncl_vanderwaerden2nd_cs(ncl_vanderwaerden2nd_cs);
00066 okltest_ncl_vanderwaerden_cl(ncl_vanderwaerden_cl);
00067 okltest_ncl_vanderwaerden_cs(ncl_vanderwaerden_cs);
00068 okltest_ncl_vanderwaerden_aloamo_cl(ncl_vanderwaerden_aloamo_cl);
00069 okltest_ncl_vanderwaerden_aloamo_cs(ncl_vanderwaerden_aloamo_cs);
00070 
00071 /* ********************
00072    * Output functions *
00073    ********************
00074 */
00075 
00076