Implement :named and let abbreviation modes in ExprSMTLIBPrinter

This is a slightly updated patch by Peter Collingbourne (@pcc) that addresses issue #170. It teaches ```ExprSMTLIBPrinter``` to (optionally) use expression abbreviations using the SMTLIBv2 ```:named``` keyword. Since not every solver supports this annotation, the default is to use the ```let``` abbreviations where applicable making ```ExprSMLIBLetPrinter``` obsolete. Each abbreviation mode is now tested using a separate test case.