Update + fix TPTP problem parser

Author: augustepoiroux

.gitignore

@@ -25,3 +25,6 @@ cache
 
 # data extracted
 data_extract
+
+# TPTP data
+lisa-utils/src/main/resources

lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala

@@ -10,6 +10,7 @@ import lisa.utils.KernelHelpers.*
 import lisa.utils.KernelHelpers.given_Conversion_Identifier_String
 import lisa.utils.KernelHelpers.given_Conversion_String_Identifier
 import lisa.utils.tptp.*
+import lisa.kernel.fol.FOL.*
 
 import java.io.File
 import scala.util.matching.Regex
@@ -26,13 +27,15 @@ object KernelParser {
    */
   def parseToKernel(formula: String): K.Formula = convertToKernel(Parser.fof(formula))
 
+  def cleanVarname(f: String): String = f.replaceAll(Identifier.counterSeparator.toString, "")
+
   /**
    * @param formula a tptp formula in leo parser
    * @return the same formula in LISA
    */
   def convertToKernel(formula: FOF.Formula): K.Formula = {
     formula match {
-      case FOF.AtomicFormula(f, args) => K.AtomicFormula(K.ConstantAtomicLabel(f, args.size), args map convertTermToKernel)
+      case FOF.AtomicFormula(f, args) => K.AtomicFormula(K.ConstantAtomicLabel(cleanVarname(f), args.size), args map convertTermToKernel)
       case FOF.QuantifiedFormula(quantifier, variableList, body) =>
         quantifier match {
           case FOF.! => variableList.foldRight(convertToKernel(body))((s, f) => K.Forall(K.VariableLabel(s), f))
@@ -63,8 +66,8 @@ object KernelParser {
     K.ConnectorFormula(
       K.Or,
       formula.map {
-        case CNF.PositiveAtomic(formula) => K.AtomicFormula(K.ConstantAtomicLabel(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
-        case CNF.NegativeAtomic(formula) => !K.AtomicFormula(K.ConstantAtomicLabel(formula.f, formula.args.size), formula.args.map(convertTermToKernel).toList)
+        case CNF.PositiveAtomic(formula) => K.AtomicFormula(K.ConstantAtomicLabel(cleanVarname(formula.f), formula.args.size), formula.args.map(convertTermToKernel).toList)
+        case CNF.NegativeAtomic(formula) => !K.AtomicFormula(K.ConstantAtomicLabel(cleanVarname(formula.f), formula.args.size), formula.args.map(convertTermToKernel).toList)
         case CNF.Equality(left, right) => K.equality(convertTermToKernel(left), convertTermToKernel(right))
         case CNF.Inequality(left, right) => !K.equality(convertTermToKernel(left), convertTermToKernel(right))
       }
@@ -76,7 +79,7 @@ object KernelParser {
    * @return the same term in LISA
    */
   def convertTermToKernel(term: CNF.Term): K.Term = term match {
-    case CNF.AtomicTerm(f, args) => K.Term(K.ConstantFunctionLabel(f, args.size), args map convertTermToKernel)
+    case CNF.AtomicTerm(f, args) => K.Term(K.ConstantFunctionLabel(cleanVarname(f), args.size), args map convertTermToKernel)
     case CNF.Variable(name) => K.VariableTerm(K.VariableLabel(name))
     case CNF.DistinctObject(name) => ???
   }
@@ -87,7 +90,7 @@ object KernelParser {
    */
   def convertTermToKernel(term: FOF.Term): K.Term = term match {
     case FOF.AtomicTerm(f, args) =>
-      K.Term(K.ConstantFunctionLabel(f, args.size), args map convertTermToKernel)
+      K.Term(K.ConstantFunctionLabel(cleanVarname(f), args.size), args map convertTermToKernel)
     case FOF.Variable(name) => K.VariableTerm(K.VariableLabel(name))
     case FOF.DistinctObject(name) => ???
     case FOF.NumberTerm(value) => ???
@@ -174,11 +177,15 @@ object KernelParser {
       if (d.isDirectory) {
         if (d.listFiles().isEmpty) println("empty directory")
         d.listFiles.filter(_.isDirectory)
-
       } else throw new Exception("Specified path is not a directory.")
     } else throw new Exception("Specified path does not exist.")
 
-    probfiles.map(d => gatherFormulas(spc, d.getPath)).toSeq
+    probfiles.zipWithIndex
+      .map((d, i) => {
+        println("[ " + (i + 1) + " / " + probfiles.size + " ] Gathering formulas from " + d.getName())
+        gatherFormulas(spc, d.getPath)
+      })
+      .toSeq
   }
 
   def gatherFormulas(spc: Seq[String], path: String): Seq[Problem] = {
@@ -187,14 +194,27 @@ object KernelParser {
       if (d.isDirectory) {
         if (d.listFiles().isEmpty) println("empty directory")
         d.listFiles.filter(_.isFile)
-
       } else throw new Exception("Specified path is not a directory.")
     } else throw new Exception("Specified path does not exist.")
 
-    val r = probfiles.foldRight(List.empty[Problem])((p, current) => {
-      val md = getProblemInfos(p)
-      if (md.spc.exists(spc.contains)) problemToKernel(p, md) :: current
-      else current
+    val r = probfiles.zipWithIndex.foldLeft(List.empty[Problem])((current, p_i) => {
+      val (p, i) = p_i
+
+      // Progress bar
+      if ((i + 1) % 100 == 0 || i + 1 == probfiles.size) {
+        val pbarLength = 30
+        var pbarContent = "=" * (((i + 1) * pbarLength) / probfiles.size)
+        pbarContent += " " * (pbarLength - pbarContent.length)
+        println("\t[" + pbarContent + "] (" + (i + 1) + " / " + probfiles.size + ") " + d.getName())
+      }
+
+      try {
+        val md = getProblemInfos(p)
+        if (md.spc.exists(spc.contains)) current :+ problemToKernel(p, md)
+        else current
+      } catch {
+        case _ => current
+      }
     })
     r
   }