OKlibrary  0.2.1.6
Substitutions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 27.7.2007 (Swansea) */
00002 /* Copyright 2008, 2009, 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 
00022 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00025 
00026 kill(f)$
00027 
00028 /* ********************************************
00029    * Substitutions for variables and literals *
00030    ********************************************
00031 */
00032 
00033 okltest_substitute_l(f) := block([h],
00034   h : sm2hm({[1,3],[2,-4],[3,-3]}),
00035   assert(f(1,h) = 3), assert(f(-1,h) = -3),
00036   assert(f(2,h) = -4), assert(f(-2,h) = 4),
00037   assert(f(3,h) = -3), assert(f(-3,h) = 3),
00038   assert(f(4,h) = false), assert(f(-4,h) = -false),
00039   true)$
00040 
00041 
00042 /* *****************************
00043    * Substitutions for clauses *
00044    *****************************
00045 */
00046 
00047 okltest_substitute_c(f) := block([h],
00048   h : sm2hm({[1,3],[2,-4],[3,-3]}),
00049   assert(f({},h) = {}),
00050   assert(f({1},h) = {3}), assert(f({-1},h) = {-3}),
00051   assert(f({2},h) = {-4}), assert(f({-2},h) = {4}),
00052   assert(f({3},h) = {-3}), assert(f({-3},h) = {3}),
00053   assert(f({1,2,3},h) = {3,-4,-3}),
00054   assert(f({1,2,-3},h) = {3,-4}),
00055   assert(f({1,2,-3,4},h) = {3,-4,4}),
00056   assert(f({1,2,-3,-4},h) = {3,-4}),
00057   assert(f({1,2,-3,5},h) = {3,-4,5}),
00058   true)$
00059 
00060 
00061 /* *********************************
00062    * Substitutions for clause-sets *
00063    *********************************
00064 */
00065 
00066 okltest_substitute_cs(f) := block([h],
00067   h : sm2hm({[1,3],[2,-4],[3,-3]}),
00068   assert(f({},h) = {}),
00069   assert(f({{}},h) = {{}}),
00070   assert(f({{},{4,5}},h) = {{},{4,5}}),
00071   assert(f({{1,2},{1,3},{-2,3}},h) = {{3,-4},{3,-3},{4,-3}}),
00072   true)$
00073 
00074 okltest_rename_fcs(f) := block(
00075   assert(f([{},{}],[]) = [{},{}]),
00076   assert(f([{},{{}}],[]) = [{},{{}}]),
00077   assert(f([{1},{}],[2]) = [{2},{}]),
00078   assert(f([{1},{{}}],[2]) = [{2},{{}}]),
00079   assert(f([{1},{{1}}],[-2]) = [{2},{{-2}}]),
00080   assert(f([{1},{{-1}}],[-1]) = [{1},{{1}}]),
00081   assert(f([{1,2},{{1,2},{-1,2}}],[-2,1]) = [{1,2},{{-2,1},{1,2}}]),
00082   assert(okltest_rename_cs(buildq([f], lambda([F,L], fcs2cs(f(cs2fcs(F),L))))) = true),
00083   true)$
00084 
00085 okltest_rename_cs(f) := (
00086   assert(f({},[]) = {}),
00087   assert(f({{}},[]) = {{}}),
00088   assert(f({{1}},[-3]) = {{-3}}),
00089   assert(f({{1,2},{-2,3},{}},[2,-3,1]) = {{2,-3},{3,1},{}}),
00090   /* XXX */
00091   true)$
00092 
00093 okltest_all_var_renamings_fcs(f) := (
00094   assert(f([{},{}]) = { [{},{}] }),
00095   assert(f([{},{{}}]) = { [{},{{}}] }),
00096   assert(f([{1,2},{}]) = { [{1,2},{}] }),
00097   assert(f([{1,2},{{}}]) = { [{1,2},{{}}] }),
00098   assert(f([{1},{{1}}]) = { [{1},{{1}}] }),
00099   assert(f([{1,2},{{1}}]) = { [{1,2},{{1}}],[{1,2},{{2}}] }),
00100   /* XXX */
00101   true)$
00102 
00103 okltest_all_sign_flippings_fcs(f) := (
00104   assert(f([{},{}]) = { [{},{}] }),
00105   assert(f([{},{{}}]) = { [{},{{}}] }),
00106   assert(f([{1,2},{}]) = { [{1,2},{}] }),
00107   assert(f([{1,2},{{}}]) = { [{1,2},{{}}] }),
00108   assert(f([{1},{{1}}]) = { [{1},{{1}}],[{1},{{-1}}] }),
00109   assert(f([{1,2},{{1}}]) = { [{1,2},{{1}}],[{1,2},{{-1}}] }),
00110   /* XXX */
00111   true)$
00112 
00113 okltest_all_renamings_fcs(f) := (
00114   assert(f([{},{}]) = { [{},{}] }),
00115   assert(f([{},{{}}]) = { [{},{{}}] }),
00116   assert(f([{1,2},{}]) = { [{1,2},{}] }),
00117   assert(f([{1,2},{{}}]) = { [{1,2},{{}}] }),
00118   assert(f([{1},{{1}}]) = { [{1},{{1}}], [{1},{{-1}}] }),
00119   assert(f([{1,2},{{1}}]) = { [{1,2},{{1}}],[{1,2},{{2}}],[{1,2},{{-1}}],[{1,2},{{-2}}] }),
00120   /* XXX */
00121   true)$
00122 
00123 okltest_standardise_fcs(f) := block(
00124   assert(f([{},{}]) = [[{},{}],[]]),
00125   assert(f([{},{{}}]) = [[{},{{}}],[]]),
00126   assert(f([{1},{{}}]) = [[{1},{{}}],[1]]),
00127   assert(f([{2,3},{{}}]) = [[{1,2},{{}}],[2,3]]),
00128   assert(f([{4,5,6},{{},{-4,5,6},{5},{4,-5},{-5,-6}}]) = [[{1,2,3},{{},{-1,2,3},{2},{1,-2},{-2,-3}}],[4,5,6]]),
00129   true)$
00130 
00131 okltest_make_vardisjoint_fcs(f) := (
00132   assert(f([]) = [[],0]),
00133   assert(f(map(cs_to_fcs,[{},{{}},{},{{}}])) = [map(cs_to_fcs,[{},{{}},{},{{}}]), 0]),
00134   assert(f(map(cs_to_fcs,[{{1}},{{}},{{1}},{{}}])) = [map(cs_to_fcs,[{{1}},{{}},{{2}},{{}}]), 2]),
00135   assert(f(map(cs_to_fcs,[{{4}},{{2}},{{2}},{{1}}])) = [map(cs_to_fcs,[{{1}},{{2}},{{3}},{{4}}]), 4]),
00136   true)$
00137 
00138 okltest_make_vardisjoint_vl_fcs(f) := (
00139   assert(f([]) = [[],0,[]]),
00140   assert(okltest_make_vardisjoint_fcs(buildq([f], lambda([L],rest(f(L),-1)))) = true),
00141   assert(f([[{2},{}],[{1},{}]]) = [[[{1},{}],[{2},{}]],2,[[2],[1]]]),
00142   assert(f([[{2},{{2},{-2}}],[{1},{{1}}]]) = [[[{1},{{1},{-1}}],[{2},{{2}}]],2,[[2],[1]]]),
00143   true)$
00144 
00145