Module Preprocessing_split_ground (.ml)

module Preprocessing_split_ground: sig .. end

splitting of variable disjoint clause parts

Implements ground splitting, see the paper Splitting without Backtracking by Alexander Riazanov and Andrei Voronkov.

Replaces a clause C \/ D, where C and D are variable disjoint and not ground, with the three clauses C \/ -p, D \/ -q, p \/ q, where p and q are fresh 0-ary predicates (of typeSymbol.sort.Connection).

Created clauses labelled by such a p can be reused. E.g. C \/ D, where D' \/ -p and p \/ q do already exists and D and D' are variants, is replaced by the clause C \/ -q.

Types

type clause = Term.clause

Functions

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

performs ground clause splitting and returns the split clauses.

print prints splits.

a clause is split as often as possible.

Horn clauses are split into Horn clauses.