OKlibrary  0.2.1.6
SplittingAnalysis.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 24.4.2008 (Guangzhou) */
00002 /* Copyright 2008, 2009 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/Backtracking/DLL_solvers.mac")$
00024 
00025 
00026 
00027 kill(f)$
00028 
00029 
00030 okltest_random_splitting_mus(f) := ([S : dll_simplest_trivial2],
00031   assert(f({{}},0,S) = [{{}}]),
00032   assert(f({{-1},{1}},1,S) = [{{-1},{1}},{{}}]),
00033   for n : 0 thru 3 do block(
00034    [F : full_fcs(n)[2]],
00035     for s : 0 thru 1 do block(
00036      [L : f(F,s,S)],
00037       assert(L[1] = F),
00038       assert(length(L) = n+1),
00039       assert(last(L) = {{}}),
00040       assert(map(nvar_cs,L) = create_list(n-i,i,0,n))
00041     )
00042   ),
00043   true)$
00044 
00045 okltest_random_splitting_nsing_mus(f) := ([S : dll_simplest_trivial2],
00046   assert(f({{}},0,S) = [{{}}]),
00047   assert(f({{-1},{1}},1,S) = [{{}}]),
00048   assert(f({{1,2},{1,-2},{-1,3},{-1,-3}},0,S) = [{{}}]),
00049   for n : 0 thru 3 do block(
00050    [F : full_fcs(n)[2]],
00051     for s : 0 thru 1 do block(
00052      [L : f(F,s,S)],
00053       assert(L[1] = if n <= 1 then {{}} else F),
00054       assert(length(L) = max(1,n)),
00055       assert(last(L) = {{}}),
00056       assert(map(nvar_cs,L) = if n <= 1 then [0] else append(create_list(n-i,i,0,n-2),[0]))
00057     )
00058   ),
00059   true)$
00060 
00061