From: Andrea Asperti Date: Fri, 18 Dec 2009 08:53:10 +0000 (+0000) Subject: Final subst returned by superposition and passed around. X-Git-Tag: make_still_working~3162 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dce1bca274f93a3bddcc0f6b04cbf126ccff42b0;p=helm.git Final subst returned by superposition and passed around. --- diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index 7b57e5bb3..1dfdbc57c 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -28,7 +28,7 @@ module Utils (B : Orderings.Blob) = struct let rec eq_foterm x y = x == y || match x, y with - | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2 + | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2 | Terms.Var i, Terms.Var j -> i = j | Terms.Node l1, Terms.Node l2 -> List.for_all2 eq_foterm l1 l2 | _ -> false diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 78a57faa2..fb60d3142 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -17,7 +17,7 @@ NCicProof.set_default_sig() ;; let debug _ = ();; -(* let debug s = prerr_endline (Lazy.force s);; *) +let print s = prerr_endline (Lazy.force s);; module B(C : NCicBlob.NCicContext): Orderings.Blob with type t = NCic.term and type input = NCic.term @@ -25,15 +25,15 @@ module B(C : NCicBlob.NCicContext): Orderings.Blob module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C)) -let readback rdb metasenv subst context (bag,i,l) = +let readback rdb metasenv subst context (bag,i,fo_subst,l) = (* List.iter (fun x -> print_endline (Pp.pp_unit_clause ~margin:max_int (fst(Terms.M.find x bag)))) l; *) let stamp = Unix.gettimeofday () in - let proofterm = NCicProof.mk_proof bag i l in - debug (lazy (Printf.sprintf "Got proof term in %fs" + let proofterm = NCicProof.mk_proof bag i fo_subst l in + print (lazy (Printf.sprintf "Got proof term in %fs" (Unix.gettimeofday() -. stamp))); let metasenv, proofterm = let rec aux k metasenv = function @@ -48,13 +48,15 @@ let readback rdb metasenv subst context (bag,i,l) = in aux 0 metasenv proofterm in - debug (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm)); + print (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm)); + let stamp = Unix.gettimeofday () in let metasenv, subst, proofterm, _prooftype = NCicRefiner.typeof (rdb#set_coerc_db NCicCoercion.empty_db) metasenv subst context proofterm None in - debug (lazy "refined!"); + print (lazy (Printf.sprintf "Refined in %fs" + (Unix.gettimeofday() -. stamp))); proofterm, metasenv, subst let nparamod rdb metasenv subst context t table = @@ -113,9 +115,12 @@ let index_obj s uri = ;; let fast_eq_check rdb metasenv subst context s goal = + let stamp = Unix.gettimeofday () in match P.fast_eq_check s goal with | P.Error _ | P.GaveUp | P.Timeout _ -> [] | P.Unsatisfiable solutions -> + print (lazy (Printf.sprintf "Got solutions in %fs" + (Unix.gettimeofday() -. stamp))); List.map (readback rdb metasenv subst context) solutions ;; diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index 59d7e95ff..65c0b1613 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -14,9 +14,8 @@ type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl let eqsig = ref (fun _ -> assert false);; -let set_sig f = eqsig:= -f;; - +let set_sig f = eqsig:= f;; +let get_sig = fun x -> !eqsig x;; let default_sig = function | Eq -> @@ -66,12 +65,13 @@ let set_reference_of_oxuri reference_of_oxuri = in eqsig:= nsig ;; -let debug c r = prerr_endline r; c +(* let debug c r = prerr_endline r; c *) +let debug c _ = c;; - let eqP() = prerr_endline "1"; prerr_endline "1"; debug (!eqsig Eq) "eqp" ;; - let eq_ind() = prerr_endline "2"; debug (!eqsig EqInd_l) "eq_ind" ;; - let eq_ind_r() = prerr_endline "3"; debug (!eqsig EqInd_r) "eq_ind_r";; - let eq_refl() = prerr_endline "4"; debug (!eqsig Refl) "refl";; + let eqP() = debug (!eqsig Eq) "eqp" ;; + let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;; + let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";; + let eq_refl() = debug (!eqsig Refl) "refl";; let extract lift vl t = @@ -122,7 +122,7 @@ let debug c r = prerr_endline r; c NCic.Lambda("x", hole_type, aux ft (List.rev p1)) ;; - let mk_proof (bag : NCic.term Terms.bag) mp steps = + let mk_proof (bag : NCic.term Terms.bag) mp subst steps = let module Subst = FoSubst in let position i l = let rec aux = function @@ -155,16 +155,22 @@ let debug c r = prerr_endline r; c in lit, vl, proof in + let mk_refl = function + | NCic.Appl [_; ty; l; _] + -> NCic.Appl [eq_refl();ty;l] + | _ -> assert false + in let rec aux ongoal seen = function | [] -> NCic.Rel 1 | id :: tl -> let amount = List.length seen in let lit,vl,proof = get_literal id in if not ongoal && id = mp then + let lit = Subst.apply_subst subst lit in + let eq_ty = extract amount [] lit in + let refl = mk_refl eq_ty in ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*) - NCic.LetIn ("clause_" ^ string_of_int id, - extract amount [] lit, - (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]), + NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl, aux true ((id,([],lit))::seen) (id::tl))) else match proof with diff --git a/helm/software/components/ng_paramodulation/nCicProof.mli b/helm/software/components/ng_paramodulation/nCicProof.mli index 0c65b5793..4383b2928 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.mli +++ b/helm/software/components/ng_paramodulation/nCicProof.mli @@ -11,7 +11,15 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) +type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl + val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit val set_default_sig: unit -> unit +val get_sig: eq_sig_type -> NCic.term -val mk_proof:NCic.term Terms.bag -> Terms.M.key -> Terms.M.key list -> NCic.term +val mk_proof: + NCic.term Terms.bag + -> Terms.M.key + -> NCic.term Terms.substitution + -> Terms.M.key list + -> NCic.term diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index b06d8a654..a3fd41e21 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -11,7 +11,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -(* let debug s = prerr_endline (Lazy.force s) ;; *) +(* let debug s = prerr_endline (Lazy.force s) ;; *) let debug _ = ();; let monster = 100;; @@ -21,7 +21,8 @@ module type Paramod = type t type input type szsontology = - | Unsatisfiable of (t Terms.bag * int * int list) list + | Unsatisfiable of + (t Terms.bag * int * t Terms.substitution * int list) list | GaveUp | Error of string | Timeout of int * t Terms.bag @@ -80,7 +81,8 @@ module Paramod (B : Orderings.Blob) = struct type input = B.input type bag = B.t Terms.bag * int type szsontology = - | Unsatisfiable of (B.t Terms.bag * int * int list) list + | Unsatisfiable of + (B.t Terms.bag * int * B.t Terms.substitution * int list) list | GaveUp | Error of string | Timeout of int * B.t Terms.bag @@ -460,7 +462,7 @@ module Paramod (B : Orderings.Blob) = struct in goal_narrowing iterno max_steps timeout newstatus - let compute_result bag i = + let compute_result bag i subst = let l = let rec traverse ongoal (accg,acce) i = match Terms.get_from_bag i bag with @@ -503,7 +505,7 @@ module Paramod (B : Orderings.Blob) = struct (fun x -> let cl,_,_ = Terms.get_from_bag x bag in Pp.pp_unit_clause cl) l)))); - Unsatisfiable [ bag, i, l ] + Unsatisfiable [ bag, i, subst, l ] let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = let _initial_timestamp = Unix.gettimeofday () in @@ -519,8 +521,8 @@ 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,_,_,_)) -> - compute_result bag i + | Sup.Success (bag, _, (i,_,_,_),subst) -> + compute_result bag i subst | Stop (Unsatisfiable _) -> Error "solution found!" | Stop o -> o ;; @@ -532,8 +534,8 @@ let fast_eq_check s goal = try goal_narrowing 0 2 None s with - | Sup.Success (bag, _, (i,_,_,_)) -> - compute_result bag i + | Sup.Success (bag, _, (i,_,_,_),subst) -> + compute_result bag i subst | Stop (Unsatisfiable _) -> Error "solution found!" | Stop o -> o ;; diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index b161ae459..321d0f897 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -17,7 +17,8 @@ module type Paramod = type input type state type szsontology = - | Unsatisfiable of (t Terms.bag * int * int list) list + | Unsatisfiable of + (t Terms.bag * int * t Terms.substitution * int list) list | GaveUp | Error of string | Timeout of int * t Terms.bag diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 585fbe237..6f1fb0f7f 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -20,7 +20,11 @@ module Superposition (B : Orderings.Blob) = module Utils = FoUtils.Utils(B) module Pp = Pp.Pp(B) - exception Success of B.t Terms.bag * int * B.t Terms.unit_clause + exception Success of + B.t Terms.bag + * int + * B.t Terms.unit_clause + * B.t Terms.substitution (* let debug s = prerr_endline (Lazy.force s);; *) let debug _ = ();; @@ -311,15 +315,21 @@ module Superposition (B : Orderings.Blob) = ;; (* move away *) - let is_identity_clause ~unify = function + let is_identity_clause = function | _, 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 ;; + let is_identity_goal = function + | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> Some [] + | _, Terms.Equation (l,r,_,_), vl, proof -> + (try Some (Unif.unification (* vl *) [] l r) + with FoUnif.UnificationFailure _ -> None) + | _, Terms.Equation (_,_,_,_), _, _ -> None + | _, Terms.Predicate _, _, _ -> assert false + ;; + let build_new_clause bag maxvar filter rule t subst id id2 pos dir = let maxvar, _vl, subst = Utils.relocate maxvar (Terms.vars_of_term (Subst.apply_subst subst t)) subst in @@ -475,10 +485,10 @@ module Superposition (B : Orderings.Blob) = (* demodulate and check for subsumption *) let simplify table maxvar bag clause = debug (lazy "simplify..."); - if is_identity_clause ~unify:false clause then bag,None + if is_identity_clause clause then bag,None (* else if orphan_murder bag actives clause then bag,None *) else let bag, clause = demodulate bag clause table in - if is_identity_clause ~unify:false clause then bag,None + if is_identity_clause clause then bag,None else match is_subsumed ~unify:false bag maxvar clause table with | None -> bag, Some clause @@ -608,9 +618,9 @@ module Superposition (B : Orderings.Blob) = if no_demod then bag, clause else demodulate bag clause table in if List.exists (are_alpha_eq clause) g_actives then None - else if (is_identity_clause ~unify:true clause) - then raise (Success (bag, maxvar, clause)) - else + else match (is_identity_goal clause) with + | Some subst -> raise (Success (bag,maxvar,clause,subst)) + | None -> 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 *) @@ -627,7 +637,7 @@ module Superposition (B : Orderings.Blob) = | None -> Some (bag,clause) | Some (bag,maxvar,cl,subst) -> debug (lazy "Goal subsumed"); - raise (Success (bag,maxvar,cl)) + raise (Success (bag,maxvar,cl,subst)) (* match is_subsumed ~unify:true bag maxvar clause table with | None -> Some (bag, clause) diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index 9bd662b19..c67dbfb07 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -15,7 +15,11 @@ module Superposition (B : Orderings.Blob) : sig (* bag, maxvar, meeting point *) - exception Success of B.t Terms.bag * int * B.t Terms.unit_clause + exception Success of + B.t Terms.bag + * int + * B.t Terms.unit_clause + * B.t Terms.substitution (* The returned active set is the input one + the selected clause *) val infer_right :