fixes to the compatibility layer; this fixes the broken system test
allow SmtEngine::setOption() for trace and debug tags
Single driver for both sequential and portfolio

A "command executer" layer between parsing commands and invoking them.

New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
Some minor changes after reviewing the portfolio "unified driver" commit.

(this commit was certified error- and warning-free by the test-and-commit script.)
Add [*] footnotes to --help output indicating for many options --FOO that there are --no-FOO variants.
list portfolio_util.h in Makefile, so it gets distributed (fixes debian build)
Fixed an error in the rewriter Pascal pointed out. This was in effectively dead code. (Nobody internally made minus nodes.)
modified getValue to return Expr instead of Node
Partially reverting the changes made in 4308. There is now both an Expr and Node version of getValue() in TheoryModel.
added getCardinality to model
Adding model assertions after SAT responses.

To enable, use --check-models.  Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not.  This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too.

By default, --check-models is quiet (no output unless it detects a problem).  That allows regression runs to pass unless there are problems:

  make regress CVC4_REGRESSION_ARGS=--check-models

To see it work, use -v in addition to --check-models.

There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state.

--check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models.  This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting).

Also:

* TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants)
* The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2)
* The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)
ensure that get-value and get-model are consistent, rewrite function value bodies, do not dag-ify model output
Fix a few minor issues in options processing, improving usability, consistency, error-reporting, and documentation.
Fix a soundness bug reported by Matthias Weiler (had to do with expired TNodes).

Also fix an issue where --check-model didn't take user define-funs into account.

Also make preprocessing a bit more chatty (with -v -v).

(this commit was certified error- and warning-free by the test-and-commit script.)
a fix for the java bindings for wei
bug testcase for model generation
another bindings fix (should fix debian build)
minor interface improvements, compliance fixes

(this commit was certified error- and warning-free by the test-and-commit script.)
store values returned by get-value in TheoryModel::d_reps if necessary, fixes bug 382.
enable bug regression for bug 382

(this commit was certified error- and warning-free by the test-and-commit script.)