X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturate_main.ml;h=af0861b605ef54aa758034b779e874292ac0bc86;hb=e9a76af2c3c2a70f26b0315225b596bcba1a585d;hp=ab39ff3deb327587e32ef6b8393aaa42088bece2;hpb=890385fa69623abbcfbfe758218c080b7c80903e;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml
index ab39ff3de..af0861b60 100644
--- a/helm/ocaml/paramodulation/saturate_main.ml
+++ b/helm/ocaml/paramodulation/saturate_main.ml
@@ -15,6 +15,8 @@ let get_from_user ~(dbd:HMysql.dbd) =
   term, metasenv, ugraph
 ;;
 
+let full = ref false;;
+
 let _ =
   let module S = Saturation in
   let set_ratio v = S.weight_age_ratio := v; S.weight_age_counter := v
@@ -30,8 +32,10 @@ let _ =
   and set_time_limit v = S.time_limit := float_of_int v
   and set_width w = S.maxwidth := w
   and set_depth d = S.maxdepth := d
+  and set_full () = full := true
   in
   Arg.parse [
+    "-full", Arg.Unit set_full, "Enable full mode";
     "-f", Arg.Bool set_fullred,
     "Enable/disable full-reduction strategy (default: enabled)";
     
@@ -67,4 +71,4 @@ let dbd = HMysql.quick_connect
   ()
 in
 let term, metasenv, ugraph = get_from_user ~dbd in
-Saturation.main dbd term metasenv ugraph;;
+Saturation.main dbd !full term metasenv ugraph;;