OKlibrary  0.2.1.6
Transformations.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 16.9.2008 (Swansea) */
00002 /* Copyright 2008, 2009 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/Transformations.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/tests/Transformations.mac")$
00023 
00024 /* **************************************************
00025    * Translated minimally unsatisfiable clause-sets *
00026    **************************************************
00027 */
00028 
00029 okltest_n_var_usat_musat(n_var_usat_musat);
00030 okltest_n_cl_usat_musat(n_cl_usat_musat);
00031 okltest_deficiency_usat_musat(deficiency_usat_musat);
00032 okltest_ncl_list_usat_musat(ncl_list_usat_musat);
00033 
00034 okltest_n_var_sat_musat(n_var_sat_musat);
00035 okltest_n_cl_sat_musat(n_cl_sat_musat);
00036 okltest_deficiency_sat_musat(deficiency_sat_musat);
00037 okltest_ncl_list_sat_musat(ncl_list_sat_musat);
00038 
00039 /* ********************************************************
00040    * Max-Clique translated to "SHORT RES" and "SMALL MUS" *
00041    ********************************************************
00042 */
00043 
00044 okltest_new_k(new_k);
00045 
00046 okltest_maxclique_start(maxclique_start);
00047 okltest_maxclique_edges(maxclique_edges);
00048 okltest_maxclique_cleanup(maxclique_cleanup);
00049 
00050 okltest_maxclique_mures_fcs(maxclique_mures_fcs);
00051 
00052 okltest_nvar_maxclique_mures_fcs(nvar_maxclique_mures_fcs);
00053 okltest_ncl_list_maxclique_mures_fcs(ncl_list_maxclique_mures_fcs);
00054