Fix two variants of Node::substitute().

Node::substitute() is overloaded.  One version was properly substituting
operators (e.g. the "f" in f(x) could be substituted).  The others were
ignoring anything in function position.  Fixed.  Thanks to Wei Wang for
pointing this out.
Merge branch '1.3.x'
reorganize substr, fix some potential bugs, adds cache for preprocessing
reorganize substr, fix some potential bugs, adds cache for preprocessing
Merge branch 'master' of github.com:tiliang/CVC4
No diamond-breaking under quantifiers (resolves bug #550).
Merge branch '1.3.x'
bug fix: strings preprocess for the orignal term, causing unknown in some cases
Add options --full-saturate-quant and --mbqi=trust.  Other minor changes.
Fix quotes in string constants.
New translation work, support Z3-str-style string constraints.
Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).
Minor code clean up in parser.