OKlibrary  0.2.1.6
Constructions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 5.5.2008 (Guangzhou) */
00002 /* Copyright 2008, 2009, 2010, 2012, 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/Satisfiability/Lisp/ClauseSets/tests/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/tests/Generators.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00028 
00029 kill(f)$
00030 
00031 
00032 /* **********************
00033    * Logical operations *
00034    **********************
00035 */
00036 
00037 okltest_c2cl_expand(f) := (
00038   assert(f({},[]) = [{}]),
00039   assert(f({},[1]) = [{-1},{1}]),
00040   assert(f({1},[]) = [{1}]),
00041   assert(f({1},[2]) = [{1,-2},{1,2}]),
00042   assert(f({1,2},[3,4]) = [{1,2,-3,-4},{1,2,-3,4},{1,2,3,-4},{1,2,3,4}]),
00043   true)$
00044 
00045 okltest_c2cs_expand(f) := (
00046   assert(f({},{}) = {{}}),
00047   assert(f({},{1}) = {{-1},{1}}),
00048   assert(f({1},{}) = {{1}}),
00049   assert(f({1},{2}) = {{1,-2},{1,2}}),
00050   assert(f({1,2},{3,4}) = {{1,2,-3,-4},{1,2,-3,4},{1,2,3,-4},{1,2,3,4}}),
00051   true)$
00052 
00053 okltest_expand_fcs(f) := (
00054   assert(okltest_full_fcs_v(buildq([f], lambda([V], f([if listp(V) then setify(V) else V,{{}}])))) = true),
00055   for n : 0 thru 5 do block([V : setn(n), FF : full_fcs(n)],
00056     assert(f([V, create_list({i},i,1,n)]) = [V, disjoin(comp_sl(V),FF[2])])),
00057   true)$
00058 
00059 okltest_expand_cs(f) := (
00060   assert(f({}) = {}),
00061   assert(f({{}}) = {{}}),
00062   assert(f({{1}}) = {{1}}),
00063   assert(f({{1},{-1}}) = {{1},{-1}}),
00064   assert(f({{1},{2}}) = {{1,2},{1,-2},{2,-1}}),
00065   true)$
00066 
00067 okltest_or_cs2(f) := (
00068   assert(f({},{}) = {}),
00069   assert(f({},{{}}) = {}),
00070   assert(f({{}},{}) = {}),
00071   assert(f({{}},{{}}) = {{}}),
00072   assert(f({{}},{{1}}) = {{1}}),
00073   assert(f({{1}},{{-1}}) = {}),
00074   assert(f({{},{1},{-1}},{{},{1},{-1}}) = {{},{1},{-1}}),
00075   true)$
00076 
00077 okltest_or_cs(f) := (
00078   /* XXX */
00079   true)$
00080 
00081 okltest_dual_cs(f) := (
00082   assert(f({}) = {{}}),
00083   assert(f({{}}) = {}),
00084   assert(f({{1}}) = {{1}}),
00085   assert(f({{1},{-1}}) = {}),
00086   assert(f({{1},{2}}) = {{1,2}}),
00087   assert(f({{1},{-1,2}}) = {{1,2}}),
00088   assert(f({{1,2},{1,-2}}) = {{1},{1,-2},{1,2}}),
00089   assert(f({{1,2},{1,-2},{-1,2}}) = {{1,2}}),
00090   true)$
00091 
00092 okltest_comp_cs(f) := (
00093   assert(f({}) = {}),
00094   assert(f({{}}) = {{}}),
00095   assert(f({{1}}) = {{-1}}),
00096   assert(f({{1,2},{-2,-3}}) = {{-1,-2},{2,3}}),
00097   true)$
00098 
00099 okltest_comp_fcs(f) := block(
00100   okltest_comp_cs(buildq([f],lambda([F], fcs2cs(f(cs2fcs(F)))))),
00101   assert(f([{1,2,3},{{1,2},{-1,2}}]) = [{1,2,3},{{-1,-2},{1,-2}}]),
00102   true)$
00103 
00104 okltest_neg_cs(f) := (
00105   assert(f({}) = {{}}),
00106   assert(f({{}}) = {}),
00107   assert(f({{1}}) = {{-1}}),
00108   assert(f({{1},{-1}}) = {}),
00109   /* XXX */
00110   true)$
00111 
00112 
00113 /* ****************************
00114    * Combinatorial operations *
00115    ****************************
00116 */
00117 
00118 okltest_vardisjoint_sum_fcs(f) := (
00119   assert(f() = [{},{}]),
00120   okltest_standardise_fcs(buildq([f],lambda([FF],[f(FF),listify(FF[1])]))),
00121   assert(f([{3,4},{{-3},{4}}],[{1,3},{{1,3},{-1,-3}}]) = [{1,2,3,4},{{-1},{2},{3,4},{-3,-4}}]),
00122   true)$
00123 
00124 okltest_vardisjoint_full_gluing(f) := (
00125   assert(f([{},{}],[{},{}]) = [{},{}]),
00126   assert(f([{},{}],[{},{{}}]) = [{1},{{-1}}]),
00127   assert(f([{},{{}}],[{},{{}}]) = [{1},{{1},{-1}}]),
00128   assert(f([{},{}],[{1},{{1},{-1}}]) = [{1,2},{{-2,1},{-2,-1}}]),
00129   assert(f([{1,2},{{1},{-1,2}}],full_fcs(2)) = [{1,2,3,4,5},{{5,1},{5,-1,2},{-5,3,4},{-5,-3,4},{-5,3,-4},{-5,-3,-4}}]),
00130   true)$
00131 
00132 okltest_full_gluing(f) := (
00133   assert(f([{},{}],[{},{}]) = [{1},{}]),
00134   assert(f([{},{{}}],[{},{}]) = [{1},{{1}}]),
00135   assert(f([{},{}],[{},{{}}]) = [{1},{{-1}}]),
00136   assert(f([{},{{}}],[{},{{}}]) = [{1},{{1},{-1}}]),
00137   assert(f([{1},{{1}}],[{1},{{1}}]) = [{1,2},{{1,2},{1,-2}}]),
00138   assert(f([{1,3},{{1},{3}}],[{1,2},{{1},{2}}]) = [{1,2,3,4},{{1,4},{3,4},{1,-4},{2,-4}}]),
00139   assert(f([{2,4},{{2},{4}}],[{2,3},{{2},{3}}]) = [{1,2,3,4},{{1,4},{3,4},{1,-4},{2,-4}}]),
00140   assert(f([{1,2},{{1,2},{-1,2},{-2}}],[{1,2},{{1,-2},{1,2},{-1}}]) = [{1,2,3},{{1,2,3},{-1,2,3},{-2,3},{1,-2,-3},{1,2,-3},{-1,-3}}]),
00141   true)$
00142 
00143 okltest_partial_gluing(f) := (
00144   okltest_full_gluing(buildq([f],lambda([FF1,FF2],f(FF1,FF1[2],FF2,FF2[2])))),
00145   assert(f([{1,2},{{1},{2}}],{{2}},[{2,3},{{2},{3}}],{{3}}) = [{1,2,3,4},{{1},{2,4},{2},{3,-4}}]),
00146   true)$
00147 
00148 okltest_twisting_cs(f) := (
00149   assert(f({{}},{},{}) = {}),
00150   assert(f({{}},{},{{1,2},{-1}}) = {{1,2},{-1}}),
00151   assert(f({{1}},{1},{{1,2},{-1}}) = {{1,2}}),
00152   assert(f({{-1}},{-1},{{1,2},{-1}}) = {{-1}}),
00153   assert(f({{3}},{3},{{1,2},{-1}}) = {{1,2,3},{-1,3}}),
00154   assert(f({{1},{2}},{1},{}) = {{2}}),
00155   assert(f({{1},{2}},{1},{{}}) = {{1},{2}}),
00156   assert(f({{1},{2}},{1},{{3}}) = {{1,3},{2}}),
00157   assert(f({{1},{2},{-1}},{-1},{{3},{1,2},{2,3}}) = {{1},{2},{-1,3},{-1,2,3}}),
00158   true)$
00159 
00160 okltest_twisting_var_disjoint_cs(f) := (
00161   assert(f({{}},{},{}) = {}),
00162   assert(f({{}},{},{{1,2},{-1}}) = {{1,2},{-1}}),
00163   assert(f({{1}},{1},{{1,2},{-1}}) = {{1,2,3},{1,-2}}),
00164   assert(f({{-1}},{-1},{{1,2},{-1}}) = {{-1,2,3},{-1,-2}}),
00165   assert(f({{3}},{3},{{1,2},{-1}}) = {{1,2,3},{1,-2}}),
00166   assert(f({{1},{2}},{1},{}) = {{2}}),
00167   assert(f({{1},{2}},{1},{{}}) = {{1},{2}}),
00168   assert(f({{1},{2}},{1},{{3}}) = {{1,3},{2}}),
00169   assert(f({{1},{2},{-1}},{-1},{{3},{1,2},{2,3}}) = {{1},{2},{-1,5},{-1,3,4},{-1,4,5}}),
00170   true)$
00171