OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 27.3.2008 (Swansea) */
00002 /* Copyright 2008, 2010, 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/Resolution/Basics.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/tests/Basics.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Primality/tests/PrimeImplicatesImplicants.mac")$
00024 
00025 
00026 /* ***************************
00027    * Single resolution steps *
00028    ***************************
00029 */
00030 
00031 okltest_resolvable(resolvable);
00032 
00033 okltest_resolution_literal(resolution_literal);
00034 
00035 okltest_resolvable_p(resolvable_p);
00036 
00037 okltest_two_subsumption_resolvent_p(two_subsumption_resolvent_p);
00038 
00039 /* *************************
00040    * Adding all resolvents *
00041    *************************
00042 */
00043 
00044 okltest_resolvable_cs(resolvable_cs);
00045 okltest_two_subsumption_resolvable_cs(two_subsumption_resolvable_cs);
00046 
00047 okltest_two_subsumption_resolvents_rem_cs(two_subsumption_resolvents_rem_cs);
00048 
00049 /* ***********************
00050    * Iterated resolution *
00051    ***********************
00052 */
00053 
00054 okltest_prime_clauses_cs(lambda([F], min_resolution_closure_cs(F)[1]));
00055 
00056 /* *****************
00057    * DP resolution *
00058    *****************
00059 */
00060 
00061 okltest_dp_operator(dp_operator);
00062 okltest_dp_operator_fcs(dp_operator_fcs);
00063 
00064 okltest_distribution_min_dp(distribution_min_dp);
00065 
00066 /* ****************************
00067    * Width-bounded resolution *
00068    ****************************
00069 */
00070 
00071 okltest_kresolvable(kresolvable);
00072 okltest_kresolvable_s(kresolvable_s);
00073 okltest_kresolvable_cs(kresolvable_cs);
00074 
00075 okltest_kresolvents_cs(kresolvents_cs);
00076 okltest_add_kresolvents_cs(add_kresolvents_cs);
00077 
00078 okltest_kresolution_closure_cs(kresolution_closure_cs);
00079 okltest_min_add_kresolvents_cs(min_add_kresolvents_cs);
00080 okltest_min_kresolution_closure_cs(min_kresolution_closure_cs);
00081 
00082 okltest_bresolvable(bresolvable);
00083 okltest_bresolvable_s(bresolvable_s);
00084 okltest_bresolvable_cs(bresolvable_cs);
00085 
00086 okltest_bresolvents_cs(bresolvents_cs);
00087 okltest_add_bresolvents_cs(add_bresolvents_cs);
00088 
00089 okltest_bresolution_closure_cs(bresolution_closure_cs);
00090 okltest_min_add_bresolvents_cs(min_add_bresolvents_cs);
00091 okltest_min_bresolution_closure_cs(min_bresolution_closure_cs);
00092 
00093 /* *******************
00094    * Blocked clauses *
00095    *******************
00096 */
00097 
00098 okltest_blocking_literal_p(blocking_literal_p);
00099 okltest_blocked_cs_p(blocked_cs_p);
00100 okltest_elim_blocked_cs(elim_blocked_cs);
00101 okltest_elim_blockedk_cs(elim_blockedk_cs);
00102 okltest_blocked_extension_cs_p(blocked_extension_cs_p);
00103