Implement Constraint Independence.

[feliam]

Many constraints do not overlap in terms of the memory they reference. Constraint independence divides constraint sets into disjoint independent subsets based on the symbolic variables and memory cells they reference. By explicitly tracking these subsets, it can frequently eliminate irrelevant constraints prior to sending it to the solver. For example, given the constraint set {i < j, j < 20, k > 0}, a query of whether i = 20 just requires the first two constraints.

We need tests for the implemented bit related to this feature:

manticore/manticore/core/smtlib/constraints.py

Lines 85 to 117 in 98190d8

	def __get_related(self, related_to=None):
	if related_to is not None:
	number_of_constraints = len(self.constraints)
	remaining_constraints = set(self.constraints)
	related_variables = get_variables(related_to)
	related_constraints = set()
	added = True
	while added:
	added = False
	logger.debug('Related variables %r', [x.name for x in related_variables])
	for constraint in list(remaining_constraints):
	if isinstance(constraint, BoolConstant):
	if constraint.value:
	continue
	else:
	related_constraints = {constraint}
	break
	variables = get_variables(constraint)
	if related_variables & variables:
	remaining_constraints.remove(constraint)
	related_constraints.add(constraint)
	related_variables |= variables
	added = True
	logger.debug('Reduced %d constraints!!', number_of_constraints - len(related_constraints))
	else:
	related_variables = set()
	for constraint in self.constraints:
	related_variables |= get_variables(constraint)
	related_constraints = set(self.constraints)
	return related_variables, related_constraints

And research the possibility of doing the same thing for not overlapping array references.
If you have constraints over the first half of the memory that are never related to the constraints that work over the second half of the memory you could send only half the memory array to the solver at certain situations.

• This should be configurable using config.py
• Overall symbolic execution performance gain should be measure/tested over a big test set (see Put together a large set of contract examples #1204)