add an API for SMT-powered simplification

This implementation is pretty minimal and simply bails out (throwing
smt::Unsupported) when it encounters any complicated feature. However, it's
already enough to simplify the example in tests/disabled/smt-simplify.m.

Github: related to #130 "interact with SMT solver"