X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicParamod.ml;h=16ae66e5da45f76259420625ebd2311247899987;hb=b3f366c0fa3fcadcf5f21913f71a2bce591e47d0;hp=5b3e6148b99d4519ef0446941a35a10882a90f7a;hpb=e22808c929a9cebf5e4e2b7428ff0cbf89e1f92a;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 5b3e6148b..16ae66e5d 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))); *)
 (*
@@ -115,12 +115,25 @@ let index_obj s uri =
   debug (lazy ("indexing : " ^ (NUri.string_of_uri uri)));
   debug (lazy ("no : " ^ (string_of_int (fst (Obj.magic uri)))));
   match obj with
+    | (_,_,[],[],NCic.Constant(_,_,None,ty,_)) ->
+        let nref = NReference.reference_of_spec uri NReference.Decl in
+	forward_infer_step s (NCic.Const nref) ty
     | (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) ->
         let nref = NReference.reference_of_spec uri (NReference.Def d) in
 	forward_infer_step s (NCic.Const nref) ty
     | _ -> 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