Added a couple of flags to auto

[helm.git] / components / tactics / auto.ml

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 06aa8b303496b17942cc7e62d774ce510617bb88..698053b40d48fff8c92823522f6aec05056abdf5 100644 (file)
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -933,9 +933,11 @@ let int params name default =
 let flags_of_params params ?(for_applyS=false) () =
  let int = int params in
  let bool = bool params in
+ let close_more = bool "close_more" false in
  let use_paramod = bool "use_paramod" true in
  let use_only_paramod =
   if for_applyS then true else bool "paramodulation" false in
+ let use_library = bool "library" (not use_only_paramod) in
  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
  let timeout = int "timeout" 0 in
@@ -948,9 +950,11 @@ let flags_of_params params ?(for_applyS=false) () =
        else
          infinity
       else
-       Unix.gettimeofday() +. (float_of_int timeout); 
+       Unix.gettimeofday() +. (float_of_int timeout);
+    AutoTypes.use_library = use_library; 
     AutoTypes.use_paramod = use_paramod;
     AutoTypes.use_only_paramod = use_only_paramod;
+    AutoTypes.close_more = close_more;
     AutoTypes.dont_cache_failures = false;
   }
 
@@ -1111,11 +1115,14 @@ let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
       let _,context,_ = CicUtil.lookup_meta goal metasenv in
       let flags = flags_of_params params () in
       (* just for testing *)
-      let use_library = not flags.use_only_paramod in
+      let use_library = flags.use_library in
       let tables,cache,newmeta =
        init_cache_and_tables dbd use_library (proof, goal) in
       let tables,cache,newmeta =
-       close_more tables newmeta context (proof, goal) auto_all_solutions cache in
+        if flags.close_more then
+         close_more 
+           tables newmeta context (proof, goal) auto_all_solutions cache 
+       else tables,cache,newmeta in
       let initial_time = Unix.gettimeofday() in
       let (_,oldmetasenv,_,_) = proof in
       let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in