OKlibrary  0.2.1.6
LeanKernel.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 29.7.2008 (Swansea) */
00002 /* Copyright 2008 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/DLL_solvers.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Autarkies/LeanKernel.mac")$
00025 
00026 kill(f)$
00027 
00028 /* **************************
00029    * Generic test functions *
00030    **************************
00031 */
00032 
00033 /* A generic test-funcion for f(FF), returning the lean kernel
00034    of FF: */
00035 okltest_lean_kernel_fcs(f) := (
00036   assert(f([{},{}]) = [{},{}]),
00037   assert(f([{},{{}}]) = [{},{{}}]),
00038   assert(f([{1},{}]) = [{},{}]),
00039   assert(f([{1,2},{{}}]) = [{},{{}}]),
00040   assert(f([{1},{{1},{-1}}]) = [{1},{{1},{-1}}]),
00041   assert(f([{1,2},{{1},{-1},{2},{1,2},{}}]) = [{1},{{1},{-1},{}}]),
00042   assert(f([{1,2,3},{{1,2},{-1,2},{-2},{1,3},{-2,3},{3}}]) = [{1,2},{{1,2},{-1,2},{-2}}]),
00043   true)$
00044 
00045 /* A generic test-function for f(FF), return a non-trivial autarky
00046    for FF iff possible (using variables from FF), and {} otherwise: 
00047 */
00048 
00049 okltest_find_autarky_cs(f) := block(
00050   assert(f({}) = {}),
00051   assert(f({{}}) = {}),
00052   assert(f({{1}}) = {1}),
00053   assert(f({{1},{-1}}) = {}),
00054   assert(f({{1},{-1},{2}}) = {2}),
00055   assert(f({{1,2},{-2,3},{2,3},{-3}}) = {1}),
00056   true)$
00057 
00058 okltest_find_autarky_fcs(f) := block(
00059   assert(f([{},{}]) = {}),
00060   assert(f([{},{{}}]) = {}),
00061   assert(elementp(f([{1},{}]), {{-1},{1}}) = true),
00062   assert(elementp(f([{1},{{}}]), {{-1},{1}}) = true),
00063   assert(f([{1},{{1}}]) = {1}),
00064   assert(f([{1},{{1},{-1}}]) = {}),
00065   assert(f([{1,2},{{1},{-1},{2}}]) = {2}),
00066   assert(okltest_lean_kernel_fcs(buildq([f],lambda([FF],
00067     lean_kernel_autfind_fcs(FF,f))))),
00068   assert(okltest_find_autarky_cs(buildq([f],lambda([F],
00069     f(cs2fcs(F)))))),
00070   true)$
00071 
00072 
00073 /* ***********************************
00074    * Computing the lean kernel bydef *
00075    ***********************************
00076 */
00077 
00078 okltest_lean_kernel_autfind_fcs(f) := block([af],
00079   local(af),
00080   af(FF) := {},
00081   test_cases : [
00082     [{},{}], [{},{{}}],[{1.2},{{1},{2}}]
00083   ],
00084   for FF in test_cases do
00085     assert(f(FF,af) = FF),
00086   true)$
00087