Module Preprocessing_pure (.ml)

module Preprocessing_pure: sig .. end

removes pure clauses

A clause is pure in a clause set, if it contains a literal which does not unify with the negation of a literal in any other clause.

For problems without equality this is detected by unification of the literals occuring in the clause set.

For problems with equality by checking that a predicate symbol occurs only in one polarity.

type literal = Term.literal

type clause = Term.clause

val simplify : print:bool ->
       equality:bool ->
       clause list ->
       clause list * literal list

removes pure clauses.

print prints removed pure clauses. equality denotes that the input contains equality.

Is done up to fixpoint for equality, but due to the overhead only one pass is performed otherwise.

returns the simplified clause set, and the pure literals of the removed pure clauses.