(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
let print s = prerr_endline (Lazy.force s) ;;
-let noprint s = ();;
-let debug = print;;
+let noprint _s = ();;
+let debug = noprint;;
let monster = 100;;
module Paramod (B : Orderings.Blob) = struct
module Pp = Pp.Pp (B)
- module FU = FoUnif.Founif(B)
+ (*module FU = FoUnif.Founif(B)*)
module IDX = Index.Index(B)
module Sup = Superposition.Superposition(B)
module Utils = FoUtils.Utils(B)
* new = supright e'' A'' *
* new'= demod A'' new *
* P' = P + new' *)
- debug (lazy "Forward infer step...");
+ debug (lazy ("Forward infer step for "^ (Pp.pp_unit_clause current)));
debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
noprint (lazy (pp_clauses actives passives));
+ let _ = noprint
+ (lazy
+ ("Actives before simplification:" ^ (String.concat ";\n"
+ (List.map Pp.pp_unit_clause (fst actives))))) in
match Sup.keep_simplified current actives bag maxvar
with
- | _,None -> s
+ | _,None -> debug(lazy("None")); s
| bag,Some (current,actives) ->
debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current)));
+ let _ = noprint
+ (lazy
+ ("Actives after simplification:" ^ (String.concat ";\n"
+ (List.map Pp.pp_unit_clause (fst actives))))) in
let bag, maxvar, actives, new_clauses =
Sup.infer_right bag maxvar current actives
in
debug (lazy("Last chance " ^ string_of_float
(Unix.gettimeofday())));
let actives_l, active_t = actives in
- let passive_t,wset,_ = passives in
+ let passive_t,_wset,_ = passives in
let _ = noprint
(lazy
("Actives :" ^ (String.concat ";\n"
let newstatus =
List.fold_left
(fun acc g ->
- let bag,maxvar,actives,passives,g_actives,g_passives = acc in
- let g_passives =
+ let _bag,_maxvar,_actives,_passives,_g_actives,g_passives = acc in
+ let _g_passives =
remove_passive_goal g_passives g in
let current = snd g in
let _ =
- debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current))
+ debug (lazy("Selected goal gn: " ^ Pp.pp_unit_clause current))
in
(* we work both on the original goal and the demodulated one*)
let acc = check_and_infer ~no_demod:false iterno acc current
let l =
let rec traverse ongoal (accg,acce) i =
match Terms.get_from_bag i bag with
- | (id,_,_,Terms.Exact _),_,_ ->
+ | (_id,_,_,Terms.Exact _),_,_ ->
if ongoal then [i],acce else
if (List.mem i acce) then accg,acce else accg,acce@[i]
| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ ->
;;
let demod s goal =
- let bag,maxvar,actives,passives,g_actives,g_passives = s in
- let (bag,maxvar), g = mk_goal (bag,maxvar) goal in
+ let bag,maxvar,actives,_passives,_g_actives,_g_passives = s in
+ let (bag,_maxvar), g = mk_goal (bag,maxvar) goal in
let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
if g1 = g then GaveUp else compute_result bag i []
(*
let fast_eq_check s goal =
let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
- if is_passive_g_set_empty g_passives then Error "not an equation"
+ if is_passive_g_set_empty g_passives then (Error "not an equation" : szsontology)
else
try
goal_narrowing 0 2 None s
let nparamod ~useage ~max_steps ?timeout s goal =
let bag,maxvar,actives,passives,g_actives,g_passives
= initialize_goal s goal in
- if is_passive_g_set_empty g_passives then Error "not an equation"
+ if is_passive_g_set_empty g_passives then (Error "not an equation" : szsontology)
else
try given_clause ~useage ~noinfer:false
bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives