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
- | Terms.Var i as t ->
+ let bag,subst,t,id = f bag t pos ctx id in
+ assert (subst=[]); bag,t,id
+ | Terms.Var _ as t ->
let t= Subst.apply_subst subst t in
bag,t,id
| Terms.Node (hd::l) ->
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)
+ (* CSC: to avoid equations of the form ? -> T that
+ can always be applied and that lead to type-checking errors *)
+ (match l,r,o with
+(*
+ (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,Terms.Gt
+ | _,(Terms.Var _ | Terms.Node (Terms.Var _ ::_)),Terms.Lt -> assert false
+*)
+ | (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,(Terms.Incomparable | Terms.Invertible) ->
+ Terms.Equation (l, r, ty, Terms.Lt)
+ | _, (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),(Terms.Incomparable | Terms.Invertible) ->
+ Terms.Equation (l, r, ty, Terms.Gt)
+ | _ -> Terms.Equation (l, r, ty, o))
| t -> Terms.Predicate t
in
let bag, uc =
(IDX.DT.retrieve_generalizations table) subterm
in
list_first
- (fun (dir, (id,lit,vl,_)) ->
+ (fun (dir, (id,lit,_vl,_)) ->
match lit with
| Terms.Predicate _ -> assert false
| Terms.Equation (l,r,_,o) ->
(IDX.DT.retrieve_generalizations table) subterm
in
list_first
- (fun (dir, ((id,lit,vl,_) as c)) ->
+ (fun (dir, ((id,lit,_vl,_) as c)) ->
debug (lazy("candidate: "
^ Pp.pp_unit_clause c));
match lit with
(bag,subst,newside,id)
;;
- let rec demodulate bag (id, literal, vl, pr) table =
+ let demodulate bag (id, literal, vl, _pr) table =
debug (lazy ("demodulate " ^ (string_of_int id)));
match literal with
| Terms.Predicate t -> (* assert false *)
let is_identity_goal = function
| _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> Some []
- | _, Terms.Equation (l,r,_,_), vl, proof ->
+ | _, Terms.Equation (l,r,_,_), _vl, _proof ->
(try Some (Unif.unification (* vl *) [] l r)
with FoUnif.UnificationFailure _ -> None)
| _, Terms.Predicate _, _, _ -> assert 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
+ | (d, (id,Terms.Equation (l,r,_ty,_),vl,_))-> id, d, l, r, vl
|_ -> assert false
in
let reverse = (dir = Terms.Left2Right) = b in
| [] -> 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) ->
+ | 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])
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 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,_,_,_)),true,_ -> (true,acc)
| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false,_ ->
if (List.mem i acc) then (false,acc)
else match orphan_murder bag acc i1 with
match simplify ctable maxvar bag c with
|bag,None -> (bag,alist,atable)
(* an active clause as been discarded *)
- |bag,Some c1 ->
+ |bag,Some _c1 ->
bag, c :: alist, IDX.index_unit_clause atable c)
(bag,[],IDX.DT.empty) alist
in
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
else match (is_identity_goal clause) with
| Some subst -> raise (Success (bag,maxvar,clause,subst))
| None ->
- let (id,lit,vl,_) = clause in
+ let (_id,lit,vl,_) = clause in
(* this optimization makes sense only if we demodulated, since in
that case the clause should have been turned into an identity *)
if (vl = [] && not(no_demod))
| 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))
*)
;;
(* =================== inference ===================== *)
(* this is OK for both the sup_left and sup_right inference steps *)
- let superposition table varlist subterm pos context =
+ 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*))) ->
+ (fun (dir, (id,lit,_vl,_ (*as uc*))) ->
match lit with
| Terms.Predicate _ -> assert false
| Terms.Equation (l,r,_,o) ->
projects / helm.git / blobdiff