Remove the options in the js worker

src/bin/js/options_interface.ml

@@ -66,14 +66,6 @@ let get_instantiation_heuristic = function
     | IAuto -> Some Options.IAuto
     | IGreedy -> Some Options.IGreedy
 
-let get_interpretation = function
-  | None -> None
-  | Some m -> match m with
-    | INone -> Some Options.INone
-    | IFirst -> Some Options.IFirst
-    | IEvery -> Some Options.IEvery
-    | ILast -> Some Options.ILast
-
 let get_no_decisions_on = function
   | None -> None
   | Some l ->
@@ -140,9 +132,6 @@ let set_options r =
   set_options_opt Options.set_fm_cross_limit (get_numbers r.fm_cross_limit);
   set_options_opt Options.set_steps_bound r.steps_bound;
 
-  set_options_opt Options.set_interpretation
-    (get_interpretation r.interpretation);
-
   set_options_opt Options.set_output_format
     (get_output_format r.output_format);
   Options.set_infer_output_format

src/bin/js/worker_example.ml

@@ -68,7 +68,6 @@ let solve () =
      debug = Some true;
      verbose = Some true;
      answers_with_loc = Some false;
-     interpretation = Some IEvery;
      sat_solver = Some Worker_interface.Tableaux;
      unsat_core = Some true;
     } in

src/bin/js/worker_interface.ml

@@ -112,7 +112,6 @@ let sat_solver_encoding =
   ]
 
 type instantiation_heuristic =  INormal | IAuto | IGreedy
-type interpretation = INone | IFirst | IEvery | ILast
 
 let instantiation_heuristic_encoding =
   union [
@@ -133,30 +132,6 @@ let instantiation_heuristic_encoding =
       (fun () -> IGreedy);
   ]
 
-let interpretation_encoding =
-  union [
-    case(Tag 1)
-      ~title:"INone"
-      (constant "INone")
-      (function INone -> Some () | _ -> None)
-      (fun () -> INone);
-    case(Tag 2)
-      ~title:"IFirst"
-      (constant "IFirst")
-      (function IFirst -> Some () | _ -> None)
-      (fun () -> IFirst);
-    case(Tag 3)
-      ~title:"IEvery"
-      (constant "IEvery")
-      (function IEvery -> Some () | _ -> None)
-      (fun () -> IEvery);
-    case(Tag 4)
-      ~title:"ILast"
-      (constant "ILast")
-      (function ILast -> Some () | _ -> None)
-      (fun () -> ILast);
-  ]
-
 type options = {
   debug : bool option;
   debug_ac : bool option;
@@ -206,8 +181,6 @@ type options = {
   fm_cross_limit : int option;
   steps_bound : int option;
 
-  interpretation : interpretation option;
-
   output_format : output_format option;
   unsat_core : bool option;
 
@@ -303,8 +276,6 @@ let init_options () = {
   fm_cross_limit = None;
   steps_bound = None;
 
-  interpretation = None;
-
   output_format = None;
   unsat_core = None;
 
@@ -428,13 +399,12 @@ let opt3_encoding =
   conv
     (fun opt3 -> opt3)
     (fun opt3 -> opt3)
-    (obj8
+    (obj7
        (opt "disable_weaks" bool)
        (opt "enable_assertions" bool)
        (opt "age_bound" int31)
        (opt "fm_cross_limit" int31)
        (opt "steps_bound" int31)
-       (opt "interpretation" interpretation_encoding)
        (opt "output_format" format_encoding)
        (opt "unsat_core" bool)
     )
@@ -569,7 +539,6 @@ let options_to_json opt =
      opt.age_bound,
      opt.fm_cross_limit,
      opt.steps_bound,
-     opt.interpretation,
      opt.output_format,
      opt.unsat_core)
   in
@@ -687,7 +656,6 @@ let options_from_json options =
          age_bound,
          fm_cross_limit,
          steps_bound,
-         interpretation,
          output_format,
          unsat_core) = all_opt3 in
     let (verbose,
@@ -769,7 +737,6 @@ let options_from_json options =
       age_bound;
       fm_cross_limit;
       steps_bound;
-      interpretation;
       output_format;
       unsat_core;
       verbose;

src/bin/js/worker_interface.mli

@@ -50,8 +50,6 @@ type sat_solver =
 
 type instantiation_heuristic =  INormal | IAuto | IGreedy
 
-type interpretation = INone | IFirst | IEvery | ILast
-
 (** Record type that contains all options that can be set for the Alt-Ergo's
     worker. *)
 type options = {
@@ -103,8 +101,6 @@ type options = {
   fm_cross_limit : int option;
   steps_bound : int option;
 
-  interpretation : interpretation option;
-
   output_format : output_format option;
   unsat_core : bool option;