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