-(* let refl_equal = *)
-(* CicUtil.term_of_uri *)
-(* (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *)
-(* in *)
- let goals = simplify_goals env goals ~passive active in
- let theorems = simplify_theorems env theorems ~passive active in
- let is_passive_empty = passive_is_empty passive in
- try
- let ok, goals = apply_to_goals env is_passive_empty theorems active goals in
- if ok then
- let proof =
- match goals with
- | (_, [proof, _, _])::_ -> Some proof
- | _ -> assert false
- in
- ParamodulationSuccess (proof, env)
- else
- let _ =
- debug_print
- (lazy ("new_goals: " ^ (string_of_int (List.length goals))));
- debug_print
- (lazy
- (String.concat "\n"
- (List.map
- (fun (d, gl) ->
- let gl' =
- List.map
- (fun (p, _, t) ->
- (string_of_proof p) ^ ", " ^ (CicPp.ppterm t)) gl
- in
- Printf.sprintf "%d: %s" d (String.concat "; " gl'))
- goals)));
- in
- match is_passive_empty (* passive_is_empty passive *) with
- | true -> (* ParamodulationFailure *)
- given_clause_fullred env goals theorems passive active
- | false ->
- let (sign, current), passive = select env goals passive active in
- let time1 = Unix.gettimeofday () in
- let res = forward_simplify env (sign, current) ~passive active in
- let time2 = Unix.gettimeofday () in
- forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
- match res with
- | None ->
- given_clause_fullred env goals theorems passive active
- | Some (sign, current) ->
- if (sign = Negative) && (is_identity env current) then (
- debug_print
- (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
- (string_of_equality ~env current)));
- let _, proof, _, _, _ = current in
- ParamodulationSuccess (Some proof (* current *), env)
- ) else (
- debug_print
- (lazy "\n================================================");
- debug_print (lazy (Printf.sprintf "selected: %s %s"
- (string_of_sign sign)
- (string_of_equality ~env current)));
-
- let t1 = Unix.gettimeofday () in
- let new' = infer env sign current active in
- let t2 = Unix.gettimeofday () in
- infer_time := !infer_time +. (t2 -. t1);
-
- let active =
- if is_identity env current then active
- else
- let al, tbl = active in
- match sign with
- | Negative -> (sign, current)::al, tbl
- | Positive ->
- al @ [(sign, current)], Indexing.index tbl current
- in
- let rec simplify new' active passive =
- let t1 = Unix.gettimeofday () in
- let new' = forward_simplify_new env new' ~passive active in
- let t2 = Unix.gettimeofday () in
- forward_simpl_new_time :=
- !forward_simpl_new_time +. (t2 -. t1);
- let t1 = Unix.gettimeofday () in
- let active, passive, newa, retained =
- backward_simplify env new' ~passive active in
- let t2 = Unix.gettimeofday () in
- backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
- match newa, retained with
- | None, None -> active, passive, new'
- | Some (n, p), None
- | None, Some (n, p) ->
- let nn, np = new' in
- simplify (nn @ n, np @ p) active passive
- | Some (n, p), Some (rn, rp) ->
- let nn, np = new' in
- simplify (nn @ n @ rn, np @ p @ rp) active passive
- in
- let active, passive, new' = simplify new' active passive in
-
- let k = size_of_passive passive in
- if k < (kept - 1) then
- processed_clauses := !processed_clauses + (kept - 1 - k);
-
- let _ =