From 075db7ec126b616fdd6bdeaaaff2c097afe3e3da Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Mon, 11 Aug 2025 23:23:31 +0900 Subject: [PATCH 1/6] fix (lib/muhfl_prover): delete the options for rethfl The deleted options are the ones that are not supported by the current rethfl. Moreover, it doesn't seem to be a good design to support these options. --- lib/muhfl_prover/muhfl_prover.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/lib/muhfl_prover/muhfl_prover.ml b/lib/muhfl_prover/muhfl_prover.ml index e1b1605..3b97aa7 100644 --- a/lib/muhfl_prover/muhfl_prover.ml +++ b/lib/muhfl_prover/muhfl_prover.ml @@ -404,22 +404,20 @@ module KatsuraSolver : BackendSolver = struct Deferred.return path in path ) - - let solver_command hes_path solver_options stop_if_intractable will_try_weak_subtype remove_disjunction_only remove_temporary_files = + + + let solver_command hes_path solver_options will_try_weak_subtype remove_disjunction_only = let solver_path = get_katsura_solver_path () in Array.of_list ( - solver_path :: ["--solve-dual=auto-conservative"] @ + solver_path :: (if solver_options.no_disprove then ["--no-disprove"] else []) @ (List.filter_map (fun x -> x) [ (if solver_options.no_backend_inlining then Some "--no-inlining" else None); (match solver_options.backend_solver with None -> None | Some s -> Some ("--solver=" ^ s)); - (if stop_if_intractable then Some "--stop-if-intractable" else None); (if will_try_weak_subtype then Some "--mode-burn-et-al" else None); (if solver_options.backend_options <> "" then Some solver_options.backend_options else None); - (if remove_disjunction_only then Some "--stop-if-tractable" else None); - (if remove_disjunction_only then Some "--remove-disjunctions-if-intractable" else None); - (if remove_temporary_files then Some "--remove-temporary-files" else None) + (if remove_disjunction_only then Some "--remove-disjunction" else None); ] ) @ [hes_path] @@ -466,7 +464,7 @@ module KatsuraSolver : BackendSolver = struct save_hes_to_file hes (if debug_context.mode = "prover" && solve_options.approx_parameter.add_arg_coe1 <> 0 && solve_options.approx_parameter.lexico_pair_number = 1 then solve_options.replacer else "") debug_context solve_options.with_usage_analysis solve_options.with_partial_analysis solve_options.no_temp_files >>= (fun path -> let debug_context = { debug_context with temp_file = path } in - let command = solver_command path solve_options stop_if_intractable will_try_weak_subtype stop_if_tractable !Solve_options.remove_temporary_files in + let command = solver_command path solve_options will_try_weak_subtype true (* remove_disjunction *) in if solve_options.dry_run then failwith @@ "DRY RUN (" ^ show_debug_context debug_context ^ ") / command: " ^ (Array.to_list command |> String.concat " "); run_command_with_timeout solve_options.timeout command (Some debug_context.mode) >>| (fun (status_code, elapsed, stdout, stderr) -> From 560b27356046cdb4b6e3a5d380cc5fc578761425 Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Mon, 11 Aug 2025 23:59:44 +0900 Subject: [PATCH 2/6] fix (muhfl_prover): change the type of BackendSolver.run Now - stop_if_tractable - stop_if_intractable are removed. Instead there's a boolean flag named rethfl_remove_disjunction --- lib/muhfl_prover/muhfl_prover.ml | 59 ++++++++++++++++---------------- 1 file changed, 29 insertions(+), 30 deletions(-) diff --git a/lib/muhfl_prover/muhfl_prover.ml b/lib/muhfl_prover/muhfl_prover.ml index 3b97aa7..4da71e8 100644 --- a/lib/muhfl_prover/muhfl_prover.ml +++ b/lib/muhfl_prover/muhfl_prover.ml @@ -92,7 +92,7 @@ type extra_status = | ExStatusTractable module type BackendSolver = sig - val run : options -> debug_context -> Hfl.Type.simple_ty Hflz.hes -> bool -> bool -> bool -> bool -> (Status.t * extra_status option) Deferred.t + val run : options -> debug_context -> Hfl.Type.simple_ty Hflz.hes -> bool -> bool -> bool -> (Status.t * extra_status option) Deferred.t end module FptProverRecLimitSolver : BackendSolver = struct @@ -101,7 +101,7 @@ module FptProverRecLimitSolver : BackendSolver = struct | None -> failwith "Please set environment variable `first_order_solver_path`" | Some s -> s - let run option _debug_context (hes : 'a Hflz.hes) with_par _ _ _ = + let run option _debug_context (hes : 'a Hflz.hes) with_par _will_try_weak_subtype _rethfl_remove_disjunction = let solver_path = get_first_order_solver_path () in let debug_output = match option.log_level with @@ -322,7 +322,7 @@ module MochiSolver : BackendSolver = struct Status.Fail, None ) - let run solve_options (debug_context: debug_context) hes _ _ _ _ = + let run solve_options (debug_context: debug_context) hes _with_par _will_try_weak_subtype _rethfl_remove_disjunction = save_hes_to_file hes debug_context.mode debug_context solve_options.no_temp_files >>= (fun path -> let debug_context = { debug_context with temp_file = path } in @@ -460,11 +460,11 @@ module KatsuraSolver : BackendSolver = struct end ) - let run solve_options (debug_context: debug_context) hes _ stop_if_intractable will_try_weak_subtype stop_if_tractable = + let run solve_options (debug_context: debug_context) hes _with_par will_try_weak_subtype rethfl_remove_disjunction = save_hes_to_file hes (if debug_context.mode = "prover" && solve_options.approx_parameter.add_arg_coe1 <> 0 && solve_options.approx_parameter.lexico_pair_number = 1 then solve_options.replacer else "") debug_context solve_options.with_usage_analysis solve_options.with_partial_analysis solve_options.no_temp_files >>= (fun path -> let debug_context = { debug_context with temp_file = path } in - let command = solver_command path solve_options will_try_weak_subtype true (* remove_disjunction *) in + let command = solver_command path solve_options will_try_weak_subtype rethfl_remove_disjunction in if solve_options.dry_run then failwith @@ "DRY RUN (" ^ show_debug_context debug_context ^ ") / command: " ^ (Array.to_list command |> String.concat " "); run_command_with_timeout solve_options.timeout command (Some debug_context.mode) >>| (fun (status_code, elapsed, stdout, stderr) -> @@ -528,7 +528,7 @@ module IwayamaSolver : BackendSolver = struct | Not_found -> failwith @@ "not matched" ) - let run solve_options debug_context hes _ _ _ _ = + let run solve_options debug_context hes _with_par _will_try_weak_subtype _rethfl_remove_disjunction = let path = save_hes_to_file hes debug_context solve_options.no_temp_files in let debug_context = { debug_context with temp_file = path } in let command = solver_command path solve_options in @@ -581,7 +581,7 @@ module SuzukiSolver : BackendSolver = struct | Not_found -> failwith @@ "not matched" ) - let run solve_options debug_context hes _ _ _ _ = + let run solve_options debug_context hes _with_par _will_try_weak_subtype _rethfl_remove_disjunction = let path = save_hes_to_file hes debug_context solve_options.no_temp_files in let debug_context = { debug_context with temp_file = path } in let command = solver_command path solve_options in @@ -597,7 +597,7 @@ let is_first_order_hes hes = |> (fun hes -> Hflz_util.merge_entry_rule hes) |> List.for_all (fun { Hflz.var; _} -> Hfl.Type.order var.ty <= 1) -let solve_onlynu_onlyforall solve_options debug_context hes with_par stop_if_intractable will_try_weak_subtype stop_if_tractable = +let solve_onlynu_onlyforall solve_options debug_context hes with_par will_try_weak_subtype rethfl_remove_disjunction = let run = if is_first_order_hes hes && solve_options.first_order_solver = Some FptProverRecLimit then ( FptProverRecLimitSolver.run @@ -608,7 +608,7 @@ let solve_onlynu_onlyforall solve_options debug_context hes with_par stop_if_int | Suzuki -> SuzukiSolver.run | Mochi -> MochiSolver.run ) in - run solve_options debug_context hes with_par stop_if_intractable will_try_weak_subtype stop_if_tractable >>| (fun s -> (s, debug_context)) + run solve_options debug_context hes with_par will_try_weak_subtype rethfl_remove_disjunction >>| (fun s -> (s, debug_context)) let is_nu_only_tractable hes = let path = Manipulate.Print_syntax.MachineReadable.save_hes_to_file ~without_id:false true hes in @@ -962,20 +962,23 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ If one of instantiation of existential variables has returned "valid," then result of current iteration is "valid." *) let pass_result = (fun ((s, _), d) -> (s, d)) in - let (solvers: (Status.t * debug_context) Deferred.t list list) = + let (solvers: (Status.t * debug_context) Deferred.t list list) = + let remove_disjunction = solve_options.remove_disjunctions || solve_options.only_remove_disjunctions in + let debug_context_ = {debug_context_ with remove_disjunctions = remove_disjunction} in match solve_options.backend_solver with | None -> List.map (fun (nu_only_hes, exists_assignment, hflz_info) -> let debug_context_ = {debug_context_ with hflz_info} in + let hoice = if remove_disjunction then "hoice_rd" else "hoice" in + let z3 = if remove_disjunction then "z3_rd" else "z3" in [ solve_onlynu_onlyforall { solve_options with backend_solver = Some "hoice" } - ({ debug_context_ with backend_solver = Some "hoice"; solved_by = "hoice"; exists_assignment = Some exists_assignment }) + ({ debug_context_ with backend_solver = Some "hoice"; solved_by = hoice; exists_assignment = Some exists_assignment }) nu_only_hes false - (if solve_options.only_remove_disjunctions then (* do not solve echc *) true else false) - false false + remove_disjunction >>| (fun ((s, ex), d) -> match ex with | Some ExStatusIntractable -> (s, {d with solved_by = "pcsat"}) @@ -983,23 +986,21 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ ); solve_onlynu_onlyforall { solve_options with backend_solver = Some "z3" } - ({ debug_context_ with backend_solver = Some "z3"; solved_by = "z3"; exists_assignment = Some exists_assignment }) + ({ debug_context_ with backend_solver = Some "z3"; solved_by = z3; exists_assignment = Some exists_assignment }) nu_only_hes false - true (* if the formula is intractable in katsura-solver, stop either of the two solving processes to save computational resources *) - false false + remove_disjunction >>| pass_result ] @ (if solve_options.try_weak_subtype then [ solve_onlynu_onlyforall { solve_options with backend_solver = Some "hoice" } - ({ debug_context_ with backend_solver = Some "hoice"; solved_by = "hoice_weak_subtype"; exists_assignment = Some exists_assignment }) + ({ debug_context_ with backend_solver = Some "hoice"; solved_by = hoice ^ "_weak_subtype"; exists_assignment = Some exists_assignment }) nu_only_hes false true - true - false + remove_disjunction >>| pass_result >>| (fun (s, d) -> match s with @@ -1008,12 +1009,11 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ ); solve_onlynu_onlyforall { solve_options with backend_solver = Some "z3" } - ({ debug_context_ with backend_solver = Some "z3"; solved_by = "z3_weak_subtype"; exists_assignment = Some exists_assignment }) + ({ debug_context_ with backend_solver = Some "z3"; solved_by = z3 ^ "_weak_subtype"; exists_assignment = Some exists_assignment }) nu_only_hes false true - true - false + remove_disjunction >>| pass_result >>| (fun (s, d) -> match s with @@ -1021,15 +1021,15 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ | _ -> (s, d) ) ] else []) - @ (if solve_options.remove_disjunctions || solve_options.only_remove_disjunctions then [ + (* try both remove_disjunction and ECHC (i.e. pc sat)*) + @ (if solve_options.remove_disjunctions && not solve_options.only_remove_disjunctions then [ solve_onlynu_onlyforall { solve_options with backend_solver = Some "hoice" } - ({ debug_context_ with backend_solver = Some "hoice"; solved_by = "hoice_rd"; exists_assignment = Some exists_assignment; remove_disjunctions = solve_options.remove_disjunctions }) + ({ debug_context_ with backend_solver = Some "hoice"; solved_by = "hoice"; exists_assignment = Some exists_assignment; remove_disjunctions = solve_options.remove_disjunctions }) nu_only_hes false false false - true >>| pass_result >>| (fun (s, d) -> match s with @@ -1039,12 +1039,11 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ ); solve_onlynu_onlyforall { solve_options with backend_solver = Some "z3" } - ({ debug_context_ with backend_solver = Some "z3"; solved_by = "z3_rd"; exists_assignment = Some exists_assignment; remove_disjunctions = solve_options.remove_disjunctions }) + ({ debug_context_ with backend_solver = Some "z3"; solved_by = "z3"; exists_assignment = Some exists_assignment; remove_disjunctions = solve_options.remove_disjunctions }) nu_only_hes false false false - true >>| pass_result >>| (fun (s, d) -> match s with @@ -1052,10 +1051,10 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ if solve_options.only_remove_disjunctions then (s, d) else Status.Fail, d | _ -> (s, d) ) - ] else []) + ] else []) ) nu_only_heses - | Some _ -> - List.map (fun (nu_only_hes, _, hflz_info) -> [solve_onlynu_onlyforall solve_options {debug_context_ with hflz_info} nu_only_hes false false false false >>| pass_result]) nu_only_heses in + | Some _ -> (*TODO: Why is this ignored??? *) + List.map (fun (nu_only_hes, _, hflz_info) -> [solve_onlynu_onlyforall solve_options {debug_context_ with hflz_info} nu_only_hes false false remove_disjunction >>| pass_result]) nu_only_heses in let (is_valid : (Status.t * debug_context list) list Ivar.t) = Ivar.create () in let deferred_is_valid = Ivar.read is_valid in let (deferred_all : (Status.t * debug_context list) list Deferred.t) = From d99b976cd260542d2bbaf296fa5a44747027e3ac Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Tue, 12 Aug 2025 00:32:16 +0900 Subject: [PATCH 3/6] fix (muhfl_prover): remove extra_status This extra information was reported by a modified version of rethfl and we do not need that anymore --- lib/muhfl_prover/muhfl_prover.ml | 92 ++++++++++---------------------- 1 file changed, 28 insertions(+), 64 deletions(-) diff --git a/lib/muhfl_prover/muhfl_prover.ml b/lib/muhfl_prover/muhfl_prover.ml index 4da71e8..17716b1 100644 --- a/lib/muhfl_prover/muhfl_prover.ml +++ b/lib/muhfl_prover/muhfl_prover.ml @@ -87,12 +87,8 @@ let show_debug_contexts debugs = debugs |> String.concat ", " -type extra_status = - | ExStatusIntractable - | ExStatusTractable - module type BackendSolver = sig - val run : options -> debug_context -> Hfl.Type.simple_ty Hflz.hes -> bool -> bool -> bool -> (Status.t * extra_status option) Deferred.t + val run : options -> debug_context -> Hfl.Type.simple_ty Hflz.hes -> bool -> bool -> bool -> Status.t Deferred.t end module FptProverRecLimitSolver : BackendSolver = struct @@ -121,15 +117,15 @@ module FptProverRecLimitSolver : BackendSolver = struct let reg = Str.regexp "^Verification Result: \\([a-z]+\\)$" in try ignore @@ Str.search_forward reg stdout 0; - Status.of_string @@ Str.matched_group 1 stdout, None + Status.of_string @@ Str.matched_group 1 stdout with | Not_found -> log_string "Failure in parsing output"; - Status.Fail, None + Status.Fail end | Error code -> begin log_string @@ "Error status (" ^ Unix_command.show_code (Error code) ^ ")"; - Status.Fail, None + Status.Fail end ) end @@ -232,47 +228,46 @@ module SolverCommon = struct type solver_error_category = S_ParseError | S_TypeError | S_OtherError let parse_results_inner (exit_status, stdout, stderr) debug_context elapsed no_temp_files status_parser = - let res, tmp_res, log_message, extra_status = + let res, tmp_res, log_message = match exit_status with | Ok () -> begin - let status, extra_status = status_parser stdout in + let status = status_parser stdout in status, ( match status with | Status.Valid -> TValid | Invalid -> TInvalid | _ -> TUnknown), - "Parsed status: " ^ Status.string_of status ^ " " ^ (show_debug_context debug_context), extra_status + "Parsed status: " ^ Status.string_of status ^ " " ^ (show_debug_context debug_context) end | Error (`Exit_non_zero 2) -> begin Status.Fail, TTerminated, - "Error code 2 " ^ (show_debug_context debug_context), None + "Error code 2 " ^ (show_debug_context debug_context) end | Error (`Exit_non_zero 127) -> begin Status.Fail, TTerminated, - "Command not found " ^ (show_debug_context debug_context), None + "Command not found " ^ (show_debug_context debug_context) end | Error (`Exit_non_zero 143) -> begin Status.Unknown, TTerminated, - "SIGTERMed " ^ (show_debug_context debug_context), None + "SIGTERMed " ^ (show_debug_context debug_context) end | Error (`Exit_non_zero 128) -> begin (* SIGTERMed. (why 128?) *) Status.Unknown, TTerminated, - "SIGTERMed (128) " ^ (show_debug_context debug_context), None + "SIGTERMed (128) " ^ (show_debug_context debug_context) end | Error (`Exit_non_zero 124) -> begin Status.Unknown, TUnknown, - "Timeout " ^ (show_debug_context debug_context), None + "Timeout " ^ (show_debug_context debug_context) end | Error code -> begin Status.Unknown, TError, - "Error status (" ^ Unix_command.show_code (Error code) ^ ")", None + "Error status (" ^ Unix_command.show_code (Error code) ^ ")" end in if not no_temp_files then output_post_debug_info tmp_res elapsed stdout stderr debug_context; - if extra_status = None then message_string ~header:"Result" @@ Status.string_of res ^ " / " ^ log_message; - res, extra_status + res let run_command_with_timeout ?env timeout command mode = unix_system ?env timeout command mode @@ -314,12 +309,12 @@ module MochiSolver : BackendSolver = struct try ignore @@ Str.search_forward reg stdout 0; match Str.matched_group 1 stdout with - | "Safe!" -> Valid, None - | "Unsafe!" -> Invalid, None + | "Safe!" -> Valid + | "Unsafe!" -> Invalid | _ -> assert false with | Not_found -> - Status.Fail, None + Status.Fail ) let run solve_options (debug_context: debug_context) hes _with_par _will_try_weak_subtype _rethfl_remove_disjunction = @@ -429,35 +424,9 @@ module KatsuraSolver : BackendSolver = struct try ignore @@ Str.search_forward reg stdout 0; let status = Status.of_string @@ Str.matched_group 2 stdout in - let ex = - try - let reg = Str.regexp "^Tractability: \\([a-z]+\\)$" in - ignore @@ Str.search_forward reg stdout 0; - match Str.matched_group 1 stdout with - | "tractable" -> Some ExStatusTractable - | "intractable" -> Some ExStatusIntractable - | _ -> None - with - | Not_found -> None - in - status, ex + status with - | Not_found -> begin - let reg = Str.regexp "^intractable$" in - try - ignore @@ Str.search_forward reg stdout 0; - message_string ~header:"Result" @@ "stop becasuse intractable (" ^ (show_debug_context debug_context) ^ ")"; - Status.Fail, Some ExStatusIntractable - with - | Not_found -> begin - let reg = Str.regexp "^tractable$" in - try - ignore @@ Str.search_forward reg stdout 0; - message_string ~header:"Result" @@ "stop becasuse tractable (" ^ (show_debug_context debug_context) ^ ")"; - Status.Fail, Some ExStatusTractable - with Not_found -> failwith @@ "not matched" - end - end + | Not_found -> Status.Fail ) let run solve_options (debug_context: debug_context) hes _with_par will_try_weak_subtype rethfl_remove_disjunction = @@ -490,7 +459,7 @@ module KatsuraSolver : BackendSolver = struct | _ -> try parse_results (status_code, stdout, stderr) debug_context elapsed solve_options.no_temp_files - with _ -> Status.Unknown, None) + with _ -> Status.Unknown) ) end @@ -523,7 +492,7 @@ module IwayamaSolver : BackendSolver = struct let reg = Str.regexp "^Verification Result:\n\\( \\)*\\([a-zA-Z]+\\)\nLoop Count:$" in try ignore @@ Str.search_forward reg stdout 0; - Status.of_string @@ Str.matched_group 2 stdout, None + Status.of_string @@ Str.matched_group 2 stdout with | Not_found -> failwith @@ "not matched" ) @@ -536,7 +505,7 @@ module IwayamaSolver : BackendSolver = struct >>| (fun (status_code, elapsed, stdout, stderr) -> try parse_results (status_code, stdout, stderr) debug_context elapsed solve_options.no_temp_files - with _ -> Status.Unknown, None) + with _ -> Status.Unknown) end module SuzukiSolver : BackendSolver = struct @@ -576,7 +545,7 @@ module SuzukiSolver : BackendSolver = struct | "Sat" -> "valid" | "UnSat" -> "invalid" | _ -> failwith @@ "Illegal status string1 (" ^ s ^ ")" - ), None + ) with | Not_found -> failwith @@ "not matched" ) @@ -589,7 +558,7 @@ module SuzukiSolver : BackendSolver = struct >>| (fun (status_code, elapsed, stdout, stderr) -> try parse_results (status_code, stdout, stderr) debug_context elapsed solve_options.no_temp_files - with _ -> Status.Unknown, None) + with _ -> Status.Unknown) end let is_first_order_hes hes = @@ -961,7 +930,6 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ If either of hoice and z3 returned some result other than "fail," then the result of the current iteration is the result returned by the solvers. If one of instantiation of existential variables has returned "valid," then result of current iteration is "valid." *) - let pass_result = (fun ((s, _), d) -> (s, d)) in let (solvers: (Status.t * debug_context) Deferred.t list list) = let remove_disjunction = solve_options.remove_disjunctions || solve_options.only_remove_disjunctions in let debug_context_ = {debug_context_ with remove_disjunctions = remove_disjunction} in @@ -979,11 +947,12 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ false false remove_disjunction - >>| (fun ((s, ex), d) -> + (*>>| (fun ((s, ex), d) -> match ex with | Some ExStatusIntractable -> (s, {d with solved_by = "pcsat"}) | _ -> (s, d) - ); + ) )* *) + ; solve_onlynu_onlyforall { solve_options with backend_solver = Some "z3" } ({ debug_context_ with backend_solver = Some "z3"; solved_by = z3; exists_assignment = Some exists_assignment }) @@ -991,7 +960,6 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ false false remove_disjunction - >>| pass_result ] @ (if solve_options.try_weak_subtype then [ solve_onlynu_onlyforall @@ -1001,7 +969,6 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ false true remove_disjunction - >>| pass_result >>| (fun (s, d) -> match s with | Status.Unknown -> Status.Fail, d @@ -1014,7 +981,6 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ false true remove_disjunction - >>| pass_result >>| (fun (s, d) -> match s with | Status.Unknown -> Status.Fail, d @@ -1030,7 +996,6 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ false false false - >>| pass_result >>| (fun (s, d) -> match s with | Status.Unknown -> @@ -1044,7 +1009,6 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ false false false - >>| pass_result >>| (fun (s, d) -> match s with | Status.Unknown -> @@ -1054,7 +1018,7 @@ let rec mu_elim_solver ?(cached_formula=None) iter_count (solve_options : Solve_ ] else []) ) nu_only_heses | Some _ -> (*TODO: Why is this ignored??? *) - List.map (fun (nu_only_hes, _, hflz_info) -> [solve_onlynu_onlyforall solve_options {debug_context_ with hflz_info} nu_only_hes false false remove_disjunction >>| pass_result]) nu_only_heses in + List.map (fun (nu_only_hes, _, hflz_info) -> [solve_onlynu_onlyforall solve_options {debug_context_ with hflz_info} nu_only_hes false false remove_disjunction]) nu_only_heses in let (is_valid : (Status.t * debug_context list) list Ivar.t) = Ivar.create () in let deferred_is_valid = Ivar.read is_valid in let (deferred_all : (Status.t * debug_context list) list Deferred.t) = From b95c0be8275eff43a74c35673d9470f5b4fe36f9 Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Wed, 13 Aug 2025 17:01:47 +0900 Subject: [PATCH 4/6] refactor (muhfl_prover): don't invoke rethfl to check tractability Current rethfly does not have the option --tractable-check-only, so we should not invoke rethfl for this. Moreover, this functionallity is already provided by the hfl library --- lib/muhfl_prover/muhfl_prover.ml | 82 ++++++++++++-------------------- 1 file changed, 30 insertions(+), 52 deletions(-) diff --git a/lib/muhfl_prover/muhfl_prover.ml b/lib/muhfl_prover/muhfl_prover.ml index 17716b1..5c45966 100644 --- a/lib/muhfl_prover/muhfl_prover.ml +++ b/lib/muhfl_prover/muhfl_prover.ml @@ -579,25 +579,7 @@ let solve_onlynu_onlyforall solve_options debug_context hes with_par will_try_we ) in run solve_options debug_context hes with_par will_try_weak_subtype rethfl_remove_disjunction >>| (fun s -> (s, debug_context)) -let is_nu_only_tractable hes = - let path = Manipulate.Print_syntax.MachineReadable.save_hes_to_file ~without_id:false true hes in - let solver_path = get_katsura_solver_path () in - let stdout_name = Hflmc2_util.gen_temp_filename "/tmp/" "_stdout.tmp" in - let command = "\"" ^ solver_path ^ "\" --tractable-check-only \"" ^ path ^ "\" > " ^ stdout_name in - log_string @@ "command: " ^ command; - Unix.system command - >>= (fun _ -> - Reader.file_lines stdout_name >>| (fun stdout_lines -> - match (List.rev stdout_lines) with - | last_line::_ -> begin - match last_line with - | "tractable" -> true - | "intractable" -> false - | _ -> failwith @@ "run_tractable_check: Illegal result (" ^ last_line ^ ")" - end - | _ -> failwith @@ "run_tractable_check: No result" - ) - ) +let is_nu_only_tractable hes = Hfl.Trans.RemoveDisjunction.check hes let count_exists hes = let entry = Hflz.top_formula_of hes in @@ -622,23 +604,19 @@ let should_instantiate_exists original_hes z3_path = let hes_ = Hflz_mani.encode_body_exists coe1 coe2 original_hes Hfl.IdMap.empty [] false in let hes_ = Hflz_mani.elim_mu_with_rec hes_ coe1 coe2 lexico_pair_number Hfl.IdMap.empty false [] z3_path in if not @@ Hflz.is_nuonly hes_ then failwith "elim_mu"; - is_nu_only_tractable hes_ - >>= (fun t_prover -> - let dual_hes = Hflz_mani.get_dual_hes original_hes in - let exists_count_disprover = count_exists dual_hes in - let dual_hes = Hflz_mani.encode_body_exists coe1 coe2 dual_hes Hfl.IdMap.empty [] false in - let dual_hes = Hflz_mani.elim_mu_with_rec dual_hes coe1 coe2 lexico_pair_number Hfl.IdMap.empty false [] z3_path in - if not @@ Hflz.is_nuonly dual_hes then failwith "elim_mu"; - is_nu_only_tractable dual_hes - >>| (fun t_disprover -> - let should_instantiate = - (not t_prover || not t_disprover) && - exists_count_prover <= existential_quantifier_number_threthold && exists_count_disprover <= existential_quantifier_number_threthold in - log_string @@ "should_instantiate_exists: " ^ (string_of_bool should_instantiate) ^ " (tractable_prover=" ^ string_of_bool t_prover ^ ", tractable_disprover=" ^ string_of_bool t_disprover ^ ",exists_count_prover=" ^ string_of_int exists_count_prover ^ ", exists_count_disprover=" ^ string_of_int exists_count_disprover ^ ")"; - should_instantiate - ) - ) - + let t_prover = is_nu_only_tractable hes_ in + let dual_hes = Hflz_mani.get_dual_hes original_hes in + let exists_count_disprover = count_exists dual_hes in + let dual_hes = Hflz_mani.encode_body_exists coe1 coe2 dual_hes Hfl.IdMap.empty [] false in + let dual_hes = Hflz_mani.elim_mu_with_rec dual_hes coe1 coe2 lexico_pair_number Hfl.IdMap.empty false [] z3_path in + if not @@ Hflz.is_nuonly dual_hes then failwith "elim_mu"; + let t_disprover = is_nu_only_tractable dual_hes in + let should_instantiate = + (not t_prover || not t_disprover) && + exists_count_prover <= existential_quantifier_number_threthold && exists_count_disprover <= existential_quantifier_number_threthold in + log_string @@ "should_instantiate_exists: " ^ (string_of_bool should_instantiate) ^ " (tractable_prover=" ^ string_of_bool t_prover ^ ", tractable_disprover=" ^ string_of_bool t_disprover ^ ",exists_count_prover=" ^ string_of_int exists_count_prover ^ ", exists_count_disprover=" ^ string_of_int exists_count_disprover ^ ")"; + should_instantiate + let count_occuring (*id_type_map:(unit Hflmc2_syntax.Id.t, Manipulate.Hflz_util.variable_type, Hflmc2_syntax.IdMap.Key.comparator_witness) Base.Map.t*) hes s = let open Hfl in (* let ids = @@ -1194,25 +1172,25 @@ let check_validity solve_options (hes : 'a Hflz.hes) cont = { solve_options with approx_parameter = initial_param }, iter_count_offset in let dresult = + let solve_options = (if solve_options.auto_existential_quantifier_instantiation && not solve_options.assign_values_for_exists_at_first_iteration then - should_instantiate_exists hes solve_options.z3_path - >>| (fun f -> - if f then { solve_options with assign_values_for_exists_at_first_iteration = true } else solve_options - ) + if should_instantiate_exists hes solve_options.z3_path + then { solve_options with assign_values_for_exists_at_first_iteration = true } + else solve_options else - return solve_options) - >>= (fun solve_options -> - if solve_options.always_approximate then - check_validity_full_entry solve_options hes iter_count_offset - else begin - if Hflz.is_nuonly hes then - solve_onlynu_onlyforall_with_schedule solve_options hes - else if Hflz.is_muonly hes then - solve_onlynu_onlyforall_with_schedule solve_options (Hflz_mani.get_dual_hes hes) - >>| (fun (status_pair, i) -> (Status.flip status_pair, i)) - else check_validity_full_entry solve_options hes iter_count_offset + solve_options) + in + if solve_options.always_approximate then + check_validity_full_entry solve_options hes iter_count_offset + else begin + if Hflz.is_nuonly hes then + solve_onlynu_onlyforall_with_schedule solve_options hes + else if Hflz.is_muonly hes then + solve_onlynu_onlyforall_with_schedule solve_options (Hflz_mani.get_dual_hes hes) + >>| (fun (status_pair, i) -> (Status.flip status_pair, i)) + else check_validity_full_entry solve_options hes iter_count_offset end - ) in + in upon dresult ( fun (result, info) -> cont (result, info); From b7b15d28301a0405d004af34beebc318f5572335 Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Wed, 13 Aug 2025 17:05:15 +0900 Subject: [PATCH 5/6] fix (muhfl_prover): show debug context when error code is returned The other cases always shows debug context, so to be consistent we should show it in this case as well --- lib/muhfl_prover/muhfl_prover.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/muhfl_prover/muhfl_prover.ml b/lib/muhfl_prover/muhfl_prover.ml index 5c45966..2841fd0 100644 --- a/lib/muhfl_prover/muhfl_prover.ml +++ b/lib/muhfl_prover/muhfl_prover.ml @@ -262,7 +262,7 @@ module SolverCommon = struct end | Error code -> begin Status.Unknown, TError, - "Error status (" ^ Unix_command.show_code (Error code) ^ ")" + "Error status (" ^ Unix_command.show_code (Error code) ^ ")" ^ (show_debug_context debug_context) end in if not no_temp_files then output_post_debug_info tmp_res elapsed stdout stderr debug_context; From 6dadb5f3b26d81e9f960bf4040a0c2145a28c04b Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Wed, 13 Aug 2025 17:19:24 +0900 Subject: [PATCH 6/6] refactor: katsura solver -> rethfl --- benchmark/run_muapprox_katsura.sh | 2 +- benchmark/run_muapprox_katsura_no_options.sh | 2 +- benchmark/run_muapprox_katsura_replacer.sh | 2 +- lib/muhfl_prover/muhfl_prover.ml | 12 ++++++------ lib/muhfl_prover/solve_options.ml | 8 ++++---- lib/options.ml | 8 ++++---- run_muhfl.sh | 4 ++-- 7 files changed, 19 insertions(+), 19 deletions(-) diff --git a/benchmark/run_muapprox_katsura.sh b/benchmark/run_muapprox_katsura.sh index 0b8ee70..a33c11f 100755 --- a/benchmark/run_muapprox_katsura.sh +++ b/benchmark/run_muapprox_katsura.sh @@ -5,6 +5,6 @@ SCRIPT_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &> /dev/null && pwd)" --remove-disjunction \ --agg \ --timeout=300 \ - --solver katsura --verbose "${@:2}" \ + --solver rethfl --verbose "${@:2}" \ "$1" > /tmp/stdout_1.txt 2> /tmp/stderr_1.txt # --replacer="$(basename "$1" .in)" diff --git a/benchmark/run_muapprox_katsura_no_options.sh b/benchmark/run_muapprox_katsura_no_options.sh index 1392a66..f4604ea 100755 --- a/benchmark/run_muapprox_katsura_no_options.sh +++ b/benchmark/run_muapprox_katsura_no_options.sh @@ -3,6 +3,6 @@ SCRIPT_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &> /dev/null && pwd)" "$(dirname -- "$SCRIPT_DIR")"/_build/default/bin/muapprox_main.exe \ --try-weak \ --timeout=300 \ - --solver katsura --verbose "${@:2}" \ + --solver rethfl --verbose "${@:2}" \ "$1" > /tmp/stdout_1.txt 2> /tmp/stderr_1.txt # --replacer="$(basename "$1" .in)" diff --git a/benchmark/run_muapprox_katsura_replacer.sh b/benchmark/run_muapprox_katsura_replacer.sh index 470513f..0ec7d3a 100755 --- a/benchmark/run_muapprox_katsura_replacer.sh +++ b/benchmark/run_muapprox_katsura_replacer.sh @@ -1,5 +1,5 @@ #!/bin/bash # OLD # /opt/home2/git/muapprox/_build/default/bin/muapprox_main.exe \ -# --no-au --solver katsura --no-simplify --replacer="$(basename "$1" .in)" --verbose "${@:2}" \ +# --no-au --solver rethfl --no-simplify --replacer="$(basename "$1" .in)" --verbose "${@:2}" \ # "$1" > /tmp/stdout_1.txt 2> /tmp/stderr_1.txt diff --git a/lib/muhfl_prover/muhfl_prover.ml b/lib/muhfl_prover/muhfl_prover.ml index 2841fd0..fc705a9 100644 --- a/lib/muhfl_prover/muhfl_prover.ml +++ b/lib/muhfl_prover/muhfl_prover.ml @@ -329,12 +329,12 @@ module MochiSolver : BackendSolver = struct ) end -let get_katsura_solver_path () = - match Stdlib.Sys.getenv_opt "katsura_solver_path" with - | None -> failwith "Please set environment variable `katsura_solver_path`" +let get_rethfl_path () = + match Stdlib.Sys.getenv_opt "rethfl_path" with + | None -> failwith "Please set environment variable `rethfl_path`" | Some s -> s -module KatsuraSolver : BackendSolver = struct +module Rethfl : BackendSolver = struct include SolverCommon let replacer_path () = @@ -402,7 +402,7 @@ module KatsuraSolver : BackendSolver = struct let solver_command hes_path solver_options will_try_weak_subtype remove_disjunction_only = - let solver_path = get_katsura_solver_path () in + let solver_path = get_rethfl_path () in Array.of_list ( solver_path :: (if solver_options.no_disprove then ["--no-disprove"] else []) @ @@ -572,7 +572,7 @@ let solve_onlynu_onlyforall solve_options debug_context hes with_par will_try_we FptProverRecLimitSolver.run ) else ( match solve_options.solver with - | Katsura -> KatsuraSolver.run + | Rethfl -> Rethfl.run | Iwayama -> IwayamaSolver.run | Suzuki -> SuzukiSolver.run | Mochi -> MochiSolver.run diff --git a/lib/muhfl_prover/solve_options.ml b/lib/muhfl_prover/solve_options.ml index 19e1e97..250690d 100644 --- a/lib/muhfl_prover/solve_options.ml +++ b/lib/muhfl_prover/solve_options.ml @@ -1,4 +1,4 @@ -type solver_type = Iwayama | Katsura | Suzuki | Mochi +type solver_type = Iwayama | Rethfl | Suzuki | Mochi type first_order_solver_type = FptProverRecLimit let remove_temporary_files = ref false @@ -54,7 +54,7 @@ type options = let get_solver solver_name = match solver_name with | "iwayama" -> Iwayama - | "katsura" -> Katsura + | "rethfl" -> Rethfl | "suzuki" -> Suzuki | "mochi" -> ((print_endline "In MoCHi solver mode, translation with correct evaluation order is not implemented, so we may output incorrect result or failure"); Mochi) | s -> failwith @@ "unknown solver \"" ^ s ^ "\"" @@ -64,8 +64,8 @@ let get_first_order_solver use_fo_solver = let get_backend_solver s solver = match solver with - | Katsura -> begin - (* backend-solver option is only for katsura-solver *) + | Rethfl-> begin + (* backend-solver option is only for rethfl *) let s = String.trim s in match s with | "" -> None diff --git a/lib/options.ml b/lib/options.ml index 13e2a14..4aca332 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -63,11 +63,11 @@ type params = ; timeout : int [@default 600] (** Timeout for a backend solver *) - ; solver : string [@default "katsura"] - (** Choose background nu-only-HFLz solver. Available: katsura, iwayama, suzuki, mochi *) + ; solver : string [@default "rethfl"] + (** Choose background nu-only-HFLz solver. Available: rethfl, iwayama, suzuki, mochi *) ; backend_solver : string [@default ""] - (** --solver option on the backend solver. (only used in the katsura solver) *) + (** --solver option on the backend solver. (only used in the rethfl) *) ; first_order_solver : bool [@default false] (** If true, use z3 or hoice to solve first-order formulas. If empty (or default), always use a solver for higher-order formulas. *) @@ -121,7 +121,7 @@ type params = (** (old option) Use all variables (not only variables which are occured in arguments of application) to guess a recursion bound to approximate least-fixpoints. (This may (or may not) help Hoice.) *) ; replacer : string [@default ""] - (** (old option) Ad-hoc replacement of approximated forumula (for katsura-solver only) *) + (** (old option) Ad-hoc replacement of approximated forumula (for rethfl only) *) ; auto_existential_quantifier_instantiation : bool [@default false] (** Instantiate existential quantifiers even if instantiation seems to be effective *) diff --git a/run_muhfl.sh b/run_muhfl.sh index dbee74b..2075891 100755 --- a/run_muhfl.sh +++ b/run_muhfl.sh @@ -1,7 +1,7 @@ #!/bin/bash # Options -# --try-weak-subtype: try to solve nuHFL(Z) formulas with the katsura solver with the weak subtyping rules by Burn et al. in parallel +# --try-weak-subtype: try to solve nuHFL(Z) formulas with rethfl with the weak subtyping rules by Burn et al. in parallel # --remove-disjunctions: try to solve nuHFL(Z) formulas with the disjunction removal transformation in parallel # --aggressive-simplification: simplify HFL(Z) formulas # --timeout: timeout for each approximation refinement iteration @@ -12,7 +12,7 @@ PATH=/home/kentotanahashi/hoice/target/release:/home/kentotanahashi/eldarica:/home/katsura/bin:$PATH \ fptprove=/home/kentotanahashi/fptprove \ - katsura_solver_path=/home/kentotanahashi/hflmc2-dev/_build/default/bin/main.exe \ + rethfl_path=/home/kentotanahashi/hflmc2-dev/_build/default/bin/main.exe \ /home/kentotanahashi/muapprox-dev/_build/default/bin/muapprox_main.exe \ --try-weak-subtype --remove-disjunctions --aggressive-simplification --timeout=300 \ "$@"