OKlibrary  0.2.1.6
NonBoolean.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 16.4.2009 (Swansea) */
00002 /* Copyright 2009, 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/DataStructures/Lisp/Lists.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00024 
00025 
00026 /* **************************
00027    * Variables and literals *
00028    **************************
00029 */
00030 
00031 /*
00032  Any value can be a "variable" or a "value" of a variable.
00033 */
00034 
00035 
00036 /*
00037  A "non-boolean literals" ("nbl") is a pair [v,e], where v
00038  is a variable and e a value.
00039  In a CNF the meaning is "v # e", while in a DNF the meaning is "v = e".
00040 */
00041 nbl_p(x) := listp(x) and is(length(x)=2)$
00042 
00043 var_nbl(x) := first(x)$
00044 val_nbl(x) := second(x)$
00045 
00046 
00047 /*
00048  A "signed non-boolean literal" ("snbl") is a triple [v,e,s] such
00049  that [v,e] is a non-boolean literal and s in {-1,+1}.
00050  The meaning is that if s = +1, then we have the DNF context, while
00051  if s = -1, then we have the CNF context.
00052 */
00053 snbl_p(x) :=
00054  listp(x) and is(length(x)=3) and nbl_p(rest(x,-1)) and elementp(x[3],{-1,+1})$
00055 
00056 var_snbl(x) := first(x)$
00057 val_snbl(x) := second(x)$
00058 sgn_snbl(x) := third(x)$
00059 
00060 
00061 /*
00062  A "power literal" ("pl") is a pair [v,V], where v is a variable and V is
00063  a set of values.
00064 */
00065 
00066 pl_p(x) := listp(x) and is(length(x)=2) and setp(second(x))$
00067 
00068 var_pl(x) := first(x)$
00069 val_pl(x) := second(x)$
00070 
00071 
00072 /*
00073  A "signed power literal" ("spl") is a triple [v,V,s] such
00074  that [v,V] is a power literal and s in {-1,+1}.
00075 */
00076 spl_p(x) :=
00077  listp(x) and is(length(x)=3) and pl_p(rest(x,-1)) and elementp(x[3],{-1,+1})$
00078 
00079 var_spl(x) := first(x)$
00080 val_spl(x) := second(x)$
00081 sgn_spl(x) := third(x)$
00082 
00083 
00084 /* ***********
00085    * Clauses *
00086    ***********
00087 */
00088 
00089 /*
00090  A "non-boolean clause" ("nbc") is a set of non-boolean literals
00091  such that different literals have different values.
00092 */
00093 nbc_p(C) :=
00094  setp(C) and every_s(nbl_p,C) and is(length(map(var_nbl,C))=length(C))$
00095 
00096 var_nbc(C) := map(var_nbl,C)$
00097 val_nbc(C) := map(val_nbl,C)$
00098 
00099 
00100 /*
00101  A "signed non-boolean clause" ("snbc") is a set of signed non-boolean literals
00102  such that different literals have different values.
00103 */
00104 snbc_p(C) :=
00105  setp(C) and every_s(snbl_p,C) and is(length(map(var_snbl,C))=length(C))$
00106 
00107 var_snbc(C) := map(var_snbl,C)$
00108 val_snbc(C) := map(val_snbl,C)$
00109 sgn_snbc(C) := map(sgn_snbl,C)$
00110 
00111 
00112 /* ***************
00113    * Clause-sets *
00114    ***************
00115 */
00116 
00117 /*
00118  A "non-boolean clause-set" ("nbcs") is a set of non-boolean clauses.
00119 */
00120 nbcs_p(F) := setp(F) and every_s(nbc_p,F)$
00121 
00122 var_nbcs(F) := lunion(map(var_nbc,listify(F)))$
00123 val_nbcs(F) := lunion(map(val_nbc,listify(F)))$
00124 
00125 lit_nbcs(F) := lunion(F)$
00126 
00127 /*
00128  A "signed non-boolean clause-set" ("snbcs") is a set of signed
00129  non-boolean clauses.
00130 */
00131 snbcs_p(F) := setp(F) and every_s(snbc_p,F)$
00132 
00133 var_snbcs(F) := lunion(map(var_snbc,listify(F)))$
00134 val_snbcs(F) := lunion(map(val_snbc,listify(F)))$
00135 sgn_snbcs(F) := lunion(map(sgn_snbc,listify(F)))$
00136 
00137 lit_snbcs(F) := lunion(F)$
00138 
00139 
00140 
00141 /*
00142  A "non-boolean clause-list" ("nbcl") is a list of non-boolean clauses.
00143 */
00144 nbcl_p(F) := listp(F) and every_s(nbc_p,F)$
00145 
00146 var_nbcl(F) := lunion(map(var_nbc,F))$
00147 val_nbcl(F) := lunion(map(val_nbc,F))$
00148 
00149 lit_nbcl(F) := lunion(F)$
00150 
00151 /*
00152  A "signed non-boolean clause-list" ("nbcl") is a list of signed
00153  non-boolean clauses.
00154 */
00155 snbcl_p(F) := listp(F) and every_s(snbc_p,F)$
00156 
00157 var_snbcl(F) := lunion(map(var_snbc,F))$
00158 val_snbcl(F) := lunion(map(val_snbc,F))$
00159 sgn_snbcl(F) := lunion(map(sgn_snbc,F))$
00160 
00161 lit_snbcl(F) := lunion(F)$
00162 
00163 
00164 
00165 /*
00166  A "non-boolean formal clause-set" ("nbfcs") is a pair [V,F] such that
00167  V is a set of variables and F is a non-boolean clause-set with
00168  var(F) <= V.
00169 */
00170 nbfcs_p(FF) :=
00171  listp(FF) and is(length(FF)=2) and setp(FF[1]) and nbcs_p(FF[2]) and
00172   subsetp(var_nbcs(FF[2]),FF[1])$
00173 
00174 var_nbfcs(FF) := FF[1]$
00175 val_nbfcs(FF) := val_nbcs(nbfcs2nbcs(FF))$
00176 
00177 lit_nbfcs(FF) := lit_nbcs(nbfcs2nbcs(FF))$
00178 
00179 /*
00180  A "signed non-boolean formal clause-set" ("snbfcs") is a pair [V,F] such that
00181  V is a set of variables and F is a signed non-boolean clause-set with
00182  var(F) <= V.
00183 */
00184 snbfcs_p(FF) :=
00185  listp(FF) and is(length(FF)=2) and setp(FF[1]) and snbcs_p(FF[2]) and
00186   subsetp(var_nbcs(FF[2]),FF[1])$
00187 
00188 var_snbfcs(FF) := FF[1]$
00189 val_snbfcs(FF) := val_snbcs(FF[2])$
00190 sgn_snbfcs(FF) := sgn_snbcs(FF[2])$
00191 
00192 lit_snbfcs(FF) := lit_snbcs(FF[2])$
00193 
00194 
00195 /*
00196  A "non-boolean formal clause-list" ("nbfcl") is a pair [V,F] such that
00197  V is a repetition-free list of variables and F is a non-boolean clause-list
00198  with var(F) <= V.
00199 */
00200 nbfcl_p(FF) :=
00201  listp(FF) and is(length(FF)=2) and listnorep_p(FF[1]) and nbcl_p(FF[2]) and
00202   subsetp(var_nbcl(FF[2]),setify(FF[1]))$
00203 
00204 var_nbfcl(FF) := FF[1]$
00205 val_nbfcl(FF) := val_nbcl(FF[2])$
00206 
00207 lit_nbfcl(FF) := lit_nbcl(FF[2])$
00208 
00209 /*
00210  A "signed non-boolean formal clause-list" ("snbfcl") is a pair [V,F] such that
00211  V is a repetition-free list of variables and F is a signed
00212  non-boolean clause-list with var(F) <= V.
00213 */
00214 snbfcl_p(FF) :=
00215  listp(FF) and is(length(FF)=2) and listnorep_p(FF[1]) and snbcl_p(FF[2]) and
00216   subsetp(var_snbcl(FF[2]),setify(FF[1]))$
00217 
00218 var_snbfcl(FF) := setify(FF[1])$
00219 val_snbfcl(FF) := val_snbcl(FF[2])$
00220 sgn_snbfcl(FF) := sgn_snbcl(FF[2])$
00221 
00222 lit_snbfcl(FF) := lit_snbcl(FF[2])$
00223 
00224 
00225 /*
00226  A "non-boolean formal clause-set with uniform domain" ("nbfcsud") is
00227  a triple [V,F,D] such that [V,F] is a non-boolean formal clause-set and
00228  D is a set with val(FF) <= D.
00229 */
00230 nbfcsud_p(FF) :=
00231  listp(FF) and is(length(FF)=3) and nbfcs_p(rest(FF,-1)) and
00232   subsetp(val_nbcs(FF[2]),FF[3])$
00233 
00234 /*
00235  A "signed non-boolean formal clause-set with uniform domain" ("snbfcsud") is
00236  a triple [V,F,D] such that [V,F] is a signed non-boolean formal clause-set and
00237  D is a set with val(FF) <= D.
00238 */
00239 snbfcsud_p(FF) :=
00240  listp(FF) and is(length(FF)=3) and snbfcs_p(rest(FF,-1)) and
00241   subsetp(val_snbcs(FF[2]),FF[3])$
00242 
00243 /*
00244  A "non-boolean formal clause-list with uniform domain" ("nbfclud") is
00245  a triple [V,F,D] such that [V,F] is a non-boolean formal clause-list and
00246  D is a repetition-free list with val(FF) <= D.
00247 */
00248 nbfclud_p(FF) :=
00249  listp(FF) and is(length(FF)=3) and nbfcl_p(rest(FF,-1)) and
00250   listnorep_p(FF[3]) and subsetp(val_nbcl(FF[2]),setify(FF[3]))$
00251 
00252 /*
00253  A "signed non-boolean formal clause-list with uniform domain" ("snbfclud") is
00254  a triple [V,F,D] such that [V,F] is a signed non-boolean formal clause-list
00255  and D is a repetition-free list with val(FF) <= D.
00256 */
00257 snbfclud_p(FF) :=
00258  listp(FF) and is(length(FF)=3) and snbfcl_p(rest(FF,-1)) and
00259   listnorep_p(FF[3]) and subsetp(val_snbcl(FF[2]),setify(FF[3]))$
00260 
00261 
00262 /*
00263  A "non-boolean formal clause-set with function domain" ("nbfcsfd") is
00264  a triple [V,F,D] such that [V,F] is a non-boolean formal clause-set and
00265  D is a map defined for all v in V such that D(v) is a set of values and
00266  for all literals x in F with var(x)=v we have val(x) in D(v).
00267 */
00268 nbfcsfd_p(FF) := block(
00269  [e : errcatch(
00270    listp(FF) and is(length(FF)=3) and nbfcs_p(rest(FF,-1)) and
00271    every_s(lambda([x], block([d: FF[3](var_nbl(x))], setp(d) and elementp(val_nbl(x),d))), lit_nbfcs(FF)))],
00272   not emptyp(e) and e[1])$
00273 
00274 /*
00275  A "signed non-boolean formal clause-set with function domain" ("snbfcsfd") is
00276  a triple [V,F,D] such that [V,F] is a signed non-boolean formal clause-set and
00277  D is a map defined for all v in V such that D(v) is a set of values and
00278  for all literals x in F with var(x)=v we have val(x) in D(v).
00279 */
00280 snbfcsfd_p(FF) := block(
00281  [e : errcatch(
00282    listp(FF) and is(length(FF)=3) and snbfcs_p(rest(FF,-1)) and
00283    every_s(lambda([x], block([d: FF[3](var_snbl(x))], setp(d) and elementp(val_snbl(x),d))), lit_snbfcs(FF)))],
00284   not emptyp(e) and e[1])$
00285 
00286 
00287 /*
00288  A "non-boolean formal clause-list with function domain" ("nbfclfd") is
00289  a triple [V,F,D] such that [V,F] is a non-boolean formal clause-list and
00290  D is a map defined for all v in V such that D(v) is a repetition-free list
00291  of values and for all literals x in F with var(x)=v we have val(x) in D(v).
00292 */
00293 nbfclfd_p(FF) := block(
00294  [e : errcatch(
00295    listp(FF) and is(length(FF)=3) and nbfcl_p(rest(FF,-1)) and
00296    every_s(lambda([x], block([d:FF[3](var_nbl(x))], listnorep_p(d) and member(val_nbl(x),d))), lit_nbfcl(FF)))],
00297   not emptyp(e) and e[1])$
00298 
00299 /*
00300  A "signed non-boolean formal clause-list with function domain" ("snbfclfd") is
00301  a triple [V,F,D] such that [V,F] is a signed non-boolean formal clause-list
00302  and D is a map defined for all v in V such that D(v) is a repetition-free
00303  list of values and for all literals x in F with var(x)=v we have val(x) in
00304  D(v).
00305 */
00306 snbfclfd_p(FF) := block(
00307  [e : errcatch(
00308    listp(FF) and is(length(FF)=3) and snbfcl_p(rest(FF,-1)) and
00309    every_s(lambda([x], block([d:FF[3](var_snbl(x))], listnorep_p(d) and member(val_snbl(x),d))), lit_snbfcl(FF)))],
00310   not emptyp(e) and e[1])$
00311 
00312 
00313 
00314 
00315 /* Checking equality */
00316 
00317 nbfcsfd_equalp(FF1,FF2) :=
00318  is(FF1[1]=FF2[1]) and is(FF1[2]=FF2[2]) and
00319  every_s(lambda([v], is(FF1[3](v) = FF2[3](v))), FF1[1])$
00320 
00321 
00322 /* ***************
00323    * Conversions *
00324    ***************
00325 */
00326 
00327 nbcs2nbcl(F) := listify(F)$
00328 nbcl2nbcs(F) := setify(F)$
00329 
00330 nbfcs2nbfcl(FF) := map(listify,FF)$
00331 snbfcs2snbfcl(FF) := map(listify,FF)$
00332 nbfcl2nbfcs(FF) := map(setify,FF)$
00333 snbfcl2snbfcs(FF) := map(setify,FF)$
00334 
00335 nbfcs2nbcs(FF) := second(FF)$
00336 nbfcl2nbcl(FF) := second(FF)$
00337 
00338 nbfcsud2nbfclud(FF) := map(listify,FF)$
00339 nbfclud2nbfcsud(FF) := map(setify,FF)$
00340 
00341 nbfcsfd2nbfclfd(FF) := [listify(FF[1]),listify(FF[2]),buildq([D:FF[3]],lambda([v],listify(D(v))))]$
00342 snbfcsfd2snbfclfd(FF) := nbfcsfd2nbfclfd(FF)$
00343 nbfclfd2nbfcsfd(FF) := [setify(FF[1]),setify(FF[2]),buildq([D:FF[3]],lambda([v],setify(D(v))))]$
00344 snbfclfd2snbfcsfd(FF) := nbfclfd2nbfcsfd(FF)$
00345 
00346 nbcs2nbfcs(F) := [var_nbcs(F),F]$
00347 snbcs2snbfcs(F) := [var_snbcs(F),F]$
00348 nbcl2nbfcl(F) := [listify(var_nbcs(F)),F]$
00349 snbcl2snbfcl(F) := [listify(var_snbcs(F)),F]$
00350 
00351 nbfcs2nbfcsud(FF) := endcons(val_nbfcs(FF), FF)$
00352 nbfcl2nbfclud(FF) := endcons(listify(val_nbfcl(FF)), FF)$
00353 
00354 nbfcsud2nbfcsfd(FF) := endcons(buildq([D:FF[3]], lambda([v],listify(D))), rest(FF,-1))$
00355 snbfcsud2snbfcsfd(FF) := nbfcsud2nbfcsfd(FF)$
00356 nbfclud2nbfclfd(FF) := endcons(buildq([D:FF[3]], lambda([v],listify(D))), rest(FF,-1))$
00357 snbfclud2snbfclfd(FF) := nbfclud2nbfclfd(FF)$
00358