(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
let debug s = prerr_endline s ;;
-(* let debug _ = ();;*)
+let debug _ = ();;
-let monster = 500;;
+let monster = 100;;
module Paramod (B : Terms.Blob) = struct
exception Failure of string * B.t Terms.bag * int * int
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 bag, c = Utils.add_to_bag bag c in
+ let bag, c = Terms.add_to_bag c bag in
(bag, maxvar), c
;;
let rec aux_select bag passives g_passives =
let backward,(weight,current),passives,g_passives =
- select ~use_age passives g_passives
+ select ~use_age:false passives g_passives
in
if use_age && weight > monster then
- let bag,cl = Utils.add_to_bag bag current in
+ let bag,cl = Terms.add_to_bag current bag in
if backward then
aux_select bag passives (add_passive_clause g_passives cl)
else
if weight > monster then bag,None
else bag, Some (current,actives)
else if Sup.orphan_murder bag (fst actives) current then
- let (id,_,_,_) = current in
- let bag = Terms.M.add id (current,true) bag in
+ let _ = debug "Orphan murdered" in
+ let bag = Terms.replace_in_bag (current,true) bag in
bag, None
else Sup.keep_simplified current actives bag maxvar
with
| Sup.Success (bag, _, (i,_,_,_)) ->
let l =
let rec traverse ongoal (accg,acce) i =
- match Terms.M.find i bag with
+ match Terms.get_from_bag i bag with
| (id,_,_,Terms.Exact _),_ ->
if ongoal then [i],acce else
if (List.mem i acce) then accg,acce else accg,acce@[i]