adding rs2fol support

eyereasoner · Jun 27, 2024 · 9c6107a · 9c6107a
1 parent c42e567
commit 9c6107a
Show file tree

Hide file tree

Showing 9 changed files with 126 additions and 3 deletions.
diff --git a/bin/make_examples.js b/bin/make_examples.js
@@ -157,6 +157,9 @@ async function run_tests_one(reasoner,filePath) {
     else if (filePath.match(/:FAIL/)) {
         type = `fail`;
     }
+    else if (filePath.match(/:LIE/)) {
+        type = `lie`;
+    }
     else {
         type = `normal`;
     }

diff --git a/config.json-example b/config.json-example
@@ -11,12 +11,17 @@
         "timeout": "10"
     },
     "tension": {
-        "path": "timeout 10s /Users/hochsten/github.com/joachimvh/tension.js/bin/tension.js",
+        "path": "timeout 10s $HOME/github.com/joachimvh/tension.js/bin/tension.js",
         "args": "-f",
         "timeout": "10"
     },
     "latar": {
-        "path": "timeout 10s /Users/hochsten/github.com/KNowledgeOnWebScale/Latar/latar",
+        "path": "timeout 10s $HOME/github.com/KNowledgeOnWebScale/Latar/latar",
+        "args": "",
+        "timeout": "10"
+    },
+    "rs2fol": {
+        "path": "timeout 10s ./script/rs2fol.sh",
         "args": "",
         "timeout": "10"
     }

diff --git a/lib/eye.js b/lib/eye.js
@@ -26,6 +26,12 @@ async function reason(filePath, config) {
                 if (config.type == 'normal' && output.match(/.*:test.*is.*true/g)) {
                     resolve(IS_OK);
                 }
+                else if (config.type == 'lie' && output.match(/.*:test.*is.*true/g)) {
+                    resolve(IS_LIE);
+                }
+                else if (config.type == 'lie' && output.match(/^\s*$/g)) {
+                    resolve(IS_OK);
+                }
                 else if (config.type == 'fail' && output.match(/inference_fuse/g)) {
                     resolve(IS_OK);
                 }

diff --git a/lib/latar.js b/lib/latar.js
@@ -26,6 +26,12 @@ async function reason(filePath, config) {
                 if (config.type == 'normal' && output.match(/.*:test.*is.*true/g)) {
                     resolve(IS_OK);
                 }
+                else if (config.type == 'lie' && output.match(/.*:test.*is.*true/g)) {
+                    resolve(IS_LIE);
+                }
+                else if (config.type == 'lie' && output.match(/^\s*$/g)) {
+                    resolve(IS_OK);
+                }
                 else if (config.type == 'fail' && output.match(/contradicton detected/g)) {
                     resolve(IS_OK);
                 }

diff --git a/lib/rs2fol.js b/lib/rs2fol.js
@@ -0,0 +1,53 @@
+const fs  = require('fs');
+const exec = require('child_process').exec;
+const { IS_OK , IS_INCOMPLETE , IS_TIMEOUT , IS_LIE , IS_SKIPPED , IS_CRASHED } = require('../lib/errors');
+
+async function reason(filePath, config) {
+    return new Promise( (resolve) => {
+        if (config.type === 'skip' || ! filePath.match(/\/pure\//g)) {
+            resolve(IS_SKIPPED);
+            return;
+        }
+
+        try {
+            const command = `${config.rs2fol.path} ${config.rs2fol.args} ${filePath} > ${filePath}.out 2>&1`;
+            exec(command, {
+                timeout: config.rs2fol.timeout * 1000, 
+                killSignal: 'SIGKILL',
+                windowsHide: true
+            }, (error) => {
+                if (error && error.killed) {
+                    resolve(IS_TIMEOUT);
+                    return;
+                }
+
+                const output = fs.readFileSync(`${filePath}.out`, { encoding: 'utf-8'});
+
+                if (config.type == 'normal' && output.match(/.*:test.*is.*true/g)) {
+                    resolve(IS_OK);
+                }
+                else if (config.type == 'lie' && output.match(/.*:test.*is.*true/g)) {
+                    resolve(IS_LIE);
+                }
+                else if (config.type == 'lie' && output.match(/No answers found/g)) {
+                    resolve(IS_OK);
+                }
+                else if (config.type == 'fail' && output.match(/Refutation found/g)) {
+                    resolve(IS_OK);
+                }
+                else if (config.type == 'normal' && output.match(/Refutation found/g)) {
+                    resolve(IS_LIE);
+                }
+                else {
+                    resolve(IS_INCOMPLETE);
+                }
+            });
+        }
+        catch (e) {
+            console.error(e);
+            resolve(IS_CRASHED);
+        }
+    });
+}
+
+module.exports = { reason };
diff --git a/lib/tension.js b/lib/tension.js
@@ -26,6 +26,12 @@ async function reason(filePath, config) {
                 if (config.type == 'normal' && output.match(/.*:test.*is.*true/g)) {
                     resolve(IS_OK);
                 }
+                else if (config.type == 'lie' && output.match(/.*:test.*is.*true/g)) {
+                    resolve(IS_LIE);
+                }
+                else if (config.type == 'lie' && output.match(/^\s*$/g)) {
+                    resolve(IS_OK);
+                }
                 else if (config.type == 'fail' && output.match(/Found a contradiction at root level/g)) {
                     resolve(IS_OK);
                 }

diff --git a/script/rs2fol.sh b/script/rs2fol.sh
@@ -0,0 +1,24 @@
+#!/bin/bash
+
+FILE=$1
+R2FOL=${HOME}/github.com/RebekkaMa/rs2fol/bin/rs2fol
+VAMPIRE=/usr/local/bin/vampire
+
+if [ "${FILE}" == "" ]; then
+   echo "usage: $0 file"
+   exit 1
+fi
+
+TMPFILE=$(mktemp)
+
+cat ${FILE} > ${TMPFILE}
+
+>> ${TMPFILE} cat <<EOF
+() log:onQuerySurface {
+   :test :is true .
+} .
+EOF
+
+${R2FOL} transform-qa --vampire-exec ${VAMPIRE} -q -i ${TMPFILE}
+
+rm ${TMPFILE}
diff --git a/test/pure/contradiction2:FAIL.n3s b/test/pure/contradiction2:FAIL.n3s
@@ -22,4 +22,4 @@
     } .
 } .
 
-() log:onNegativeSurface { :test :is true. () log:onNegativeAnswerSurface { :test :is true } } .
+() log:onNegativeSurface { :test :is true. () log:onNegativeAnswerSurface { :test :is true } } .
diff --git a/test/pure/socrates4:LIE.n3s b/test/pure/socrates4:LIE.n3s
@@ -0,0 +1,20 @@
+@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
+@prefix log: <http://www.w3.org/2000/10/swap/log#>.
+@prefix : <urn:example:>.
+
+:Socrates a :Man.
+:Man rdfs:subClassOf :Mortal.
+
+(_:S) log:onNegativeSurface {
+    _:S a :Mortal.
+    () log:onNegativeSurface {
+        :test :is true.
+    }.
+}.
+
+() log:onNegativeSurface {
+    :test :is true.
+    () log:onNegativeAnswerSurface {
+        :test :is true.
+    }
+}.
-Original file line number
+Diff line change
@@ Expand Up / @@ -22,4 +22,4 @@ @@
         } .
     } .
-    () log:onNegativeSurface { :test :is true. () log:onNegativeAnswerSurface { :test :is true } } .
+    () log:onNegativeSurface { :test :is true. () log:onNegativeAnswerSurface { :test :is true } } .