helm/ocaml/paramodulation/saturation.ml

   1 open Inference;;
   2 open Utils;;
   3
   4 type result =
   5   | Failure
   6   | Success of Cic.term option * environment
   7 ;;
   8
   9
  10 (*
  11 let symbols_of_equality (_, (_, left, right), _, _) =
  12   TermSet.union (symbols_of_term left) (symbols_of_term right)
  13 ;;
  14 *)
  15
  16 let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
  17   let m1 = symbols_of_term left in
  18   let m =
  19     TermMap.fold
  20       (fun k v res ->
  21          try
  22            let c = TermMap.find k res in
  23            TermMap.add k (c+v) res
  24          with Not_found ->
  25            TermMap.add k v res)
  26       (symbols_of_term right) m1
  27   in
  28 (*   Printf.printf "symbols_of_equality %s:\n" *)
  29 (*     (string_of_equality equality); *)
  30 (*   TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
  31 (*   print_newline (); *)
  32   m
  33 ;;
  34
  35
  36 module OrderedEquality =
  37 struct
  38   type t = Inference.equality
  39
  40   let compare eq1 eq2 =
  41     match meta_convertibility_eq eq1 eq2 with
  42     | true -> 0
  43     | false ->
  44         let _, (ty, left, right, _), _, _ = eq1
  45         and _, (ty', left', right', _), _, _ = eq2 in
  46         let weight_of t = fst (weight_of_term ~consider_metas:false t) in
  47         let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
  48         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
  49         match Pervasives.compare w1 w2 with
  50         | 0 -> Pervasives.compare eq1 eq2
  51         | res -> res
  52 end
  53
  54 module EqualitySet = Set.Make(OrderedEquality);;
  55
  56
  57 let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
  58 let weight_age_counter = ref !weight_age_ratio;;
  59
  60 let symbols_ratio = ref 0;;
  61 let symbols_counter = ref 0;;
  62
  63
  64 let select env passive (active, _) =
  65   let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
  66   let remove eq l =
  67     List.filter (fun e -> e <> eq) l
  68   in
  69   if !weight_age_ratio > 0 then
  70     weight_age_counter := !weight_age_counter - 1;
  71   match !weight_age_counter with
  72   | 0 -> (
  73       weight_age_counter := !weight_age_ratio;
  74       match neg_list, pos_list with
  75       | hd::tl, pos ->
  76           (* Negatives aren't indexed, no need to remove them... *)
  77           (Negative, hd),
  78           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
  79       | [], hd::tl ->
  80           let passive_table = Indexing.remove_index passive_table hd in
  81           (Positive, hd),
  82           (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
  83       | _, _ -> assert false
  84     )
  85   | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
  86       symbols_counter := !symbols_counter - 1;
  87       let cardinality map =
  88         TermMap.fold (fun k v res -> res + v) map 0
  89       in
  90       match active with
  91       | (Negative, e)::_ ->
  92           let symbols = symbols_of_equality e in
  93           let card = cardinality symbols in
  94           let f equality (i, e) =
  95             let common, others =
  96               TermMap.fold
  97                 (fun k v (r1, r2) ->
  98                    if TermMap.mem k symbols then
  99                      let c = TermMap.find k symbols in
 100                      let c1 = abs (c - v) in
 101                      let c2 = v - c1 in
 102                      r1 + c2, r2 + c1
 103                    else
 104                      r1, r2 + v)
 105                 (symbols_of_equality equality) (0, 0)
 106             in
 107 (*             Printf.printf "equality: %s, common: %d, others: %d\n" *)
 108 (*               (string_of_equality ~env equality) common others; *)
 109             let c = others + (abs (common - card)) in
 110             if c < i then (c, equality)
 111             else (i, e)
 112           in
 113           let e1 = EqualitySet.min_elt pos_set in
 114           let initial =
 115             let common, others =
 116               TermMap.fold
 117                 (fun k v (r1, r2) ->
 118                    if TermMap.mem k symbols then
 119                      let c = TermMap.find k symbols in
 120                      let c1 = abs (c - v) in
 121                      let c2 = v - (abs (c - v)) in
 122                      r1 + c1, r2 + c2
 123                    else
 124                      r1, r2 + v)
 125                 (symbols_of_equality e1) (0, 0)
 126             in
 127             (others + (abs (common - card))), e1
 128           in
 129           let _, current = EqualitySet.fold f pos_set initial in
 130 (*           Printf.printf "\nsymbols-based selection: %s\n\n" *)
 131 (*             (string_of_equality ~env current); *)
 132           let passive_table = Indexing.remove_index passive_table current in
 133           (Positive, current),
 134           (([], neg_set),
 135            (remove current pos_list, EqualitySet.remove current pos_set),
 136            passive_table)
 137       | _ ->
 138             let current = EqualitySet.min_elt pos_set in
 139           let passive =
 140             (neg_list, neg_set),
 141             (remove current pos_list, EqualitySet.remove current pos_set),
 142             Indexing.remove_index passive_table current
 143           in
 144           (Positive, current), passive
 145     )
 146   | _ ->
 147       symbols_counter := !symbols_ratio;
 148       let set_selection set = EqualitySet.min_elt set in
 149       if EqualitySet.is_empty neg_set then
 150         let current = set_selection pos_set in
 151         let passive =
 152           (neg_list, neg_set),
 153           (remove current pos_list, EqualitySet.remove current pos_set),
 154           Indexing.remove_index passive_table current
 155         in
 156         (Positive, current), passive
 157       else
 158         let current = set_selection neg_set in
 159         let passive =
 160           (remove current neg_list, EqualitySet.remove current neg_set),
 161           (pos_list, pos_set),
 162           passive_table
 163         in
 164         (Negative, current), passive
 165 ;;
 166
 167
 168 let make_passive neg pos =
 169   let set_of equalities =
 170     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
 171   in
 172   let table = Hashtbl.create (List.length pos) in
 173   (neg, set_of neg),
 174   (pos, set_of pos),
 175   List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
 176 ;;
 177
 178
 179 let make_active () =
 180   [], Hashtbl.create 1
 181 ;;
 182
 183
 184 let add_to_passive passive (new_neg, new_pos) =
 185   let (neg_list, neg_set), (pos_list, pos_set), table = passive in
 186   let ok set equality = not (EqualitySet.mem equality set) in
 187   let neg = List.filter (ok neg_set) new_neg
 188   and pos = List.filter (ok pos_set) new_pos in
 189   let add set equalities =
 190     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
 191   in
 192   (neg @ neg_list, add neg_set neg),
 193   (pos_list @ pos, add pos_set pos),
 194   List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
 195 ;;
 196
 197
 198 let passive_is_empty = function
 199   | ([], _), ([], _), _ -> true
 200   | _ -> false
 201 ;;
 202
 203
 204 (* TODO: find a better way! *)
 205 let maxmeta = ref 0;;
 206
 207 let infer env sign current (active_list, active_table) =
 208   match sign with
 209   | Negative ->
 210       Indexing.superposition_left env active_table current, []
 211   | Positive ->
 212       let maxm, res =
 213         Indexing.superposition_right !maxmeta env active_table current in
 214       maxmeta := maxm;
 215       let rec infer_positive table = function
 216         | [] -> [], []
 217         | (Negative, equality)::tl ->
 218             let res = Indexing.superposition_left env table equality in
 219             let neg, pos = infer_positive table tl in
 220             res @ neg, pos
 221         | (Positive, equality)::tl ->
 222             let maxm, res =
 223               Indexing.superposition_right !maxmeta env table equality in
 224             maxmeta := maxm;
 225             let neg, pos = infer_positive table tl in
 226             neg, res @ pos
 227       in
 228       let curr_table = Indexing.index (Hashtbl.create 1) current in
 229       let neg, pos = infer_positive curr_table active_list in
 230       neg, res @ pos
 231 ;;
 232
 233
 234 let contains_empty env (negative, positive) =
 235   let metasenv, context, ugraph = env in
 236   try
 237     let (proof, _, _, _) =
 238       List.find
 239         (fun (proof, (ty, left, right, ordering), m, a) ->
 240            fst (CicReduction.are_convertible context left right ugraph))
 241         negative
 242     in
 243     true, Some proof
 244   with Not_found ->
 245     false, None
 246 ;;
 247
 248
 249 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
 250   let pl, passive_table =
 251     match passive with
 252     | None -> [], None
 253     | Some ((pn, _), (pp, _), pt) ->
 254         let pn = List.map (fun e -> (Negative, e)) pn
 255         and pp = List.map (fun e -> (Positive, e)) pp in
 256         pn @ pp, Some pt
 257   in
 258   let all = active_list @ pl in
 259   let rec find_duplicate sign current = function
 260     | [] -> false
 261     | (s, eq)::tl when s = sign ->
 262         if meta_convertibility_eq current eq then true
 263         else find_duplicate sign current tl
 264     | _::tl -> find_duplicate sign current tl
 265   in
 266   let demodulate table current =
 267     let newmeta, newcurrent =
 268       Indexing.demodulation !maxmeta env table current in
 269     maxmeta := newmeta;
 270     if is_identity env newcurrent then
 271       if sign = Negative then Some (sign, newcurrent) else None
 272     else
 273       Some (sign, newcurrent)
 274   in
 275   let res =
 276     let res = demodulate active_table current in
 277     match res with
 278     | None -> None
 279     | Some (sign, newcurrent) ->
 280         match passive_table with
 281         | None -> res
 282         | Some passive_table -> demodulate passive_table newcurrent
 283   in
 284   match res with
 285   | None -> None
 286   | Some (s, c) ->
 287       if find_duplicate s c all then
 288         None
 289       else
 290         let pred (sign, eq) =
 291           if sign <> s then false
 292           else subsumption env c eq
 293         in
 294         if List.exists pred all then None
 295         else res
 296 ;;
 297
 298
 299 let forward_simplify_new env (new_neg, new_pos) ?passive active =
 300   let active_list, active_table = active in
 301   let pl, passive_table =
 302     match passive with
 303     | None -> [], None
 304     | Some ((pn, _), (pp, _), pt) ->
 305         let pn = List.map (fun e -> (Negative, e)) pn
 306         and pp = List.map (fun e -> (Positive, e)) pp in
 307         pn @ pp, Some pt
 308   in
 309   let all = active_list @ pl in
 310   let demodulate table target =
 311     let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
 312     maxmeta := newmeta;
 313     newtarget
 314   in
 315   let new_neg, new_pos =
 316     let new_neg = List.map (demodulate active_table) new_neg
 317     and new_pos = List.map (demodulate active_table) new_pos in
 318     match passive_table with
 319     | None -> new_neg, new_pos
 320     | Some passive_table ->
 321         List.map (demodulate passive_table) new_neg,
 322         List.map (demodulate passive_table) new_pos
 323   in
 324   let new_pos_set =
 325     List.fold_left
 326       (fun s e ->
 327          if not (Inference.is_identity env e) then EqualitySet.add e s else s)
 328       EqualitySet.empty new_pos
 329   in
 330   let new_pos = EqualitySet.elements new_pos_set in
 331   let f sign' target (sign, eq) =
 332     if sign <> sign' then false
 333     else subsumption env target eq
 334   in
 335   (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
 336    List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
 337 ;;
 338
 339
 340 let backward_simplify_active env (new_neg, new_pos) active =
 341   let active_list, active_table = active in
 342   let new_pos, new_table =
 343     List.fold_left
 344       (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
 345       ([], Hashtbl.create (List.length new_pos)) new_pos
 346   in
 347   let active_list, newa =
 348     List.fold_right
 349       (fun (s, equality) (res, newn) ->
 350          match forward_simplify env (s, equality) (new_pos, new_table) with
 351          | None -> res, newn
 352          | Some (s, e) ->
 353              if equality = e then
 354                (s, e)::res, newn
 355              else
 356                res, (s, e)::newn)
 357       active_list ([], [])
 358   in
 359   let find eq1 where =
 360     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 361   in
 362   let active, newa =
 363     List.fold_right
 364       (fun (s, eq) (res, tbl) ->
 365          if (is_identity env eq) || (find eq res) then
 366            res, tbl
 367          else
 368            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
 369       active_list ([], Hashtbl.create (List.length active_list)),
 370     List.fold_right
 371       (fun (s, eq) (n, p) ->
 372          if (s <> Negative) && (is_identity env eq) then
 373            (n, p)
 374          else
 375            if s = Negative then eq::n, p
 376            else n, eq::p)
 377       newa ([], [])
 378   in
 379   match newa with
 380   | [], [] -> active, None
 381   | _ -> active, Some newa
 382 ;;
 383
 384
 385 let backward_simplify_passive env (new_neg, new_pos) passive =
 386   let new_pos, new_table =
 387     List.fold_left
 388       (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
 389       ([], Hashtbl.create (List.length new_pos)) new_pos
 390   in
 391   let (nl, ns), (pl, ps), passive_table = passive in
 392   let f sign equality (resl, ress, newn) =
 393     match forward_simplify env (sign, equality) (new_pos, new_table) with
 394     | None -> resl, EqualitySet.remove equality ress, newn
 395     | Some (s, e) ->
 396         if equality = e then
 397           equality::resl, ress, newn
 398         else
 399           let ress = EqualitySet.remove equality ress in
 400           resl, ress, e::newn
 401   in
 402   let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
 403   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
 404   let passive_table =
 405     List.fold_left
 406       (fun tbl e -> Indexing.index tbl e) (Hashtbl.create (List.length pl)) pl
 407   in
 408   match newn, newp with
 409   | [], [] -> ((nl, ns), (pl, ps), passive_table), None
 410   | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
 411 ;;
 412
 413
 414 let backward_simplify env new' ?passive active =
 415   let active, newa = backward_simplify_active env new' active in
 416   match passive with
 417   | None ->
 418       active, (make_passive [] []), newa, None
 419   | Some passive ->
 420       let passive, newp =
 421         backward_simplify_passive env new' passive in
 422       active, passive, newa, newp
 423 ;;
 424
 425
 426 let rec given_clause env passive active =
 427   match passive_is_empty passive with
 428   | true -> Failure
 429   | false ->
 430       let (sign, current), passive = select env passive active in
 431       match forward_simplify env (sign, current) ~passive active with
 432       | None ->
 433           given_clause env passive active
 434       | Some (sign, current) ->
 435           if (sign = Negative) && (is_identity env current) then (
 436             Printf.printf "OK!!! %s %s" (string_of_sign sign)
 437               (string_of_equality ~env current);
 438             print_newline ();
 439             let proof, _, _, _ = current in
 440             Success (Some proof, env)
 441           ) else (
 442             print_endline "\n================================================";
 443             Printf.printf "selected: %s %s"
 444               (string_of_sign sign) (string_of_equality ~env current);
 445             print_newline ();
 446
 447             let new' = infer env sign current active in
 448             let res, proof = contains_empty env new' in
 449             if res then
 450               Success (proof, env)
 451             else
 452               let new' = forward_simplify_new env new' active in
 453               let active =
 454                 match sign with
 455                 | Negative -> active
 456                 | Positive ->
 457                     let active, _, newa, _ =
 458                       backward_simplify env ([], [current]) active
 459                     in
 460                     match newa with
 461                     | None -> active
 462                     | Some (n, p) ->
 463                         let al, tbl = active in
 464                         let nn = List.map (fun e -> Negative, e) n in
 465                         let pp, tbl =
 466                           List.fold_right
 467                             (fun e (l, t) ->
 468                                (Positive, e)::l,
 469                                Indexing.index tbl e)
 470                             p ([], tbl)
 471                         in
 472                         nn @ al @ pp, tbl
 473               in
 474               let _ =
 475                 Printf.printf "active:\n%s\n"
 476                   (String.concat "\n"
 477                      ((List.map
 478                          (fun (s, e) -> (string_of_sign s) ^ " " ^
 479                             (string_of_equality ~env e)) (fst active))));
 480                 print_newline ();
 481               in
 482               let _ =
 483                 match new' with
 484                 | neg, pos ->
 485                     Printf.printf "new':\n%s\n"
 486                       (String.concat "\n"
 487                          ((List.map
 488                              (fun e -> "Negative " ^
 489                                 (string_of_equality ~env e)) neg) @
 490                             (List.map
 491                                (fun e -> "Positive " ^
 492                                   (string_of_equality ~env e)) pos)));
 493                     print_newline ();
 494               in
 495               match contains_empty env new' with
 496               | false, _ ->
 497                   let active =
 498                     let al, tbl = active in
 499                     match sign with
 500                     | Negative -> (sign, current)::al, tbl
 501                     | Positive ->
 502                         al @ [(sign, current)], Indexing.index tbl current
 503                   in
 504                   let passive = add_to_passive passive new' in
 505                   let (_, ns), (_, ps), _ = passive in
 506                   Printf.printf "passive:\n%s\n"
 507                     (String.concat "\n"
 508                        ((List.map (fun e -> "Negative " ^
 509                                      (string_of_equality ~env e))
 510                            (EqualitySet.elements ns)) @
 511                           (List.map (fun e -> "Positive " ^
 512                                        (string_of_equality ~env e))
 513                              (EqualitySet.elements ps))));
 514                   print_newline ();
 515                   given_clause env passive active
 516               | true, proof ->
 517                   Success (proof, env)
 518           )
 519 ;;
 520
 521
 522 let rec given_clause_fullred env passive active =
 523   match passive_is_empty passive with
 524   | true -> Failure
 525   | false ->
 526       let (sign, current), passive = select env passive active in
 527       match forward_simplify env (sign, current) ~passive active with
 528       | None ->
 529           given_clause_fullred env passive active
 530       | Some (sign, current) ->
 531           if (sign = Negative) && (is_identity env current) then (
 532             Printf.printf "OK!!! %s %s" (string_of_sign sign)
 533               (string_of_equality ~env current);
 534             print_newline ();
 535             let proof, _, _, _ = current in
 536             Success (Some proof, env)
 537           ) else (
 538             print_endline "\n================================================";
 539             Printf.printf "selected: %s %s"
 540               (string_of_sign sign) (string_of_equality ~env current);
 541             print_newline ();
 542
 543             let new' = infer env sign current active in
 544
 545             let active =
 546               if is_identity env current then active
 547               else
 548                 let al, tbl = active in
 549                 match sign with
 550                 | Negative -> (sign, current)::al, tbl
 551                 | Positive -> al @ [(sign, current)], Indexing.index tbl current
 552             in
 553             let rec simplify new' active passive =
 554               let new' = forward_simplify_new env new' ~passive active in
 555               let active, passive, newa, retained =
 556                 backward_simplify env new' ~passive active
 557               in
 558               match newa, retained with
 559               | None, None -> active, passive, new'
 560               | Some (n, p), None
 561               | None, Some (n, p) ->
 562                   let nn, np = new' in
 563                   simplify (nn @ n, np @ p) active passive
 564               | Some (n, p), Some (rn, rp) ->
 565                   let nn, np = new' in
 566                   simplify (nn @ n @ rn, np @ p @ rp) active passive
 567             in
 568             let active, passive, new' = simplify new' active passive in
 569             let _ =
 570               Printf.printf "active:\n%s\n"
 571                 (String.concat "\n"
 572                    ((List.map
 573                        (fun (s, e) -> (string_of_sign s) ^ " " ^
 574                           (string_of_equality ~env e)) (fst active))));
 575               print_newline ();
 576             in
 577             let _ =
 578               match new' with
 579               | neg, pos ->
 580                   Printf.printf "new':\n%s\n"
 581                     (String.concat "\n"
 582                        ((List.map
 583                            (fun e -> "Negative " ^
 584                               (string_of_equality ~env e)) neg) @
 585                           (List.map
 586                              (fun e -> "Positive " ^
 587                                 (string_of_equality ~env e)) pos)));
 588                   print_newline ();
 589             in
 590             match contains_empty env new' with
 591             | false, _ ->
 592                 let passive = add_to_passive passive new' in
 593                 given_clause_fullred env passive active
 594             | true, proof ->
 595                 Success (proof, env)
 596           )
 597 ;;
 598
 599
 600 let get_from_user () =
 601   let dbd = Mysql.quick_connect
 602     ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
 603   let rec get () =
 604     match read_line () with
 605     | "" -> []
 606     | t -> t::(get ())
 607   in
 608   let term_string = String.concat "\n" (get ()) in
 609   let env, metasenv, term, ugraph =
 610     List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
 611   in
 612   term, metasenv, ugraph
 613 ;;
 614
 615
 616 let given_clause_ref = ref given_clause;;
 617
 618
 619 let main () =
 620   let module C = Cic in
 621   let module T = CicTypeChecker in
 622   let module PET = ProofEngineTypes in
 623   let module PP = CicPp in
 624   let term, metasenv, ugraph = get_from_user () in
 625   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
 626   let proof, goals =
 627     PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
 628   let goal = List.nth goals 0 in
 629   let _, metasenv, meta_proof, _ = proof in
 630   let _, context, goal = CicUtil.lookup_meta goal metasenv in
 631   let equalities, maxm = find_equalities context proof in
 632   maxmeta := maxm; (* TODO ugly!! *)
 633   let env = (metasenv, context, ugraph) in
 634   try
 635     let term_equality = equality_of_term meta_proof goal in
 636     let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
 637     let active = make_active () in
 638     let passive = make_passive [term_equality] equalities in
 639     Printf.printf "\ncurrent goal: %s\n"
 640       (string_of_equality ~env term_equality);
 641     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
 642     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
 643     Printf.printf "\nequalities:\n%s\n"
 644       (String.concat "\n"
 645          (List.map
 646             (string_of_equality ~env)
 647             equalities));
 648     print_endline "--------------------------------------------------";
 649     let start = Unix.gettimeofday () in
 650     print_endline "GO!";
 651     let res = !given_clause_ref env passive active in
 652     let finish = Unix.gettimeofday () in
 653     match res with
 654     | Failure ->
 655         Printf.printf "NO proof found! :-(\n\n"
 656     | Success (Some proof, env) ->
 657         Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
 658           (PP.pp proof (names_of_context context))
 659           (finish -. start);
 660     | Success (None, env) ->
 661         Printf.printf "Success, but no proof?!?\n\n"
 662   with exc ->
 663     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
 664 ;;
 665
 666
 667 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
 668
 669 let _ =
 670   let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
 671   and set_sel v = symbols_ratio := v; symbols_counter := v;
 672   and set_conf f = configuration_file := f
 673   and set_lpo () = Utils.compare_terms := lpo
 674   and set_kbo () = Utils.compare_terms := nonrec_kbo
 675   and set_fullred () = given_clause_ref := given_clause_fullred
 676   in
 677   Arg.parse [
 678     "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
 679
 680     "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
 681
 682     "-s", Arg.Int set_sel,
 683     "symbols-based selection ratio (relative to the weight ratio)";
 684
 685     "-c", Arg.String set_conf, "Configuration file (for the db connection)";
 686
 687     "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
 688
 689     "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
 690   ] (fun a -> ()) "Usage:"
 691 in
 692 Helm_registry.load_from !configuration_file;
 693 main ()