;
(fun () -> worker `KBO ~useage:true ~printmsg:false goal hypotheses)
;
- (fun () -> worker `LPO ~useage:true ~printmsg:true goal hypotheses)
+ (fun () -> worker `LPO ~useage:true ~printmsg:false goal hypotheses)
;
(fun () -> worker `NRKBO ~useage:false ~printmsg:false goal hypotheses)
];
match ty with
| Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
let o = Order.compare_terms l r in
- (vars,(Terms.Equation (l, r, ty, o),false)::literals)
- | _ -> (vars,(Terms.Predicate ty,false)::literals)
+ (vars,(Terms.Equation (l, r, ty, o),true)::literals)
+ | _ -> (vars,(Terms.Predicate ty,true)::literals)
in
let varlist = Terms.vars_of_term proofterm in
let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in
(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
-let debug s = prerr_endline s ;;
+let debug s = prerr_endline (Lazy.force s) ;;
let debug _ = ();;
let monster = 100;;
let backward_infer_step bag maxvar actives passives
g_actives g_passives g_current iterno =
(* superposition left, simplifications on goals *)
- debug "infer_left step...";
+ debug (lazy "infer_left step...");
let bag, maxvar, new_goals =
Sup.infer_left bag maxvar g_current actives
in
- debug "Performed infer_left step";
+ debug (lazy "Performed infer_left step");
let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
bag, maxvar, actives, passives, g_current::g_actives,
(add_passive_goals g_passives new_goals)
* new = supright e'' A'' *
* new'= demod A'' new *
* P' = P + new' *)
- debug "Forward infer step...";
+ debug (lazy "Forward infer step...");
debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
let bag, maxvar, actives, new_clauses =
Sup.infer_right bag maxvar current actives
in
- debug "Demodulating goals with actives...";
+ debug (lazy "Demodulating goals with actives...");
(* keep goals demodulated w.r.t. actives and check if solved *)
let bag, g_actives =
List.fold_left
if weight > monster then bag,None
else bag, Some (current,actives)
else if Sup.orphan_murder bag (fst actives) current then
- let _ = debug "Orphan murdered" in
+ let _ = debug (lazy "Orphan murdered") in
let bag = Terms.replace_in_bag (current,true,iterno) bag in
bag, None
else Sup.keep_simplified current actives bag maxvar
(*prerr_endline "Active table :";
(List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
(fst actives)); *)
-
let bag,maxvar,actives,passives,g_actives,g_passives =
aux_select bag passives g_passives
in
| Terms.Incomparable -> "=?="
| Terms.Invertible -> "=<->="
-(*let pp_literal ~formatter:f l =
- match l with
+let pp_literal ~formatter:f l =
+ match fst l with
| Terms.Predicate t ->
Format.fprintf f "@[<hv>{";
pp_foterm f t;
- Format.fprintf f "@;[%s] by "
- (String.concat ", " (List.map string_of_int vars));
- (match proof with
- | Terms.Exact t -> pp_foterm f t
- | Terms.Step (rule, id1, id2, _, p, _) ->
- Format.fprintf f "%s %d with %d at %s"
- (string_of_rule rule) id1 id2 (String.concat
- "," (List.map string_of_int p)));
- Format.fprintf f "@]"
+ Format.fprintf f "}@;"
| Terms.Equation (lhs, rhs, ty, comp) ->
Format.fprintf f "@[<hv>{";
pp_foterm f ty;
pp_foterm f lhs;
Format.fprintf f "@;%s@;" (string_of_comparison comp);
pp_foterm f rhs;
- Format.fprintf f "@]@;[%s] by "
- (String.concat ", " (List.map string_of_int vars));
- (match proof with
- | Terms.Exact t -> pp_foterm f t
- | Terms.Step (rule, id1, id2, _, p, _) ->
- Format.fprintf f "%s %d with %d at %s"
- (string_of_rule rule) id1 id2 (String.concat
- "," (List.map string_of_int p)));
- Format.fprintf f "@]"
-*)
+ Format.fprintf f "@]@;"
+;;
let pp_unit_clause ~formatter:f c =
let (id, l, vars, proof) = c in
Format.fprintf f "%s %d with %d at %s"
(string_of_rule rule) id1 id2 (String.concat
"," (List.map string_of_int p)));
- Format.fprintf f "@]"
+ Format.fprintf f "@]"
;;
let pp_clause ~formatter:f c =
- assert false
+ let (id, nlit, plit, vars, proof) = c in
+ Format.fprintf f "Id : %3d, " id ;
+ let pr_literals l =
+ if l <> [] then begin
+ pp_literal f (List.hd l);
+ List.iter (fun lit -> Format.fprintf f "\\/"; pp_literal f lit) (List.tl l);
+ end
+ in
+ pr_literals nlit;
+ Format.fprintf f " -> ";
+ pr_literals plit;
+ Format.fprintf f "[%s] by " (String.concat ", " (List.map string_of_int vars));
+ match proof with
+ | Terms.Exact t -> pp_foterm f t
+ | Terms.Step (rule, id1, id2, _, p, _) ->
+ Format.fprintf f "%s %d with %d at %s"
+ (string_of_rule rule) id1 id2 (String.concat
+ "," (List.map string_of_int p))
;;
let pp_bag ~formatter:f (_,bag) =
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
;;
projects / helm.git / commitdiff