package logtk

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
LogtkTransformations on LogtkFormulas and Terms
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 =
  1. | RwTerm of LogtkRewriting.TRS.t
  2. | RwForm of LogtkRewriting.FormRW.t
  3. | 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