src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
changeset 53115 e08a58161bf1
parent 53100 1133b9e83f09
child 53119 ac18480cbf9d
equal deleted inserted replaced
53114:4c2b1e64c990 53115:e08a58161bf1
    33 def communicate(data,host,port):
    33 def communicate(data,host,port):
    34     sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
    34     sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
    35     try:
    35     try:
    36         sock.connect((host,port))
    36         sock.connect((host,port))
    37         sock.sendall(data)
    37         sock.sendall(data)
    38         received = sock.recv(262144)
    38         received = sock.recv(4194304)
    39     except:
    39     except:
    40         logger = logging.getLogger('communicate')
    40         logger = logging.getLogger('communicate')
    41         logger.warning('Communication with server failed.')
    41         logger.warning('Communication with server failed.')
    42         received = -1
    42         received = -1
    43     finally:
    43     finally:
    67         logging.getLogger('').addHandler(console)
    67         logging.getLogger('').addHandler(console)
    68         
    68         
    69     if not os.path.exists(args.outputDir):
    69     if not os.path.exists(args.outputDir):
    70         os.makedirs(args.outputDir)
    70         os.makedirs(args.outputDir)
    71 
    71 
       
    72     # Shutdown commands need not start the server fist.
       
    73     if args.shutdownServer:
       
    74         try:
       
    75             communicate('shutdown',args.host,args.port)
       
    76         except:
       
    77             pass
       
    78         return
       
    79 
    72     # If server is not running, start it.
    80     # If server is not running, start it.
       
    81     startedServer = False
    73     try:
    82     try:
    74         sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
    83         sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
    75         sock.connect((args.host,args.port))       
    84         sock.connect((args.host,args.port))       
    76         sock.close()
    85         sock.close()
    77     except:
    86     except:
    78         logger.info('Starting Server.')
    87         logger.info('Starting Server.')
    79         spawnDaemon('server.py')
    88         spawnDaemon('server.py')
    80         # TODO: Make this fault tolerant
    89         # TODO: Make this fault tolerant
    81         time.sleep(0.5)
    90         time.sleep(0.5)
    82         # Init server
    91         startedServer = True
       
    92         
       
    93     if args.init or startedServer:
       
    94         logger.info('Initializing Server.')
    83         data = "i "+";".join(argv)
    95         data = "i "+";".join(argv)
    84         received = communicate(data,args.host,args.port)
    96         received = communicate(data,args.host,args.port)
    85         logger.info(received)     
    97         logger.info(received)     
    86     
    98     
    87     if args.inputFile == None:
    99     if args.inputFile == None:
    88         return
   100         return
    89     logger.debug('Using the following settings: %s',args)
   101     logger.debug('Using the following settings: %s',args)
    90     # IO Streams
   102     # IO Streams
    91     OS = open(args.predictions,'w')
   103     OS = open(args.predictions,'w')
    92     IS = open(args.inputFile,'r')
   104     IS = open(args.inputFile,'r')
    93     count = 0
   105     for line in IS:    
    94     for line in IS:
       
    95         count += 1
       
    96         #if count == 127:
       
    97         #    break as       
       
    98         received = communicate(line,args.host,args.port)
   106         received = communicate(line,args.host,args.port)
    99         if not received == '':
   107         if not received == '':
   100             OS.write('%s\n' % received)
   108             OS.write('%s\n' % received)
   101         #logger.info(received)
       
   102     OS.close()
   109     OS.close()
   103     IS.close()
   110     IS.close()
   104 
   111 
   105     # Statistics
   112     # Statistics
   106     if args.statistics:
   113     if args.statistics:
   107         received = communicate('avgStats',args.host,args.port)
   114         received = communicate('avgStats',args.host,args.port)
   108         logger.info(received)
   115         logger.info(received)
       
   116     elif args.saveModels:
       
   117         communicate('save',args.host,args.port)
   109 
   118 
   110 
   119 
   111 if __name__ == "__main__":
   120 if __name__ == "__main__":
   112     sys.exit(mash())
   121     sys.exit(mash())