let create (config: config) (bound: bound) (statistic: statistic) (state: state)
(context: context) (problem_literals: problem_literals) : candidates =
let unprocessed =
Array.make (Tools.max_int 1 Const.max_unprocessed_assert_candidates) Context_unifier.null_context_unifier
in
{
cd_config = config;
cd_bound = bound;
cd_statistic = statistic;
cd_state = state;
cd_context = context;
cd_problem_literals = problem_literals;
cd_unprocessed = unprocessed;
cd_unprocessed_size = 0;
cd_valid = Valid.create null_candidate;
cd_forgotten_order = ForgottenOrder.empty;
cd_forgotten_barrier = ForgottenBarrier.create 64;
cd_forgotten_recomputation_barrier = None;
cd_exceeding_elements = Hashtbl.create 64;
cd_check_exceeding = false;
cd_lookahead = Selection_lookahead.create Const.max_assert_lookahead;
cd_lookahead_exceeding = Selection_lookahead.create Const.max_assert_lookahead_exceeding;
cd_preselected = None;
}