src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
changeset 53152 cbd3c7c48d2c
parent 53119 ac18480cbf9d
child 53555 12251bc889f1
equal deleted inserted replaced
53151:fbf4d50dec91 53152:cbd3c7c48d2c
   101         logger.info('Initializing Server.')
   101         logger.info('Initializing Server.')
   102         data = "i "+";".join(argv)
   102         data = "i "+";".join(argv)
   103         received = communicate(data,args.host,args.port)
   103         received = communicate(data,args.host,args.port)
   104         logger.info(received)     
   104         logger.info(received)     
   105     
   105     
   106     if args.inputFile == None:
   106     if not args.inputFile == None:
   107         return
   107         logger.debug('Using the following settings: %s',args)
   108     logger.debug('Using the following settings: %s',args)
   108         # IO Streams
   109     # IO Streams
   109         OS = open(args.predictions,'w')
   110     OS = open(args.predictions,'w')
   110         IS = open(args.inputFile,'r')
   111     IS = open(args.inputFile,'r')
   111         lineCount = 0
   112     lineCount = 0
   112         for line in IS:
   113     for line in IS:
   113             lineCount += 1
   114         lineCount += 1
   114             if lineCount % 100 == 0:
   115         if lineCount % 100 == 0:
   115                 logger.info('On line %s', lineCount)
   116             logger.info('On line %s', lineCount)
   116             received = communicate(line,args.host,args.port)
   117         #if lineCount == 50: ###
   117             if not received == '':
   118         #    break       
   118                 OS.write('%s\n' % received)
   119         received = communicate(line,args.host,args.port)
   119         OS.close()
   120         if not received == '':
   120         IS.close()
   121             OS.write('%s\n' % received)
       
   122     OS.close()
       
   123     IS.close()
       
   124 
   121 
   125     # Statistics
   122     # Statistics
   126     if args.statistics:
   123     if args.statistics:
   127         received = communicate('avgStats',args.host,args.port)
   124         received = communicate('avgStats',args.host,args.port)
   128         logger.info(received)
   125         logger.info(received)
   129     elif args.saveModels:
   126     if args.saveModels:
   130         communicate('save',args.host,args.port)
   127         communicate('save',args.host,args.port)
   131 
   128 
   132 
   129 
   133 if __name__ == "__main__":
   130 if __name__ == "__main__":
   134     sys.exit(mash())
   131     sys.exit(mash())