Module SharedInput

module SharedInput: sig .. end

type table 

val make_table : unit -> table

val null_table : table

val share_subterms : table -> Term.term -> Term.term

share_subterms table term returns a variant of term with subterms replaced as far as possible by subterms stored in table. Subterms not already in the table are inserted.

This function is intended to be called on propositional (instead of functional) terms. Since handling of variants on the propositional level is usually performed using other means such as subsumption, only proper subterms of term are considered for sharing.

Only subterms which are ground are shared.