Moved compare in a different file.

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 8abdaaec509301e7ef7cae20300601925d9739f0..de32ab5ddf8b7e0fe1b8984ed4bdad4e4d4c3970 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -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"