Branched paramodulation for CNF (Horn clauses)

[helm.git] / helm / software / components / tptp_grafite / parser.mly

diff --git a/helm/software/components/tptp_grafite/parser.mly b/helm/software/components/tptp_grafite/parser.mly
index 05577000cf650f214a101af4f2a8a1d23b1e0d1e..0f3525689212de5c2ae37b3a20d91363018f3afd 100644 (file)
--- a/helm/software/components/tptp_grafite/parser.mly
+++ b/helm/software/components/tptp_grafite/parser.mly
@@ -56,7 +56,12 @@
             name COMMA formula_type COMMA formula formula_source_and_infos 
           RPAREN DOT {
             AnnotatedFormula ($3,$5,$7,fst $8,snd $8)  
-      }
+         }
+    | CNF LPAREN
+         TYPE COMMA formula_type COMMA formula formula_source_and_infos
+       RPAREN DOT {
+         AnnotatedFormula ($3,$5,$7,fst $8,snd $8)  
+       }
   ;
   
   formula_type: 
@@ -119,6 +124,11 @@
   atomic_word:
     | LNAME { $1 }
     | QSTRING { rm_q $1 }
+    | TYPE { (* workaround! *)
+      match $1 with 
+      | "theorem" -> "theoremP" 
+      | "axiom" -> "axiomP" 
+      | s -> prerr_endline s;assert false }
   ;
   
   formula_source_and_infos: