Portfolio of parallel solvers

[ggrieco-tob]

This PR contains:

• A new meta solver called portfolio, that runs several solvers in parallel. Once one solver wins the race, the other ones are stopped, since there is no way to use their results in a meaningful way.
• As expected, the number of workers is adjusted when using the portfolio to avoid using more than core.procs processes.
• A new recv implementation based on non-blocking reads from the stdout pipe. I'm still experimenting how each to increase each timeout to avoid busy waiting.
• All the installed solvers but z3 are going to be used in the portfolio. I excluded z3 because I suspect it's the slowest one in almost all the tests but I need some more hard evidence. I'm tracking this in Collect some benchmark data and determinate the best smt solver to use/recommend #2449.
• Fixes for smtlib2 tests with multiple solvers use z3 almost always #2421

[feliam]

Put the config of each solver in each solver class?

[ehennenfent]

As Felipe points out, it'd probably be easier to set some abstract defaults on the Solver class. You could use abc.abstractproperty on Solver and override it on YicesSolver, Z3Solver, etc.

[ggrieco-tob]

I believe we cannot use abstract classes here since we need the command line for each solver and they depend on global options. For instance, "{consts.z3_bin} -t:{consts.timeout * 1000} -memory:{consts.memory} -smt2 -in depends on consts.z3_bin and consts.timeout, and consts.timeout which are going to be computed when the command line options are parsed.

[ehennenfent]

From our discussion this morning, I see what you mean now. The issue you've encountered is that when Manticore starts up, the following happens:

• The config module is loaded, and default values set for the values therein
• The solver module is loaded, and the types contained there are created
• The command line options are parsed (or a user script runs), setting the config values accordingly.

That means that if you try to define the solver commands on the solver type, like this:

class BoolectorSolver(SMTLIBSolver):
    command = f"{consts.boolector_bin} --time={consts.timeout} -i"
    inits = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]

then values pulled from consts will have their initial, default values, not whatever the user wanted them to be.

So instead, your solution is to create a SolverInfo object that pulls the values from the config module when it's created, and create one of these SolverInfo objects in the __init__ function of each of the solvers. While this works (and there's something to be said for having all the SMT commands in one location), I do agree with Felipe that it simplifies the code to distribute the commands onto the relevant classes.

The problem ultimately boils down to: you don't want to generate the commands to start the solver until they're needed. Fortunately, this is one of the problems that properties were designed to solve, since they're dynamically evaluated each time they're retrieved instead of being assigned a single value.

So, to split up SolverInfo, you could do something like this:

class SMTLIBSolver(Solver):

    @property
    @abstractmethod
    def command(self) -> str:
        raise NotImplementedError()

    @property
    @abstractmethod
    def inits(self) -> typing.List[str]:
        raise NotImplementedError()

    ...


class BoolectorSolver(SMTLIBSolver):
    sname = "boolector"

    @property
    def command(self) -> str:
        return f"{consts.boolector_bin} --time={consts.timeout} -i"

    @property
    def inits(self) -> typing.List[str]:
        return ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]

    ...

And then in SMTLIBSolver.__init__ you would be able to retrieve self.command and self.inits and know that their values would accurately reflect the contents of the config module at that time, not at the time the type was created.

[ggrieco-tob]

I followed your advise, but instead of using a property, I had to use a classmethod. That was the only way to allow to call command and inits from the class, without actually create an instance the solvers. Please take a look to my recent changes.

[ehennenfent]

As Felipe points out, it'd probably be easier to set some abstract defaults on the Solver class. You could use abc.abstractproperty on Solver and override it on YicesSolver, Z3Solver, etc.

[ekilmer]

Exciting PR!

[ekilmer]

Looks good on my end, but there are still comments from other people that should be resolved first before merging. Thank you!!