open Inference;;
open Utils;;
+
(* profiling statistics... *)
let infer_time = ref 0.;;
let forward_simpl_time = ref 0.;;
let maximal_retained_equality = ref None;;
(* equality-selection related globals *)
+let use_fullred = ref false;;
let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
let weight_age_counter = ref !weight_age_ratio;;
let symbols_ratio = ref 0;;
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
| [], hd::tl ->
- let passive_table = Indexing.remove_index passive_table hd in
+ let passive_table =
+ Indexing.remove_index passive_table hd
+(* if !use_fullred then Indexing.remove_index passive_table hd *)
+(* else passive_table *)
+ in
(Positive, hd),
(([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
| _, _ -> assert false
let _, current = EqualitySet.fold f pos_set initial in
(* Printf.printf "\nsymbols-based selection: %s\n\n" *)
(* (string_of_equality ~env current); *)
- let passive_table = Indexing.remove_index passive_table current in
+ let passive_table =
+ Indexing.remove_index passive_table current
+(* if !use_fullred then Indexing.remove_index passive_table current *)
+(* else passive_table *)
+ in
(Positive, current),
(([], neg_set),
(remove current pos_list, EqualitySet.remove current pos_set),
passive_table)
| _ ->
let current = EqualitySet.min_elt pos_set in
+ let passive_table =
+ Indexing.remove_index passive_table current
+(* if !use_fullred then Indexing.remove_index passive_table current *)
+(* else passive_table *)
+ in
let passive =
(neg_list, neg_set),
(remove current pos_list, EqualitySet.remove current pos_set),
- Indexing.remove_index passive_table current
+ passive_table
in
(Positive, current), passive
)
(neg_list, neg_set),
(remove current pos_list, EqualitySet.remove current pos_set),
Indexing.remove_index passive_table current
+(* if !use_fullred then Indexing.remove_index passive_table current *)
+(* else passive_table *)
in
(Positive, current), passive
else
let set_of equalities =
List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
in
- let table = Indexing.empty_table () in
+ let table =
+ List.fold_left (fun tbl e -> Indexing.index tbl e)
+ (Indexing.empty_table ()) pos
+(* if !use_fullred then *)
+(* List.fold_left (fun tbl e -> Indexing.index tbl e) *)
+(* (Indexing.empty_table ()) pos *)
+(* else *)
+(* Indexing.empty_table () *)
+ in
(neg, set_of neg),
(pos, set_of pos),
- List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+ table
;;
let ok set equality = not (EqualitySet.mem equality set) in
let neg = List.filter (ok neg_set) new_neg
and pos = List.filter (ok pos_set) new_pos in
+ let table =
+ List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+(* if !use_fullred then *)
+(* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
+(* else *)
+(* table *)
+ in
let add set equalities =
List.fold_left (fun s e -> EqualitySet.add e s) set equalities
in
(neg @ neg_list, add neg_set neg),
(pos_list @ pos, add pos_set pos),
- List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+ table
;;
let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
and in_age = int_of_float (howmany /. (ratio +. 1.)) in
Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age;
-(* let rec pickw w s = *)
-(* if w > 0 then *)
-(* try *)
-(* let e = EqualitySet.min_elt s in *)
-(* let w, s' = pickw (w-1) (EqualitySet.remove e s) in *)
-(* w, EqualitySet.add e s' *)
-(* with Not_found -> *)
-(* w, s *)
-(* else *)
-(* 0, EqualitySet.empty *)
-(* in *)
let symbols, card =
match active with
| (Negative, e)::_ ->
maximal_retained_equality := Some (EqualitySet.max_elt ps);
let tbl =
EqualitySet.fold
- (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) in
+ (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
+(* if !use_fullred then *)
+(* EqualitySet.fold *)
+(* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
+(* else *)
+(* tbl *)
+ in
(nl, ns), (pl, ps), tbl
;;
and pp = List.map (fun e -> (Positive, e)) pp in
pn @ pp, Some pt
in
- let all = active_list @ pl in
- let rec find_duplicate sign current = function
- | [] -> false
- | (s, eq)::tl when s = sign ->
- if meta_convertibility_eq current eq then true
- else find_duplicate sign current tl
- | _::tl -> find_duplicate sign current tl
- in
+ let all = if pl = [] then active_list else active_list @ pl in
+
+(* let rec find_duplicate sign current = function *)
+(* | [] -> false *)
+(* | (s, eq)::tl when s = sign -> *)
+(* if meta_convertibility_eq current eq then true *)
+(* else find_duplicate sign current tl *)
+(* | _::tl -> find_duplicate sign current tl *)
+(* in *)
let demodulate table current =
let newmeta, newcurrent =
Indexing.demodulation !maxmeta env table current in
in
match res with
| None -> None
- | Some (s, c) ->
- if find_duplicate s c all then
+ | Some (Negative, c) ->
+ let ok = not (
+ List.exists
+ (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
+ all)
+ in
+ if ok then res else None
+ | Some (Positive, c) ->
+ if Indexing.in_index active_table c then
None
else
- res
+ match passive_table with
+ | None -> res
+ | Some passive_table ->
+ if Indexing.in_index passive_table c then None else res
+
+(* | Some (s, c) -> if find_duplicate s c all then None else res *)
+
(* if s = Utils.Negative then *)
(* res *)
(* else *)
in
let new_pos = EqualitySet.elements new_pos_set in
- let subs =
- match passive_table with
- | None ->
- (fun e -> not (Indexing.subsumption env active_table e))
- | Some passive_table ->
- (fun e -> not ((Indexing.subsumption env active_table e) ||
- (Indexing.subsumption env passive_table e)))
- in
+(* let subs = *)
+(* match passive_table with *)
+(* | None -> *)
+(* (fun e -> not (Indexing.subsumption env active_table e)) *)
+(* | Some passive_table -> *)
+(* (fun e -> not ((Indexing.subsumption env active_table e) || *)
+(* (Indexing.subsumption env passive_table e))) *)
+(* in *)
let t1 = Unix.gettimeofday () in
let t2 = Unix.gettimeofday () in
fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
- new_neg, new_pos
+ let is_duplicate =
+ match passive_table with
+ | None -> (fun e -> not (Indexing.in_index active_table e))
+ | Some passive_table ->
+ (fun e -> not ((Indexing.in_index active_table e) ||
+ (Indexing.in_index passive_table e)))
+ in
+ new_neg, List.filter is_duplicate new_pos
+
+(* new_neg, new_pos *)
+
(* let res = *)
(* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
(* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
let get_selection_estimate () =
elapsed_time := (Unix.gettimeofday ()) -. !start_time;
- !processed_clauses * (int_of_float (!time_limit /. !elapsed_time))
+ int_of_float (
+ ceil ((float_of_int !processed_clauses) *.
+ (!time_limit /. !elapsed_time -. 1.)))
;;
Success (proof, env)
else
let t1 = Unix.gettimeofday () in
- let new' = forward_simplify_new env new' active in
+ let new' = forward_simplify_new env new' (* ~passive *) active in
let t2 = Unix.gettimeofday () in
let _ =
forward_simpl_time := !forward_simpl_time +. (t2 -. t1)
let start = Unix.gettimeofday () in
print_endline "GO!";
start_time := Unix.gettimeofday ();
- let res = !given_clause_ref env passive active in
+ let res =
+ (if !use_fullred then given_clause_fullred else given_clause)
+ env passive active
+ in
let finish = Unix.gettimeofday () in
match res with
| Failure ->
and set_conf f = configuration_file := f
and set_lpo () = Utils.compare_terms := lpo
and set_kbo () = Utils.compare_terms := nonrec_kbo
- and set_fullred () = given_clause_ref := given_clause_fullred
+ and set_fullred () = use_fullred := true
and set_time_limit v = time_limit := float_of_int v
in
Arg.parse [
projects / helm.git / blobdiff