From 02b8e64e0c49688358be60c9f0f37d63df939f60 Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Sat, 20 Jul 2024 20:45:31 +0900 Subject: [PATCH] remove disjunctions by default We don't want to rely on PCSat, and thus, it is preferable to make an order n nuHFL formula tractable by translating it to an order (n + 1) formula. --- lib/options/rethfl_options.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/options/rethfl_options.ml b/lib/options/rethfl_options.ml index 4f26002..8dbef37 100644 --- a/lib/options/rethfl_options.ml +++ b/lib/options/rethfl_options.ml @@ -60,7 +60,7 @@ type params = (* Preprocess *) ; no_inlining : bool [@default false] (** Disable inlining *) - ; remove_disjunction: bool [@default false] + ; no_remove_disjunction: bool [@default false] (** Remove disjunction *) (* Logging *) @@ -103,7 +103,7 @@ let set_up_params params = set_module_log_level Info params.log_info; set_ref oneshot params.oneshot; set_ref Preprocess.inlining (not params.no_inlining); - set_ref Preprocess.remove_disjunction params.remove_disjunction; + set_ref Preprocess.remove_disjunction (not params.no_remove_disjunction); set_ref Abstraction.max_I params.abst_max_I; set_ref Abstraction.max_ands params.abst_max_ands; set_ref Abstraction.modify_pred_by_guard (not params.abst_no_modify_pred_by_guard);