OKlibrary  0.2.1.6
PrimeImplicatesImplicants.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 27.3.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 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/Primality/PrimeImplicatesImplicants.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Primality/tests/PrimeImplicatesImplicants.mac")$
00023 
00024 /* *****************
00025    * Prime clauses *
00026    *****************
00027 */
00028 
00029 okltest_prime_clauses_cs(prime_clauses_cs);
00030 
00031 /* *************************************
00032    * Prime-clauses of full clause-sets *
00033    *************************************
00034 */
00035 
00036 okltest_min_2resolution_closure_cs(min_2resolution_closure_cs);
00037 
00038 /* ******************************************************
00039    * Minimum equivalent clause-sets of full clause-sets *
00040    ******************************************************
00041 */
00042 
00043 okltest_subsumption_hg_full_cs(subsumption_hg_full_cs);
00044 okltest_rsubsumption_hg_full_cs(rsubsumption_hg_full_cs);
00045 
00046 okltest_minequiv_cs(lambda([F],setify(all_minequiv_bvs_cs(F))));
00047 okltest_minequiv_cs(lambda([F],setify(all_minequiv_bvsr_cs(F))));
00048 
00049 /* *************************************
00050    * Dualisation for full clause-sets  *
00051    *************************************
00052 */
00053 
00054 okltest_dual_min_2resolution_closure_cs(dual_min_2resolution_closure_cs);
00055 okltest_dual_minequiv_cs(dual_all_minequiv_bvs_cs);
00056 
00057 /* **************************************************
00058    * Finding contained prime-clauses by SAT solvers *
00059    **************************************************
00060 */
00061 
00062 okltest_contained_prime_implicate(contained_prime_implicate);
00063 
00064 okltest_replace_by_prime_implicates_hitting(replace_by_prime_implicates_hitting);
00065 
00066