Commit 69ec1f03 authored by Simon Cruanes's avatar Simon Cruanes

why.conf avec de nouveaux drivers utilisant simple_types

scripts de comparaison
parent 053e110e
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
import sys
# ce script donne la différence entre les résultats des 2 prouveurs en entrée
if len(sys.argv) <= 1:
print """usage: ./diff prover1,prover2[,prover3,[...]]"""
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)
# se connecte à la DB
import sqlite3
db_file = "output.db"
conn = sqlite3.connect(db_file)
cursor = conn.cursor()
# utilise la lib pour calculer les différences
import lib
table = []
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
lib.print_columns(table)
......@@ -2,7 +2,7 @@
#-*- coding: UTF-8 -*-
# ce script cherche un but qui corresponde aux critères demandés
# ce script cherche les (file,goal) pour lesquels un prouveur SMT et un prouveur TPTP ont des résultats différents.
import sys
......
......@@ -30,9 +30,9 @@ def superior(cursor, prover1, prover2):
query = """SELECT distinct r1.file, r1.goal
FROM runs r1 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"
AND r2.result = "Timeout"
AND r1.file = r2.file AND r1.goal = r2.goal
""" % (prover1, prover2)
try:
......@@ -44,8 +44,9 @@ def superior(cursor, prover1, prover2):
def print_columns(lines, sep = "."):
def print_columns(lines, sep = u"."):
"affiche les colonnes bien alignées"
sep = unicode(sep)
if len(lines) == 0:
return
column_width = len(lines[0])
......@@ -58,7 +59,9 @@ def print_columns(lines, sep = "."):
for line in lines:
for i in xrange(column_width-1):
assert(len(unicode(line[i])) <= widths[i])
print unicode(line[i]).ljust(widths[i]+2, sep),
item = unicode(line[i])
item = item.ljust(widths[i]+2, sep)
print item,
print line[-1]
......
......@@ -2,13 +2,19 @@
PROVERS="spass,eprover,z3,cvc3,simplify,alt-ergo,z3_simple,cvc3_simple,eprover_simple,spass_simple"
if [ -n $1 ]; then
PROVERS="$1"
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
for target_file in $TARGET_DIR/*.mlw; do
echo ./process_file.py $@ "$target_file" "$PROVERS"
./process_file.py -C ../why.conf $@ "$target_file" "$PROVERS"
echo ./process_file.py "$target_file" "$PROVERS"
./process_file.py -C ../why.conf "$target_file" "$PROVERS"
done
done
......@@ -17,7 +17,7 @@ cursor = conn.cursor()
# trouver les prouveurs
provers = cursor.execute("select distinct prover from runs").fetchall()
provers = [line[0] for line in provers]
provers = [unicode(line[0]) for line in provers]
print "prouveurs trouvés :", ", ".join(provers)
......@@ -46,19 +46,17 @@ for prover in provers:
stats[prover] = (len(successes), len(failures))
sys.stdout.flush()
# mettre en forme
table = [["prouveur", u"nombre de succès", u"nombre d'échecs", "nombre total"]]
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 = " ")
lib.print_columns(table, sep = u" ")
# trouver quels prouveurs sont supérieurs les uns aux autres
......@@ -82,17 +80,16 @@ print "\n"
# affiche l'ordre partiel
table = [ ["prouveur1", ">", "prouveur2", "de", "nombre de tasks"] ]
table = []
for ((p1,p2), num) in order.iteritems():
table.append( [p1, "", p2, "", unicode(num)] )
def getKey(x):
try:
return int(x[4])
except:
return 0
table.sort(key = getKey)
# trier puis insérer en haut la légende
table.sort(key = lambda x:x[0])
table[:0] = [["prouveur1", ">", "prouveur2", "pour", "nombre de tasks"]]
lib.print_columns(table, sep = " ") # TODO : afficher un tableau
......@@ -17,21 +17,41 @@ name = "CVC3"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3.drv"
[prover cvc3_simple]
name = "CVC3_simple"
command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3_simple.drv"
[prover z3]
name = "Z3"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3.drv"
[prover z3_simple]
name = "Z3_simple"
command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3_simple.drv"
[prover spass]
name = "spass"
command = "why3-cpulimit 0 %m SPASS -TPTP -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%t %f 2>&1"
driver = "drivers/tptp.drv"
[prover spass_simple]
name = "spass_simple"
command = "why3-cpulimit 0 %m SPASS -TPTP -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%t %f 2>&1"
driver = "drivers/tptp_simple.drv"
[prover eprover]
name = "eprover"
command = "why3-cpulimit 0 %m eprover -s --print-statistics -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
driver = "drivers/tptp.drv"
[prover eprover_simple]
name = "eprover_simple"
command = "why3-cpulimit 0 %m eprover -s --print-statistics -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
driver = "drivers/tptp_simple.drv"
[prover simplify]
name = "simplify"
command = "why3-cpulimit %t %m Simplify %f 2>&1"
......
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