type bag = t Terms.bag * int
val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
- val paramod :
+ val paramod :
+ useage:bool ->
max_steps:int ->
?timeout:float ->
bag ->
* new'= demod A'' new *
* P' = P + new' *)
debug "Forward infer step...";
+ debug ("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
(Printf.sprintf "Number of passives : %d"
(passive_set_cardinal passives));
- given_clause ~noinfer
+ given_clause ~useage ~noinfer
bag maxvar iterno weight_picks max_steps timeout
actives passives g_actives g_passives
;;
- let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+ let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
let initial_timestamp = Unix.gettimeofday () in
let passives =
add_passive_clauses ~no_weight:true passive_empty_set passives
let g_actives = [] in
let actives = [], IDX.DT.empty in
try
- given_clause ~noinfer:false
+ given_clause ~useage ~noinfer:false
bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
with
| Sup.Success (bag, _, (i,_,_,_)) ->