Revert Clark's last commit, at his request; there are some bugs.

This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.
adds model generation for strings, and a hacked way in arith engine for models
optimizing model generation for strings
fix loop detection for multi-vars
Better fix for bug 528
Reduce compiler dependencies on substitutions.h,
Some new functionality in substitutions.h/cpp
for morgan to see the regression problems
fix the infinite issue
removes unsound cases, adds unrolling
adds model generation for strings, and a hacked way in arith engine for models
optimizing model generation for strings
fix loop detection for multi-vars
for morgan to see the regression problems
fix the infinite issue
removes unsound cases, adds unrolling
Merge branch 'master' of github.com:tiliang/CVC4
Add new symmetry breaking technique for finite model finding.  Improvements to bounded integer quantifier instantiation.
adds communication with arith engine
Merge branch 'master' of github.com:tiliang/CVC4
Some fixes to recent strings commits.