let retrieve_only = ref false;;
+let demod_equalities = ref false;;
+
let _ =
let module S = Saturation in
let set_ratio v = S.weight_age_ratio := v; S.weight_age_counter := v
and set_depth d = S.maxdepth := d
and set_full () = full := true
and set_retrieve () = retrieve_only := true
+ and set_demod_equalities () = demod_equalities := true
in
Arg.parse [
"-full", Arg.Unit set_full, "Enable full mode";
Printf.sprintf "Maximal depth (default: %d)" !Saturation.maxdepth;
"-retrieve", Arg.Unit set_retrieve, "retrieve only";
+ "-demod-equalities", Arg.Unit set_demod_equalities, "demod equalities";
] (fun a -> ()) "Usage:"
in
Helm_registry.load_from !configuration_file;
let term, metasenv, ugraph = get_from_user ~dbd in
if !retrieve_only then
Saturation.retrieve_and_print dbd term metasenv ugraph
+else if !demod_equalities then
+ Saturation.main_demod_equalities dbd term metasenv ugraph
else
Saturation.main dbd !full term metasenv ugraph
;;