pub fn new(s: &'static str, times: usize) -> Self {

        Self { s, times }

    }

pub fn solve_variability_zielonka(

    manager_ref: &BDDManagerRef,

    game: &VariabilityParityGame,

    variant: ZielonkaVariant,

    alternative_solving: bool,

) -> Result<[Submap; 2], MercError> {

    debug_assert!(

        game.is_total(manager_ref)?,

    let mut zielonka = VariabilityZielonkaSolver::new(manager_ref, game, alternative_solving);

    let V = Submap::new(

        manager_ref.with_manager_shared(|manager| {

            if alternative_solving {

                game.configuration().clone()

        }),

        manager_ref.with_manager_shared(|manager| BDDFunction::f(manager)),

        game.num_of_vertices(),

    let full_V = V.clone();

    let (W0, W1) = match variant {

        ZielonkaVariant::Family => zielonka.solve_recursive(V, 0)?,

        ZielonkaVariant::FamilyOptimisedLeft => zielonka.zielonka_family_optimised(V, 0)?,

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

    if cfg!(debug_assertions) {

        zielonka.check_partition(&W0, &W1, &full_V)?;

    let (W0, W1) = if alternative_solving {

        (W0, W1)

    Ok([W0, W1])

}

    pub fn new(manager_ref: &'a BDDManagerRef, game: &'a VariabilityParityGame, alternative_solving: bool) -> Self {

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

        let false_bdd = manager_ref.with_manager_shared(|manager| BDDFunction::f(manager));

        Self {

            game,

            manager_ref,

            temp_queue: Vec::new(),

            temp_vertices: BitVec::repeat(false, game.num_of_vertices()),

            predecessors: VariabilityPredecessors::new(manager_ref, game),

            priority_vertices,

            recursive_calls: 0,

            alternative_solving,

            false_bdd,

        }

    }

    fn solve_recursive(&mut self, gamma: Submap, depth: usize) -> Result<(Submap, Submap), MercError> {

        self.recursive_calls += 1;

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

        let gamma_copy = gamma.clone();

        if gamma.is_empty() {

            return Ok((gamma.clone(), gamma));

        }

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

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

        let not_x = x.opponent();

        let mut mu = Submap::new(

            self.manager_ref.with_manager_shared(|manager| BDDFunction::f(manager)),

            self.false_bdd.clone(),

            self.game.num_of_vertices(),

        for v in &self.priority_vertices[*highest_prio] {

            mu.set(*v, gamma[*v].clone());

        }

        debug!(

        trace!("{indent}Vertices in gamma: {:?}", gamma);

        trace!("{indent}Vertices in mu: {:?}", mu);

        let alpha = self.attractor(x, &gamma, mu)?;

        trace!("{indent}Vertices in alpha: {:?}", alpha);

        debug!(

        let (omega1_0, omega1_1) = self.solve_recursive(gamma.clone().minus(&alpha.clone())?, depth + 1)?;

        let (mut omega1_x, mut omega1_not_x) = x_and_not_x(omega1_0, omega1_1, x);

        if omega1_not_x.is_empty() {

            omega1_x = omega1_x.or(&alpha)?;

            Ok(combine(omega1_x, omega1_not_x, x))

            let beta = self.attractor(not_x, &gamma, omega1_not_x)?;

            debug!(

            trace!("{indent}Vertices in beta: {:?}", beta);

            let (mut omega2_0, mut omega2_1) = self.solve_recursive(gamma.minus(&beta)?, depth + 1)?;

            let (omega2_x, mut omega2_not_x) = x_and_not_x(omega2_0, omega2_1, x);

            omega2_not_x = omega2_not_x.or(&beta)?;

            self.check_partition(&omega2_x, &omega2_not_x, &gamma_copy)?;

            Ok(combine(omega2_x, omega2_not_x, x))

    }

    fn zielonka_family_optimised(&mut self, gamma: Submap, depth: usize) -> Result<(Submap, Submap), MercError> {

        self.recursive_calls += 1;

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

        let gamma_copy = gamma.clone();

        if gamma.is_empty() {

            return Ok((gamma.clone(), gamma));

        }

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

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

        let not_x = x.opponent();

        let mut mu = Submap::new(

            self.false_bdd.clone(),

            self.false_bdd.clone(),

            self.game.num_of_vertices(),

        let mut C = self.false_bdd.clone();

        for v in &self.priority_vertices[*highest_prio] {

            mu.set(*v, gamma[*v].clone());

            C = C.or(&gamma[*v])?;

        debug!(

        trace!("{indent}gamma: {:?}", gamma);

        trace!("{indent}C: {}", FormatConfigSet(&C));

        let alpha = self.attractor(x, &gamma, mu)?;

        trace!("{indent}alpha: {:?}", alpha);

        debug!(

        let (omega1_0, omega1_1) = self.zielonka_family_optimised(gamma.clone().minus(&alpha)?, depth + 1)?;

        let C_restricted = minus(

            &if !self.alternative_solving {

                self.manager_ref.with_manager_shared(|m| BDDFunction::t(m)).clone()

            &C,

        let (mut omega1_x, omega1_not_x) = x_and_not_x(omega1_0, omega1_1, x);

        let omega1_not_x_restricted = omega1_not_x.clone().minus_function(&C_restricted)?;

        if omega1_not_x_restricted.is_empty() {

            omega1_x = omega1_x.or(&alpha)?;

            self.check_partition(&omega1_x, &omega1_not_x, &gamma_copy)?;

            Ok(combine(omega1_x, omega1_not_x, x))

            let mut C1 = self.false_bdd.clone();

            for (_v, func) in omega1_not_x.iter() {

                C1 = C1.or(func)?;

            C1 = C1.and(&C)?;

            let C1_restricted = minus(

                &if self.alternative_solving {

                    self.game.configuration().clone()

                &C1,

            let omega1_not_x_restricted1 = omega1_not_x.clone().minus_function(&C1_restricted)?;

            trace!("{indent}omega'_notx_restricted: {:?}", omega1_not_x_restricted1);

            let alpha1 = self.attractor(not_x, &gamma, omega1_not_x_restricted1)?;

            trace!("{indent}alpha': {:?}", alpha1);

            let gamma_restricted = gamma.minus_function(&C1_restricted)?;

            debug!("{indent}zielonka_family_opt((gamma | C') \\ alpha')");

            let (omega2_0, omega2_1) = self.zielonka_family_optimised(gamma_restricted.minus(&alpha1)?, depth + 1)?;

            let (omega2_x, omega2_not_x) = x_and_not_x(omega2_0, omega2_1, x);

            let omega1_x_restricted = omega1_x.minus_function(&C1)?;

            let omega1_not_x_restricted = omega1_not_x.minus_function(&C1)?;

            let alpha_restricted = alpha.minus_function(&C1)?;

            let omega2_x_result = omega2_x.or(&omega1_x_restricted.or(&alpha_restricted)?)?;

            let omega2_not_x_result = omega2_not_x.or(&omega1_not_x_restricted)?.or(&alpha1)?;

            debug!("{indent}return (omega''_0, omega''_1)");

            Ok(combine(omega2_x_result, omega2_not_x_result, x))

    }

    fn attractor(&mut self, alpha: Player, gamma: &Submap, mut A: Submap) -> Result<Submap, MercError> {

        self.temp_vertices.fill(false);

        for v in A.iter_vertices() {

            self.temp_queue.push(v);

            // temp_vertices keeps track of which vertices are in the queue.

            self.temp_vertices.set(*v, true);

        }

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

            self.temp_vertices.set(*w, false);

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

                let mut a = gamma[v].and(&A[w])?.and(edge_guard)?;

                if a.satisfiable() {

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

                        // 8. a := gamma(v) \intersect \theta(v, w) \intersect A(w)

                        // This assignment has already been computed above.

                    } else {

                        a = gamma[v].clone();

                        for edge_w1 in self.game.outgoing_conf_edges(v) {

                            let tmp = gamma[v].and(edge_w1.configuration())?.and(&gamma[edge_w1.to()])?;

                            if tmp.satisfiable() {

                                let tmp = edge_w1.configuration().and(&gamma[edge_w1.to()])?;

                                a = a.and(&minus(self.game.configuration(), &tmp)?.or(&A[edge_w1.to()])?)?;

                            }

                    if minus(&a, &A[v])?.satisfiable() {

                        A.set(v, A[v].or(&a)?);

                        if !self.temp_vertices[*v] {

                            self.temp_queue.push(v);

                            self.temp_vertices.set(*v, true);

                        }

                    }

                }

        debug_assert!(

            !self.temp_vertices.any(),

        Ok(A)

    }

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

        let mut highest = usize::MIN;

        let mut lowest = usize::MAX;

        for v in V.iter_vertices() {

            let prio = self.game.priority(v);

            highest = highest.max(*prio);

            lowest = lowest.min(*prio);

        }

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

    }

    fn check_partition(&self, W0: &Submap, W1: &Submap, V: &Submap) -> Result<(), MercError> {

        for v in V.iter_vertices() {

            let tmp = W0[v].or(&W1[v])?;

            debug_assert!(

                tmp == V[v],

            debug_assert!(

                !W0[v].and(&W1[v])?.satisfiable(),

        Ok(())

    }

pub fn minus(lhs: &BDDFunction, rhs: &BDDFunction) -> AllocResult<BDDFunction> {

    lhs.and(&rhs.not()?)

}

    fn new(initial: BDDFunction, false_bdd: BDDFunction, num_of_vertices: usize) -> Self {

            mapping: vec![initial.clone(); num_of_vertices],

            false_bdd,

            non_empty_count: if initial.satisfiable() {

                num_of_vertices // If the initial function is satisfiable, all entries are non-empty.

                0

    }

    pub fn iter_vertices(&self) -> impl Iterator<Item = VertexIndex> + '_ {

        self.mapping.iter().enumerate().filter_map(|(i, func)| {

            if func.satisfiable() {

                Some(VertexIndex::new(i))

                None

        })

    }

    fn set(&mut self, index: VertexIndex, func: BDDFunction) {

        let was_empty = !self.mapping[*index].satisfiable();

        let is_empty = !func.satisfiable();

        self.mapping[*index] = func;

        if was_empty && !is_empty {

            self.non_empty_count += 1;

        } else if !was_empty && is_empty {

        }

    }

    fn is_empty(&self) -> bool {

        self.non_empty_count == 0

    }

    fn len(&self) -> usize {

        self.mapping.len()

    }

    fn minus(mut self, other: &Submap) -> Result<Submap, MercError> {

        for (i, func) in self.mapping.iter_mut().enumerate() {

            let was_satisfiable = func.satisfiable();

            *func = minus(func, &other.mapping[i])?;

            let is_satisfiable = func.satisfiable();

            if was_satisfiable && !is_satisfiable {

                self.non_empty_count -= 1;

            }

        Ok(self)

    }

    fn or(mut self, other: &Submap) -> Result<Submap, MercError> {

        for (i, func) in self.mapping.iter_mut().enumerate() {

            let was_satisfiable = func.satisfiable();

            *func = func.or(&other.mapping[i])?;

            let is_satisfiable = func.satisfiable();

            if !was_satisfiable && is_satisfiable {

                self.non_empty_count += 1;

            }

        Ok(self)

    }

    fn minus_function(mut self, configuration: &BDDFunction) -> Result<Submap, MercError> {

        for (i, func) in self.mapping.iter_mut().enumerate() {

            let was_satisfiable = func.satisfiable();

            *func = minus(func, configuration)?;

            let is_satisfiable = func.satisfiable();

            if was_satisfiable && !is_satisfiable {

                self.non_empty_count -= 1;

            }

        Ok(self)

    }

    pub fn iter(&self) -> impl Iterator<Item = (VertexIndex, &BDDFunction)> {

        self.mapping

            .iter()

            .enumerate()

            .map(|(i, func)| (VertexIndex::new(i), func))

    }

    fn index(&self, index: VertexIndex) -> &Self::Output {

        &self.mapping[*index]

    }

            .with_manager_exclusive(|manager| {

                AllocResult::from_iter(manager.add_vars(3).map(|i| BDDFunction::var(manager, i)))

            })

        let false_bdd = manager_ref.with_manager_shared(|manager| BDDFunction::f(manager));

        random_test(100, |rng| {

            let manager_ref = oxidd::bdd::new_manager(2048, 1024, 1);

            let vpg = random_variability_parity_game(&manager_ref, rng, true, 20, 3, 3, 3).unwrap();

            let solution = solve_variability_zielonka(&manager_ref, &vpg, ZielonkaVariant::Family, false).unwrap();

            verify_variability_product_zielonka_solution(&vpg, &solution).unwrap();

        })

        random_test(100, |rng| {

            let manager_ref = oxidd::bdd::new_manager(2048, 1024, 1);

            let vpg = random_variability_parity_game(&manager_ref, rng, true, 20, 3, 3, 3).unwrap();

            let solution =

                solve_variability_zielonka(&manager_ref, &vpg, ZielonkaVariant::FamilyOptimisedLeft, false).unwrap();

            let solution_expected =

                solve_variability_zielonka(&manager_ref, &vpg, ZielonkaVariant::Family, false).unwrap();

            debug_assert_eq!(solution[0], solution_expected[0]);

            debug_assert_eq!(solution[1], solution_expected[1]);

        })