pub fn solve_zielonka<G: PG>(game: &G, compute_strategy: bool) -> ([Set; 2], Option<[Strategy; 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::new(game, compute_strategy);

    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);

    }

    if compute_strategy {

        debug_assert!(S0.is_some() || S1.is_some(), "At least one strategy should be computed if compute_strategy is true");

        let S0 = S0.unwrap_or_default();

        let S1 = S1.unwrap_or_default();

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

        ([W0, W1], None)

}

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

        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,

            compute_strategy,

        }

    }

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

        self.recursive_calls += 1;

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

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

        if !V.any() {

            return (V.clone(), None, V.clone(), None);

        }

        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 = if self.compute_strategy {

            U.clone()

            Set::default()

        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 = if self.compute_strategy { self.union_strategies(S1_alpha, A_strategy).map_or_else(

                |s| Some(s.extend_arbitrary(self.game, &U_clone, &V, alpha)),

                None

            combine_with_strategy(W1_alpha, S1_alpha, W1_not_alpha, None, 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 = self.union_strategies(self.union_strategies(S2_not_alpha, B_strategy), 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, Option<Strategy>) {

        let mut strategy = if self.compute_strategy {

            Some(Strategy::new())

            None

        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 let Some(s) = strategy.as_mut() && self.game.owner(v) == alpha {

                            s.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))

    }

    fn union_strategies(&self, strategy1: Option<Strategy>, strategy2: Option<Strategy>) -> Option<Strategy> {

        if let Some(s1) = strategy1 {

            if let Some(s2) = strategy2 {

                Some(s1.union(s2))

        } else { strategy2 }

    }

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: Option<V>,

    omega_not_x: U,

    strategy_not_x: Option<V>,

    player: Player,

) -> (U, Option<V>, U, Option<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());

        });

    }