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