package libzipperposition

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = {
  1. ord : string ref;
  2. seed : int;
  3. steps : int;
  4. version : bool;
  5. timeout : float;
  6. prelude : (string, CCVector.ro) CCVector.t;
  7. files : (string, CCVector.ro) CCVector.t;
  8. select : string;
    (*

    name of the selection function

    *)
  9. bool_select : string;
    (*

    name of the boolean selection function

    *)
  10. dot_file : string option;
    (*

    file to print the final state in

    *)
  11. dot_llproof : string option;
    (*

    file to print llproof

    *)
  12. dot_sat : bool;
    (*

    Print saturated set into DOT?

    *)
  13. dot_all_roots : bool;
  14. dot_check : string option;
    (*

    prefix for printing checker proofs

    *)
  15. def_as_rewrite : bool;
  16. expand_def : bool;
    (*

    expand definitions

    *)
  17. stats : bool;
  18. presaturate : bool;
    (*

    initial interreduction of proof state?

    *)
  19. unary_depth : int;
    (*

    Maximum successive levels of unary inferences

    *)
  20. check : bool;
    (*

    check proof

    *)
}
val parse_args : unit -> t
val default : t
val add_opt : (string * Arg.spec * string) -> unit
val add_opts : (string * Arg.spec * string) list -> unit
val add_to_mode : string -> (unit -> unit) -> unit
val add_to_modes : string list -> (unit -> unit) -> unit
OCaml

Innovation. Community. Security.