OKlibrary  0.2.1.6
NonBooleanTranslations.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 27.5.2009 (Swansea) */
00002 /* Copyright 2009, 2010, 2011, 2012 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/Generators/Generators.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/NonBooleanTranslations.mac")$
00027 
00028 
00029 /* ******************************
00030    * The "direct" translation *
00031    ******************************
00032 */
00033 
00034 okltest_nbfclfd2fcl_core(f) := (
00035   /* XXX */
00036   true)$
00037 
00038 okltest_nbfclud2fcl_core(f) := block([FF],
00039   assert(f([[],[],[]]) = [[],[]]),
00040   assert(f([[1],[],[]]) = [[],[]]),
00041   assert(f([[1],[],[2]]) = [[nbv(1,2)],[]]),
00042   assert(f([[3,1],[],[4,2]]) = [[nbv(3,4),nbv(3,2),nbv(1,4),nbv(1,2)],[]]),
00043   assert(f([[],[{}],[]]) = [[],[{}]]),
00044   assert(f([[],[{},{}],[]]) = [[],[{},{}]]),
00045   assert(f([[1],[{},{[1,1]},{[1,1]}],[1]]) = [[nbv(1,1)], [{},{-nbv(1,1)},{-nbv(1,1)}]]),
00046   /* XXX */
00047   true)$
00048 
00049 okltest_nbfcsfd2fcs_core(f) := block([FF,D],
00050   assert(f([{},{},D]) = [{},{}]),
00051   /* XXX */
00052   true)$
00053 
00054 okltest_nbfclud2fcl_alo(f) := block(
00055   assert(f([[],[],[]]) = [[],[]]),
00056   /* XXX */
00057   true)$
00058 
00059 okltest_nbfcsfd2fcs_alo(f) := block([FF,D],
00060   assert(f([{},{},D]) = [{},{}]),
00061   /* XXX */
00062   true)$
00063 
00064 okltest_nbfclud2fcl_aloamo(f) := block(
00065   assert(f([[],[],[]]) = [[],[]]),
00066   /* XXX */
00067   true)$
00068 
00069 okltest_nbfcsfd2fcs_aloamo(f) := block([FF,D],
00070   assert(f([{},{},D]) = [{},{}]),
00071   /* XXX */
00072   true)$
00073 
00074 okltest_snbfclfd2fcl_core(f) := (
00075   /* XXX */
00076   true)$
00077 
00078 okltest_snbfclud2fcl_core(f) := block([FF],
00079   assert(f([[],[],[]]) = [[],[]]),
00080   assert(f([[1],[],[]]) = [[],[]]),
00081   assert(f([[1],[],[2]]) = [[nbv(1,2)],[]]),
00082   assert(f([[3,1],[],[4,2]]) = [[nbv(3,4),nbv(3,2),nbv(1,4),nbv(1,2)],[]]),
00083   assert(f([[],[{}],[]]) = [[],[{}]]),
00084   assert(f([[],[{},{}],[]]) = [[],[{},{}]]),
00085   assert(f([[1],[{},{[1,1,1]},{[1,1,-1]}],[1]]) = [[nbv(1,1)], [{},{nbv(1,1)},{-nbv(1,1)}]]),
00086   /* XXX */
00087   true)$
00088 
00089 okltest_snbfcsfd2fcs_core(f) := (
00090   assert(f([{},{},{}]) = [{},{}]),
00091   assert(f([{1},{},lambda([x],{})]) = [{},{}]),
00092   /* XXX */
00093   true)$
00094 
00095 okltest_snbfclfd2fcl_aloamo(f) := block([D],
00096   assert(f([[],[],D]) = [[],[]]),
00097   /* XXX */
00098   true)$
00099 
00100 okltest_snbfclud2fcl_aloamo(f) := (
00101   assert(f([[],[],[]]) = [[],[]]),
00102   assert(f([[1],[],[]]) = [[],[{}]]),
00103   assert(f([[1],[],[2]]) = [[nbv(1,2)],[{nbv(1,2)}]]),
00104   assert(f([[3,1],[],[4,2]]) = [[nbv(3,4),nbv(3,2),nbv(1,4),nbv(1,2)],[{nbv(3,4),nbv(3,2)},{nbv(1,4),nbv(1,2)},{-nbv(3,4),-nbv(3,2)},{-nbv(1,4),-nbv(1,2)}]]),
00105   assert(f([[],[{}],[]]) = [[],[{}]]),
00106   assert(f([[],[{},{}],[]]) = [[],[{},{}]]),
00107   assert(f([[1],[{},{[1,1,1]},{[1,1,-1]}],[1]]) = [[nbv(1,1)], [{},{nbv(1,1)},{-nbv(1,1)},{nbv(1,1)}]]),
00108   /* XXX */
00109   true)$
00110 
00111 okltest_snbfcsfd2fcs_aloamo(f) := block([D],
00112   assert(f([{},{},D]) = [{},{}]),
00113   /* XXX */
00114   true)$
00115 
00116 okltest_extract_partition(f) := (
00117   assert(f({}) = []),
00118   assert(f({nbv(1,1)}) = [{1}]),
00119   assert(f({nbv(1,2)}) = [{},{1}]),
00120   assert(f({nbv(2,1)}) = [{2}]),
00121   assert(f({nbv(2,2)}) = [{},{2}]),
00122   assert(f({nbv(-1,3)}) = [{},{},{-1}]),
00123   assert(f({nbv(1,1),nbv(2,1)}) = [{1,2}]),
00124   assert(f({nbv(1,1),nbv(2,2)}) = [{1},{2}]),
00125   true)$
00126 
00127 
00128 /* **************************************
00129    * The generalised nested translation *
00130    **************************************
00131 */
00132 
00133 okltest_gennest_clause_trans(f) := (
00134 
00135   true)$
00136 
00137 okltest_gennest_nbfcl2fcl(f) := (
00138 
00139   true)$
00140 
00141 okltest_standtrans_T(f) := (
00142 
00143   true)$
00144 
00145 okltest_standtrans_fd_weak_TR(f) := (
00146 
00147   true)$
00148 
00149 okltest_standtrans_ud_weak_TR(f) := (
00150 
00151   true)$
00152 
00153 okltest_standtrans_fd_TV(f) := (
00154 
00155   true)$
00156 
00157 okltest_standtrans_ud_TV(f) := (
00158 
00159   true)$
00160 
00161 okltest_nbfclfd2fcl_alo_2(f) := (
00162 
00163   true)$
00164 
00165 okltest_nbfclud2fcl_alo_2(f) := (
00166 
00167   true)$
00168 
00169 okltest_standnest_T(f) := (
00170 
00171   true)$
00172 
00173 okltest_standnest_TR(f) := (
00174 
00175   true)$
00176 
00177 okltest_standnest_strong_TR(f) := (
00178 
00179   true)$
00180 
00181 okltest_standnest_TV(f) := (
00182 
00183   true)$
00184 
00185 okltest_nbfclud2fcl_standnest(f) := (
00186 
00187   true)$
00188 
00189 okltest_nbfclud2fcl_standnest_strong(f) := (
00190 
00191   true)$
00192 
00193 okltest_logarithmic_T(f) := block([t,v,e],
00194   t : f([3]),
00195   assert(t(v,3) = {}),
00196   t : f([4,2]),
00197   assert(t(v,4) = {-nbv(v,1)}),
00198   assert(t(v,2) = {nbv(v,1)}),
00199   t : f([1,3,2]),
00200   assert(t(v,1) = {-nbv(v,1),-nbv(v,2)}),
00201   assert(t(v,3) = {-nbv(v,1),nbv(v,2)}),
00202   assert(t(v,2) = {nbv(v,1),-nbv(v,2)}),
00203   t : f([-1,3,5,e]),
00204   assert(t(v,-1) = {-nbv(v,1),-nbv(v,2)}),
00205   assert(t(v,3) = {-nbv(v,1),nbv(v,2)}),
00206   assert(t(v,5) = {nbv(v,1),-nbv(v,2)}),
00207   assert(t(v,e) = {nbv(v,1),nbv(v,2)}),
00208   t : f([1,2,-3,4,5]),
00209   assert(t(v,1) = {-nbv(v,1),-nbv(v,2),-nbv(v,3)}),
00210   assert(t(v,2) = {-nbv(v,1),-nbv(v,2),nbv(v,3)}),
00211   assert(t(v,-3) = {-nbv(v,1),nbv(v,2),-nbv(v,3)}),
00212   assert(t(v,4) = {-nbv(v,1),nbv(v,2),nbv(v,3)}),
00213   assert(t(v,5) = {nbv(v,1),-nbv(v,2),-nbv(v,3)}),
00214   true)$
00215 
00216 okltest_logarithmic_TR(f) := block([t,v,e],
00217   t : f([3]),
00218   assert(t(v) = []),
00219   t : f([4,2]),
00220   assert(t(v) = []),
00221   t : f([1,3,2]),
00222   assert(t(v) = [{nbv(v,1),nbv(v,2)}]),
00223   t : f([-1,3,5,e]),
00224   assert(t(v) = []),
00225   t : f([1,2,-3,4,5]),
00226   assert(t(v) = [{nbv(v,1),-nbv(v,2),nbv(v,3)},{nbv(v,1),nbv(v,2),-nbv(v,3)},{nbv(v,1),nbv(v,2),nbv(v,3)}]),
00227   true)$
00228 
00229 okltest_logarithmic_TV(f) := block([t,v,e],
00230   t : f([3]),
00231   assert(t(v) = []),
00232   t : f([4,2]),
00233   assert(t(v) = [nbv(v,1)]),
00234   t : f([1,3,2]),
00235   assert(t(v) = [nbv(v,1),nbv(v,2)]),
00236   t : f([-1,3,5,e]),
00237   assert(t(v) = [nbv(v,1),nbv(v,2)]),
00238   t : f([1,2,-3,4,5]),
00239   assert(t(v) = [nbv(v,1),nbv(v,2),nbv(v,3)]),
00240   true)$
00241 
00242 okltest_nbfclud2fcl_logarithmic(f) := (
00243 
00244   true)$
00245 
00246 okltest_reduced_T(f) := (
00247 
00248   true)$
00249 
00250 okltest_reduced_TR(f) := (
00251 
00252   true)$
00253 
00254 okltest_reduced_strong_TR(f) := (
00255 
00256   true)$
00257 
00258 okltest_reduced_TV(f) := (
00259 
00260   true)$
00261 
00262 okltest_nbfclud2fcl_reduced(f) := (
00263 
00264   true)$
00265 
00266 okltest_nbfclud2fcl_reduced_strong(f) := (
00267 
00268   true)$
00269 
00270 
00271 /* ************************************************
00272    * Tools for the generalised nested translation *
00273    ************************************************
00274 */
00275 
00276 okltest_gennest_nbfcl2fcl_p(f) := block([Du,D],
00277   /* XXX */
00278   Du : [1,2,3,4],
00279   D : lambda([x],Du),
00280   assert(f([1,2,3,4,5],D,dll_simplest_trivial2, standtrans_T,standtrans_fd_weak_TR(D),standtrans_fd_TV(D)) = true),
00281   assert(f([1,2,3,4,5],D,dll_simplest_trivial2, standnest_T(Du),standnest_TR(Du),standnest_TV(Du)) = true),
00282   assert(f([1,2,3,4,5],D,dll_simplest_trivial2, standnest_T(Du),standnest_strong_TR(Du),standnest_TV(Du)) = true),
00283   assert(f([1,2,3,4,5],D,dll_simplest_trivial2, logarithmic_T(Du),logarithmic_TR(Du),logarithmic_TV(Du)) = true),
00284   assert(f([1,2,3,4,5],D,dll_simplest_trivial2, reduced_T(Du),reduced_TR(Du),reduced_TV(Du)) = true),
00285   assert(f([1,2,3,4,5],D,dll_simplest_trivial2, reduced_T(Du),reduced_strong_TR(Du),reduced_TV(Du)) = true),
00286   true)$
00287 
00288 okltest_add_bincl_nec(f) := (
00289   for n : 0 thru 4 do block(
00290    [F : setify(create_list({i},i,1,n)),
00291     C : setify(create_list(-i,i,1,n))],
00292     assert(f(F,{C},dll_simplest_trivial2) = powerset(setn(n),2))
00293   ),
00294   for n : 0 thru 4 do block(
00295    [F : full_cs(n)],
00296     assert(f(F,{},dll_simplest_trivial2) = {})
00297   ),
00298   /* XXX */
00299   true)$
00300