From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 25 Mar 2010 08:36:02 +0000 (+0000)
Subject: Extension of demod to arbtrary predicates (not just equalities).
X-Git-Tag: make_still_working~2964
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d3494c5c68a48b663eed55c1ac55f3c8f832820;p=helm.git

Extension of demod to arbtrary predicates (not just equalities).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>
---

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index df6f949b6..c5290694b 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -218,7 +218,6 @@ let debug c _ = c;;
     in aux ft (List.rev pl)
     ;;
 
-  (* we should better split forward and backward rewriting *)
   let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps =
     let module NCicBlob = 
        NCicBlob.NCicBlob(
@@ -254,7 +253,7 @@ let debug c _ = c;;
     let get_literal id =
       let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
       let lit =match lit with 
-          | Terms.Predicate t -> assert false 
+          | Terms.Predicate t -> t (* assert false *) 
           | Terms.Equation (l,r,ty,_) -> 
               Terms.Node [ Terms.Leaf eqP(); ty; l; r]
       in
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 7fc13b504..86a964c14 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -567,10 +567,12 @@ module Paramod (B : Orderings.Blob) = struct
 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
+  let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
+    if g1 = g then GaveUp else compute_result bag i []
+(*
   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
+
+  else GaveUp *)
 
 let fast_eq_check s goal =
   let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index c5bb640a2..42cf063b6 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -272,7 +272,12 @@ module Superposition (B : Orderings.Blob) =
     let rec demodulate bag (id, literal, vl, pr) table =
       debug (lazy ("demodulate " ^ (string_of_int id)));
        match literal with
-      | Terms.Predicate t -> assert false
+      | Terms.Predicate t -> (* assert false *)
+	  let bag,_,id1 =
+	    visit bag [] (fun x -> x) id t (ctx_demod table vl)
+	  in          
+	  let cl,_,_ = Terms.get_from_bag id1 bag in
+	    bag,cl
       | Terms.Equation (l,r,ty,_) ->
           let bag,l,id1 = 
 	    visit bag [2]