Module Unification (.ml)

module Unification: sig .. end

type term = Term.term 

type literal = Term.literal 

type clause = Term.clause 

type binding = Subst.binding 

type subst = Subst.subst 

exception UNIFICATION_FAIL

raised by all functions when the unification fails.

val is_term_generalization : ?p_preserving:bool -> term -> term -> bool

is the first term a (proper or improper) generalization of the second?

val is_term_instance : ?p_preserving:bool -> term -> term -> bool

is the first term a (proper or improper) instance of the second?

val is_literal_instance : ?p_preserving:bool -> literal -> literal -> bool

see Unification.is_term_instance.

val match_terms : recompute:bool ->
       ?p_preserving:bool ->
       term -> int -> term -> int -> subst

match_terms term1 offset1 term2 offset2 returns a most general substitution which applied to term1 offset1 produces term2.

raises Unification.UNIFICATION_FAIL

val match_literals : recompute:bool ->
       ?p_preserving:bool ->
       literal -> int -> literal -> int -> subst

like Unification.match_terms over literals.

val are_terms_unifiable : ?p_preserving:bool -> term -> term -> bool

are the two terms unifiable?

val unify_terms : recompute:bool ->
       ?p_preserving:bool ->
       term -> int -> term -> int -> subst

unify_terms term1 offset1 term2 offset2 returns a most general substitution which applied to term1 offset1 or term2 offset2 produces the same term.

prefers to bind universal variables to parametric ones instead of vice versa (see Admissible).

raises Unification.UNIFICATION_FAIL if no unifier exists.

val unify_terms_ : recompute:bool ->
       ?p_preserving:bool ->
       subst ->
       term -> int -> term -> int -> subst

like unify_terms, but extends the given substitution.

val unify_literals : recompute:bool ->
       ?p_preserving:bool ->
       literal -> int -> literal -> int -> subst

like Unification.unify_terms over literals.

val unify_literals_ : recompute:bool ->
       ?p_preserving:bool ->
       subst ->
       literal -> int -> literal -> int -> subst

like unify_literals, but extends the given substitution.

val unify_constraints : recompute:bool ->
       ((literal * int) * (literal * int)) list ->
       subst

unifies constraints of universal literals with offsets. e.g. the constraint (p(x), 1), (q(f(x)), 2) yields [ 1:x -> 2:f(x) ]

val unify_constraints' : recompute:bool ->
       ((literal * int) * (literal * int)) list ->
       Subst.hash_subst

like , but returns a hash_subst.

val match_substs : recompute:bool ->
       ?p_preserving:bool ->
       int -> subst -> subst -> subst

match_substs subsuming_offset subst1 subst2 merges subst1 and subst2.

Terms with subsuming_offset have been matched to other terms, and the resulting substitutions are now to be merged.

If a variable is bound to different terms in subst1 and subst2 the bound terms are unified. I.e. if

• both terms have subsuming_offset they are unified (Unification.unify_terms)
• if one term has subsuming_offset it is matched (Unification.match_terms) to the other
• if no term has subsuming_offset the substitutions are not matcheable and Unification.UNIFICATION_FAIL is raised.

val unify_substs : recompute:bool ->
       ?p_preserving:bool ->
       subst -> subst -> subst

match_substs subsuming_offset subst1 subst2 merges subst1 and subst2.

If a variable is bound to different terms in subst1 and subst2 the bound terms are unified (Unification.unify_terms).

if x -> y and y -> x have to be merged one is dropped and the other kept, i.e. this is not considered to be a cyclic binding.

Examples:

• x -> a and x -> b are not mergeable.
• x -> g(y) and y -> a becomes x -> g(y); y -> a.
• x -> g(y) and x -> g(a) becomes x -> g(y); y -> a.
• x -> y and y -> x becomes x -> y or y -> x.

raises Unification.UNIFICATION_FAIL on not mergeable substitutions.

val unify_substs_shallow : subst -> subst -> unit

a pre-check to unify_subst which only unifies top symbols of terms. raises Unification.UNIFICATION_FAIL if that fails.

val merge_substs : subst -> subst -> subst

merge_substs subst1 subst2 merges subst1 and subst2 by adding all bindings into one substitution.

if a variable is bound in both substitutions, Unification.UNIFICATION_FAIL is raised if it is bound to different terms, otherwise only one of the two identical bindings is kept. no other consistency checks are performed, that is for example cycles may be introduced.

val subsumes : clause -> clause -> bool

does the first clause subsume the second one? that is, exists a subsitution that applied to the second clause yields the first clause (if seen as sets)?

e.g. { p(a) } subsumes { p(x), p(a) }.

this implies that the subsuming clause has at most as many literal as the subsumed clause. despite of this, no prefiltering is done at all, subsumption is strictly done in an exponential trial and error way.

the clauses are subsumed to be universal, i.e. unification is not done p-preserving.

val condense : clause -> clause

a clause is condensed if it subsumes no proper subset of itself, i.e. it contains no logical equivalent subset. put another way, the clause and its condensed version mutually subsume each other (the subset trivially subsumes the superset), and there is no subset of the condensed clause for which this is the case.

e.g. { p(x), p(a) } is condensed to { p(a) }.

worst case complexity is a linear number of subsumption tests.