pub fn read_vpg(manager: &BDDManagerRef, reader: impl Read) -> Result<VariabilityParityGame, MercError> {

    info!("Reading variability parity game in .vpg format...");

    manager.with_manager_exclusive(|manager| {

        debug_assert_eq!(

            manager.num_vars(),

    });

    let mut lines = LineIterator::new(reader);

    lines.advance();

    let header = lines

        .get()

        .ok_or(IOError::InvalidHeader("The first line should be the confs header"))?;

    let confs_regex = Regex::new(r#"confs\s+([+-01]*)\s*;"#).expect("Regex compilation should not fail");

    let (_, [configurations_txt]) = confs_regex

        .captures(header)

        .ok_or(IOError::InvalidHeader("header does not match confs <configurations>;"))?

        .extract();

    let (variables, configurations) = parse_configuration(manager, configurations_txt)?;

    let header_regex = Regex::new(r#"parity\s+([0-9]+)\s*;"#).expect("Regex compilation should not fail");

    let header = lines

        .next()

        .ok_or(IOError::InvalidHeader("The second line should be the parity header"))?;

    let (_, [num_of_vertices_txt]) = header_regex

        .captures(header)

        .ok_or(IOError::InvalidHeader(

            "header does not match parity <num_of_vertices>;",

        ))?

        .extract();

    let num_of_vertices: usize = num_of_vertices_txt.parse()?;

    let mut owner: Vec<Player> = vec![Player::Even; num_of_vertices];

    let mut priority: Vec<Priority> = vec![Priority::new(0); num_of_vertices];

    let mut vertices: Vec<usize> = Vec::with_capacity(num_of_vertices + 1);

    let mut edges_to: Vec<VertexIndex> = Vec::with_capacity(num_of_vertices);

    let mut edges_configuration: Vec<BDDFunction> = Vec::with_capacity(num_of_vertices);

    let progress = TimeProgress::new(|(amount, total): (usize, usize)| info!("Read {} vertices ({}%)...", amount, amount * 100 / total), 1);

    let mut vertex_count = 0;

    while let Some(line) = lines.next() {

        let mut parts = line.split_whitespace();

        let index: usize = parts

            .next()

            .ok_or(IOError::InvalidLine("Expected at least <index> ...;"))?

            .parse()?;

        let vertex_priority: usize = parts

            .next()

            .ok_or(IOError::InvalidLine("Expected at least <index> <priority> ...;"))?

            .parse()?;

        let vertex_owner = Player::from_index(

            parts

                .next()

                .ok_or(IOError::InvalidLine(

                    "Expected at least <index> <priority> <owner> ...;",

                ))?

                .parse()?,

        owner[index] = vertex_owner;

        priority[index] = Priority::new(vertex_priority);

        vertices.push(edges_configuration.len());

        for successors in parts {

            for successor in successors

                .trim_end_matches(';')

                .split(',')

                .filter(|s| !s.trim().is_empty())

                let parts: Vec<&str> = successor.trim().split('|').collect();

                let successor_index: usize = parts[0].trim().parse()?;

                edges_to.push(VertexIndex::new(successor_index));

                if parts.len() > 1 {

                    let config = parse_configuration_set(manager, &variables, parts[1].trim())?;

                    edges_configuration.push(config);

        progress.print((vertex_count + 1, num_of_vertices));

        vertex_count += 1;

    vertices.push(edges_configuration.len());

    Ok(VariabilityParityGame::new(

        ParityGame::new(VertexIndex::new(0), owner, priority, vertices, edges_to),

        configurations,

        variables,

        edges_configuration,

    ))

}

fn parse_configuration(manager: &BDDManagerRef, config: &str) -> Result<(Vec<BDDFunction>, BDDFunction), MercError> {

    if let Some(first_part) = config.split('+').next() {

        let variables = manager.with_manager_exclusive(|manager| {

            manager

                .add_vars(first_part.len() as u32)

                .map(|i| BDDFunction::var(manager, i))

                .collect::<Result<Vec<_>, _>>()

        })?;

        let configuration = parse_configuration_set(manager, &variables, config)?;

        return Ok((variables, configuration));

}

pub fn parse_configuration_set(

    manager_ref: &BDDManagerRef,

    variables: &[BDDFunction],

    config: &str,

) -> Result<BDDFunction, MercError> {

    manager_ref.with_manager_shared(|manager| -> Result<BDDFunction, MercError> {

        let mut result = BDDFunction::f(manager);

        for part in config.split('+') {

            let mut conjunction = BDDFunction::t(manager);

            for (i, c) in part.chars().enumerate() {

                let var = &variables[i];

                match c {

                    '1' => conjunction = conjunction.and(var)?,

                    '0' => conjunction = minus(&conjunction, var)?,

                    '-' => {} // don't care

            result = result.or(&conjunction)?;

        Ok(result)

    })

}

    fn test_read_vpg() {

        let manager = oxidd::bdd::new_manager(2048, 1024, 8);

        let parity_game = read_vpg(

            &manager,

            include_bytes!("../../../../examples/vpg/example.vpg") as &[u8],

        .unwrap();

        assert_eq!(parity_game.num_of_vertices(), 61014);

    }