Module Admissible (.ml)

module Admissible: sig .. end

type subst = Subst.subst 

type raw_context_unifier = Context_unifier.raw_context_unifier 

val make_admissible : Config.config ->
       raw_context_unifier ->
       subst -> bool array -> subst

make_admissible config database raw_context_unifier subst remainder_flags makes the context unifier raw_context_unifier admissible.

The actual context unifiers (subst, Context_unifier.recompute_unifier) and the remainder states of the literals (remainder_flags, Context_unifier.compute_remainder_states) have to be explicitly given (which is just a combination of performance and convenience based on the current implementation and usage of make_admissible).

The context unifier is made admissible in a way that the remainder literals contain as few parameters as possible, while no new remainder literals are introduced.

Based on Config.mixed_literals the resulting remainder may contain mixed literals, or literals containing either universal or parametric variables.