-let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
- ?full ~(dbd:HMysql.dbd) () =
- let auto_tac dbd (proof, goal) =
- let normal_auto () =
- let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in
- Hashtbl.clear inspected_goals;
- debug_print (lazy "Entro in Auto");
- let id t = t in
- let t1 = Unix.gettimeofday () in
- match
- auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)]
- with
- [] -> debug_print(lazy "Auto failed");
- raise (ProofEngineTypes.Fail (lazy "No Applicable theorem"))
- | (_,(proof,[],_))::_ ->
- let t2 = Unix.gettimeofday () in
- debug_print (lazy "AUTO_TAC HA FINITO");
- let _,_,p,_ = proof in
- debug_print (lazy (CicPp.ppterm p));
- debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
- (proof,[])
- | _ -> assert false
- in
- let full = match full with None -> false | Some _ -> true in
- let paramodulation_ok =
- match paramodulation with
- | None -> false
- | Some _ ->
- let _, metasenv, _, _ = proof in
- let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
- full || (Equality.term_is_equality meta_goal)
- in
- if paramodulation_ok then (
- debug_print (lazy "USO PARAMODULATION...");
-(* try *)
- try
- let rc = Saturation.saturate dbd ~depth ~width ~full (proof, goal) in
- prerr_endline (Saturation.get_stats ());
- rc
- with exn ->
- prerr_endline (Saturation.get_stats ());
- raise exn
-
-(* with ProofEngineTypes.Fail _ -> *)
-(* normal_auto () *)
- ) else
- normal_auto ()
- in
- ProofEngineTypes.mk_tactic (auto_tac dbd)
+let int params name default =
+ try int_of_string (List.assoc name params) with
+ | Not_found -> default
+ | Failure _ ->
+ raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
+;;
+
+let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
+ (* argument parsing *)
+ let int = int params
+ and string = string params
+ and bool = bool params in
+ let newauto = bool "new" false 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
+ let use_paramod = bool "use_paramod" true in
+ let use_only_paramod = bool "paramodulation" false in
+ (* hacks to debug paramod *)
+ let superposition = bool "superposition" false in
+ let target = string "target" "" in
+ let table = string "table" "" in
+ let subterms_only = bool "subterms_only" false in
+ let demod_table = string "demod_table" "" in
+ let newauto = if use_only_paramod then true else newauto in
+ match superposition with
+ | true ->
+ (* this is the ugly hack to debug paramod *)
+ Saturation.superposition_tac
+ ~target ~table ~subterms_only ~demod_table (proof,goal)
+ | false ->
+ if not newauto then
+ auto_tac_old ~depth ~width ~dbd () (proof,goal)
+ else
+ (* this is the real auto *)
+ let _, metasenv, _, _ = proof in
+ let _, context, goalty = CicUtil.lookup_meta goal metasenv in
+ let cache =
+ let cache =
+ AutoCache.cache_add_context context metasenv AutoCache.cache_empty
+ in
+ if use_only_paramod then (* only paramod *)
+ cache
+ else
+ AutoCache.cache_add_library dbd proof [goal] cache
+ in
+ let oldmetasenv = metasenv in
+ let flags = {
+ AutoTypes.maxdepth =
+ if use_only_paramod then 2 else depth;
+ AutoTypes.maxwidth = width;
+ AutoTypes.timeout =
+ if timeout = 0 then float_of_int timeout
+ else Unix.gettimeofday() +. (float_of_int timeout);
+ AutoTypes.use_paramod = use_paramod;
+ AutoTypes.use_only_paramod = use_only_paramod;
+ AutoTypes.dont_cache_failures = false
+ }
+ in
+ match Auto.auto dbd cache context metasenv [goal] flags with
+ | None,cache ->
+ raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+ | Some (subst,metasenv),cache ->
+ let proof,metasenv =
+ ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+ proof goal (CicMetaSubst.apply_subst subst) metasenv
+ in
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:metasenv
+ in
+ proof,opened