Previous  Up  Next

Module Subst (.ml)


module Subst: sig .. end
a substitution

A substitution is an immutable mapping from variables to terms.

In order to be able to efficiently reuse a literal when several fresh variants of it are needed during a unification process, each variable and term is paired with an offset. Thus creating a fresh variant of a literal consists just of pairing the literal with fresh offsets.

Therefore a Subst.subst stores not a mapping from Var.var to Term.term, but from Subst.var to Subst.term.

A substitution is represented in the triangular form. I.e. if variables occuring in bound terms are also bound in the substitution, they have to be replaced by their binding.

E.g. instead of [x -> (g(a)); y -> a] the substitution may be [x -> (g(y)), y -> a].

Path compression is exhaustively done for variable to variable bindings, but not for bound variables within a bound term. E.g. [x -> (g(z)); y -> z; z -> a] would be represented as [x -> (g(z)); y -> a; z -> a].

A substitution is parameter preserving (p_preserving) if parameters are only bound injectively to parameters of other terms.

Thus a p_preserving unifier between two terms contains a renaming between the parameters (indicator variables) of the two terms.

If p_preserving is an optional argument of a function below, it always defaults to false, thus completely ignoring the different variable types.

if recompute is true as an argument of a function below, the unifier is recomputed and is thus known to be computable. then consistency checks like the occur check are not performed.


Types


type var = private {
   sv_var : Var.var;
   sv_offset : int;
}
associates a Var.var with an offset.

type term = private {
   st_term : Term.term;
   st_offset : int;
}
associates a Term.term with an offset.

type binding = private {
   sb_var : var;
   sb_term : term;
}
a binding of a Subst.var to a Subst.term.
type subst = binding list
a substitution is a set of bindings.
module VarTable: Hashtbl.S  with type key = var
a specialized Hashtbl with variables as keys. 
type hash_subst = term VarTable.t
a substitution as a mapping from variables to bindings. In general slower than subst, but for some huge substitutions way faster.
exception SET_FAIL
see Subst.set

Functions


Offsets



A context unifier is not build at once, its literal pairs are unified separately into partial context unifiers which are merged afterwards (Context_unifier_space, Context_unifier_search). Creating a fresh variant of a literal merely consists of pairing the literal with an offset. Thus in order to be able to correctly merge the partial context unifiers they must use different offsets, as determined by the following functions:
val input_literal_offset : int
a literal of the input clause.
val context_literal_offset : int -> int
context_literal_offset input_clause_literal_index computes the offset of the context literal paired with the input literal at position input_clause_literal_index of the clause.
val fresh_par_offset : int
to make a context unifier admissible it might be necessary to bind universal variables to new/fresh parameters.

Creation


val empty : subst
empty substitution. immutable.
val make_var : Var.var -> int -> var
create a Subst.var.
val make_term : Term.term -> int -> term
create a Subst.term.
val make_binding : var -> term -> binding
create a Subst.binding.

Access


val get : subst -> var -> term option
get subst var returns the term bound to var, or None if var is unbound. Because of the triangular substitution (see module description) the returned term may contain other variables bound in the substitution. To get the real term its variables binding must be evaluated as well, or equivalently Subst.apply_to_term must be applied to the term to create the proper term instance.
val get' : subst -> Var.var -> int -> term option
get' subst var offset wrapper for Subst.get.
val get_bound_vars : subst -> var list -> var list
get_bound_vars subst vars returns for each var in vars 
val set : recompute:bool ->
       ?p_preserving:bool -> subst -> var -> term -> subst
set subst var term. extends subst by the binding var -> term.
Raises SET_FAIL if p_preserving is by default false. If true, subst is expected to be p_preserving and is extended with the new binding var -> term retaining a p_preserving substitution. If this is not possible, SET_FAIL is raised.
val set' : recompute:bool ->
       ?p_preserving:bool ->
       subst -> Var.var -> int -> Term.term -> int -> subst
wrapper for Subst.set
val orient : binding -> binding
orients bindings by imposing a total order: 
val dereference' : hash_subst -> term -> term
dereferences term in the substitution. i.e., if the term is a variable and this variable is bound, the bound term is returned, otherwise the original term.

performs path compression.

val first : subst -> binding
get any binding in the substitution. the substitution may not be empty.
val find : (binding -> bool) -> subst -> binding
find a binding satisfying the predicate
val find_all : (binding -> bool) -> subst -> subst
find all bindings satisfying the predicate
val is_empty : subst -> bool
is this the empty substitution?
val is_p_renaming : subst -> int -> bool
is this subset p-preserving on the given offset? I.e. after a unification it can be checked if a term paired with this offset is instantiated only in a p-preserving way.
val length : subst -> int
the number of bindings in the substitution.
val append : binding -> subst -> subst
adds the binding to the substitution without doing any of the consistency checks that Subst.set does perform.
val map : (binding -> binding) -> subst -> subst
like List.map, but the result must be a substitution.
val map' : (binding -> 'a) -> subst -> 'a list
like List.map, but the result may be any list.
val partition : (binding -> bool) -> subst -> subst * subst
like List.partition
val for_all : (binding -> bool) -> subst -> bool
like List.for_all
val exists : (binding -> bool) -> subst -> bool
like List.exists
val fold : ('a -> binding -> 'a) -> 'a -> subst -> 'a
like List.fold
val iter : (binding -> unit) -> subst -> unit
like List.iter

Access - Modules



In functions which heavily rely on substitution access it pays of to hard code the p_preserving options in terms of performance. For these means the following modules specialize on the set function:
module type T_Preserving = sig .. end
interface for specialized set modules 
module PPreserving: T_Preserving
recompute = false; p_preserving = true 
module Preserving: T_Preserving
recompute = false; p_preserving = false 
module RPPreserving: T_Preserving
recompute = true; p_preserving = true 
module RPreserving: T_Preserving
recompute = true; p_preserving = false

Application


val normalize_term : Term.term -> Term.term
returns the normalized version of the term. I.e. the variables' ids in the new term are enumerated from 0 on.
val normalize_literal : Term.literal -> Term.literal
see Subst.normalize_term.
val normalize_clause : Term.clause -> Term.clause
see Subst.normalize_term.
val apply_to_term : ?insert_db:bool ->
       ?normalize:bool -> subst -> Term.term -> int -> Term.term
apply_to_term subst term offset applies subst to term with offset and returns a new term.

for insert_db see Term

if normalize is true the term is normalized (default:true) .

val apply_to_literal : ?insert_db:bool ->
       ?normalize:bool -> subst -> Term.literal -> int -> Term.literal
see Subst.apply_to_term.
val apply_to_clause : subst -> Term.clause -> int -> Term.clause
see Subst.apply_to_term.
val apply_to_literals : subst -> (Term.literal * int) list -> Term.literal list
like Subst.apply_to_term. the normalization is done consistently over all literals, i.e. a variable occuring in several term instances is mapped to the same literal in the normalized version. E.g. apply_to_literals [ 0:x -> 2:z; 1:y -> 2:z ] [ (p(x), 0); (q(y), 1) ] returns [ p(x), q(x) ], where x has the id 0.
val apply_to_literals_groups : subst -> (Term.literal * int) list list -> Term.literal list list
like Subst.apply_to_literals, but for lists of literals.
val apply_to_literal_groups' : hash_subst -> (Term.literal * int) list list -> Term.literal list list
like Subst.apply_to_literals, but using a hash_subst.
val replace_offset : subst -> int -> int -> subst
replace_offset subst old_offset new_offset replaces all occurences of old_offset in subst by new_offset.
val replace_in_bound_terms : subst -> Term.term -> Term.term -> subst
replace_offset subst old_term new_term replaces in all terms bound in subst all occurences of old_term by new_term.

No offsets can be specified and there may only be one offset used in the whole substitution.

val reverse_bindings : subst -> var list -> var list -> subst
reverse_var_to_par subst vars_to_reverse pars_to_keep reverses one by one the bindings of the variables in vars_to_reverse, if 
val remove_context_var_renamings : subst -> subst
removes all renamings of context variables that are not bound by/in a term bound by another variable. e.g. u -> a; v -> x; w -> y; z -> f(w) becomes u -> a; w -> y; z -> f(w)

Comparison


val var_equal : var -> var -> bool
are the two variables identical?
val term_equal : term -> term -> bool
are the two terms identical?
val binding_equal : binding -> binding -> bool
are the two bindings identical?
val subst_equal : subst -> subst -> bool
are the two substitutions identical?

String Representation


val var_to_string : var -> string
val term_to_string : term -> string
val binding_to_string : binding -> string
val subst_to_string : subst -> string
returns the triangular form, i.e. bound variables are not replaced by their bound term.