(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
-(* let debug s = prerr_endline s ;;*)
+let debug s = prerr_endline s ;;
let debug _ = ();;
module Paramod (B : Terms.Blob) = struct
let bag, g_actives =
List.fold_left
(fun (bag,acc) c ->
- match Sup.simplify_goal maxvar (snd actives) bag acc c with
+ match
+ Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
+ with
| None -> bag, acc
| Some (bag,c) -> bag,c::acc)
(bag,[]) g_actives
add_passive_clauses g_passives new_goals
;;
- let rec given_clause
+ let rec given_clause ~noinfer
bag maxvar iterno max_steps timeout
actives passives g_actives g_passives
=
if iterno = max_steps then
raise (Failure ("No iterations left !",bag,maxvar,iterno));
(* timeout check: gettimeofday called only if timeout set *)
- (match timeout with
- | None -> ()
- | Some timeout ->
- if Unix.gettimeofday () > timeout then
- raise (Failure ("Timeout !",bag,maxvar,iterno)));
+ if timeout <> None &&
+ (match timeout with
+ | None -> assert false
+ | Some timeout -> Unix.gettimeofday () > timeout) then
+ begin
+ prerr_endline("Last chance: "^string_of_float (Unix.gettimeofday()));
+ given_clause ~noinfer:true bag maxvar iterno max_steps None
+ actives passives g_actives g_passives
+ (*raise (Failure ("Timeout !",bag,maxvar,iterno))*)
+ end
+ else
let use_age = iterno mod 10 = 0 in
let rec aux_select bag passives g_passives =
+ if noinfer &&
+ is_passive_set_empty passives &&
+ is_passive_set_empty g_passives then
+ begin
+ prerr_endline
+ ("Last chance: all is indexed " ^ string_of_float
+ (Unix.gettimeofday()));
+ let maxgoals = 100 in
+ List.fold_left
+ (fun (acc,i) x ->
+ if i < maxgoals then
+ ignore(Sup.simplify_goal ~no_demod:true
+ maxvar (snd actives) bag acc x)
+ else
+ ();
+ x::acc,i+1)
+ ([],0) g_actives;
+ raise (Failure (("Last chance: failed over " ^
+ string_of_int maxgoals^ " goal " ^
+ string_of_float (Unix.gettimeofday())),bag,maxvar,0));
+ end;
let backward,current,passives,g_passives =
select ~use_age:false passives g_passives
in
if backward then
- match Sup.simplify_goal maxvar (snd actives) bag g_actives current with
+ match
+ if noinfer then Some (bag,current)
+ else
+ Sup.simplify_goal
+ ~no_demod:false maxvar (snd actives) bag g_actives current
+ with
| None -> aux_select bag passives g_passives
| Some (bag,g_current) ->
- backward_infer_step bag maxvar actives passives
- g_actives g_passives g_current
+ if noinfer then
+ let g_actives = g_current :: g_actives in
+ bag,maxvar,actives,passives,g_actives,g_passives
+ else
+ backward_infer_step bag maxvar actives passives
+ g_actives g_passives g_current
else
(* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *)
- match Sup.keep_simplified current actives bag maxvar with
+ match
+ if noinfer then bag, Some (current,actives)
+ else Sup.keep_simplified current actives bag maxvar with
(* match Sup.one_pass_simplification current actives bag maxvar with*)
| bag,None -> aux_select bag passives g_passives
| bag,Some (current,actives) ->
- forward_infer_step bag maxvar actives passives
- g_actives g_passives current
+ if noinfer then
+ let actives =
+ current::fst actives,
+ IDX.index_unit_clause (snd actives) current
+ in
+ bag,maxvar,actives,passives,g_actives,g_passives
+ else
+ forward_infer_step bag maxvar actives passives
+ g_actives g_passives current
in
(* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
debug
(Printf.sprintf "Number of passives : %d"
(passive_set_cardinal passives));
- given_clause
+ given_clause ~noinfer
bag maxvar iterno max_steps timeout
actives passives g_actives g_passives
;;
let g_actives = [] in
let actives = [], IDX.DT.empty in
try
- given_clause
+ given_clause ~noinfer:false
bag maxvar 0 max_steps timeout actives passives g_actives g_passives
with
| Sup.Success (bag, _, (i,_,_,_)) ->
| (false,acc) ->
let (res,acc) = orphan_murder bag acc i2 in
if res then res,acc else res,i::acc
-;;
+ ;;
let orphan_murder bag cl =
let (id,_,_,_) = cl in
let (res,_) = orphan_murder bag [] id in
if res then debug "Orphan murdered"; res
-;;
+ ;;
(* demodulate and check for subsumption *)
let simplify table maxvar bag clause =
| bag, None -> let (id,_,_,_) = clause in
Terms.M.add id (clause,true) bag, None
| bag, Some clause -> bag, Some clause
-;;
+ ;;
let one_pass_simplification new_clause (alist,atable) bag maxvar =
match simplify atable maxvar bag new_clause with
;;
(* this is like simplify but raises Success *)
- let simplify_goal maxvar table bag g_actives clause =
- let bag, clause = demodulate bag clause table in
+ let simplify_goal ~no_demod maxvar table bag g_actives clause =
+ let bag, clause =
+ if no_demod then bag, clause else demodulate bag clause table
+ in
+ if List.exists (are_alpha_eq clause) g_actives then None else
if (is_identity_clause ~unify:true clause)
then raise (Success (bag, maxvar, clause))
-
else
let (id,lit,vl,_) = clause in
let l,r,ty =
in
match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x)
table (Some(bag,maxvar,clause,Subst.id_subst)) with
- | None ->
- if List.exists (are_alpha_eq clause) g_actives then None
- else Some (bag, clause)
+ | None -> Some (bag,clause)
| Some (bag,maxvar,cl,subst) ->
prerr_endline "Goal subsumed";
raise (Success (bag,maxvar,cl))
- (*
+(*
else match is_subsumed ~unify:true bag maxvar clause table with
- | None ->
- if List.exists (are_alpha_eq clause) g_actives then None
- else Some (bag, clause)
+ | None -> Some (bag, clause)
| Some ((bag,maxvar),c) ->
prerr_endline "Goal subsumed";
- raise (Success (bag,maxvar,c))*)
+ raise (Success (bag,maxvar,c))
+*)
;;
(* =================== inference ===================== *)
let bag, new_goals =
List.fold_left
(fun (bag, acc) g ->
- match simplify_goal maxvar atable bag [] g with
+ match simplify_goal ~no_demod:false maxvar atable bag [] g with
| None -> assert false
| Some (bag,g) -> bag,g::acc)
(bag, []) new_goals
projects / helm.git / commitdiff