parse predicate symbols
remove printing stuff
Added support for set-info in theory solver
Fixed some problems in various parts of the code

In the middle of debugging. Some benchmarks which should be sat are unsat.
Using a second congruence closure object as a sanity checker after the dpll
engine was run.
Added useList backtracking. Fixed a bug where a wrong timestamp was set to
invalid when backtracking. Clearing pending queue in backtrack.
Debugging unsat instead of sat cases

Added reason for an inequality to the diseq computation. Negative T-consequence
computation updated. Some tests (without asserts) added to debug the changes.
Backtracking before explain changed in order to support areCongruent call
thereafter.
T-consequence computation and backtrackTo

Changed the T-consequence computation, by making it more understandable. Not
sure if it's correct yet and therefore it's disabled. Added backtrackTo method
to the theory solver interface. It's needed to backtrack properly in the
presence of T-consequences in the DPLL-engine.
Conflict analysis

Changes to how a T-inconsistency is handled in the DPLL engine. It's still not
working correctly, though. This commit fixes a problem, where the UIP analysis
didn't work properly for theory conflicts.
E.g.:
x @ 2 --> a = b @ 2
                    \
                     --> Conflict
                    /
-y @ 1 --> a != b @ 1

With a propositional conflict, different decision levels right before the
conflict cannot happen.
The conflict clause/learnt clause is computed as the negated conjunction of the
theory explanation and adding the literal causing the conflict. Finally all but
one literal per decision level are removed.
Setting of conflict/reason clause after T-conflict

After a theory conflict:
Switched back to using the UIP analysis code (with setting the conflict clause
correctly beforehand now). The UIP is correctly computed for the current
decision level, but for every other level in the implication graph the literals
are added immediately. I think that we could compute a UIP for each decision
level to make the learnt clause more succinct.