nCicProof.cmi: terms.cmi
terms.cmo: terms.cmi
terms.cmx: terms.cmi
-pp.cmo: terms.cmi pp.cmi
-pp.cmx: terms.cmx pp.cmi
+pp.cmo: terms.cmi foUtils.cmi pp.cmi
+pp.cmx: terms.cmx foUtils.cmx pp.cmi
foSubst.cmo: terms.cmi foSubst.cmi
foSubst.cmx: terms.cmx foSubst.cmi
orderings.cmo: terms.cmi orderings.cmi
nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi
cicBlob.cmo: terms.cmi cicBlob.cmi
cicBlob.cmx: terms.cmx cicBlob.cmi
-nCicProof.cmo: terms.cmi foSubst.cmi nCicProof.cmi
-nCicProof.cmx: terms.cmx foSubst.cmx nCicProof.cmi
-nCicParamod.cmo: terms.cmi paramod.cmi nCicProof.cmi nCicBlob.cmi \
+nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi
+nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
+nCicParamod.cmo: terms.cmi pp.cmi paramod.cmi nCicProof.cmi nCicBlob.cmi \
nCicParamod.cmi
-nCicParamod.cmx: terms.cmx paramod.cmx nCicProof.cmx nCicBlob.cmx \
+nCicParamod.cmx: terms.cmx pp.cmx paramod.cmx nCicProof.cmx nCicBlob.cmx \
nCicParamod.cmi
| _,[] -> 1
;;
-let mk_id =
- let id = ref 0 in
- fun () -> incr id; !id
-;;
-
module Utils (B : Terms.Blob) = struct
module Subst = FoSubst;; (*.Subst(B) ;;*)
module Order = Orderings.Orderings(B) ;;
| t -> Terms.Predicate t
in
let proof = Terms.Exact proofterm in
- fresh_unit_clause maxvar (mk_id (), lit, varlist, proof)
+ fresh_unit_clause maxvar (0, lit, varlist, proof)
;;
- let add_to_bag bag (_,lit,vl,proof) =
- let id = mk_id () in
- let clause = (id, lit, vl, proof) in
- let bag = Terms.M.add id (clause,false) bag in
- bag, clause
- ;;
-
- let empty_bag = Terms.M.empty ;;
-
let mk_passive_clause cl =
(Order.compute_unit_clause_weight cl, cl)
;;
(* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *)
val relocate : int -> int list -> int * int list * B.t Terms.substitution
- (* also gives a fresh ID to the clause *)
- val add_to_bag :
- B.t Terms.bag -> B.t Terms.unit_clause ->
- B.t Terms.bag * B.t Terms.unit_clause
-
- val empty_bag : B.t Terms.bag
-
val compare_passive_clauses_weight :
B.t Terms.passive_clause -> B.t Terms.passive_clause -> int
in
let module P = Paramod.Paramod(B) in
let module Pp = Pp.Pp(B) in
- let bag, maxvar = Terms.M.empty, 0 in
+ let bag, maxvar = Terms.empty_bag, 0 in
let (bag,maxvar), passives =
HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table
in
t vl
in
let get_literal id =
- let (_, lit, vl, proof),_ = Terms.M.find id bag in
+ let (_, lit, vl, proof),_ = Terms.get_from_bag id bag in
let lit =match lit with
| Terms.Predicate t -> assert false
| Terms.Equation (l,r,ty,_) ->
(* $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]
eq (string_of_rule rule);
Format.fprintf f "|%d with %d dir %s))" eq1 eq2
(string_of_direction dir);
- let (_, _, _, proof1),_ = Terms.M.find eq1 bag in
- let (_, _, _, proof2),_ = Terms.M.find eq2 bag in
+ let (_, _, _, proof1),_ = Terms.get_from_bag eq1 bag in
+ let (_, _, _, proof2),_ = Terms.get_from_bag eq2 bag in
Format.fprintf f "@[<v 2>";
aux eq1 proof1;
aux eq2 proof2;
Format.fprintf f "@]"
;;
-let pp_bag ~formatter:f bag =
+let pp_bag ~formatter:f (_,bag) =
Format.fprintf f "@[<v>";
Terms.M.iter
(fun _ (c,d) -> pp_unit_clause ~formatter:f c;
| t -> Terms.Predicate t
in
let bag, uc =
- Utils.add_to_bag bag (0, literal, vars_of_term t, proof)
+ Terms.add_to_bag (0, literal, vars_of_term t, proof) bag
in
Some (bag, uc)
else
;;
let rec orphan_murder bag acc i =
- match Terms.M.find i bag with
+ match Terms.get_from_bag i bag with
| (_,_,_,Terms.Exact _),discarded -> (discarded,acc)
| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true -> (true,acc)
| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false ->
let simplify table maxvar bag clause =
match simplify table maxvar bag clause with
- | bag, None -> let (id,_,_,_) = clause in
- Terms.M.add id (clause,true) bag, None
+ | bag, None ->
+ Terms.replace_in_bag (clause,true) bag, None
| bag, Some clause -> bag, Some clause
(*let (id,_,_,_) = clause in
if orphan_murder bag clause then
let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
(* We need to put fresh_current into the bag so that all *
* variables clauses refer to are known. *)
- let bag, fresh_current = Utils.add_to_bag bag fresh_current in
+ let bag, fresh_current = Terms.add_to_bag fresh_current bag in
(* We superpose current with active clauses *)
let bag, maxvar, additional_new_clauses =
superposition_with_table bag maxvar fresh_current atable
module M : Map.S with type key = int
= Map.Make(OT)
-type 'a bag = ('a unit_clause * bool) M.t
+type 'a bag = int
+ * (('a unit_clause * bool) M.t)
+
+ let add_to_bag (_,lit,vl,proof) (id,bag) =
+ let id = id+1 in
+ let clause = (id, lit, vl, proof) in
+ let bag = M.add id (clause,false) bag in
+ (id,bag), clause
+ ;;
+
+ let replace_in_bag ((id,_,_,_),_ as cl) (max_id,bag) =
+ let bag = M.add id cl bag in
+ (max_id,bag)
+ ;;
+
+ let get_from_bag id (_,bag) =
+ M.find id bag
+ ;;
+
+ let empty_bag = (0,M.empty);;
module type Blob =
sig
module M : Map.S with type key = int
-type 'a bag = ('a unit_clause * bool) M.t
+type 'a bag = int (* max ID *)
+ * (('a unit_clause * bool) M.t)
+
+(* also gives a fresh ID to the clause *)
+ val add_to_bag :
+ 'a unit_clause -> 'a bag ->
+ 'a bag * 'a unit_clause
+
+ val replace_in_bag :
+ 'a unit_clause * bool -> 'a bag ->
+ 'a bag
+
+ val get_from_bag :
+ int -> 'a bag -> 'a unit_clause * bool
+
+ val empty_bag : 'a bag
module type Blob =
sig
projects / helm.git / commitdiff