|
| 1 | +# An expression of the form "X %in% {x1, x2, x3}" |
| 2 | +#' @title Atoms for CNF Formulas |
| 3 | +#' |
| 4 | +#' @description |
| 5 | +#' `CnfAtom` objects represent a single statement that is used to build up CNF formulae. |
| 6 | +#' They are mostly intermediate, created using the [`%among%`] operator or [`CnfAtom()`] |
| 7 | +#' directly, and combined into [`CnfClause`] and [`CnfFormula`] objects. |
| 8 | +#' [`CnfClause`] and [`CnfFormula`] do not, however, contain [`CnfAtom`] objects directly, |
| 9 | +#' |
| 10 | +#' `CnfAtom`s contain an indirect reference to a [`CnfSymbol`] by referencing its name |
| 11 | +#' and its [`CnfUniverse`]. They furthermore contain a set of values. An `CnfAtom` |
| 12 | +#' represents a statement asserting that the given symbol takes up one of the |
| 13 | +#' given values. |
| 14 | +#' |
| 15 | +#' If the set of values is empty, the `CnfAtom` represents a contradiction (FALSE). |
| 16 | +#' If it is the full domain of the symbol, the `CnfAtom` represents a tautology (TRUE). |
| 17 | +#' These values can be converted to, and from, `logical(1)` values using `as.logical()` |
| 18 | +#' and `as.CnfAtom()`. |
| 19 | +#' |
| 20 | +#' `CnfAtom` objects can be negated using the `!` operator, which will return the `CnfAtom` |
| 21 | +#' representing set membership in the complement of the symbol with respect to its domain. |
| 22 | +#' `CnfAtom`s can furthermore be combined using the `|` operator to form a [`CnfClause`], |
| 23 | +#' and using the `&` operator to form a [`CnfFormula`]. This happens even if the |
| 24 | +#' resulting statement could be represented as a single `CnfAtom`. |
| 25 | +#' |
| 26 | +#' This is part of the CNF representation tooling, which is currently considered |
| 27 | +#' experimental; it is for internal use. |
| 28 | +#' |
| 29 | +#' @details |
| 30 | +#' We would have preferred to overload the `%in%` operator, but this is currently |
| 31 | +#' not easily possible in R. We therefore created the `%among%` operator. |
| 32 | +#' |
| 33 | +#' The internal representation of a `CnfAtom` may change in the future. |
| 34 | +#' |
| 35 | +#' @param symbol ([`CnfSymbol`]) \cr |
| 36 | +#' The symbol to which the atom refers. |
| 37 | +#' @param values (`character`) \cr |
| 38 | +#' The values that the symbol can take. |
| 39 | +#' @param e1 (`CnfSymbol`) \cr |
| 40 | +#' Left-hand side of the `%among%` operator. |
| 41 | +#' Passed as `symbol` to `CnfAtom()`. |
| 42 | +#' @param e2 (`character`) \cr |
| 43 | +#' Right-hand side of the `%among%` operator. |
| 44 | +#' Passed as `values` to `CnfAtom()`. |
| 45 | +#' @param x (any) \cr |
| 46 | +#' The object to be coerced to a `CnfAtom` by `as.CnfAtom`. |
| 47 | +#' Only `logical(1)` and `CnfAtom` itself are currently supported. |
| 48 | +#' @return A new `CnfAtom` object. |
| 49 | +#' @examples |
| 50 | +#' u = CnfUniverse() |
| 51 | +#' X = CnfSymbol(u, "X", c("a", "b", "c")) |
| 52 | +#' |
| 53 | +#' CnfAtom(X, c("a", "b")) |
| 54 | +#' X %among% "a" |
| 55 | +#' X %among% character(0) |
| 56 | +#' X %among% c("a", "b", "c") |
| 57 | +#' |
| 58 | +#' as.logical(X %among% character(0)) |
| 59 | +#' as.CnfAtom(TRUE) |
| 60 | +#' |
| 61 | +#' !(X %among% "a") |
| 62 | +#' |
| 63 | +#' X %among% "a" | X %among% "b" # creates a CnfClause |
| 64 | +#' |
| 65 | +#' X %among% "a" & X %among% c("a", "b") # creates a CnfFormula |
| 66 | +#' @family CNF representation objects |
| 67 | +#' @keywords internal |
| 68 | +#' @export |
| 69 | +CnfAtom = function(symbol, values) { |
| 70 | + assert_class(symbol, "CnfSymbol") |
| 71 | + domain = attr(symbol, "universe")[[symbol]] |
| 72 | + assert_subset(values, domain) |
| 73 | + if (all(domain %in% values)) { |
| 74 | + entry = TRUE |
| 75 | + } else if (length(values) == 0) { |
| 76 | + entry = FALSE |
| 77 | + } else { |
| 78 | + entry = list(symbol = c(symbol), values = unique(values)) |
| 79 | + } |
| 80 | + structure( |
| 81 | + entry, |
| 82 | + universe = attr(symbol, "universe"), |
| 83 | + class = "CnfAtom" |
| 84 | + ) |
| 85 | +} |
| 86 | + |
| 87 | +#' @export |
| 88 | +print.CnfAtom = function(x, ...) { |
| 89 | + if (isTRUE(x)) { |
| 90 | + cat("CnfAtom: <TRUE>\n") |
| 91 | + } else if (isFALSE(x)) { |
| 92 | + cat("CnfAtom: <FALSE>\n") |
| 93 | + } else { |
| 94 | + cat(sprintf("CnfAtom: %s \U2208 {%s}.\n", x$symbol, paste(x$values, collapse = ", "))) |
| 95 | + } |
| 96 | + invisible(x) |
| 97 | +} |
| 98 | + |
| 99 | +#' @export |
| 100 | +format.CnfAtom = function(x, ...) { |
| 101 | + if (isTRUE(x)) { |
| 102 | + return("CnfAtom: T") |
| 103 | + } else if (isFALSE(x)) { |
| 104 | + return("CnfAtom: F") |
| 105 | + } else { |
| 106 | + return(sprintf("CnfAtom(%s)", x$symbol)) |
| 107 | + } |
| 108 | +} |
| 109 | + |
| 110 | +# construct CnfAtom with `X %among% c("a", "b", "c")` |
| 111 | +# we cannot overload `%in%`, unfortunately |
| 112 | +#' @export |
| 113 | +#' @rdname CnfAtom |
| 114 | +`%among%` = function(e1, e2) { |
| 115 | + UseMethod("%among%") |
| 116 | +} |
| 117 | + |
| 118 | +#' @export |
| 119 | +`%among%.CnfSymbol` = function(e1, e2) { |
| 120 | + CnfAtom(e1, e2) |
| 121 | +} |
| 122 | + |
| 123 | +#' @export |
| 124 | +`%among%.default` = function(e1, e2) { |
| 125 | + stop("%among% operation not defined for LHS. %among% should typically be used with a CnfSymbol.") |
| 126 | +} |
| 127 | + |
| 128 | + |
| 129 | +#' @rdname CnfAtom |
| 130 | +#' @export |
| 131 | +as.CnfAtom = function(x) { |
| 132 | + UseMethod("as.CnfAtom") |
| 133 | +} |
| 134 | + |
| 135 | +#' @export |
| 136 | +as.CnfAtom.default = function(x) { |
| 137 | + stop("Cannot convert object to CnfAtom.") |
| 138 | +} |
| 139 | + |
| 140 | +#' @export |
| 141 | +as.CnfAtom.logical = function(x) { |
| 142 | + assert_flag(x) |
| 143 | + structure( |
| 144 | + x, |
| 145 | + universe = attr(x, "universe"), |
| 146 | + class = "CnfAtom" |
| 147 | + ) |
| 148 | +} |
| 149 | + |
| 150 | +#' @export |
| 151 | +as.CnfAtom.CnfAtom = function(x) { |
| 152 | + x |
| 153 | +} |
| 154 | + |
| 155 | +#' @export |
| 156 | +as.logical.CnfAtom = function(x, ...) { |
| 157 | + if (is.logical(x)) { |
| 158 | + return(unclass(x)) |
| 159 | + } |
| 160 | + return(NA) |
| 161 | +} |
| 162 | + |
| 163 | +#' @export |
| 164 | +all.equal.CnfAtom = function(target, current, ...) { |
| 165 | + if (is.logical(target) && is.logical(current)) { |
| 166 | + # compare truth-values directly, even if they disagree on universe |
| 167 | + # (since logical atoms sometimes have universe set to NULL) |
| 168 | + if (identical(c(target), c(current))) { |
| 169 | + return(TRUE) |
| 170 | + } |
| 171 | + return("target and current are both logicals but not equal") |
| 172 | + } |
| 173 | + if (is.logical(target) || is.logical(current)) { |
| 174 | + return("target and current are not both logicals") |
| 175 | + } |
| 176 | + if (!inherits(current, "CnfAtom")) { |
| 177 | + return("current is not a CnfAtom") |
| 178 | + } |
| 179 | + target$values = sort(target$values) |
| 180 | + current$values = sort(current$values) |
| 181 | + all.equal.list(target, current, ...) |
| 182 | +} |
| 183 | + |
| 184 | +#' @rawNamespace if (getRversion() >= "4.3.0") S3method(chooseOpsMethod,CnfAtom) |
| 185 | +chooseOpsMethod.CnfAtom <- function(x, y, mx, my, cl, reverse) TRUE |
| 186 | + |
| 187 | +#' @export |
| 188 | +`&.CnfAtom` = function(e1, e2) { |
| 189 | + # Will return a CnfFormula, so we can just delegate to there. |
| 190 | + # `&.CnfFormula` handles conversion. |
| 191 | + `&.CnfFormula`(e1, e2) |
| 192 | +} |
| 193 | + |
| 194 | +#' @export |
| 195 | +`|.CnfAtom` = function(e1, e2) { |
| 196 | + if (inherits(e2, "CnfFormula")) { |
| 197 | + # `|.CnfFormula` handles conversion |
| 198 | + return(`|.CnfFormula`(e1, e2)) |
| 199 | + } |
| 200 | + if (isFALSE(e1) || isTRUE(e2)) return(as.CnfClause(e2)) |
| 201 | + if (isFALSE(e2) || isTRUE(e1)) return(as.CnfClause(e1)) |
| 202 | + |
| 203 | + # either two proper CnfAtoms, or e2 is a CnfClause. |
| 204 | + CnfClause(list(e1, e2)) |
| 205 | +} |
| 206 | + |
| 207 | +#' @export |
| 208 | +`!.CnfAtom` = function(x) { |
| 209 | + if (is.logical(x)) { |
| 210 | + return(as.CnfAtom(!unclass(x))) |
| 211 | + } |
| 212 | + structure( |
| 213 | + list(symbol = x$symbol, values = setdiff(attr(x, "universe")[[x$symbol]], x$values)), |
| 214 | + universe = attr(x, "universe"), |
| 215 | + class = "CnfAtom" |
| 216 | + ) |
| 217 | +} |
0 commit comments