Added a couple of flags to auto

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

diff --git a/components/tactics/autoTypes.ml b/components/tactics/autoTypes.ml
index 93205c8362f5289957ce06f8d3973bd844c69a42..9031a0338736fa152c1efd1add013abc95a66b5c 100644 (file)
--- a/components/tactics/autoTypes.ml
+++ b/components/tactics/autoTypes.ml
@@ -27,8 +27,10 @@ type flags = {
   maxwidth: int;
   maxdepth: int;
   timeout: float;
+  use_library: bool;
   use_paramod: bool;
   use_only_paramod : bool;
+  close_more : bool; 
   dont_cache_failures: bool;
 }
 
@@ -36,8 +38,10 @@ let default_flags _ =
   {maxwidth=3;
    maxdepth=3;
    timeout=Unix.gettimeofday() +.3.0;
+   use_library=true;
    use_paramod=true;
    use_only_paramod=false;
+   close_more=false; 
    dont_cache_failures=false}
 ;;
 

diff --git a/components/tactics/autoTypes.mli b/components/tactics/autoTypes.mli
index d3081b0abe9f10bb8d81f7b8cab027e881ddca7c..5014f41ce10d6eb75c60a6b2ec1a768cf5120ae0 100644 (file)
--- a/components/tactics/autoTypes.mli
+++ b/components/tactics/autoTypes.mli
@@ -27,8 +27,10 @@ type flags = {
   maxwidth: int;
   maxdepth: int;
   timeout: float;
+  use_library: bool;
   use_paramod: bool;
   use_only_paramod : bool;
+  close_more : bool;
   dont_cache_failures: bool
 }