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
and this?