src/HOL/Library/Sum_Of_Squares/neos_csdp_client
author hellerar
Thu, 02 Sep 2010 15:36:15 +0200
changeset 39095 f92b7e2877c2
parent 32542 e37c0ddf257e
permissions -rwxr-xr-x
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
     1
#!/usr/bin/env python
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
     2
import sys
32362
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
     3
import signal
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
     4
import xmlrpclib
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
     5
import time
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
     6
import re
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
     7
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
     8
# Neos server config
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
     9
NEOS_HOST="neos.mcs.anl.gov"
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    10
NEOS_PORT=3332
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    11
32542
e37c0ddf257e fixed cleanup routine in neos csdp script
Philipp Meyer
parents: 32362
diff changeset
    12
neos=xmlrpclib.Server("http://%s:%d" % (NEOS_HOST, NEOS_PORT))
e37c0ddf257e fixed cleanup routine in neos csdp script
Philipp Meyer
parents: 32362
diff changeset
    13
32362
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    14
jobNumber = 0
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    15
password = ""
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    16
inputfile = None
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    17
outputfile = None
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    18
# interrupt handler
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    19
def cleanup(signal, frame):
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    20
  sys.stdout.write("Caught interrupt, cleaning up\n")
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    21
  if jobNumber != 0:
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    22
    neos.killJob(jobNumber, password)
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    23
  if inputfile != None:
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    24
    inputfile.close()
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    25
  if outputfile != None:
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    26
    outputfile.close()
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    27
  sys.exit(21)
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    28
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    29
signal.signal(signal.SIGHUP, cleanup)
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    30
signal.signal(signal.SIGINT, cleanup)
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    31
signal.signal(signal.SIGQUIT, cleanup)
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    32
signal.signal(signal.SIGTERM, cleanup)
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    33
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    34
if len(sys.argv) <> 3:
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    35
  sys.stderr.write("Usage: neos_csdp_client <input_filename> <output_filename>\n")
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    36
  sys.exit(19)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    37
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    38
xml_pre = "<document>\n<category>sdp</category>\n<solver>csdp</solver>\n<inputMethod>SPARSE_SDPA</inputMethod>\n<dat><![CDATA["
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    39
xml_post = "]]></dat>\n</document>\n"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    40
xml = xml_pre
32362
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    41
inputfile = open(sys.argv[1],"r")
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    42
buffer = 1
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    43
while buffer:
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    44
  buffer = inputfile.read()
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    45
  xml += buffer
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    46
inputfile.close()
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    47
xml += xml_post
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    48
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    49
(jobNumber,password) = neos.submitJob(xml)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    50
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    51
if jobNumber == 0:
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    52
  sys.stdout.write("error submitting job: %s" % password)
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    53
  sys.exit(20)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    54
else:
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    55
  sys.stdout.write("jobNumber = %d\tpassword = %s\n" % (jobNumber,password))
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    56
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    57
offset=0
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    58
messages = ""
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    59
status="Waiting"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    60
while status == "Running" or status=="Waiting":
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    61
  time.sleep(1)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    62
  (msg,offset) = neos.getIntermediateResults(jobNumber,password,offset)
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    63
  messages += msg.data
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    64
  sys.stdout.write(msg.data)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    65
  status = neos.getJobStatus(jobNumber, password)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    66
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    67
msg = neos.getFinalResults(jobNumber, password).data
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    68
sys.stdout.write("---------- Begin CSDP Output -------------\n");
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    69
sys.stdout.write(msg)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    70
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    71
# extract solution
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    72
result = msg.split("Solution:")
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    73
if len(result) > 1:
32362
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    74
  solution = result[1].strip()
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
    75
  if solution != "":
32542
e37c0ddf257e fixed cleanup routine in neos csdp script
Philipp Meyer
parents: 32362
diff changeset
    76
    outputfile = open(sys.argv[2],"w")
e37c0ddf257e fixed cleanup routine in neos csdp script
Philipp Meyer
parents: 32362
diff changeset
    77
    outputfile.write(solution)
e37c0ddf257e fixed cleanup routine in neos csdp script
Philipp Meyer
parents: 32362
diff changeset
    78
    outputfile.close()
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    79
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    80
# extract return code
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    81
p = re.compile(r"^Error: Command exited with non-zero status (\d+)$", re.MULTILINE)
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    82
m = p.search(messages)
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    83
if m:
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    84
  sys.exit(int(m.group(1)))
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    85
else:
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    86
  sys.exit(0)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    87