class ExternalSolver(SATSolver):
    def __init__(self, path):
        self.path = path

        args = shlex.split(self.path)
        self.proc = subprocess.Popen(args,
                                     stdin=subprocess.PIPE,
                                     stdout=subprocess.PIPE,
                                     stderr=subprocess.PIPE)

    def solve(self, formula):
        # Compose the formula to send
        dimacsFormula = getDIMACSFormula(formula)

        (outdata, errdata) = self.proc.communicate(dimacsFormula)


        if self.proc.returncode >= 0 and len(outdata) > 0:
            solFile = StringIO(outdata)
            solution = parseDIMACSSolution(solFile)
            return solution

    def abort(self):
        self.proc.kill()


class _PortfolioThread(Thread):
    def __init__(self, solver, formula, sem):
        Thread.__init__(self)

        self.solution = None
        self.solver = solver
        self.formula = formula
        self.sem = sem

    def run(self):
        self.solution = self.solver.solve(self.formula)
        self.sem.release()

class PortfolioSolver(SATSolver):
    def __init__(self, solvers):
        self.solvers = solvers

    def solve(self, formula):
        solverThreads = []
        solution = None

        sem = Semaphore(0)

        for solver in self.solvers:
            sThread = _PortfolioThread(solver, formula, sem)
            solverThreads.append(sThread)

            sThread.start()

        # Wait for at least one thread to finish
        sem.acquire()

        for sThread in solverThreads:
            if solution is None:
                if sThread.solution is not None:
                    solution = sThread.solution

            sThread.solver.abort()

        assert solution is not None, "Solver returned with invalid solution"

        for sThread in solverThreads:
            sThread.join()

        return solution

    def abort(self):
        pass