Add --smt-output-dir option

lib/options/rethfl_options.ml

@@ -29,6 +29,7 @@ module Typing = struct
   let show_refinement      = ref (Obj.magic())
   let mode_burn_et_al      = ref (Obj.magic())
   let no_disprove          = ref (Obj.magic())
+  let smt_output_dir       = ref (Obj.magic())
 end
 
 (******************************************************************************)
@@ -95,6 +96,9 @@ type params =
 
   ; no_disprove: bool [@default false]
     (** Disable disproving*)
+
+  ; smt_output_dir: string option
+    (** Set output dir for smt2 files *)
   }
   [@@deriving cmdliner,show]
 
@@ -112,6 +116,7 @@ let set_up_params params =
   set_ref Typing.show_refinement           params.show_refinement;
   set_ref Typing.mode_burn_et_al           params.mode_burn_et_al;
   set_ref Typing.no_disprove               params.no_disprove;
+  set_ref Typing.smt_output_dir            params.smt_output_dir;
   params.input
 
 (******************************************************************************)

lib/typing/chc_solver.ml

@@ -273,7 +273,11 @@ let save_chc_to_smt2 chcs solver =
     let smt2 = chc2smt2 chcs solver in
     Random.self_init ();
     let r = Random.int 0x10000000 in
-    let file = Printf.sprintf "/tmp/%s-%d.smt2" (name_of_solver solver) r in
+    let base = match !Rethfl_options.Typing.smt_output_dir with
+      | Some x -> x
+      | None -> "/tmp"
+    in
+    let file = Printf.sprintf "%s/%s-%d.smt2" base (name_of_solver solver) r in
     let oc = open_out file in
     Printf.fprintf oc "%s" smt2;
     close_out oc;

lib/typing/smt_solver.ml

@@ -24,7 +24,11 @@ let save_fpl_to_smt2 solver fpl =
     let smt2 = fpl2smt2 solver fpl in
     Random.self_init ();
     let r = Random.int 0x10000000 in
-    let file = Printf.sprintf "/tmp/%s-%d.smt2" (name_of_solver solver) r in
+    let base = match !Rethfl_options.Typing.smt_output_dir with
+      | Some x -> x
+      | None -> "/tmp"
+    in
+    let file = Printf.sprintf "%s/%s-%d.smt2" base (name_of_solver solver) r in
     let oc = open_out file in
     Printf.fprintf oc "%s" smt2;
     close_out oc;