--- a/src/HOL/Tools/Sledgehammer/MaSh/src/readData.py Thu Sep 12 00:34:48 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/readData.py Thu Sep 12 09:59:45 2013 +0200
@@ -14,55 +14,6 @@
import sys,logging
-def create_feature_dict(nameIdDict,idNameDict,maxNameId,featureIdDict,maxFeatureId,featureCountDict,\
- triggerFeaturesDict,featureTriggeredFormulasDict,sineFeatures,inputFile):
- logger = logging.getLogger('create_feature_dict')
- featureDict = {}
- IS = open(inputFile,'r')
- for line in IS:
- line = line.split(':')
- name = line[0]
- # Name Id
- if nameIdDict.has_key(name):
- logger.warning('%s appears twice in the feature file. Aborting.',name)
- sys.exit(-1)
- else:
- nameIdDict[name] = maxNameId
- idNameDict[maxNameId] = name
- nameId = maxNameId
- maxNameId += 1
- # Feature Ids
- featureNames = [f.strip() for f in line[1].split()]
- features = []
- minFeatureCount = 9999999
- for fn in featureNames:
- weight = 1.0
- tmp = fn.split('=')
- if len(tmp) == 2:
- fn = tmp[0]
- weight = float(tmp[1])
- if not featureIdDict.has_key(fn):
- featureIdDict[fn] = maxFeatureId
- featureCountDict[maxFeatureId] = 0
- maxFeatureId += 1
- fId = featureIdDict[fn]
- features.append((fId,weight))
- if sineFeatures:
- featureCountDict[fId] += 1
- minFeatureCount = min(minFeatureCount,featureCountDict[fId])
- # Store results
- featureDict[nameId] = features
- if sineFeatures:
- triggerFeatures = [f for f,_w in features if featureCountDict[f] == minFeatureCount]
- triggerFeaturesDict[nameId] = triggerFeatures
- for f in triggerFeatures:
- if featureTriggeredFormulasDict.has_key(f):
- featureTriggeredFormulasDict[f].append(nameId)
- else:
- featureTriggeredFormulasDict[f] = [nameId]
- IS.close()
- return featureDict,maxNameId,maxFeatureId,featureCountDict,triggerFeaturesDict,featureTriggeredFormulasDict
-
def create_dependencies_dict(nameIdDict,inputFile):
logger = logging.getLogger('create_dependencies_dict')
dependenciesDict = {}