Merging some cleanup work:

* Comment cleanup
* Spelling fixes
* Fix warnings
* Documentation updates
* References in docs to cryptominisat removed
* Unneeded scope resolutions removed
* Old, unused regression removed

Fix for iff terms over equalities between the same term and differing constants.

Fix bug 491 and related issues with checkModel() and quantifiers.  Enabling previously-failing testcase.

fixed TheoryBool rewriter bug

fixed bug 502; now the core bv solver only gives the model for variables and shared terms.

changed option to run inequality solver by default

Disabling eager array index splitting for QF_AUFLIA
Minor changes to model-based array solver

do simple ite rewriting within quantifiers

make Boolean term conversion partially non-recursive (resolves bug 501)

Merge branch 'master' of github.com:CVC4/CVC4

removing cryptominisat since we're not using it

fix memory corruption in arrays destructor

some Java bindings fixes (fixes Debian build problems)

Fixed a warning, made eager-index default to true (better for QF_AUFBV)

Fixed bug in arrays

Added assertion

Updates to model-based array solver
Minor fixes to bv and theory_engine

New model-based array procedure

reverted the core solver to do static slicing, added option --bv-core-solver

fixed inequality checkDisequalities inefficiency

Merge branch 'master' into bv-core

fixed some model stuff

fixed  model generation bug; commented out attempt at inequality propagation

inequality solver now only splits on disequalities when complete

added model generation for bv subtheories and bv-inequality solver option

Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac

Make --incremental the default when running interactively

core theory currently disabled

getModelValue implementation in bitvectors

adding
* getModelValue to valuation
* getModelValue to theory engine
* getModelValue to theory
implemented getModelValue in bitvector

the purpose of getModelValue is to ask for a concrete value of a shared term

Merge branch 'master' of git@github.com:CVC4/CVC4.git

moving bv before arrays

fixed inequality bugs due to improper explanation

cleaned up the bv subtheory interface; added check for inequality theory completeness

java input stream adapters working

getEqualityStatus now also queries the inequality solver

Fix for SCM detection

Merge pull request #7 from kbansal/portfolio

finish removal of separateOutput

finish removal of separateOutput

added support for disequalities in the inequality solver

incremental inequality solver implemented

Fix bug in portfolio executor output; fixes nightly portfolio-checking runs.

non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)

fixed some explanation problems for the core theory; still slow

Merge remote-tracking branch 'dddejan/c++11'

Conflicts:
src/smt/boolean_terms.cpp

changing string hash function to use the gnu namespace
due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem

Support for Boolean term conversion in datatypes.

compiles with
export CXXFLAGS='-std=gnu++0x' before configure
fails all regressions in the parser

Merge branch 'master' into bv-core

another typo/bugfix for equality constant evaluation

Merge branch 'master' into bv-core

fixed more equality stuff

Better error in case of nonlinear assertions while in linear logic

Add the ability to "mute" commands, needed for SMT-LIB compliance.

fixing markings of internal nodes in equality engine

fixed compilation problem

incorporated dejan's constant evaluation; now getting destruction seg fault

Merge branch 'master' into bv-core

disabled ineq

Merge branch 'master' of github.com:CVC4/CVC4

Some model and printing fixes for defined functions in input.

more equality constant evaluation

Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException

added regression test for constant eval

Merge branch 'master' into bv-core

fixing constant evaluation bugs

added more tests

generalized bv inequality reasoning to handle both strict and non-strict inequalities

Better reporting of detached git state in --version and --show-config

Fix to bug 497: make justification heuristic's ITE cache context-dependent.

Remove unintentionally-committed-to-master README from interactive branch

Interactive mode support for multiline input

Properly |quote| symbols in SMT-LIBv2 output.

Some statistics for narrowing down incrementality issues (push/pop vs solve timing)

one more ineq regression

fixed reversed concat in core theory

merged dejan's stuff

merged master with dejan's constant evaluating equality engine

inequality reasoning works on small examples added to regressions (not incremental); currently disabled though

Adding evaluation of constant terms to the equality engine. Evaluation on a particular kind can be set by setting interpreted = true when calling addFunctionKind.

Minor cleanup of sources

Fixes for miplib-trick application (and a new testcase)

Remove PropositionalQuery class and all CUDD-related build stuff (and references)

Minor fixes to build system

added the cpp file for the inequality graph

implementing more inequality graph stuff; work in progress doesn't compile

more work on inequality reasoning for bv

started work on the inequality bv subtheory

Boolean terms rewriting for quantified variables of type Bool, when quantifier body uses them in term context

Merge branch '1.0.x'

fix up build system for swig (d242c30 introduced a subtle error)

changed default option for quantifier instantiation

Merge branch '1.0.x'

Fix warning (line annotation)

fix to build system: #include the proper file when they are in both builds and src

Added a rewrite for iff:
x = c iff x = d ---> false
This fixes Andy's problem if unconstrained simplification is turned on.

post failed attempts at getting the incremental solver to work

ite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms, improvement for pre skolemization

Disallow overflow in bitvector literals (parser only)

* For example, (_ bv5 1) is now an error instead of being silently truncated.
* Probably inappropriate for 1.0.x because it changes exception specifications.

more slicer changes for incremental