ord : string Stdlib.ref; |
seed : int; |
steps : int; |
version : bool; |
timeout : float; |
prelude : (string, CCVector.ro) CCVector.t; |
files : (string, CCVector.ro) CCVector.t; |
select : string; | name of the selection function |
dot_file : string option; | file to print the final state in |
dot_llproof : string option; | file to print llproof |
dot_sat : bool; | Print saturated set into DOT? |
dot_all_roots : bool; |
dot_check : string option; | prefix for printing checker proofs |
def_as_rewrite : bool; |
expand_def : bool; | expand definitions |
stats : bool; |
presaturate : bool; | initial interreduction of proof state? |
unary_depth : int; | Maximum successive levels of unary inferences |
check : bool; | check proof |