ReasonLS/sources/simp/pmaple.py

# -*- coding: utf-8 -*-
# reasonLS
# authors
#
# runs n instances of reasonLS in parallel (script code based on code of Norbert Manthey 2014)
#

# used libraries
import os, signal, subprocess, time
import sys, shutil, random, re 


def check_pid(pid):        
    """ Check For the existence of a unix pid. """
    try:
        os.kill(pid, 0)
    except OSError:
        return False
    else:
        return True

def kill_pid(pid):        
    """ Check For the existence of a unix pid. """
    try:
        os.kill(pid, 15)
    except OSError:
        return False
    else:
        return True


#
# usage and current PID
#
print ("c reasonLS SC18")
print ("c authors")
print ("c runs n instances of reasonLS in parallel")

if (len(sys.argv) < 4):
    print ("c usage: python pmapple.py <input.cnf> <seed> <numCores> [<proofFile>] [<tmpDirectory>]" ) #n is the number of instances to start
    sys.exit(0)
print ("c running with PID " + str(os.getpid()))

#
# Handle parameters
#
# get input file
#
inputFile = sys.argv[1]
seed = int(sys.argv[2])
numCores = int(sys.argv[3])
if (numCores == 1):
    print ("c does not make sense, please start reasonLS directly")
    sys.exit(0)

# set proof file
if (len(sys.argv) > 4):
    tmpProofz = sys.argv[4] 
    path_proof = tmpProofz[tmpProofz.find('drup-file=')+10:]
    pathz = os.path.dirname(path_proof)
    proof = os.path.basename(path_proof)
else:
    proof = "/dev/null"

#
# setup tmp files
#
tmpDir = "/tmp/"
print ("c found " + str(len(sys.argv)) + " parameters")
if (len(sys.argv) > 5):
    tmpDir = sys.argv[5]
if (tmpDir[-1:] != '/'):
    tmpDir = tmpDir + "/"

#construction of temporary files for output

# let user know that everything has been read correctly
print ("c starting " + str(numCores) + " instances of reasonLS with seed " + str(
    seed) + " on instance " + str(
        inputFile) + " \nc writing temp files to  " + tmpDir)

#
# start the two solvers, each in its private process group
#
random.seed(seed)
pids = set()
pidsseed = set()
seeds = set()
            #  1        2       3       4       5       6       7       8       9       10      11      12      13      14      15      16      17      18      19      20      21      22      23      24
confl       = [0.9,     0.9,    0.9,    0.9,    0.9,    0.9,    0.9,    0.1,    0.1,    0.1,    0.1,    0.1,    0.1,    0.1,    0.1,    0.1,    0.9,    0.7,    0.5,    0.9,    0.7,    0.5,    1,      1]
area        = [1.01,    1.01,   1.01,   1.01,   1.01,   1.01,   1.01,   1.01,   1,      1,      1,      1,      1,      1,      1,      1,      1.01,   1.05,   1.1,    1.01,   1.05,   1.1,    1.01,   1.01]
maxflip     = [600,     600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    600,    500,    600,    600,    500,    600,    600,    600,    600]
initflip    = [100,     100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    100,    50,     50,     50,     50,     50,     50,     100,    100]
raiseflip   = [1.02,    1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02,   1.02]
switch      = [2500,    2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   2500,   0,      0,      0,      0,      2500]
time        = [0.35,    0.35,   0.35,   0.35,   0.35,   0.35,   0.35,   0.35,   1.1,    1.1,    1.1,    1.1,    1.1,    1.1,    1.1,    1.1,    0.35,   0.45,   0.55,   0.35,   0.45,   0.55,   0.35,   0.35]
aspiration  = [1,       1,      1,      1,      0,      0,      0,      0,      1,      1,      1,      1,      0,      0,      0,      0,      1,      1,      1,      1,      1,      1,      1,      1]
threshold   = [50,      50,     300,    300,    50,     50,     300,    300,    50,     50,     300,    300,    50,     50,     300,    300,    50,     50,     50,     50,     50,     50,     50,     50]
q           = [0,       0.7,    0,      0.7,    0,      0.7,    0,      0.7,    0,      0.7,    0,      0.7,    0,      0.7,    0,      0.7,    0.7,    0.7,    0.7,    0.7,    0.7,    0.7,    0.7,    0.7]


tmpBassename = os.path.basename(inputFile)


for i in range(0, numCores):
    seed=random.randint(0,2147483647)
    tmpFile = tmpDir + tmpBassename + "reasonLS_" + str(seed)
    print ("c starting instance " + str(
        i) + " of reasonLS started with seed " + str(seed))
    print ("c writing to files " + tmpFile + ".out .err")
    # start reasonLS
    if (proof != "/dev/null"):
        tmpProof = tmpDir + tmpBassename + proof + "reasonLS_" + str(seed)
    else:
        tmpProof = proof
    reasonLSCallString = "./ReasonLS " + inputFile + " -drup-file=" + tmpProof  # add CNF file and tmp directory
    reasonLSCallString = reasonLSCallString + " -conflRatio=" + str(confl[i])     + " -areaRatio=" + str(area[i])
    reasonLSCallString = reasonLSCallString + " -maxFlipRatio=" + str(maxflip[i]) + " -initFlipRatio=" + str(initflip[i]) + " -raiseFlipRatio=" + str(raiseflip[i])
    reasonLSCallString = reasonLSCallString + " -timeRatio=" + str(time[i])       + " -switchMode=" +str(switch[i])
    reasonLSCallString = reasonLSCallString + " -swt_q=" + str(q[i])              + " -swt_threshold="+ str(threshold[i]) + " -aspiration=" +str(aspiration[i])

    args = reasonLSCallString.split()
    # split the actual command line
    print ("c calling reasonLS with " + str(args))
    reasonLSProcess = subprocess.Popen(
        args,
        stdout=open(tmpFile + ".out", "w"),
        stderr=open(tmpFile + ".err", "w"),
        preexec_fn=os.setpgrp)
    pidsseed.add((reasonLSProcess.pid, seed))
    pids.add(reasonLSProcess.pid)
    seeds.add(seed)
    print ("c started reasonLS instance with PID" + str(reasonLSProcess.pid))


# wait until the first solver returns
winner = ""
winnerCode = 0
while pids:
    pid, retval = os.wait()
    print ("c finished " + str(pid) + " with return value " + str(retval))
    pids.remove(pid)
    # extract the exit code
    signal = retval & 255
    exitCode = (retval >> 8) & 255
    print ("c signal: " + str(signal) + " exit code: " + str(exitCode))
    # if exit code is nice, select the winner
    winnerseed = -1
    if signal == 0 and (exitCode == 10 or exitCode == 20):
        winnerCode = exitCode  # get exit code
        for i in range(numCores):
            proc = pidsseed.pop()
            if proc[0] == pid:
                winnerseed = proc[1]
                break  # do not wait for the other process as well, if a solution has been found!
    if winnerseed != -1:
        break
#
# output the result
#
if winnerCode != 0:
    print ("c winner seed: " + str(winnerseed))
    tmpFile = tmpDir + tmpBassename + "reasonLS_" + str(winnerseed)
    # for more recent python versions:
    #	with open(tmpFile + ".out", "r") as f:

    # for the competition 2014 version:
    f = open(tmpFile + ".out", "r")
    if f:
        shutil.copyfileobj(f, sys.stdout)

    if (proof != "/dev/null"):
        tmpProof = tmpBassename + proof + "reasonLS_" + str(winnerseed)
        if( not os.path.exists(pathz) ):
            os.mkdir(pathz)
        if( os.path.exists(tmpDir+tmpProof)):
            os.system("cp " + tmpDir + tmpProof + " " + pathz + '/' +proof)
    

else:
    print ("s UNKNOWN")

# kill the other process, and its child processes
for p in pids:
    kill_pid(p)

# clean up the temporary files
for i in range(numCores):
    seed = seeds.pop()
    tmpFile = tmpDir + tmpBassename + "reasonLS_" + str(seed)
    if(os.path.exists(tmpFile + ".err")):    
        os.unlink(tmpFile + ".err")
    if(os.path.exists(tmpFile + ".out")):
        os.unlink(tmpFile + ".out")
    if(proof != "/dev/null"):
        tmpProof = tmpDir + tmpBassename + proof + "reasonLS_" + str(seed)
        #if(os.path.exists(tmpProof)):
        os.unlink(tmpProof)

# exit with the correct exit code
sys.exit(winnerCode)