module LogtkFormulaShape:`sig`

..`end`

type`form =`

`LogtkFormula.FO.t`

type`term =`

`LogtkFOTerm.t`

`val is_definition : ``form ->`

(term * term) option

Check whether the clause defines a symbol, e.g.
subset(X,Y) = \forall Z(Z in X -> Z in Y). It means the LHS
is a flat symbol with variables, and all variables in RHS
are also in LHS

`val is_pred_definition : ``form ->`

(term * form) option

Check whether the formula is a predicate definition

`val is_rewrite_rule : ``form ->`

(term * term) list

More general than definition. It means the clause is an
equality where all variables in RHS are also in LHS. It
can return two rewrite rules if the clause can be oriented
in both ways, e.g. associativity axiom.

`val is_pred_rewrite_rule : ``form ->`

(term * form) option

LogtkRewriting rule for predicates

`val is_const_definition : ``form -> (LogtkSymbol.t * term) option`

Checks whether the clause is "const = ground composite term", e.g.
a clause "aIbUc = inter(a, union(b, c))". In this case it returns
Some(constant, definition of constant)

`val is_const_pred_definition : ``form -> (LogtkSymbol.t * form) option`

Definition of constant predicate

See module

`LogtkTransform`

. By detecting some shapes in the input,
for instance rewrite rules or term definitions, one can obtain
interesting transformations`val detect : ``form Sequence.t -> LogtkTransform.t list`

Detect shapes in the given sequence, and convert them into
transformations over formulas

`val detect_list : ``form list -> LogtkTransform.t list`

`val detect_def : ``?only:[ `Pred | `Term ] ->`

?arity:[ `Nonzero | `Zero ] ->

form Sequence.t -> LogtkTransform.t list

Detect definitions.

`only`

: if present, restrict detection to predicates or terms`arity`

: if present, restrict to constant or non-constant symbols