Z3: Improve back conversion efficiency
Z3: Improve back conversion efficiency

Z3Converter.back was relying on z3.is_app_of to perform back
conversion. Each call to this method creates unnecessary intermediate
objects. The back conversion now works by directly obtaining the Kind of
the expression (e.g., z3.Z3_OP_AND), and using it to access a map.

On big problems this is ~2x faster.

This makes all the custom z3.is_* methods obsolete

agriggio/pysmt,pysmt/pysmt,pysmt/pysmt,agriggio/pysmt