Optimizing congruence closure

Allocating as many objects as possible in initialize. Representing Terms by Ints
where possible.
Got rid of LazyBasicSolver and FastCongruenceSolver for the time being.
Simplified diseq update code

Instead of updating the reprs in diseq, look them up at every access. Use a
robust iterator, such that invalid timestamps can be removed while iterating
over diseq.

Also, some minor code cleanup.
Proof code rewritten to Int + code reorganization

Got rid of the ProofStructureNode class and changed the code accordingly. Now
the parents are stored in proofStructure and the edge labels in proofLabels.
Both are Array[Int].

Added a comment to the TheorySolver interface, stating that adheres to the one
in the DPLL(T) paper.

Reorganized the CongruenceClosure class, such that all vars/vals are at the top,
followed by the classes in approximate call order.