Functor LogtkFormula.Make

module Make (MyT : TERM) : S 
  with type term = MyT.t
  and type term_set = MyT.Set.t
Parameters:
MyT : TERM

type term 
type term_set 
type t = private LogtkScopedTerm.t 
type form = t 
type view = private 
| True
| False
| Atom of term
| And of t list
| Or of t list
| Not of t
| Imply of t * t
| Equiv of t * t
| Xor of t * t
| Eq of term * term
| Neq of term * term
| Forall of LogtkFormula.type_ * t (*
Quantified formula, with De Bruijn index
*)
| Exists of LogtkFormula.type_ * t
| ForallTy of t (*
quantification on type variable
*)
val view : t -> view
View of the formula
val kind : LogtkScopedTerm.Kind.t
val of_term : LogtkScopedTerm.t -> t option
val of_term_exn : LogtkScopedTerm.t -> t
Raises Invalid_argument if the term isn't a formula
val is_form : LogtkScopedTerm.t -> bool
include LogtkInterfaces.HASH
include LogtkInterfaces.ORD

Containers


module Tbl: Hashtbl.S  with type key = t
module Set: Sequence.Set.S  with type elt = t
module Map: Sequence.Map.S  with type key = t

Caution: constructors can raise LogtkType.Error if the types are not as expected. In particular, LogtkFormula.S.Base.eq and LogtkFormula.S.Base.neq expect two terms of the exact same type.
module Base: sig .. end

Sequence


module Seq: sig .. end

Combinators


val map_leaf : (t -> t) ->
t -> t
Call the function on leaves (atom,equal,true,false) and replace the leaves by their image. The image formulas should not contain free De Bruijn indexes (ie, should verify db_closed).
val map : (term -> term) ->
t -> t
Map on terms
val fold : ('a -> term -> 'a) -> 'a -> t -> 'a
Fold on terms
val iter : (term -> unit) -> t -> unit
val map_shallow : (t -> t) ->
t -> t
Apply the function to the immediate subformulas
val map_depth : ?depth:int ->
(int -> term -> term) ->
t -> t
Map each term to another term. The number of binders from the root of the formula to the term is given to the function.
val map_leaf_depth : ?depth:int ->
(int -> t -> t) ->
t -> t
val fold_depth : ?depth:int ->
('a -> int -> term -> 'a) -> 'a -> t -> 'a
Fold on terms, but with an additional argument, the number of De Bruijn indexes bound on through the path to the term
val weight : t -> int
Number of 'nodes' of the formula, including the terms
val subterm : term -> t -> bool
subterm t f true iff t occurs in some term of f
val is_atomic : t -> bool
No connectives?
val is_ground : t -> bool
No variables?
val is_closed : t -> bool
All variables bound?
val contains_symbol : LogtkSymbol.t -> t -> bool
val symbols : ?init:LogtkSymbol.Set.t -> t -> LogtkSymbol.Set.t
Set of symbols occurring in the formula

High level operations


val free_vars_set : t -> term_set
Set of free variables
val free_vars : t -> term list
Set of free vars
val de_bruijn_set : t -> LogtkType.Set.t * term_set
Deprecated.dangerous, use LogtkDBEnv functions
Set of De Bruijn indices that are not bound for types and terms
val close_forall : t -> t
Bind all free variables with forall
val close_exists : t -> t
Bind all free variables with exists
val open_forall : ?offset:int -> t -> t
Remove outer forall binders, using fresh vars instead of DB symbols
val open_and : t -> t list
If the formula is an outer conjunction, return the list of elements of the conjunction
val open_or : t -> t list

Simplifications


val flatten : t -> t
Flatten AC connectives (or/and)
val simplify : t -> t
Simplify the formula
val is_trivial : t -> bool
Trivially true formula?
val ac_normal_form : t -> t
Normal form modulo AC of "or" and "and"
val ac_eq : t -> t -> bool
Equal modulo AC?

Conversions


val to_prolog : ?depth:int -> t -> LogtkPrologTerm.t

IO


include LogtkInterfaces.PRINT
include LogtkInterfaces.PRINT_DE_BRUIJN
module TPTP: sig .. end