Merge pull request #527 from ontologyportal/Rose_5-26-26

Fixed a Hardcoded Predicate Arity Conditional in SUMOKBtoTFAKB

Author: apease

src/java/com/articulate/sigma/tp/TheoremProverController.java

@@ -21,6 +21,7 @@ portions copyright Teknowledge (c) 2003 and reused under the terms of the GNU li
 import com.articulate.sigma.tp.ATPQuery.RunSource;
 import com.articulate.sigma.tp.ATPQuery.TptpLanguage;
 import com.articulate.sigma.trans.TPTP3ProofProcessor;
+import com.articulate.sigma.trans.TPTPGenerationManager;
 import com.articulate.sigma.parsing.CLIMapParser;
 
 import java.util.ArrayList;
@@ -38,7 +39,8 @@ public TheoremProverController () {}
      * @param query ATPQuery object used to determine which prover to ask with associated options.
      */
     public ATPResult ask (ATPQuery query) {
-
+        
+        TPTPGenerationManager.waitForAllTPTP(600);
         switch (query.getProverType()) {
             case EPROVER:
                 return this.askEProver(query);

src/java/com/articulate/sigma/tp/Vampire.java

@@ -21,7 +21,6 @@ portions copyright Teknowledge (c) 2003 and reused under the terms of the GNU li
 import com.articulate.sigma.trans.SessionTPTPManager;
 import com.articulate.sigma.trans.THFnew;
 import com.articulate.sigma.trans.TPTP3ProofProcessor;
-import com.articulate.sigma.trans.TPTPGenerationManager;
 import com.articulate.sigma.trans.TPTPutil;
 import com.articulate.sigma.utils.FileUtil;
 import com.articulate.sigma.utils.StringUtil;
@@ -182,13 +181,6 @@ else if ("tff".equalsIgnoreCase(requestedTptpLang)){
         this.timeout = timeout;
         this.maxAnswers = maxAnswers;
         this.inferenceFilePath = KBmanager.getMgr().getPref("kbDir") + File.separator + KBmanager.getMgr().getPref("sumokbname") + "." + this.inferenceFileExtension;
-        if (!(new File(this.inferenceFilePath).exists()) || KBmanager.getMgr().infBaseFileOldIgnoringUserAssertions(this.inferenceFileExtension)) {
-            System.out.println("INFO in KB.loadVampire(): this.inferenceFilePath=" + !(new File(this.inferenceFilePath).exists()));
-            System.out.println("INFO in KB.loadVampire(): managerInfFileOld " + KBmanager.getMgr().infFileOld());
-            synchronized (kb.baseGenLock) {
-                TPTPGenerationManager.generateProperFile(kb, this.requestedTptpLanguage);
-            }
-        }
     }
 
     /***************************************************************
@@ -379,18 +371,6 @@ public void askVampireHOL(String stmt, boolean useModals) {
             File thfAxioms = new File(kbThfPath);
             if (!thfAxioms.exists()) {
                 System.out.println("Vampire.askVampireHOL(): no such file: " + kbThfPath + ". Waiting for background generation or creating it.");
-                // Wait for background THF generation if in progress, otherwise generate synchronously
-                if (useModals) {
-                    if (!TPTPGenerationManager.waitForTHFModal(600)) {
-                        System.out.println("Vampire.askVampireHOL(): Background generation not ready, generating THF Modal synchronously");
-                        THFnew.transModalTHF(this.kb);
-                    }
-                } else {
-                    if (!TPTPGenerationManager.waitForTHFPlain(600)) {
-                        System.out.println("Vampire.askVampireHOL(): Background generation not ready, generating THF Plain synchronously");
-                        THFnew.transPlainTHF(this.kb);
-                    }
-                }
             }
             // -------- 2. Prepare temp-stmt.thf and temp-comb.thf (mirrors FOF/TFF run() pattern) --------
             String stmtFile = dir + "temp-stmt." + this.inferenceFileExtension;

src/java/com/articulate/sigma/trans/SUMOKBtoTFAKB.java

@@ -314,7 +314,7 @@ public void writeRelationSort(String t, PrintWriter pw) {
         int endIndex = sig.size();
         if (KButilities.isVariableArity(kb,SUMOtoTFAform.withoutSuffix(t)))
             endIndex = getVariableAritySuffix(t) + 1;
-        if (endIndex > 9) {
+        if (endIndex > Formula.MAX_PREDICATE_ARITY) {
             pw.println("% SUMOKBtoTFAKB.writeRelationSort(): size too large: " + t);
             return;
         }

src/java/com/articulate/sigma/trans/TPTPGenerationManager.java

@@ -19,6 +19,7 @@ Manages background generation of TPTP translation files (FOF, TFF, THF).
 import java.io.*;
 import java.nio.charset.StandardCharsets;
 import java.nio.file.*;
+import java.util.Date;
 import java.util.HashMap;
 import java.util.concurrent.*;
 import java.util.concurrent.atomic.AtomicBoolean;
@@ -61,7 +62,6 @@ public static void setSkipBackgroundGeneration(boolean skip) {
         skipBackgroundGeneration.set(skip);
     }
 
-
     /*********************************************************************************
      * Start background generation of all TPTP formats for all KBs.
      * This should be called after KBmanager initialization is complete.
@@ -373,6 +373,15 @@ private static void generateTHFPlain(KB kb) {
         }
     }
 
+    /*********************************************************************************
+     * Wait for all TPTP generation to complete.
+     * @param timeoutSec Maximum time to wait in seconds
+     * @return true if generation completed successfully, false if timed out
+     */
+    public static boolean waitForAllTPTP(int timeoutSec) {
+        return waitForFOF(timeoutSec) && waitForTFF(timeoutSec) && waitForTHFModal(timeoutSec) && waitForTHFPlain(timeoutSec);
+    }
+
     /*********************************************************************************
      * Wait for FOF generation to complete.
      * @param timeoutSec Maximum time to wait in seconds