Module Preprocessing_unit (.ml)

module Preprocessing_unit: sig .. end

unit subsumption and resolution

removes (non-unit) clauses subsumed by unit clauses, and simplifies clauses by removing literals resolved by unit clauses.

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 unit simplification.

print prints simplifications.

Only one pass is performed, that is if clauses are simplified to unit clauses, these new unit clauses are not used to simplify already processed clauses.

returns the simplified clause set.
Raises EMPTY_CLAUSE if a clause resolved to the empty clause.