Module Admissible (.ml)


module Admissible: sig .. end
making a context unifier admissible


Types

type subst = Subst.subst 
type raw_context_unifier = Context_unifier.raw_context_unifier 

Functions

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.