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