Adapt to the latest rethfl.

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)" 

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)" 

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

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

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 *)

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 \
     "$@"