package libzipperposition

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = {
  1. ord : string;
  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. dot_file : string option;
    (*

    file to print the final state in

    *)
  10. dot_llproof : string option;
    (*

    file to print llproof

    *)
  11. dot_sat : bool;
    (*

    Print saturated set into DOT?

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

    prefix for printing checker proofs

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

    expand definitions

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

    initial interreduction of proof state?

    *)
  18. unary_depth : int;
    (*

    Maximum successive levels of unary inferences

    *)
  19. check : bool;
    (*

    check proof

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

Innovation. Community. Security.