(* $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
passives_w,passives_a
;;
- let add_passive_clauses (passives_w,passives_a) new_clauses =
- let new_clauses_w,new_clauses_a = List.fold_left add_passive_clause
+ let add_passive_clauses ?(no_weight=false)
+ (passives_w,passives_a) new_clauses =
+ let new_clauses_w,new_clauses_a =
+ List.fold_left (add_passive_clause ~no_weight)
(WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
in
(WeightPassiveSet.union new_clauses_w passives_w,
let use_age = iterno mod 10 = 0 in
- let rec aux_select passives g_passives =
+ let rec aux_select bag passives g_passives =
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
- | None -> aux_select passives g_passives
- | Some x -> let bag,g_current = x in
+ | None -> aux_select bag passives g_passives
+ | Some (bag,g_current) ->
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 Sup.one_pass_simplification current actives bag maxvar with*)
- | None -> aux_select passives g_passives
- | Some x -> let (current, bag, actives) = x in
+ | bag,None -> aux_select bag passives g_passives
+ | bag,Some (current,actives) ->
forward_infer_step bag maxvar actives passives
g_actives g_passives current
in
(fst actives)); *)
let bag,maxvar,actives,passives,g_actives,g_passives =
- aux_select passives g_passives
+ aux_select bag passives g_passives
in
debug
(Printf.sprintf "Number of active goals : %d"
let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
let initial_timestamp = Unix.gettimeofday () in
- let passives = add_passive_clauses passive_empty_set passives in
- let g_passives = add_passive_clauses passive_empty_set g_passives in
+ let passives =
+ add_passive_clauses ~no_weight:true passive_empty_set passives
+ in
+ let g_passives =
+ add_passive_clauses ~no_weight:true passive_empty_set g_passives
+ in
let g_actives = [] in
let actives = [], IDX.DT.empty in
try