Standardize SMT-LIBv2 set of logics to use LogicInfo.

Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2.
This led to inconsistencies---such as nonstandard logics like "QF_LIRA"
being accepted in set-logic but not providing the "Real" sort.  Now,
the LogicInfo is used and queried, so nonstandard logics should work
fine and declare the correct symbols.  SMT-LIB v1.2, unfortunately,
can't take advantage of this fully since symbols like "Array" have
substantially different meanings in different logics.
Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real division
SMT-LIB printer updates (some missing cases).
Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with unknown key.