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 df6f949b603c867128b5d31634cf72091199ab9e..c5290694bfd96a4c5179b70eaeb665d8a742d3d7 100644 (file)
--- 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 7fc13b504290aebbf11bbcfbf5032131ce60ad7d..86a964c1487f36a7f72deb0c8f2608f621ec2aac 100644 (file)
--- 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 c5bb640a2ba8bdb5c532f7bcf89a3686c0c29fa9..42cf063b64f08b3e352693d7a30bebff78025e95 100644 (file)
--- 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]