Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master.  See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
Fixing a SWIG problem for RationalFromDoubleException.
Fix bug 554 (nominally).
Fix run_regression on Mac.
Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies; fix bug 551, improper ITE removal under quantifiers.
Merge remote-tracking branch 'CVC4root/master'
Fixing name changes that cam in from the merge.
Merge pull request #18 from timothy-king/master

Merging in the glpk changes
Re-fix bug 551 by adding a check to the arith ITE simplifier to ignore non-ground ITEs also.
minor change for strings-fmf
minor change for strings-fmf
Merge branch 'master' of github.com:tiliang/CVC4
adds intro vars length cache
Initial refactor of rewrite rules, make theory_rewriterules empty theory.  Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.

Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.

QCF is now functional backend to rewrite rules. Support boolean variables in QCF.  Change check-model to ignore rewrite rules.  Incorporate some fixes from master.

Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.

Minor fixes to QCF/rewrite engine, removes RE on last call approach.  Add option for one inst per round in RE.

Merging rewrite rules into master, check-model current fails on 3 FMF regressions.

Fix check-model issue, a line of code was omitted during merge.
Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.
Merge branch '1.3.x'
Fix for (get-assignment), resolves bug 553.
Minor cleanup.

* Reenable parts of bvsimple test
* Fix typo in #endif comment
Fix for portfolio.
Fix for random-seed option.