helm/ocaml/paramodulation/saturation.ml

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