Module FFTNF

module FFTNF: sig .. end
Computing the FF Type Normal Form.

Compact tentative specification of FFTNF(_<_):

Consider a graph whose nodes are literals of a formula and two nodes are connected by an edge iff the literals share a variable. Direct the edges so that there is no edge a->b for b_<_a. The formula is in FFTNF(_<_) iff it is in TNF and the number of quantifiers a literal is in scope of never decreases along an edge, for some such directing of edges.

FIXME: the above specification is not correct (too weak).

val parsimony_threshold_1 : int Pervasives.ref
val parsimony_threshold_2 : int Pervasives.ref
val p_pn_nnf : ?do_pnf:bool -> Formula.formula -> Formula.formula
Prenex-normal negation normal form of a formula with minimized alternation and preference to start from existential quantification.
val ff_tnf : ?force_parsimony:int ->
(Formula.formula -> Formula.formula -> bool) ->
Formula.formula -> Formula.formula
FF Type Normal Form: a variant of Type Normal Form that promotes literals with older (earlier quantified) variables, and if undecisive, according to the given relation.
val promote_rels : Aux.Strings.t -> Formula.formula -> Formula.formula -> bool
Promote relations from the given set.
val ffsep : Aux.Strings.t ->
Aux.Strings.t ->
Formula.formula ->
(Formula.fo_var list * Formula.formula list * Formula.formula) list