helm/ocaml/paramodulation/saturation.ml

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