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