Module Preprocessing_split_nonground (.ml)

module Preprocessing_split_nonground: sig .. end

splitting of clause parts

Implements non-ground splitting, see the paper New Techniques that Improve MACE-style Finite Model Finding by Koen Classen and Niklas Soerensson.

Say var(C) are the variables contained in the literals C. The non-ground splitting replaces a clause C \/ D with the clauses C \/ p, D \/ -p. var(C) and var(D) must share some variables X, but each must alsto contain variables not in X. p is a fresh predicate (of typeSymbol.sort.Connection) over X. For example, if X = { x, y, z } then p is p(x, y, z).

Labelling is used as described in Preprocessing_split_ground.

Types

type clause = Term.clause

Functions

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

performs non-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.