After predicate refinement, instead of starting to build the ART from scratch, we keep the current one, but update it to reflect the new set of predicates.
This means that we have to check for each node if the newly added predicates are true in that node or not (this needs to be done in the order that guarantees that parents are refined before the children).
Since we are currently building abstract reachability tree and not graph, we have to maintain the set of covered nodes (to prevent explosion). The covering relations has to be checked because refinement may have invalidated some coveree-coverer pairs.
NOTE: In case we switch from ART to ARG (which may be more efficient), refinement would have to be very differently.
In case a node has more than one incoming edge, some new predicate might hold via one edge but not via other one.
That means that the node would effectively have to be split during refinement, with transitive consequences on the nodes children.
After predicate refinement, instead of starting to build the ART from scratch, we keep the current one, but update it to reflect the new set of predicates. This means that we have to check for each node if the newly added predicates are true in that node or not (this needs to be done in the order that guarantees that parents are refined before the children). Since we are currently building abstract reachability tree and not graph, we have to maintain the set of covered nodes (to prevent explosion). The covering relations has to be checked because refinement may have invalidated some coveree-coverer pairs.
NOTE: In case we switch from ART to ARG (which may be more efficient), refinement would have to be very differently. In case a node has more than one incoming edge, some new predicate might hold via one edge but not via other one. That means that the node would effectively have to be split during refinement, with transitive consequences on the nodes children.