sig
  type flag_id
  type opt_equality = EQ_None | EQ_Axioms
  type opt_backtracking = BT_Naive | BT_Backjumping
  type opt_iterative_deepening = IT_TermDepth | IT_TermWeight
  type opt_restart = RS_Eager | RS_Lazy | RS_Delayed
  type opt_neg_assert_candidates = NAC_Ignore | NAC_Lookahead | NAC_Use
  type opt_lemma = LM_None | LM_Grounded | LM_Lifted | LM_Propositional
  type opt_preprocess_split = PPS_None | PPS_Ground | PPS_NonGround
  type opt_input_format = FI_TME | FI_TPTP | FI_Darwin
  type opt_print_fd_problem = PFD_Silent | PFD_Print | PFD_Exit
  class type ['a, 'b] flag_type =
    object
      method argument_to_string : 'b -> string
      method description : string list
      method id : Flags.flag_id
      method is_default : bool
      method long_name : string
      method opt_to_string : string list
      method set : 'b -> unit
      method set_opt : 'a -> unit
      method short_name : string
      method signature : string
      method value : 'a
      method value_to_string : 'a -> string
    end
  type flag_type_bool = (bool, bool) Flags.flag_type
  type flag_type_int = (int, int) Flags.flag_type
  type flag_type_float = (float, float) Flags.flag_type
  type flag_type_unit = (unit, unit) Flags.flag_type
  type flag_type_string = (string, string) Flags.flag_type
  type flag_type_equality = (Flags.opt_equality, string) Flags.flag_type
  type flag_type_backtracking =
      (Flags.opt_backtracking, string) Flags.flag_type
  type flag_type_iterative_deepening =
      (Flags.opt_iterative_deepening, string) Flags.flag_type
  type flag_type_restart = (Flags.opt_restart, string) Flags.flag_type
  type flag_type_neg_assert_candidates =
      (Flags.opt_neg_assert_candidates, string) Flags.flag_type
  type flag_type_lemma = (Flags.opt_lemma, string) Flags.flag_type
  type flag_type_preprocess_split =
      (Flags.opt_preprocess_split, string) Flags.flag_type
  type flag_type_input_format =
      (Flags.opt_input_format, string) Flags.flag_type
  type flag_type_print_fd_problem =
      (Flags.opt_print_fd_problem, string) Flags.flag_type
  type flag
  type flags = private {
    flags : Flags.flag list;
    mutable problem_file_name : string;
  }
  val eval_command_line : unit -> Flags.flags
  val create : string -> Flags.flags
  val resolve : Flags.flags -> Flags.flag_type_bool
  val subsume : Flags.flags -> Flags.flag_type_bool
  val compact : Flags.flags -> Flags.flag_type_bool
  val productivity : Flags.flags -> Flags.flag_type_bool
  val mixed_literals : Flags.flags -> Flags.flag_type_bool
  val finite_domain : Flags.flags -> Flags.flag_type_bool
  val finite_domain_functionality : Flags.flags -> Flags.flag_type_bool
  val lemma : Flags.flags -> Flags.flag_type_lemma
  val lemma_min : Flags.flags -> Flags.flag_type_int
  val lemma_max : Flags.flags -> Flags.flag_type_int
  val lemma_uip : Flags.flags -> Flags.flag_type_bool
  val lemma_parametric_assert : Flags.flags -> Flags.flag_type_int
  val equality : Flags.flags -> Flags.flag_type_equality
  val plus_v : Flags.flags -> Flags.flag_type_bool
  val backtracking : Flags.flags -> Flags.flag_type_backtracking
  val iterative_deepening :
    Flags.flags -> Flags.flag_type_iterative_deepening
  val deepening_bound : Flags.flags -> Flags.flag_type_int
  val lookahead_exceeding : Flags.flags -> Flags.flag_type_bool
  val restart : Flags.flags -> Flags.flag_type_restart
  val jumping : Flags.flags -> Flags.flag_type_bool
  val neg_assert_candidates :
    Flags.flags -> Flags.flag_type_neg_assert_candidates
  val eprover : Flags.flags -> Flags.flag_type_string
  val preprocess_split : Flags.flags -> Flags.flag_type_preprocess_split
  val preprocess_unit : Flags.flags -> Flags.flag_type_bool
  val preprocess_pure : Flags.flags -> Flags.flag_type_bool
  val preprocess_resolution : Flags.flags -> Flags.flag_type_bool
  val preprocess_equality : Flags.flags -> Flags.flag_type_bool
  val input_format : Flags.flags -> Flags.flag_type_input_format
  val time_out_CPU : Flags.flags -> Flags.flag_type_float
  val time_out_WC : Flags.flags -> Flags.flag_type_float
  val memory_limit : Flags.flags -> Flags.flag_type_int
  val print_level : Flags.flags -> Flags.flag_type_int
  val print_preprocess_split : Flags.flags -> Flags.flag_type_bool
  val print_preprocess_unit : Flags.flags -> Flags.flag_type_bool
  val print_preprocess_pure : Flags.flags -> Flags.flag_type_bool
  val print_preprocess_resolution : Flags.flags -> Flags.flag_type_bool
  val print_preprocess_equality : Flags.flags -> Flags.flag_type_bool
  val print_configuration : Flags.flags -> Flags.flag_type_bool
  val print_lemmas : Flags.flags -> Flags.flag_type_bool
  val print_finite_domain_sorts : Flags.flags -> Flags.flag_type_bool
  val print_finite_domain_transformation :
    Flags.flags -> Flags.flag_type_bool
  val print_finite_domain_axioms : Flags.flags -> Flags.flag_type_bool
  val print_finite_domain_problem :
    Flags.flags -> Flags.flag_type_print_fd_problem
  val print_equality_axioms : Flags.flags -> Flags.flag_type_bool
  val print_statistics : Flags.flags -> Flags.flag_type_bool
  val print_model_context : Flags.flags -> Flags.flag_type_bool
  val print_model_context_file : Flags.flags -> Flags.flag_type_string
  val print_model_DIG : Flags.flags -> Flags.flag_type_bool
  val print_model_DIG_file : Flags.flags -> Flags.flag_type_string
  val print_model_ARM : Flags.flags -> Flags.flag_type_bool
  val print_model_finite : Flags.flags -> Flags.flag_type_bool
  val print_model_tptp : Flags.flags -> Flags.flag_type_bool
  val print_model_tptp_file : Flags.flags -> Flags.flag_type_string
  val print_derivation_online : Flags.flags -> Flags.flag_type_bool
  val print_derivation_context_unifier : Flags.flags -> Flags.flag_type_bool
  val print_assert_candidates : Flags.flags -> Flags.flag_type_bool
  val print_split_candidates : Flags.flags -> Flags.flag_type_bool
  val problem_file_name : Flags.flags -> string
  val zipped_file_name : Flags.flags -> string
  type 'a apply_to_flag = { apply : 'b 'c. ('b, 'c) Flags.flag_type -> 'a; }
  val process_flag : Flags.flag -> 'a Flags.apply_to_flag -> 'a
end