OKlibrary  0.2.1.6
UnitClausePropagation.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 23.12.2008 (Schwalbach) */
00002 /* Copyright 2008, 2009, 2012 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/ConflictCombinatorics/HittingClauseSets.mac")$
00024 
00025 kill(f)$
00026 
00027 okltest_ucp_cs(f) := block(
00028   assert(f({}) = {}),
00029   assert(f({{}}) = {{}}),
00030   assert(f({{1}}) = {}),
00031   assert(f({{-1}}) = {}),
00032   assert(f({{-1},{1}}) = {{}}),
00033   assert(f({{-1},{1,2}}) = {}),
00034   assert(f({{-1},{1,2,3}}) = {{2,3}}),
00035   assert(f({{-1},{1,2},{-2,3},{-3}}) = {{}}),
00036   for n : 0 thru 5 do block([F : smusat_horn_cs(n)],
00037     assert(f(F) = {{}}),
00038     assert(f(union(F,{{1,2}})) = {{}})
00039   ),
00040   true)$
00041 
00042 okltest_ucp_lpa_cs(f) := (
00043   assert(f({}) = [{},[]]),
00044   assert(f({{}}) = [{{}},[]]),
00045   assert(f({{},{1}}) = [{{},{1}},[]]),
00046   assert(f({{1}}) = [{},[{1}]]),
00047   assert(f({{-1}}) = [{},[{-1}]]),
00048   assert(f({{1},{-1}}) = [{{}},[{1}]]),
00049   assert(f({{1},{-2}}) = [{},[{1,-2}]]),
00050   assert(f({{1,2}}) = [{{1,2}},[]]),
00051   assert(f({{1},{-1,-2},{2,3}}) = [{},[{1},{-2},{3}]]),
00052   assert(f({{1},{-1,-2},{2,3},{-1,2,-3}}) = [{{}},[{1},{-2},{3}]]),
00053   assert(f({{1},{-1,-2},{2,3},{-1,2,-3},{-1,2,-3,4}}) = [{{},{4}},[{1},{-2},{3}]]),
00054   assert(f({{1},{2},{3},{4},{-1,-2},{-3,-4}}) = [{{}},[{1,2,3,4}]]),
00055   assert(f({{1},{-1},{2},{-2}}) = [{{},{1},{-1}},[{2}]]),
00056   true)$
00057 
00058