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