Perform z3.simplify() in z3_visitor.py

[Raine-Yang-UofT]

Currently, the set_function_def_z3_constraints function in z3_visitor.py evaluates the z3 constraints for each function precondition and directly combine them as the z3_constraints attribute of the FunctionDef node. We may be able to call z3.simplify() on the list of constraints in the end to get an equivalent and simplified constraints.

Proposed Change:

After evaluating and combining the Z3 constraints for each function precondition, call z3.simplify() on the list of constraints.
Assign the simplified constraints back to the z3_constraints attribute of the FunctionDef node.

Code Example:

def set_function_def_z3_constraints(self, node: nodes.FunctionDef):
    ''' previous code omitted '''
    # Get z3 constraints
        z3_constraints = []
        for pre in preconditions:
            pre = astroid.parse(pre).body[0]
            ew = ExprWrapper(pre, types)
            try:
                transformed = ew.reduce()
            except (Z3Exception, Z3ParseException):
                transformed = None
            if transformed is not None:
                z3_constraints.append(transformed)

    # Simplify constraints
    z3_constraints = [z3.simplify(z3.And(*z3_constraints))]        

    # Set z3 constraints
    node.z3_constraints = z3_constraints
    return node