type form = LogtkFormula.FO.ttype term = LogtkFOTerm.tCheck 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
Check whether the formula is a predicate definition
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_const_definition : form -> (LogtkSymbol.t * term) optionChecks 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) optionDefinition 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 listDetect shapes in the given sequence, and convert them into transformations over formulas
val detect_list : form list -> LogtkTransform.t listval detect_def :
?only:[ `Pred | `Term ] ->
?arity:[ `Zero | `Nonzero ] ->
form Sequence.t ->
LogtkTransform.t listDetect definitions.
if present, restrict detection to predicates or terms
if present, restrict to constant or non-constant symbols