src/HOL/Library/Sum_Of_Squares/neos_csdp_client

misc changes to SOS by Philipp Meyer:
CSDP_EXE as central setting;
separate component src/HOL/Library/Sum_Of_Squares;
misc tuning and rearrangement of neos_csdp_client;
more robust treatment of shell paths;
debugging depends on local flag;
removed unused parts;

#!/usr/bin/env python
import sys
import xmlrpclib
import time
import re

# Neos server config
NEOS_HOST="neos.mcs.anl.gov"
NEOS_PORT=3332

if len(sys.argv) < 3 or len(sys.argv) > 3:
  sys.stderr.write("Usage: NeosCSDPClient <input_filename> <output_filename>\n")
  sys.exit(1)

neos=xmlrpclib.Server("http://%s:%d" % (NEOS_HOST, NEOS_PORT))

inputfile = open(sys.argv[1],"r")
xml_pre = "<document>\n<category>sdp</category>\n<solver>csdp</solver>\n<inputMethod>SPARSE_SDPA</inputMethod>\n<dat><![CDATA["
xml_post = "]]></dat>\n</document>\n"
xml = xml_pre
buffer = 1
while buffer:
  buffer = inputfile.read()
  xml += buffer
inputfile.close()
xml += xml_post

(jobNumber,password) = neos.submitJob(xml)

if jobNumber == 0:
  sys.stdout.write("error submitting job: %s" % password)
  sys.exit(20)
else:
  sys.stdout.write("jobNumber = %d\tpassword = %s\n" % (jobNumber,password))

offset=0
messages = ""
status="Waiting"
while status == "Running" or status=="Waiting":
  time.sleep(1)
  (msg,offset) = neos.getIntermediateResults(jobNumber,password,offset)
  messages += msg.data
  sys.stdout.write(msg.data)
  status = neos.getJobStatus(jobNumber, password)

msg = neos.getFinalResults(jobNumber, password).data
sys.stdout.write("---------- Begin CSDP Output -------------\n");
sys.stdout.write(msg)

# extract solution
result = msg.split("Solution:")
if len(result) > 1:
  output = open(sys.argv[2],"w")
  output.write(result[1].strip())
  output.close()

# extract return code
p = re.compile(r"^Error: Command exited with non-zero status (\d+)$", re.MULTILINE)
m = p.search(messages)
if m:
  sys.exit(int(m.group(1)))
else:
  sys.exit(0)