let create (config: config)
    (statistic: Statistic.statistic) (state: state) : context =

  let index =
    if Config.is_horn config then
      Discrimination_tree.create_index false (new index_data)
    else
      Discrimination_tree.create_index true (new index_data)
(*      Substitution_tree.create_index (new index_data)*)
  in
    {
      config = config;
      statistic = statistic;
      state = state;
      id_counter = Counter.create_with 0;
      max_size = 0;
      context = Stack.create null_element;
      index = index;
      universal = None;
    }