OKlibrary  0.2.1.6
TseitinTranslation.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 24.12.2010 (Swansea) */
00002 /* Copyright 2010, 2011, 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/Generators/Generators.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/TseitinTranslation.mac")$
00025 
00026 
00027 kill(f)$
00028 
00029 
00030 /* ****************************
00031    * Translating DNF into CNF *
00032    ****************************
00033 */
00034 
00035 okltest_dualts_fcl(f) := block(
00036   assert(f([[],[]]) = [[],[{}]]),
00037   assert(f([[3,1],[]]) = [[3,1],[{}]]),
00038   assert(f([[],[{}]]) = [[dts(1)],[{dts(1)},{dts(1)}]]),
00039   assert(f([[3,1],[{}]]) = [[3,1,dts(1)],[{dts(1)},{dts(1)}]]),
00040   assert(f([[3,1],[{},{1,3},{-3},{-1,-3}]]) = [
00041    [3,1,dts(1),dts(2),dts(3),dts(4)],
00042    [{dts(1)}, {-1,-3,dts(2)}, {3,dts(3)}, {1,3,dts(4)},
00043     {-dts(2),1}, {-dts(2),3}, {-dts(3),-3}, {-dts(4),-3},{-dts(4),-1},
00044     {dts(1),dts(2),dts(3),dts(4)}
00045    ]]),
00046   if oklib_test_level = 0 then return(true),
00047   for n : 0 thru 10 do block([input_FF,FF],
00048     input_FF : full_fcl(n),
00049     FF : f(input_FF),
00050     assert(nvar_fcl(FF) = nvar_dualts(input_FF)),
00051     assert(ncl_fcl(FF) = ncl_dualts(input_FF)),
00052     assert(ncl_list_fcl(FF) = ncl_list_dualts(input_FF))),
00053   true)$
00054 
00055 okltest_dualts_cs(f) := (
00056   assert(f({}) = {{}}),
00057   assert(f({{}}) = {{dts(1)}}),
00058   assert(f({{1}}) = {{-1,dts(1)},{1,-dts(1)},{dts(1)}}),
00059   true)$
00060 
00061 okltest_rcantrans_fcl2fcl(f) := (
00062   assert(f([[],[]]) = [[],[{}]]),
00063   assert(f([[3,1],[]]) = [[3,1],[{}]]),
00064   assert(f([[],[{}]]) = [[dts(1)],[{dts(1)}]]),
00065   assert(f([[3,1],[{}]]) = [[3,1,dts(1)],[{dts(1)}]]),
00066   assert(f([[3,1],[{},{1,3},{-3},{-1,-3}]]) = [
00067    [3,1,dts(1),dts(2),dts(3),dts(4)],
00068    [
00069     {-dts(2),1}, {-dts(2),3}, {-dts(3),-3}, {-dts(4),-3},{-dts(4),-1},
00070     {dts(1),dts(2),dts(3),dts(4)}
00071    ]]),
00072   true)$
00073 
00074 okltest_rcantrans_cs2cs(f) := (
00075   assert(f({}) = {{}}),
00076   assert(f({{}}) = {{dts(1)}}),
00077   assert(f({{},{1,3},{-3},{-1,-3}}) = {{-dts(2),-3},{-dts(3),-3},{-dts(3),-1},{-dts(4),1}, {-dts(4),3}, {dts(1),dts(2),dts(3),dts(4)}}),
00078   true)$
00079 
00080 okltest_dualtsplus_fcl(f) := block(
00081   assert(f([[],[]]) = [[],[{}]]),
00082   assert(f([[3,1],[]]) = [[3,1],[{}]]),
00083   assert(f([[],[{}]]) = [[dts(1)],[{dts(1)},{dts(1)}]]),
00084   assert(f([[3,1],[{}]]) = [[3,1,dts(1)],[{dts(1)},{dts(1)}]]),
00085   assert(f([[3,1],[{1,3},{1,-3},{-1,-3}]]) = [
00086    [3,1,dts(1),dts(2),dts(3)],
00087    [{-1,-3,dts(1)}, {-1,3,dts(2)}, {1,3,dts(3)},
00088     {-dts(1),1}, {-dts(1),3}, {-dts(2),-3}, {-dts(2),1}, {-dts(3),-3},
00089     {-dts(3),-1},{-3,dts(1)},{-1,dts(1),dts(2)},{1,dts(3)},
00090     {3,dts(2),dts(3)},{dts(1),dts(2),dts(3)}
00091    ]]),
00092   if oklib_test_level = 0 then return(true),
00093   for n : 0 thru 10 do block([input_FF,FF],
00094     input_FF : full_fcl(n),
00095     FF : f(input_FF),
00096     assert(nvar_fcl(FF) = nvar_dualts(input_FF)),
00097     assert(ncl_fcl(FF) = ncl_dualts(input_FF) + 2*n)
00098     /*assert(ncl_list_fcl(FF) = ncl_list_dualts(input_FF))*/),
00099   true)$
00100 
00101 okltest_dualtsext_fcl(f) := block([x],
00102   assert(f([[],[]],x) = [[],[{}]]),
00103   assert(f([[3,1],[]],x) = [[3,1],[{}]]),
00104   assert(f([[],[{}]],x) = [[dts(1,x)],[{dts(1,x)},{dts(1,x)}]]),
00105   assert(f([[3,1],[{}]],x) = [[3,1,dts(1,x)],[{dts(1,x)},{dts(1,x)}]]),
00106   assert(f([[3,1],[{},{1,3},{-3},{-1,-3}]],1) = [
00107    [3,1,dts(1,1),dts(2,1),dts(3,1),dts(4,1)],
00108    [{dts(1,1)}, {-1,-3,dts(2,1)}, {3,dts(3,1)}, {1,3,dts(4,1)},
00109     {-dts(2,1),1}, {-dts(2,1),3}, {-dts(3,1),-3}, {-dts(4,1),-3},{-dts(4,1),-1},
00110     {dts(1,1),dts(2,1),dts(3,1),dts(4,1)}
00111    ]]),
00112   if oklib_test_level = 0 then return(true),
00113   for n : 0 thru 10 do block([input_FF,FF],
00114     input_FF : full_fcl(n),
00115     FF : f(input_FF,1),
00116     assert(nvar_fcl(FF) = nvar_dualts(input_FF)),
00117     assert(ncl_fcl(FF) = ncl_dualts(input_FF)),
00118     assert(ncl_list_fcl(FF) = ncl_list_dualts(input_FF))),
00119   true)$
00120 
00121 /* Measures */
00122 
00123 okltest_nvar_dualts(f) := (
00124   assert(f([[],[]]) = 0),
00125   assert(f([[],[{}]]) = 1),
00126   assert(f([[1,2],[{1,2},{-1,2}]]) = 4),
00127   assert(f([[1,2],[{1,2},{-1}]]) = 4),
00128   assert(f([[1,2],[{1,2},{-1,2},{1,-2}]]) = 5),
00129   true)$
00130 
00131 okltest_nvar_dualts_num(f) := (
00132   assert(okltest_nvar_dualts(buildq([f], lambda([FF], f(nvar_fcl(FF), ncl_fcl(FF))))) = true),
00133   assert(okltest_nvar_full_dualts(f) = true),
00134   true)$
00135 
00136 okltest_nvar_full_dualts(f) := (
00137   assert(f(0,0) = 0),
00138   assert(f(1,0) = 1),
00139   for i : 1 thru 10 do
00140     assert(f(i,0) = i),
00141   assert(f(1,1) = 2),
00142   for i : 1 thru 5 do
00143     assert(f(i,i) = 2*i),
00144   assert(f(16,256) = 272),
00145   true)$
00146 
00147 okltest_ncl_dualts(f) := (
00148   assert(f([[],[]]) = 1),
00149   assert(f([[],[{}]]) = 2),
00150   assert(f([[1,2],[{1,2},{-1,2}]]) = 7),
00151   assert(f([[1,2],[{1,2},{-1}]]) = 6),
00152   assert(f([[1,2],[{1,2},{-1,2},{1,-2}]]) = 10),
00153   true)$
00154 
00155 okltest_ncl_full_dualts(f) := (
00156   assert(f(0,0) = 1),
00157   assert(f(1,0) = 1),
00158   assert(f(1,1) = 3),
00159   assert(f(16,256) = 4353),
00160   true)$
00161 
00162 okltest_ncl_list_dualts(f) := block(
00163   assert(f([[],[]]) = [[0,1]]),
00164   assert(f([[],[{}]]) = [[1,2]]),
00165   assert(f([[1,2],[{1,2},{-1,2}]]) = [[2,5],[3,2]]),
00166   assert(f([[1,2],[{1,2},{-1}]]) = [[2,5],[3,1]]),
00167   assert(f([[1,2],[{1,2},{-1,2},{1,-2}]]) = [[2,6],[3,4]]),
00168   assert(f([[1,2,3],[{1,2,3},{-1,2,3},{1,-2,3},{1,-2,-3},{-1,-2,-3}]]) =
00169     [[2,15],[4,5],[5,1]]),
00170   true)$
00171 
00172 okltest_ncl_list_full_dualts(f) := block(
00173   assert(f(0,0) = [[0,1]]),
00174   assert(f(1,0) = [[0,1]]),
00175   assert(f(0,1) = [[1,2]]),
00176   assert(f(1,1) = [[1,1],[2,2]]),
00177   assert(f(2,2) = [[2,5],[3,2]]),
00178   assert(f(2,4) = [[2,8],[3,4],[4,1]]),
00179   assert(f(16,256) = [[2,4096],[17,256],[256,1]]),
00180   if oklib_test_level = 1 then return(true),
00181   for n : 0 thru 10 do
00182     assert(f(n,n) = ncl_list_dualts([create_list(i,i,1,n),
00183         take_elements(n,full_fcl(n)[2])])),
00184   true)$   
00185