Context_unifier.create

let create_space id clause clause_vars shared_vars local_vars input_partners ordering

    process_close process_assert process_split

    is_element_incomplete_assert is_element_incomplete_split is_lemma =

  {

    cus_id = id;

    cus_clause = clause;

    cus_vars = clause_vars;

    cus_shared_vars = shared_vars;

    cus_local_vars = local_vars;

    cus_input_partners = input_partners;

    cus_input_partners_ordering = ordering;

    cus_process_close_candidate = process_close;

    cus_process_assert_candidate = process_assert;

    cus_process_split_candidate = process_split;

    cus_is_element_incomplete_assert = is_element_incomplete_assert;

    cus_is_element_incomplete_split = is_element_incomplete_split;

    cus_lemma = is_lemma;

    cus_lemma_learned = if is_lemma then 1 else 0;

    cus_utility = ref 0;

  }