Structure-Aware Computation of Predicate Abstraction