pub fn solve_zielonka<G: PG>(game: &G, compute_strategy: bool) -> ([Set; 2], Option<[Strategy; 2]>) {

    if compute_strategy {

        let (solution, strategy) = solve_zielonka_impl::<G, Strategy>(game);

        (solution, Some(strategy))

        let (solution, _) = solve_zielonka_impl::<G, ()>(game);

        (solution, None)

}

fn solve_zielonka_impl<G: PG, S: Strat>(game: &G) -> ([Set; 2], [S; 2]) {

    debug_assert!(game.is_total(), "Zielonka solver requires a total parity game");

    let mut V = bitvec![usize, Lsb0; 0; game.num_of_vertices()];

    V.set_elements(usize::MAX);

    let full_V = V.clone(); // Used for debugging.

    let mut zielonka = ZielonkaSolver::<_, S>::new(game);

    let (W0, S0, W1, S1) = zielonka.zielonka_rec(V, 0);

    debug!("Performed {} recursive calls", zielonka.recursive_calls);

    if cfg!(debug_assertions) {

        check_partition(&W0, &W1, &full_V);

    }

    ([W0, W1], [S0, S1])

}

    fn new<'a>(game: &'a G) -> ZielonkaSolver<'a, G, S> {

        let mut priority_vertices = Vec::new();

        for v in game.iter_vertices() {

            let prio = game.priority(v);

            while prio >= priority_vertices.len() {

                priority_vertices.push(Vec::new());

            }

            priority_vertices[prio].push(v);

        ZielonkaSolver {

            game,

            predecessors: Predecessors::new(game),

            priority_vertices,

            temp_queue: Vec::new(),

            recursive_calls: 0,

            _strategy: std::marker::PhantomData,

        }

    }

    fn zielonka_rec(&mut self, V: Set, depth: usize) -> (Set, S, Set, S) {

        self.recursive_calls += 1;

        let full_V = V.clone(); // Used for debugging

        let indent = Repeat::new(" ", depth);

        if !V.any() {

            return (V.clone(), S::new(), V.clone(), S::new());

        }

        let (highest_prio, lowest_prio) = self.get_highest_lowest_prio(&V);

        let alpha = Player::from_priority(&highest_prio);

        let not_alpha = alpha.opponent();

        let mut U = bitvec![usize, Lsb0; 0; self.game.num_of_vertices()];

        for &v in self.priority_vertices[highest_prio].iter() {

            if V[*v] {

                U.set(*v, true);

            }

        debug!(

        trace!("{}Vertices in U: {}", indent, DisplaySet(&U));

        let U_clone = U.clone();

        let (A, A_strategy) = self.attractor(alpha, &V, U);

        trace!("{}Vertices in A: {}", indent, DisplaySet(&A));

        debug!("{}zielonka(V \\ A) |A| = {}", indent, A.count_ones());

        let (W1_0, S1_0, W1_1, S1_1) = self.zielonka_rec(V.clone().bitand(!A.clone()), depth + 1);

        let (mut W1_alpha, mut S1_alpha, W1_not_alpha, S1_not_alpha) =

            x_and_not_x_strategy(W1_0, S1_0, W1_1, S1_1, alpha);

        if !W1_not_alpha.any() {

            W1_alpha |= A;

            S1_alpha = S1_alpha

                .union(A_strategy)

                .extend_arbitrary(self.game, &U_clone, &V, alpha);

            combine_with_strategy(W1_alpha, S1_alpha, W1_not_alpha, S::new(), alpha)

            let (B, B_strategy) = self.attractor(not_alpha, &V, W1_not_alpha);

            trace!("{}Vertices in B: {}", indent, DisplaySet(&B));

            debug!("{}zielonka(V \\ B)", indent);

            let (W2_0, S2_0, W2_1, S2_1) = self.zielonka_rec(V.bitand(!B.clone()), depth + 1);

            let (W2_alpha, S2_alpha, mut W2_not_alpha, mut S2_not_alpha) =

                x_and_not_x_strategy(W2_0, S2_0, W2_1, S2_1, alpha);

            W2_not_alpha |= B;

            S2_not_alpha = S2_not_alpha.union(B_strategy).union(S1_not_alpha);

            check_partition(&W2_alpha, &W2_not_alpha, &full_V);

            combine_with_strategy(W2_alpha, S2_alpha, W2_not_alpha, S2_not_alpha, alpha)

    }

    fn attractor(&mut self, alpha: Player, V: &Set, mut A: Set) -> (Set, S) {

        let mut strategy = S::new();

        self.temp_queue.clear();

        for v in A.iter_ones() {

            self.temp_queue.push(VertexIndex::new(v));

        }

        while let Some(w) = self.temp_queue.pop() {

            for v in self.predecessors.predecessors(w) {

                if V[*v] {

                    let attracted = if self.game.owner(v) == alpha {

                        true

                        self.game.outgoing_edges(v).all(|edge| !V[*edge.to()] || A[*edge.to()])

                    if attracted && !A[*v] {

                        if self.game.owner(v) == alpha {

                            strategy.set(v, w);

                        }

                        A.set(*v, true);

                        self.temp_queue.push(v);

                    }

                }

        (A, strategy)

    }

    fn get_highest_lowest_prio(&self, V: &Set) -> (Priority, Priority) {

        let mut highest = usize::MIN;

        let mut lowest = usize::MAX;

        for v in V.iter_ones() {

            let prio = self.game.priority(VertexIndex::new(v));

            highest = highest.max(*prio);

            lowest = lowest.min(*prio);

        }

        (Priority::new(highest), Priority::new(lowest))

    }

pub fn check_partition(W0: &Set, W1: &Set, V: &Set) {

    let intersection = W0.clone() & W1;

    if intersection.any() {

    }

    let both = W0.clone() | W1;

    if both != *V {

    }

}

pub fn x_and_not_x<U>(omega_0: U, omega_1: U, player: Player) -> (U, U) {

    match player {

        Player::Even => (omega_0, omega_1),

        Player::Odd => (omega_1, omega_0),

}

pub fn combine<U>(omega_x: U, omega_not_x: U, player: Player) -> (U, U) {

    match player {

        Player::Even => (omega_x, omega_not_x),

        Player::Odd => (omega_not_x, omega_x),

}

pub fn x_and_not_x_strategy<U, V>(

    omega_0: U,

    strategy_0: V,

    omega_1: U,

    strategy_1: V,

    player: Player,

) -> (U, V, U, V) {

    match player {

        Player::Even => (omega_0, strategy_0, omega_1, strategy_1),

        Player::Odd => (omega_1, strategy_1, omega_0, strategy_0),

}

pub fn combine_with_strategy<U, V>(

    omega_x: U,

    strategy_x: V,

    omega_not_x: U,

    strategy_not_x: V,

    player: Player,

) -> (U, V, U, V) {

    match player {

        Player::Even => (omega_x, strategy_x, omega_not_x, strategy_not_x),

        Player::Odd => (omega_not_x, strategy_not_x, omega_x, strategy_x),

}

    fn test_random_zielonka_solver() {

        random_test(100, |rng| {

            let mut files = DumpFiles::new("test_random_zielonka_solver");

            let game = random_parity_game(rng, true, 100, 5, 3);

            files.dump("input.pg", |writer| write_pg(writer, &game)).unwrap();

            let (solution, strategy) = super::solve_zielonka(&game, true);

            verify_solution(&game, &solution, &strategy.unwrap());

        });

    }