112 lines
3.8 KiB
Python
Executable File
112 lines
3.8 KiB
Python
Executable File
#!/usr/bin/env python3
|
|
import json
|
|
import logging
|
|
import os
|
|
import subprocess
|
|
import sys
|
|
import threading
|
|
|
|
logging.basicConfig(format='%(asctime)s - %(name)s - %(levelname)s - %(message)s')
|
|
|
|
class Runner:
|
|
def __init__(self, request_directory: str):
|
|
self.logger = logging.getLogger("Runner")
|
|
self.logger.setLevel(logging.INFO)
|
|
self.request_directory = request_directory
|
|
os.environ['PYTHONUNBUFFERED'] = "1"
|
|
|
|
def process_stream(self, stream, str_name, file_handle):
|
|
line = stream.readline()
|
|
while line != "":
|
|
self.logger.info(f"{str_name}: {line}")
|
|
file_handle.write(line)
|
|
line = stream.readline()
|
|
|
|
def run(self, cmd: list):
|
|
self.logger.info("Running command: %s", str(cmd))
|
|
|
|
stdout_target_loc = os.path.join(self.request_directory, "stdout.log")
|
|
stderr_target_loc = os.path.join(self.request_directory, "stderr.log")
|
|
|
|
with open(stdout_target_loc, "w") as stdout_handle:
|
|
with open(stderr_target_loc, "w") as stderr_handle:
|
|
proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE,
|
|
universal_newlines=True, start_new_session=True)
|
|
stdout_t = threading.Thread(target = self.process_stream, args=(proc.stdout, "STDOUT", stdout_handle))
|
|
stderr_t = threading.Thread(target = self.process_stream, args=(proc.stderr, "STDERR", stderr_handle))
|
|
stdout_t.start()
|
|
stderr_t.start()
|
|
return_code = proc.wait()
|
|
stdout_t.join()
|
|
stderr_t.join()
|
|
|
|
return {
|
|
"stdout": stdout_target_loc,
|
|
"stderr": stderr_target_loc,
|
|
"return_code": return_code,
|
|
"output_directory": self.request_directory
|
|
}
|
|
|
|
def get_input_json(self):
|
|
input = os.path.join(self.request_directory, "input.json")
|
|
with open(input) as f:
|
|
return json.loads(f.read())
|
|
|
|
def create_hostfile(self,ips, request_dir):
|
|
hostfile_path = os.path.join(request_dir, 'combined_hostfile')
|
|
with open(hostfile_path, 'w+') as f:
|
|
for ip in ips:
|
|
f.write(f'{ip} slots=1') # distributed default
|
|
f.write('\n')
|
|
return hostfile_path
|
|
|
|
def get_command(self, input_json):
|
|
formula_file = input_json.get("formula_file")
|
|
worker_node_ips = input_json.get("worker_node_ips", [])
|
|
|
|
combined_hostfile = self.create_hostfile(worker_node_ips, self.request_directory)
|
|
|
|
run_list = ["/competition/run_solver.sh"]
|
|
run_list.append(combined_hostfile)
|
|
run_list.append(formula_file)
|
|
|
|
return run_list
|
|
|
|
class MallobParser:
|
|
@staticmethod
|
|
def get_result(output_file):
|
|
"""
|
|
TODO: Participants should replace this with something more robust for their own solver!
|
|
"""
|
|
with open(output_file) as f:
|
|
raw_logs = f.read()
|
|
if "s UNSAT" in raw_logs:
|
|
return 20
|
|
elif "s SAT" in raw_logs:
|
|
return 10
|
|
elif "s UNKNOWN" in raw_logs:
|
|
return 0
|
|
else:
|
|
return -1
|
|
|
|
if __name__ == "__main__":
|
|
request_directory = sys.argv[1]
|
|
runner = Runner(request_directory)
|
|
|
|
input_json = runner.get_input_json()
|
|
cmd = runner.get_command(input_json)
|
|
|
|
print (f"cmd: {cmd}")
|
|
output = runner.run(cmd)
|
|
result = MallobParser.get_result(output["stdout"])
|
|
logging.info(f"RESULT: {result}")
|
|
solver_output = {
|
|
"return_code": result,
|
|
"artifacts": {
|
|
"stdout_path": output["stdout"],
|
|
"stderr_path": output["stderr"]
|
|
}
|
|
}
|
|
|
|
with open(os.path.join(request_directory, "solver_out.json"), "w+") as f:
|
|
f.write(json.dumps(solver_output)) |