separated SymbolicUnifier and SymbolicConstraint

OK, I finally managed to cut the complex interdependence of ```SymbolicUnifier``` and ```SymbolicConstraint```. ```SymbolicUnifier``` no longer takes a ```SymbolicConstraint``` in its constructor and ```SymbolicConstraint``` no longer relies on the ```SymbolicUnifer``` to update itself. This is quite an important step towards further refactoring of the ml prover.

@dwightguth @andreistefanescu please review
Sure, but I might need to add a few more commits to make this pull request complete. However, I would like to start getting reviews.