-(** given-clause algorithm with full reduction strategy *)
-let rec given_clause_fullred dbd env goals theorems passive active =
-(*
- let table,list = active in
- assert (check_table list table);
-*)
- let goals = simplify_goals env goals ~passive active in
- let _,context,_ = env in
- let ok, goals = activate_goal goals in
-(* let theorems = simplify_theorems env theorems ~passive active in *)
- if ok then
- let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
- let _, _, t = List.hd (snd (List.hd (fst goals))) in
- let _ = prerr_endline ("goal activated = " ^ (CicPp.pp t names)) in
-(* let _ = *)
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" *)
-(* (print_goals (fst goals)) (print_goals (snd goals)))); *)
-(* let current = List.hd (fst goals) in *)
-(* let p, _, t = List.hd (snd current) in *)
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "goal activated:\n%s\n%s\n" *)
-(* (CicPp.ppterm t) (string_of_proof p))); *)
-(* in *)
- let ok, proof =
- (* apply_goal_to_theorems dbd env theorems ~passive active goals in *)
- let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
- match (fst goals) with
- | (_, [proof, m, Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_
- when left = right && iseq uri ->
- let p =
- Cic.Appl [Cic.MutConstruct (* reflexivity *)
- (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left]
- in
- let newp =
- let rec repl = function
- | Inference.ProofGoalBlock (_, gp) ->
- Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
- | Inference.NoProof -> Inference.BasicProof ([],p)
- | Inference.BasicProof _ -> Inference.BasicProof ([],p)
- | Inference.SubProof (t, i, p2) ->
- Inference.SubProof (t, i, repl p2)
- | _ -> assert false
- in
- repl proof
- in true, Some newp
- | _ -> false, None
- in
- if ok then
- (* let proof =
- match (fst goals) with
- | (_, [proof, m, _])::_ ->
- prerr_endline (CicMetaSubst.ppmetasenv [] m); Some proof
- | _ -> assert false
- in *)
- ( prerr_endline "esco qui";
- let active =
- List.filter test (fst active) in
- let s = Printf.sprintf "actives:\n%s\n"
- (String.concat "\n"
- ((List.map
- (fun (s, e) -> (string_of_sign s) ^ " " ^
- (string_of_equality ~env e))
- active)))
- in prerr_endline s;
- let passive =
- List.filter
- (fun x -> test (1,x))
- (let x,y,_ = passive in (fst x)@(fst y)) in
- let p = Printf.sprintf "passives:\n%s\n"
- (String.concat "\n"
- ((List.map
- (fun e ->
- (string_of_equality ~env e))
- passive)))
- in prerr_endline p;
- (*
- let s = Printf.sprintf "actives:\n%s\n"
- (String.concat "\n"
- ((List.map
- (fun (s, e) -> (string_of_sign s) ^ " " ^
- (string_of_equality ~env e))
- (fst active)))) in
- let sp = Printf.sprintf "passives:\n%s\n"
- (String.concat "\n"
- (List.map
- (string_of_equality ~env)
- (let x,y,_ = passive in (fst x)@(fst y)))) in
- prerr_endline s;
- prerr_endline sp; *)
- ParamodulationSuccess (proof, env))
- else
- given_clause_fullred_aux dbd env goals theorems passive active
- else
-(* let ok', theorems = activate_theorem theorems in *)
-(* if ok' then *)
-(* let ok, goals = apply_theorem_to_goals env theorems active goals in *)
-(* if ok then *)
-(* let proof = *)
-(* match (fst goals) with *)
-(* | (_, [proof, _, _])::_ -> Some proof *)
-(* | _ -> assert false *)
-(* in *)
-(* ParamodulationSuccess (proof, env) *)
-(* else *)
-(* given_clause_fullred_aux env goals theorems passive active *)
-(* else *)
- if (passive_is_empty passive) then ParamodulationFailure
- else given_clause_fullred_aux dbd env goals theorems passive active
-
-and given_clause_fullred_aux dbd env goals theorems passive active =
- prerr_endline (string_of_int !counter ^
- " MAXMETA: " ^ string_of_int !maxmeta ^
- " LOCALMAX: " ^ string_of_int !Indexing.local_max ^
- " #ACTIVES: " ^ string_of_int (size_of_active active) ^
- " #PASSIVES: " ^ string_of_int (size_of_passive passive));
- incr counter;
-(* if !counter mod 10 = 0 then
- begin
- let size = HExtlib.estimate_size (passive,active) in
- let sizep = HExtlib.estimate_size (passive) in
- let sizea = HExtlib.estimate_size (active) in
- let (l1,s1),(l2,s2), t = passive in
- let sizetbl = HExtlib.estimate_size t in
- let sizel = HExtlib.estimate_size (l1,l2) in
- let sizes = HExtlib.estimate_size (s1,s2) in
-
- prerr_endline ("SIZE: " ^ string_of_int size);
- prerr_endline ("SIZE P: " ^ string_of_int sizep);
- prerr_endline ("SIZE A: " ^ string_of_int sizea);
- prerr_endline ("SIZE TBL: " ^ string_of_int sizetbl ^
- " SIZE L: " ^ string_of_int sizel ^
- " SIZE S:" ^ string_of_int sizes);
- end;*)
-(*
- if (size_of_active active) mod 50 = 0 then
- (let s = Printf.sprintf "actives:\n%s\n"
- (String.concat "\n"
- ((List.map
- (fun (s, e) -> (string_of_sign s) ^ " " ^
- (string_of_equality ~env e))
- (fst active)))) in
- let sp = Printf.sprintf "passives:\n%s\n"
- (String.concat "\n"
- (List.map
- (string_of_equality ~env)
- (let x,y,_ = passive in (fst x)@(fst y)))) in
- prerr_endline s;
- prerr_endline sp); *)
- let time1 = Unix.gettimeofday () in
- let (_,context,_) = env in
- let selection_estimate = get_selection_estimate () in
- let kept = size_of_passive passive in
- let passive =
- if !time_limit = 0. || !processed_clauses = 0 then
- passive
- else if !elapsed_time > !time_limit then (
- debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
- !time_limit !elapsed_time));
- make_passive [] []
- ) else if kept > selection_estimate then (
- debug_print
- (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
- "(kept: %d, selection_estimate: %d)\n")
- kept selection_estimate));
- prune_passive selection_estimate active passive
- ) else
- passive