Commit dfa35b47 authored by Simon Cruanes's avatar Simon Cruanes

commentaires pour les scripts de comparaison

parent 56d48bb8
......@@ -6,6 +6,7 @@
import sys
import sqlite3
# demander confirmation pour effacer la base
print "ceci va effacer la base de tests. Continuer ?"
while True:
confirm = raw_input("[y/n] ")
......@@ -14,6 +15,7 @@ while True:
elif confirm in ["n","No","N","no"]:
sys.exit(0)
# on veut effacer la base. Pour cela, il faut d'abord s'y connecter.
conn = sqlite3.connect("output.db")
cursor = conn.cursor()
......@@ -22,7 +24,6 @@ try:
cursor.close()
conn.commit()
conn.close()
except:
print >> sys.stderr, "database non valide !"
sys.exit(1)
......
......@@ -3,24 +3,25 @@
import sys
# ce script donne la différence entre les résultats des 2 prouveurs en entrée
# ce script donne la différence entre les résultats des prouveurs donnés
# en argument
if len(sys.argv) <= 1:
print """usage: ./diff prover1,prover2[,prover3,[...]]"""
sys.exit(0)
# parser les prouveurs
provers = sys.argv[1]
provers = [p.strip() for p in provers.split(",")]
print "compare les prouveurs", ", ".join(provers)
if len(provers) <= 1:
print "erreur, il faut au moins 2 prouveurs !"
sys.exit(1)
print "compare les prouveurs", ", ".join(provers)
# se connecte à la DB
# se connecte à la DB
import sqlite3
db_file = "output.db"
......@@ -34,11 +35,11 @@ import lib
table = []
# comparer les couples de prouveurs. On évite les redondances en ne comparant
# un couple (p1,p2) que dans le sens p1<p2 (ordre lexicographique)
for p1, p2 in [(p1, p2) for p1 in provers for p2 in provers if p1 < p2]:
diffs = lib.diff(cursor, p1, p2)
table += diffs
# afficher les différences
lib.print_columns(table)
......@@ -6,6 +6,7 @@
import sys
import sqlite3
# ouvrir la DB
db_file = "output.db"
if len(sys.argv) > 1:
......@@ -16,15 +17,15 @@ print >> sys.stderr, "utile la database", db_file
conn = sqlite3.connect(db_file)
cursor = conn.cursor()
# essayer de dumper la table runs (échoue si elle n'existe pas)
try:
dump = cursor.execute("select * from runs")
dump = dump.fetchall()
except:
print >> sys.stderr, "database %s non valide !" % db_file
sys.exit(1)
dump = dump.fetchall()
# afficher le dump
import lib
lib.print_columns(dump)
......@@ -2,7 +2,8 @@
#-*- coding: UTF-8 -*-
# ce script cherche les (file,goal) pour lesquels un prouveur SMT et un prouveur TPTP ont des résultats différents.
# ce script cherche les (file,goal) pour lesquels un prouveur SMT et
# un prouveur TPTP ont des résultats différents.
import sys
......@@ -14,18 +15,19 @@ conn = sqlite3.connect("output.db")
cursor = conn.cursor()
# utilitaires
import lib
# les prouveurs
# les prouveurs (demander à la DB)
provers = cursor.execute("select distinct prover from runs").fetchall()
provers = [p[0] for p in provers]
# les 2 uplets de prouveurs
# les 2 uplets de prouveurs, sans redondances
provers_combinaisons = [(p1,p2) for p1 in provers for p2 in provers if p1 < p2]
# trouver les couples de prouveurs dont l'un échoue et l'autre réussit,
# pour chaque (fichier,but)
diffs = []
diffs = cursor.execute("""SELECT r1.file,r1.goal, r1.prover, r1.result, r2.prover, r2.result
FROM runs r1
......@@ -33,9 +35,11 @@ diffs = cursor.execute("""SELECT r1.file,r1.goal, r1.prover, r1.result, r2.prove
WHERE r1.file = r2.file
AND r1.goal = r2.goal
AND r1.result = "Valid"
AND r2.result = "Timeout"
AND r2.result <> "Valid"
ORDER BY r1.file ASC""").fetchall()
# comment différencier un prouveur TPTP d'un prouveur SMT ?
tptp = ["spass", "eprover"]
def isTptp(x):
......
......@@ -6,14 +6,14 @@
import sys
# différences de résultats entre les 2 prouveurs
def diff(cursor, prover1, prover2):
"trouve les (file,goal) dont le résultat est différent\
pour prover1 et prover2"
query = """SELECT r1.file, r1.goal, r1.prover, r1.result, r2.prover, r2.result
FROM runs r1 JOIN runs r2
FROM runs r1
INNER JOIN runs r2
WHERE r1.prover = "%s" AND r2.prover = "%s"
AND r1.file = r2.file AND r1.goal = r2.goal
AND r1.result <> r2.result""" % \
......@@ -26,11 +26,13 @@ def diff(cursor, prover1, prover2):
return []
# (file,goal) sur lesquels le premier prouveur est meilleur que le second
def superior(cursor, prover1, prover2):
"trouve les (file,goal) pour lesquels prover1 > prover2"
query = """SELECT distinct r1.file, r1.goal
FROM runs r1 JOIN runs r2
FROM runs r1
INNER JOIN runs r2
WHERE r1.prover = "%s" AND r2.prover = "%s"
AND r1.file = r2.file AND r1.goal = r2.goal
AND r1.result = "Valid"
......@@ -45,7 +47,7 @@ def superior(cursor, prover1, prover2):
return None
# affichage aligné en colonnes
def print_columns(lines, sep = u"."):
"affiche les colonnes bien alignées"
sep = unicode(sep)
......@@ -53,7 +55,7 @@ def print_columns(lines, sep = u"."):
return
column_width = len(lines[0])
widths = [0 for x in xrange(column_width)]
# calculer la largeur de chaque colonne (max des largeurs de ses éléments)
for line in lines:
for i in xrange(column_width-1):
widths[i] = max(widths[i], len(unicode(line[i])))
......@@ -67,18 +69,21 @@ def print_columns(lines, sep = u"."):
print line[-1]
# petite facilité
def print_sep():
"affiche une ligne de '-' pour séparer clairement des sections de l'affichage"
"affiche une ligne de '-' pour séparer clairement des\
sections de l'affichage"
print "---------------------------------------------------------------"
# effacer la ligne courante du terminal
def erase_line(stream = sys.stdout):
"efface la ligne et revient au début"
stream.write("\033[2K\r")
stream.flush()
# récupéré sur le net, pour obtenir largeur et hauteur du terminal
def getTerminalSize():
"récupère la largeur et la hauteur du terminal"
# {{{
......@@ -105,6 +110,12 @@ def getTerminalSize():
return int(cr[1]), int(cr[0])
# }}}
# tente d'affichier un tableau donné en entrée. Ce tableau
# est un dictionnaire (colonne,ligne) -> item qui doit vérifier
# la propriété suivante :
# pour tout (i,j) dans tab, (j,i) est aussi dans tab
def printTab(tab):
"affiche le tableau carré donné en entrée"
......
......@@ -2,8 +2,9 @@
#-*- coding: UTF-8 -*-
# ce script lance un prouveur sur un fichier .mlw (grâce à why3)
# ce script lance un prouveur sur un fichier .mlw (grâce à whyml3)
# et stocke la sortie dans la base output.db
# il peut aussi être utilisé avec why3 grâce à l'option -t
import sys
from os import path
......@@ -15,12 +16,12 @@ import getopt
#------------------------------------------------
# parse les arguments
db_file = "output.db"
try:
opt, args = getopt.getopt(sys.argv[1:], "df:C:", [])
opt, args = getopt.getopt(sys.argv[1:], "df:C:t:", [])
target_file = args[0]
_,extension = path.splitext(target_file)
provers = args[1]
provers = provers.split(",")
......@@ -33,18 +34,26 @@ try:
if '-f' in opt:
db_file = opt['-f']
else:
db_file = "output.db"
if '-C' in opt:
config_file = opt['-C']
else:
config_file = None
if '-t' in opt:
tool = opt['-t']
else:
tool = "whyml3"
except:
print """usage:
process_file [-d] [-f file] [-C config_file] file prover[,prover[,prover...]]
process_file.py [-d] [-f file] [-C config_file] [-t tool] file prover[,prover[,prover...]]
-d : active le mode debug
-f <file> : stocke les résultats dans <file>
-C <file> : utilise le fichier de configuration <file>"""
-C <file> : utilise le fichier de configuration <file>
-t <tool> : utilise <tool> pour les preuves (why, whyml...)"""
sys.exit(1)
print >> sys.stderr, "utilise le(s) prouveur(s) %s sur %s (db : %s)" % \
......@@ -59,6 +68,8 @@ import sqlite3
conn = sqlite3.connect(db_file)
cursor = conn.cursor()
# si la table runs n'existe pas, la créer. Sinon, signaler qu'on a trouvé une base.
# le cas où la table existe mais n'est pas au bon format n'est pas traité.
try:
cursor.execute("""create table runs
(file string, goal string, prover string, result string, time float)""")
......@@ -68,12 +79,11 @@ except sqlite3.OperationalError:
#------------------------------------------------
# lance whyml3 sur le fichier
def launch_whyml(target_file, prover):
# lance [tool] sur le fichier pour récupérer les résultats
def launch_tool(target_file, prover):
target_file = path.abspath(target_file)
command_list = ["whyml3", "-P", prover, "-a", "split_goal"]
command_list = [tool, "-P", prover, "-a", "split_goal"]
if config_file:
command_list += ["-C", config_file]
command_list.append(target_file)
......@@ -92,7 +102,7 @@ def launch_whyml(target_file, prover):
def getFile(x):
"récupère le nom de fichier"
return path.basename(x.partition(".mlw")[0] + ".mlw")
return path.basename(x.partition(extension)[0] + extension)
def getGoal(x):
"récupère le nom du but"
......@@ -190,7 +200,7 @@ def process(prover):
"toute la chaine de traitement pour un prouveur donné"
prover = prover.strip()
results = launch_whyml(target_file, prover)
results = launch_tool(target_file, prover)
lines = process_results(results)
process_lines(lines)
print_lines(lines)
......
#!/bin/sh
# lance les prouveurs donnés (ou ceux donnés en argument) sur les fichiers de 2 dossiers
PROVERS="spass,eprover,z3,cvc3,simplify,alt-ergo,z3_simple,cvc3_simple,eprover_simple,spass_simple"
......@@ -8,7 +9,6 @@ if [ -n $1 ]; then
echo "utilise les prouveurs $1"
fi
#TARGET_DIR="../bench/programs/good/"
TARGET_DIRS="../examples/programs/ ../bench/programs/good/"
for TARGET_DIR in $TARGET_DIRS; do
......
......@@ -15,7 +15,6 @@ conn = sqlite3.connect("output.db")
cursor = conn.cursor()
# trouver les prouveurs
provers = cursor.execute("select distinct prover from runs").fetchall()
provers = [unicode(line[0]) for line in provers]
......@@ -26,65 +25,57 @@ print ""
# collecter les statistiques (succès, échecs) de chaque prouveur
stats = {}
for prover in provers:
successes = cursor.execute("""
SELECT DISTINCT file,goal FROM runs
WHERE result = "Valid"
AND prover = "%s"
""" % prover).fetchall()
failures = cursor.execute("""
SELECT DISTINCT file,goal FROM runs
WHERE result <> "Valid"
AND prover = "%s"
""" % prover).fetchall()
stats[prover] = (len(successes), len(failures))
sys.stdout.flush()
# mettre en forme
# mettre en forme : afficher, par colonne, le taux d'échec et de succès des prouveurs
table = [["prouveur", "nombre de succes", "nombre d'echecs", "nombre total"]]
for prover in provers:
entry = [prover, stats[prover][0], stats[prover][1], stats[prover][0] + stats[prover][1]]
table.append(entry)
lib.print_columns(table, sep = u" ")
# trouver quels prouveurs sont supérieurs les uns aux autres
lib.print_columns(table, sep = " ")
lib.print_sep()
# trouver sur combien de buts les prouveurs sont supérieurs les uns aux autres
order = {}
tuples = [(p1,p2) for p1 in provers for p2 in provers if p1 != p2]
max_len = 0
for prover in provers:
max_len = max(max_len, len(prover))
# pour chaque couple de prouveur, calculer la supériorité
for tuple in tuples:
p1,p2 = tuple
# afficher ce que l'on fait
current = ("compare " + p1 + " "+ p2).ljust(12+2*max_len, " ")
print current ,"(%.2f %%)" % (float(tuples.index(tuple)) / len(tuples)*100),
print current ,"(%.1f %%)" % (float(tuples.index(tuple)) / len(tuples)*100),
sys.stdout.flush()
# effectuer le calcul
sups = lib.superior(cursor, p1, p2)
order[ (p1, p2) ] = len(sups)
# effacer la ligne
lib.erase_line()
order[ (p1, p2) ] = len(sups)
print "\n"
# affiche l'ordre partiel
print ""
# affiche les résultats sous forme de tableau
table = {}
for ((p1,p2), num) in order.iteritems():
......
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