OKlibrary  0.2.1.6
Generators.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 1.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011, 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/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00027 
00028 kill(f)$
00029 
00030 
00031 /* ********************
00032    * Full clause-sets *
00033    ********************
00034 */
00035 
00036 okltest_full_fcs_v(f) := (
00037   assert(f([]) = [{},{{}}]),
00038   assert(f({}) = [{},{{}}]),
00039   assert(f([1,3]) = [{1,3},{{-1,-3},{1,-3},{-1,3},{1,3}}]),
00040   assert(f({1,3,5}) = [{1,3,5},{{-1,-3,-5},{1,-3,-5},{-1,3,-5},{1,3,-5},{-1,-3,5},{1,-3,5},{-1,3,5},{1,3,5}}]),
00041   assert(okltest_full_fcs(buildq([f], lambda([n], f(setn(n))))) = true),
00042   true)$
00043 
00044 okltest_full_cs_v(f) := (
00045   assert(f([]) = {{}}),
00046   assert(f({}) = {{}}),
00047   assert(okltest_full_fcs_v(buildq([f], lambda([V], cs2fcs(f(V))))) = true),
00048   true)$
00049 
00050 okltest_full_fcl_v(f) := (
00051   assert(f([]) = [[],[{}]]),
00052   assert(f([1,2]) = [[1,2],[{-1,-2},{-1,2},{1,-2},{1,2}]]),
00053   assert(f({1,2}) = [[1,2],[{-1,-2},{-1,2},{1,-2},{1,2}]]),
00054   assert(f([3,1]) = [[3,1],[{-1,-3},{1,-3},{-1,3},{1,3}]]),
00055   assert(okltest_full_fcs_v(buildq([f], lambda([V], fcl2fcs(f(V))))) = true),
00056   assert(okltest_full_cl_v(buildq([f], lambda([V], fcl2cl(f(V))))) = true),
00057   true)$
00058 
00059 okltest_full_cl_v(f) := (
00060   assert(f([]) = [{}]),
00061   assert(f([2,3,4]) = [{-2,-3,-4},{-2,-3,4},{-2,3,-4},{-2,3,4},{2,-3,-4},{2,-3,4},{2,3,-4},{2,3,4}]),
00062   assert(okltest_full_cs_v(buildq([f], lambda([V], cl2cs(f(V))))) = true),
00063   true)$
00064 
00065 okltest_full_fcs(f) := (
00066   assert(f(0) = [{},{{}}]),
00067   assert(f(1) = [{1},{{-1},{1}}]),
00068   assert(f(2) = [{1,2},{{-1,-2},{-1,2},{1,-2},{1,2}}]),
00069   true)$
00070 
00071 okltest_full_cs(f) := (
00072   assert(f(0) = {{}}),
00073   assert(okltest_full_fcs(buildq([f], lambda([n], [setn(n),f(n)]))) = true),
00074   true)$
00075 
00076 okltest_full_fcl(f) := (
00077   assert(f(0) = [[],[{}]]),
00078   assert(okltest_full_fcs(buildq([f], lambda([n], fcl2fcs(f(n))))) = true),
00079   true)$
00080 
00081 okltest_full_cl(f) := (
00082   assert(f(0) = [{}]),
00083   assert(okltest_full_fcl(buildq([f], lambda([n], [create_list(i,i,1,n),f(n)]))) = true),
00084   true)$
00085 
00086 okltest_nvar_full_fcs(f) := block(
00087  for n : 0 thru 4 do
00088    assert(f(n) = nvar_f(full_fcs(n))),
00089  true)$
00090 
00091 okltest_ncl_list_full_fcs(f) := block(
00092  for n : 0 thru 4 do
00093    assert(f(n) = ncl_list_fcs(full_fcs(n))),
00094  true
00095 )$
00096 
00097 okltest_ncl_full_fcs(f) := block(
00098  for n : 0 thru 4 do
00099    assert(f(n) = ncl_fcs(full_fcs(n))),
00100  true
00101 )$
00102 
00103 okltest_deficiency_full_fcs(f) := block(
00104  for n : 0 thru 4 do
00105    assert(f(n) = deficiency_fcs(full_fcs(n))),
00106  true
00107 )$
00108 
00109 
00110 
00111 /* ********************
00112    * Order principles *
00113    ********************
00114 */
00115 
00116 okltest_gt_var(f) := block([x,y].
00117   assert(f(x,y) = gt(x,y)),
00118   true)$
00119 
00120 okltest_var_ordergt(f) := (
00121   assert(f(0) = []),
00122   assert(f(1) = []),
00123   assert(f(2) = [gt(1,2),gt(2,1)]),
00124   assert(f(3) = [gt(1,2),gt(2,1),gt(1,3),gt(3,1),gt(2,3),gt(3,2)]),
00125   true)$
00126 
00127 okltest_ordergt_transitivity_ocs(f) := (
00128   assert(f(0) = []),
00129   assert(f(1) = []),
00130   assert(f(2) = []),
00131   assert(f(3) = [{-gt(1,2),-gt(2,3),gt(1,3)},{-gt(1,3),-gt(3,2),gt(1,2)},{-gt(2,1),-gt(1,3),gt(2,3)},{-gt(2,3),-gt(3,1),gt(2,1)},{-gt(3,1),-gt(1,2),gt(3,2)},{-gt(3,2),-gt(2,1),gt(3,1)}]),
00132   true)$
00133 
00134 okltest_ordergt_nocycles_ocs(f) := (
00135   assert(f(0) = []),
00136   assert(f(1) = []),
00137   assert(f(2) = [{-gt(1,2),-gt(2,1)}]),
00138   assert(f(3) = [{-gt(1,2),-gt(2,1)},{-gt(1,3),-gt(3,1)},{-gt(2,3),-gt(3,2)}]),
00139   true)$
00140 
00141 okltest_ordergt_nosource_ocs(f) := (
00142   assert(f(0) = []),
00143   assert(f(1) = [{}]),
00144   assert(f(2) = [{gt(2,1)},{gt(1,2)}]),
00145   assert(f(3) = [{gt(2,1),gt(3,1)},{gt(1,2),gt(3,2)},{gt(1,3),gt(2,3)}]),
00146   true)$
00147 
00148 okltest_ordergt_ofcs(f) := (
00149   assert(f(0) = [[],[]]),
00150   assert(f(1) = [[],[{}]]),
00151   assert(f(2) = [[gt(1,2),gt(2,1)],[{-gt(1,2),-gt(2,1)},{gt(2,1)},{gt(1,2)}]]),
00152   true)$
00153