Commit e2fca2b8 authored by Carlos Galindo's avatar Carlos Galindo
Browse files

constrained subsumed tabular algorithm fix

WorkNS didn't take into account lastEdgeType, causing incompleteness errors in slices.
parent 28d1ae52
Loading
Loading
Loading
Loading
+12 −13
Original line number Diff line number Diff line
@@ -13,7 +13,9 @@ import java.util.*;
 */
public class ConstrainedSubsumedTabularAlgorithm extends ConstrainedTabularAlgorithm {

    protected Map<WorkNS, Set<Work>> subLookupMap;
    /** Lookup map for subsumption, to be able to search by
     *  context-current.node-lastEdgeType (current.stack=null in all keys). */
    protected Map<Work, Set<Work>> subLookupMap;

    public ConstrainedSubsumedTabularAlgorithm(EDG edg) {
        super(edg);
@@ -28,31 +30,28 @@ public class ConstrainedSubsumedTabularAlgorithm extends ConstrainedTabularAlgor
    @Override
    protected void propagate(Work work) {
        if (!pathEdge.contains(work)) {
            WorkNS wns = new WorkNS(work);
            Work wns = cloneNclearCurrentStack(work);
            Set<Work> matchedWorks = subLookupMap.getOrDefault(wns, Collections.emptySet());
            if (work.current().stack().isEdgeConstraintsEmpty() ||
                    matchedWorks.stream()
                            .map(Work::current)
                            .map(State::stack)
                            .noneMatch(work.current().stack()::isSuffix)) {
                // Removed subsumed copies that haven't been analyzed yet
                for (Work w : matchedWorks)
                    if (w.isSubsumedBy(work))
                    if (work.current().stack().isSuffix(w.current().stack()))
                        workList.remove(w);
                // Original behaviour
                pathEdge.add(work);
                workList.add(work);
                if (!subLookupMap.containsKey(wns))
                    subLookupMap.put(wns, new HashSet<>());
                subLookupMap.get(wns).add(work);
                // Populate subLookupMap
                subLookupMap.computeIfAbsent(wns, k -> new HashSet<>()).add(work);
            }
        }
    }

    /**
     * An equivalent to {@link Work} without a current stack, for faster lookup
     */
    protected record WorkNS(State context, Node currentNode) {
        public WorkNS(Work work) {
            this(work.context(), work.current().node());
        }
    /** Create an object suitable as a {@link #subLookupMap} key. */
    protected Work cloneNclearCurrentStack(Work work) {
        return new Work(work.context(), new State(work.current().node(), null), work.lastEdgeType());
    }
}
+4 −0
Original line number Diff line number Diff line
@@ -240,6 +240,10 @@ public class ConstrainedTabularAlgorithm implements SlicingAlgorithm {
         */
        @Override
        public int compareTo(Work o) {
            // This conditional is necessary due to subclass using null values
            // and storing Work as key in a map.
            if (current.stack == null || o.current.stack == null)
                return 0;
            return current.stack.sizeEdgeConstraints() - o.current.stack.sizeEdgeConstraints();
        }
    }