src/HOL/Library/Sum_of_Squares/neos_csdp_client
author Christian Sternagel
Thu Dec 13 13:11:38 2012 +0100 (2012-12-13)
changeset 50516 ed6b40d15d1c
parent 41947 0b8a13b145e9
permissions -rwxr-xr-x
renamed "emb" to "list_hembeq";
make "list_hembeq" reflexive independent of the base order;
renamed "sub" to "sublisteq";
dropped "transp_on" (state transitivity explicitly instead);
no need to hide "sub" after renaming;
replaced some ASCII symbols by proper Isabelle symbols;
NEWS
Philipp@32268
     1
#!/usr/bin/env python
Philipp@32268
     2
import sys
Philipp@32362
     3
import signal
Philipp@32268
     4
import xmlrpclib
Philipp@32268
     5
import time
Philipp@32268
     6
import re
wenzelm@41475
     7
import os
Philipp@32268
     8
wenzelm@32332
     9
# Neos server config
wenzelm@41947
    10
neos = xmlrpclib.Server(os.getenv("ISABELLE_NEOS_SERVER"))
Philipp@32542
    11
Philipp@32362
    12
jobNumber = 0
Philipp@32362
    13
password = ""
Philipp@32362
    14
inputfile = None
Philipp@32362
    15
outputfile = None
Philipp@32362
    16
# interrupt handler
Philipp@32362
    17
def cleanup(signal, frame):
Philipp@32362
    18
  sys.stdout.write("Caught interrupt, cleaning up\n")
Philipp@32362
    19
  if jobNumber != 0:
Philipp@32362
    20
    neos.killJob(jobNumber, password)
Philipp@32362
    21
  if inputfile != None:
Philipp@32362
    22
    inputfile.close()
Philipp@32362
    23
  if outputfile != None:
Philipp@32362
    24
    outputfile.close()
Philipp@32362
    25
  sys.exit(21)
Philipp@32362
    26
Philipp@32362
    27
signal.signal(signal.SIGHUP, cleanup)
Philipp@32362
    28
signal.signal(signal.SIGINT, cleanup)
Philipp@32362
    29
signal.signal(signal.SIGQUIT, cleanup)
Philipp@32362
    30
signal.signal(signal.SIGTERM, cleanup)
Philipp@32362
    31
Philipp@32362
    32
if len(sys.argv) <> 3:
Philipp@32362
    33
  sys.stderr.write("Usage: neos_csdp_client <input_filename> <output_filename>\n")
Philipp@32362
    34
  sys.exit(19)
Philipp@32268
    35
Philipp@32268
    36
xml_pre = "<document>\n<category>sdp</category>\n<solver>csdp</solver>\n<inputMethod>SPARSE_SDPA</inputMethod>\n<dat><![CDATA["
Philipp@32268
    37
xml_post = "]]></dat>\n</document>\n"
Philipp@32268
    38
xml = xml_pre
Philipp@32362
    39
inputfile = open(sys.argv[1],"r")
Philipp@32268
    40
buffer = 1
Philipp@32268
    41
while buffer:
wenzelm@32332
    42
  buffer = inputfile.read()
Philipp@32268
    43
  xml += buffer
wenzelm@32332
    44
inputfile.close()
Philipp@32268
    45
xml += xml_post
Philipp@32268
    46
Philipp@32268
    47
(jobNumber,password) = neos.submitJob(xml)
Philipp@32268
    48
Philipp@32268
    49
if jobNumber == 0:
Philipp@32268
    50
  sys.stdout.write("error submitting job: %s" % password)
wenzelm@32332
    51
  sys.exit(20)
Philipp@32268
    52
else:
Philipp@32268
    53
  sys.stdout.write("jobNumber = %d\tpassword = %s\n" % (jobNumber,password))
Philipp@32268
    54
Philipp@32268
    55
offset=0
wenzelm@32332
    56
messages = ""
Philipp@32268
    57
status="Waiting"
Philipp@32268
    58
while status == "Running" or status=="Waiting":
Philipp@32268
    59
  time.sleep(1)
Philipp@32268
    60
  (msg,offset) = neos.getIntermediateResults(jobNumber,password,offset)
wenzelm@32332
    61
  messages += msg.data
Philipp@32268
    62
  sys.stdout.write(msg.data)
Philipp@32268
    63
  status = neos.getJobStatus(jobNumber, password)
Philipp@32268
    64
Philipp@32268
    65
msg = neos.getFinalResults(jobNumber, password).data
wenzelm@32332
    66
sys.stdout.write("---------- Begin CSDP Output -------------\n");
wenzelm@32332
    67
sys.stdout.write(msg)
Philipp@32268
    68
wenzelm@32332
    69
# extract solution
wenzelm@32332
    70
result = msg.split("Solution:")
Philipp@32268
    71
if len(result) > 1:
Philipp@32362
    72
  solution = result[1].strip()
Philipp@32362
    73
  if solution != "":
Philipp@32542
    74
    outputfile = open(sys.argv[2],"w")
Philipp@32542
    75
    outputfile.write(solution)
Philipp@32542
    76
    outputfile.close()
Philipp@32268
    77
wenzelm@32332
    78
# extract return code
wenzelm@32332
    79
p = re.compile(r"^Error: Command exited with non-zero status (\d+)$", re.MULTILINE)
wenzelm@32332
    80
m = p.search(messages)
wenzelm@32332
    81
if m:
wenzelm@32332
    82
  sys.exit(int(m.group(1)))
wenzelm@32332
    83
else:
wenzelm@32332
    84
  sys.exit(0)
Philipp@32268
    85