OKlibrary  0.2.1.6
Search.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 7.10.2011 (Swansea) */
00002 /* Copyright 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 
00025 kill(f)$
00026 
00027 
00028 /* *******************
00029    * Tree resolution *
00030    *******************
00031 */
00032 
00033 okltest_resolution_closure_treecomp_cs(f) := (
00034   assert(hm2sm(f({},0)) = {}),
00035   assert(hm2sm(f({{1},{-1}},0)) = {[{1},1],[{-1},1],[{},3]}),
00036   assert(hm2sm(f({{1},{-1}},{})) = {[{1},1],[{-1},1],[{},3]}),
00037   assert(hm2sm(f({{1},{-1}},{1})) = {[{1},1],[{-1},1]}),
00038   true)$
00039 
00040 okltest_treecomp_refutation_cs(f) := (
00041   assert(f({}) = false),
00042   assert(f({{}}) = 1),
00043   assert(f({{1},{-1}}) = 3),
00044   assert(f({{},{1},{-1}}) = 1),
00045   assert(f({{1,2},{-1},{-2}}) = 5),
00046   for n : 0 thru 3 do
00047     assert(f(full_cs(n)) = 2^(n+1)-1),
00048   true)$
00049 
00050 
00051 /* ***********************************
00052    * Short resolution proofs via SAT *
00053    ***********************************
00054 */
00055 
00056 okltest_shortresref_fcl2snbfclfd(f) := block([F,n,c,k],
00057   [n,c,k] : [0,0,1],
00058   F : f([[],[]],k),
00059   assert(nvar_fcl(F) = nvar_shortres_snbfclfd(n,c,k)),
00060   assert(ncl_fcl(F) = ncl_shortresref_snbfclfd(n,c,k)),
00061   assert(snbfclfd_p(F) = true),
00062   [n,c,k] : [0,1,1],
00063   F : f([[],[{}]],k),
00064   assert(nvar_fcl(F) = nvar_shortres_snbfclfd(n,c,k)),
00065   assert(ncl_fcl(F) = ncl_shortresref_snbfclfd(n,c,k)),
00066   assert(snbfclfd_p(F) = true),
00067   [n,c,k] : [1,2,1],
00068   F : f([[1],[{1},{-1}]],k),
00069   assert(nvar_fcl(F) = nvar_shortres_snbfclfd(n,c,k)),
00070   assert(ncl_fcl(F) = ncl_shortresref_snbfclfd(n,c,k)),
00071   assert(snbfclfd_p(F) = true),
00072   [n,c,k] : [2,4,1],
00073   F : f([[1,2],[{1,2},{1,-2},{-1,2},{-1,-2}]],k),
00074   assert(nvar_fcl(F) = nvar_shortres_snbfclfd(n,c,k)),
00075   assert(ncl_fcl(F) = ncl_shortresref_snbfclfd(n,c,k)),
00076   assert(snbfclfd_p(F) = true),
00077   [n,c,k] : [2,4,2],
00078   F : f([[1,2],[{1,2},{1,-2},{-1,2},{-1,-2}]],k),
00079   assert(nvar_fcl(F) = nvar_shortres_snbfclfd(n,c,k)),
00080   assert(ncl_fcl(F) = ncl_shortresref_snbfclfd(n,c,k)),
00081   assert(snbfclfd_p(F) = true),
00082   /* XXX */
00083   true)$
00084 
00085 okltest_shortresref_aloamo_fcl(f) := block([F,FF,n,c,k],
00086   [F,n,c,k] : [[[],[]],0,0,1],
00087   FF : f(F,k),
00088   assert(FF = [[],[{},{},{}]]),
00089   assert(nvar_fcl(FF) = nvar_shortres_aloamo(n,c,k)),
00090   assert(ncl_fcl(FF) = ncl_shortresref_aloamo(n,c,k)),
00091   [F,n,c,k] : [[[1],[{1},{-1}]],1,2,1],
00092   FF : f(F,k),
00093   assert(nvar_fcl(FF) = nvar_shortres_aloamo(n,c,k)),
00094   assert(ncl_fcl(FF) = ncl_shortresref_aloamo(n,c,k)),
00095   [F,n,c,k] : [[[1,2],[{1,2},{-1,2},{1,-2},{-1,-2}]],2,4,1],
00096   FF : f(F,k),
00097   assert(nvar_fcl(FF) = nvar_shortres_aloamo(n,c,k)),
00098   assert(ncl_fcl(FF) = ncl_shortresref_aloamo(n,c,k)),
00099   [F,n,c,k] : [[[1,2],[{1,2},{-1,2},{1,-2},{-1,-2}]],2,4,2],
00100   FF : f(F,k),
00101   assert(nvar_fcl(FF) = nvar_shortres_aloamo(n,c,k)),
00102   assert(ncl_fcl(FF) = ncl_shortresref_aloamo(n,c,k)),
00103   assert(ncl_fcl(FF) = ncl_shortresref_aloamo(n,c,k)),
00104   [F,n,c,k] : [[[1,2],[{1,2},{-1,2},{1,-2},{-1,-2},{1}]],2,5,3],
00105   FF : f(F,k),
00106   assert(nvar_fcl(FF) = nvar_shortres_aloamo(n,c,k)),
00107   assert(ncl_fcl(FF) = ncl_shortresref_aloamo(n,c,k)),
00108   /* XXX */
00109   true)$
00110 
00111 okltest_shortresref_setfirstresolvent_snbcl(f) := (
00112   assert(f([[1],[{1},{-1}]],1,2) = [{[sres_cl(1,3),0,1]}, {[sres_rv(3),1,1]}, {[sres_rp1(3),1,1]}, {[sres_rp2(3),2,1]}]),
00113   /* XXX */
00114   true)$
00115 
00116