Source file params.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
(** {1 Parameters for the prover, etc.} *)
open Logtk
type t = {
ord : string;
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 *)
eta: [`Reduce | `Expand | `None]; (** eta conversion *)
}
let default : t = {
ord= "kbo";
seed = 1928575;
steps = -1;
version= false;
timeout = 0.;
prelude= CCVector.create() |> CCVector.freeze;
files = CCVector.create() |> CCVector.freeze;
select = "default";
stats= !Options._stats;
def_as_rewrite= true;
presaturate = false;
dot_all_roots= false;
dot_file = None;
dot_llproof= None;
dot_check=None;
unary_depth= 1;
dot_sat= false;
expand_def= false;
check= false;
eta = `Reduce;
}
let select = ref default.select
let _modes = Hashtbl.create 10
let mode_spec () =
Arg.Symbol
(List.sort_uniq String.compare (CCHashtbl.keys_list _modes),
fun s -> List.iter (fun f -> f ()) (Hashtbl.find_all _modes s))
let add_to_mode mode f =
Hashtbl.add _modes mode f
(** parse_args returns parameters *)
let parse_args () =
let ord = ref default.ord
and seed = ref default.seed
and steps = ref default.steps
and version = ref default.version
and timeout = ref default.timeout
and presaturate = ref default.presaturate
and dot_file = ref default.dot_file
and dot_llproof = ref default.dot_llproof
and dot_sat = ref default.dot_sat
and dot_all_roots = ref default.dot_all_roots
and dot_check = ref default.dot_check
and expand_def = ref default.expand_def
and unary_depth = ref default.unary_depth
and def_as_rewrite = ref default.def_as_rewrite
and prelude = CCVector.create()
and files = CCVector.create ()
and check = ref default.check
and eta = ref `Reduce
in
let eta_opt =
let set_ n = eta := n in
let l = [ "reduce", `Reduce; "expand", `Expand; "none", `None] in
Arg.Symbol (List.map fst l, fun s -> set_ (List.assoc s l))
in
let add_file s = CCVector.push files s in
let options = (
[ "--mode", mode_spec (), " mode"
; "--ord", Arg.Set_string ord, " choose ordering (rpo,kbo)"
; "--version", Arg.Set version, " print version"
; "--steps", Arg.Set_int steps,
" maximal number of steps of given clause loop (no limit if negative)"
; "--timeout", Arg.Set_float timeout, " timeout (in seconds)"
; "-t", Arg.Set_float timeout, " short for --timeout"
; "--expand-def", Arg.Set expand_def, " expand definitions"
; "--presaturate", Arg.Set presaturate,
" pre-saturate (interreduction of) the initial clause set"
; "--dot", Arg.String (fun s -> dot_file := Some s) , " print final state to file in DOT"
; "--dot-llproof", Arg.String (fun s -> dot_llproof := Some s) , " print LLProof to file in DOT"
; "--dot-sat", Arg.Set dot_sat, " print saturated set into DOT"
; "--dot-all-roots", Arg.Set dot_all_roots, " print all empty clauses into DOT"
; "--dot-check-prefix", Arg.String (fun s-> dot_check :=Some s), " prefix for printing checker proofs in DOT"
; "--color", Arg.Bool CCFormat.set_color_default, " enable/disable ANSI color codes"
; "--seed", Arg.Set_int seed, " set random seed"
; "--unary-depth", Arg.Set_int unary_depth, " maximum depth for successive unary inferences"
; "--def-as-rewrite", Arg.Set def_as_rewrite, " treat definitions as rewrite rules"
; "--def-as-assert", Arg.Clear def_as_rewrite, " treat definitions as axioms"
; "--check", Arg.Set check, " check proof"
; "--prelude", Arg.String (CCVector.push prelude), " parse prelude file"
; "--no-check", Arg.Clear check, " do not check proof"
; "--ho-eta", eta_opt, " eta-expansion/reduction"
] @ Options.make ()
) |> List.sort (fun (s1,_,_)(s2,_,_) -> String.compare s1 s2)
|> Arg.align
in
Arg.parse options add_file "solve problems in files";
if CCVector.is_empty files then (
CCVector.push files "stdin";
if !Options.input = Options.I_guess then Options.input := Options.I_zf;
);
let prelude = CCVector.freeze prelude in
let files = CCVector.freeze files in
{ ord= !ord; seed = !seed; steps = !steps;
version= !version; timeout = !timeout; prelude= prelude;
files = files; select = !select;
stats= ! Options._stats; def_as_rewrite= !def_as_rewrite;
presaturate = !presaturate; dot_all_roots= !dot_all_roots;
dot_file = !dot_file; dot_llproof= !dot_llproof;
dot_check= !dot_check;
unary_depth= !unary_depth; dot_sat= !dot_sat;
expand_def= !expand_def; check= !check; eta = !eta}
let add_opt = Options.add_opt
let add_opts = Options.add_opts
let key : t Flex_state.key = Flex_state.create_key()