diff --git a/R/CnfFormula_simplify1.R b/R/CnfFormula_simplify1.R index 7aae90e96..4cee6a104 100644 --- a/R/CnfFormula_simplify1.R +++ b/R/CnfFormula_simplify1.R @@ -619,19 +619,24 @@ simplify_cnf = function(entries, universe) { second_order_enabled = TRUE second_order_enabled_matrix = not_subset_count > 2L # allow cascading of indirect SSE, except for the combinations where we trigger it manually (otherwise we'd be running them twice) + # we need to make sure we don't trigger for eliminated / unit clauses, so we set them to TRUE here. + # This means all remaining entries of the second_order_enabled_matrix are exactly the ones for which we trigger on_updated_subset_relations() manually. + meta_disabled = eliminated[available] | is_unit[available] + second_order_enabled_matrix[meta_disabled, ] = TRUE + second_order_enabled_matrix[, meta_disabled] = TRUE # alternatively, we could also enable none of the cascading in the beginning and have a nested loop in the following, where we 'repeat' until there are no more rowsum <= 2L # That would probably give uns less cascading, but we'd have to run 'which()' on a N^2 matrix potentially many times. - sse_to_trigger = which(not_subset_count <= 2L, arr.ind = TRUE) + + sse_to_trigger = which(!second_order_enabled_matrix, arr.ind = TRUE) for (sse_idx in seq_len(nrow(sse_to_trigger))) { meta_idx = sse_to_trigger[sse_idx, 1L] meta_idx_other = sse_to_trigger[sse_idx, 2L] + if (eliminated[[available[[meta_idx]]]] || is_unit[[available[[meta_idx]]]] || eliminated[[available[[meta_idx_other]]]] || is_unit[[available[[meta_idx_other]]]]) next second_order_enabled_matrix[meta_idx, meta_idx_other] = TRUE - on_updated_subset_relations(meta_idx, meta_idx_other, TRUE) + if (identical(on_updated_subset_relations(meta_idx, meta_idx_other, TRUE), TRUE)) return(return_entries(FALSE)) } - - # Now for the big one: Asymmetric Hidden Literal Addition (Marijn et al.) # First, we do non-units, then we do units separately. diff --git a/attic/experiments.R b/attic/experiments.R index c72ac7e3d..1aa5a3e35 100644 --- a/attic/experiments.R +++ b/attic/experiments.R @@ -1245,6 +1245,8 @@ meta_idx_inner c lapply(seq_along(eliminated), function(x) if (eliminated[[x]]) FALSE else structure(entries[[x]], class = "CnfClause")) + + entries[!eliminated] |> lapply(structure, class = "CnfClause") which(eliminated) @@ -1307,6 +1309,34 @@ C = CnfSymbol(u, "C", c("c1", "c2", "c3")) +quote( + (W %among% "p" | Y %among% "x") | + Y %among% "x" & W %among% "p" +) |> eval() |> formula_to_expression() |> evaluate_expression(assignment) + + +(W %among% "p" | Y %among% "x") + + Y %among% "x" & W %among% "p" + + +e1 <- (W %among% "p" | Y %among% "x") +e2 <- Y %among% "x" & W %among% "p" + +e1 +e2 + +e1 | e2 + + + + assignment + + + (W %among% "p" | Y %among% "x" | + Y %among% "x" & W %among% "p") + + diff --git a/tests/testthat/test_CnfFormula_simplify.R b/tests/testthat/test_CnfFormula_simplify.R index fae8fe3f9..d59fcf739 100644 --- a/tests/testthat/test_CnfFormula_simplify.R +++ b/tests/testthat/test_CnfFormula_simplify.R @@ -68,7 +68,6 @@ test_that("CnfFormula Regression Tests", { paste(capture.output(print(assignment)), collapse = "\n"), deparse1(simplified) )) - } dti <- as.data.table(stats)