1 # Title: HOL/Tools/Sledgehammer/MaSh/src/readData.py |
|
2 # Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen |
|
3 # Copyright 2012 |
|
4 # |
|
5 # All functions to read the Isabelle output. |
|
6 |
|
7 ''' |
|
8 All functions to read the Isabelle output. |
|
9 |
|
10 Created on July 9, 2012 |
|
11 |
|
12 @author: Daniel Kuehlwein |
|
13 ''' |
|
14 |
|
15 import sys,logging |
|
16 |
|
17 def create_dependencies_dict(nameIdDict,inputFile): |
|
18 logger = logging.getLogger('create_dependencies_dict') |
|
19 dependenciesDict = {} |
|
20 IS = open(inputFile,'r') |
|
21 for line in IS: |
|
22 line = line.split(':') |
|
23 name = line[0] |
|
24 # Name Id |
|
25 if not nameIdDict.has_key(name): |
|
26 logger.warning('%s is missing in nameIdDict. Aborting.',name) |
|
27 sys.exit(-1) |
|
28 |
|
29 nameId = nameIdDict[name] |
|
30 dependenciesIds = [nameIdDict[f.strip()] for f in line[1].split()] |
|
31 # Store results, add p proves p |
|
32 if nameId == 0: |
|
33 dependenciesDict[nameId] = dependenciesIds |
|
34 else: |
|
35 dependenciesDict[nameId] = [nameId] + dependenciesIds |
|
36 IS.close() |
|
37 return dependenciesDict |
|
38 |
|
39 def create_accessible_dict(nameIdDict,idNameDict,maxNameId,inputFile): |
|
40 logger = logging.getLogger('create_accessible_dict') |
|
41 accessibleDict = {} |
|
42 IS = open(inputFile,'r') |
|
43 for line in IS: |
|
44 line = line.split(':') |
|
45 name = line[0] |
|
46 # Name Id |
|
47 if not nameIdDict.has_key(name): |
|
48 logger.warning('%s is missing in nameIdDict. Adding it as theory.',name) |
|
49 nameIdDict[name] = maxNameId |
|
50 idNameDict[maxNameId] = name |
|
51 nameId = maxNameId |
|
52 maxNameId += 1 |
|
53 else: |
|
54 nameId = nameIdDict[name] |
|
55 accessibleStrings = line[1].split() |
|
56 accessibleDict[nameId] = [nameIdDict[a.strip()] for a in accessibleStrings] |
|
57 IS.close() |
|
58 return accessibleDict,maxNameId |
|