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

[geo2a]

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.