Module Preprocessing_resolution (.ml)

module Preprocessing_resolution: sig .. end

type clause = Term.clause 

exception EMPTY_CLAUSE of (clause * clause)

these clauses simplify to the empty clause, so the clause set is unsatisfiable.

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

Computes and returns short resolvents for the clause set.

Performs binary resolution between input clauses. Only resolvent of size < Const.resolvent_max_size are kept. At most Const.resolvents_max_number resolvents are computed.

print prints computed resolvents.
Raises EMPTY_CLAUSE if two clauses resolved to the empty clause.