Commit ac57ed96 authored by Simon Cruanes's avatar Simon Cruanes
Browse files

small changes in tptp2why test script

parent 3cd6d4ab
......@@ -24,7 +24,8 @@ directly. Every prover is called on every problem.
options :
-P prover : adds a why prover
-p prover : adds a prover to be called directly on tptp problem"""
-p prover : adds a prover to be called directly on tptp problem
-I dir : use this dir to search for included files"""
class Options:
......@@ -70,10 +71,17 @@ def sendTo(problem, prover, useWhy = True):
"calls the prover on the problem, and return its return value and output's \
if useWhy:
left = subprocess.Popen("tptp2why -", shell=True, \
if "-I" in options.options:
command = "tptp2why - -I "+options.options["-I"]
command = "tptp2why -"
left = subprocess.Popen(command, shell=True, \
stdout=subprocess.PIPE, stdin=subprocess.PIPE)
problem = left.communicate(problem)[0]
prover = "why - -P "+prover
if "-I" in options.options:
prover = prover + " -I "+options.options["-I"]
s = subprocess.Popen(prover, shell=True, \
stdin=subprocess.PIPE, stdout=subprocess.PIPE)
print "\n"+ansi.inBlue("*", pos="background"), "send data to prover "+ prover
......@@ -85,7 +93,7 @@ def sendTo(problem, prover, useWhy = True):
def isValid(retcode, output):
"returns True in case of success"
for pattern in ["Valid","valid", "[Pp]roof found"]:
for pattern in ["Valid","valid", "[Pp]roof found", "[cC]ompletion [fF]ound"]:
if any( [, line) for line in output ] ):
return True
return False
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment