fixed a bug (status not reset properly between calls), tried some other

[helm.git] / helm / ocaml / paramodulation / saturate_main.ml

diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml
index ab39ff3deb327587e32ef6b8393aaa42088bece2..af0861b605ef54aa758034b779e874292ac0bc86 100644 (file)
--- 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;;