(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
let print s = prerr_endline (Lazy.force s) ;;
-(* let debug = print *)
-let debug s = ();;
+let noprint s = ();;
+let debug = noprint;;
let monster = 100;;
bag ->
g_passives:t Terms.unit_clause list ->
passives:t Terms.unit_clause list -> szsontology
+ val demod :
+ state -> input* input -> szsontology
val fast_eq_check :
state -> input* input -> szsontology
val nparamod :
else WeightPassiveSet.min_elt passives_w
;;
+ let mk_unit_clause bag maxvar (t,ty) =
+ let c, maxvar = Utils.mk_unit_clause maxvar (B.embed ty) (B.embed t) in
+ let bag, c = Terms.add_to_bag c bag in
+ (bag, maxvar), c
+ ;;
+
let mk_clause bag maxvar (t,ty) =
let (proof,ty) = B.saturate t ty in
let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
;;
let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
+
let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
+
let initialize_goal (bag,maxvar,actives,passives,_,_) t =
- let (bag,maxvar), g = mk_goal (bag,maxvar) t in
+ let (bag,maxvar), g = mk_unit_clause bag maxvar t in
let g_passives = g_passive_empty_set in
(* if the goal is not an equation we returns an empty
passive set *)
(List.map Pp.pp_unit_clause actives_l)))
^
("Passives:" ^(String.concat ";\n"
- (List.map (fun _,cl -> Pp.pp_unit_clause cl)
+ (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
(IDX.ClauseSet.elements wset))))
;;
* P' = P + new' *)
debug (lazy "Forward infer step...");
debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
- debug (lazy (pp_clauses actives passives));
+ noprint (lazy (pp_clauses actives passives));
match Sup.keep_simplified current actives bag maxvar
with
| _,None -> s
(Unix.gettimeofday())));
let actives_l, active_t = actives in
let passive_t,wset,_ = passives in
- let _ = debug
+ let _ = noprint
(lazy
("Actives :" ^ (String.concat ";\n"
(List.map Pp.pp_unit_clause actives_l)))) in
let wset = IDX.elems passive_t in
- let _ = debug
+ let _ = noprint
(lazy
("Passives:" ^(String.concat ";\n"
- (List.map (fun _,cl -> Pp.pp_unit_clause cl)
+ (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
(IDX.ClauseSet.elements wset))))) in
let g_passives =
WeightPassiveSet.fold
Sup.simplify_goal
~no_demod maxvar (snd actives) bag g_actives current
with
- | None -> status
+ | None -> debug (lazy "None"); status
| Some (bag,g_current) ->
let _ =
debug (lazy("Infer on goal : "
| Stop o -> o
;;
+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, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
+ if g1 = g then GaveUp else compute_result bag i []
+(*
+ if Terms.is_eq_clause g then
+
+ else GaveUp *)
+
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"
else
try
goal_narrowing 0 2 None s