|
1 ''' |
|
2 All functions to read the Isabelle output. |
|
3 |
|
4 Created on July 9, 2012 |
|
5 |
|
6 @author: Daniel Kuehlwein |
|
7 ''' |
|
8 |
|
9 import sys,logging |
|
10 |
|
11 def create_feature_dict(nameIdDict,idNameDict,maxNameId,featureIdDict,maxFeatureId,inputFile): |
|
12 logger = logging.getLogger('create_feature_dict') |
|
13 featureDict = {} |
|
14 IS = open(inputFile,'r') |
|
15 for line in IS: |
|
16 line = line.split(':') |
|
17 name = line[0] |
|
18 # Name Id |
|
19 if nameIdDict.has_key(name): |
|
20 logger.warning('%s appears twice in the feature file. Aborting.',name) |
|
21 sys.exit(-1) |
|
22 else: |
|
23 nameIdDict[name] = maxNameId |
|
24 idNameDict[maxNameId] = name |
|
25 nameId = maxNameId |
|
26 maxNameId += 1 |
|
27 # Feature Ids |
|
28 featureNames = [f.strip() for f in line[1].split()] |
|
29 for fn in featureNames: |
|
30 if not featureIdDict.has_key(fn): |
|
31 featureIdDict[fn] = maxFeatureId |
|
32 maxFeatureId += 1 |
|
33 featureIds = [featureIdDict[fn] for fn in featureNames] |
|
34 # Store results |
|
35 featureDict[nameId] = featureIds |
|
36 IS.close() |
|
37 return featureDict,maxNameId,maxFeatureId |
|
38 |
|
39 def create_dependencies_dict(nameIdDict,inputFile): |
|
40 logger = logging.getLogger('create_dependencies_dict') |
|
41 dependenciesDict = {} |
|
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. Aborting.',name) |
|
49 sys.exit(-1) |
|
50 |
|
51 nameId = nameIdDict[name] |
|
52 dependenciesIds = [nameIdDict[f.strip()] for f in line[1].split()] |
|
53 # Store results, add p proves p |
|
54 dependenciesDict[nameId] = [nameId] + dependenciesIds |
|
55 IS.close() |
|
56 return dependenciesDict |
|
57 |
|
58 def create_accessible_dict(nameIdDict,idNameDict,maxNameId,inputFile): |
|
59 logger = logging.getLogger('create_accessible_dict') |
|
60 accessibleDict = {} |
|
61 IS = open(inputFile,'r') |
|
62 for line in IS: |
|
63 line = line.split(':') |
|
64 name = line[0] |
|
65 # Name Id |
|
66 if not nameIdDict.has_key(name): |
|
67 logger.warning('%s is missing in nameIdDict. Adding it as theory.',name) |
|
68 nameIdDict[name] = maxNameId |
|
69 idNameDict[maxNameId] = name |
|
70 nameId = maxNameId |
|
71 maxNameId += 1 |
|
72 else: |
|
73 nameId = nameIdDict[name] |
|
74 accessibleStrings = line[1].split() |
|
75 accessibleDict[nameId] = [nameIdDict[a.strip()] for a in accessibleStrings] |
|
76 IS.close() |
|
77 return accessibleDict,maxNameId |
|
78 |
|
79 |