OKlibrary  0.2.1.6
RandomClauseSets.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 6.7.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011 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/DataStructures/Lisp/Lists.mac")$
00025 
00026 
00027 kill(f)$
00028 
00029 /* *********************************
00030    * The fixed-clause-length model *
00031    *********************************
00032 */
00033 
00034 okltest_random_k_sublist_l(f) := block(
00035   assert(f([],0) = []),
00036   assert(f([1],0) = []),
00037   assert(f([1],1) = [1]),
00038   assert(f([1,1],1) = [1]),
00039   assert(elementp(f([1,2],1), {[1],[2]}) = true),
00040   assert(elementp(f([1,2],2), {[1,2],[2,1]}) = true),
00041   assert(elementp(f([1,2,1,2],2), {[1,2],[2,1]}) = true),
00042   for n : 0 thru 4 do block([L : create_list(i,i,1,n)],
00043     assert(sort(f(L,n)) = L)),
00044   block([L : [1,1,1,1,2,3,4,5,5]],
00045     set_random_state(make_random_state(0)),
00046     assert(f(L,2) = [5,1]),
00047     assert(f(L,3) = [1,2,5]),
00048     assert(f(L,4) = [4,1,5,3])),
00049   true)$
00050 
00051 okltest_random_fcl(f) := block(
00052   for n : 0 thru 3 do block([V : create_list(i,i,1,n),L],
00053     L : setify(append(V,-V)),
00054     for c : 0 thru 3 do
00055       for k : 0 thru n do block([LF : f(n,k,c)],
00056         assert(LF[1] = V),
00057         assert(listp(LF[2]) = true),
00058         assert(length(LF[2]) = c),
00059         assert(every_s(
00060          lambda([C],c_p(C) and subsetp(C,L) and is(length(C)=k)), LF[2]) = true))),
00061   set_random_state(make_random_state(0)),
00062   assert(f(3,2,3) = [[1,2,3],[{-3,2},{-3,-2},{-2,3}]]),
00063   assert(f(5,3,2) = [[1,2,3,4,5],[{2,3,5},{-5,-2,4}]]),
00064   true)$
00065 
00066 
00067 /* **********************************
00068    * The random clause-length model *
00069    **********************************
00070 */
00071 
00072 okltest_random_rcl_fcl(f) := block(
00073   assert(f(0,0,0) = [[],[]]),
00074   assert(f(0,1,0) = [[],[]]),
00075   assert(f(0,0,1) = [[],[{}]]),
00076   assert(f(0,1,1) = [[],[{}]]),
00077   assert(f(0,1,2) = [[],[{},{}]]),
00078   for n : 0 thru 3 do block([V : create_list(i,i,1,n), L],
00079     L : setify(append(V,-V)),
00080     for c : 0 thru 3 do block([LF : f(n,1,c)],
00081       assert(LF[1] = V),
00082       assert(listp(LF[2]) = true),
00083       assert(length(LF[2]) = c),
00084       assert(every_s(
00085          lambda([C],c_p(C) and subsetp(C,L) and is(length(C)=n)), LF[2]) = true))),
00086   set_random_state(make_random_state(0)),
00087   assert(f(3,1/3,3) = [[1,2,3],[{-1},{-1},{1}]]),
00088   assert(f(4,2/3,3) = [[1,2,3,4],[{-3,1},{-2},{-3,-2}]]),
00089   true)$
00090 
00091 
00092 /* **********************************
00093    * The OKgenerator (based on AES) *
00094    **********************************
00095 */
00096 
00097 okltest_OKlitgenerator_l(f) := (
00098   assert(f(0,0,100,3,0) = 30),
00099   assert(f(0,0,99,3,1) = -70),
00100   assert(f(0,0,98,3,2) = -73),
00101   assert(f(0,0,100,3,3) = 18),
00102   assert(f(0,0,99,3,4) = -9),
00103   assert(f(0,0,98,3,5) = -98),
00104   true)$
00105 
00106 okltest_OKlitgenerator_l_p(f) := (
00107   assert(f(0,0,1,0,0) = true),
00108   assert(f(2^64-1,2^64-1,2^31-1,2^31-1,2^64-1) = true),
00109   assert(f(2^64,2^64-1,2^31-1,2^31-1,2^64-1) = false),
00110   assert(f(2^64-1,2^64,2^31-1,2^31-1,2^64-1) = false),
00111   assert(f(2^64-1,2^64-1,2^31,2^31-1,2^64-1) = false),
00112   assert(f(2^64-1,2^64-1,2^31-1,2^31,2^64-1) = false),
00113   assert(f(2^64-1,2^64-1,2^31-1,2^31-1,2^64) = false),
00114   assert(f(0,0,100,3,0) = true),
00115   assert(f(0,0,99,3,1) = true),
00116   assert(f(0,0,98,3,2) = true),
00117   assert(f(0,0,100,3,3) = true),
00118   assert(f(0,0,99,3,4) = true),
00119   assert(f(0,0,98,3,5) = true),
00120   true)$
00121     
00122 okltest_OKgenerator_fcl(f) := block(
00123   assert(f(0,0,100,[3],[2]) = [create_list(i,i,1,100), [{-75,-71,30},{-100,-9,18}]]),
00124   if oklib_test_level=0 then return(true),
00125   assert(f(0,0,20,[3],[5]) = [create_list(i,i,1,20), [{-14,-9,-7},{-16,-3,13},{-17,10,11},{-9,3,15},{-16,4,6}]]),
00126   assert(f(0,1,20,[3],[5]) = [create_list(i,i,1,20), [{-12,1,6},{-3,7,8},{-3,9,13},{-12,2,14},{-12,18,20}]]),
00127   assert(f(0,2^32,20,[3],[5]) = [create_list(i,i,1,20), [{-16,-11,-3},{-20,-16,-11},{-17,8,20},{-19,-7,2},{-3,1,9}]]),
00128   assert(f(232,2^32,20,[3],[5]) = [create_list(i,i,1,20), [{-16,-13,19},{-1,9,20},{9,10,19},{-5,13,19},{-4,-2,13}]]),
00129   assert(f(0,0,1000,[3,4],[5,6]) = [create_list(i,i,1,1000), 
00130    [{-467,768,935},{-264,30,489},{321,676,879},{-962,602,780},{-318,21,68},
00131     {-492,-77,443,777},{-285,407,482,656},{-757,-336,-215,-123},
00132     {-914,-547,90,833},{-957,-267,507,747},{-707,-699,-196,170}]]),
00133   true)$
00134