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