From: Andrea Asperti Date: Thu, 18 Mar 2010 11:22:11 +0000 (+0000) Subject: Exporting the demodulation function. X-Git-Tag: make_still_working~2993 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8c678be0b7ee11a60f21b002553cc414f1d18267;p=helm.git Exporting the demodulation function. --- diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 5b3e6148b..0fff20b4f 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -25,14 +25,14 @@ module B(C : NCicBlob.NCicContext): Orderings.Blob module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C)) -let readback rdb metasenv subst context (bag,i,fo_subst,l) = +let readback ?(demod=false) 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,prooftype = NCicProof.mk_proof bag i fo_subst l in + let proofterm,prooftype = NCicProof.mk_proof ~demod bag i fo_subst l in (* debug (lazy (Printf.sprintf "Got proof term in %fs" (Unix.gettimeofday() -. stamp))); *) (* @@ -121,6 +121,16 @@ let index_obj s uri = | _ -> s ;; +let demod rdb metasenv subst context s goal = + (* let stamp = Unix.gettimeofday () in *) + match P.demod 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 ~demod:true rdb metasenv subst context) solutions +;; + let paramod rdb metasenv subst context s goal = (* let stamp = Unix.gettimeofday () in *) match P.nparamod ~useage:true ~max_steps:max_int diff --git a/helm/software/components/ng_paramodulation/nCicParamod.mli b/helm/software/components/ng_paramodulation/nCicParamod.mli index 3c813a075..96eeb71ae 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.mli +++ b/helm/software/components/ng_paramodulation/nCicParamod.mli @@ -35,3 +35,9 @@ val fast_eq_check : state -> (NCic.term * NCic.term) -> (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list +val demod : + #NRstatus.status -> + NCic.metasenv -> NCic.substitution -> NCic.context -> + state -> + (NCic.term * NCic.term) -> + (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index b5f4af9d6..781b6bf08 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -218,7 +218,8 @@ let debug c _ = c;; in aux ft (List.rev pl) ;; - let mk_proof (bag : NCic.term Terms.bag) mp subst steps = + (* we should better split forward and backard rewriting *) + let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps = let module NCicBlob = NCicBlob.NCicBlob( struct @@ -271,7 +272,9 @@ let debug c _ = c;; 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 + let refl = + if demod then NCic.Implicit `Term + else mk_refl eq_ty in (* prerr_endline ("Reached m point, id=" ^ (string_of_int id)); (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl, aux true ((id,([],lit))::seen) (id::tl))) *) diff --git a/helm/software/components/ng_paramodulation/nCicProof.mli b/helm/software/components/ng_paramodulation/nCicProof.mli index 1ba93353b..2aa0a8dd8 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.mli +++ b/helm/software/components/ng_paramodulation/nCicProof.mli @@ -18,7 +18,8 @@ val set_default_sig: unit -> unit val get_sig: eq_sig_type -> NCic.term val mk_proof: - NCic.term Terms.bag + ?demod:bool + -> NCic.term Terms.bag -> Terms.M.key -> NCic.term Terms.substitution -> Terms.M.key list diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 8abdaaec5..4b9d29e1c 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -13,7 +13,7 @@ let print s = prerr_endline (Lazy.force s) ;; let noprint s = ();; -let debug = noprint;; +let debug = print;; let monster = 100;; @@ -52,6 +52,8 @@ module type Paramod = bag -> g_passives:t Terms.unit_clause list -> passives:t Terms.unit_clause list -> szsontology + val demod : + state -> input* input -> szsontology val fast_eq_check : state -> input* input -> szsontology val nparamod : @@ -554,6 +556,14 @@ module Paramod (B : Orderings.Blob) = struct | Stop o -> o ;; +let demod s goal = + let bag,maxvar,actives,passives,g_actives,g_passives = s in + let (bag,maxvar), g = mk_goal (bag,maxvar) goal in + if Terms.is_eq_clause g then + let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in + if g1 = g then GaveUp else compute_result bag i [] + else GaveUp + let fast_eq_check s goal = let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in if is_passive_g_set_empty g_passives then Error "not an equation" diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index 1142b03c7..367d79394 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -46,6 +46,8 @@ module type Paramod = bag -> g_passives:t Terms.unit_clause list -> passives:t Terms.unit_clause list -> szsontology + val demod : + state -> input* input -> szsontology val fast_eq_check : state -> input* input -> szsontology val nparamod :