Fix equality infix printing + parsing issues

Author: augustepoiroux

lisa-examples/src/main/scala/TPTPSolver.scala

@@ -19,26 +19,26 @@ object TPTPSolver extends lisa.Main {
 
   class ProblemSolverResults(val problem: Problem, val solverName: String, val solverStatus: String, val proofCode: String, val proofType: ProofType)
 
+  val spc = Seq("PRP", "FOF") // type of problems we want to extract and solve
+  // val spc = Seq("CNF") // almost no CNF problems are solved by Tableau, TODO: investigate why
+
+  // We limit the execution time to solve each problem
+  val timeoutTableau = .1.second
+  val timeoutTautology = .1.second
+
   val exportOnlySolvedProblems = true
   val exportOptimizedProofs = true
   val exportBySolverProofs = true
 
   val jsonResultsPath: String = "/home/auguste/Documents/EPFL/PhD/Projects/lisa/lisa-examples/src/main/resources/TPTPResults.json"
   val TPTPProblemPath: String = "/home/auguste/Documents/EPFL/PhD/Projects/TPTP-v8.2.0/Problems/"
 
-  val spc = Seq("PRP", "FOF") // type of problems we want to extract and solve
-  // val spc = Seq("CNF") // almost no CNF problems are solved by Tableau, TODO: investigate why
-
-  // val d = new File(TPTPProblemPath)
-  // val libraries = d.listFiles.filter(_.isDirectory)
-  // val probfiles = libraries.flatMap(_.listFiles).filter(_.isFile)
-
-  val d = new File(TPTPProblemPath + "SYN/")
-  val probfiles = d.listFiles.filter(_.isFile)
+  val d = new File(TPTPProblemPath)
+  val libraries = d.listFiles.filter(_.isDirectory)
+  val probfiles = libraries.flatMap(_.listFiles).filter(_.isFile)
 
-  // We limit the execution time to solve each problem
-  val timeoutTableau = .1.second
-  val timeoutTautology = .1.second
+  // val d = new File(TPTPProblemPath + "SYN/")
+  // val probfiles = d.listFiles.filter(_.isFile)
 
   var nbProblemsExtracted = 0
   var nbProblemsSolved = Map("Tableau" -> 0, "Tautology" -> 0)
@@ -120,8 +120,8 @@ object TPTPSolver extends lisa.Main {
         "problemFile" -> r.problem.file,
         "solver" -> r.solverName,
         "solverStatus" -> r.solverStatus,
-        "solverProofCode" -> r.proofCode,
-        "proofType" -> r.proofType.getClass.getSimpleName.stripSuffix("$")
+        "proofType" -> r.proofType.getClass.getSimpleName.stripSuffix("$"),
+        "solverProofCode" -> r.proofCode
       )
     ),
     jsonWriter,

lisa-utils/src/main/scala/lisa/fol/Common.scala

@@ -610,7 +610,8 @@ trait Common {
     def rename(newid: Identifier): ConstantPredicateLabel[N] = ConstantPredicateLabel(newid, arity)
     def freshRename(taken: Iterable[Identifier]): ConstantPredicateLabel[N] = rename(K.freshId(taken, id))
     override def toString(): String = id
-    def mkString(args: Seq[Term]): String = if (infix) (args(0).toStringSeparated() + " " + toString() + " " + args(1).toStringSeparated()) else toString() + "(" + args.mkString(", ") + ")"
+    def mkString(args: Seq[Term]): String =
+      if (infix) ("(" + args(0).toStringSeparated() + " " + toString() + " " + args(1).toStringSeparated() + ")") else toString() + "(" + args.mkString(", ") + ")"
     override def mkStringSeparated(args: Seq[Term]): String = if (infix) "(" + mkString(args) + ")" else mkString(args)
   }
   object ConstantPredicateLabel {

lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala

@@ -84,7 +84,11 @@ object FOLHelpers {
     case cl: K.SchematicConnectorLabel => asFrontLabel(cl)
   def asFrontLabel[N <: Arity](cpl: K.ConstantAtomicLabel): ConstantAtomicLabelOfArity[N] = cpl.arity.asInstanceOf[N] match
     case n: 0 => ConstantFormula(cpl.id)
-    case n: N => ConstantPredicateLabel(cpl.id, cpl.arity.asInstanceOf)
+    case n: N =>
+      if (cpl.id == Identifier("="))
+        ConstantPredicateLabel.infix("===", cpl.arity.asInstanceOf)
+      else
+        ConstantPredicateLabel(cpl.id, cpl.arity.asInstanceOf)
   def asFrontLabel(sfl: K.SchematicFormulaLabel): SchematicAtomicLabel[?] | SchematicConnectorLabel[?] =
     sfl match
       case v: K.VariableFormulaLabel => asFrontLabel(v)

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

@@ -27,7 +27,10 @@ object KernelParser {
    */
   def parseToKernel(formula: String): K.Formula = convertToKernel(Parser.fof(formula))
 
-  def cleanVarname(f: String): String = f.replaceAll(Identifier.counterSeparator.toString, "")
+  def cleanVarname(f: String): String =
+    val forbiddenChars = Identifier.forbiddenChars ++ Set('\\', '/', '\'', '"', '`', '.', ',', ';', ':', '!', '%', '^', '&', '*', '|', '-', '+', '=', '<', '>', '~', '@', '#')
+    // replace all the forbidden chars + whitespaces by '0'
+    f.map(c => if (forbiddenChars.contains(c) || c.isWhitespace) then '0' else c)
 
   /**
    * @param formula a tptp formula in leo parser
@@ -96,7 +99,7 @@ object KernelParser {
         else K.SchematicFunctionLabel(cleanVarname(f), args.size),
         args map convertTermToKernel
       )
-    case CNF.Variable(name) => K.VariableTerm(K.VariableLabel(name))
+    case CNF.Variable(name) => K.VariableTerm(K.VariableLabel(cleanVarname(name)))
     case CNF.DistinctObject(name) => ???
   }
 
@@ -111,7 +114,7 @@ object KernelParser {
         else K.SchematicFunctionLabel(cleanVarname(f), args.size),
         args map convertTermToKernel
       )
-    case FOF.Variable(name) => K.VariableTerm(K.VariableLabel(name))
+    case FOF.Variable(name) => K.VariableTerm(K.VariableLabel(cleanVarname(name)))
     case FOF.DistinctObject(name) => ???
     case FOF.NumberTerm(value) => ???
   }
@@ -171,7 +174,7 @@ object KernelParser {
     if (problem.spc.contains("CNF")) problem.formulas.map(_.formula) |- ()
     else
       problem.formulas.foldLeft[LK.Sequent](() |- ())((s, f) =>
-        if (f._1 == "axiom") s +<< f._3
+        if (Set("axiom", "hypothesis", "lemma").contains(f._1)) s +<< f._3
         else if (f._1 == "conjecture" && s.right.isEmpty) s +>> f._3
         else throw Exception("Can only agglomerate axioms and one conjecture into a sequents")
       )