OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 28.12.2009 (Swansea) */
00002 /* Copyright 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 
00022 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/tests/DLL_solvers.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00026 
00027 kill(f)$
00028 
00029 /* *****************************
00030    * The notion of a reduction *
00031    *****************************
00032 */
00033 
00034 okltest_weakest_reduction_cs(f) := block([F],
00035   assert(f(F) = F),
00036   true)$
00037 
00038 okltest_strongest_reduction_cs(f) := block(
00039  [S : dll_simplest_first_shortest_clause],
00040   assert(okltest_SATsolver(buildq([f,S], lambda([FF], if f(fcs2cs(FF),S)={} then true else false))) = true),
00041   true)$
00042 
00043 
00044 /* ***************************
00045    * Subsumption elimination *
00046    ***************************
00047 */
00048 
00049 okltest_subsumption_elimination_cs(f) := (
00050   assert(f({}) = {}),
00051   assert(f({{}}) = {{}}),
00052   assert(f({{},{1}}) = {{}}),
00053   assert(f({{1},{2,3},{-1},{1,3}}) = {{1},{2,3},{-1}}),
00054   assert(f({{1,2},{2,3},{-1},{1,3}}) = {{1,2},{2,3},{-1},{1,3}}),
00055   assert(f({{1,2},{1,3,2},{1,-4,2},{2,3},{2,3,4},{2,3,-5}}) = {{1,2},{2,3}}),
00056   true)$
00057