From: denes Date: Thu, 23 Jul 2009 17:54:28 +0000 (+0000) Subject: First compiling version X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bebc917ebff72c2e235cb3062a4c94f10a9aab27;p=helm.git First compiling version --- diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index 9223d1bcb..b1373819c 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -120,11 +120,11 @@ t vl in let get_literal id = - 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,_) -> + let (_, nlit, plit, vl, proof),_,_ = Terms.get_from_bag id bag in + let lit = match nlit,plit with + | [],[Terms.Equation (l,r,ty,_),_] -> Terms.Node [ Terms.Leaf eqP(); ty; l; r] + | _ -> assert false in lit, vl, proof in diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 137cb4586..d65fce1b2 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -26,15 +26,15 @@ module type Paramod = | Error of string | Timeout of int * t Terms.bag 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 mk_passive : bag -> input * input -> bag * t Terms.clause + val mk_goal : bag -> input * input -> bag * t Terms.clause val paramod : useage:bool -> max_steps:int -> ?timeout:float -> bag -> - g_passives:t Terms.unit_clause list -> - passives:t Terms.unit_clause list -> szsontology + g_passives:t Terms.clause list -> + passives:t Terms.clause list -> szsontology end module Paramod (B : Orderings.Blob) = struct @@ -127,7 +127,7 @@ module Paramod (B : Orderings.Blob) = struct 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 c, maxvar = Utils.mk_clause maxvar [] [ty] proof in let bag, c = Terms.add_to_bag c bag in (bag, maxvar), c ;; @@ -149,7 +149,7 @@ module Paramod (B : Orderings.Blob) = struct (false,cl,remove_passive_clause passives cl,g_passives) else let g_cl = pick_min_passive ~use_age:use_age g_passives in - let (id1,_,_,_),(id2,_,_,_) = snd cl, snd g_cl in + let (id1,_,_,_,_),(id2,_,_,_,_) = snd cl, snd g_cl in let cmp = if use_age then id1 <= id2 else fst cl <= fst g_cl in @@ -185,7 +185,7 @@ module Paramod (B : Orderings.Blob) = struct * new'= demod A'' new * * P' = P + new' *) debug "Forward infer step..."; - debug ("Number of actives : " ^ (string_of_int (List.length (fst actives)))); + debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives))))); let bag, maxvar, actives, new_clauses = Sup.infer_right bag maxvar current actives in @@ -201,7 +201,7 @@ module Paramod (B : Orderings.Blob) = struct | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc) (bag,[]) g_actives in - let ctable = IDX.index_unit_clause IDX.DT.empty current in + let ctable = IDX.index_clause IDX.DT.empty current in let bag, maxvar, new_goals = List.fold_left (fun (bag,m,acc) g -> @@ -215,7 +215,7 @@ module Paramod (B : Orderings.Blob) = struct add_passive_goals g_passives new_goals ;; - let rec given_clause ~noinfer + let rec given_clause ~useage ~noinfer bag maxvar iterno weight_picks max_steps timeout actives passives g_actives g_passives = @@ -229,8 +229,8 @@ module Paramod (B : Orderings.Blob) = struct if noinfer then begin debug - ("Last chance: all is indexed " ^ string_of_float - (Unix.gettimeofday())); + (lazy("Last chance: all is indexed " ^ string_of_float + (Unix.gettimeofday()))); let maxgoals = 100 in ignore(List.fold_left (fun (acc,i) x -> @@ -245,15 +245,15 @@ module Paramod (B : Orderings.Blob) = struct end else if false then (* activates last chance strategy *) begin - debug("Last chance: "^string_of_float (Unix.gettimeofday())); - given_clause ~noinfer:true bag maxvar iterno weight_picks max_steps + debug (lazy("Last chance: "^string_of_float (Unix.gettimeofday()))); + given_clause ~useage ~noinfer:true bag maxvar iterno weight_picks max_steps (Some (Unix.gettimeofday () +. 20.)) actives passives g_actives g_passives; raise (Stop (Timeout (maxvar,bag))); end else raise (Stop (Timeout (maxvar,bag))); - let use_age = weight_picks = (iterno / 6 + 1) in + let use_age = useage && (weight_picks = (iterno / 6 + 1)) in let weight_picks = if use_age then 0 else weight_picks+1 in @@ -270,7 +270,7 @@ module Paramod (B : Orderings.Blob) = struct else let bag = Terms.replace_in_bag (current,false,iterno) bag in if backward then - let _ = debug ("Selected goal : " ^ Pp.pp_unit_clause current) in + let _ = debug (lazy("Selected goal : " ^ Pp.pp_clause current)) in match if noinfer then if weight > monster then None else Some (bag,current) @@ -287,7 +287,7 @@ module Paramod (B : Orderings.Blob) = struct backward_infer_step bag maxvar actives passives g_actives g_passives g_current iterno else - let _ = debug ("Selected fact : " ^ Pp.pp_unit_clause current) in + let _ = debug (lazy("Selected fact : " ^ Pp.pp_clause current)) in (*let is_orphan = Sup.orphan_murder bag (fst actives) current in*) match if noinfer then @@ -316,7 +316,7 @@ module Paramod (B : Orderings.Blob) = struct if noinfer then let actives = current::fst actives, - IDX.index_unit_clause (snd actives) current + IDX.index_clause (snd actives) current in bag,maxvar,actives,passives,g_actives,g_passives else @@ -333,16 +333,16 @@ module Paramod (B : Orderings.Blob) = struct aux_select bag passives g_passives in debug - (Printf.sprintf "Number of active goals : %d" - (List.length g_actives)); + (lazy(Printf.sprintf "Number of active goals : %d" + (List.length g_actives))); debug - (Printf.sprintf "Number of passive goals : %d" - (passive_set_cardinal g_passives)); + (lazy(Printf.sprintf "Number of passive goals : %d" + (passive_set_cardinal g_passives))); debug - (Printf.sprintf "Number of actives : %d" (List.length (fst actives))); + (lazy(Printf.sprintf "Number of actives : %d" (List.length (fst actives)))); debug - (Printf.sprintf "Number of passives : %d" - (passive_set_cardinal passives)); + (lazy(Printf.sprintf "Number of passives : %d" + (passive_set_cardinal passives))); given_clause ~useage ~noinfer bag maxvar iterno weight_picks max_steps timeout actives passives g_actives g_passives @@ -362,14 +362,14 @@ module Paramod (B : Orderings.Blob) = struct given_clause ~useage ~noinfer:false bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives with - | Sup.Success (bag, _, (i,_,_,_)) -> + | Sup.Success (bag, _, (i,_,_,_,_)) -> let l = let rec traverse ongoal (accg,acce) i = match Terms.get_from_bag i bag with - | (id,_,_,Terms.Exact _),_,_ -> + | (id,_,_,_,Terms.Exact _),_,_ -> if ongoal then [i],acce else if (List.mem i acce) then accg,acce else accg,acce@[i] - | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ -> + | (_,_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ -> if (not ongoal) && (List.mem i acce) then accg,acce else let accg,acce = @@ -382,7 +382,7 @@ module Paramod (B : Orderings.Blob) = struct in let max_w = List.fold_left (fun acc i -> let (cl,_,_) = Terms.get_from_bag i bag in - max acc (Order.compute_unit_clause_weight cl)) 0 l in + max acc (Order.compute_clause_weight cl)) 0 l in prerr_endline "Statistics :"; prerr_endline ("Max weight : " ^ (string_of_int max_w)); (* List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) = diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index 9cffd9d28..8376b256b 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -21,15 +21,15 @@ module type Paramod = | Error of string | Timeout of int * t Terms.bag 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 mk_passive : bag -> input * input -> bag * t Terms.clause + val mk_goal : bag -> input * input -> bag * t Terms.clause val paramod : useage:bool -> max_steps:int -> ?timeout:float -> bag -> - g_passives:t Terms.unit_clause list -> - passives:t Terms.unit_clause list -> szsontology + g_passives:t Terms.clause list -> + passives:t Terms.clause list -> szsontology end module Paramod ( B : Orderings.Blob ) : Paramod diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index ddf5726c4..061dae2b1 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -68,8 +68,8 @@ let pp_proof bag ~formatter:f p = eq (string_of_rule rule); Format.fprintf f "|%d with %d dir %s))" eq1 eq2 (string_of_direction dir); - let (_, _, _, proof1),_,_ = Terms.get_from_bag eq1 bag in - let (_, _, _, proof2),_,_ = Terms.get_from_bag eq2 bag in + let (_, _, _, _, proof1),_,_ = Terms.get_from_bag eq1 bag in + let (_, _, _, _, proof2),_,_ = Terms.get_from_bag eq2 bag in Format.fprintf f "@["; aux eq1 proof1; aux eq2 proof2; @@ -87,6 +87,38 @@ let string_of_comparison = function | Terms.Incomparable -> "=?=" | Terms.Invertible -> "=<->=" +(*let pp_literal ~formatter:f l = + match l with + | Terms.Predicate t -> + Format.fprintf f "@[{"; + pp_foterm f t; + Format.fprintf f "@;[%s] by " + (String.concat ", " (List.map string_of_int vars)); + (match proof with + | Terms.Exact t -> pp_foterm f t + | Terms.Step (rule, id1, id2, _, p, _) -> + Format.fprintf f "%s %d with %d at %s" + (string_of_rule rule) id1 id2 (String.concat + "," (List.map string_of_int p))); + Format.fprintf f "@]" + | Terms.Equation (lhs, rhs, ty, comp) -> + Format.fprintf f "@[{"; + pp_foterm f ty; + Format.fprintf f "}:@;@["; + pp_foterm f lhs; + Format.fprintf f "@;%s@;" (string_of_comparison comp); + pp_foterm f rhs; + Format.fprintf f "@]@;[%s] by " + (String.concat ", " (List.map string_of_int vars)); + (match proof with + | Terms.Exact t -> pp_foterm f t + | Terms.Step (rule, id1, id2, _, p, _) -> + Format.fprintf f "%s %d with %d at %s" + (string_of_rule rule) id1 id2 (String.concat + "," (List.map string_of_int p))); + Format.fprintf f "@]" +*) + let pp_unit_clause ~formatter:f c = let (id, l, vars, proof) = c in Format.fprintf f "Id : %3d, " id ; @@ -121,10 +153,14 @@ let pp_unit_clause ~formatter:f c = Format.fprintf f "@]" ;; +let pp_clause ~formatter:f c = + assert false +;; + let pp_bag ~formatter:f (_,bag) = Format.fprintf f "@["; Terms.M.iter - (fun _ (c,d,_) -> pp_unit_clause ~formatter:f c; + (fun _ (c,d,_) -> pp_clause ~formatter:f c; if d then Format.fprintf f " (discarded)@;" else Format.fprintf f "@;") bag; Format.fprintf f "@]" @@ -160,4 +196,8 @@ let pp_unit_clause ?margin x= on_buffer ?margin pp_unit_clause x ;; +let pp_clause ?margin x = + on_buffer ?margin pp_clause x +;; + end diff --git a/helm/software/components/ng_paramodulation/pp.mli b/helm/software/components/ng_paramodulation/pp.mli index 767c87e0b..df0c0d325 100644 --- a/helm/software/components/ng_paramodulation/pp.mli +++ b/helm/software/components/ng_paramodulation/pp.mli @@ -18,6 +18,7 @@ module Pp (B : Terms.Blob) : val pp_proof: B.t Terms.bag -> B.t Terms.proof -> string val pp_substitution: B.t Terms.substitution -> string val pp_unit_clause: ?margin:int -> B.t Terms.unit_clause -> string + val pp_clause: ?margin:int -> B.t Terms.clause -> string val pp_bag: B.t Terms.bag -> string end diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml index fd68f0fe7..04aaa75f5 100644 --- a/helm/software/components/ng_paramodulation/stats.ml +++ b/helm/software/components/ng_paramodulation/stats.ml @@ -25,7 +25,7 @@ module Stats (B : Terms.Blob) = let occ_nbr t = occ_nbr t 0;; let goal_occ_nbr t = function - | (_,Terms.Equation (l,r,_,_),_,_) -> + | (_,[],[Terms.Equation (l,r,_,_),_],_,_) -> occ_nbr t l + occ_nbr t r | _ -> assert false ;; @@ -48,11 +48,11 @@ module Stats (B : Terms.Blob) = in match l with | [] -> acc - | (_,hd,_,_)::tl -> - match hd with - | Terms.Equation (l,r,_,_) -> + | (_,nlit,plit,_,_)::tl -> + match nlit,plit with + | [],[Terms.Equation (l,r,_,_),_] -> parse_symbols (aux (aux acc l) r) tl - | Terms.Predicate _ -> assert false; + | _ -> assert false; ;; let goal_pos t goal = @@ -73,8 +73,9 @@ module Stats (B : Terms.Blob) = in aux [] (match goal with - | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] - | _,Terms.Predicate p,_,_ -> p) + | _,[],[Terms.Equation (l,r,ty,_),_],_,_ -> + Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] + | _ -> assert false) ;; let parse_symbols l goal = @@ -92,11 +93,10 @@ module Stats (B : Terms.Blob) = let rec dependencies op clauses acc = match clauses with | [] -> acc - | (_,lit,_,_)::tl -> - match lit with - | Terms.Predicate _ -> assert false - | Terms.Equation (l,r,_,_) -> - match l,r with + | (_,nlit,plit,_,_)::tl -> + match nlit,plit with + | [],[Terms.Equation (l,r,_,_),_] -> + (match l,r with | (Terms.Node (Terms.Leaf op1::_),Terms.Node (Terms.Leaf op2::_)) -> if (B.eq op1 op) && not (B.eq op2 op) then @@ -126,7 +126,8 @@ module Stats (B : Terms.Blob) = dependencies op tl (op1::acc) else dependencies op tl acc - | _ -> dependencies op tl acc + | _ -> dependencies op tl acc) + | _ -> assert false ;; let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));; diff --git a/helm/software/components/ng_paramodulation/stats.mli b/helm/software/components/ng_paramodulation/stats.mli index 271fd2bcf..95fbe1d0c 100644 --- a/helm/software/components/ng_paramodulation/stats.mli +++ b/helm/software/components/ng_paramodulation/stats.mli @@ -16,11 +16,11 @@ module Stats (B : Orderings.Blob) : module SymbMap : Map.S with type key = B.t - val parse_symbols : B.t Terms.unit_clause list -> (* hypotheses *) - B.t Terms.unit_clause -> (* goal *) + val parse_symbols : B.t Terms.clause list -> (* hypotheses *) + B.t Terms.clause -> (* goal *) (B.t * int * int * int * int list) list - val dependencies : B.t -> B.t Terms.unit_clause list -> B.t list + val dependencies : B.t -> B.t Terms.clause list -> B.t list end diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 93468738b..0dbac61c3 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -113,7 +113,7 @@ module Superposition (B : Orderings.Blob) = | t -> Terms.Predicate t in let bag, uc = - Terms.add_to_bag (0, literal, Terms.vars_of_term t, proof) bag + Terms.add_to_bag (0, [], [literal,true], Terms.vars_of_term t, proof) bag in Some (bag, uc) else @@ -138,77 +138,48 @@ module Superposition (B : Orderings.Blob) = in list_first (fun (dir, is_pos, pos, (id,nlit,plit,vl,_)) -> - match lit with - | Terms.Predicate _ -> assert false - | Terms.Equation (l,r,_,o) -> - let side, newside = if dir=Terms.Left2Right then l,r else r,l in - try - let subst = - prof_demod_u.HExtlib.profile - (Unif.unification (* (varlist@vl) *) varlist subterm) side - in - let side = - prof_demod_s.HExtlib.profile - (Subst.apply_subst subst) side - in - let newside = - prof_demod_s.HExtlib.profile - (Subst.apply_subst subst) newside - in - if o = Terms.Incomparable || o = Terms.Invertible then - let o = - prof_demod_o.HExtlib.profile - (Order.compare_terms newside) side in - (* Riazanov, pp. 45 (ii) *) - if o = Terms.Lt then - Some (newside, subst, id, dir) - else - ((*prerr_endline ("Filtering: " ^ - Pp.pp_foterm side ^ " =(< || =)" ^ - Pp.pp_foterm newside ^ " coming from " ^ - Pp.pp_clause uc );*)None) - else - Some (newside, subst, id, dir) - with FoUnif.UnificationFailure _ -> None) - (IDX.ClauseSet.elements cands) + match nlit,plit with + | [], [(lit,_)] -> + (match lit with + | Terms.Predicate _ -> assert false + | Terms.Equation (l,r,_,o) -> + let side, newside = if dir=Terms.Left2Right then l,r else r,l in + try + let subst = + prof_demod_u.HExtlib.profile + (Unif.unification (* (varlist@vl) *) varlist subterm) side + in + let side = + prof_demod_s.HExtlib.profile + (Subst.apply_subst subst) side + in + let newside = + prof_demod_s.HExtlib.profile + (Subst.apply_subst subst) newside + in + if o = Terms.Incomparable || o = Terms.Invertible then + let o = + prof_demod_o.HExtlib.profile + (Order.compare_terms newside) side in + (* Riazanov, pp. 45 (ii) *) + if o = Terms.Lt then + Some (newside, subst, id, dir) + else + ((*prerr_endline ("Filtering: " ^ + Pp.pp_foterm side ^ " =(< || =)" ^ + Pp.pp_foterm newside ^ " coming from " ^ + Pp.pp_clause uc );*)None) + else + Some (newside, subst, id, dir) + with FoUnif.UnificationFailure _ -> None) + | _ -> None) + (IDX.ClauseSet.elements cands) ;; let prof_demod = HExtlib.profile ~enable "demod";; let demod table varlist x = prof_demod.HExtlib.profile (demod table varlist) x ;; - let demodulate_once_old ~jump_to_right bag (id, literal, vl, pr) table = - match literal with - | Terms.Predicate t -> assert false - | Terms.Equation (l,r,ty,_) -> - let left_position = if jump_to_right then None else - first_position [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l - (demod table vl) - in - match left_position with - | Some (newt, subst, id2, dir, pos) -> - begin - match build_clause bag (fun _ -> true) Terms.Demodulation - newt subst id id2 pos dir - with - | None -> assert false - | Some x -> Some (x,false) - end - | None -> - match first_position - [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) r - (demod table vl) - with - | None -> None - | Some (newt, subst, id2, dir, pos) -> - match build_clause bag (fun _ -> true) - Terms.Demodulation newt subst id id2 pos dir - with - | None -> assert false - | Some x -> Some (x,true) - ;; - let parallel_demod table vl bag t pos ctx id = match demod table vl t with | None -> (bag,t,id) @@ -217,12 +188,14 @@ module Superposition (B : Orderings.Blob) = Terms.Demodulation (ctx newside) subst id id2 pos dir with | None -> assert false - | Some (bag,(id,_,_,_)) -> + | Some (bag,(id,_,_,_,_)) -> (bag,newside,id) ;; - let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table = - match literal with + let demodulate_once ~jump_to_right bag (id, nlit, plit, vl, pr) table = + match nlit,plit with + |[],[literal,_] -> + (match literal with | Terms.Predicate t -> assert false | Terms.Equation (l,r,ty,_) -> let bag,l,id1 = if jump_to_right then (bag,l,id) else @@ -239,7 +212,8 @@ module Superposition (B : Orderings.Blob) = if id = id2 then None else let cl,_,_ = Terms.get_from_bag id2 bag in - Some ((bag,cl),jump_to_right) + Some ((bag,cl),jump_to_right)) + | _ -> assert false; ;; let rec demodulate ~jump_to_right bag clause table = @@ -249,19 +223,12 @@ module Superposition (B : Orderings.Blob) = bag clause table ;; - let rec demodulate_old ~jump_to_right bag clause table = - match demodulate_once_old ~jump_to_right bag clause table with - | None -> bag, clause - | Some ((bag, clause),r) -> demodulate_old ~jump_to_right:r - bag clause table - ;; - let are_alpha_eq cl1 cl2 = - let get_term (_,lit,_,_) = - match lit with - | Terms.Predicate _ -> assert false - | Terms.Equation (l,r,ty,_) -> + let get_term (_,nlit,plit,_,_) = + match nlit,plit with + | [], [Terms.Equation (l,r,ty,_),_] -> Terms.Node [Terms.Leaf B.eqP; ty; l ; r] + | _ -> assert false in try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true with FoUnif.UnificationFailure _ -> false @@ -288,12 +255,12 @@ module Superposition (B : Orderings.Blob) = (* move away *) let is_identity_clause ~unify = function - | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true - | _, Terms.Equation (l,r,_,_), vl, proof when unify -> + | _, [], [Terms.Equation (_,_,_,Terms.Eq),_], _, _ -> true + | _, [], [Terms.Equation (l,r,_,_),_], vl, proof when unify -> (try ignore(Unif.unification (* vl *) [] l r); true with FoUnif.UnificationFailure _ -> false) - | _, Terms.Equation (_,_,_,_), _, _ -> false - | _, Terms.Predicate _, _, _ -> assert false + | _, [], [Terms.Equation (_,_,_,_),_], _, _ -> false + | _ -> assert false ;; let build_new_clause bag maxvar filter rule t subst id id2 pos dir = @@ -319,7 +286,7 @@ module Superposition (B : Orderings.Blob) = bag, maxvar, res ;; - + (* Tries to rewrite an equality to identity, using unit equalities in table *) let rewrite_eq ~unify l r ty vl table = let retrieve = if unify then IDX.DT.retrieve_unifiables else IDX.DT.retrieve_generalizations in @@ -328,7 +295,7 @@ module Superposition (B : Orderings.Blob) = let f b c = let id, dir, l, r, vl = match c with - | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl + | (d,_,_, (id,[],[Terms.Equation (l,r,ty,_),_],vl,_))-> id, d, l, r, vl |_ -> assert false in let reverse = (dir = Terms.Left2Right) = b in @@ -351,16 +318,16 @@ module Superposition (B : Orderings.Blob) = aux (cands1 @ cands2) ;; - let is_subsumed ~unify bag maxvar (id, lit, vl, _) table = - match lit with - | Terms.Predicate _ -> assert false - | Terms.Equation (l,r,ty,_) -> - match rewrite_eq ~unify l r ty vl table with + let is_subsumed ~unify bag maxvar (id, nlit, plit, vl, _) table = + match nlit,plit with + | [],[Terms.Equation (l,r,ty,_) ,_]-> + (match rewrite_eq ~unify l r ty vl table with | None -> None | Some (id2, dir, subst) -> let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in build_new_clause bag maxvar (fun _ -> true) - Terms.Superposition id_t subst id id2 [2] dir + Terms.Superposition id_t subst id id2 [2] dir) + | _ -> assert false ;; let prof_is_subsumed = HExtlib.profile ~enable "is_subsumed";; let is_subsumed ~unify bag maxvar c x = @@ -371,18 +338,19 @@ module Superposition (B : Orderings.Blob) = let rec deep_eq ~unify l r ty pos contextl contextr table acc = match acc with | None -> None - | Some(bag,maxvar,(id,lit,vl,p),subst) -> + | Some(bag,maxvar,(id,nlit,plit,vl,p),subst) -> let l = Subst.apply_subst subst l in let r = Subst.apply_subst subst r in try let subst1 = Unif.unification (* vl *) [] l r in let lit = - match lit with Terms.Predicate _ -> assert false - | Terms.Equation (l,r,ty,o) -> + match nlit,plit with + | [],[Terms.Equation (l,r,ty,o),_] -> Terms.Equation (FoSubst.apply_subst subst1 l, FoSubst.apply_subst subst1 r, ty, o) + | _ -> assert false in - Some(bag,maxvar,(id,lit,vl,p),Subst.concat subst1 subst) + Some(bag,maxvar,(id,[],[lit,true],vl,p),Subst.concat subst1 subst) with FoUnif.UnificationFailure _ -> match rewrite_eq ~unify l r ty vl table with | Some (id2, dir, subst1) -> @@ -427,9 +395,9 @@ module Superposition (B : Orderings.Blob) = let rec orphan_murder bag acc i = 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,_ -> + | (_,_,_,_,Terms.Exact _),discarded,_ -> (discarded,acc) + | (_,_,_,_,Terms.Step (_,i1,i2,_,_,_)),true,_ -> (true,acc) + | (_,_,_,_,Terms.Step (_,i1,i2,_,_,_)),false,_ -> if (List.mem i acc) then (false,acc) else match orphan_murder bag acc i1 with | (true,acc) -> (true,acc) @@ -439,8 +407,8 @@ module Superposition (B : Orderings.Blob) = ;; let orphan_murder bag actives cl = - let (id,_,_,_) = cl in - let actives = List.map (fun (i,_,_,_) -> i) actives in + let (id,_,_,_,_) = cl in + let actives = List.map (fun (i,_,_,_,_) -> i) actives in let (res,_) = orphan_murder bag actives id in if res then debug "Orphan murdered"; res ;; @@ -464,7 +432,7 @@ module Superposition (B : Orderings.Blob) = let simplify table maxvar bag clause = match simplify table maxvar bag clause with | bag, None -> - let (id,_,_,_) = clause in + let (id,_,_,_,_) = clause in let (_,_,iter) = Terms.get_from_bag id bag in Terms.replace_in_bag (clause,true,iter) bag, None | bag, Some clause -> bag, Some clause @@ -587,12 +555,12 @@ module Superposition (B : Orderings.Blob) = if (is_identity_clause ~unify:true clause) then raise (Success (bag, maxvar, clause)) else - let (id,lit,vl,_) = clause in + let (id,nlit,plit,vl,_) = clause in if vl = [] then Some (bag,clause) else let l,r,ty = - match lit with - | Terms.Equation(l,r,ty,_) -> l,r,ty + match nlit,plit with + | [],[Terms.Equation(l,r,ty,_),_] -> l,r,ty | _ -> assert false in match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x) @@ -621,11 +589,10 @@ module Superposition (B : Orderings.Blob) = let superposition table varlist subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in HExtlib.filter_map - (fun (dir, (id,lit,vl,_ (*as uc*))) -> - match lit with - | Terms.Predicate _ -> assert false - | Terms.Equation (l,r,_,o) -> - let side, newside = if dir=Terms.Left2Right then l,r else r,l in + (fun (dir, _, _, (id,nlit,plit,vl,_ (*as uc*))) -> + match nlit,plit with + | [],[Terms.Equation (l,r,_,o),_] -> + (let side, newside = if dir=Terms.Left2Right then l,r else r,l in try let subst = Unif.unification (* (varlist@vl)*) [] subterm side @@ -644,27 +611,27 @@ module Superposition (B : Orderings.Blob) = else Some (context newside, subst, id, pos, dir) with FoUnif.UnificationFailure _ -> None) + | _ -> assert false) (IDX.ClauseSet.elements cands) ;; (* Superposes selected equation with equalities in table *) - let superposition_with_table bag maxvar (id,selected,vl,_) table = - match selected with - | Terms.Predicate _ -> assert false - | Terms.Equation (l,r,ty,Terms.Lt) -> + let superposition_with_table bag maxvar (id,nlit,plit,vl,_) table = + match nlit,plit with + | [],[Terms.Equation (l,r,ty,Terms.Lt),_] -> fold_build_new_clause bag maxvar id Terms.Superposition (fun _ -> true) (all_positions [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) r (superposition table vl)) - | Terms.Equation (l,r,ty,Terms.Invertible) - | Terms.Equation (l,r,ty,Terms.Gt) -> + | [],[Terms.Equation (l,r,ty,Terms.Invertible),_] + | [],[Terms.Equation (l,r,ty,Terms.Gt),_] -> fold_build_new_clause bag maxvar id Terms.Superposition (fun _ -> true) (all_positions [2] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l (superposition table vl)) - | Terms.Equation (l,r,ty,Terms.Incomparable) -> + | [],[Terms.Equation (l,r,ty,Terms.Incomparable),_] -> let filtering avoid subst = (* Riazanov: p.33 condition (iv) *) let l = Subst.apply_subst subst l in let r = Subst.apply_subst subst r in @@ -730,8 +697,8 @@ module Superposition (B : Orderings.Blob) = in debug "Another superposition"; let new_clauses = new_clauses @ additional_new_clauses in - debug (Printf.sprintf "Demodulating %d clauses" - (List.length new_clauses)); + debug (lazy (Printf.sprintf "Demodulating %d clauses" + (List.length new_clauses))); let bag, new_clauses = HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses in @@ -746,7 +713,7 @@ module Superposition (B : Orderings.Blob) = let infer_left bag maxvar goal (_alist, atable) = (* We superpose the goal with active clauses *) - if (match goal with (_,_,[],_) -> true | _ -> false) then bag, maxvar, [] + if (match goal with (_,_,_,[],_) -> true | _ -> false) then bag, maxvar, [] else let bag, maxvar, new_goals = superposition_with_table bag maxvar goal atable diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index a7173b1b9..0e69cace9 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -74,16 +74,16 @@ module M : Map.S with type key = int = Map.Make(OT) type 'a bag = int - * (('a unit_clause * bool * int) M.t) + * (('a clause * bool * int) M.t) - let add_to_bag (_,lit,vl,proof) (id,bag) = + let add_to_bag (_,nlit,plit,vl,proof) (id,bag) = let id = id+1 in - let clause = (id, lit, vl, proof) in + let clause = (id, nlit, plit, vl, proof) in let bag = M.add id (clause,false,0) bag in (id,bag), clause ;; - let replace_in_bag ((id,_,_,_),_,_ as cl) (max_id,bag) = + let replace_in_bag ((id,_,_,_,_),_,_ as cl) (max_id,bag) = let bag = M.add id cl bag in (max_id,bag) ;; diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index 6ef3eeed8..90ccaf591 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -66,19 +66,19 @@ val vars_of_term : ?start_acc:int list -> 'a foterm -> int list module M : Map.S with type key = int type 'a bag = int (* max ID *) - * (('a unit_clause * bool * int) M.t) + * (('a clause * bool * int) M.t) (* also gives a fresh ID to the clause *) val add_to_bag : - 'a unit_clause -> 'a bag -> - 'a bag * 'a unit_clause + 'a clause -> 'a bag -> + 'a bag * 'a clause val replace_in_bag : - 'a unit_clause * bool * int -> 'a bag -> + 'a clause * bool * int -> 'a bag -> 'a bag val get_from_bag : - int -> 'a bag -> 'a unit_clause * bool * int + int -> 'a bag -> 'a clause * bool * int val empty_bag : 'a bag