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
```