Merge pull request #556 from ontologyportal/install_test_7-10-26

Added Editor Querying / Search, Syntax Diagnostics, & EAxFilter Updates

Author: apease

src/java/com/articulate/sigma/Diagnostics.java

@@ -15,6 +15,8 @@
 import com.articulate.sigma.parsing.Expr;
 import com.articulate.sigma.trans.*;
 import com.articulate.sigma.tp.e.*;
+import com.articulate.sigma.editor.ErrRec;
+import com.articulate.sigma.editor.KifFileChecker;
 
 import com.articulate.sigma.utils.FileUtil;
 import com.articulate.sigma.utils.StringUtil;
@@ -93,6 +95,27 @@ public static List<String> termsWithoutRelation(KB kb, String rel, int argnum, c
         return result;
     }
 
+    /**
+     * Parses every constituent and returns only parser errors.
+     */
+    public static Map<String, Set<String>> kifSyntaxErrors(KB kb) {
+
+        Map<String, Set<String>> result = new LinkedHashMap<>();
+        if (kb == null || kb.constituents == null) return result;
+        for (String constituent : kb.constituents) {
+            try {
+                KIF kif = new KIF();
+                kif.readFile(constituent);
+                if (!kif.errorSet.isEmpty()) result.put(constituent, new TreeSet<>(kif.errorSet));
+            }
+            catch (IOException e) {
+                result.put(constituent, Collections.singleton("Could not read constituent: " + e.getMessage()));
+            }
+        }
+
+        return result;
+    }
+
     /** *****************************************************************
      * Return a list of terms that do not have a documentation string.
      */
@@ -246,7 +269,7 @@ private static Map<Formula, Set<String>> formulaeWithTypeViolations(KB kb) {
             KButilities.clearErrors();
             kb.kbCache.errors.clear();
             SUMOtoTFAform.errors.clear();
-            if(result.size() > 20) break;
+            // if(result.size() > 20) break;
         }
         return result;
     }

src/java/com/articulate/sigma/editor/EditorServlet.java

@@ -2,6 +2,12 @@
 
 import com.articulate.sigma.trans.SUMOformulaToTPTPformula;
 import com.articulate.sigma.*;
+import com.articulate.sigma.tp.ATPQuery;
+import com.articulate.sigma.tp.ATPResult;
+import com.articulate.sigma.tp.ProverCrashedException;
+import com.articulate.sigma.tp.ProverTimeoutException;
+import com.articulate.sigma.tp.TheoremProverController;
+
 
 import javax.servlet.*;
 import javax.servlet.http.*;
@@ -70,6 +76,9 @@ protected void doPost(HttpServletRequest req, HttpServletResponse resp) throws I
             case "translatetotptp":
                 handleTranslateToTPTP(req, resp);
                 break;
+            case "query":
+                handleQuery(req, resp);
+                break;
             case "format":
             case "check":
             default:
@@ -296,6 +305,91 @@ private void handleTranslateToTPTP(HttpServletRequest req, HttpServletResponse r
         }
     }
 
+    /**
+     * Run a highlighted SUO-KIF expression as a query without leaving the editor.
+     * The first version intentionally mirrors AskTell's basic Vampire defaults.
+     */
+    private void handleQuery(HttpServletRequest req, HttpServletResponse resp) throws IOException {
+
+        resp.setContentType("application/json; charset=UTF-8");
+        String statement = Optional.ofNullable(req.getParameter("stmt")).orElse("").trim();
+        String kbName = Optional.ofNullable(req.getParameter("kb")).orElse("SUMO").trim();
+        if (kbName.isEmpty()) kbName = "SUMO";
+
+        if (statement.isEmpty()) {
+            resp.setStatus(HttpServletResponse.SC_BAD_REQUEST);
+            writeJson(resp, false, "Highlight a SUO-KIF expression first.", null);
+            return;
+        }
+        if (statement.indexOf('@') >= 0) {
+            resp.setStatus(HttpServletResponse.SC_BAD_REQUEST);
+            writeJson(resp, false, "Row variables (@) are not allowed in queries.", null);
+            return;
+        }
+
+        HttpSession session = req.getSession(false);
+        if (session == null) {
+            resp.setStatus(HttpServletResponse.SC_UNAUTHORIZED);
+            writeJson(resp, false, "Your session has expired. Please log in again.", null);
+            return;
+        }
+
+        try {
+            KBmanager.getMgr().initializeOnce();
+            KB kb = KBmanager.getMgr().getKB(kbName);
+            if (kb == null) {
+                resp.setStatus(HttpServletResponse.SC_BAD_REQUEST);
+                writeJson(resp, false, "Knowledge base not found: " + kbName, null);
+                return;
+            }
+
+            ATPQuery atpQuery = new ATPQuery(
+                    kb,
+                    session.getId(),
+                    statement,
+                    null,
+                    "custom",
+                    "Vampire",
+                    "fof",
+                    "CASC",
+                    false,
+                    false,
+                    false,
+                    false,
+                    30,
+                    1
+            );
+            ATPResult result = new TheoremProverController().ask(atpQuery);
+
+            if (result == null) {
+                writeJson(resp, false, "No result returned by Vampire.", null);
+                return;
+            }
+
+            List<String> stdout = result.getStdout();
+            String proof = stdout == null || stdout.isEmpty()
+                    ? "Vampire completed, but returned no proof output."
+                    : String.join(System.lineSeparator(), stdout);
+            writeJson(resp, true, proof, null);
+        }
+        catch (ProverTimeoutException e) {
+            resp.setStatus(HttpServletResponse.SC_GATEWAY_TIMEOUT);
+            writeJson(resp, false, "Vampire timed out after 30 seconds.", null);
+        }
+        catch (ProverCrashedException e) {
+            resp.setStatus(HttpServletResponse.SC_INTERNAL_SERVER_ERROR);
+            String detail = e.getResult() == null || e.getResult().getStdout() == null
+                    ? ""
+                    : System.lineSeparator() + String.join(System.lineSeparator(), e.getResult().getStdout());
+            writeJson(resp, false, "Vampire crashed." + detail, null);
+        }
+        catch (Exception e) {
+            resp.setStatus(HttpServletResponse.SC_INTERNAL_SERVER_ERROR);
+            writeJson(resp, false, "Unable to run query: " +
+                    (e.getMessage() == null ? e.getClass().getSimpleName() : e.getMessage()), null);
+        }
+    }
+
     private void handleFormatOrCheck(HttpServletRequest req, HttpServletResponse resp)
             throws IOException, ServletException {
 
@@ -622,4 +716,4 @@ private static String stripTqMetaPredicatesForCheck(String text) {
 
         return out.toString();
     }
-}
+}

src/java/com/articulate/sigma/jobscheduler/JobScheduleXML.java

@@ -180,6 +180,13 @@ private Element createJobElement(Document document, Job job) throws IOException
                 appendTextElement(document, jobElement, "filterTimeout", Integer.toString(axJob.getFilterTimeout()));
                 appendTextElement(document, jobElement, "vampireTimeout", Integer.toString(axJob.getVampireTimeout()));
         }
+        else if (job instanceof SInEContradictionJob sineJob) {
+                appendTextElement(document, jobElement, "kbName", sineJob.getKbName());
+                appendTextElement(document, jobElement, "attempts", Integer.toString(sineJob.getAttempts()));
+                appendTextElement(document, jobElement, "scope", Integer.toString(sineJob.getScope()));
+                appendTextElement(document, jobElement, "vampireTimeout", Integer.toString(sineJob.getVampireTimeout()));
+                appendTextElement(document, jobElement, "maxAxioms", Integer.toString(sineJob.getMaxAxioms()));
+        }
         else if (job instanceof ConsistencyCheckJob consistencyJob) appendTextElement(document, jobElement, "kbName", consistencyJob.getKbName());
         else if (!(job instanceof SumoUpdateJob)) throw new IOException("Unsupported job class: " + job.getClass().getName());
         return jobElement;
@@ -261,6 +268,9 @@ private Job parseJob(Element jobElement) throws IOException {
                 parseRequiredInt(jobElement, "filterTimeout"),
                 parseRequiredInt(jobElement, "vampireTimeout"));
         break;
+            case "sine-contradiction":
+                job = new SInEContradictionJob(id, requireChildText(jobElement, "kbName"), schedule, parseRequiredInt(jobElement, "attempts"), parseRequiredInt(jobElement, "scope"), parseRequiredInt(jobElement, "vampireTimeout"), parseRequiredInt(jobElement, "maxAxioms"));
+                break;
             case "consistency-check":
                 job = new ConsistencyCheckJob(id, requireChildText(jobElement, "kbName"), schedule);
                 break;