package support;

import java.util.*;

/**
 * SwiplAlgorithm — models three CWE-407 sites in SWI-Prolog library code.
 *
 * ── swipl-0001  library/ugraphs.pl:509-510  (HIGH) ──────────────────────────
 *
 * DEFECT: In top_sort/5 (Kahn's topological sort), decr_zero_neighbors/7
 * looks up each zero-in-degree vertex in the graph by linear scan:
 *
 *   decr_zero_neighbors([Zero|Zeros], Graph, Vertices, ...) :-
 *       graph_memberchk(Zero-Neibs, Graph),   % O(|V|) scan — DEFECT
 *       decr_list(Neibs, Vertices, ...),
 *       decr_zero_neighbors(Zeros, ...).
 *
 *   graph_memberchk(Element1-Edges, [Element2-Edges2|_]) :-
 *       Element1 == Element2, !, Edges = Edges2.
 *   graph_memberchk(Element, [_|Rest]) :-
 *       graph_memberchk(Element, Rest).
 *
 * The graph is a sorted vertex-edges association list. For each vertex in Zeros
 * (up to |V| vertices), graph_memberchk does an O(|V|) scan from the beginning.
 * Total: O(|V|²). Correct Kahn's algorithm complexity: O(|V| + |E|).
 *
 * Fix: Pass a pre-built HashMap<Vertex, List<Vertex>> alongside Graph.
 * O(1) lookup per zero-vertex. Total becomes O(|V| + |E|).
 *
 * ── swipl-0002  library/aggregate.pl:673  (MEDIUM) ──────────────────────────
 *
 * DEFECT: free_variables/4 builds a VarList accumulator and checks each new
 * candidate variable with list_is_free_of/2:
 *
 *   free_variables(Term, Bound, VarList, [Term|VarList]) :-
 *       var(Term),
 *       term_is_free_of(Bound, Term),
 *       list_is_free_of(VarList, Term),   % O(n) scan — DEFECT
 *       !.
 *
 *   list_is_free_of([Head|Tail], Var) :- Head \== Var, !, list_is_free_of(Tail, Var).
 *   list_is_free_of([], _).
 *
 * VarList grows by one entry per unique free variable. With N unique variables,
 * list_is_free_of is called N times (once per candidate), each scanning O(n)
 * entries already in VarList. Total: 0+1+2+...+(N-1) = N*(N-1)/2 = O(N²).
 *
 * Even the maintainer flagged it: @tbd "Exploit our built-in term_variables/2
 * at some places?" — term_variables/2 is a C built-in that is O(N).
 *
 * Fix: Use a HashSet<Integer> (modeling variable identity) alongside VarList.
 * Check HashSet.contains() — O(1) — before adding to VarList.
 *
 * ── swipl-0003  library/clp/clp_distinct.pl:173-174  (MEDIUM) ───────────────
 *
 * DEFECT: attr_unify_hook/2 fires during unification of CLP(distinct)-
 * constrained variables. It checks:
 *
 *   attr_unify_hook(dom_neq(Dom, Lefts, Rights), Y) :-
 *       ( ground(Y) -> ...
 *       ;
 *           \+ lists_contain(Lefts, Y),   % O(K×N) — DEFECT
 *           \+ lists_contain(Rights, Y),  % O(K×N) — DEFECT
 *
 *   lists_contain([X|Xs], Y) :-
 *       ( list_contains(X, Y) -> true ; lists_contain(Xs, Y) ).
 *   list_contains([X|Xs], Y) :-
 *       ( X == Y -> true ; list_contains(Xs, Y) ).
 *
 * Lefts/Rights are lists of variable lists accumulated per constraint group.
 * With K constraint groups each of average N variables, each unification hook
 * call costs O(K×N). For constraints on many variables, this becomes significant.
 *
 * Fix: Replace list-of-lists with a flat HashSet<Integer> per constraint group,
 * built once when the constraint is posted. Check HashSet.contains() — O(1).
 *
 * Comparison counts:
 *   0001 defective: |V|² — O(|V|) scan per vertex in Zeros
 *   0001 fixed:     |V|  — O(1) HashMap lookup per vertex
 *   0002 defective: N*(N-1)/2  — triangular accumulator scan
 *   0002 fixed:     N          — one O(1) set check per variable
 *   0003 defective: K × N      — nested list scan per unification
 *   0003 fixed:     1          — one O(1) hash lookup per unification
 */
public class SwiplAlgorithm {

    // ── swipl-0001: ugraphs.pl top_sort graph_memberchk ──────────────────────

    public static final class TopoResult {
        public final List<List<Integer>> layers;  // topological layers (Kahn's)
        public final long comparisons;

        public TopoResult(List<List<Integer>> layers, long comparisons) {
            this.layers = layers;
            this.comparisons = comparisons;
        }
    }

    /**
     * Defective: graph_memberchk — O(|V|) scan per zero-vertex.
     * Graph: sorted list of (vertex → neighbors) pairs modeled as array of lists.
     */
    public static TopoResult defectiveTopSort(List<List<Integer>> adjList) {
        int V = adjList.size();
        int[] indegree = new int[V];
        for (int u = 0; u < V; u++)
            for (int w : adjList.get(u)) indegree[w]++;

        long comparisons = 0;
        List<Integer> zeros = new ArrayList<>();
        for (int v = 0; v < V; v++) if (indegree[v] == 0) zeros.add(v);

        List<List<Integer>> layers = new ArrayList<>();

        while (!zeros.isEmpty()) {
            layers.add(new ArrayList<>(zeros));
            List<Integer> nextZeros = new ArrayList<>();

            for (int zero : zeros) {
                // graph_memberchk: scan sorted graph list from beginning — O(|V|)
                List<Integer> neibs = null;
                for (int v = 0; v < V; v++) {        // O(|V|) scan
                    comparisons++;
                    if (v == zero) { neibs = adjList.get(v); break; }
                }
                if (neibs != null) {
                    for (int w : neibs) {
                        if (--indegree[w] == 0) nextZeros.add(w);
                    }
                }
            }
            zeros = nextZeros;
        }

        return new TopoResult(layers, comparisons);
    }

    /**
     * Fixed: HashMap<vertex, neighbors> — O(1) lookup per zero-vertex.
     * Pre-build a HashMap alongside the graph, as the fix prescribes.
     */
    public static TopoResult fixedTopSort(List<List<Integer>> adjList) {
        int V = adjList.size();
        int[] indegree = new int[V];

        // Build HashMap once — O(|V|)
        Map<Integer, List<Integer>> graphMap = new HashMap<>(V * 2);
        for (int u = 0; u < V; u++) {
            graphMap.put(u, adjList.get(u));
            for (int w : adjList.get(u)) indegree[w]++;
        }

        long comparisons = 0;
        List<Integer> zeros = new ArrayList<>();
        for (int v = 0; v < V; v++) if (indegree[v] == 0) zeros.add(v);

        List<List<Integer>> layers = new ArrayList<>();

        while (!zeros.isEmpty()) {
            layers.add(new ArrayList<>(zeros));
            List<Integer> nextZeros = new ArrayList<>();

            for (int zero : zeros) {
                comparisons++;  // O(1) HashMap lookup
                List<Integer> neibs = graphMap.get(zero);
                if (neibs != null) {
                    for (int w : neibs) {
                        if (--indegree[w] == 0) nextZeros.add(w);
                    }
                }
            }
            zeros = nextZeros;
        }

        return new TopoResult(layers, comparisons);
    }

    // ── swipl-0002: aggregate.pl free_variables/4 list_is_free_of ────────────

    public static final class FreeVarsResult {
        public final List<Integer> varList;  // accumulated unique free variables
        public final long comparisons;

        public FreeVarsResult(List<Integer> varList, long comparisons) {
            this.varList = varList;
            this.comparisons = comparisons;
        }
    }

    /**
     * Defective: list_is_free_of — O(n) scan per candidate variable.
     * Models the accumulator-with-linear-check pattern.
     *
     * @param candidates  variable IDs to process (some duplicates, models term walk)
     * @param bound       set of bound variables to exclude
     */
    public static FreeVarsResult defectiveFreeVariables(
            List<Integer> candidates, Set<Integer> bound) {
        List<Integer> varList = new ArrayList<>();
        long comparisons = 0;

        for (int term : candidates) {
            if (bound.contains(term)) continue;  // term_is_free_of(Bound, Term)

            // list_is_free_of: scan varList for identity
            boolean free = true;
            for (int existing : varList) {
                comparisons++;
                if (existing == term) { free = false; break; }
            }
            if (free) varList.add(term);
        }

        return new FreeVarsResult(varList, comparisons);
    }

    /**
     * Fixed: HashSet — O(1) per candidate variable.
     * Models term_variables/2 built-in or HashSet-backed accumulator.
     */
    public static FreeVarsResult fixedFreeVariables(
            List<Integer> candidates, Set<Integer> bound) {
        List<Integer> varList = new ArrayList<>();
        Set<Integer> seen = new HashSet<>();
        long comparisons = 0;

        for (int term : candidates) {
            if (bound.contains(term)) continue;

            comparisons++;  // O(1) hash lookup
            if (!seen.contains(term)) {
                varList.add(term);
                seen.add(term);
            }
        }

        return new FreeVarsResult(varList, comparisons);
    }

    // ── swipl-0003: clp_distinct.pl lists_contain in attr_unify_hook ─────────

    public static final class UnifyHookResult {
        public final boolean compatible;  // could the unification proceed?
        public final long comparisons;

        public UnifyHookResult(boolean compatible, long comparisons) {
            this.compatible = compatible;
            this.comparisons = comparisons;
        }
    }

    /**
     * Defective: lists_contain — O(K × N) nested list scan per unification.
     *
     * @param leftsGroups  K constraint groups (each a list of variable IDs)
     * @param candidate    the variable Y being unified
     */
    public static UnifyHookResult defectiveUnifyHook(
            List<List<Integer>> leftsGroups, int candidate) {
        long comparisons = 0;

        // lists_contain: for each group, scan its list for candidate
        for (List<Integer> group : leftsGroups) {
            for (int v : group) {
                comparisons++;
                if (v == candidate) {
                    return new UnifyHookResult(false, comparisons);
                }
            }
        }

        return new UnifyHookResult(true, comparisons);
    }

    /**
     * Fixed: pre-built flat HashSet — O(1) per unification hook call.
     *
     * @param flatSet  pre-built set of all variables in all constraint groups
     * @param candidate the variable Y being unified
     */
    public static UnifyHookResult fixedUnifyHook(
            Set<Integer> flatSet, int candidate) {
        long comparisons = 1;  // O(1) hash lookup
        boolean compatible = !flatSet.contains(candidate);
        return new UnifyHookResult(compatible, comparisons);
    }

    // ── Test data builders ────────────────────────────────────────────────────

    /** Builds a random DAG with V vertices and E edges (no self-loops, no back-edges). */
    public static List<List<Integer>> buildDAG(int V, int E, Random rng) {
        List<List<Integer>> adj = new ArrayList<>();
        for (int i = 0; i < V; i++) adj.add(new ArrayList<>());
        int added = 0;
        while (added < E) {
            int u = rng.nextInt(V - 1);
            int w = u + 1 + rng.nextInt(V - u - 1);
            if (!adj.get(u).contains(w)) {
                adj.get(u).add(w);
                added++;
            }
        }
        for (List<Integer> nb : adj) Collections.sort(nb);
        return adj;
    }

    /** Builds a list of candidates with some duplicates (models term walk). */
    public static List<Integer> buildCandidates(int uniqueVars, int duplicates, Random rng) {
        List<Integer> cands = new ArrayList<>();
        for (int i = 0; i < uniqueVars; i++) cands.add(i);
        for (int i = 0; i < duplicates; i++) cands.add(rng.nextInt(uniqueVars));
        Collections.shuffle(cands, rng);
        return cands;
    }

    // ── Self-test ─────────────────────────────────────────────────────────────

    public static void main(String[] args) {
        System.out.println("SwiplAlgorithm — swipl-0001 + swipl-0002 + swipl-0003");
        System.out.println();

        // swipl-0001: top_sort graph_memberchk
        System.out.println("── swipl-0001: ugraphs.pl top_sort (graph_memberchk) ──");
        System.out.println("Defect: graph_memberchk O(|V|) scan per zero-vertex in Kahn loop");
        System.out.println("Fix:    HashMap<vertex,neighbors> built once — O(1) per lookup");
        System.out.println();
        System.out.printf("%-8s  %-8s  %-14s  %-10s  %s%n",
            "|V|", "|E|", "Defective ops", "Fixed ops", "Speedup");
        System.out.println("─".repeat(52));

        for (int V : new int[]{10, 20, 50, 100, 200, 500}) {
            int E = V * 2;  // sparse graph
            List<List<Integer>> dag = buildDAG(V, Math.min(E, V * (V - 1) / 2),
                new Random(42));

            TopoResult def = defectiveTopSort(dag);
            TopoResult fix = fixedTopSort(dag);

            assert def.layers.equals(fix.layers)
                : "layer mismatch at V=" + V;

            System.out.printf("%-8d  %-8d  %-14d  %-10d  %.1fx%n",
                V, E, def.comparisons, fix.comparisons,
                (double) def.comparisons / Math.max(1, fix.comparisons));
        }

        System.out.println();

        // swipl-0002: free_variables/4 accumulator
        System.out.println("── swipl-0002: aggregate.pl free_variables/4 (list_is_free_of) ──");
        System.out.println("Defect: list_is_free_of O(n) scan per candidate — O(N²) total");
        System.out.println("Fix:    HashSet<Var> — O(1) per candidate");
        System.out.println();
        System.out.printf("%-10s  %-10s  %-14s  %-10s  %s%n",
            "N unique", "candidates", "Defective ops", "Fixed ops", "Speedup");
        System.out.println("─".repeat(56));

        for (int N : new int[]{10, 50, 100, 500, 1000}) {
            List<Integer> cands = buildCandidates(N, N / 2, new Random(42));
            Set<Integer> bound = Collections.emptySet();

            FreeVarsResult def = defectiveFreeVariables(cands, bound);
            FreeVarsResult fix = fixedFreeVariables(cands, bound);

            assert def.varList.size() == fix.varList.size()
                : "varList size mismatch at N=" + N;

            System.out.printf("%-10d  %-10d  %-14d  %-10d  %.1fx%n",
                N, cands.size(), def.comparisons, fix.comparisons,
                (double) def.comparisons / Math.max(1, fix.comparisons));
        }

        System.out.println();

        // swipl-0003: clp_distinct attr_unify_hook
        System.out.println("── swipl-0003: clp_distinct.pl attr_unify_hook (lists_contain) ──");
        System.out.println("Defect: lists_contain O(K×N) nested scan per unification hook");
        System.out.println("Fix:    pre-built flat HashSet — O(1) per hook call");
        System.out.println();
        System.out.printf("%-8s  %-8s  %-14s  %-10s  %s%n",
            "K groups", "N per grp", "Defective ops", "Fixed ops", "Speedup");
        System.out.println("─".repeat(52));

        Random rng = new Random(42);
        for (int K : new int[]{2, 5, 10, 20, 50}) {
            int N = 20;
            List<List<Integer>> groups = new ArrayList<>();
            Set<Integer> flat = new HashSet<>();
            for (int k = 0; k < K; k++) {
                List<Integer> grp = new ArrayList<>();
                for (int i = 0; i < N; i++) {
                    int v = k * N + i;
                    grp.add(v);
                    flat.add(v);
                }
                groups.add(grp);
            }
            int candidate = rng.nextInt(K * N + 10);  // sometimes not in groups

            UnifyHookResult def = defectiveUnifyHook(groups, candidate);
            UnifyHookResult fix = fixedUnifyHook(flat, candidate);

            assert def.compatible == fix.compatible
                : "compatibility mismatch at K=" + K;

            System.out.printf("%-8d  %-8d  %-14d  %-10d  %.1fx%n",
                K, N, def.comparisons, fix.comparisons,
                (double) def.comparisons / Math.max(1, fix.comparisons));
        }
    }
}