package logtk

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Some helpers

package logtk

logtk
- Logtk
  - AllocCache
    
    Arr
  - Binder
    
    TPTP
    
    ZF
  - Builtin
    
    Arith
    
    ArithOp
    
    TPTP
    
    Tag
    
    ZF
  - Cnf
  - Comparison
    
    PARTIAL_ORD
  - Compute_prec
  - Congruence
    
    FO
    
    Make
    
    T
    
    TERM
  - Congruence_intf
    
    S
  - DBEnv
  - Defined_pos
    
    Arr
  - Dtree
    
    Default
    
    Make
    
    E
  - FV_tree
    
    Make
    
    C
    
    Feature_fun
  - FeatureVector
    
    Make
    
    C
    
    Feature
  - Fingerprint
    
    Make
    
    Leaf
  - Flex_state
  - HO_unif
  - HVar
  - Hash
  - Hashcons
    
    HashedType
    
    Make
    
    X
    
    MakeNonWeak
    
    X
    
    S
  - Head
  - IArray
  - ID
    
    Map
    
    Set
    
    Tbl
  - Ind_ty
  - Index
    
    BasicEquation
    
    MakeLeaf
  - Index_intf
    
    CLAUSE
    
    EQUATION
    
    LEAF
    
    SUBSUMPTION_IDX
    
    C
    
    TERM_IDX
    
    Leaf
    
    UNIT_IDX
    
    E
  - InnerTerm
    
    DB
    
    Map
    
    Pos
    
    Seq
    
    Set
    
    Tbl
    
    VarMap
    
    VarSet
    
    VarTbl
  - Input_format
  - Int_lit
    
    Focus
    
    Seq
    
    Util
  - Interfaces
    
    EQ
    
    GROUP
    
    HASH
    
    ITER
    
    MONOID
    
    ORD
    
    PRINT
    
    PRINT1
    
    PRINT2
    
    PRINT3
    
    PRINT_DE_BRUIJN
    
    PRINT_OVERLOAD
  - Lambda
    
    Inner
  - LazyList
  - Literal
    
    Comp
    
    Conv
    
    Pos
    
    Seq
    
    Set
    
    View
  - Literals
    
    Conv
    
    Pos
    
    Seq
    
    View
  - Monome
    
    Focus
    
    Int
    
    Modulo
    
    Solve
    
    Rat
    
    Seq
  - Multiset
    
    Make
    
    Seq
  - Multiset_intf
    
    S
    
    Seq
  - Multisets
    
    MMT
    
    Seq
    
    MT
    
    Seq
  - NPDtree
    
    Make
    
    E
    
    MakeTerm
    
    Leaf
  - Options
  - Ordering
  - Ordinal
  - Output_format
  - ParseLocation
    
    Infix
  - Polynomial
    
    IntegerModule
    
    Make
    
    Coeff
    
    Indet
    
    OrderedType
    
    S
  - Position
    
    Build
    
    Map
    
    With
    
    Infix
  - Precedence
    
    Constr
    
    Seq
    
    Weight
    
    Infix
  - Proof
    
    Kind
    
    Parent
    
    Result
    
    Rule
    
    S
    
    Tbl
    
    Src
    
    Step
  - Rat_lit
    
    Focus
    
    Seq
  - Rewrite
    
    Defined_cst
    
    Lit
    
    Rule
    
    Rule
    
    Rule_set
    
    Term
    
    Rule
    
    Rule_inst_set
    
    Set
  - SLiteral
    
    TPTP
    
    ZF
  - STerm
    
    Map
    
    Seq
    
    Set
    
    StrMap
    
    StringSet
    
    TPTP
    
    Tbl
    
    ZF
  - Scoped
  - Signal
  - Signature
    
    Seq
  - Skolem
  - Statement
    
    Seq
    
    TPTP
    
    ZF
  - Subst
    
    FO
    
    Projection
    
    Renaming
    
    SPECIALIZED
    
    Ty
  - Term
    
    AC
    
    A
    
    AC_SPEC
    
    Arith
    
    Classic
    
    Conv
    
    DB
    
    Form
    
    Map
    
    Pos
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
    
    VarMap
    
    VarSet
    
    VarTbl
    
    ZF
  - Test_prop
  - Type
    
    Conv
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
    
    VarMap
    
    VarSet
    
    VarTbl
    
    ZF
  - TypeInference
    
    Ctx
    
    TyBuiltin
  - TypedSTerm
    
    Form
    
    Seq
    
    Subst
    
    TPTP
    
    Ty
    
    UStack
    
    Var_tbl
    
    ZF
  - Unif
    
    FO
    
    Inner
    
    Ty
  - Unif_constr
    
    FO
  - Unif_intf
    
    S
  - Unif_subst
    
    FO
  - UnionFind
    
    Make
    
    P
    
    PAIR
  - UntypedAST
    
    A
  - Util
    
    Exn
    
    Flag
    
    Int_map
    
    Int_set
    
    Section
  - Var
    
    Set
    
    Subst
logtk.parsers
- Logtk_parsers
  - Ast_dk
  - Ast_tptp
  - CallProver
    
    Eprover
    
    Prover
  - Lex_dk
  - Lex_tptp
  - Lex_zf
  - Parse_dk
  - Parse_tptp
  - Parse_zf
  - Parsing_utils
  - Tip_ast
  - Tip_lexer
  - Tip_parser
  - Trace_tstp
  - Util_dk
  - Util_tip
  - Util_tptp
  - Util_zf
logtk.proofs
- Logtk_proofs
  - LLProof
    
    Dot
    
    Tbl
  - LLProof_check
  - LLProof_conv
  - LLProver
  - LLTerm
    
    Conv
    
    Form
    
    Int_op
    
    LINEXP
    
    Linexp_int
    
    Linexp_rat
    
    Rat_op
    
    Set
logtk.solving
- Logtk_solving
  - Lpo
    
    Constraint
    
    Seq
    
    FO
    
    Solution
    
    TypedSTerm

Legend:
Library
Module
Module type
Parameter
Class
Class type

Some helpers

Various helpers for the provers.

It provides counters for statistics, basic profilers, helper functions, debugging functions…

Time facilities

val total_time_s : unit -> float

time elapsed since start of program, in seconds

Misc

module Section : sig ... end

Debug section

val set_debug : int -> unit

Set debug level of Section.root

val get_debug : unit -> int

Current debug level for Section.root

val break_on_debug : bool Stdlib.ref

Shall we wait for user input after each debug message?

val debugf : 
  ?section:Section.t ->
  int ->
  ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 ->
  ('a -> unit) ->
  unit

Print a debug message, with the given section and verbosity level. The message might be dropped if its level is too high.

val debug : ?section:Section.t -> int -> string -> unit

Cheap non-formatting version of debugf

val ksprintf_noc : 
  f:(string -> 'a) ->
  ('b, Stdlib.Format.formatter, unit, 'a) Stdlib.format4 ->
  'b

Same as CCFormat.ksprintf, but without colors

val err_spf : ('b, Stdlib.Format.formatter, unit, string) Stdlib.format4 -> 'b

Version of sprintf that adds a colored "error" prefix

val warn : string -> unit

Emit warning

val warnf : ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 -> 'a

Emit warning, with formatting

exception Error of string * string

generalist error that do not really belong elsewhere. Error (where,what) means that error what was raised from where.

val error : where:string -> string -> 'a

error msg raises Error msg

raises Error
duh

val errorf : 
  where:string ->
  ('b, Stdlib.Format.formatter, unit, 'a) Stdlib.format4 ->
  'b

Formatting version of error

val pp_pos : Stdlib.Lexing.position -> string

val set_memory_limit : int -> unit

Limit the amount of memory available to the process (in MB)

val set_time_limit : int -> unit

Limit the CPU time available to the process (in seconds)

OCaml Stack

requires ocaml >= 4.01

since 0.8

module Exn : sig ... end

profiling facilities

type profiler

val enable_profiling : bool Stdlib.ref

Enable/disable profiling

val mk_profiler : string -> profiler

Create a named profiler

val enter_prof : profiler -> unit

Enter the profiler

val exit_prof : profiler -> unit

Exit the profiler

val with_prof : profiler -> ('a -> 'b) -> 'a -> 'b

Runtime statistics

type stat

val mk_stat : string -> stat

val print_global_stats : comment:string -> unit -> unit

comment prefix

val incr_stat : stat -> unit

val add_stat : stat -> int -> unit

Flags as integers

module Flag : sig ... end

Others

val finally : do_:(unit -> unit) -> (unit -> 'a) -> 'a

finally ~do_ f calls f () and returns its result. If it raises, the same exception is raised; in any case, do_ () is called after f () terminates.

val pp_pair : 
  ?sep:string ->
  'a CCFormat.printer ->
  'b CCFormat.printer ->
  ('a * 'b) CCFormat.printer

val pp_list : ?sep:string -> 'a CCFormat.printer -> 'a list CCFormat.printer

Print a list without begin/end separators

val pp_seq : ?sep:string -> 'a CCFormat.printer -> 'a Iter.t CCFormat.printer

val pp_list0 : ?sep:string -> 'a CCFormat.printer -> 'a list CCFormat.printer

Print a list with a whitespace in front if it's non empty, or does nothing if the list is empty Default separator is " "

val tstp_needs_escaping : string -> bool

Is this name a proper TSTP identifier, or does it need ' ' around it?

val pp_str_tstp : string CCFormat.printer

possibly escaping

val pp_var_tstp : string CCFormat.printer

val ord_option : 'a CCOrd.t -> 'a option CCOrd.t

val take_drop_while : ('a -> bool) -> 'a list -> 'a list * 'a list

val map_product : f:('a -> 'b list list) -> 'a list -> 'b list list

val seq_map_l : f:('a -> 'b list) -> 'a list -> 'b list Iter.t

val seq_zipi : 'a Iter.t -> (int * 'a) Iter.t

val invalid_argf : ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

val failwithf : ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

module Int_map : CCMap.S with type key = int

module Int_set : CCSet.S with type elt = int

val escape_dot : string -> string

String escaping for graphviz

File utils

type 'a or_error = ('a, string) CCResult.t

val popen : cmd:string -> input:string -> string or_error

Run the given command cmd with the given input, wait for it to terminate, and return its stdout.