* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Inference;;
open Utils;;
(* non-recursive Knuth-Bendix term ordering by default *)
Utils.compare_terms := Utils.nonrec_kbo;;
+(* Utils.compare_terms := Utils.ao;; *)
(* statistics... *)
let derived_clauses = ref 0;;
(* Negatives aren't indexed, no need to remove them... *)
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
- | [], hd::tl ->
+ | [], (hd:EqualitySet.elt)::tl ->
let passive_table =
Indexing.remove_index passive_table hd
in
List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
in
let table =
- List.fold_left (fun tbl e -> Indexing.index tbl e)
- (Indexing.empty_table ()) pos
+ List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos
in
(neg, set_of neg),
(pos, set_of pos),
let make_active () =
- [], Indexing.empty_table ()
+ [], Indexing.empty
;;
maximal_retained_equality := Some (EqualitySet.max_elt ps);
let tbl =
EqualitySet.fold
- (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
+ (fun e tbl -> Indexing.index tbl e) ps Indexing.empty
in
(nl, ns), (pl, ps), tbl
;;
let neg, pos = infer_positive table tl in
neg, res @ pos
in
- let curr_table = Indexing.index (Indexing.empty_table ()) current in
+ let curr_table = Indexing.index Indexing.empty current in
let neg, pos = infer_positive curr_table active_list in
neg, res @ pos
in
)
else
(s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
- active_list ([], Indexing.empty_table ()),
+ active_list ([], Indexing.empty),
List.fold_right
(fun (s, eq) (n, p) ->
if (s <> Negative) && (is_identity env eq) then (
and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
let passive_table =
List.fold_left
- (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
+ (fun tbl e -> Indexing.index tbl e) Indexing.empty pl
in
match newn, newp with
| [], [] -> ((nl, ns), (pl, ps), passive_table), None
(fun (l, t, w) e ->
let ew, _, _, _, _ = e in
(Positive, e)::l, Indexing.index t e, min ew w)
- ([], Indexing.empty_table (), 1000000) (snd new')
+ ([], Indexing.empty, 1000000) (snd new')
in
let active, newa =
backward_simplify_active env new_pos new_table min_weight active in
let tbl =
List.fold_left
(fun t (_, e) -> Indexing.index t e)
- (Indexing.empty_table ()) active
+ Indexing.empty active
in
let res = forward_simplify env e (active, tbl) in
match others with
let tbl =
List.fold_left
(fun t (_, e) -> Indexing.index t e)
- (Indexing.empty_table ()) active
+ Indexing.empty active
in
let res = forward_simplify env e (active, tbl) in
match others with
let tbl =
List.fold_left
(fun t (_, e) -> Indexing.index t e)
- (Indexing.empty_table ()) active
+ Indexing.empty active
in
let res = forward_simplify env (Positive, e) (active, tbl) in
match others with
let tbl =
List.fold_left
(fun t (_, e) -> Indexing.index t e)
- (Indexing.empty_table ()) active
+ Indexing.empty active
in
let res = forward_simplify env e (active, tbl) in
match others with
saturate_equations env goal (fun e -> true) passive active
in
let finish = Unix.gettimeofday () in
+
+ let initial =
+ List.fold_left (fun s e -> EqualitySet.add e s)
+ EqualitySet.empty equalities
+ in
+ let addfun s e =
+ if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
+ in
+
+ let passive =
+ match rp with
+ | (n, _), (p, _), _ ->
+ EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
+ in
+ let active =
+ let l = List.map snd (fst ra) in
+ EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
+ in
Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
+(* (String.concat "\n" (List.map (string_of_equality ~env) active)) *)
(String.concat "\n"
- (List.map (fun (s, e) -> (string_of_equality ~env e)) (fst ra)))
+ (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active))
+(* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
(String.concat "\n"
- (List.map (string_of_equality ~env)
- (match rp with (n, _), (p, _), _ -> p)));
+ (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive));
print_newline ();
with e ->
debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))