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 = Indexing.demodulate !maxmeta env table current in
 268     maxmeta := newmeta;
 269     if is_identity env newcurrent then
 270       if sign = Negative then Some (sign, newcurrent) else None
 271     else
 272       Some (sign, newcurrent)
 273   in
 274   let res =
 275     let res = demodulate active_table current in
 276     match res with
 277     | None -> None
 278     | Some (sign, newcurrent) ->
 279         match passive_table with
 280         | None -> res
 281         | Some passive_table -> demodulate passive_table newcurrent
 282   in
 283   match res with
 284   | None -> None
 285   | Some (s, c) ->
 286       if find_duplicate s c all then
 287         None
 288       else
 289         let pred (sign, eq) =
 290           if sign <> s then false
 291           else subsumption env c eq
 292         in
 293         if List.exists pred all then None
 294         else res
 295 ;;
 296
 297
 298 let forward_simplify_new env (new_neg, new_pos) ?passive active =
 299   let active_list, active_table = active in
 300   let pl, passive_table =
 301     match passive with
 302     | None -> [], None
 303     | Some ((pn, _), (pp, _), pt) ->
 304         let pn = List.map (fun e -> (Negative, e)) pn
 305         and pp = List.map (fun e -> (Positive, e)) pp in
 306         pn @ pp, Some pt
 307   in
 308   let all = active_list @ pl in
 309   let demodulate table target =
 310     let newmeta, newtarget = Indexing.demodulate !maxmeta env table target in
 311     maxmeta := newmeta;
 312     newtarget
 313   in
 314   let new_neg, new_pos =
 315     let new_neg = List.map (demodulate active_table) new_neg
 316     and new_pos = List.map (demodulate active_table) new_pos in
 317     match passive_table with
 318     | None -> new_neg, new_pos
 319     | Some passive_table ->
 320         List.map (demodulate passive_table) new_neg,
 321         List.map (demodulate passive_table) new_pos
 322   in
 323   let new_pos_set =
 324     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos
 325   in
 326   let new_pos = EqualitySet.elements new_pos_set in
 327   let f sign' target (sign, eq) =
 328     if sign <> sign' then false
 329     else subsumption env target eq
 330   in
 331   (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
 332    List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
 333 ;;
 334
 335
 336 let backward_simplify_active env (new_neg, new_pos) active =
 337   let active_list, active_table = active in
 338   let new_pos, new_table =
 339     List.fold_left
 340       (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
 341       ([], Hashtbl.create (List.length new_pos)) new_pos
 342   in
 343   let active_list, newa =
 344     List.fold_right
 345       (fun (s, equality) (res, newn) ->
 346          match forward_simplify env (s, equality) (new_pos, new_table) with
 347          | None -> res, newn
 348          | Some (s, e) ->
 349              if equality = e then
 350                (s, e)::res, newn
 351              else
 352                res, (s, e)::newn)
 353       active_list ([], [])
 354   in
 355   let find eq1 where =
 356     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 357   in
 358   let active, newa =
 359     List.fold_right
 360       (fun (s, eq) (res, tbl) ->
 361          if (is_identity env eq) || (find eq res) then
 362            res, tbl
 363          else
 364            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
 365       active_list ([], Hashtbl.create (List.length active_list)),
 366     List.fold_right
 367       (fun (s, eq) (n, p) ->
 368          if (s <> Negative) && (is_identity env eq) then
 369            (n, p)
 370          else
 371            if s = Negative then eq::n, p
 372            else n, eq::p)
 373       newa ([], [])
 374   in
 375   match newa with
 376   | [], [] -> active, None
 377   | _ -> active, Some newa
 378 ;;
 379
 380
 381 let backward_simplify_passive env (new_neg, new_pos) passive =
 382   let new_pos, new_table =
 383     List.fold_left
 384       (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
 385       ([], Hashtbl.create (List.length new_pos)) new_pos
 386   in
 387   let (nl, ns), (pl, ps), passive_table = passive in
 388   let f sign equality (resl, ress, newn) =
 389     match forward_simplify env (sign, equality) (new_pos, new_table) with
 390     | None -> resl, EqualitySet.remove equality ress, newn
 391     | Some (s, e) ->
 392         if equality = e then
 393           equality::resl, ress, newn
 394         else
 395           let ress = EqualitySet.remove equality ress in
 396           resl, ress, e::newn
 397   in
 398   let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
 399   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
 400   let passive_table =
 401     List.fold_left
 402       (fun tbl e -> Indexing.index tbl e) (Hashtbl.create (List.length pl)) pl
 403   in
 404   match newn, newp with
 405   | [], [] -> ((nl, ns), (pl, ps), passive_table), None
 406   | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
 407 ;;
 408
 409
 410 let backward_simplify env new' ?passive active =
 411   let active, newa = backward_simplify_active env new' active in
 412   match passive with
 413   | None ->
 414       active, (make_passive [] []), newa, None
 415   | Some passive ->
 416       let passive, newp =
 417         backward_simplify_passive env new' passive in
 418       active, passive, newa, newp
 419 ;;
 420
 421
 422 let rec given_clause env passive active =
 423   match passive_is_empty passive with
 424   | true -> Failure
 425   | false ->
 426       let (sign, current), passive = select env passive active in
 427       match forward_simplify env (sign, current) ~passive active with
 428       | None ->
 429           given_clause env passive active
 430       | Some (sign, current) ->
 431           if (sign = Negative) && (is_identity env current) then (
 432             Printf.printf "OK!!! %s %s" (string_of_sign sign)
 433               (string_of_equality ~env current);
 434             print_newline ();
 435             let proof, _, _, _ = current in
 436             Success (Some proof, env)
 437           ) else (
 438             print_endline "\n================================================";
 439             Printf.printf "selected: %s %s"
 440               (string_of_sign sign) (string_of_equality ~env current);
 441             print_newline ();
 442
 443             let new' = infer env sign current active in
 444             let res, proof = contains_empty env new' in
 445             if res then
 446               Success (proof, env)
 447             else
 448               let new' = forward_simplify_new env new' active in
 449               let active =
 450                 match sign with
 451                 | Negative -> active
 452                 | Positive ->
 453                     let active, _, newa, _ =
 454                       backward_simplify env ([], [current]) active
 455                     in
 456                     match newa with
 457                     | None -> active
 458                     | Some (n, p) ->
 459                         let al, tbl = active in
 460                         let nn = List.map (fun e -> Negative, e) n in
 461                         let pp, tbl =
 462                           List.fold_right
 463                             (fun e (l, t) ->
 464                                (Positive, e)::l,
 465                                Indexing.index tbl e)
 466                             p ([], tbl)
 467                         in
 468                         nn @ al @ pp, tbl
 469               in
 470               let _ =
 471                 Printf.printf "active:\n%s\n"
 472                   (String.concat "\n"
 473                      ((List.map
 474                          (fun (s, e) -> (string_of_sign s) ^ " " ^
 475                             (string_of_equality ~env e)) (fst active))));
 476                 print_newline ();
 477               in
 478               let _ =
 479                 match new' with
 480                 | neg, pos ->
 481                     Printf.printf "new':\n%s\n"
 482                       (String.concat "\n"
 483                          ((List.map
 484                              (fun e -> "Negative " ^
 485                                 (string_of_equality ~env e)) neg) @
 486                             (List.map
 487                                (fun e -> "Positive " ^
 488                                   (string_of_equality ~env e)) pos)));
 489                     print_newline ();
 490               in
 491               match contains_empty env new' with
 492               | false, _ ->
 493                   let active =
 494                     let al, tbl = active in
 495                     match sign with
 496                     | Negative -> (sign, current)::al, tbl
 497                     | Positive ->
 498                         al @ [(sign, current)], Indexing.index tbl current
 499                   in
 500                   let passive = add_to_passive passive new' in
 501                   let (_, ns), (_, ps), _ = passive in
 502                   Printf.printf "passive:\n%s\n"
 503                     (String.concat "\n"
 504                        ((List.map (fun e -> "Negative " ^
 505                                      (string_of_equality ~env e))
 506                            (EqualitySet.elements ns)) @
 507                           (List.map (fun e -> "Positive " ^
 508                                        (string_of_equality ~env e))
 509                              (EqualitySet.elements ps))));
 510                   print_newline ();
 511                   given_clause env passive active
 512               | true, proof ->
 513                   Success (proof, env)
 514           )
 515 ;;
 516
 517
 518 let rec given_clause_fullred env passive active =
 519   match passive_is_empty passive with
 520   | true -> Failure
 521   | false ->
 522       let (sign, current), passive = select env passive active in
 523       match forward_simplify env (sign, current) ~passive active with
 524       | None ->
 525           given_clause_fullred env passive active
 526       | Some (sign, current) ->
 527           if (sign = Negative) && (is_identity env current) then (
 528             Printf.printf "OK!!! %s %s" (string_of_sign sign)
 529               (string_of_equality ~env current);
 530             print_newline ();
 531             let proof, _, _, _ = current in
 532             Success (Some proof, env)
 533           ) else (
 534             print_endline "\n================================================";
 535             Printf.printf "selected: %s %s"
 536               (string_of_sign sign) (string_of_equality ~env current);
 537             print_newline ();
 538
 539             let new' = infer env sign current active in
 540
 541             let active =
 542               if is_identity env current then active
 543               else
 544                 let al, tbl = active in
 545                 match sign with
 546                 | Negative -> (sign, current)::al, tbl
 547                 | Positive -> al @ [(sign, current)], Indexing.index tbl current
 548             in
 549             let rec simplify new' active passive =
 550               let new' = forward_simplify_new env new' ~passive active in
 551               let active, passive, newa, retained =
 552                 backward_simplify env new' ~passive active
 553               in
 554               match newa, retained with
 555               | None, None -> active, passive, new'
 556               | Some (n, p), None
 557               | None, Some (n, p) ->
 558                   let nn, np = new' in
 559                   simplify (nn @ n, np @ p) active passive
 560               | Some (n, p), Some (rn, rp) ->
 561                   let nn, np = new' in
 562                   simplify (nn @ n @ rn, np @ p @ rp) active passive
 563             in
 564             let active, passive, new' = simplify new' active passive in
 565             let _ =
 566               Printf.printf "active:\n%s\n"
 567                 (String.concat "\n"
 568                    ((List.map
 569                        (fun (s, e) -> (string_of_sign s) ^ " " ^
 570                           (string_of_equality ~env e)) (fst active))));
 571               print_newline ();
 572             in
 573             let _ =
 574               match new' with
 575               | neg, pos ->
 576                   Printf.printf "new':\n%s\n"
 577                     (String.concat "\n"
 578                        ((List.map
 579                            (fun e -> "Negative " ^
 580                               (string_of_equality ~env e)) neg) @
 581                           (List.map
 582                              (fun e -> "Positive " ^
 583                                 (string_of_equality ~env e)) pos)));
 584                   print_newline ();
 585             in
 586             match contains_empty env new' with
 587             | false, _ ->
 588                 let passive = add_to_passive passive new' in
 589                 given_clause_fullred env passive active
 590             | true, proof ->
 591                 Success (proof, env)
 592           )
 593 ;;
 594
 595
 596 let get_from_user () =
 597   let dbd = Mysql.quick_connect
 598     ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
 599   let rec get () =
 600     match read_line () with
 601     | "" -> []
 602     | t -> t::(get ())
 603   in
 604   let term_string = String.concat "\n" (get ()) in
 605   let env, metasenv, term, ugraph =
 606     List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
 607   in
 608   term, metasenv, ugraph
 609 ;;
 610
 611
 612 let given_clause_ref = ref given_clause;;
 613
 614
 615 let main () =
 616   let module C = Cic in
 617   let module T = CicTypeChecker in
 618   let module PET = ProofEngineTypes in
 619   let module PP = CicPp in
 620   let term, metasenv, ugraph = get_from_user () in
 621   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
 622   let proof, goals =
 623     PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
 624   let goal = List.nth goals 0 in
 625   let _, metasenv, meta_proof, _ = proof in
 626   let _, context, goal = CicUtil.lookup_meta goal metasenv in
 627   let equalities, maxm = find_equalities context proof in
 628   maxmeta := maxm; (* TODO ugly!! *)
 629   let env = (metasenv, context, ugraph) in
 630   try
 631     let term_equality = equality_of_term meta_proof goal in
 632     let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
 633     let active = make_active () in
 634     let passive = make_passive [term_equality] equalities in
 635     Printf.printf "\ncurrent goal: %s\n"
 636       (string_of_equality ~env term_equality);
 637     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
 638     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
 639     Printf.printf "\nequalities:\n%s\n"
 640       (String.concat "\n"
 641          (List.map
 642             (string_of_equality ~env)
 643             equalities));
 644     print_endline "--------------------------------------------------";
 645     let start = Unix.gettimeofday () in
 646     print_endline "GO!";
 647     let res = !given_clause_ref env passive active in
 648     let finish = Unix.gettimeofday () in
 649     match res with
 650     | Failure ->
 651         Printf.printf "NO proof found! :-(\n\n"
 652     | Success (Some proof, env) ->
 653         Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof)
 654           (finish -. start);
 655     | Success (None, env) ->
 656         Printf.printf "Success, but no proof?!?\n\n"
 657   with exc ->
 658     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
 659 ;;
 660
 661
 662 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
 663
 664 let _ =
 665   let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
 666   and set_sel v = symbols_ratio := v; symbols_counter := v;
 667   and set_conf f = configuration_file := f
 668   and set_lpo () = Utils.compare_terms := lpo
 669   and set_kbo () = Utils.compare_terms := nonrec_kbo
 670   and set_fullred () = given_clause_ref := given_clause_fullred
 671   in
 672   Arg.parse [
 673     "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
 674
 675     "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
 676
 677     "-s", Arg.Int set_sel,
 678     "symbols-based selection ratio (relative to the weight ratio)";
 679
 680     "-c", Arg.String set_conf, "Configuration file (for the db connection)";
 681
 682     "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
 683
 684     "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
 685   ] (fun a -> ()) "Usage:"
 686 in
 687 Helm_registry.load_from !configuration_file;
 688 main ()