Commit 9253d753 authored by Simon Cruanes's avatar Simon Cruanes
Browse files

output more readable for tptp2why test script, with nice colors \o/

parent 8773dc40
from sys import stderr
class Ansi:
"""ANSI control sequences control"""
CSI = "\x1B["
# colors
Black = "0"
Red = "1"
Green = "2"
Yellow = "3"
Blue = "4"
Magenta = "5"
Cyan = "6"
White = "7"
Reset = "9"
# effects
bold = "1"
reset = "0"
underline = "4"
blinkSlow = "5"
blinkFast = "6"
negative = "7"
normal = "22"
notUnderlined = "24"
# fore|back ground
foreground = "3"
background = "4"
def colorize( s, color = "reset", pos = "foreground", *args ):
"applies changes to the string given"
prefix = Ansi.CSI + getattr( Ansi, pos, Ansi.foreground) + getattr( Ansi, color, Ansi.reset )
suffix = Ansi.CSI + "m"
for item in args:
prefix += ";" + getattr( Ansi, item, Ansi.normal )
prefix += "m"
return prefix + s + suffix
def inBlue( s, bold = False, pos = "foreground" ):
args = []
if bold:
args.append( "bold" )
return colorize( s, "Blue", pos, *args )
def inGreen( s, bold = False, pos = "foreground" ):
args = []
if bold:
args.append( "bold" )
return colorize( s, "Green", pos, *args )
def inRed( s, bold = False, pos = "foreground" ):
args = []
if bold:
args.append( "bold" )
return colorize( s, "Red", pos, *args )
def inBlack( s, bold = False, pos = "foreground" ):
args = []
if bold:
args.append( "bold" )
return colorize( s, "Black", pos, *args )
def inNormal( s, bold = False, pos = "foreground" ):
"uses normal color"
args = []
if bold:
args.append( "bold" )
return colorize( s, "Reset", pos, *args )
class Log:
logStream = stderr
@classmethod
def log( self, s, bold=False ):
"""
>>> Log.setLogStream( sys.stdout )
>>> Log.log( 'coin' )
coin
>>> Log.setLogStream( file('/dev/null', 'w') )
>>> Log.log( 'pan' )
"""
print >> self.logStream, ansi.inNormal( s, bold= bold )
@classmethod
def logImportant( self, s, bold=False ):
"prints in reversed blue"
print >> self.logStream, ansi.inBlue( s, bold=bold, pos="background" )
@classmethod
def logSoft( self, s ):
"prints in blue"
print >> self.logStream, inBlue( s )
@classmethod
def logFail( self, s ):
"for fails, print in red"
print >> self.logStream, ansi.inRed( s, bold=True )
@classmethod
def logCritical( self, s ):
"for critical warning, very visible !"
print >> self.logStream, inRed( s, pos="background", blink=1 )
@classmethod
def setLogStream( self, logStream ):
self.logStream = logStream
......@@ -8,15 +8,21 @@ import getopt
import time
import subprocess
from os import path
import re
import ansi
#------------------------------------------------------------------------------
# parsing options
usage = """usage : dispatcher [-P prover [-P prover...]] [-I dir] [-o file] \
[-p prover [-p prover...]] [--help] [--] file1 [file2...]
usage = """usage : dispatcher [--help] [-P prover [-P prover...]] \
[-p prover [-p prover...]] [-I dir] [-o file][--] file1 [file2...]
It tries to solve the given files with given provers.
Tries to solve the given tptp files (*.p) with given provers, through why or \
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"""
......@@ -24,6 +30,7 @@ It tries to solve the given files with given provers.
class Options:
"contains all options parsed on the command line"
optstring = "P:p:I:o:h"
long_optstring = ["help"]
......@@ -31,6 +38,7 @@ class Options:
tptpProvers = []
def parse(self):
self.path = path.dirname(sys.argv[0])
self.options, self.args = \
getopt.getopt(sys.argv[1:], self.optstring, self.long_optstring)
# add each prover to self.provers
......@@ -46,6 +54,7 @@ class Options:
def __init__(self):
self.parse()
print "search for files in", self.path
options = Options()
......@@ -67,23 +76,63 @@ output's lines"
prover = "why - -P "+prover
s = subprocess.Popen(prover, shell=True, \
stdin=subprocess.PIPE, stdout=subprocess.PIPE)
print "send data to prover"
return (s.returncode, s.communicate(problem)[0].split("\n"))
print "\n"+ansi.inBlue("*", pos="background"), "send data to prover "+ prover
output = s.communicate(problem)[0].splitlines()
return (s.returncode, output)
#-----------------------------------------------------------------------------
# interpreting provers output
def isValid(retcode, output):
"returns True in case of success"
for pattern in ["Valid","valid", "[Pp]roof found"]:
if any( [ re.search(pattern, line) for line in output ] ):
return True
return False
def isFailure(retcode, output):
"returns True in case of failure"
if retcode != 0:
return True
for pattern in ["[fF]ailure","[fF]alse", "[nN]o [Pp]roof found"]:
if any( [ re.search(pattern, line) for line in output ] ):
return True
return False
def handleOutput(retcode, output):
"""if we can find it is a failure or a success, print it.
Else, print the output."""
print "retcode :",(ansi.inGreen(`retcode`) if retcode==0 else ansi.inRed(`retcode`))
if isFailure(retcode, output):
print ansi.inRed("Failure")
return
elif isValid(retcode, output):
print ansi.inGreen("Valid")
return
else:
for line in output:
print line
def main():
for f in options.args:
print "file %s\n" % f
print "\n\n"+ ansi.inBlue("file "+f, pos="background") + "\n"
try:
fd = open(f, 'r')
problem = fd.read()
fd.close()
# tptp provers
for prover in options.tptpProvers:
for line in sendTo(problem, prover, useWhy = False)[1]:
print line.strip()
try:
retcode, output = sendTo(problem, prover, useWhy = False)
handleOutput(retcode, output)
except: pass
# why-driven provers
for prover in options.provers:
for line in sendTo(problem, prover)[1]:
print line.strip()
try:
retcode, output = sendTo(problem, prover)
handleOutput(retcode, output)
except: pass
except Exception, e:
print "exception :", e, e.args
......
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