OKlibrary  0.2.1.6
GreenTaoProblems.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 30.12.2009 (Swansea) */
00002 /* Copyright 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/GreenTaoProblems.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/tests/GreenTaoProblems.mac")$
00023 
00024 /* *****************************************
00025    * Arithmetic progressions in the primes *
00026    *****************************************
00027 */
00028 
00029 okltest_greentao2_fcl(greentao2_fcl);
00030 okltest_greentao2_fcs(greentao2_fcs);
00031 
00032 okltest_greentao2nd_fcl(greentao2nd_fcl);
00033 okltest_greentao2nd_fcs(greentao2nd_fcs);
00034 
00035 okltest_greentao_nbfclud(greentao_nbfclud);
00036 okltest_greentao_nbfcsud(greentao_nbfcsud);
00037 
00038 okltest_greentaod_nbfclud(greentaod_nbfclud);
00039 okltest_greentaod_nbfcsud(greentaod_nbfcsud);
00040 
00041 /* ****************************************
00042    * Translation into boolean clause-sets *
00043    ****************************************
00044 */
00045 
00046 okltest_greentao_aloamo_fcl(greentao_aloamo_fcl);
00047 okltest_greentao_aloamo_fcs(greentao_aloamo_fcs);
00048 
00049 okltest_greentao_standnest_fcl(greentao_standnest_fcl);
00050 okltest_greentao_standnest_fcs(greentao_standnest_fcs);
00051 
00052 okltest_greentao_standnest_strong_fcl(okltest_greentao_standnest_fcl);
00053 okltest_greentao_standnest_strong_fcs(okltest_greentao_standnest_fcs);
00054 
00055 okltest_greentao_logarithmic_fcl(greentao_logarithmic_fcl);
00056 okltest_greentao_logarithmic_fcs(greentao_logarithmic_fcs);
00057 
00058 okltest_greentao_reduced_fcl(greentao_reduced_fcl);
00059 okltest_greentao_reduced_fcs(greentao_reduced_fcs);
00060 
00061 okltest_greentao_reduced_strong_fcl(okltest_greentao_reduced_fcl);
00062 okltest_greentao_reduced_strong_fcs(okltest_greentao_reduced_fcs);
00063 
00064 /* *********************
00065    * Symmetry breaking *
00066    *********************
00067 */
00068 
00069 okltest_greentao2_sb_fcs(greentao2_sb_fcs);
00070 
00071 okltest_greentao_sb_aloamo_fcs(greentao_sb_aloamo_fcs);
00072 
00073 okltest_greentaod_sb_nbfcsud(greentaod_sb_nbfcsud);
00074 
00075 
00076 /* ************************
00077    * Statistics functions *
00078    ************************
00079 */
00080 
00081 
00082 /* *******************
00083    * Standardisation *
00084    *******************
00085 */
00086 
00087 okltest_greentao_aloamo_stdfcl(greentao_aloamo_stdfcl);
00088 
00089 okltest_greentao_standnest_stdfcl(greentao_standnest_stdfcl);
00090 
00091 okltest_greentao_standnest_strong_stdfcl(greentao_standnest_strong_stdfcl);
00092 
00093 okltest_greentao_logarithmic_stdfcl(greentao_logarithmic_stdfcl);
00094 
00095 okltest_greentao_reduced_stdfcl(greentao_reduced_stdfcl);
00096 
00097 okltest_greentao_reduced_strong_stdfcl(greentao_reduced_strong_stdfcl);
00098 
00099 /* ********************
00100    * Output functions *
00101    ********************
00102 */
00103 
00104