let apply_propagation (state: state) (literal: literal) (context_unifier: subst)
(clause: clause) (clause_vars: Subst.var list) (clause_index: int) (clause_value: unit -> unit)
(context_literals: literal array)
: unit =
let literal_info =
create_literal_info literal Propagation (active_choice_point state)
context_unifier clause clause_vars context_literals clause_index clause_value None
in
LiteralTable.add state.st_literal_info literal literal_info