OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 28.3.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011, 2012 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/Basics.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/tests/Basics.mac")$
00023 
00024 
00025 /* *************************
00026    * Deciding irredundancy *
00027    *************************
00028 */
00029 
00030 okltest_impliesp_fcs(impliesp_fcs);
00031 okltest_impliesp_cs(impliesp_cs);
00032 
00033 okltest_min_unsat_bydef(min_unsat_bydef);
00034 okltest_irredundant_bydef(irredundant_bydef);
00035 
00036 /* *****************************
00037    * Classification of clauses *
00038    *****************************
00039 */
00040 
00041 okltest_all_irrcl_bydef(all_irrcl_bydef);
00042 
00043 /* **************************************
00044    * Saturated minimal unsatisfiability *
00045    **************************************
00046 */
00047 
00048 okltest_saturated_min_unsat_bydef(saturated_min_unsat_bydef);
00049 okltest_non_saturating_pas_bydef(non_saturating_pas_bydef);
00050 
00051 /* *************************************
00052    * Marginal minimal unsatisfiability *
00053    *************************************
00054 */
00055 
00056 okltest_marginal_min_unsat_bydef_fcs(marginal_min_unsat_bydef_fcs);
00057