helm/ocaml/paramodulation/saturation.ml

   1 open Inference;;
   2 open Utils;;
   3
   4 (* profiling statistics... *)
   5 let infer_time = ref 0.;;
   6 let forward_simpl_time = ref 0.;;
   7 let backward_simpl_time = ref 0.;;
   8
   9 (* limited-resource-strategy related globals *)
  10 let processed_clauses = ref 0;; (* number of equalities selected so far... *)
  11 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
  12 let start_time = ref 0.;; (* time at which the execution started *)
  13 let elapsed_time = ref 0.;;
  14 let maximal_retained_equality = ref None;;
  15
  16 (* equality-selection related globals *)
  17 let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
  18 let weight_age_counter = ref !weight_age_ratio;;
  19 let symbols_ratio = ref 0;;
  20 let symbols_counter = ref 0;;
  21
  22 (* index of the greatest Cic.Meta created - TODO: find a better way! *)
  23 let maxmeta = ref 0;;
  24
  25
  26 type result =
  27   | Failure
  28   | Success of Cic.term option * environment
  29 ;;
  30
  31
  32 (*
  33 let symbols_of_equality (_, (_, left, right), _, _) =
  34   TermSet.union (symbols_of_term left) (symbols_of_term right)
  35 ;;
  36 *)
  37
  38 let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
  39   let m1 = symbols_of_term left in
  40   let m =
  41     TermMap.fold
  42       (fun k v res ->
  43          try
  44            let c = TermMap.find k res in
  45            TermMap.add k (c+v) res
  46          with Not_found ->
  47            TermMap.add k v res)
  48       (symbols_of_term right) m1
  49   in
  50 (*   Printf.printf "symbols_of_equality %s:\n" *)
  51 (*     (string_of_equality equality); *)
  52 (*   TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
  53 (*   print_newline (); *)
  54   m
  55 ;;
  56
  57
  58 module OrderedEquality = struct
  59   type t = Inference.equality
  60
  61   let compare eq1 eq2 =
  62     match meta_convertibility_eq eq1 eq2 with
  63     | true -> 0
  64     | false ->
  65         let _, (ty, left, right, _), _, _ = eq1
  66         and _, (ty', left', right', _), _, _ = eq2 in
  67         let weight_of t = fst (weight_of_term ~consider_metas:false t) in
  68         let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
  69         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
  70         match Pervasives.compare w1 w2 with
  71         | 0 -> Pervasives.compare eq1 eq2
  72         | res -> res
  73 end
  74
  75 module EqualitySet = Set.Make(OrderedEquality);;
  76
  77
  78 let select env passive (active, _) =
  79   processed_clauses := !processed_clauses + 1;
  80
  81   let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
  82   let remove eq l =
  83     List.filter (fun e -> e <> eq) l
  84   in
  85   if !weight_age_ratio > 0 then
  86     weight_age_counter := !weight_age_counter - 1;
  87   match !weight_age_counter with
  88   | 0 -> (
  89       weight_age_counter := !weight_age_ratio;
  90       match neg_list, pos_list with
  91       | hd::tl, pos ->
  92           (* Negatives aren't indexed, no need to remove them... *)
  93           (Negative, hd),
  94           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
  95       | [], hd::tl ->
  96           let passive_table = Indexing.remove_index passive_table hd in
  97           (Positive, hd),
  98           (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
  99       | _, _ -> assert false
 100     )
 101   | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
 102       symbols_counter := !symbols_counter - 1;
 103       let cardinality map =
 104         TermMap.fold (fun k v res -> res + v) map 0
 105       in
 106       match active with
 107       | (Negative, e)::_ ->
 108           let symbols = symbols_of_equality e in
 109           let card = cardinality symbols in
 110           let foldfun k v (r1, r2) =
 111             if TermMap.mem k symbols then
 112               let c = TermMap.find k symbols in
 113               let c1 = abs (c - v) in
 114               let c2 = v - c1 in
 115               r1 + c2, r2 + c1
 116             else
 117               r1, r2 + v
 118           in
 119           let f equality (i, e) =
 120             let common, others =
 121               TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 122             in
 123             let c = others + (abs (common - card)) in
 124             if c < i then (c, equality)
 125             else (i, e)
 126           in
 127           let e1 = EqualitySet.min_elt pos_set in
 128           let initial =
 129             let common, others =
 130               TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 131             in
 132             (others + (abs (common - card))), e1
 133           in
 134           let _, current = EqualitySet.fold f pos_set initial in
 135 (*           Printf.printf "\nsymbols-based selection: %s\n\n" *)
 136 (*             (string_of_equality ~env current); *)
 137           let passive_table = Indexing.remove_index passive_table current in
 138           (Positive, current),
 139           (([], neg_set),
 140            (remove current pos_list, EqualitySet.remove current pos_set),
 141            passive_table)
 142       | _ ->
 143           let current = EqualitySet.min_elt pos_set in
 144           let passive =
 145             (neg_list, neg_set),
 146             (remove current pos_list, EqualitySet.remove current pos_set),
 147             Indexing.remove_index passive_table current
 148           in
 149           (Positive, current), passive
 150     )
 151   | _ ->
 152       symbols_counter := !symbols_ratio;
 153       let set_selection set = EqualitySet.min_elt set in
 154       if EqualitySet.is_empty neg_set then
 155         let current = set_selection pos_set in
 156         let passive =
 157           (neg_list, neg_set),
 158           (remove current pos_list, EqualitySet.remove current pos_set),
 159           Indexing.remove_index passive_table current
 160         in
 161         (Positive, current), passive
 162       else
 163         let current = set_selection neg_set in
 164         let passive =
 165           (remove current neg_list, EqualitySet.remove current neg_set),
 166           (pos_list, pos_set),
 167           passive_table
 168         in
 169         (Negative, current), passive
 170 ;;
 171
 172
 173 let make_passive neg pos =
 174   let set_of equalities =
 175     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
 176   in
 177   let table = Indexing.empty_table () in
 178   (neg, set_of neg),
 179   (pos, set_of pos),
 180   List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
 181 ;;
 182
 183
 184 let make_active () =
 185   [], Indexing.empty_table ()
 186 ;;
 187
 188
 189 let add_to_passive passive (new_neg, new_pos) =
 190   let (neg_list, neg_set), (pos_list, pos_set), table = passive in
 191   let ok set equality = not (EqualitySet.mem equality set) in
 192   let neg = List.filter (ok neg_set) new_neg
 193   and pos = List.filter (ok pos_set) new_pos in
 194   let add set equalities =
 195     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
 196   in
 197   (neg @ neg_list, add neg_set neg),
 198   (pos_list @ pos, add pos_set pos),
 199   List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
 200 ;;
 201
 202
 203 let passive_is_empty = function
 204   | ([], _), ([], _), _ -> true
 205   | _ -> false
 206 ;;
 207
 208
 209 let size_of_passive ((_, ns), (_, ps), _) =
 210   (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
 211 ;;
 212
 213
 214 let prune_passive howmany (active, _) passive =
 215   let (nl, ns), (pl, ps), tbl = passive in
 216   let howmany = float_of_int howmany
 217   and ratio = float_of_int !weight_age_ratio in
 218   let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
 219   and in_age = int_of_float (howmany /. (ratio +. 1.)) in
 220   Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age;
 221 (*   let rec pickw w s = *)
 222 (*     if w > 0 then  *)
 223 (*       try *)
 224 (*         let e = EqualitySet.min_elt s in *)
 225 (*         let w, s' = pickw (w-1) (EqualitySet.remove e s) in *)
 226 (*         w, EqualitySet.add e s' *)
 227 (*       with Not_found -> *)
 228 (*         w, s *)
 229 (*     else *)
 230 (*       0, EqualitySet.empty *)
 231 (*   in *)
 232   let symbols, card =
 233     match active with
 234     | (Negative, e)::_ ->
 235         let symbols = symbols_of_equality e in
 236         let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
 237         Some symbols, card
 238     | _ -> None, 0
 239   in
 240   let counter = ref !symbols_ratio in
 241   let rec pickw w ns ps =
 242     if w > 0 then
 243       if not (EqualitySet.is_empty ns) then
 244         let e = EqualitySet.min_elt ns in
 245         let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
 246         EqualitySet.add e ns', ps
 247       else if !counter > 0 then
 248         let _ =
 249           counter := !counter - 1;
 250           if !counter = 0 then counter := !symbols_ratio
 251         in
 252         match symbols with
 253         | None ->
 254             let e = EqualitySet.min_elt ps in
 255             let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 256             ns, EqualitySet.add e ps'
 257         | Some symbols ->
 258             let foldfun k v (r1, r2) =
 259               if TermMap.mem k symbols then
 260                 let c = TermMap.find k symbols in
 261                 let c1 = abs (c - v) in
 262                 let c2 = v - c1 in
 263                 r1 + c2, r2 + c1
 264               else
 265                 r1, r2 + v
 266             in
 267             let f equality (i, e) =
 268               let common, others =
 269                 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 270               in
 271               let c = others + (abs (common - card)) in
 272               if c < i then (c, equality)
 273               else (i, e)
 274             in
 275             let e1 = EqualitySet.min_elt ps in
 276             let initial =
 277               let common, others =
 278                 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 279               in
 280               (others + (abs (common - card))), e1
 281             in
 282             let _, e = EqualitySet.fold f ps initial in
 283             let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 284             ns, EqualitySet.add e ps'
 285       else
 286         let e = EqualitySet.min_elt ps in
 287         let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 288         ns, EqualitySet.add e ps'
 289     else
 290       EqualitySet.empty, EqualitySet.empty
 291   in
 292 (*   let in_weight, ns = pickw in_weight ns in *)
 293 (*   let _, ps = pickw in_weight ps in *)
 294   let ns, ps = pickw in_weight ns ps in
 295   let rec picka w s l =
 296     if w > 0 then
 297       match l with
 298       | [] -> w, s, []
 299       | hd::tl when not (EqualitySet.mem hd s) ->
 300           let w, s, l = picka (w-1) s tl in
 301           w, EqualitySet.add hd s, hd::l
 302       | hd::tl ->
 303           let w, s, l = picka w s tl in
 304           w, s, hd::l
 305     else
 306       0, s, []
 307   in
 308   let in_age, ns, nl = picka in_age ns nl in
 309   let _, ps, pl = picka in_age ps pl in
 310   if not (EqualitySet.is_empty ps) then
 311     maximal_retained_equality := Some (EqualitySet.max_elt ps);
 312   let tbl =
 313     EqualitySet.fold
 314       (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) in
 315   (nl, ns), (pl, ps), tbl
 316 ;;
 317
 318
 319 let infer env sign current (active_list, active_table) =
 320   let new_neg, new_pos =
 321     match sign with
 322     | Negative ->
 323         Indexing.superposition_left env active_table current, []
 324     | Positive ->
 325         let maxm, res =
 326           Indexing.superposition_right !maxmeta env active_table current in
 327         maxmeta := maxm;
 328         let rec infer_positive table = function
 329           | [] -> [], []
 330           | (Negative, equality)::tl ->
 331               let res = Indexing.superposition_left env table equality in
 332               let neg, pos = infer_positive table tl in
 333               res @ neg, pos
 334           | (Positive, equality)::tl ->
 335               let maxm, res =
 336                 Indexing.superposition_right !maxmeta env table equality in
 337               maxmeta := maxm;
 338               let neg, pos = infer_positive table tl in
 339               neg, res @ pos
 340         in
 341         let curr_table = Indexing.index (Indexing.empty_table ()) current in
 342         let neg, pos = infer_positive curr_table active_list in
 343         neg, res @ pos
 344   in
 345   match !maximal_retained_equality with
 346   | None -> new_neg, new_pos
 347   | Some eq ->
 348       let new_pos =
 349         List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos in
 350       new_neg, new_pos
 351 ;;
 352
 353
 354 let contains_empty env (negative, positive) =
 355   let metasenv, context, ugraph = env in
 356   try
 357     let (proof, _, _, _) =
 358       List.find
 359         (fun (proof, (ty, left, right, ordering), m, a) ->
 360            fst (CicReduction.are_convertible context left right ugraph))
 361         negative
 362     in
 363     true, Some proof
 364   with Not_found ->
 365     false, None
 366 ;;
 367
 368
 369 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
 370   let pl, passive_table =
 371     match passive with
 372     | None -> [], None
 373     | Some ((pn, _), (pp, _), pt) ->
 374         let pn = List.map (fun e -> (Negative, e)) pn
 375         and pp = List.map (fun e -> (Positive, e)) pp in
 376         pn @ pp, Some pt
 377   in
 378   let all = active_list @ pl in
 379   let rec find_duplicate sign current = function
 380     | [] -> false
 381     | (s, eq)::tl when s = sign ->
 382         if meta_convertibility_eq current eq then true
 383         else find_duplicate sign current tl
 384     | _::tl -> find_duplicate sign current tl
 385   in
 386   let demodulate table current =
 387     let newmeta, newcurrent =
 388       Indexing.demodulation !maxmeta env table current in
 389     maxmeta := newmeta;
 390     if is_identity env newcurrent then
 391       if sign = Negative then Some (sign, newcurrent) else None
 392     else
 393       Some (sign, newcurrent)
 394   in
 395   let res =
 396     let res = demodulate active_table current in
 397     match res with
 398     | None -> None
 399     | Some (sign, newcurrent) ->
 400         match passive_table with
 401         | None -> res
 402         | Some passive_table -> demodulate passive_table newcurrent
 403   in
 404   match res with
 405   | None -> None
 406   | Some (s, c) ->
 407       if find_duplicate s c all then
 408         None
 409       else
 410         res
 411 (*         if s = Utils.Negative then *)
 412 (*           res *)
 413 (*         else *)
 414 (*           if Indexing.subsumption env active_table c then *)
 415 (*             None *)
 416 (*           else ( *)
 417 (*             match passive_table with *)
 418 (*             | None -> res *)
 419 (*             | Some passive_table -> *)
 420 (*                 if Indexing.subsumption env passive_table c then *)
 421 (*                   None *)
 422 (*                 else *)
 423 (*                   res *)
 424 (*           ) *)
 425
 426 (*         let pred (sign, eq) = *)
 427 (*           if sign <> s then false *)
 428 (*           else subsumption env c eq *)
 429 (*         in *)
 430 (*         if List.exists pred all then None *)
 431 (*         else res *)
 432 ;;
 433
 434 type fs_time_info_t = {
 435   mutable build_all: float;
 436   mutable demodulate: float;
 437   mutable subsumption: float;
 438 };;
 439
 440 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
 441
 442
 443 let forward_simplify_new env (new_neg, new_pos) ?passive active =
 444   let t1 = Unix.gettimeofday () in
 445
 446   let active_list, active_table = active in
 447   let pl, passive_table =
 448     match passive with
 449     | None -> [], None
 450     | Some ((pn, _), (pp, _), pt) ->
 451         let pn = List.map (fun e -> (Negative, e)) pn
 452         and pp = List.map (fun e -> (Positive, e)) pp in
 453         pn @ pp, Some pt
 454   in
 455   let all = active_list @ pl in
 456
 457   let t2 = Unix.gettimeofday () in
 458   fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
 459
 460   let demodulate table target =
 461     let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
 462     maxmeta := newmeta;
 463     newtarget
 464   in
 465 (*   let f sign' target (sign, eq) = *)
 466 (*     if sign <> sign' then false *)
 467 (*     else subsumption env target eq  *)
 468 (*   in *)
 469
 470   let t1 = Unix.gettimeofday () in
 471
 472   let new_neg, new_pos =
 473     let new_neg = List.map (demodulate active_table) new_neg
 474     and new_pos = List.map (demodulate active_table) new_pos in
 475     match passive_table with
 476     | None -> new_neg, new_pos
 477     | Some passive_table ->
 478         List.map (demodulate passive_table) new_neg,
 479         List.map (demodulate passive_table) new_pos
 480   in
 481
 482   let t2 = Unix.gettimeofday () in
 483   fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
 484
 485   let new_pos_set =
 486     List.fold_left
 487       (fun s e ->
 488          if not (Inference.is_identity env e) then EqualitySet.add e s else s)
 489       EqualitySet.empty new_pos
 490   in
 491   let new_pos = EqualitySet.elements new_pos_set in
 492
 493   let subs =
 494     match passive_table with
 495     | None ->
 496         (fun e -> not (Indexing.subsumption env active_table e))
 497     | Some passive_table ->
 498         (fun e -> not ((Indexing.subsumption env active_table e) ||
 499                          (Indexing.subsumption env passive_table e)))
 500   in
 501
 502   let t1 = Unix.gettimeofday () in
 503
 504 (*   let new_neg, new_pos = *)
 505 (*     List.filter subs new_neg, *)
 506 (*     List.filter subs new_pos *)
 507 (*   in *)
 508
 509 (*   let new_neg, new_pos =  *)
 510 (*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
 511 (*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
 512 (*   in *)
 513
 514   let t2 = Unix.gettimeofday () in
 515   fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
 516
 517   new_neg, new_pos
 518 (*   let res = *)
 519 (*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
 520 (*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
 521 (*   in *)
 522 (*   res *)
 523 ;;
 524
 525
 526 let backward_simplify_active env (new_neg, new_pos) active =
 527   let active_list, active_table = active in
 528   let new_pos, new_table =
 529     List.fold_left
 530       (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
 531       ([], Indexing.empty_table ()) new_pos
 532   in
 533   let active_list, newa =
 534     List.fold_right
 535       (fun (s, equality) (res, newn) ->
 536          match forward_simplify env (s, equality) (new_pos, new_table) with
 537          | None -> res, newn
 538          | Some (s, e) ->
 539              if equality = e then
 540                (s, e)::res, newn
 541              else
 542                res, (s, e)::newn)
 543       active_list ([], [])
 544   in
 545   let find eq1 where =
 546     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 547   in
 548   let active, newa =
 549     List.fold_right
 550       (fun (s, eq) (res, tbl) ->
 551          if (is_identity env eq) || (find eq res) then
 552            res, tbl
 553          else
 554            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
 555       active_list ([], Indexing.empty_table ()),
 556     List.fold_right
 557       (fun (s, eq) (n, p) ->
 558          if (s <> Negative) && (is_identity env eq) then
 559            (n, p)
 560          else
 561            if s = Negative then eq::n, p
 562            else n, eq::p)
 563       newa ([], [])
 564   in
 565   match newa with
 566   | [], [] -> active, None
 567   | _ -> active, Some newa
 568 ;;
 569
 570
 571 let backward_simplify_passive env (new_neg, new_pos) passive =
 572   let new_pos, new_table =
 573     List.fold_left
 574       (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
 575       ([], Indexing.empty_table ()) new_pos
 576   in
 577   let (nl, ns), (pl, ps), passive_table = passive in
 578   let f sign equality (resl, ress, newn) =
 579     match forward_simplify env (sign, equality) (new_pos, new_table) with
 580     | None -> resl, EqualitySet.remove equality ress, newn
 581     | Some (s, e) ->
 582         if equality = e then
 583           equality::resl, ress, newn
 584         else
 585           let ress = EqualitySet.remove equality ress in
 586           resl, ress, e::newn
 587   in
 588   let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
 589   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
 590   let passive_table =
 591     List.fold_left
 592       (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
 593   in
 594   match newn, newp with
 595   | [], [] -> ((nl, ns), (pl, ps), passive_table), None
 596   | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
 597 ;;
 598
 599
 600 let backward_simplify env new' ?passive active =
 601   let active, newa = backward_simplify_active env new' active in
 602   match passive with
 603   | None ->
 604       active, (make_passive [] []), newa, None
 605   | Some passive ->
 606       let passive, newp =
 607         backward_simplify_passive env new' passive in
 608       active, passive, newa, newp
 609 ;;
 610
 611
 612 let get_selection_estimate () =
 613   elapsed_time := (Unix.gettimeofday ()) -. !start_time;
 614   !processed_clauses * (int_of_float (!time_limit /. !elapsed_time))
 615 ;;
 616
 617
 618 let rec given_clause env passive active =
 619   let selection_estimate = get_selection_estimate () in
 620   let kept = size_of_passive passive in
 621   let passive =
 622     if !time_limit = 0. || !processed_clauses = 0 then
 623       passive
 624     else if !elapsed_time > !time_limit then (
 625       Printf.printf "Time limit (%.2f) reached: %.2f\n"
 626         !time_limit !elapsed_time;
 627       make_passive [] []
 628     ) else if kept > selection_estimate then (
 629       Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
 630                        "selection_estimate: %d)\n") kept selection_estimate;
 631       prune_passive selection_estimate active passive
 632     ) else
 633       passive
 634   in
 635
 636   match passive_is_empty passive with
 637   | true -> Failure
 638   | false ->
 639       let (sign, current), passive = select env passive active in
 640       match forward_simplify env (sign, current) ~passive active with
 641       | None ->
 642           given_clause env passive active
 643       | Some (sign, current) ->
 644           if (sign = Negative) && (is_identity env current) then (
 645             Printf.printf "OK!!! %s %s" (string_of_sign sign)
 646               (string_of_equality ~env current);
 647             print_newline ();
 648             let proof, _, _, _ = current in
 649             Success (Some proof, env)
 650           ) else (
 651             print_endline "\n================================================";
 652             Printf.printf "selected: %s %s"
 653               (string_of_sign sign) (string_of_equality ~env current);
 654             print_newline ();
 655
 656             let t1 = Unix.gettimeofday () in
 657             let new' = infer env sign current active in
 658             let t2 = Unix.gettimeofday () in
 659             infer_time := !infer_time +. (t2 -. t1);
 660
 661             let res, proof = contains_empty env new' in
 662             if res then
 663               Success (proof, env)
 664             else
 665               let t1 = Unix.gettimeofday () in
 666               let new' = forward_simplify_new env new' active in
 667               let t2 = Unix.gettimeofday () in
 668               let _ =
 669                 forward_simpl_time := !forward_simpl_time +. (t2 -. t1)
 670               in
 671               let active =
 672                 match sign with
 673                 | Negative -> active
 674                 | Positive ->
 675                     let t1 = Unix.gettimeofday () in
 676                     let active, _, newa, _ =
 677                       backward_simplify env ([], [current]) active
 678                     in
 679                     let t2 = Unix.gettimeofday () in
 680                     backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
 681                     match newa with
 682                     | None -> active
 683                     | Some (n, p) ->
 684                         let al, tbl = active in
 685                         let nn = List.map (fun e -> Negative, e) n in
 686                         let pp, tbl =
 687                           List.fold_right
 688                             (fun e (l, t) ->
 689                                (Positive, e)::l,
 690                                Indexing.index tbl e)
 691                             p ([], tbl)
 692                         in
 693                         nn @ al @ pp, tbl
 694               in
 695               let _ =
 696                 Printf.printf "active:\n%s\n"
 697                   (String.concat "\n"
 698                      ((List.map
 699                          (fun (s, e) -> (string_of_sign s) ^ " " ^
 700                             (string_of_equality ~env e)) (fst active))));
 701                 print_newline ();
 702               in
 703               let _ =
 704                 match new' with
 705                 | neg, pos ->
 706                     Printf.printf "new':\n%s\n"
 707                       (String.concat "\n"
 708                          ((List.map
 709                              (fun e -> "Negative " ^
 710                                 (string_of_equality ~env e)) neg) @
 711                             (List.map
 712                                (fun e -> "Positive " ^
 713                                   (string_of_equality ~env e)) pos)));
 714                     print_newline ();
 715               in
 716               match contains_empty env new' with
 717               | false, _ ->
 718                   let active =
 719                     let al, tbl = active in
 720                     match sign with
 721                     | Negative -> (sign, current)::al, tbl
 722                     | Positive ->
 723                         al @ [(sign, current)], Indexing.index tbl current
 724                   in
 725                   let passive = add_to_passive passive new' in
 726                   let (_, ns), (_, ps), _ = passive in
 727                   Printf.printf "passive:\n%s\n"
 728                     (String.concat "\n"
 729                        ((List.map (fun e -> "Negative " ^
 730                                      (string_of_equality ~env e))
 731                            (EqualitySet.elements ns)) @
 732                           (List.map (fun e -> "Positive " ^
 733                                        (string_of_equality ~env e))
 734                              (EqualitySet.elements ps))));
 735                   print_newline ();
 736                   given_clause env passive active
 737               | true, proof ->
 738                   Success (proof, env)
 739           )
 740 ;;
 741
 742
 743 let rec given_clause_fullred env passive active =
 744   let selection_estimate = get_selection_estimate () in
 745   let kept = size_of_passive passive in
 746   let passive =
 747     if !time_limit = 0. || !processed_clauses = 0 then
 748       passive
 749     else if !elapsed_time > !time_limit then (
 750       Printf.printf "Time limit (%.2f) reached: %.2f\n"
 751         !time_limit !elapsed_time;
 752       make_passive [] []
 753     ) else if kept > selection_estimate then (
 754       Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^
 755                        "selection_estimate: %d)\n") kept selection_estimate;
 756       prune_passive selection_estimate active passive
 757     ) else
 758       passive
 759   in
 760
 761   match passive_is_empty passive with
 762   | true -> Failure
 763   | false ->
 764       let (sign, current), passive = select env passive active in
 765       match forward_simplify env (sign, current) ~passive active with
 766       | None ->
 767           given_clause_fullred env passive active
 768       | Some (sign, current) ->
 769           if (sign = Negative) && (is_identity env current) then (
 770             Printf.printf "OK!!! %s %s" (string_of_sign sign)
 771               (string_of_equality ~env current);
 772             print_newline ();
 773             let proof, _, _, _ = current in
 774             Success (Some proof, env)
 775           ) else (
 776             print_endline "\n================================================";
 777             Printf.printf "selected: %s %s"
 778               (string_of_sign sign) (string_of_equality ~env current);
 779             print_newline ();
 780
 781             let t1 = Unix.gettimeofday () in
 782             let new' = infer env sign current active in
 783             let t2 = Unix.gettimeofday () in
 784             infer_time := !infer_time +. (t2 -. t1);
 785
 786             let active =
 787               if is_identity env current then active
 788               else
 789                 let al, tbl = active in
 790                 match sign with
 791                 | Negative -> (sign, current)::al, tbl
 792                 | Positive -> al @ [(sign, current)], Indexing.index tbl current
 793             in
 794             let rec simplify new' active passive =
 795               let t1 = Unix.gettimeofday () in
 796               let new' = forward_simplify_new env new' ~passive active in
 797               let t2 = Unix.gettimeofday () in
 798               forward_simpl_time := !forward_simpl_time +. (t2 -. t1);
 799               let t1 = Unix.gettimeofday () in
 800               let active, passive, newa, retained =
 801                 backward_simplify env new' ~passive active in
 802               let t2 = Unix.gettimeofday () in
 803               backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
 804               match newa, retained with
 805               | None, None -> active, passive, new'
 806               | Some (n, p), None
 807               | None, Some (n, p) ->
 808                   let nn, np = new' in
 809                   simplify (nn @ n, np @ p) active passive
 810               | Some (n, p), Some (rn, rp) ->
 811                   let nn, np = new' in
 812                   simplify (nn @ n @ rn, np @ p @ rp) active passive
 813             in
 814             let active, passive, new' = simplify new' active passive in
 815
 816             let k = size_of_passive passive in
 817             if k < (kept - 1) then
 818               processed_clauses := !processed_clauses + (kept - 1 - k);
 819
 820             let _ =
 821               Printf.printf "active:\n%s\n"
 822                 (String.concat "\n"
 823                    ((List.map
 824                        (fun (s, e) -> (string_of_sign s) ^ " " ^
 825                           (string_of_equality ~env e)) (fst active))));
 826               print_newline ();
 827             in
 828             let _ =
 829               match new' with
 830               | neg, pos ->
 831                   Printf.printf "new':\n%s\n"
 832                     (String.concat "\n"
 833                        ((List.map
 834                            (fun e -> "Negative " ^
 835                               (string_of_equality ~env e)) neg) @
 836                           (List.map
 837                              (fun e -> "Positive " ^
 838                                 (string_of_equality ~env e)) pos)));
 839                   print_newline ();
 840             in
 841             match contains_empty env new' with
 842             | false, _ ->
 843                 let passive = add_to_passive passive new' in
 844                 given_clause_fullred env passive active
 845             | true, proof ->
 846                 Success (proof, env)
 847           )
 848 ;;
 849
 850
 851 let get_from_user () =
 852   let dbd = Mysql.quick_connect
 853     ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
 854   let rec get () =
 855     match read_line () with
 856     | "" -> []
 857     | t -> t::(get ())
 858   in
 859   let term_string = String.concat "\n" (get ()) in
 860   let env, metasenv, term, ugraph =
 861     List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
 862   in
 863   term, metasenv, ugraph
 864 ;;
 865
 866
 867 let given_clause_ref = ref given_clause;;
 868
 869
 870 let main () =
 871   let module C = Cic in
 872   let module T = CicTypeChecker in
 873   let module PET = ProofEngineTypes in
 874   let module PP = CicPp in
 875   let term, metasenv, ugraph = get_from_user () in
 876   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
 877   let proof, goals =
 878     PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
 879   let goal = List.nth goals 0 in
 880   let _, metasenv, meta_proof, _ = proof in
 881   let _, context, goal = CicUtil.lookup_meta goal metasenv in
 882   let equalities, maxm = find_equalities context proof in
 883   maxmeta := maxm; (* TODO ugly!! *)
 884   let env = (metasenv, context, ugraph) in
 885   try
 886     let term_equality = equality_of_term meta_proof goal in
 887     let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
 888     let active = make_active () in
 889     let passive = make_passive [term_equality] equalities in
 890     Printf.printf "\ncurrent goal: %s\n"
 891       (string_of_equality ~env term_equality);
 892     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
 893     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
 894     Printf.printf "\nequalities:\n%s\n"
 895       (String.concat "\n"
 896          (List.map
 897             (string_of_equality ~env)
 898             equalities));
 899     print_endline "--------------------------------------------------";
 900     let start = Unix.gettimeofday () in
 901     print_endline "GO!";
 902     start_time := Unix.gettimeofday ();
 903     let res = !given_clause_ref env passive active in
 904     let finish = Unix.gettimeofday () in
 905     match res with
 906     | Failure ->
 907         Printf.printf "NO proof found! :-(\n\n"
 908     | Success (Some proof, env) ->
 909         Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
 910           (PP.pp proof (names_of_context context))
 911           (finish -. start);
 912         Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
 913                          "backward_simpl_time: %.9f\n")
 914           !infer_time !forward_simpl_time !backward_simpl_time;
 915 (*         Printf.printf ("forward_simpl_details:\n  build_all: %.9f\n" ^^ *)
 916 (*                          "  demodulate: %.9f\n  subsumption: %.9f\n") *)
 917 (*           fs_time_info.build_all fs_time_info.demodulate *)
 918 (*           fs_time_info.subsumption; *)
 919     | Success (None, env) ->
 920         Printf.printf "Success, but no proof?!?\n\n"
 921   with exc ->
 922     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
 923     raise exc
 924 ;;
 925
 926
 927 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
 928
 929 let _ =
 930   let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
 931   and set_sel v = symbols_ratio := v; symbols_counter := v;
 932   and set_conf f = configuration_file := f
 933   and set_lpo () = Utils.compare_terms := lpo
 934   and set_kbo () = Utils.compare_terms := nonrec_kbo
 935   and set_fullred () = given_clause_ref := given_clause_fullred
 936   and set_time_limit v = time_limit := float_of_int v
 937   in
 938   Arg.parse [
 939     "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
 940
 941     "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
 942
 943     "-s", Arg.Int set_sel,
 944     "symbols-based selection ratio (relative to the weight ratio)";
 945
 946     "-c", Arg.String set_conf, "Configuration file (for the db connection)";
 947
 948     "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
 949
 950     "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
 951
 952     "-l", Arg.Int set_time_limit, "Time limit (in seconds)";
 953   ] (fun a -> ()) "Usage:"
 954 in
 955 Helm_registry.load_from !configuration_file;
 956 main ()