helm/ocaml/paramodulation/saturation.ml

   1 open Inference;;
   2 open Utils;;
   3
   4
   5 (* set to false to disable paramodulation inside auto_tac *)
   6 let connect_to_auto = true;;
   7
   8
   9 (* profiling statistics... *)
  10 let infer_time = ref 0.;;
  11 let forward_simpl_time = ref 0.;;
  12 let forward_simpl_new_time = ref 0.;;
  13 let backward_simpl_time = ref 0.;;
  14 let passive_maintainance_time = ref 0.;;
  15
  16 (* limited-resource-strategy related globals *)
  17 let processed_clauses = ref 0;; (* number of equalities selected so far... *)
  18 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
  19 let start_time = ref 0.;; (* time at which the execution started *)
  20 let elapsed_time = ref 0.;;
  21 (* let maximal_weight = ref None;; *)
  22 let maximal_retained_equality = ref None;;
  23
  24 (* equality-selection related globals *)
  25 let use_fullred = ref true;;
  26 let weight_age_ratio = ref (* 5 *) 4;; (* settable by the user *)
  27 let weight_age_counter = ref !weight_age_ratio;;
  28 let symbols_ratio = ref (* 0 *) 3;;
  29 let symbols_counter = ref 0;;
  30
  31 (* non-recursive Knuth-Bendix term ordering by default *)
  32 Utils.compare_terms := Utils.nonrec_kbo;;
  33
  34 (* statistics... *)
  35 let derived_clauses = ref 0;;
  36 let kept_clauses = ref 0;;
  37
  38 (* index of the greatest Cic.Meta created - TODO: find a better way! *)
  39 let maxmeta = ref 0;;
  40
  41
  42 type result =
  43   | ParamodulationFailure
  44   | ParamodulationSuccess of Inference.equality option * environment
  45 ;;
  46
  47
  48 (*
  49 let symbols_of_equality (_, (_, left, right), _, _) =
  50   TermSet.union (symbols_of_term left) (symbols_of_term right)
  51 ;;
  52 *)
  53
  54 let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
  55   let m1 = symbols_of_term left in
  56   let m =
  57     TermMap.fold
  58       (fun k v res ->
  59          try
  60            let c = TermMap.find k res in
  61            TermMap.add k (c+v) res
  62          with Not_found ->
  63            TermMap.add k v res)
  64       (symbols_of_term right) m1
  65   in
  66 (*   Printf.printf "symbols_of_equality %s:\n" *)
  67 (*     (string_of_equality equality); *)
  68 (*   TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
  69 (*   print_newline (); *)
  70   m
  71 ;;
  72
  73
  74 module OrderedEquality = struct
  75   type t = Inference.equality
  76
  77   let compare eq1 eq2 =
  78     match meta_convertibility_eq eq1 eq2 with
  79     | true -> 0
  80     | false ->
  81         let w1, _, (ty, left, right, _), _, a = eq1
  82         and w2, _, (ty', left', right', _), _, a' = eq2 in
  83 (*         let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
  84 (*         let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
  85 (*         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)
  86         match Pervasives.compare w1 w2 with
  87         | 0 ->
  88             let res = (List.length a) - (List.length a') in
  89             if res <> 0 then res else (
  90               try
  91                 let res = Pervasives.compare (List.hd a) (List.hd a') in
  92                 if res <> 0 then res else Pervasives.compare eq1 eq2
  93               with Failure "hd" -> Pervasives.compare eq1 eq2
  94 (*               match a, a' with *)
  95 (*               | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
  96 (*                   let res = Pervasives.compare i j in *)
  97 (*                   if res <> 0 then res else Pervasives.compare eq1 eq2 *)
  98 (*               | _, _ -> Pervasives.compare eq1 eq2 *)
  99             )
 100         | res -> res
 101 end
 102
 103 module EqualitySet = Set.Make(OrderedEquality);;
 104
 105
 106 let select env passive (active, _) =
 107   processed_clauses := !processed_clauses + 1;
 108
 109   let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
 110   let remove eq l =
 111     List.filter (fun e -> e <> eq) l
 112   in
 113   if !weight_age_ratio > 0 then
 114     weight_age_counter := !weight_age_counter - 1;
 115   match !weight_age_counter with
 116   | 0 -> (
 117       weight_age_counter := !weight_age_ratio;
 118       match neg_list, pos_list with
 119       | hd::tl, pos ->
 120           (* Negatives aren't indexed, no need to remove them... *)
 121           (Negative, hd),
 122           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
 123       | [], hd::tl ->
 124           let passive_table =
 125             Indexing.remove_index passive_table hd
 126 (*             if !use_fullred then Indexing.remove_index passive_table hd *)
 127 (*             else passive_table *)
 128           in
 129           (Positive, hd),
 130           (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
 131       | _, _ -> assert false
 132     )
 133   | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
 134       symbols_counter := !symbols_counter - 1;
 135       let cardinality map =
 136         TermMap.fold (fun k v res -> res + v) map 0
 137       in
 138       match active with
 139       | (Negative, e)::_ ->
 140           let symbols = symbols_of_equality e in
 141           let card = cardinality symbols in
 142           let foldfun k v (r1, r2) =
 143             if TermMap.mem k symbols then
 144               let c = TermMap.find k symbols in
 145               let c1 = abs (c - v) in
 146               let c2 = v - c1 in
 147               r1 + c2, r2 + c1
 148             else
 149               r1, r2 + v
 150           in
 151           let f equality (i, e) =
 152             let common, others =
 153               TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 154             in
 155             let c = others + (abs (common - card)) in
 156             if c < i then (c, equality)
 157 (*             else if c = i then *)
 158 (*               match OrderedEquality.compare equality e with *)
 159 (*               | -1 -> (c, equality) *)
 160 (*               | res -> (i, e) *)
 161             else (i, e)
 162           in
 163           let e1 = EqualitySet.min_elt pos_set in
 164           let initial =
 165             let common, others =
 166               TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 167             in
 168             (others + (abs (common - card))), e1
 169           in
 170           let _, current = EqualitySet.fold f pos_set initial in
 171 (*           Printf.printf "\nsymbols-based selection: %s\n\n" *)
 172 (*             (string_of_equality ~env current); *)
 173           let passive_table =
 174             Indexing.remove_index passive_table current
 175 (*             if !use_fullred then Indexing.remove_index passive_table current *)
 176 (*             else passive_table *)
 177           in
 178           (Positive, current),
 179           (([], neg_set),
 180            (remove current pos_list, EqualitySet.remove current pos_set),
 181            passive_table)
 182       | _ ->
 183           let current = EqualitySet.min_elt pos_set in
 184           let passive_table =
 185             Indexing.remove_index passive_table current
 186 (*             if !use_fullred then Indexing.remove_index passive_table current *)
 187 (*             else passive_table *)
 188           in
 189           let passive =
 190             (neg_list, neg_set),
 191             (remove current pos_list, EqualitySet.remove current pos_set),
 192             passive_table
 193           in
 194           (Positive, current), passive
 195     )
 196   | _ ->
 197       symbols_counter := !symbols_ratio;
 198       let set_selection set = EqualitySet.min_elt set in
 199       if EqualitySet.is_empty neg_set then
 200         let current = set_selection pos_set in
 201         let passive =
 202           (neg_list, neg_set),
 203           (remove current pos_list, EqualitySet.remove current pos_set),
 204           Indexing.remove_index passive_table current
 205 (*           if !use_fullred then Indexing.remove_index passive_table current *)
 206 (*           else passive_table *)
 207         in
 208         (Positive, current), passive
 209       else
 210         let current = set_selection neg_set in
 211         let passive =
 212           (remove current neg_list, EqualitySet.remove current neg_set),
 213           (pos_list, pos_set),
 214           passive_table
 215         in
 216         (Negative, current), passive
 217 ;;
 218
 219
 220 let make_passive neg pos =
 221   let set_of equalities =
 222     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
 223   in
 224   let table =
 225       List.fold_left (fun tbl e -> Indexing.index tbl e)
 226         (Indexing.empty_table ()) pos
 227 (*     if !use_fullred then *)
 228 (*       List.fold_left (fun tbl e -> Indexing.index tbl e) *)
 229 (*         (Indexing.empty_table ()) pos *)
 230 (*     else *)
 231 (*       Indexing.empty_table () *)
 232   in
 233   (neg, set_of neg),
 234   (pos, set_of pos),
 235   table
 236 ;;
 237
 238
 239 let make_active () =
 240   [], Indexing.empty_table ()
 241 ;;
 242
 243
 244 let add_to_passive passive (new_neg, new_pos) =
 245   let (neg_list, neg_set), (pos_list, pos_set), table = passive in
 246   let ok set equality = not (EqualitySet.mem equality set) in
 247   let neg = List.filter (ok neg_set) new_neg
 248   and pos = List.filter (ok pos_set) new_pos in
 249   let table =
 250       List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
 251 (*     if !use_fullred then *)
 252 (*       List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
 253 (*     else *)
 254 (*       table *)
 255   in
 256   let add set equalities =
 257     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
 258   in
 259   (neg @ neg_list, add neg_set neg),
 260   (pos_list @ pos, add pos_set pos),
 261   table
 262 ;;
 263
 264
 265 let passive_is_empty = function
 266   | ([], _), ([], _), _ -> true
 267   | _ -> false
 268 ;;
 269
 270
 271 let size_of_passive ((_, ns), (_, ps), _) =
 272   (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
 273 ;;
 274
 275
 276 let size_of_active (active_list, _) =
 277   List.length active_list
 278 ;;
 279
 280
 281 let prune_passive howmany (active, _) passive =
 282   let (nl, ns), (pl, ps), tbl = passive in
 283   let howmany = float_of_int howmany
 284   and ratio = float_of_int !weight_age_ratio in
 285   let round v =
 286     let t = ceil v in
 287     int_of_float (if t -. v < 0.5 then t else v)
 288   in
 289   let in_weight = round (howmany *. ratio /. (ratio +. 1.))
 290   and in_age = round (howmany /. (ratio +. 1.)) in
 291   debug_print (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
 292   let symbols, card =
 293     match active with
 294     | (Negative, e)::_ ->
 295         let symbols = symbols_of_equality e in
 296         let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
 297         Some symbols, card
 298     | _ -> None, 0
 299   in
 300   let counter = ref !symbols_ratio in
 301   let rec pickw w ns ps =
 302     if w > 0 then
 303       if not (EqualitySet.is_empty ns) then
 304         let e = EqualitySet.min_elt ns in
 305         let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
 306         EqualitySet.add e ns', ps
 307       else if !counter > 0 then
 308         let _ =
 309           counter := !counter - 1;
 310           if !counter = 0 then counter := !symbols_ratio
 311         in
 312         match symbols with
 313         | None ->
 314             let e = EqualitySet.min_elt ps in
 315             let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 316             ns, EqualitySet.add e ps'
 317         | Some symbols ->
 318             let foldfun k v (r1, r2) =
 319               if TermMap.mem k symbols then
 320                 let c = TermMap.find k symbols in
 321                 let c1 = abs (c - v) in
 322                 let c2 = v - c1 in
 323                 r1 + c2, r2 + c1
 324               else
 325                 r1, r2 + v
 326             in
 327             let f equality (i, e) =
 328               let common, others =
 329                 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 330               in
 331               let c = others + (abs (common - card)) in
 332               if c < i then (c, equality)
 333               else (i, e)
 334             in
 335             let e1 = EqualitySet.min_elt ps in
 336             let initial =
 337               let common, others =
 338                 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 339               in
 340               (others + (abs (common - card))), e1
 341             in
 342             let _, e = EqualitySet.fold f ps initial in
 343             let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 344             ns, EqualitySet.add e ps'
 345       else
 346         let e = EqualitySet.min_elt ps in
 347         let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 348         ns, EqualitySet.add e ps'
 349     else
 350       EqualitySet.empty, EqualitySet.empty
 351   in
 352 (*   let in_weight, ns = pickw in_weight ns in *)
 353 (*   let _, ps = pickw in_weight ps in *)
 354   let ns, ps = pickw in_weight ns ps in
 355   let rec picka w s l =
 356     if w > 0 then
 357       match l with
 358       | [] -> w, s, []
 359       | hd::tl when not (EqualitySet.mem hd s) ->
 360           let w, s, l = picka (w-1) s tl in
 361           w, EqualitySet.add hd s, hd::l
 362       | hd::tl ->
 363           let w, s, l = picka w s tl in
 364           w, s, hd::l
 365     else
 366       0, s, l
 367   in
 368   let in_age, ns, nl = picka in_age ns nl in
 369   let _, ps, pl = picka in_age ps pl in
 370   if not (EqualitySet.is_empty ps) then
 371 (*     maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
 372     maximal_retained_equality := Some (EqualitySet.max_elt ps);
 373   let tbl =
 374     EqualitySet.fold
 375       (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
 376 (*     if !use_fullred then *)
 377 (*       EqualitySet.fold *)
 378 (*         (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
 379 (*     else *)
 380 (*       tbl *)
 381   in
 382   (nl, ns), (pl, ps), tbl
 383 ;;
 384
 385
 386 let infer env sign current (active_list, active_table) =
 387   let new_neg, new_pos =
 388     match sign with
 389     | Negative ->
 390         let maxm, res =
 391           Indexing.superposition_left !maxmeta env active_table current in
 392         maxmeta := maxm;
 393         res, []
 394     | Positive ->
 395         let maxm, res =
 396           Indexing.superposition_right !maxmeta env active_table current in
 397         maxmeta := maxm;
 398         let rec infer_positive table = function
 399           | [] -> [], []
 400           | (Negative, equality)::tl ->
 401               let maxm, res =
 402                 Indexing.superposition_left !maxmeta env table equality in
 403               maxmeta := maxm;
 404               let neg, pos = infer_positive table tl in
 405               res @ neg, pos
 406           | (Positive, equality)::tl ->
 407               let maxm, res =
 408                 Indexing.superposition_right !maxmeta env table equality in
 409               maxmeta := maxm;
 410               let neg, pos = infer_positive table tl in
 411               neg, res @ pos
 412         in
 413         let curr_table = Indexing.index (Indexing.empty_table ()) current in
 414         let neg, pos = infer_positive curr_table active_list in
 415         neg, res @ pos
 416   in
 417   derived_clauses := !derived_clauses + (List.length new_neg) +
 418     (List.length new_pos);
 419   match !maximal_retained_equality with
 420   | None -> new_neg, new_pos
 421   | Some eq ->
 422       (* if we have a maximal_retained_equality, we can discard all equalities
 423          "greater" than it, as they will never be reached...  An equality is
 424          greater than maximal_retained_equality if it is bigger
 425          wrt. OrderedEquality.compare and it is less similar than
 426          maximal_retained_equality to the current goal *)
 427       let symbols, card =
 428         match active_list with
 429         | (Negative, e)::_ ->
 430             let symbols = symbols_of_equality e in
 431             let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
 432             Some symbols, card
 433         | _ -> None, 0
 434       in
 435       let new_pos =
 436         match symbols with
 437         | None ->
 438             List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
 439         | Some symbols ->
 440             let filterfun e =
 441               if OrderedEquality.compare e eq <= 0 then
 442                 true
 443               else
 444                 let foldfun k v (r1, r2) =
 445                   if TermMap.mem k symbols then
 446                     let c = TermMap.find k symbols in
 447                     let c1 = abs (c - v) in
 448                     let c2 = v - c1 in
 449                     r1 + c2, r2 + c1
 450                   else
 451                     r1, r2 + v
 452                 in
 453                 let initial =
 454                   let common, others =
 455                     TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in
 456                   others + (abs (common - card))
 457                 in
 458                 let common, others =
 459                   TermMap.fold foldfun (symbols_of_equality e) (0, 0) in
 460                 let c = others + (abs (common - card)) in
 461                 if c < initial then true else false
 462             in
 463             List.filter filterfun new_pos
 464       in
 465       new_neg, new_pos
 466 ;;
 467
 468
 469 let contains_empty env (negative, positive) =
 470   let metasenv, context, ugraph = env in
 471   try
 472     let found =
 473       List.find
 474         (fun (w, proof, (ty, left, right, ordering), m, a) ->
 475            fst (CicReduction.are_convertible context left right ugraph))
 476         negative
 477     in
 478     true, Some found
 479   with Not_found ->
 480     false, None
 481 ;;
 482
 483
 484 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
 485   let pl, passive_table =
 486     match passive with
 487     | None -> [], None
 488     | Some ((pn, _), (pp, _), pt) ->
 489         let pn = List.map (fun e -> (Negative, e)) pn
 490         and pp = List.map (fun e -> (Positive, e)) pp in
 491         pn @ pp, Some pt
 492   in
 493   let all = if pl = [] then active_list else active_list @ pl in
 494
 495   (*   let rec find_duplicate sign current = function *)
 496 (*     | [] -> false *)
 497 (*     | (s, eq)::tl when s = sign -> *)
 498 (*         if meta_convertibility_eq current eq then true *)
 499 (*         else find_duplicate sign current tl *)
 500 (*     | _::tl -> find_duplicate sign current tl *)
 501 (*   in *)
 502
 503 (*   let res =  *)
 504 (*     if sign = Positive then *)
 505 (*       Indexing.subsumption env active_table current *)
 506 (*     else *)
 507 (*       false *)
 508 (*   in *)
 509 (*   if res then *)
 510 (*     None *)
 511 (*   else *)
 512
 513   let demodulate table current =
 514     let newmeta, newcurrent =
 515       Indexing.demodulation !maxmeta env table sign current in
 516     maxmeta := newmeta;
 517     if is_identity env newcurrent then
 518       if sign = Negative then Some (sign, newcurrent)
 519       else None
 520     else
 521       Some (sign, newcurrent)
 522   in
 523   let res =
 524     let res = demodulate active_table current in
 525     match res with
 526     | None -> None
 527     | Some (sign, newcurrent) ->
 528         match passive_table with
 529         | None -> res
 530         | Some passive_table -> demodulate passive_table newcurrent
 531   in
 532   match res with
 533   | None -> None
 534   | Some (Negative, c) ->
 535       let ok = not (
 536         List.exists
 537           (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
 538           all)
 539       in
 540       if ok then res else None
 541   | Some (Positive, c) ->
 542       if Indexing.in_index active_table c then
 543         None
 544       else
 545         match passive_table with
 546         | None -> res
 547         | Some passive_table ->
 548             if Indexing.in_index passive_table c then None
 549             else res
 550
 551 (*   | Some (s, c) -> if find_duplicate s c all then None else res *)
 552
 553 (*         if s = Utils.Negative then *)
 554 (*           res *)
 555 (*         else *)
 556 (*           if Indexing.subsumption env active_table c then *)
 557 (*             None *)
 558 (*           else ( *)
 559 (*             match passive_table with *)
 560 (*             | None -> res *)
 561 (*             | Some passive_table -> *)
 562 (*                 if Indexing.subsumption env passive_table c then *)
 563 (*                   None *)
 564 (*                 else *)
 565 (*                   res *)
 566 (*           ) *)
 567
 568 (*         let pred (sign, eq) = *)
 569 (*           if sign <> s then false *)
 570 (*           else subsumption env c eq *)
 571 (*         in *)
 572 (*         if List.exists pred all then None *)
 573 (*         else res *)
 574 ;;
 575
 576 type fs_time_info_t = {
 577   mutable build_all: float;
 578   mutable demodulate: float;
 579   mutable subsumption: float;
 580 };;
 581
 582 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
 583
 584
 585 let forward_simplify_new env (new_neg, new_pos) ?passive active =
 586   let t1 = Unix.gettimeofday () in
 587
 588   let active_list, active_table = active in
 589   let pl, passive_table =
 590     match passive with
 591     | None -> [], None
 592     | Some ((pn, _), (pp, _), pt) ->
 593         let pn = List.map (fun e -> (Negative, e)) pn
 594         and pp = List.map (fun e -> (Positive, e)) pp in
 595         pn @ pp, Some pt
 596   in
 597   let all = active_list @ pl in
 598
 599   let t2 = Unix.gettimeofday () in
 600   fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
 601
 602   let demodulate sign table target =
 603     let newmeta, newtarget =
 604       Indexing.demodulation !maxmeta env table sign target in
 605     maxmeta := newmeta;
 606     newtarget
 607   in
 608 (*   let f sign' target (sign, eq) = *)
 609 (*     if sign <> sign' then false *)
 610 (*     else subsumption env target eq  *)
 611 (*   in *)
 612
 613   let t1 = Unix.gettimeofday () in
 614
 615   let new_neg, new_pos =
 616     let new_neg = List.map (demodulate Negative active_table) new_neg
 617     and new_pos = List.map (demodulate Positive active_table) new_pos in
 618     match passive_table with
 619     | None -> new_neg, new_pos
 620     | Some passive_table ->
 621         List.map (demodulate Negative passive_table) new_neg,
 622         List.map (demodulate Positive passive_table) new_pos
 623   in
 624
 625   let t2 = Unix.gettimeofday () in
 626   fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
 627
 628   let new_pos_set =
 629     List.fold_left
 630       (fun s e ->
 631          if not (Inference.is_identity env e) then
 632            if EqualitySet.mem e s then s
 633            else EqualitySet.add e s
 634          else s)
 635       EqualitySet.empty new_pos
 636   in
 637   let new_pos = EqualitySet.elements new_pos_set in
 638
 639   let subs =
 640     match passive_table with
 641     | None ->
 642         (fun e -> not (Indexing.subsumption env active_table e))
 643     | Some passive_table ->
 644         (fun e -> not ((Indexing.subsumption env active_table e) ||
 645                          (Indexing.subsumption env passive_table e)))
 646   in
 647
 648   let t1 = Unix.gettimeofday () in
 649
 650 (*   let new_neg, new_pos = *)
 651 (*     List.filter subs new_neg, *)
 652 (*     List.filter subs new_pos *)
 653 (*   in *)
 654
 655 (*   let new_neg, new_pos =  *)
 656 (*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
 657 (*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
 658 (*   in *)
 659
 660   let t2 = Unix.gettimeofday () in
 661   fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
 662
 663   let is_duplicate =
 664     match passive_table with
 665     | None ->
 666         (fun e -> not (Indexing.in_index active_table e))
 667     | Some passive_table ->
 668         (fun e ->
 669            not ((Indexing.in_index active_table e) ||
 670                   (Indexing.in_index passive_table e)))
 671   in
 672   new_neg, List.filter is_duplicate new_pos
 673
 674 (*   new_neg, new_pos *)
 675
 676 (*   let res = *)
 677 (*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
 678 (*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
 679 (*   in *)
 680 (*   res *)
 681 ;;
 682
 683
 684 let backward_simplify_active env new_pos new_table min_weight active =
 685   let active_list, active_table = active in
 686   let active_list, newa =
 687     List.fold_right
 688       (fun (s, equality) (res, newn) ->
 689          let ew, _, _, _, _ = equality in
 690          if ew < min_weight then
 691            (s, equality)::res, newn
 692          else
 693            match forward_simplify env (s, equality) (new_pos, new_table) with
 694            | None -> res, newn
 695            | Some (s, e) ->
 696                if equality = e then
 697                  (s, e)::res, newn
 698                else
 699                  res, (s, e)::newn)
 700       active_list ([], [])
 701   in
 702   let find eq1 where =
 703     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 704   in
 705   let active, newa =
 706     List.fold_right
 707       (fun (s, eq) (res, tbl) ->
 708          if List.mem (s, eq) res then
 709            res, tbl
 710          else if (is_identity env eq) || (find eq res) then (
 711            res, tbl
 712          ) (* else if (find eq res) then *)
 713 (*            res, tbl *)
 714          else
 715            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
 716       active_list ([], Indexing.empty_table ()),
 717     List.fold_right
 718       (fun (s, eq) (n, p) ->
 719          if (s <> Negative) && (is_identity env eq) then (
 720            (n, p)
 721          ) else
 722            if s = Negative then eq::n, p
 723            else n, eq::p)
 724       newa ([], [])
 725   in
 726   match newa with
 727   | [], [] -> active, None
 728   | _ -> active, Some newa
 729 ;;
 730
 731
 732 let backward_simplify_passive env new_pos new_table min_weight passive =
 733   let (nl, ns), (pl, ps), passive_table = passive in
 734   let f sign equality (resl, ress, newn) =
 735     let ew, _, _, _, _ = equality in
 736     if ew < min_weight then
 737 (*       let _ = debug_print (lazy (Printf.sprintf "OK: %d %d" ew min_weight)) in *)
 738       equality::resl, ress, newn
 739     else
 740       match forward_simplify env (sign, equality) (new_pos, new_table) with
 741       | None -> resl, EqualitySet.remove equality ress, newn
 742       | Some (s, e) ->
 743           if equality = e then
 744             equality::resl, ress, newn
 745           else
 746             let ress = EqualitySet.remove equality ress in
 747             resl, ress, e::newn
 748   in
 749   let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
 750   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
 751   let passive_table =
 752     List.fold_left
 753       (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
 754   in
 755   match newn, newp with
 756   | [], [] -> ((nl, ns), (pl, ps), passive_table), None
 757   | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
 758 ;;
 759
 760
 761 let backward_simplify env new' ?passive active =
 762   let new_pos, new_table, min_weight =
 763     List.fold_left
 764       (fun (l, t, w) e ->
 765          let ew, _, _, _, _ = e in
 766          (Positive, e)::l, Indexing.index t e, min ew w)
 767       ([], Indexing.empty_table (), 1000000) (snd new')
 768   in
 769   let active, newa =
 770     backward_simplify_active env new_pos new_table min_weight active in
 771   match passive with
 772   | None ->
 773       active, (make_passive [] []), newa, None
 774   | Some passive ->
 775       let passive, newp =
 776         backward_simplify_passive env new_pos new_table min_weight passive in
 777       active, passive, newa, newp
 778 ;;
 779
 780
 781 let get_selection_estimate () =
 782   elapsed_time := (Unix.gettimeofday ()) -. !start_time;
 783 (*   !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
 784   int_of_float (
 785     ceil ((float_of_int !processed_clauses) *.
 786             ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
 787 ;;
 788
 789
 790 let rec given_clause env passive active =
 791   let time1 = Unix.gettimeofday () in
 792
 793   let selection_estimate = get_selection_estimate () in
 794   let kept = size_of_passive passive in
 795   let passive =
 796     if !time_limit = 0. || !processed_clauses = 0 then
 797       passive
 798     else if !elapsed_time > !time_limit then (
 799       debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
 800                      !time_limit !elapsed_time));
 801       make_passive [] []
 802     ) else if kept > selection_estimate then (
 803       debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
 804                                      "(kept: %d, selection_estimate: %d)\n")
 805                      kept selection_estimate));
 806       prune_passive selection_estimate active passive
 807     ) else
 808       passive
 809   in
 810
 811   let time2 = Unix.gettimeofday () in
 812   passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
 813
 814   kept_clauses := (size_of_passive passive) + (size_of_active active);
 815
 816   match passive_is_empty passive with
 817   | true -> ParamodulationFailure
 818   | false ->
 819       let (sign, current), passive = select env passive active in
 820       let time1 = Unix.gettimeofday () in
 821       let res = forward_simplify env (sign, current) ~passive active in
 822       let time2 = Unix.gettimeofday () in
 823       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
 824       match res with
 825       | None ->
 826           given_clause env passive active
 827       | Some (sign, current) ->
 828           if (sign = Negative) && (is_identity env current) then (
 829             debug_print (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
 830                            (string_of_equality ~env current)));
 831             ParamodulationSuccess (Some current, env)
 832           ) else (
 833             debug_print (lazy "\n================================================");
 834             debug_print (lazy (Printf.sprintf "selected: %s %s"
 835                            (string_of_sign sign)
 836                            (string_of_equality ~env current)));
 837
 838             let t1 = Unix.gettimeofday () in
 839             let new' = infer env sign current active in
 840             let t2 = Unix.gettimeofday () in
 841             infer_time := !infer_time +. (t2 -. t1);
 842
 843             let res, goal = contains_empty env new' in
 844             if res then
 845               ParamodulationSuccess (goal, env)
 846             else
 847               let t1 = Unix.gettimeofday () in
 848               let new' = forward_simplify_new env new' (* ~passive *) active in
 849               let t2 = Unix.gettimeofday () in
 850               let _ =
 851                 forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1)
 852               in
 853               let active =
 854                 match sign with
 855                 | Negative -> active
 856                 | Positive ->
 857                     let t1 = Unix.gettimeofday () in
 858                     let active, _, newa, _ =
 859                       backward_simplify env ([], [current]) active
 860                     in
 861                     let t2 = Unix.gettimeofday () in
 862                     backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
 863                     match newa with
 864                     | None -> active
 865                     | Some (n, p) ->
 866                         let al, tbl = active in
 867                         let nn = List.map (fun e -> Negative, e) n in
 868                         let pp, tbl =
 869                           List.fold_right
 870                             (fun e (l, t) ->
 871                                (Positive, e)::l,
 872                                Indexing.index tbl e)
 873                             p ([], tbl)
 874                         in
 875                         nn @ al @ pp, tbl
 876               in
 877 (*               let _ = *)
 878 (*                 Printf.printf "active:\n%s\n" *)
 879 (*                   (String.concat "\n" *)
 880 (*                      ((List.map *)
 881 (*                          (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
 882 (*                             (string_of_equality ~env e)) (fst active)))); *)
 883 (*                 print_newline (); *)
 884 (*               in *)
 885 (*               let _ = *)
 886 (*                 match new' with *)
 887 (*                 | neg, pos -> *)
 888 (*                     Printf.printf "new':\n%s\n" *)
 889 (*                       (String.concat "\n" *)
 890 (*                          ((List.map *)
 891 (*                              (fun e -> "Negative " ^ *)
 892 (*                                 (string_of_equality ~env e)) neg) @ *)
 893 (*                             (List.map *)
 894 (*                                (fun e -> "Positive " ^ *)
 895 (*                                   (string_of_equality ~env e)) pos))); *)
 896 (*                     print_newline (); *)
 897 (*               in *)
 898               match contains_empty env new' with
 899               | false, _ ->
 900                   let active =
 901                     let al, tbl = active in
 902                     match sign with
 903                     | Negative -> (sign, current)::al, tbl
 904                     | Positive ->
 905                         al @ [(sign, current)], Indexing.index tbl current
 906                   in
 907                   let passive = add_to_passive passive new' in
 908                   let (_, ns), (_, ps), _ = passive in
 909 (*                   Printf.printf "passive:\n%s\n" *)
 910 (*                     (String.concat "\n" *)
 911 (*                        ((List.map (fun e -> "Negative " ^ *)
 912 (*                                      (string_of_equality ~env e)) *)
 913 (*                            (EqualitySet.elements ns)) @ *)
 914 (*                           (List.map (fun e -> "Positive " ^ *)
 915 (*                                        (string_of_equality ~env e)) *)
 916 (*                              (EqualitySet.elements ps)))); *)
 917 (*                   print_newline (); *)
 918                   given_clause env passive active
 919               | true, goal ->
 920                   ParamodulationSuccess (goal, env)
 921           )
 922 ;;
 923
 924
 925 let rec given_clause_fullred env passive active =
 926   let time1 = Unix.gettimeofday () in
 927
 928   let selection_estimate = get_selection_estimate () in
 929   let kept = size_of_passive passive in
 930   let passive =
 931     if !time_limit = 0. || !processed_clauses = 0 then
 932       passive
 933     else if !elapsed_time > !time_limit then (
 934       debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
 935                      !time_limit !elapsed_time));
 936       make_passive [] []
 937     ) else if kept > selection_estimate then (
 938       debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
 939                                      "(kept: %d, selection_estimate: %d)\n")
 940                      kept selection_estimate));
 941       prune_passive selection_estimate active passive
 942     ) else
 943       passive
 944   in
 945
 946   let time2 = Unix.gettimeofday () in
 947   passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
 948
 949   kept_clauses := (size_of_passive passive) + (size_of_active active);
 950
 951   match passive_is_empty passive with
 952   | true -> ParamodulationFailure
 953   | false ->
 954       let (sign, current), passive = select env passive active in
 955       let time1 = Unix.gettimeofday () in
 956       let res = forward_simplify env (sign, current) ~passive active in
 957       let time2 = Unix.gettimeofday () in
 958       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
 959       match res with
 960       | None ->
 961           given_clause_fullred env passive active
 962       | Some (sign, current) ->
 963           if (sign = Negative) && (is_identity env current) then (
 964             debug_print (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
 965                            (string_of_equality ~env current)));
 966             ParamodulationSuccess (Some current, env)
 967           ) else (
 968             debug_print (lazy "\n================================================");
 969             debug_print (lazy (Printf.sprintf "selected: %s %s"
 970                            (string_of_sign sign)
 971                            (string_of_equality ~env current)));
 972
 973             let t1 = Unix.gettimeofday () in
 974             let new' = infer env sign current active in
 975             let t2 = Unix.gettimeofday () in
 976             infer_time := !infer_time +. (t2 -. t1);
 977
 978             let active =
 979               if is_identity env current then active
 980               else
 981                 let al, tbl = active in
 982                 match sign with
 983                 | Negative -> (sign, current)::al, tbl
 984                 | Positive -> al @ [(sign, current)], Indexing.index tbl current
 985             in
 986             let rec simplify new' active passive =
 987               let t1 = Unix.gettimeofday () in
 988               let new' = forward_simplify_new env new' ~passive active in
 989               let t2 = Unix.gettimeofday () in
 990               forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1);
 991               let t1 = Unix.gettimeofday () in
 992               let active, passive, newa, retained =
 993                 backward_simplify env new' ~passive active in
 994               let t2 = Unix.gettimeofday () in
 995               backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
 996               match newa, retained with
 997               | None, None -> active, passive, new'
 998               | Some (n, p), None
 999               | None, Some (n, p) ->
1000                   let nn, np = new' in
1001                   simplify (nn @ n, np @ p) active passive
1002               | Some (n, p), Some (rn, rp) ->
1003                   let nn, np = new' in
1004                   simplify (nn @ n @ rn, np @ p @ rp) active passive
1005             in
1006             let active, passive, new' = simplify new' active passive in
1007
1008             let k = size_of_passive passive in
1009             if k < (kept - 1) then
1010               processed_clauses := !processed_clauses + (kept - 1 - k);
1011
1012             let _ =
1013               debug_print (lazy (
1014                 Printf.sprintf "active:\n%s\n"
1015                   (String.concat "\n"
1016                      ((List.map
1017                          (fun (s, e) -> (string_of_sign s) ^ " " ^
1018                             (string_of_equality ~env e)) (fst active))))))
1019             in
1020             let _ =
1021               match new' with
1022               | neg, pos ->
1023                   debug_print (lazy (
1024                     Printf.sprintf "new':\n%s\n"
1025                       (String.concat "\n"
1026                          ((List.map
1027                              (fun e -> "Negative " ^
1028                                 (string_of_equality ~env e)) neg) @
1029                             (List.map
1030                                (fun e -> "Positive " ^
1031                                   (string_of_equality ~env e)) pos)))))
1032             in
1033             match contains_empty env new' with
1034             | false, _ ->
1035                 let passive = add_to_passive passive new' in
1036 (*                 let (_, ns), (_, ps), _ = passive in *)
1037 (*                 Printf.printf "passive:\n%s\n" *)
1038 (*                   (String.concat "\n" *)
1039 (*                      ((List.map (fun e -> "Negative " ^ *)
1040 (*                                    (string_of_equality ~env e)) *)
1041 (*                          (EqualitySet.elements ns)) @ *)
1042 (*                         (List.map (fun e -> "Positive " ^ *)
1043 (*                                      (string_of_equality ~env e)) *)
1044 (*                            (EqualitySet.elements ps)))); *)
1045 (*                 print_newline (); *)
1046                 given_clause_fullred env passive active
1047             | true, goal ->
1048                 ParamodulationSuccess (goal, env)
1049           )
1050 ;;
1051
1052
1053 let given_clause_ref = ref given_clause;;
1054
1055
1056 let main dbd term metasenv ugraph =
1057   let module C = Cic in
1058   let module T = CicTypeChecker in
1059   let module PET = ProofEngineTypes in
1060   let module PP = CicPp in
1061   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
1062   let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
1063   let proof, goals = status in
1064   let goal' = List.nth goals 0 in
1065   let _, metasenv, meta_proof, _ = proof in
1066   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1067   let equalities, maxm = find_equalities context proof in
1068   let library_equalities, maxm =
1069     find_library_equalities ~dbd context (proof, goal') (maxm+2)
1070   in
1071   maxmeta := maxm+2; (* TODO ugly!! *)
1072   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1073   let new_meta_goal, metasenv, type_of_goal =
1074     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1075     Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
1076     print_newline ();
1077     Cic.Meta (maxm+1, irl),
1078     (maxm+1, context, ty)::metasenv,
1079     ty
1080   in
1081 (*   let new_meta_goal = Cic.Meta (goal', irl) in *)
1082   let env = (metasenv, context, ugraph) in
1083   try
1084     let term_equality = equality_of_term new_meta_goal goal in
1085     let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
1086     if is_identity env term_equality then
1087       let proof =
1088         Cic.Appl [Cic.MutConstruct (* reflexivity *)
1089                     (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
1090                   eq_ty; left]
1091       in
1092       let _ =
1093         Printf.printf "OK, found a proof!\n";
1094         let names = names_of_context context in
1095         print_endline (PP.pp proof names)
1096       in
1097       ()
1098     else
1099       let equalities =
1100         let equalities = equalities @ library_equalities in
1101         debug_print (lazy (
1102           Printf.sprintf "equalities:\n%s\n"
1103             (String.concat "\n"
1104                (List.map string_of_equality equalities))));
1105         debug_print (lazy "SIMPLYFYING EQUALITIES...");
1106         let rec simpl e others others_simpl =
1107           let active = others @ others_simpl in
1108           let tbl =
1109             List.fold_left
1110               (fun t (_, e) -> Indexing.index t e)
1111               (Indexing.empty_table ()) active
1112           in
1113           let res = forward_simplify env e (active, tbl) in
1114           match others with
1115           | hd::tl -> (
1116               match res with
1117               | None -> simpl hd tl others_simpl
1118               | Some e -> simpl hd tl (e::others_simpl)
1119             )
1120           | [] -> (
1121               match res with
1122               | None -> others_simpl
1123               | Some e -> e::others_simpl
1124             )
1125         in
1126         match equalities with
1127         | [] -> []
1128         | hd::tl ->
1129             let others = List.map (fun e -> (Positive, e)) tl in
1130             let res =
1131               List.rev (List.map snd (simpl (Positive, hd) others []))
1132             in
1133             debug_print (lazy (
1134               Printf.sprintf "equalities AFTER:\n%s\n"
1135                 (String.concat "\n"
1136                    (List.map string_of_equality res))));
1137             res
1138       in
1139       let active = make_active () in
1140       let passive = make_passive [term_equality] equalities in
1141       Printf.printf "\ncurrent goal: %s\n"
1142         (string_of_equality ~env term_equality);
1143       Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
1144       Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
1145       Printf.printf "\nequalities:\n%s\n"
1146         (String.concat "\n"
1147            (List.map
1148               (string_of_equality ~env)
1149               (equalities @ library_equalities)));
1150       print_endline "--------------------------------------------------";
1151       let start = Unix.gettimeofday () in
1152       print_endline "GO!";
1153       start_time := Unix.gettimeofday ();
1154       let res =
1155         (if !use_fullred then given_clause_fullred else given_clause)
1156           env passive active
1157       in
1158       let finish = Unix.gettimeofday () in
1159       let _ =
1160         match res with
1161         | ParamodulationFailure ->
1162             Printf.printf "NO proof found! :-(\n\n"
1163         | ParamodulationSuccess (Some goal, env) ->
1164             let proof = Inference.build_proof_term goal in
1165             let newmetasenv =
1166               List.fold_left
1167                 (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
1168             in
1169             let _ =
1170               try
1171                 let ty, ug =
1172                   CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
1173                 in
1174                 Printf.printf "OK, found a proof!\n";
1175                 (* REMEMBER: we have to instantiate meta_proof, we should use
1176                    apply  the "apply" tactic to proof and status
1177                 *)
1178                 let names = names_of_context context in
1179                 print_endline (PP.pp proof names);
1180                 (*           print_endline (PP.ppterm proof); *)
1181
1182                 print_endline (string_of_float (finish -. start));
1183                 Printf.printf
1184                   "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
1185                   (CicPp.pp type_of_goal names) (CicPp.pp ty names)
1186                   (string_of_bool
1187                      (fst (CicReduction.are_convertible
1188                              context type_of_goal ty ug)));
1189               with e ->
1190                 Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
1191                 Printf.printf "MAXMETA USED: %d\n" !maxmeta;
1192                 print_endline (string_of_float (finish -. start));
1193             in
1194             ()
1195
1196         | ParamodulationSuccess (None, env) ->
1197             Printf.printf "Success, but no proof?!?\n\n"
1198       in
1199       Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
1200                        "forward_simpl_new_time: %.9f\n" ^^
1201                        "backward_simpl_time: %.9f\n")
1202         !infer_time !forward_simpl_time !forward_simpl_new_time
1203         !backward_simpl_time;
1204       Printf.printf "passive_maintainance_time: %.9f\n"
1205         !passive_maintainance_time;
1206       Printf.printf "    successful unification/matching time: %.9f\n"
1207         !Indexing.match_unif_time_ok;
1208       Printf.printf "    failed unification/matching time: %.9f\n"
1209         !Indexing.match_unif_time_no;
1210       Printf.printf "    indexing retrieval time: %.9f\n"
1211         !Indexing.indexing_retrieval_time;
1212       Printf.printf "    demodulate_term.build_newtarget_time: %.9f\n"
1213         !Indexing.build_newtarget_time;
1214       Printf.printf "derived %d clauses, kept %d clauses.\n"
1215         !derived_clauses !kept_clauses;
1216   with exc ->
1217     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
1218     raise exc
1219 ;;
1220
1221
1222 let saturate dbd (proof, goal) =
1223   let module C = Cic in
1224   maxmeta := 0;
1225   let goal' = goal in
1226   let uri, metasenv, meta_proof, term_to_prove = proof in
1227   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1228   let equalities, maxm = find_equalities context proof in
1229   let new_meta_goal, metasenv, type_of_goal =
1230     let irl =
1231       CicMkImplicit.identity_relocation_list_for_metavariable context in
1232     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1233     debug_print (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
1234     Cic.Meta (maxm+1, irl),
1235     (maxm+1, context, ty)::metasenv,
1236     ty
1237   in
1238   let ugraph = CicUniv.empty_ugraph in
1239   let env = (metasenv, context, ugraph) in
1240 (*   try *)
1241   let term_equality = equality_of_term new_meta_goal goal in
1242   let res, time =
1243     if is_identity env term_equality then
1244       let w, _, (eq_ty, left, right, o), m, a = term_equality in
1245       let proof =
1246         Cic.Appl [Cic.MutConstruct (* reflexivity *)
1247                     (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
1248                   eq_ty; left]
1249       in
1250       (ParamodulationSuccess
1251          (Some (0, Inference.BasicProof proof,
1252                 (eq_ty, left, right, o), m, a), env), 0.)
1253     else
1254       let library_equalities, maxm =
1255         find_library_equalities ~dbd context (proof, goal') (maxm+2)
1256       in
1257       maxmeta := maxm+2;
1258       let equalities =
1259         let equalities = equalities @ library_equalities in
1260         debug_print (lazy (
1261           Printf.sprintf "equalities:\n%s\n"
1262             (String.concat "\n"
1263                (List.map string_of_equality equalities))));
1264         debug_print (lazy "SIMPLYFYING EQUALITIES...");
1265         let rec simpl e others others_simpl =
1266           let active = others @ others_simpl in
1267           let tbl =
1268             List.fold_left
1269               (fun t (_, e) -> Indexing.index t e)
1270               (Indexing.empty_table ()) active
1271           in
1272           let res = forward_simplify env e (active, tbl) in
1273           match others with
1274           | hd::tl -> (
1275               match res with
1276               | None -> simpl hd tl others_simpl
1277               | Some e -> simpl hd tl (e::others_simpl)
1278             )
1279           | [] -> (
1280               match res with
1281               | None -> others_simpl
1282               | Some e -> e::others_simpl
1283             )
1284         in
1285         match equalities with
1286         | [] -> []
1287         | hd::tl ->
1288             let others = List.map (fun e -> (Positive, e)) tl in
1289             let res =
1290               List.rev (List.map snd (simpl (Positive, hd) others []))
1291             in
1292             debug_print (lazy (
1293               Printf.sprintf "equalities AFTER:\n%s\n"
1294                 (String.concat "\n"
1295                    (List.map string_of_equality res))));
1296             res
1297       in
1298       let active = make_active () in
1299       let passive = make_passive [term_equality] equalities in
1300       let start = Unix.gettimeofday () in
1301       let res = given_clause_fullred env passive active in
1302       let finish = Unix.gettimeofday () in
1303       (res, finish -. start)
1304   in
1305   match res with
1306   | ParamodulationSuccess (Some goal, env) ->
1307       debug_print (lazy "OK, found a proof!");
1308       let proof = Inference.build_proof_term goal in
1309       let names = names_of_context context in
1310       let newmetasenv =
1311         let i1 =
1312           match new_meta_goal with
1313           | C.Meta (i, _) -> i | _ -> assert false
1314         in
1315 (*           let i2 = *)
1316 (*             match meta_proof with *)
1317 (*             | C.Meta (i, _) -> i *)
1318 (*             | t -> *)
1319 (*                 Printf.printf "\nHMMM!!! meta_proof: %s\ngoal': %s" *)
1320 (*                   (CicPp.pp meta_proof names) (string_of_int goal'); *)
1321 (*                 print_newline (); *)
1322 (*                 assert false *)
1323 (*           in *)
1324         List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
1325       in
1326       let newstatus =
1327         try
1328           let ty, ug =
1329             CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
1330           in
1331           debug_print (lazy (CicPp.pp proof [](* names *)));
1332           debug_print (lazy
1333             (Printf.sprintf
1334                "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
1335                (CicPp.pp type_of_goal names) (CicPp.pp ty names)
1336                (string_of_bool
1337                   (fst (CicReduction.are_convertible
1338                           context type_of_goal ty ug)))));
1339           let equality_for_replace i t1 =
1340             match t1 with
1341             | C.Meta (n, _) -> n = i
1342             | _ -> false
1343           in
1344           let real_proof =
1345             ProofEngineReduction.replace
1346               ~equality:equality_for_replace
1347               ~what:[goal'] ~with_what:[proof]
1348               ~where:meta_proof
1349           in
1350           debug_print (lazy (
1351             Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
1352               (match uri with Some uri -> UriManager.string_of_uri uri
1353                | None -> "")
1354               (print_metasenv newmetasenv)
1355               (CicPp.pp real_proof [](* names *))
1356               (CicPp.pp term_to_prove names)));
1357           ((uri, newmetasenv, real_proof, term_to_prove), [])
1358         with CicTypeChecker.TypeCheckerFailure _ ->
1359           debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!");
1360           debug_print (lazy (CicPp.pp proof names));
1361           raise (ProofEngineTypes.Fail
1362                    "Found a proof, but it doesn't typecheck")
1363       in
1364       debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
1365       newstatus
1366   | _ ->
1367       raise (ProofEngineTypes.Fail "NO proof found")
1368 (*   with e -> *)
1369 (*     raise (Failure "saturation failed") *)
1370 ;;
1371
1372
1373 (* dummy function called within matita to trigger linkage *)
1374 let init () = ();;
1375
1376
1377 (* UGLY SIDE EFFECT... *)
1378 if connect_to_auto then (
1379   AutoTactic.paramodulation_tactic := saturate;
1380   AutoTactic.term_is_equality := Inference.term_is_equality;
1381 );;