diff --git a/bin/make_examples.js b/bin/make_examples.js index 19ecb59..e1ebf7c 100755 --- 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 index bf07804..a3590c2 100644 --- 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 index a6bdebb..7f36a82 100644 --- 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 index 3d1a181..7542369 100644 --- 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 new file mode 100644 index 0000000..61bd8a5 --- /dev/null +++ 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 }; \ No newline at end of file diff --git a/lib/tension.js b/lib/tension.js index 0c0def3..42021b9 100644 --- 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 new file mode 100755 index 0000000..a35a059 --- /dev/null +++ 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 <. +@prefix log: . +@prefix : . + +: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. + } +}. \ No newline at end of file