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 
00021 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/NonBooleanTranslations.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/tests/NonBooleanTranslations.mac")$
00023 
00024 /* ******************************
00025    * The "direct" translation *
00026    ******************************
00027 */
00028 
00029 okltest_nbfclfd2fcl_core(nbfclfd2fcl_core);
00030 okltest_nbfclud2fcl_core(nbfclud2fcl_core);
00031 okltest_nbfcsfd2fcs_core(nbfcsfd2fcs_core);
00032 
00033 okltest_nbfclud2fcl_alo(nbfclud2fcl_alo);
00034 okltest_nbfcsfd2fcs_alo(nbfcsfd2fcs_alo);
00035 
00036 okltest_nbfclud2fcl_aloamo(nbfclud2fcl_aloamo);
00037 okltest_nbfcsfd2fcs_aloamo(nbfcsfd2fcs_aloamo);
00038 
00039 okltest_snbfclfd2fcl_core(snbfclfd2fcl_core);
00040 okltest_snbfclud2fcl_core(snbfclud2fcl_core);
00041 okltest_snbfcsfd2fcs_core(snbfcsfd2fcs_core);
00042 
00043 okltest_snbfclfd2fcl_aloamo(snbfclfd2fcl_aloamo);
00044 okltest_snbfclud2fcl_aloamo(snbfclud2fcl_aloamo);
00045 okltest_snbfcsfd2fcs_aloamo(snbfcsfd2fcs_aloamo);
00046 
00047 okltest_extract_partition(extract_partition);
00048 
00049 /* **************************************
00050    * The generalised nested translation *
00051    **************************************
00052 */
00053 
00054 okltest_gennest_clause_trans(gennest_clause_trans);
00055 okltest_gennest_nbfcl2fcl(gennest_nbfcl2fcl);
00056 
00057 okltest_standtrans_T(standtrans_T);
00058 okltest_standtrans_fd_weak_TR(standtrans_fd_weak_TR);
00059 okltest_standtrans_ud_weak_TR(standtrans_fd_weak_TR);
00060 okltest_standtrans_fd_TV(standtrans_fd_TV);
00061 okltest_standtrans_ud_TV(standtrans_ud_TV);
00062 /* okltest_nbfclfd2fcl_alo(nbfclfd2fcl_alo_2); */
00063 okltest_nbfclud2fcl_alo(nbfclud2fcl_alo_2);
00064 
00065 okltest_standnest_T(standnest_T);
00066 okltest_standnest_TR(standnest_TR);
00067 okltest_standnest_strong_TR(standnest_strong_TR);
00068 okltest_standnest_TV(standnest_TV);
00069 okltest_nbfclud2fcl_standnest(nbfclud2fcl_standnest);
00070 okltest_nbfclud2fcl_standnest_strong(nbfclud2fcl_standnest_strong);
00071 
00072 okltest_logarithmic_T(logarithmic_T);
00073 okltest_logarithmic_TR(logarithmic_TR);
00074 okltest_logarithmic_TV(logarithmic_TV);
00075 okltest_nbfclud2fcl_logarithmic(nbfclud2fcl_logarithmic);
00076 
00077 okltest_reduced_T(reduced_T);
00078 okltest_reduced_TR(reduced_TR);
00079 okltest_reduced_strong_TR(reduced_strong_TR);
00080 okltest_reduced_TV(reduced_TV);
00081 okltest_nbfclud2fcl_reduced(nbfclud2fcl_reduced);
00082 okltest_nbfclud2fcl_reduced_strong(nbfclud2fcl_reduced_strong);
00083 
00084 /* ************************************************
00085    * Tools for the generalised nested translation *
00086    ************************************************
00087 */
00088 
00089 okltest_gennest_nbfcl2fcl_p(gennest_nbfcl2fcl_p);
00090 
00091 okltest_add_bincl_nec(add_bincl_nec);
00092