let visit bag pos ctx id t f =
let rec aux bag pos ctx id subst = function
| Terms.Leaf _ as t ->
- let bag,subst,t,id = f bag t pos ctx id
- in assert (subst=[]); bag,t,id
+ let bag,subst,t,id = f bag t pos ctx id in
+ assert (subst=[]); bag,t,id
| Terms.Var i as t ->
let t= Subst.apply_subst subst t in
bag,t,id
let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
let t = Subst.apply_subst subst t in
if filter subst then
- let literal =
+ let tooflex,literal =
match t with
- | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
- let o = Order.compare_terms l r in
- Terms.Equation (l, r, ty, o)
- | t -> Terms.Predicate t
+ | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq (B.eqP()) eq ->
+ let o = Order.compare_terms l r in
+ (match l,r,o with
+ Terms.Var _,_,Terms.Gt
+ | _,Terms.Var _,Terms.Lt -> assert false
+ | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) ->
+ true, Terms.Equation (l, r, ty, o)
+ | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) ->
+ true, Terms.Equation (l, r, ty, o)
+ | _ -> false, Terms.Equation (l, r, ty, o))
+ | t -> false,Terms.Predicate t
in
let bag, uc =
Terms.add_to_bag (0, literal, Terms.vars_of_term t, proof) bag
in
- Some (bag, uc)
+ if tooflex then None else Some (bag, uc)
else
((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
;;
match build_clause bag (fun _ -> true)
Terms.Demodulation (ctx inewside) subst id id2 pos dir
with
- | None -> assert false
+ | None -> (bag,[],t,id) (* see tooflex; was assert false *)
| Some (bag,(id,_,_,_)) ->
(bag,subst,newside,id)
;;
| Terms.Equation (l,r,ty,_) ->
let bag,l,id1 =
visit bag [2]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id l
+ (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ]) id l
(ctx_demod table vl)
in
let bag,_,id2 =
visit bag [3]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 r
+ (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ]) id1 r
(ctx_demod table vl)
in
let cl,_,_ = Terms.get_from_bag id2 bag in
match lit with
| Terms.Predicate _ -> assert false
| Terms.Equation (l,r,ty,_) ->
- Terms.Node [Terms.Leaf B.eqP; ty; l ; r]
+ Terms.Node [Terms.Leaf (B.eqP()); ty; l ; r]
in
try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true
with FoUnif.UnificationFailure _ -> false
bag, maxvar, res
;;
- let rewrite_eq ~unify l r ty vl table =
+ (* rewrite_eq check if in table there an equation matching l=r;
+ used in subsumption and deep_eq. In deep_eq, we need to match
+ several times times w.r.t. the same table, hence we should refresh
+ the retrieved clauses, to avoid clashes of variables *)
+
+ let rewrite_eq ~refresh ~unify maxvar l r ty vl table =
let retrieve = if unify then IDX.DT.retrieve_unifiables
else IDX.DT.retrieve_generalizations in
let lcands = retrieve table l in
let rcands = retrieve table r in
- let f b c =
+ 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
let reverse = (dir = Terms.Left2Right) = b in
let l, r, proof_rewrite_dir = if reverse then l,r,Terms.Left2Right
else r,l, Terms.Right2Left in
- (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl)
+ (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ], vl)
in
let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in
let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in
- let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in
+ let t = Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ] in
let locked_vars = if unify then [] else vl in
let rec aux = function
| [] -> None
| (id2,dir,c,vl1)::tl ->
try
+ let c,maxvar = if refresh then
+ let maxvar,_,r = Utils.relocate maxvar vl1 [] in
+ Subst.apply_subst r c,maxvar
+ else c,maxvar in
let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in
- Some (id2, dir, subst)
+ Some (id2, dir, subst, maxvar)
with FoUnif.UnificationFailure _ -> aux tl
in
aux (cands1 @ cands2)
match lit with
| Terms.Predicate _ -> assert false
| Terms.Equation (l,r,ty,_) ->
- match rewrite_eq ~unify l r ty vl table with
+ match rewrite_eq ~refresh:false ~unify maxvar 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
+ | Some (id2, dir, subst, maxvar) ->
+ 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
;;
(* id refers to a clause proving contextl l = contextr r *)
let rec deep_eq ~unify l r ty pos contextl contextr table acc =
+ (* let _ = prerr_endline ("pos = " ^ String.concat ","
+ (List.map string_of_int pos)) in *)
match acc with
| None -> None
| Some(bag,maxvar,(id,lit,vl,p),subst) ->
(* prerr_endline ("input subst = "^Pp.pp_substitution subst); *)
+ (* prerr_endline ("l prima =" ^ Pp.pp_foterm l); *)
+ (* prerr_endline ("r prima =" ^ Pp.pp_foterm r); *)
let l = Subst.apply_subst subst l in
let r = Subst.apply_subst subst r in
+ (* prerr_endline ("l dopo =" ^ Pp.pp_foterm l); *)
+ (* prerr_endline ("r dopo =" ^ Pp.pp_foterm r); *)
try
let subst1 = Unif.unification (* vl *) [] l r in
let lit =
match lit with Terms.Predicate _ -> assert false
| Terms.Equation (l,r,ty,o) ->
- Terms.Equation (FoSubst.apply_subst subst1 l,
- FoSubst.apply_subst subst1 r, ty, o)
+ let l = Subst.apply_subst subst1 l in
+ let r = Subst.apply_subst subst1 r in
+ Terms.Equation (l, r, ty, o)
in
Some(bag,maxvar,(id,lit,vl,p),Subst.concat subst1 subst)
with FoUnif.UnificationFailure _ ->
- match rewrite_eq ~unify l r ty vl table with
- | Some (id2, dir, subst1) ->
+ match rewrite_eq ~refresh:true ~unify maxvar l r ty vl table with
+ | Some (id2, dir, subst1, maxvar) ->
(* prerr_endline ("subst1 = "^Pp.pp_substitution subst1);
- prerr_endline ("old subst = "^Pp.pp_substitution subst);*)
+ prerr_endline ("old subst = "^Pp.pp_substitution subst); *)
let newsubst = Subst.concat subst1 subst in
let id_t =
FoSubst.apply_subst newsubst
- (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r])
+ (Terms.Node[Terms.Leaf (B.eqP());ty;contextl r;contextr r])
in
- (match
+ (match
build_new_clause_reloc bag maxvar (fun _ -> true)
Terms.Superposition id_t
- subst1 id id2 (pos@[2]) dir
- with
+ subst1 id id2 (pos@[2]) dir
+ with
| Some ((bag, maxvar), c), r ->
- (* prerr_endline ("r = "^Pp.pp_substitution r); *)
+ (* prerr_endline ("creo "^ Pp.pp_unit_clause c); *)
+ (* prerr_endline ("r = "^Pp.pp_substitution r); *)
let newsubst = Subst.flat
(Subst.concat r subst) in
Some(bag,maxvar,c,newsubst)
let bag, clause =
if no_demod then bag, clause else demodulate bag clause table
in
- let _ = debug (lazy ("demodulated goal : "
+ let _ = debug(lazy ("demodulated goal : "
^ Pp.pp_unit_clause clause))
in
if List.exists (are_alpha_eq clause) g_actives then None
| None -> Some (bag,clause)
| Some (bag,maxvar,cl,subst) ->
debug (lazy "Goal subsumed");
+ debug (lazy ("subst in superpos: " ^ Pp.pp_substitution subst));
raise (Success (bag,maxvar,cl,subst))
(*
match is_subsumed ~unify:true bag maxvar clause table with
| None -> Some (bag, clause)
| Some ((bag,maxvar),c) ->
- prerr_endline "Goal subsumed";
+ debug (lazy "Goal subsumed");
raise (Success (bag,maxvar,c))
*)
;;
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 ])
+ (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) ->
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 ])
+ (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ])
l (superposition table vl))
| Terms.Equation (l,r,ty,Terms.Incomparable) ->
let filtering avoid subst = (* Riazanov: p.33 condition (iv) *)
fold_build_new_clause bag maxvar id Terms.Superposition
(filtering Terms.Gt)
(all_positions [3]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+ (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ])
r (superposition table vl))
in
let bag, maxvar, l_terms =
fold_build_new_clause bag maxvar id Terms.Superposition
(filtering Terms.Lt)
(all_positions [2]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+ (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ])
l (superposition table vl))
in
bag, maxvar, r_terms @ l_terms
projects / helm.git / blobdiff