OKlibrary  0.2.1.6
Translations.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 14.5.2008 (Guangzhou) */
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/ClauseSets/BasicOperations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Autarkies/Translations.mac")$
00027 
00028 kill(f)$
00029 
00030 
00031 okltest_aut_sat_ls(f) := (
00032   assert(f([{},{}]) = [{},{}]),
00033   assert(f([{},{{}}]) = [{lsavc_var({})}, {{-lsavc_var({})}}]),
00034   true)$
00035 
00036 /* Test function to check a leanness-decision-function (returning
00037    true iff lean (false otherwise)). */
00038 okltest_lean(f) := (
00039   assert(f([{},{}]) = true),
00040   assert(f([{},{{}}]) = true),
00041   assert(f([{1},{}]) = false),
00042   assert(f([{1},{{}}]) = false),
00043   assert(f([{1,2},{{2},{-1},{1}}]) = false),
00044   if oklib_test_level = 0 then return(true),
00045   for n : 0 thru 3 do
00046     assert(f(full_fcs(n)) = true),
00047   true)$
00048 
00049 
00050 okltest_lean_usat_ls(f) := block([solver : dll_simplest_trivial2],
00051   assert(nvar_f(f(ls_exmp_talk_guangzhou)) = 5 + 5 + 6 + 2 * 5),
00052   okltest_lean(buildq([f,solver],lambda([FF], not solver(f(FF))))),
00053   true)$
00054 
00055 ls_exmp_talk_guangzhou : [
00056   {1,2,3,4,5}, {{1},{-1,2},{-1,-2}, {-2,3},{4,5},{-4,-5}}]$
00057 
00058 autarky_test_cases : [ /* autarkies and their formal clause-sets */
00059   [{}, [{},{}]],
00060   [{}, [{},{{}}]],
00061   [{}, [{1},{{-1},{1}}]],
00062   [{1}, [{1,2},{{1},{-2},{2}}]],
00063   [{1,2}, [{1,2}, {{1,-2},{-1,2},{1,2}}]],
00064   [{3}, ls_exmp_talk_guangzhou],
00065   [{4,-5}, ls_exmp_talk_guangzhou],
00066   [{-4,5}, ls_exmp_talk_guangzhou],
00067   [{3,4,-5}, ls_exmp_talk_guangzhou],
00068   [{3,-4,5}, ls_exmp_talk_guangzhou]
00069  ]$
00070 
00071 okltest_trans_aut_sat_ls(f) := (
00072   assert(f({},[{},{}]) = {}),
00073   assert(f({},[{},{{}}]) = {-lsavc_var({})}),
00074   assert(f({},[{1},{{-1},{1}}]) = 
00075     {-lsavc_var({1}), -lsavc_var({-1}),
00076      -lsavl_var(1,-1), -lsavl_var(1,1),
00077      -lsavv_var(1)}),
00078   for P in autarky_test_cases do
00079     assert(satisfyingpafp(f(P[1],P[2]), aut_sat_ls(P[2])) = true),
00080   true)$
00081 
00082 okltest_itransc_aut_sat_ls(f) := block(
00083   for P in autarky_test_cases do block(
00084    [phi : P[1],
00085     FF : P[2],
00086     trans_phi : trans_aut_sat_ls(P[1],P[2]), 
00087     A : sat_paf(P[1],P[2])],
00088     assert(f(trans_phi,FF) = A)),
00089   true)$
00090 
00091 okltest_itrans_aut_sat_ls(f) := block(
00092   assert(f({},[{},{}]) = {}),
00093   assert(f({-lsavc_var({})},[{},{{}}]) = {}),
00094   assert(f({-lsavc_var({1}), -lsavc_var({-1}),
00095      -lsavl_var(1,-1), -lsavl_var(1,1),
00096      -lsavv_var(1)}, [{1},{{-1},{1}}]) = {}),
00097   true)$
00098