Revision f6acf47b
Added by Pierre-Loïc Garoche about 9 years ago
src/options.ml | ||
---|---|---|
41 | 41 |
let horn_cex = ref false |
42 | 42 |
let horn_queries = ref false |
43 | 43 |
|
44 |
let salsa_enabled = ref false |
|
45 | 44 |
|
46 | 45 |
let set_mpfr prec = |
47 | 46 |
if prec > 0 then ( |
48 | 47 |
mpfr := true; |
49 | 48 |
mpfr_prec := prec; |
50 |
salsa_enabled := false; (* We deactivate salsa *)
|
|
49 |
(* salsa_enabled := false; (* We deactivate salsa *) TODO *)
|
|
51 | 50 |
) |
52 | 51 |
else |
53 | 52 |
failwith "mpfr requires a positive integer" |
... | ... | |
69 | 68 |
"-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend."; |
70 | 69 |
"-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)"; |
71 | 70 |
"-horn-queries", Arg.Unit (fun () -> output := "horn"; horn_queries:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)"; |
72 |
"-salsa", Arg.Set salsa_enabled, "activate Salsa optimization <default>"; |
|
73 |
"-no-salsa", Arg.Clear salsa_enabled, "deactivate Salsa optimization"; |
|
74 | 71 |
"-print_reuse", Arg.Set print_reuse, "prints variable reuse policy"; |
75 | 72 |
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations"; |
76 | 73 |
"-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding"; |
Also available in: Unified diff
Plugin based framework