OKlibrary  0.2.1.6
Pigeonhole.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 26.8.2011 (Swansea) */
00002 /* Copyright 2011, 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 
00021 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/tests/Pigeonhole.mac")$
00023 
00024 
00025 /* ***********************
00026    * Pigeonhole formulas *
00027    ***********************
00028 */
00029 
00030 okltest_var_php_l(var_php_l);
00031 
00032 okltest_pigeons_different_holes_cl(pigeons_different_holes_cl);
00033 okltest_pigeons_in_holes_cl(pigeons_in_holes_cl);
00034 
00035 /* Measures */
00036 
00037 okltest_nvar_php(nvar_php);
00038 okltest_ncl_list_weak_php(ncl_list_weak_php);
00039 okltest_ncl_weak_php(ncl_weak_php);
00040 okltest_deficiency_weak_php(deficiency_weak_php);
00041 
00042 
00043 /* *********************************
00044    * Extended pigeon-hole formulas *
00045    *********************************
00046 */
00047 
00048 okltest_php_induction_step_cl(php_induction_step_cl);
00049 okltest_php_induction_cl(php_induction_cl);
00050 okltest_weak_php_unsat_ext_fcs(weak_php_unsat_ext_fcs);
00051 okltest_weak_php_unsat_ext_uni_fcs(weak_php_unsat_ext_uni_fcs);
00052 okltest_standardise_weak_php_unsat_ext_uni(standardise_weak_php_unsat_ext_uni);
00053 okltest_invstandardise_weak_php_unsat_ext_uni(invstandardise_weak_php_unsat_ext_uni);
00054 okltest_weak_php_unsat_ext_stdfcs(weak_php_unsat_ext_stdfcs);
00055 okltest_var_php2ephp_sm(var_php2ephp_sm);
00056 okltest_var_ephp2php_sm(var_ephp2php_sm);
00057 okltest_nvar_weak_php_unsat_ext(nvar_weak_php_unsat_ext);
00058 okltest_ncl_weak_php_unsat_ext(ncl_weak_php_unsat_ext);
00059 
00060