OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
```00001 /* Oliver Kullmann, 21.5.2010 (Swansea) */
00002 /* Copyright 2010 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
00022 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")\$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")\$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Basics.mac")\$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/Basics.mac")\$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")\$
00027 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")\$
00028
00029
00030 /*
00031   See "Notions" in Satisfiability/Lisp/Primality/plans/general.hpp for
00032   the definitions.
00033 */
00034
00035 prime_clause_p(C,F) := impliesp_cs(F,C,current_satsolver) and
00036  every_s(lambda([x], not impliesp_cs(F,disjoin(x,C),current_satsolver)), C)\$
00037
00038 dual_prime_clause_p(C,F) := sat_pacs_p(C,F) and
00039  every_s(lambda([x], not sat_pacs_p(disjoin(x,C),F)), C)\$
00040
00041 prime_cs_p(F) := every_s(lambda([C], prime_clause_p(C,F)), F)\$
00042
00043 maximal_prime_cs_p(F) := prime_cs_p(F) and
00044  min_elements(union(F,resolvents_cs(F))) = F\$
00045
```