Solver policies should be global constants (like C enums)

[pgoodman]

Summary of the problem

Right now manticore uses strings to represent solver policies. For example, there is MINMAX, etc. These are encoded in the Concretize._ValidPolicies list. These should really be named constants with numeric values, and they should be more uniformly used.

For example, the solve_n method of the State class has minmax as its policy, and it's not clear if that default policy is even possible or meaningful.

    def solve_n(self, expr, nsolves, policy='minmax'):

[feliam]

The api description of solve_n should describe all its preconditions/valid inputs.
Ideally the user facing string representation of the policies should be defined in a single place.
Numeric constants do not provide any improvement over constant strings. String constants are more human readable. You can but you do not really need to import any module to use them by name.
Internally a string constant is a number.

I do not mind if there is a module somewhere with a bunch of constants defined

ALL_POLICY = "ALL"
MINMAX_POLICY = "MINMAX"

Full disclosure, I'll use "MINMAX" instead of from modulex import MINMAX_POLICY; MINMAX_POLICY

[offlinemark]

I agree that we should have a module with constants for policies, and strictly use only it. I think it's less important whether to use strings to ints, but strings make it more tempting to not use the constants.

regardless, @pgoodman raised an excellent point that solve_n with minmax doesn't make sense. honestly, those State solve APIs need a total rework, the existence of both solve_one, and solve_n is poor design and was a big mistake on my part (i made them originally)

[feliam]

Let's do not get strict. I vote not to force users to import stuff just to do a small script.
Slow but forgiving is better than slow and strict.
I normally use solver.get_all_values or solver.get_value.

[offlinemark]

could we make the constants available through class variables, so no import is needed?

class Manticore:
  SOLVER_MINMAX = qwer
  SOLVER_ALL = zxcv
  SOLVER_SAMPLED = asdf

then users could easily use them without import, with tab-complete in their editor/ide, with equal readability to strings.

the downside is that the Manticore class is not the right place for those constants.

[feliam]

    class Policy():
        ALL = 'ALL'
        ONE = 'ONE'
        MINMAX = 'MINMAX'

        @staticmethod
        def check(x):
            d = Policy.__dict__
            return x in [name for name in d.keys() if d[name] == name]
                

    print Policy.check('ALL')
    print Policy.check(Policy.ALL)

[ehennenfent]

https://github.com/trailofbits/manticore/wiki/Ideas

[pgoodman]

In retrospect, I think policies should actually be functions or classes, not enums.