From f3db9a0fa7715783e93e4f927d5c73bff28090fa Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Thu, 21 Jul 2005 11:45:58 +0000 Subject: [PATCH] entry point of the stand-alone saturate --- helm/ocaml/paramodulation/saturate_main.ml | 52 ++++++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 helm/ocaml/paramodulation/saturate_main.ml diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml new file mode 100644 index 000000000..c9eec5e46 --- /dev/null +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -0,0 +1,52 @@ +let configuration_file = ref "../../matita/matita.conf.xml";; + +let get_from_user ~(dbd:Mysql.dbd) = + let rec get () = + match read_line () with + | "" -> [] + | t -> t::(get ()) + in + let term_string = String.concat "\n" (get ()) in + let env, metasenv, term, ugraph = + List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0 + in + term, metasenv, ugraph +;; + +let _ = + let module S = Saturation in + let set_ratio v = S.weight_age_ratio := (v+1); S.weight_age_counter := (v+1) + and set_sel v = S.symbols_ratio := v; S.symbols_counter := v; + and set_conf f = configuration_file := f + and set_lpo () = Utils.compare_terms := Utils.lpo + and set_kbo () = Utils.compare_terms := Utils.nonrec_kbo + and set_fullred b = S.use_fullred := b + and set_time_limit v = S.time_limit := float_of_int v + in + Arg.parse [ + "-f", Arg.Bool set_fullred, + "Enable/disable full-reduction strategy (default: enabled)"; + + "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 3)"; + + "-s", Arg.Int set_sel, + "symbols-based selection ratio (relative to the weight ratio, default: 2)"; + + "-c", Arg.String set_conf, "Configuration file (for the db connection)"; + + "-lpo", Arg.Unit set_lpo, "Use lpo term ordering"; + + "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)"; + + "-l", Arg.Int set_time_limit, "Time limit (in seconds)"; + ] (fun a -> ()) "Usage:" +in +Helm_registry.load_from !configuration_file; +let dbd = Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () +in +let term, metasenv, ugraph = get_from_user ~dbd in +Saturation.main dbd term metasenv ugraph;; -- 2.39.2