MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

Commit 74cf1256 authored by Simon Cruanes's avatar Simon Cruanes
Browse files

first draft (not usable) of a tool to compare tptp solvers

and solvers called by why (with tptp2why output)
parent 41d47828
#!/usr/bin/env python
# launches some provers on a bunch of tptp problems, after conversion
# with tptp2why
import sys
import getopt
import time
import subprocess
# parsing options
usage = """usage : dispatcher [-P prover [-P prover...]] [-I dir] [-o file] \
[-p prover [-p prover...]] [--help] [--] file1 [file2...]
It tries to solve the given files with given provers.
-P prover : adds a why prover
-p prover : adds a prover to be called directly on tptp problem"""
class Options:
"contains all options parsed on the command line"
optstring = "P:p:I:o:h"
long_optstring = ["help"]
provers = []
tptpProvers = []
def parse(self):
self.options, self.args = \
getopt.getopt(sys.argv[1:], self.optstring, self.long_optstring)
# add each prover to self.provers
for opt,prover in self.options:
if opt == "-P":
elif opt == "-p":
self.options = dict(self.options)
# those options are now useless
self.options.pop("-P", None)
self.options.pop("-p", None)
def __init__(self):
options = Options()
if "--help" in options.options or "-h" in options.options:
print usage
# finding provers
def sendTo(problem, prover, useWhy = True):
"calls the prover on the problem, and return its return value and\
output's lines"
if useWhy:
left = subprocess.Popen("tptp2why -", shell=True, \
stdout=subprocess.PIPE, stdin=subprocess.PIPE)
prover = "why - -P "+prover
right = subprocess.Popen(prover, shell=True, \
stdin=left.stdout, stdout=subprocess.PIPE)
left = right = subprocess.Popen(prover, shell=True, \
stdin=subprocess.PIPE, stdout=subprocess.PIPE)
print "data sent to prover"
return (right.wait(), right.stdout.readlines())
def main():
for f in options.args:
print "file %s\n" % f
fd = open(f, 'r')
problem =
for prover in options.tptpProvers:
for line in sendTo(problem, prover, useWhy = False)[1]:
print line.strip()
for prover in options.provers:
for line in sendTo(problem, prover)[1]:
print line.strip()
except Exception, e:
print "exception :", e, e.args
if __name__=="__main__":
exec eprover -s -xAuto -tAuto --memory-limit=Auto --tstp-in --cpu-limit=2 $@
FILE=$( tempfile spass )
cat - > ${FILE} && SPASS -TPTP -PGiven=0 -PProblem=0 -TimeLimit=2 ${FILE}
rm -f ${FILE}
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