Config.create

let create ~(flags: flags) ~(problem: problem) ~(is_horn: bool) ~(start_time: float)

    ~(fof: bool) ~(theorem:bool) : config =

  (* some sanity checks and changes of default settings *)

  let silent =

    (Flags.print_level flags)#value = 0

  in



  (* Horn *)

  if is_horn && problem#isHorn then begin

    (* horn always uses -v *)

    if (Flags.plus_v flags)#value then begin

      if not silent then

        print_endline ("Horn problem: using -v instead of +v");

      (Flags.plus_v flags)#set false;

    end;



    (* negative assert candidates can only be treated specially in the Horn case. *)

    if (Flags.neg_assert_candidates flags)#is_default

      &&

      (Flags.neg_assert_candidates flags)#value != Flags.NAC_Ignore

    then begin

      if not silent then

        print_endline ("Horn problem: ignoring negative assert candidates.");

      (Flags.neg_assert_candidates flags)#set_opt Flags.NAC_Ignore;

    end;

  end;



  let get_value get =

    (get flags)#value

  in

  let config =

    {

      start_time = start_time;

      problem = problem;

      is_horn = is_horn;

      is_fof = fof;

      is_theorem = theorem;

      flags = flags;

      resolve = get_value Flags.resolve;

      subsume = get_value Flags.subsume;

      compact = get_value Flags.compact;

      productivity = get_value Flags.productivity;

      mixed_literals = get_value Flags.mixed_literals;

      finite_domain = get_value Flags.finite_domain;

      finite_domain_functionality = get_value Flags.finite_domain_functionality;

      lemma = get_value Flags.lemma;

      lemma_min = get_value Flags.lemma_min;

      lemma_max = get_value Flags.lemma_max;

      lemma_uip = get_value Flags.lemma_uip;

      lemma_parametric_assert = get_value Flags.lemma_parametric_assert;

      

      equality = get_value Flags.equality;

      plus_v = get_value Flags.plus_v;

      backtracking = get_value Flags.backtracking;

      iterative_deepening = get_value Flags.iterative_deepening;

      deepening_bound = get_value Flags.deepening_bound;

      lookahead_exceeding = get_value Flags.lookahead_exceeding;

      restart = get_value Flags.restart;

      jumping = false(*get_value Flags.jumping*);

      neg_assert_candidates = get_value Flags.neg_assert_candidates;



      time_out_CPU = get_value Flags.time_out_CPU;

      time_out_WC = get_value Flags.time_out_WC;



      print_level = get_value Flags.print_level;

      print_configuration = get_value Flags.print_configuration;

      print_equality_axioms = get_value Flags.print_equality_axioms;

      print_lemmas = get_value Flags.print_lemmas;

      print_finite_domain_axioms = get_value Flags.print_finite_domain_axioms;

      print_finite_domain_problem = get_value Flags.print_finite_domain_problem;

      print_statistics = get_value Flags.print_statistics;

      print_model_context = get_value Flags.print_model_context;

      print_model_context_file = get_value Flags.print_model_context_file;

      print_model_DIG = get_value Flags.print_model_DIG;

      print_model_DIG_file = get_value Flags.print_model_DIG_file;

(*      print_model_ARM = (* :TODO: get_value Flags.print_model_ARM*) false;*)

      print_model_finite = get_value Flags.print_model_finite;

      print_model_tptp = get_value Flags.print_model_tptp;

      print_model_tptp_file = get_value Flags.print_model_tptp_file;

      print_derivation_online = get_value Flags.print_derivation_online;

      (*

      print_derivation = get_value Flags.print_derivation;

      print_derivation_file = get_value Flags.print_derivation_file;

      print_derivation_pruned = get_value Flags.print_derivation_pruned;

      print_derivation_pruned_file = get_value Flags.print_derivation_pruned_file;

      print_derivation_dot = get_value Flags.print_derivation_dot;

      print_derivation_dot_pruned = get_value Flags.print_derivation_dot_pruned;

      *)

      print_derivation_context_unifier = get_value Flags.print_derivation_context_unifier;

      print_assert_candidates = get_value Flags.print_assert_candidates;

      print_split_candidates = get_value Flags.print_split_candidates;



      problem_file_name = Flags.problem_file_name flags;

      

      term_indexing = true;

    }

  in



    config