Simplifications to speed up convert-tiff2jpg-query-1831.smt by >100,000 times.

Simplifications to speed up convert-tiff2jpg-query-1831.smt by >100,000 times.

* Some SMT-LIB format outputting of expression.
* Parsing arbitary length bitvector input strings via the C-interface.
* No more memory leaks from the _letid_expr_map & co.
* const& to reduce copy constructor usage in BVTypeCheck.
* Checks for equality on some fixed bits. e.g. (= bv0[16] (concat bv1[15] x)) == false.
* Reduces multiplications with leading 1's to a minus. e.g. 255*x == -1*x.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@68 e59a4935-1847-0410-ae03-e826735625c1