Added proof_graph_t::enumerate_descendant_nodes.
Implemented the function to add constraints for mutual-exclusion between unifications, in ilp::weighted_converter_t.