exception Success of B.t Terms.bag * int * B.t Terms.clause
- let debug s = prerr_endline s;;
+ let debug s = prerr_endline (Lazy.force s);;
let debug _ = ();;
let enable = true;;
let (id,_,_,_,_) = cl in
let actives = List.map (fun (i,_,_,_,_) -> i) actives in
let (res,_) = orphan_murder bag actives id in
- if res then debug "Orphan murdered"; res
+ if res then debug (lazy "Orphan murdered"); res
;;
let prof_orphan_murder = HExtlib.profile ~enable "orphan_murder";;
let orphan_murder bag actives x =
(* this is OK for both the sup_left and sup_right inference steps *)
let superposition table varlist subterm pos context =
let cands = IDX.DT.retrieve_unifiables table subterm in
+ debug (lazy (string_of_int (IDX.ClauseSet.cardinal cands) ^ " candidates found"));
HExtlib.filter_map
(fun (dir, _, _, (id,nlit,plit,vl,_ (*as uc*))) ->
match nlit,plit with
in
bag, (alist, List.fold_left IDX.index_clause IDX.DT.empty alist)
in*)
- debug "Simplified active clauses with fact";
+ debug (lazy "Simplified active clauses with fact");
(* We superpose active clauses with current *)
let bag, maxvar, new_clauses =
List.fold_left
bag, maxvar, newc @ acc)
(bag, maxvar, []) alist
in
- debug "First superpositions";
+ debug (lazy "First superpositions");
(* We add current to active clauses so that it can be *
* superposed with itself *)
let alist, atable =
current :: alist, IDX.index_clause atable current
in
- debug "Indexed";
+ debug (lazy "Indexed");
let fresh_current, maxvar = Utils.fresh_clause maxvar current in
(* We need to put fresh_current into the bag so that all *
* variables clauses refer to are known. *)
let bag, maxvar, additional_new_clauses =
superposition_with_table bag maxvar fresh_current atable
in
- debug "Another superposition";
+ debug (lazy "Another superposition");
let new_clauses = new_clauses @ additional_new_clauses in
debug (lazy (Printf.sprintf "Demodulating %d clauses"
(List.length new_clauses)));
let bag, new_clauses =
HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses
in
- debug "Demodulated new clauses";
+ debug (lazy "Demodulated new clauses");
bag, maxvar, (alist, atable), new_clauses
;;
let bag, maxvar, new_goals =
superposition_with_table bag maxvar goal atable
in
- debug "Superposed goal with active clauses";
+ debug (lazy "Superposed goal with active clauses");
(* We simplify the new goals with active clauses *)
let bag, new_goals =
List.fold_left
| Some (bag,g) -> bag,g::acc)
(bag, []) new_goals
in
- debug "Simplified new goals with active clauses";
+ debug (lazy "Simplified new goals with active clauses");
bag, maxvar, List.rev new_goals
;;