added fix for issue #16, thanks to Romina Filippini and Simona Toti

Author: edwindj

NAMESPACE

@@ -9,6 +9,7 @@ S3method(print,mip_rule)
 export(detect_boundary_cat)
 export(detect_boundary_num)
 export(detect_fixed_variables)
+export(detect_infeasible_if_rules)
 export(detect_infeasible_rules)
 export(detect_redundancy)
 export(is_categorical)

R/contradicted.R

@@ -10,16 +10,18 @@
 #' @return `character` with conflicting rules.
 is_contradicted_by <- function(x, rule_name){
   rn <- rule_name %in% names(x)
-  
+
   if (any(!rn)){
     nms <- paste0('"',rule_name[!rn], '"', collapse = ", ")
     warning("Rule(s) ", nms, " not found in rule set 'x'.", call. = FALSE)
   }
 
   N <- length(x)
-  weight <- rep(N, length(rule_name))
+  #weight <- rep(N, length(rule_name))
+  weight <- rep(Inf, length(rule_name))
   names(weight) <- rule_name
 
+  
   res <- character()
   contra <- detect_infeasible_rules(x, weight = weight)
   while (length(contra) && !any(contra %in% names(weight))){

R/detect_infeasible_if_rules.R

@@ -0,0 +1,91 @@
+#' Detect infeasible if clauses
+#' 
+#' Detect if clauses that contradict each other. This is useful to detect if clauses that are not satistifable.
+#' 
+#' @param x A validator object.
+#' @param ... Additional arguments passed to `detect_if_clauses`.
+#' @param verbose Logical. If `TRUE`, print the results.
+#' @return A list of contradictions found in the if clauses, or `NULL` if none are found.
+#' @family feasibility
+#' @example ./examples/detect_infeasible_if_rules.R
+#' @export
+detect_infeasible_if_rules <- function(x, ..., verbose = TRUE){
+  res <- detect_if_clauses(x, ...)
+  if (length(res) == 0){
+    if (verbose){
+      message("No contradictory if clauses found.")
+    }
+    return(NULL)
+  }
+  
+  if (verbose){
+    message(
+      length(res), 
+      " contradiction(s) with if clauses found:"
+    )
+    for (i in seq_along(res)){
+      cat(sprintf("When %s:\n", names(res)[i]))
+      x_c <- x[res[[i]]]
+      
+      expr <- sapply(x_c$rules, function(r){
+        deparse(r@expr)
+      })
+      cat(paste0("  ", res[[i]], ": ", expr, collapse = "\n"))
+      cat("\n")
+    }
+  }
+  
+  invisible(res)
+}
+
+# Detect if clauses that contradict each other. This is useful to detect if clauses that are not satistifable
+detect_if_clauses <- function(x, ...){
+  x <- check_validator(x)
+  is_cond <- is_conditional(x) | is_categorical(x)
+  vals <- to_exprs(x)
+  
+  l <- list()
+  for (i in which(is_cond)){
+    cond <- vals[[i]]
+    r <- check_condition(cond, x)
+    l[names(r)] <- r
+  }
+  
+  l
+}
+
+check_condition <- function(cond_expr, x){
+  clauses <- as_dnf(cond_expr)
+  
+  # test whether it is an if statement
+  if (length(clauses) <= 1){
+    return(NULL)
+  }
+  # to do for %in statement and replace with multiple "=="
+  neg_clauses <- lapply(clauses, invert_or_negate)
+  
+  l <- list()
+  for (neg in neg_clauses){
+    v <- x + do.call(validate::validator, list(.test = neg))
+    if (is_feasible(v)){
+      next
+    }
+    v1 <- is_contradicted_by(v, ".test")
+    l[[deparse(neg)]] <- v1
+    # op <- op_to_s(neg)
+    # if (op == "=="){
+    #   .values <- list(neg[[3]]) |> setNames(as.character(neg[[2]]))
+    #   test_rules <- substitute_values(x, .values = .values)
+    #   v <- detect_infeasible_rules(test_rules)
+    #   if (is.null(v)){
+    #     next
+    #   }
+    #   v1 <- is_contradicted_by(test_rules, v)
+    #   v <- c(v,v1)
+    #   l[[deparse(neg)]] <- v
+    # } 
+    
+    # TODO expand %in% statement here
+  }
+  l
+}

R/feasible.R

@@ -61,13 +61,19 @@ make_feasible <- function(x, ...){
 #' @param ... not used
 #' @return `character` with the names of the rules that are causing infeasibility.
 detect_infeasible_rules <- function(x, weight = numeric(), ...){
+  # browser()
   if (!is_infeasible(x)){
     return(character())
   }
-  
+  # browser()
+
   mr <- to_miprules(x)
   mr <- fix_cat_domain(mr)
 
+  nms <- mr |> sapply(\(x) x$rule)
+  w_inf <- nms[grepl("^\\.domain.", nms)] |> sapply(\(x) Inf)
+  weight <- c(weight, w_inf)
+
   is_equality <- sapply(mr, function(m){
     m$op == "==" && all(m$type == "double")
   })
@@ -87,8 +93,15 @@ detect_infeasible_rules <- function(x, weight = numeric(), ...){
   }
 
   # make all rules soft rules
+  wl <- as.list(weight)
   objective <- numeric()
   mr <- lapply(mr , function(r){
+    w <- wl[[r$rule]]
+    exclude <- (is.numeric(w) && w == Inf)
+    if (exclude){
+      return(r)
+    }
+    
     is_lin <- all(r$type == "double")
     is_cat <- all(r$type == "binary")
     if (is_lin){
@@ -102,17 +115,18 @@ detect_infeasible_rules <- function(x, weight = numeric(), ...){
     objective[[paste0(".delta_", r$rule)]] <<- r$weight
     r
   })
-  
   # set the weights to the weights supplied by the user
-  if (!is.null(names(weight))){
-    names(weight) <- paste0(".delta_", names(weight))
-    objective[names(weight)] <- weight
+  if (length(weight) && !is.null(names(weight))){
+    weight <- weight[sapply(weight, is.finite)]
+    if (length(weight)){
+      names(weight) <- paste0(".delta_", names(weight))
+      objective[names(weight)] <- weight
+    }
   }
-  
   lp <- translate_mip_lp(mr, objective = objective) #TODO figure out "eps" param
   lpSolveAPI::lp.control( lp
                         #, verbose="full"
-                        , presolve="none"
+                        , presolve="rows"
                         )
   res <- solve(lp)
 

R/soft-rule.R

@@ -1,10 +1,13 @@
 #TODO rename to mip_*
 
 # convert statements of A == '1' into A + .delta_A == '1'
+# convert statements of a:a - b:b <= 0 into a:a - b:b - delta <= 0
 soft_cat_rule <- function(x, prefix=".delta_", name = x$rule,  ...){
   stopifnot(inherits(x, "mip_rule"))
   nm <- paste0(prefix, name, collapse = "")
-  delta <- setNames(1L, nm)
+  neg <- min(sum(x$a[x$a < 0]), -1L)
+  delta <- ifelse(x$op == "==", 1L, neg)
+  delta <- setNames(delta, nm)
   x$a <- c(x$a, delta)
   x$type <- c(x$type, setNames("binary", nm))
   x

R/utils.R

@@ -26,11 +26,11 @@ get_variables_num <- function(x){
 }
 
 get_variables_cat <- function(x){
-  var_cat <- sapply(to_miprules(x), function(mr){
+  var_cat <- lapply(to_miprules(x), function(mr){
     nms <- names(mr$type)
     nms[mr$type == "binary" & grepl(":", nms)]
   })
-  var_cat <- unique(unlist(var_cat))
+  var_cat <- unique(var_cat |> unlist())
   if (length(var_cat) == 0){
     return(
       data.frame( bin_variable = character(0)

examples/detect_infeasible_if_rules.R

@@ -0,0 +1,6 @@
+rules <- validator(
+  if (nace == "a") export == "y",
+  if (nace == "a")  export == "n"
+)
+
+detect_infeasible_if_rules(rules)

issues/cat_no_domain.R

@@ -10,6 +10,8 @@ is_feasible(rules)
 
 
 conflicts <- detect_infeasible_rules(rules)
-conflict
+conflicts
 conflict2 <- is_contradicted_by(rules, conflicts)
 make_feasible(rules)
+
+