Module Logtk.FormulaShape (.ml)

module FormulaShape: LogtkFormulaShape

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

Interface to LogtkTransform



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