Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
;;
+let pp_goal_set msg goals names =
+ let active_goals, passive_goals = goals in
+ prerr_endline ("////" ^ msg);
+ prerr_endline ("ACTIVE G: " ^
+ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
+ active_goals)));
+ prerr_endline ("PASSIVE G: " ^
+ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
+ passive_goals)))
+;;
+
let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
(*
let names = names_of_context ctx in
| (Some p) as ok -> ok
;;
-let simplify_goal_set env goals passive active =
+let simplify_goal_set env goals ?passive active =
let active_goals, passive_goals = goals in
let find (_,_,g) where =
List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
let simplified =
List.fold_left
(fun acc goal ->
- match simplify_goal env goal ~passive active with
+ match simplify_goal env goal ?passive active with
| changed, g ->
if changed then prerr_endline "???????????????cambiato ancora";
if find g acc then acc else g::acc)
let infer_goal_set env active goals =
let active_goals, passive_goals = goals in
let rec aux = function
- | [] -> goals
+ | [] -> active_goals, []
| hd::tl ->
let changed,selected = simplify_goal env hd active in
if changed then
prerr_endline ("--------------- goal semplificato");
let (_,_,t1) = selected in
- if (List.exists
- (fun (_,_,t) ->
- Equality.meta_convertibility t t1)
- active_goals) then aux tl
- else
- let passive_goals = tl in
- let new_passive_goals =
- if Utils.metas_of_term t1 = [] then passive_goals
- else
- let new' =
- Indexing.superposition_left env (snd active) selected in
- passive_goals @ new'
+ let already_in =
+ List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
+ active_goals
in
- selected::active_goals, new_passive_goals
+ if already_in then
+ aux tl
+ else
+ let passive_goals = tl in
+ let new_passive_goals =
+ if Utils.metas_of_term t1 = [] then passive_goals
+ else
+ let new' =
+ Indexing.superposition_left env (snd active) selected in
+ passive_goals @ new'
+ in
+ selected::active_goals, new_passive_goals
in
aux passive_goals
;;
let infer_goal_set_with_current env current goals =
let active_goals, passive_goals = goals in
- let _,table,_ = build_table [current] in
- active_goals,
+ let l,table,_ = build_table [current] in
+ let active_goals, _ =
+ simplify_goal_set env goals (l,table)
+ in
+ active_goals,
List.fold_left
(fun acc g ->
let new' = Indexing.superposition_left env table g in
prerr_endline (Printf.sprintf "Current goal = %s\n"
(CicPp.pp g names)))
(fst goals);
+ List.iter
+ (fun _,_,g ->
+ prerr_endline (Printf.sprintf "Passive goal = %s\n"
+ (CicPp.pp g names)))
+ (snd goals);
prerr_endline (Printf.sprintf "Selected = %s\n"
(Equality.string_of_equality ~env current))
in
let new' = infer eq_uri env current active in
prerr_endline "infer goal";
let goals = infer_goal_set_with_current env current goals in
+(*
+ match check_if_goals_set_is_solved env active goals with
+ | Some p ->
+ prerr_endline
+ (Printf.sprintf "Found a proof in: %f\n"
+ (Unix.gettimeofday() -. initial_time));
+ ParamodulationSuccess p
+ | None ->
+*)
let active =
let al, tbl = active in
al @ [current], Indexing.index tbl current
let goals =
let a,b,_ = build_table new' in
let _ = <:start<simplify_goal_set new>> in
- let rc = simplify_goal_set env goals passive (a,b) in
+ let rc = simplify_goal_set env goals ~passive (a,b) in
let _ = <:stop<simplify_goal_set new>> in
rc
in
let al, tbl = active in
al @ [current], Indexing.index tbl current
in
+ (* alla fine new' contiene anche le attive semplificate!
+ * quindi le aggiungo alle passive insieme alle new *)
let rec simplify new' active passive =
let new' = forward_simplify_new eq_uri env new' ~passive active in
let active, passive, newa, retained, pruned =
;;
let saturate
+ caso_strano
dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status =
let module C = Cic in
reset_refs ();
let res, time =
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities dbd context (proof, goalno) (maxm+2)
+ find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2)
in
let library_equalities = List.map snd library_equalities in
let t2 = Unix.gettimeofday () in
*)
let goals = make_goal_set goal in
let max_iterations = 10000 in
- let max_time = Unix.gettimeofday () +. 600. (* minutes *) in
+ let max_time = Unix.gettimeofday () +. 300. (* minutes *) in
given_clause
eq_uri env goals theorems passive active max_iterations max_time
in
let env = (metasenv, context, ugraph) in
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities dbd context (proof, goal') (maxm+2) in
+ find_library_equalities false dbd context (proof, goal') (maxm+2) in
let t2 = Unix.gettimeofday () in
maxmeta := maxm+2;
let equalities = (* equalities @ *) library_equalities in
let eq_uri = eq_of_goal goal in
let eq_indexes, equalities, maxm = find_equalities context proof in
let lib_eq_uris, library_equalities, maxm =
- find_library_equalities dbd context (proof, goal') (maxm+2)
+ find_library_equalities false dbd context (proof, goal') (maxm+2)
in
let library_equalities = List.map snd library_equalities in
maxmeta := maxm+2; (* TODO ugly!! *)
Inference.find_equalities context proof
in
let lib_eq_uris, library_equalities, maxm =
- Inference.find_library_equalities dbd context (proof, goal) (maxm+2) in
+ Inference.find_library_equalities false dbd context (proof, goal) (maxm+2) in
if library_equalities = [] then prerr_endline "VUOTA!!!";
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let library_equalities = List.map snd library_equalities in
| _ -> i
;;
-let superposition_tac ~what ~other ~subterms_only ~demodulate status =
+(* Syntax:
+ * auto superposition target = NAME
+ * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
+ *
+ * - if table is omitted no superposition will be performed
+ * - if demod_table is omitted no demodulation will be prformed
+ * - subterms_only is passed to Indexing.superposition_right
+ *
+ * lists are coded using _ (example: H_H1_H2)
+ *)
+let superposition_tac ~target ~table ~subterms_only ~demod_table status =
reset_refs();
+ Indexing.init_index ();
let proof,goalno = status in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
let env = (metasenv, context, CicUniv.empty_ugraph) in
let names = names_of_context context in
let eq_index, equalities, maxm = find_equalities context proof in
- let what = find_in_ctx 1 what context in
- let other = find_in_ctx 1 other context in
- let eq_what = List.nth equalities (position_of 0 what eq_index) in
- let eq_other = List.nth equalities (position_of 0 other eq_index) in
- let index = Indexing.index Indexing.empty eq_other in
+ let eq_what =
+ let what = find_in_ctx 1 target context in
+ List.nth equalities (position_of 0 what eq_index)
+ in
+ let eq_other =
+ if table <> "" then
+ let other =
+ let others = Str.split (Str.regexp "_") table in
+ List.map (fun other -> find_in_ctx 1 other context) others
+ in
+ List.map
+ (fun other -> List.nth equalities (position_of 0 other eq_index))
+ other
+ else
+ []
+ in
+ let index = List.fold_left Indexing.index Indexing.empty eq_other in
let maxm, eql =
+ if table = "" then maxm,[eq_what] else
Indexing.superposition_right
~subterms_only eq_uri maxm env index eq_what
in
prerr_endline ("Superposition right:");
prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
- prerr_endline ("\n table: " ^ Equality.string_of_equality eq_other ~env);
+ prerr_endline ("\n table: ");
+ List.iter (fun e -> prerr_endline (" " ^ Equality.string_of_equality e ~env)) eq_other;
prerr_endline ("\n result: ");
List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
prerr_endline ("\n result (cut&paste): ");
let t = Equality.term_of_equality eq_uri e in
prerr_endline (CicPp.pp t names))
eql;
- if demodulate then
+ if demod_table <> "" then
begin
- let table = List.fold_left Indexing.index Indexing.empty equalities in
+ let demod =
+ let demod = Str.split (Str.regexp "_") demod_table in
+ List.map (fun other -> find_in_ctx 1 other context) demod
+ in
+ let eq_demod =
+ List.map
+ (fun demod -> List.nth equalities (position_of 0 demod eq_index))
+ demod
+ in
+ let table = List.fold_left Indexing.index Indexing.empty eq_demod in
let maxm,eql =
List.fold_left
(fun (maxm,acc) e ->
let get_stats () =
<:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
- Equality.get_stats ();;
+ Equality.get_stats ()
+;;