Add explicit definitions for abs_{real,int}

[bclement-ocp]

No description provided.

[bclement-ocp]

Draft because I need to rerun perfs.

[bclement-ocp]

After some more poking around, I don't think this is actually the right fix, but rather we should treat Abs_real and Abs_int as "internal" symbols for the floating-point theory and advise users to define their own abs functions rather than use the primitive ones for actual problems. IOW the abs_real and abs_int should only be used internally by the fpa theory to compute on constants, but not to define arbitrary problems. That seems to be the combination that works best in local tests.

This probably should be extended to {min,max}_{int,real} and integer_log2.