Module Logtk.Transform (.ml)

module Transform: LogtkTransform

type term = LogtkFOTerm.t 
type form = LogtkFormula.FO.t 

Provides some transformations on formulas, and sets of formulas. LogtkTransformations include definition expansion and term rewriting
type t = 
| RwTerm of LogtkRewriting.TRS.t
| RwForm of LogtkRewriting.FormRW.t
| Tr of string * (form -> form list) (*
the function can return a conjunction of formulas. The string is a short name/description of the transformation
type transformation = t 
val of_term_rule : term * term -> t
val of_term_rules : (term * term) list -> t
val of_term_rules_seq : (term * term) Sequence.t -> t
val of_form_rule : term * form -> t
val of_form_rules : (term * form) list -> t
val of_form_rules_seq : (term * form) Sequence.t -> t
val of_term_tr : string -> (term -> term) -> t
Lift a term transformation to the formula level
val open_and : t
transformation that opens outermost "and" connectives
val remove_trivial : t
Tranformation that removes trivial formulas
val apply : t -> form -> form list
Apply the transformations to a formula
val pp : Buffer.t -> t -> unit
val fmt : Format.formatter -> t -> unit

LogtkTransformation DAG

Abstraction over formulas with additional information. A FORM.t contains a formula, and is built from parent formula wrappers upon a transformation.
module type FORM = sig .. end

This module provides an infrastructure to efficiently compute the fixpoint of a set of transformations on a set of formulas. LogtkFormulas form a DAG, whose edges go from a formula to the formulas it transforms into; result set is the set of leaves reachable from the initial formulas.
module type DAG = sig .. end
module MakeDAG (Form : FORM) : DAG  with module Form = Form
Build a DAG
module FormDag: DAG  with type Form.t = form
Trivial instance, with bare formulas