From 11b3aaefc08a7dadd171aaa3b85f990bfd8fa77a Mon Sep 17 00:00:00 2001 From: mb706 Date: Mon, 9 Sep 2024 00:27:38 +0200 Subject: [PATCH] some more edgecases --- R/CnfFormula.R | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/R/CnfFormula.R b/R/CnfFormula.R index d893fbb7d..0d0b94f78 100644 --- a/R/CnfFormula.R +++ b/R/CnfFormula.R @@ -604,6 +604,22 @@ simplify_cnf = function(entries, universe) { if (do_sse || do_sse_reverse) { + if (length(new_entry) == 1) { + # we have a unit clause now + + # It could happen that we eliminate the entry further, in which + # case units[[]] would get stale, but then we return_false anyway. + units[[names(new_entry)]] = new_entry[[1]] + can_simplify = TRUE # do unit elimination all over again + ## TODO: we could probably make this more efficient by only unit-eliminating the terms that are new + } + + if (!length(new_entry)) { + # we have a contradiction now + # Maybe this could happen if we SS-Eliminate multiple symbols from a clause in a row. + return(return_false) + } + # What can have happened now is that the newly created element can eliminate other elements. # If it can eliminate the current element i, that means it is a subset of ei, which only happens if ej\s is a subset of ei\s. However, in that case, we always want to keep element i. # We therefore only need to loop up to i - 1. @@ -618,13 +634,6 @@ simplify_cnf = function(entries, universe) { eliminated[[k]] = TRUE } } - - if (length(new_entry) == 1) { - # we have a unit clause now - units[[names(new_entry)]] = new_entry[[1]] - can_simplify = TRUE # do unit elimination all over again - ## TODO: we could probably make this more efficient by only unit-eliminating the terms that are new - } next } }