lib.py 1.97 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
#!/usr/bin/env python
#-*- coding: UTF-8 -*-

# utilitaires pour manipuler la BDD

import sys




def diff(cursor, prover1, prover2):
  "trouve les (file,goal) dont le résultat est différent\
  pour prover1 et prover2"

15
  query = """SELECT r1.file, r1.goal, r1.prover, r1.result, r2.prover, r2.result
16
    FROM runs r1 JOIN runs r2
17
18
19
    WHERE r1.prover = "%s" AND r2.prover = "%s"
      AND r1.file = r2.file AND r1.goal = r2.goal
      AND r1.result <> r2.result""" % \
20
21
22
23
24
25
26
27
28
      (prover1, prover2)
  try:
    result = cursor.execute(query)
    return result.fetchall()
  except Exception, e:
    print >> sys.stderr, "exception :", repr(e)
    return []


29
30
31
32
33
34
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
    WHERE r1.prover = "%s" AND r2.prover = "%s"
35
      AND r1.file = r2.file AND r1.goal = r2.goal
36
      AND r1.result = "Valid"
37
      AND r2.result <> "Valid"
38
39
40
41
42
43
44
45
46
    """ % (prover1, prover2)

  try:
    result = cursor.execute(query)
    return result.fetchall()
  except Exception, e:
    print >> sys.stderr, "exception :", repr(e)
    return None

47
48


49
def print_columns(lines, sep = u"."):
50
  "affiche les colonnes bien alignées"
51
  sep = unicode(sep)
52
53
54
55
56
57
58
  if len(lines) == 0:
    return
  column_width = len(lines[0])
  widths = [0 for x in xrange(column_width)]

  for line in lines:
    for i in xrange(column_width-1):
59
      widths[i] = max(widths[i], len(unicode(line[i])))
60
61
62

  for line in lines:
    for i in xrange(column_width-1):
63
      assert(len(unicode(line[i])) <= widths[i])
64
65
66
      item = unicode(line[i])
      item = item.ljust(widths[i]+2, sep)
      print item,
67
    print line[-1]
68
69
70
71
72


def print_sep():
  "affiche une ligne de '-' pour séparer clairement des sections de l'affichage"
  print "---------------------------------------------------------------"
73
74
75
76
77
78
79



def erase_line(stream = sys.stdout):
  "efface la ligne et revient au début"
  stream.write("\033[2K\r")
  stream.flush()