OKlibrary  0.2.1.6
SplittingTrees.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 31.1.2008 (Swansea) */
00002 /* Copyright 2008, 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/Backtracking/SplittingTrees.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/tests/SplittingTrees.mac")$
00023 
00024 /* ***************************"""""""""
00025    * The notion of a "splitting tree" *
00026    ************************************
00027 */
00028 
00029 okltest_fst_p(fst_p);
00030 okltest_st_p(st_p);
00031 okltest_est_p(est_p);
00032 
00033 okltest_complete_stp(complete_stp);
00034 
00035 /* ********************************
00036    * Manipulating splitting trees *
00037    ********************************
00038 */
00039 
00040 okltest_fst2st(fst2st);
00041 
00042 okltest_negate_st(negate_st);
00043 
00044 okltest_condense_st(condense_st);
00045 
00046 /* ***************************
00047    * Finding splitting trees *
00048    ***************************
00049 */
00050 
00051 okltest_optimal_splitting_tree(optimal_splitting_tree);
00052 okltest_optimal_r_splitting_tree(optimal_r_splitting_tree);
00053 
00054 /* ******************************
00055    * Evaluating splitting trees *
00056    ******************************
00057 */
00058 
00059 okltest_sat_pass_st(sat_pass_st);
00060 okltest_usat_clauses_st(usat_clauses_st);
00061 
00062 okltest_st2reslrt_cs(st2reslrt_cs);
00063 okltest_reslrt2st(reslrt2st);
00064 
00065 okltest_treepruning_st(treepruning_st);
00066 
00067 /* ***********************************
00068    * Generators for splitting trees  *
00069    ***********************************
00070 */
00071 
00072 okltest_complete_st_alldifferent(complete_st_alldifferent);
00073 
00074 okltest_horn_st(horn_st);
00075 okltest_input_list_st(input_list_st);
00076 okltest_horn_st(lambda([k], genhorn_st(k,1)));
00077 okltest_genhorn_st(genhorn_st);
00078 okltest_genhornsat_st(genhornsat_st);
00079 
00080 /* ***********************
00081    * r_k splitting trees *
00082    ***********************
00083 */
00084 
00085 okltest_rst2st(rst2st);
00086 okltest_rst2est(rst2est);
00087 
00088 /* **********
00089    * Output *
00090    **********
00091 */
00092