Make all polymorphic function symbols in the egraph map to the same CCTerm.  This is needed for selects
First version of our array solver based on weak equivalences.  Currently, proof production is not really checked, and neither interpolation nor model production are implemented.
Fixed bug in the DeltaDebugger where array store terms were replaced by the store index rather than the store array
Fixed logger setup for test cases.  In some cases the appender for log4j was installed multiple times leading to lots of logging output.  Now, if an appender is already installed, we do not install another appender.
Proof production for arrays.  This needs more testing, but should in general be okay.  This commit essentially fixes the meaning of the new proof element :weakpath to be a path through the weak equivalence (modulo i) graph.  It is a path in the modulo graph if there are two selects on that path.
Fixed treatment of @diff.  The axiom for @diff was wrong and included multiple times in the clause database.
Added option create_deltadebugger_jar to buildfile.  This option creates file deltadebugger.jar that can be used to run our internal delta debugger.
Bug fix in WeakEQi path computation

Handle null-case (continue if not weak-equal)
Small optimization
Added support for model values to the Theory.

The theory now internally declares function symbols of the form
(as @1234 Sort). It is as if there is a polymorphic function symbol @x
with zero arguments and arbitrary type is declared for every decimal
number x.  The function symbols are created when needed and put into
a unify hash.
Model values are now flagged with a model flag and rejected as input in asserts.
Report error on declare-fun with the name @digits
Fixed let handling in DeltaDebugger
Array solver supports model production.  From now on, models will contain @n terms for a numeral n for every uninterpreted sort.  Furthermore, the array model term @0 represents the array that stores at every index the default value of the value sort.
Fixed creation of equalities in WeakCongruencePath.  If an EqualityProxy generated a LAEquality, but no corresponding CCEquality, we crashed with an InternalError instead of constructing the correct CCEquality.
Small performance optimization when creating a CCEquality.

We do not need to search twice for dependent CCEqualities for an LAEquality.  Now, we let the EqualityProxy take care of this.
New ArrayTheory based on DAGs.

The internal data structure for computing the weak and weak-i
equivalence classes is changed to a DAG-like structure.  We have
two outgoing edges, one for the default case (weak equivalence)
and one for the case the default case cannot be taken (weak-i
equivalence for the index of the store in the default case).
It turns out that this is enough to nicely represent the weak
equivalence and all weak-i equivalence relations for all indices.
Ran CheckStyle and PMD.
More PMD fixes.
Updated javacup (cce60ba747)
Fixed bug with fresh declarations in DeltaDebugger.

The DeltaDebugger did not include declarations of fresh symbols when minimizing
unused declarations.  This bug was fixed.  Furthermore, it is now possible to
deactivate pre commands.