Module Preprocessing_equality (.ml)


module Preprocessing_equality: sig .. end
simplifications based on equality


Types

type clause = Term.clause 
exception EMPTY_CLAUSE of clause
this clause is simplified to the empty clause, so the clause set is unsatisfiable.

Functions

val simplify : print:bool ->
clause list -> clause list
performs trivial simplificiations based on equality and returns the simplified clauses.

simplifies disequalities of the form


Raises EMPTY_CLAUSE if a clause is simplified to empty clause.