helm/ocaml/paramodulation/saturation.ml

   1 open Inference;;
   2 open Utils;;
   3
   4
   5 (* profiling statistics... *)
   6 let infer_time = ref 0.;;
   7 let forward_simpl_time = ref 0.;;
   8 let forward_simpl_new_time = ref 0.;;
   9 let backward_simpl_time = ref 0.;;
  10 let passive_maintainance_time = ref 0.;;
  11
  12 (* limited-resource-strategy related globals *)
  13 let processed_clauses = ref 0;; (* number of equalities selected so far... *)
  14 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
  15 let start_time = ref 0.;; (* time at which the execution started *)
  16 let elapsed_time = ref 0.;;
  17 (* let maximal_weight = ref None;; *)
  18 let maximal_retained_equality = ref None;;
  19
  20 (* equality-selection related globals *)
  21 let use_fullred = ref false;;
  22 let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
  23 let weight_age_counter = ref !weight_age_ratio;;
  24 let symbols_ratio = ref 0;;
  25 let symbols_counter = ref 0;;
  26
  27 (* statistics... *)
  28 let derived_clauses = ref 0;;
  29 let kept_clauses = ref 0;;
  30
  31 (* index of the greatest Cic.Meta created - TODO: find a better way! *)
  32 let maxmeta = ref 0;;
  33
  34
  35 type result =
  36   | Failure
  37   | Success of Inference.equality option * environment
  38 ;;
  39
  40
  41 (*
  42 let symbols_of_equality (_, (_, left, right), _, _) =
  43   TermSet.union (symbols_of_term left) (symbols_of_term right)
  44 ;;
  45 *)
  46
  47 let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
  48   let m1 = symbols_of_term left in
  49   let m =
  50     TermMap.fold
  51       (fun k v res ->
  52          try
  53            let c = TermMap.find k res in
  54            TermMap.add k (c+v) res
  55          with Not_found ->
  56            TermMap.add k v res)
  57       (symbols_of_term right) m1
  58   in
  59 (*   Printf.printf "symbols_of_equality %s:\n" *)
  60 (*     (string_of_equality equality); *)
  61 (*   TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
  62 (*   print_newline (); *)
  63   m
  64 ;;
  65
  66
  67 let weight_of_equality (_, (ty, left, right, _), _, _) =
  68   let meta_number = ref 0 in
  69   let weight_of t =
  70     let weight, ml =  weight_of_term t in
  71     meta_number := !meta_number + (List.fold_left (fun r (_, n) -> r+n) 0 ml);
  72     weight
  73   in
  74   (weight_of ty) + (weight_of left) + (weight_of right), meta_number
  75 ;;
  76
  77
  78 module OrderedEquality = struct
  79   type t = Inference.equality
  80
  81   let compare eq1 eq2 =
  82     match meta_convertibility_eq eq1 eq2 with
  83     | true -> 0
  84     | false ->
  85         let _, (ty, left, right, _), _, _ = eq1
  86         and _, (ty', left', right', _), _, _ = eq2 in
  87 (*         let w1, m1 = weight_of_equality eq1 *)
  88 (*         and w2, m2 = weight_of_equality eq2 in        *)
  89         let weight_of t = fst (weight_of_term ~consider_metas:false t) in
  90         let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
  91         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
  92         match Pervasives.compare w1 w2 with
  93         | 0 -> Pervasives.compare eq1 eq2
  94 (*             let res = Pervasives.compare m1 m2 in *)
  95 (*             if res = 0 then Pervasives.compare eq1 eq2 else res *)
  96         | res -> res
  97 end
  98
  99 module EqualitySet = Set.Make(OrderedEquality);;
 100
 101
 102 let select env passive (active, _) =
 103   processed_clauses := !processed_clauses + 1;
 104
 105   let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
 106   let remove eq l =
 107     List.filter (fun e -> e <> eq) l
 108   in
 109   if !weight_age_ratio > 0 then
 110     weight_age_counter := !weight_age_counter - 1;
 111   match !weight_age_counter with
 112   | 0 -> (
 113       weight_age_counter := !weight_age_ratio;
 114       match neg_list, pos_list with
 115       | hd::tl, pos ->
 116           (* Negatives aren't indexed, no need to remove them... *)
 117           (Negative, hd),
 118           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
 119       | [], hd::tl ->
 120           let passive_table =
 121             Indexing.remove_index passive_table hd
 122 (*             if !use_fullred then Indexing.remove_index passive_table hd *)
 123 (*             else passive_table *)
 124           in
 125           (Positive, hd),
 126           (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
 127       | _, _ -> assert false
 128     )
 129   | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
 130       symbols_counter := !symbols_counter - 1;
 131       let cardinality map =
 132         TermMap.fold (fun k v res -> res + v) map 0
 133       in
 134       match active with
 135       | (Negative, e)::_ ->
 136           let symbols = symbols_of_equality e in
 137           let card = cardinality symbols in
 138           let foldfun k v (r1, r2) =
 139             if TermMap.mem k symbols then
 140               let c = TermMap.find k symbols in
 141               let c1 = abs (c - v) in
 142               let c2 = v - c1 in
 143               r1 + c2, r2 + c1
 144             else
 145               r1, r2 + v
 146           in
 147           let f equality (i, e) =
 148             let common, others =
 149               TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 150             in
 151             let c = others + (abs (common - card)) in
 152             if c < i then (c, equality)
 153 (*             else if c = i then *)
 154 (*               match OrderedEquality.compare equality e with *)
 155 (*               | -1 -> (c, equality) *)
 156 (*               | res -> (i, e) *)
 157             else (i, e)
 158           in
 159           let e1 = EqualitySet.min_elt pos_set in
 160           let initial =
 161             let common, others =
 162               TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 163             in
 164             (others + (abs (common - card))), e1
 165           in
 166           let _, current = EqualitySet.fold f pos_set initial in
 167 (*           Printf.printf "\nsymbols-based selection: %s\n\n" *)
 168 (*             (string_of_equality ~env current); *)
 169           let passive_table =
 170             Indexing.remove_index passive_table current
 171 (*             if !use_fullred then Indexing.remove_index passive_table current *)
 172 (*             else passive_table *)
 173           in
 174           (Positive, current),
 175           (([], neg_set),
 176            (remove current pos_list, EqualitySet.remove current pos_set),
 177            passive_table)
 178       | _ ->
 179           let current = EqualitySet.min_elt pos_set in
 180           let passive_table =
 181             Indexing.remove_index passive_table current
 182 (*             if !use_fullred then Indexing.remove_index passive_table current *)
 183 (*             else passive_table *)
 184           in
 185           let passive =
 186             (neg_list, neg_set),
 187             (remove current pos_list, EqualitySet.remove current pos_set),
 188             passive_table
 189           in
 190           (Positive, current), passive
 191     )
 192   | _ ->
 193       symbols_counter := !symbols_ratio;
 194       let set_selection set = EqualitySet.min_elt set in
 195       if EqualitySet.is_empty neg_set then
 196         let current = set_selection pos_set in
 197         let passive =
 198           (neg_list, neg_set),
 199           (remove current pos_list, EqualitySet.remove current pos_set),
 200           Indexing.remove_index passive_table current
 201 (*           if !use_fullred then Indexing.remove_index passive_table current *)
 202 (*           else passive_table *)
 203         in
 204         (Positive, current), passive
 205       else
 206         let current = set_selection neg_set in
 207         let passive =
 208           (remove current neg_list, EqualitySet.remove current neg_set),
 209           (pos_list, pos_set),
 210           passive_table
 211         in
 212         (Negative, current), passive
 213 ;;
 214
 215
 216 let make_passive neg pos =
 217   let set_of equalities =
 218     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
 219   in
 220   let table =
 221       List.fold_left (fun tbl e -> Indexing.index tbl e)
 222         (Indexing.empty_table ()) pos
 223 (*     if !use_fullred then *)
 224 (*       List.fold_left (fun tbl e -> Indexing.index tbl e) *)
 225 (*         (Indexing.empty_table ()) pos *)
 226 (*     else *)
 227 (*       Indexing.empty_table () *)
 228   in
 229   (neg, set_of neg),
 230   (pos, set_of pos),
 231   table
 232 ;;
 233
 234
 235 let make_active () =
 236   [], Indexing.empty_table ()
 237 ;;
 238
 239
 240 let add_to_passive passive (new_neg, new_pos) =
 241   let (neg_list, neg_set), (pos_list, pos_set), table = passive in
 242   let ok set equality = not (EqualitySet.mem equality set) in
 243   let neg = List.filter (ok neg_set) new_neg
 244   and pos = List.filter (ok pos_set) new_pos in
 245   let table =
 246       List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
 247 (*     if !use_fullred then *)
 248 (*       List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
 249 (*     else *)
 250 (*       table *)
 251   in
 252   let add set equalities =
 253     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
 254   in
 255   (neg @ neg_list, add neg_set neg),
 256   (pos_list @ pos, add pos_set pos),
 257   table
 258 ;;
 259
 260
 261 let passive_is_empty = function
 262   | ([], _), ([], _), _ -> true
 263   | _ -> false
 264 ;;
 265
 266
 267 let size_of_passive ((_, ns), (_, ps), _) =
 268   (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
 269 ;;
 270
 271
 272 let size_of_active (active_list, _) =
 273   List.length active_list
 274 ;;
 275
 276
 277 let prune_passive howmany (active, _) passive =
 278   let (nl, ns), (pl, ps), tbl = passive in
 279   let howmany = float_of_int howmany
 280   and ratio = float_of_int !weight_age_ratio in
 281   let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
 282   and in_age = int_of_float (howmany /. (ratio +. 1.)) in
 283   Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age;
 284   let symbols, card =
 285     match active with
 286     | (Negative, e)::_ ->
 287         let symbols = symbols_of_equality e in
 288         let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
 289         Some symbols, card
 290     | _ -> None, 0
 291   in
 292   let counter = ref !symbols_ratio in
 293   let rec pickw w ns ps =
 294     if w > 0 then
 295       if not (EqualitySet.is_empty ns) then
 296         let e = EqualitySet.min_elt ns in
 297         let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
 298         EqualitySet.add e ns', ps
 299       else if !counter > 0 then
 300         let _ =
 301           counter := !counter - 1;
 302           if !counter = 0 then counter := !symbols_ratio
 303         in
 304         match symbols with
 305         | None ->
 306             let e = EqualitySet.min_elt ps in
 307             let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 308             ns, EqualitySet.add e ps'
 309         | Some symbols ->
 310             let foldfun k v (r1, r2) =
 311               if TermMap.mem k symbols then
 312                 let c = TermMap.find k symbols in
 313                 let c1 = abs (c - v) in
 314                 let c2 = v - c1 in
 315                 r1 + c2, r2 + c1
 316               else
 317                 r1, r2 + v
 318             in
 319             let f equality (i, e) =
 320               let common, others =
 321                 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 322               in
 323               let c = others + (abs (common - card)) in
 324               if c < i then (c, equality)
 325               else (i, e)
 326             in
 327             let e1 = EqualitySet.min_elt ps in
 328             let initial =
 329               let common, others =
 330                 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 331               in
 332               (others + (abs (common - card))), e1
 333             in
 334             let _, e = EqualitySet.fold f ps initial in
 335             let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 336             ns, EqualitySet.add e ps'
 337       else
 338         let e = EqualitySet.min_elt ps in
 339         let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 340         ns, EqualitySet.add e ps'
 341     else
 342       EqualitySet.empty, EqualitySet.empty
 343   in
 344 (*   let in_weight, ns = pickw in_weight ns in *)
 345 (*   let _, ps = pickw in_weight ps in *)
 346   let ns, ps = pickw in_weight ns ps in
 347   let rec picka w s l =
 348     if w > 0 then
 349       match l with
 350       | [] -> w, s, []
 351       | hd::tl when not (EqualitySet.mem hd s) ->
 352           let w, s, l = picka (w-1) s tl in
 353           w, EqualitySet.add hd s, hd::l
 354       | hd::tl ->
 355           let w, s, l = picka w s tl in
 356           w, s, hd::l
 357     else
 358       0, s, l
 359   in
 360   let in_age, ns, nl = picka in_age ns nl in
 361   let _, ps, pl = picka in_age ps pl in
 362   if not (EqualitySet.is_empty ps) then
 363 (*     maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
 364     maximal_retained_equality := Some (EqualitySet.max_elt ps);
 365   let tbl =
 366     EqualitySet.fold
 367       (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
 368 (*     if !use_fullred then *)
 369 (*       EqualitySet.fold *)
 370 (*         (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
 371 (*     else *)
 372 (*       tbl *)
 373   in
 374   (nl, ns), (pl, ps), tbl
 375 ;;
 376
 377
 378 let infer env sign current (active_list, active_table) =
 379   let new_neg, new_pos =
 380     match sign with
 381     | Negative ->
 382         Indexing.superposition_left env active_table current, []
 383     | Positive ->
 384         let maxm, res =
 385           Indexing.superposition_right !maxmeta env active_table current in
 386         maxmeta := maxm;
 387         let rec infer_positive table = function
 388           | [] -> [], []
 389           | (Negative, equality)::tl ->
 390               let res = Indexing.superposition_left env table equality in
 391               let neg, pos = infer_positive table tl in
 392               res @ neg, pos
 393           | (Positive, equality)::tl ->
 394               let maxm, res =
 395                 Indexing.superposition_right !maxmeta env table equality in
 396               maxmeta := maxm;
 397               let neg, pos = infer_positive table tl in
 398               neg, res @ pos
 399         in
 400         let curr_table = Indexing.index (Indexing.empty_table ()) current in
 401         let neg, pos = infer_positive curr_table active_list in
 402         neg, res @ pos
 403   in
 404   derived_clauses := !derived_clauses + (List.length new_neg) +
 405     (List.length new_pos);
 406   match (* !maximal_weight *)!maximal_retained_equality with
 407   | None -> new_neg, new_pos
 408   | Some (* w *) eq ->
 409       let new_pos =
 410         List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in
 411       new_neg, new_pos
 412 ;;
 413
 414
 415 let contains_empty env (negative, positive) =
 416   let metasenv, context, ugraph = env in
 417   try
 418     let found =
 419       List.find
 420         (fun (proof, (ty, left, right, ordering), m, a) ->
 421            fst (CicReduction.are_convertible context left right ugraph))
 422         negative
 423     in
 424     true, Some found
 425   with Not_found ->
 426     false, None
 427 ;;
 428
 429
 430 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
 431   let pl, passive_table =
 432     match passive with
 433     | None -> [], None
 434     | Some ((pn, _), (pp, _), pt) ->
 435         let pn = List.map (fun e -> (Negative, e)) pn
 436         and pp = List.map (fun e -> (Positive, e)) pp in
 437         pn @ pp, Some pt
 438   in
 439   let all = if pl = [] then active_list else active_list @ pl in
 440
 441 (*   let rec find_duplicate sign current = function *)
 442 (*     | [] -> false *)
 443 (*     | (s, eq)::tl when s = sign -> *)
 444 (*         if meta_convertibility_eq current eq then true *)
 445 (*         else find_duplicate sign current tl *)
 446 (*     | _::tl -> find_duplicate sign current tl *)
 447 (*   in *)
 448
 449 (*   let res =  *)
 450 (*     if sign = Positive then *)
 451 (*       Indexing.subsumption env active_table current *)
 452 (*     else *)
 453 (*       false *)
 454 (*   in *)
 455 (*   if res then *)
 456 (*     None *)
 457 (*   else *)
 458
 459   let demodulate table current =
 460     let newmeta, newcurrent =
 461       Indexing.demodulation !maxmeta env table current in
 462     maxmeta := newmeta;
 463     if is_identity env newcurrent then
 464       if sign = Negative then Some (sign, newcurrent)
 465       else (Inference.delete_proof newcurrent; None)
 466     else
 467       Some (sign, newcurrent)
 468   in
 469   let res =
 470     let res = demodulate active_table current in
 471     match res with
 472     | None -> None
 473     | Some (sign, newcurrent) ->
 474         match passive_table with
 475         | None -> res
 476         | Some passive_table -> demodulate passive_table newcurrent
 477   in
 478   match res with
 479   | None -> None
 480   | Some (Negative, c) ->
 481       let ok = not (
 482         List.exists
 483           (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
 484           all)
 485       in
 486       if ok then res else None
 487   | Some (Positive, c) ->
 488       if Indexing.in_index active_table c then
 489         (Inference.delete_proof c; None)
 490       else
 491         match passive_table with
 492         | None -> res
 493         | Some passive_table ->
 494             if Indexing.in_index passive_table c then
 495               (Inference.delete_proof c; None)
 496             else res
 497
 498 (*   | Some (s, c) -> if find_duplicate s c all then None else res *)
 499
 500 (*         if s = Utils.Negative then *)
 501 (*           res *)
 502 (*         else *)
 503 (*           if Indexing.subsumption env active_table c then *)
 504 (*             None *)
 505 (*           else ( *)
 506 (*             match passive_table with *)
 507 (*             | None -> res *)
 508 (*             | Some passive_table -> *)
 509 (*                 if Indexing.subsumption env passive_table c then *)
 510 (*                   None *)
 511 (*                 else *)
 512 (*                   res *)
 513 (*           ) *)
 514
 515 (*         let pred (sign, eq) = *)
 516 (*           if sign <> s then false *)
 517 (*           else subsumption env c eq *)
 518 (*         in *)
 519 (*         if List.exists pred all then None *)
 520 (*         else res *)
 521 ;;
 522
 523 type fs_time_info_t = {
 524   mutable build_all: float;
 525   mutable demodulate: float;
 526   mutable subsumption: float;
 527 };;
 528
 529 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
 530
 531
 532 let forward_simplify_new env (new_neg, new_pos) ?passive active =
 533   let t1 = Unix.gettimeofday () in
 534
 535   let active_list, active_table = active in
 536   let pl, passive_table =
 537     match passive with
 538     | None -> [], None
 539     | Some ((pn, _), (pp, _), pt) ->
 540         let pn = List.map (fun e -> (Negative, e)) pn
 541         and pp = List.map (fun e -> (Positive, e)) pp in
 542         pn @ pp, Some pt
 543   in
 544   let all = active_list @ pl in
 545
 546   let t2 = Unix.gettimeofday () in
 547   fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
 548
 549   let demodulate table target =
 550     let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
 551     maxmeta := newmeta;
 552     newtarget
 553   in
 554 (*   let f sign' target (sign, eq) = *)
 555 (*     if sign <> sign' then false *)
 556 (*     else subsumption env target eq  *)
 557 (*   in *)
 558
 559   let t1 = Unix.gettimeofday () in
 560
 561   let new_neg, new_pos =
 562     let new_neg = List.map (demodulate active_table) new_neg
 563     and new_pos = List.map (demodulate active_table) new_pos in
 564     match passive_table with
 565     | None -> new_neg, new_pos
 566     | Some passive_table ->
 567         List.map (demodulate passive_table) new_neg,
 568         List.map (demodulate passive_table) new_pos
 569   in
 570
 571   let t2 = Unix.gettimeofday () in
 572   fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
 573
 574   let new_pos_set =
 575     List.fold_left
 576       (fun s e ->
 577          if not (Inference.is_identity env e) then
 578            if EqualitySet.mem e s then
 579              (Inference.delete_proof e; s)
 580            else
 581              EqualitySet.add e s
 582          else
 583            (Inference.delete_proof e; s))
 584       EqualitySet.empty new_pos
 585   in
 586   let new_pos = EqualitySet.elements new_pos_set in
 587
 588   let subs =
 589     match passive_table with
 590     | None ->
 591         (fun e -> not (Indexing.subsumption env active_table e))
 592     | Some passive_table ->
 593         (fun e -> not ((Indexing.subsumption env active_table e) ||
 594                          (Indexing.subsumption env passive_table e)))
 595   in
 596
 597   let t1 = Unix.gettimeofday () in
 598
 599 (*   let new_neg, new_pos = *)
 600 (*     List.filter subs new_neg, *)
 601 (*     List.filter subs new_pos *)
 602 (*   in *)
 603
 604 (*   let new_neg, new_pos =  *)
 605 (*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
 606 (*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
 607 (*   in *)
 608
 609   let t2 = Unix.gettimeofday () in
 610   fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
 611
 612   let is_duplicate =
 613     match passive_table with
 614     | None ->
 615         (fun e ->
 616            let ok = not (Indexing.in_index active_table e) in
 617            if not ok then Inference.delete_proof e;
 618            ok)
 619     | Some passive_table ->
 620         (fun e ->
 621            let ok = not ((Indexing.in_index active_table e) ||
 622                            (Indexing.in_index passive_table e)) in
 623            if not ok then Inference.delete_proof e;
 624            ok)
 625   in
 626   new_neg, List.filter is_duplicate new_pos
 627
 628 (*   new_neg, new_pos *)
 629
 630 (*   let res = *)
 631 (*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
 632 (*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
 633 (*   in *)
 634 (*   res *)
 635 ;;
 636
 637
 638 let backward_simplify_active env new_pos new_table active =
 639   let active_list, active_table = active in
 640   let active_list, newa =
 641     List.fold_right
 642       (fun (s, equality) (res, newn) ->
 643          match forward_simplify env (s, equality) (new_pos, new_table) with
 644          | None -> res, newn
 645          | Some (s, e) ->
 646              if equality = e then
 647                (s, e)::res, newn
 648              else
 649                res, (s, e)::newn)
 650       active_list ([], [])
 651   in
 652   let find eq1 where =
 653     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 654   in
 655   let active, newa =
 656     List.fold_right
 657       (fun (s, eq) (res, tbl) ->
 658          if List.mem (s, eq) res then
 659            res, tbl
 660          else if (is_identity env eq) || (find eq res) then (
 661            Inference.delete_proof eq;
 662            res, tbl
 663          ) (* else if (find eq res) then *)
 664 (*            res, tbl *)
 665          else
 666            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
 667       active_list ([], Indexing.empty_table ()),
 668     List.fold_right
 669       (fun (s, eq) (n, p) ->
 670          if (s <> Negative) && (is_identity env eq) then (
 671            Inference.delete_proof eq;
 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       Printf.printf "Time limit (%.2f) reached: %.2f\n"
 744         !time_limit !elapsed_time;
 745       make_passive [] []
 746     ) else if kept > selection_estimate then (
 747       Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
 748                        "selection_estimate: %d)\n") kept selection_estimate;
 749       prune_passive selection_estimate active passive
 750     ) else
 751       passive
 752   in
 753
 754   let time2 = Unix.gettimeofday () in
 755   passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
 756
 757   kept_clauses := (size_of_passive passive) + (size_of_active active);
 758
 759   match passive_is_empty passive with
 760   | true -> Failure
 761   | false ->
 762       let (sign, current), passive = select env passive active in
 763       let time1 = Unix.gettimeofday () in
 764       let res = forward_simplify env (sign, current) ~passive active in
 765       let time2 = Unix.gettimeofday () in
 766       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
 767       match res with
 768       | None ->
 769           given_clause env passive active
 770       | Some (sign, current) ->
 771           if (sign = Negative) && (is_identity env current) then (
 772             Printf.printf "OK!!! %s %s" (string_of_sign sign)
 773               (string_of_equality ~env current);
 774             print_newline ();
 775             Success (Some current, env)
 776           ) else (
 777             print_endline "\n================================================";
 778             Printf.printf "selected: %s %s"
 779               (string_of_sign sign) (string_of_equality ~env current);
 780             print_newline ();
 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       Printf.printf "Time limit (%.2f) reached: %.2f\n"
 879         !time_limit !elapsed_time;
 880       make_passive [] []
 881     ) else if kept > selection_estimate then (
 882       Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
 883                        "selection_estimate: %d)\n") kept selection_estimate;
 884       prune_passive selection_estimate active passive
 885     ) else
 886       passive
 887   in
 888
 889   let time2 = Unix.gettimeofday () in
 890   passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
 891
 892   kept_clauses := (size_of_passive passive) + (size_of_active active);
 893
 894   match passive_is_empty passive with
 895   | true -> Failure
 896   | false ->
 897       let (sign, current), passive = select env passive active in
 898       let time1 = Unix.gettimeofday () in
 899       let res = forward_simplify env (sign, current) ~passive active in
 900       let time2 = Unix.gettimeofday () in
 901       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
 902       match res with
 903       | None ->
 904           given_clause_fullred env passive active
 905       | Some (sign, current) ->
 906           if (sign = Negative) && (is_identity env current) then (
 907             Printf.printf "OK!!! %s %s" (string_of_sign sign)
 908               (string_of_equality ~env current);
 909             print_newline ();
 910             Success (Some current, env)
 911           ) else (
 912             print_endline "\n================================================";
 913             Printf.printf "selected: %s %s"
 914               (string_of_sign sign) (string_of_equality ~env current);
 915             print_newline ();
 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 (*               Printf.printf "active:\n%s\n" *)
 958 (*                 (String.concat "\n" *)
 959 (*                    ((List.map *)
 960 (*                        (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
 961 (*                           (string_of_equality ~env e)) (fst active)))); *)
 962 (*               print_newline (); *)
 963 (*             in *)
 964 (*             let _ = *)
 965 (*               match new' with *)
 966 (*               | neg, pos -> *)
 967 (*                   Printf.printf "new':\n%s\n" *)
 968 (*                     (String.concat "\n" *)
 969 (*                        ((List.map *)
 970 (*                            (fun e -> "Negative " ^ *)
 971 (*                               (string_of_equality ~env e)) neg) @ *)
 972 (*                           (List.map *)
 973 (*                              (fun e -> "Positive " ^ *)
 974 (*                                 (string_of_equality ~env e)) pos))); *)
 975 (*                   print_newline (); *)
 976 (*             in *)
 977             match contains_empty env new' with
 978             | false, _ ->
 979                 let passive = add_to_passive passive new' in
 980                 given_clause_fullred env passive active
 981             | true, goal ->
 982                 Success (goal, env)
 983           )
 984 ;;
 985
 986
 987 let get_from_user () =
 988   let dbd = Mysql.quick_connect
 989     ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
 990   let rec get () =
 991     match read_line () with
 992     | "" -> []
 993     | t -> t::(get ())
 994   in
 995   let term_string = String.concat "\n" (get ()) in
 996   let env, metasenv, term, ugraph =
 997     List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
 998   in
 999   term, metasenv, ugraph
1000 ;;
1001
1002
1003 let given_clause_ref = ref given_clause;;
1004
1005
1006 let main () =
1007   let module C = Cic in
1008   let module T = CicTypeChecker in
1009   let module PET = ProofEngineTypes in
1010   let module PP = CicPp in
1011   let term, metasenv, ugraph = get_from_user () in
1012   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
1013   let proof, goals =
1014     PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
1015   let goal = List.nth goals 0 in
1016   let _, metasenv, meta_proof, _ = proof in
1017   let _, context, goal = CicUtil.lookup_meta goal metasenv in
1018   let equalities, maxm = find_equalities context proof in
1019   maxmeta := maxm; (* TODO ugly!! *)
1020   let env = (metasenv, context, ugraph) in
1021   try
1022     let term_equality = equality_of_term meta_proof goal in
1023     let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
1024     let active = make_active () in
1025     let passive = make_passive [term_equality] equalities in
1026     Printf.printf "\ncurrent goal: %s\n"
1027       (string_of_equality ~env term_equality);
1028     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
1029     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
1030     Printf.printf "\nequalities:\n%s\n"
1031       (String.concat "\n"
1032          (List.map
1033             (string_of_equality ~env)
1034             equalities));
1035     print_endline "--------------------------------------------------";
1036     let start = Unix.gettimeofday () in
1037     print_endline "GO!";
1038     start_time := Unix.gettimeofday ();
1039     let res =
1040       (if !use_fullred then given_clause_fullred else given_clause)
1041         env passive active
1042     in
1043     let finish = Unix.gettimeofday () in
1044     let _ =
1045       match res with
1046       | Failure ->
1047           Printf.printf "NO proof found! :-(\n\n"
1048       | Success (Some goal, env) ->
1049           Printf.printf "OK, found a proof!\n";
1050           let proof = Inference.build_term_proof goal in
1051           print_endline (PP.pp proof (names_of_context context));
1052           print_endline (string_of_float (finish -. start));
1053       | Success (None, env) ->
1054           Printf.printf "Success, but no proof?!?\n\n"
1055     in
1056     Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
1057                      "forward_simpl_new_time: %.9f\n" ^^
1058                      "backward_simpl_time: %.9f\n")
1059       !infer_time !forward_simpl_time !forward_simpl_new_time
1060       !backward_simpl_time;
1061     Printf.printf "passive_maintainance_time: %.9f\n"
1062       !passive_maintainance_time;
1063     Printf.printf "    successful unification/matching time: %.9f\n"
1064       !Indexing.match_unif_time_ok;
1065     Printf.printf "    failed unification/matching time: %.9f\n"
1066       !Indexing.match_unif_time_no;
1067     Printf.printf "    indexing retrieval time: %.9f\n"
1068       !Indexing.indexing_retrieval_time;
1069     Printf.printf "    demodulate_term.build_newtarget_time: %.9f\n"
1070       !Indexing.build_newtarget_time;
1071     Printf.printf "derived %d clauses, kept %d clauses.\n"
1072       !derived_clauses !kept_clauses;
1073   with exc ->
1074     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
1075     raise exc
1076 ;;
1077
1078
1079 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
1080
1081 let _ =
1082   let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
1083   and set_sel v = symbols_ratio := v; symbols_counter := v;
1084   and set_conf f = configuration_file := f
1085   and set_lpo () = Utils.compare_terms := lpo
1086   and set_kbo () = Utils.compare_terms := nonrec_kbo
1087   and set_fullred () = use_fullred := true
1088   and set_time_limit v = time_limit := float_of_int v
1089   in
1090   Arg.parse [
1091     "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
1092
1093     "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
1094
1095     "-s", Arg.Int set_sel,
1096     "symbols-based selection ratio (relative to the weight ratio)";
1097
1098     "-c", Arg.String set_conf, "Configuration file (for the db connection)";
1099
1100     "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
1101
1102     "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
1103
1104     "-l", Arg.Int set_time_limit, "Time limit (in seconds)";
1105   ] (fun a -> ()) "Usage:"
1106 in
1107 Helm_registry.load_from !configuration_file;
1108 main ()