Hi!
Actually, it was a tough decision in the design of filtered_graph. If you let num_vertices(g) be the actual number of vertices after filtering, it becomes an O(|V|) operation instead of an O(1) operation.
That's clear.
More importantly, external property maps that were based on the vertex_index of the graph will cease to work, because the indices no longer fall in [0, num_vertices(G)) unless you go through the painstaking task of renumbering them (which is not always possible). In
I don't see the trouble in renumbering the vertices if there is already a vertex_index-property. It should be possible to build up a map which provides a mapping from filtered vertex index number to real vertex index number. This could also speed up operations (like a loop over all vertices) on filtered graphs, since the vertice predicate would no longer be necessary to check, wheather a vertice is in the set of the filtered vertices or not.
more real terms, if we made the change to num_vertices(G) then most algorithm invocations would start failing because they rely on vertex indices :(
... a hint in the docs would be nice. I haven't found any. Greetings, Sebastian