Module Preprocessing_equality (.ml)

module Preprocessing_equality: sig .. end

type clause = Term.clause 

exception EMPTY_CLAUSE of clause

this clause is simplified to the empty clause, so the clause set is unsatisfiable.

val simplify : print:bool ->
       clause list -> clause list

performs trivial simplificiations based on equality and returns the simplified clauses.

simplifies disequalities of the form

• -(x = t) \/ C -> C where t a term or variable and x not in t

• -(t = t) \/ C -> C where t a term or variable

Raises EMPTY_CLAUSE if a clause is simplified to empty clause.