Modify equality engine to allow operators to be marked as external terms (#1082)

Modify equality engine to allow operators to be marked as external terms (#1082)

This is required for reasoning higher-order, since we may have equalities between functions, which are operators of APPLY_UF terms.

This commit gets around the previous 1% slowdown by modifying the changes to the equality engine to be minimal impact. Previously the "isInternal" flag could be reset to false after a term is marked as internal=true. This provides an interface for whether operators of a kind should be marked as internal=false from the start. When using higher-order, APPLY_UF operators will be marked as being external when the higher-order option ufHo is set to true.

This has <.001% impact on performance on QF smtlib : https://www.starexec.org/starexec/secure/details/job.jsp?id=24445