Add a lightweight check for `requires` of equations when matching is indeterminate

When matching of a function equation is indeterminate, Booster will abort the application of this function. However, sometimes the requires clause of the same equation can fully instantiated with the determinate part of the matching substitution. If the instantiated requires clause is false, we are safe to conclude that the equation does not apply, and we can proceed to attempting other equations of this function.

@PetarMax suggests to tweak the algorithm of applying equations:

• when matching is indeterminate, extract the determinate part of the substitution
• if that is non-empty, apply it to the requires clause and simplify with LLVM
• if any of the conjuncts is false --- we are safe to conclude the equation does not apply

Notes:

• the result of the equation application can only become negative or remain indeterminate. There's no way we can apply the equation if matching is indeterminate
• it is critical to not call the SMT solver on this requires clause, as it may introduce a massive performance regression. That's why we restrict ourselves to a concrete LLVM simplification and simplify the requires clause recursively with other equations.

Locate the algorithm that applies function equations and handles indeterminate matching. Trace how determinate substitutions reach requires clauses, ensuring only LLVM simplification and recursive equation simplification are used, not the SMT solver. Done means a false instantiated requires clause rejects the equation and other equations are attempted, while indeterminate matching otherwise remains non-applicable.