Exporting the demodulation function.

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 5b3e6148b99d4519ef0446941a35a10882a90f7a..0fff20b4f262badef61d0af0404b5069a83fece1 100644 (file)
--- 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 3c813a075f7eb4d8d276eed85ecdbddade6ceca0..96eeb71aeda6d8eb2fbfb13e8c1fc017c044702e 100644 (file)
--- 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 b5f4af9d6f8ede74f3a1508207fba88da6257950..781b6bf08316b42efbff3365fe47c3eb8a919333 100644 (file)
--- 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 1ba93353b4f646abe3069aff5deac5c661c219c2..2aa0a8dd81ef565a9ae2109b8e8ba7c001b3f0c1 100644 (file)
--- 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 8abdaaec509301e7ef7cae20300601925d9739f0..4b9d29e1c59ee780ebc8631a6869d2ad0ebe3500 100644 (file)
--- 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 1142b03c7ea47cc451abd48bcdfecc5f5e4a4266..367d7939448f269ebedd755cb688cbc887155c9c 100644 (file)
--- 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 :