Logtk.Util · logtk 1.6 · OCaml Packages

logtk

Core types and algorithms for logic

Version

Overview Documentation

IN THIS PACKAGE

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

Module Logtk . Util

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 ref

Shall we wait for user input after each debug message?

val debugf : 
  ?section:Section.t ->
  int ->
  ( 'a, Format.formatter, unit, unit ) 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, Format.formatter, unit, 'a ) format4 ->
  'b

Same as CCFormat.ksprintf, but without colors

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

Version of sprintf that adds a colored "error" prefix

val warn : string -> unit

Emit warning

val warnf : ( 'a, Format.formatter, unit, unit ) 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, Format.formatter, unit, 'a ) format4 -> 'b

Formatting version of error

val pp_pos : 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 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, Format.formatter, unit, 'b ) format4 -> 'a

val failwithf : ( 'a, Format.formatter, unit, 'b ) 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.