--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py Mon Nov 26 12:04:32 2012 +0100
@@ -0,0 +1,182 @@
+'''
+Created on Jul 12, 2012
+
+@author: daniel
+'''
+
+from os.path import join
+from Queue import Queue
+from readData import create_accessible_dict,create_dependencies_dict,create_feature_dict
+from cPickle import load,dump
+
+class Dictionaries(object):
+ '''
+ This class contains all info about name-> id mapping, etc.
+ '''
+ def __init__(self):
+ '''
+ Constructor
+ '''
+ self.nameIdDict = {}
+ self.idNameDict = {}
+ self.featureIdDict={}
+ self.maxNameId = 0
+ self.maxFeatureId = 0
+ self.featureDict = {}
+ self.dependenciesDict = {}
+ self.accessibleDict = {}
+ self.expandedAccessibles = {}
+ self.changed = True
+
+ """
+ Init functions. Side Effect: nameIdDict, idNameDict, featureIdDict get filled!
+ """
+ def init_featureDict(self,featureFile):
+ self.featureDict,self.maxNameId,self.maxFeatureId = create_feature_dict(self.nameIdDict,self.idNameDict,self.maxNameId,self.featureIdDict,\
+ self.maxFeatureId,featureFile)
+ def init_dependenciesDict(self,depFile):
+ self.dependenciesDict = create_dependencies_dict(self.nameIdDict,depFile)
+ def init_accessibleDict(self,accFile):
+ self.accessibleDict,self.maxNameId = create_accessible_dict(self.nameIdDict,self.idNameDict,self.maxNameId,accFile)
+
+ def init_all(self,inputFolder,featureFileName = 'mash_features',depFileName='mash_dependencies',accFileName = 'mash_accessibility'):
+ featureFile = join(inputFolder,featureFileName)
+ depFile = join(inputFolder,depFileName)
+ accFile = join(inputFolder,accFileName)
+ self.init_featureDict(featureFile)
+ self.init_accessibleDict(accFile)
+ self.init_dependenciesDict(depFile)
+ self.expandedAccessibles = {}
+ self.changed = True
+
+ def get_name_id(self,name):
+ """
+ Return the Id for a name.
+ If it doesn't exist yet, a new entry is created.
+ """
+ if self.nameIdDict.has_key(name):
+ nameId = self.nameIdDict[name]
+ else:
+ self.nameIdDict[name] = self.maxNameId
+ self.idNameDict[self.maxNameId] = name
+ nameId = self.maxNameId
+ self.maxNameId += 1
+ self.changed = True
+ return nameId
+
+ def add_feature(self,featureName):
+ if not self.featureIdDict.has_key(featureName):
+ self.featureIdDict[featureName] = self.maxFeatureId
+ self.maxFeatureId += 1
+ self.changed = True
+
+ def expand_accessibles(self,acc):
+ accessibles = set(acc)
+ unexpandedQueue = Queue()
+ for a in acc:
+ if self.expandedAccessibles.has_key(a):
+ accessibles = accessibles.union(self.expandedAccessibles[a])
+ else:
+ unexpandedQueue.put(a)
+ while not unexpandedQueue.empty():
+ nextUnExp = unexpandedQueue.get()
+ nextUnExpAcc = self.accessibleDict[nextUnExp]
+ for a in nextUnExpAcc:
+ if not a in accessibles:
+ accessibles = accessibles.union([a])
+ if self.expandedAccessibles.has_key(a):
+ accessibles = accessibles.union(self.expandedAccessibles[a])
+ else:
+ unexpandedQueue.put(a)
+ return list(accessibles)
+
+ def parse_fact(self,line):
+ """
+ Parses a single line, extracting accessibles, features, and dependencies.
+ """
+ assert line.startswith('! ')
+ line = line[2:]
+
+ # line = name:accessibles;features;dependencies
+ line = line.split(':')
+ name = line[0].strip()
+ nameId = self.get_name_id(name)
+
+ line = line[1].split(';')
+ # Accessible Ids
+ unExpAcc = [self.nameIdDict[a.strip()] for a in line[0].split()]
+ self.accessibleDict[nameId] = unExpAcc
+ # Feature Ids
+ featureNames = [f.strip() for f in line[1].split()]
+ for fn in featureNames:
+ self.add_feature(fn)
+ self.featureDict[nameId] = [self.featureIdDict[fn] for fn in featureNames]
+ self.dependenciesDict[nameId] = [self.nameIdDict[d.strip()] for d in line[2].split()]
+ self.changed = True
+ return nameId
+
+ def parse_overwrite(self,line):
+ """
+ Parses a single line, extracts the problemId and the Ids of the dependencies.
+ """
+ assert line.startswith('p ')
+ line = line[2:]
+
+ # line = name:dependencies
+ line = line.split(':')
+ name = line[0].strip()
+ nameId = self.get_name_id(name)
+
+ dependencies = [self.nameIdDict[d.strip()] for d in line[1].split()]
+ self.changed = True
+ return nameId,dependencies
+
+ def parse_problem(self,line):
+ """
+ Parses a problem and returns the features and the accessibles.
+ """
+ assert line.startswith('? ')
+ line = line[2:]
+ name = None
+
+ # Check whether there is a problem name:
+ tmp = line.split(':')
+ if len(tmp) == 2:
+ name = tmp[0].strip()
+ line = tmp[1]
+
+ # line = accessibles;features
+ line = line.split(';')
+ # Accessible Ids, expand and store the accessibles.
+ unExpAcc = [self.nameIdDict[a.strip()] for a in line[0].split()]
+ if len(self.expandedAccessibles.keys())>=100:
+ self.expandedAccessibles = {}
+ self.changed = True
+ for accId in unExpAcc:
+ if not self.expandedAccessibles.has_key(accId):
+ accIdAcc = self.accessibleDict[accId]
+ self.expandedAccessibles[accId] = self.expand_accessibles(accIdAcc)
+ self.changed = True
+ accessibles = self.expand_accessibles(unExpAcc)
+ # Feature Ids
+ featureNames = [f.strip() for f in line[1].split()]
+ for fn in featureNames:
+ self.add_feature(fn)
+ features = [self.featureIdDict[fn] for fn in featureNames]
+ return name,features,accessibles
+
+ def save(self,fileName):
+ if self.changed:
+ dictsStream = open(fileName, 'wb')
+ dump((self.accessibleDict,self.dependenciesDict,self.expandedAccessibles,self.featureDict,\
+ self.featureIdDict,self.idNameDict,self.maxFeatureId,self.maxNameId,self.nameIdDict),dictsStream)
+ self.changed = False
+ dictsStream.close()
+ def load(self,fileName):
+ dictsStream = open(fileName, 'rb')
+ self.accessibleDict,self.dependenciesDict,self.expandedAccessibles,self.featureDict,\
+ self.featureIdDict,self.idNameDict,self.maxFeatureId,self.maxNameId,self.nameIdDict = load(dictsStream)
+ self.changed = False
+ dictsStream.close()
+
+
\ No newline at end of file