Module Context_unifier_search.SearchAll (.ml)

module SearchAll: Search 

val search_context_unifiers : Context_unifier_search.config ->
       Context_unifier_search.bound ->
       Context_unifier_search.context ->
       Context_unifier_search.context_unifier_space ->
       int ->
       Context_unifier_search.context_partner ->
       Context_unifier_search.subst -> bool

search_context_unifiers config bound context space fixed_index active_partner subst searchs for all context unifiers of the clause space with the current context and the new context literal active_partner, which is paired to the clause literal with ip_index = fixed_index.

found context unifiers are propagated via the process candidate callback functions of Context_unifier.context_unifier_space.

The search must already have been initialized by unifying context_partner with the clause literal at position fixed_index in space.cus_input_partners, yielding the initial partial context unifier subst. partners must be set to context_partner at position fixed_index,

returns true, if a (at least one) closing context unifier has been found.