demystify 0.2.0

#![allow(clippy::needless_range_loop)]
/// This module contains the implementation of parsing and processing functions for problem files.
/// It includes functions for parsing DIMACS files, extracting annotations from Essence' files,
/// and creating data structures to represent the parsed information.
///
/// The main struct in this module is `PuzzleParse`, which represents the result of parsing a DIMACS file.
/// It contains various fields to store the parsed information, such as the annotations from the Essence' file,
/// the SAT instance parsed from the DIMACS file, mappings between literals and SAT integers, and more.
use anyhow::{Context, bail};
use itertools::Itertools;
use regex::Regex;
use rustsat::instances::{self, BasicVarManager, Cnf, SatInstance};
use rustsat::types::Lit;

use std::cmp::max;
use std::collections::{BTreeMap, BTreeSet, HashSet};

use std::fs;
use std::io::BufReader;
use std::io::prelude::*;

use std::path::PathBuf;
use std::sync::Arc;

use tracing::{debug, info};

use std::fs::File;
use std::io;

use crate::problem::util::exec::ProgramRunner;
use crate::problem::util::parsing;
use crate::problem::{PuzLit, PuzVar};

use super::VarValPair;
use super::util::{FindVarConnections, safe_insert};

#[derive(Debug, Clone, PartialEq)]
pub struct EPrimeAnnotations {
    /// The set of variables in the Essence' file.
    pub vars: BTreeSet<String>,
    /// The set of auxiliary variables in the Essence'file.
    pub auxvars: BTreeSet<String>,
    /// The constraints in the Essence' file, represented as a mapping from constraint name to constraint expression.
    pub cons: BTreeMap<String, String>,
    /// 'reveal', which allow extra information to be added during solving.
    pub reveal: BTreeMap<String, String>,
    /// values from the 'reveal' map (for ease of searching)
    pub reveal_values: BTreeSet<String>,
    /// The parameters read from the param file
    pub(crate) params: BTreeMap<String, serde_json::value::Value>,
    /// The kind of puzzle
    pub kind: Option<String>,
    /// Informational strings collected from $#INFO directives
    pub info: Vec<String>,
    /// SVG decoration flags collected from $#DEC directives
    pub decs: Vec<String>,
}

impl EPrimeAnnotations {
    /// Returns a reference to all parameters
    #[must_use]
    pub fn params(&self) -> &BTreeMap<String, serde_json::value::Value> {
        &self.params
    }

    #[must_use]
    pub fn has_param(&self, s: &str) -> bool {
        self.params.contains_key(s)
    }

    pub fn param_bool(&self, s: &str) -> anyhow::Result<bool> {
        serde_json::from_value(
            self.params
                .get(s)
                .context(format!("Missing param: {s}"))?
                .clone(),
        )
        .context(format!("Param {s} is not bool"))
    }

    pub fn param_i64(&self, s: &str) -> anyhow::Result<i64> {
        serde_json::from_value(
            self.params
                .get(s)
                .context(format!("Missing param: {s}"))?
                .clone(),
        )
        .context(format!("Param {s} is not int"))
    }

    pub fn param_vec_i64(&self, s: &str) -> anyhow::Result<Vec<i64>> {
        // Conjure produces arrays as maps, so we need to fix up
        let map: BTreeMap<i64, i64> = serde_json::from_value(
            self.params
                .get(s)
                .context(format!("Missing param: {s}"))?
                .clone(),
        )
        .context(format!("Param {s} is not an array of ints"))?;

        let mut ret: Vec<i64> = vec![0; map.len()];

        for i in 0..map.len() {
            ret[i] = *map
                .get(&((i + 1) as i64))
                .context(format!("Malformed param? {s}"))?;
        }

        Ok(ret)
    }

    pub fn param_vec_vec_i64(&self, s: &str) -> anyhow::Result<Vec<Vec<i64>>> {
        // Conjure produces arrays as maps, so we need to fix up
        let map: BTreeMap<i64, BTreeMap<i64, i64>> = serde_json::from_value(
            self.params
                .get(s)
                .context(format!("Missing param: {s}"))?
                .clone(),
        )
        .context(format!("Param {s} is not a 2d array of ints"))?;

        let mut ret: Vec<Vec<i64>> = vec![vec![]; map.len()];

        for i in 0..map.len() {
            let row = map
                .get(&((i + 1) as i64))
                .context(format!("Malformed param? {s}"))?;
            let mut rowvec: Vec<i64> = vec![0; row.len()];
            for j in 0..row.len() {
                rowvec[j] = *row
                    .get(&((j + 1) as i64))
                    .context(format!("Malformed param? {s}"))?;
            }

            ret[i] = rowvec;
        }

        Ok(ret)
    }

    pub fn param_vec_string(&self, s: &str) -> anyhow::Result<Vec<String>> {
        let map: BTreeMap<i64, serde_json::Value> = serde_json::from_value(
            self.params
                .get(s)
                .context(format!("Missing param: {s}"))?
                .clone(),
        )
        .context(format!("Param {s} is not an array of strings"))?;

        let mut ret: Vec<String> = vec![String::new(); map.len()];

        for i in 0..map.len() {
            ret[i] = map
                .get(&((i + 1) as i64))
                .context(format!("Malformed param? {s}"))?
                .to_string();
        }

        Ok(ret)
    }

    pub fn param_vec_vec_string(&self, s: &str) -> anyhow::Result<Vec<Vec<String>>> {
        // Conjure produces arrays as maps, so we need to fix up
        let map: BTreeMap<i64, BTreeMap<i64, serde_json::Value>> = serde_json::from_value(
            self.params
                .get(s)
                .context(format!("Missing param: {s}"))?
                .clone(),
        )
        .context(format!("Param {s} is not a 2d array of strings"))?;

        let mut ret: Vec<Vec<String>> = vec![vec![]; map.len()];

        for i in 0..map.len() {
            let row = map
                .get(&((i + 1) as i64))
                .context(format!("Malformed param? {s}"))?;
            let mut rowvec: Vec<String> = vec![String::new(); row.len()];
            for j in 0..row.len() {
                rowvec[j] = row
                    .get(&((j + 1) as i64))
                    .context(format!("Malformed param? {s}"))?
                    .to_string();
            }

            ret[i] = rowvec;
        }

        Ok(ret)
    }

    pub fn param_vec_vec_option_i64(&self, s: &str) -> anyhow::Result<Vec<Vec<Option<i64>>>> {
        // Conjure produces arrays as maps, so we need to fix up
        let map: BTreeMap<i64, BTreeMap<i64, Option<i64>>> = serde_json::from_value(
            self.params
                .get(s)
                .context(format!("Missing param: {s}"))?
                .clone(),
        )
        .context(format!("Param {s} is not a 2d array of ints and nulls"))?;

        let mut ret: Vec<Vec<Option<i64>>> = vec![vec![]; map.len()];

        for i in 0..map.len() {
            let row = map
                .get(&((i + 1) as i64))
                .context(format!("Malformed param? {s}"))?;
            let mut rowvec: Vec<Option<i64>> = vec![None; row.len()];
            for j in 0..row.len() {
                rowvec[j] = *row
                    .get(&((j + 1) as i64))
                    .context(format!("Malformed param? {s}"))?;
            }

            ret[i] = rowvec;
        }

        Ok(ret)
    }

    /// Parses the concatenated `info` strings as a JSON object
    pub fn parse_info_json<T: serde::de::DeserializeOwned>(&self) -> anyhow::Result<T> {
        let json_str = self.info.concat();
        if json_str.trim().is_empty() {
            serde_json::from_str("{}").context("Failed to parse empty info as JSON object")
        } else {
            serde_json::from_str(&json_str).context("Failed to parse info as JSON")
        }
    }
}

/// The fully-parsed puzzle, combining the Essence' annotations with all SAT encoding maps.
///
/// # Architecture overview
///
/// Conjure translates an `.eprime` model + `.param` file into a DIMACS CNF.  That CNF uses two
/// distinct encodings for the puzzle variables:
///
/// * **Direct encoding** — each assignment `var[i,j] = v` becomes one SAT literal.
///   `litmap` / `invlitmap` translate between these puzzle-level assignments and raw SAT literals.
///
/// * **Order encoding** — each threshold `var[i,j] >= v` becomes one SAT literal.
///   `order_encoding_map` / `inv_order_encoding_map` handle this encoding.
///   Most code only needs the direct encoding; the order maps are used when scanning the full SAT
///   instance (e.g. `all_var_related_lits`).
///
/// ## Key maps and their relationships
///
/// ```text
/// PuzLit (var[i,j]=v, eq/neq)  ←→  Lit (raw SAT integer)
///     litmap:     PuzLit → Lit
///     invlitmap:  Lit → BTreeSet<PuzLit>   (set because order-encoding Lits map to many PuzLits)
///
/// PuzVar (var[i,j])  →  domain values
///     domainmap:  PuzVar → BTreeSet<i64>
///
/// Constraint instances ($#CON class[i,j,...] = true):
///     conset:         Lit(CON=true) → rendered English description
///     invconset:      description   → Lit(CON=true)     (inverse of conset)
///     varlits_in_con: Lit(CON=true) → Vec<Lit>          (the VAR-encoding lits reachable from
///                                                         this constraint in the SAT formula;
///                                                         use direct_or_ordered_lit_to_varvalpair
///                                                         to convert these back to PuzLits)
///
/// Convenience sets:
///     varset_lits:     all positive direct-encoding Lits for $#VAR variables
///     varset_lits_neg: all negative direct-encoding Lits for $#VAR variables
///     conset_lits:     all positive direct-encoding Lits for $#CON variables
/// ```
///
/// ## Reveal map
///
/// `$#AUX` variables expose "extra" assignments when their trigger literal is proved.
/// `reveal_map[x] = y` means: when `x` is deduced true, also treat `y` as known.
#[derive(Debug, Clone, PartialEq)]
pub struct PuzzleParse {
    /// Annotations extracted from the `.eprime` file (VAR/CON/AUX names, param values, etc.).
    pub eprime: EPrimeAnnotations,
    /// The full SAT instance (all clauses added by Conjure).
    pub satinstance: SatInstance,
    /// Cached CNF form of `satinstance` (computed once, reused frequently).
    pub cnf: Option<Arc<Cnf>>,

    // ── Direct encoding ──────────────────────────────────────────────────────
    /// `PuzLit(var[i,j]=v, eq)` → raw SAT `Lit`.  Covers both $#VAR and $#CON variables.
    pub litmap: BTreeMap<PuzLit, Lit>,
    /// Raw SAT `Lit` → set of `PuzLit`s it encodes.
    /// A set because the same Lit can appear in multiple order-encoding threshold assignments.
    pub invlitmap: BTreeMap<Lit, BTreeSet<PuzLit>>,
    /// `PuzVar` → the set of integer values in its domain.
    pub domainmap: BTreeMap<PuzVar, BTreeSet<i64>>,

    // ── Constraint maps ($#CON) ───────────────────────────────────────────────
    /// `Lit(CON_instance=true)` → rendered English description of that constraint instance.
    /// Keys are identical to `conset_lits`.
    pub conset: BTreeMap<Lit, String>,
    /// Rendered description → `Lit(CON_instance=true)`.  Inverse of `conset`.
    pub invconset: BTreeMap<String, Lit>,
    /// For each CON instance Lit, the list of VAR-encoding Lits reachable from it in the SAT
    /// formula (via `FindVarConnections`).  Use `direct_or_ordered_lit_to_varvalpair` to convert
    /// these back to `VarValPair`s.
    pub varlits_in_con: BTreeMap<Lit, Vec<Lit>>,

    // ── Convenience literal sets ──────────────────────────────────────────────
    /// All positive direct-encoding Lits for $#VAR variables (`var[i,j]=v` true).
    pub varset_lits: BTreeSet<Lit>,
    /// All negative direct-encoding Lits for $#VAR variables (`var[i,j]=v` false).
    pub varset_lits_neg: BTreeSet<Lit>,
    /// All positive Lits for $#CON instances (`CON[...]=true`).  Same keys as `conset`.
    pub conset_lits: BTreeSet<Lit>,

    // ── Order encoding (rarely needed directly) ───────────────────────────────
    /// `PuzVar` → set of SAT Lits used to order-encode it (`var >= v` thresholds).
    pub order_encoding_map: BTreeMap<PuzVar, HashSet<Lit>>,
    /// SAT `Lit` → the `PuzVar` whose order encoding it belongs to.
    pub inv_order_encoding_map: BTreeMap<Lit, PuzVar>,
    /// Union of all Lits across all order encodings.
    pub order_encoding_all_lits: BTreeSet<Lit>,

    // ── Reveal map ($#AUX) ────────────────────────────────────────────────────
    /// When `x` is deduced true, `reveal_map[x]` should also be added to the known-lit set.
    /// Populated from `$#AUX` directives.
    pub reveal_map: BTreeMap<Lit, Lit>,
}

impl PuzzleParse {
    #[must_use]
    pub fn new_from_eprime(
        vars: BTreeSet<String>,
        auxvars: BTreeSet<String>,
        cons: BTreeMap<String, String>,
        reveal: BTreeMap<String, String>,
        params: BTreeMap<String, serde_json::value::Value>,
        kind: Option<String>,
        info: Vec<String>,
    ) -> PuzzleParse {
        PuzzleParse {
            eprime: EPrimeAnnotations {
                vars,
                auxvars,
                cons,
                reveal: reveal.clone(),
                reveal_values: reveal.values().cloned().collect(),
                params,
                kind,
                info,
                decs: vec![],
            },
            satinstance: SatInstance::new(),
            cnf: None,
            litmap: BTreeMap::new(),
            invlitmap: BTreeMap::new(),
            domainmap: BTreeMap::new(),
            order_encoding_map: BTreeMap::new(),
            inv_order_encoding_map: BTreeMap::new(),
            order_encoding_all_lits: BTreeSet::new(),
            conset: BTreeMap::new(),
            invconset: BTreeMap::new(),
            varlits_in_con: BTreeMap::new(),
            varset_lits: BTreeSet::new(),
            varset_lits_neg: BTreeSet::new(),
            conset_lits: BTreeSet::new(),
            reveal_map: BTreeMap::new(),
        }
    }

    fn finalise(&mut self) -> anyhow::Result<()> {
        {
            let mut newlitmap = BTreeMap::new();
            // Make sure 'litmap' contains both positive and negative version of every problem literal
            for (key, &value) in &self.litmap {
                if let Some(&val) = self.litmap.get(&key.neg()) {
                    if val != -value {
                        bail!(
                            "Malformed Savilerow DIMACS output: Issue with {:?}",
                            (key, value)
                        );
                    }
                } else {
                    safe_insert(&mut newlitmap, key.neg(), -value)?;
                }
            }
            self.litmap.extend(newlitmap);
        }

        // Set up inverse of 'litmap', mapping from integers to PuzLit objects
        for (key, value) in &self.litmap {
            self.invlitmap
                .entry(*value)
                .or_default()
                .insert(key.clone());
        }

        // Get the domain of each variable quickly
        for lit in self.litmap.keys() {
            let var_id = lit.var();
            if lit.sign() {
                self.domainmap.entry(var_id).or_default().insert(lit.val());
            }
        }

        for (puzlit, &lit) in &self.litmap {
            let var = puzlit.var();

            let name = var.name();
            if self.eprime.vars.contains(name) {
                self.varset_lits.insert(lit);
                if !puzlit.sign() {
                    self.varset_lits_neg.insert(lit);
                }
            } else if self.eprime.auxvars.contains(name) || name.starts_with("conjure_aux") {
                // don't care about aux vars (conjure_aux* are generated by Conjure internally)
            } else if self.eprime.cons.contains_key(name) {
                // constraints are specially dealt with above
            } else if self.eprime.reveal_values.contains(name) {
                // reveal_values are dealt with below,
                // as we need all of 'varset' to be complete first
                // So here we just allow the name
            } else {
                bail!("Cannot identify {:?}, should it be marked as AUX?", puzlit);
            }
        }

        for (puzlit, &lit) in &self.litmap {
            let var = puzlit.var();
            let name = var.name();
            if self.eprime.reveal.contains_key(name) && puzlit.sign() {
                let mut index = puzlit.varval().var().indices().clone();
                index.push(puzlit.varval().val);

                let target_name = self.eprime.reveal.get(name).unwrap();

                let target_puzvar = PuzVar::new(target_name, index);
                let target_varvalpair = VarValPair::new(&target_puzvar, 1);
                let target_puzlit = PuzLit::new_eq(target_varvalpair);

                if let Some(&target_lit) = self.litmap.get(&target_puzlit) {
                    safe_insert(&mut self.reveal_map, lit, target_lit)
                        .context("Some variable used in two 'REVEAL'")?;
                } else {
                    info!("Can't find {target_puzlit} from {puzlit}");
                }
            }
        }

        let mut usedconstraintnames: HashSet<String> = HashSet::new();

        let fvc = FindVarConnections::new(&self.satinstance, &self.all_var_related_lits());

        // Tidy up and check constraints
        for (varid, vals) in &self.domainmap {
            if let Some(template_string) = self.eprime.cons.get(varid.name()) {
                debug!(target: "parser", "Found {:?} in constraint {:?}", varid, varid.name());

                if !vals.contains(&0) {
                    bail!(format!("CON {:?} cannot be made false", varid));
                }

                if !vals.contains(&1) {
                    bail!(format!("CON {:?} cannot be made true", varid));
                }

                if vals.len() != 2 {
                    bail!(format!(
                        "CON {:?} domain is {:?}, should be (0,1)",
                        varid, vals
                    ));
                }

                let constraintname = parsing::parse_constraint_name(
                    template_string,
                    &self.eprime.params,
                    &varid.indices,
                )?;

                // Check is we have used this name before
                if usedconstraintnames.contains(&constraintname) {
                    bail!(format!(
                        "CON name {:?} used twice. This should already have substitutions done, so if you see '{{' or '}}' check your formatting string.",
                        constraintname
                    ))
                }
                usedconstraintnames.insert(constraintname.clone());

                // TODO: Skip constraints which are already parsed,
                // or trivial (parse.py 270 -- 291)

                let puzlit = PuzLit::new_eq(VarValPair::new(varid, 1));
                let lit = *self.litmap.get(&puzlit).unwrap();
                safe_insert(&mut self.conset, lit, constraintname.clone())?;
                safe_insert(&mut self.invconset, constraintname.clone(), lit)?;
                self.conset_lits.insert(lit);
                safe_insert(&mut self.varlits_in_con, lit, fvc.get_connections(lit))?;
                info!(
                    "MAP {} {:?}",
                    &constraintname,
                    self.varlits_in_con.get(&lit).unwrap()
                );
            }
        }

        Ok(())
    }

    #[must_use]
    pub fn lit_is_con(&self, lit: &Lit) -> bool {
        self.conset_lits.contains(lit)
    }

    #[must_use]
    pub fn lit_to_con(&self, lit: &Lit) -> &String {
        assert!(self.lit_is_con(lit));
        self.conset.get(lit).unwrap()
    }

    #[must_use]
    pub fn lit_is_var(&self, lit: &Lit) -> bool {
        self.varset_lits.contains(lit)
    }

    #[must_use]
    pub fn lit_to_vars(&self, lit: &Lit) -> &BTreeSet<PuzLit> {
        self.invlitmap.get(lit).expect("IE: Bad lit")
    }

    // All lits included in both the direct and ordered encoding
    // of VARs
    #[must_use]
    pub fn all_var_related_lits(&self) -> HashSet<Lit> {
        let ordered_var: BTreeSet<Lit> = self
            .order_encoding_map
            .iter()
            .filter(|(k, _)| self.eprime.vars.contains(k.name()))
            .flat_map(|(_, v)| v)
            .copied()
            .collect();

        self.varset_lits.union(&ordered_var).copied().collect()
    }

    // All VarValPairs included in VARs
    #[must_use]
    pub fn all_var_varvals(&self) -> BTreeSet<VarValPair> {
        self.varset_lits
            .iter()
            .flat_map(|x| self.lit_to_vars(x))
            .map(super::PuzLit::varval)
            .collect()
    }

    /// Given a collection of Lits representing both direct and ordered
    /// representations, collect them into a collection of `VarValPair`s
    #[must_use]
    pub fn direct_or_ordered_lit_to_varvalpair(&self, lit: &Lit) -> BTreeSet<VarValPair> {
        let direct_lits = self.invlitmap.get(lit).cloned().unwrap_or_default();

        let order_lits = if let Some(var) = self.inv_order_encoding_map.get(lit) {
            self.domainmap
                .get(var)
                .unwrap()
                .iter()
                .map(|&d| VarValPair::new(var, d))
                .collect_vec()
        } else {
            vec![]
        };

        direct_lits
            .into_iter()
            .map(|x| x.varval())
            .chain(order_lits)
            .collect()
    }

    #[must_use]
    pub fn has_facts(&self) -> bool {
        !self.eprime.reveal.is_empty()
    }

    #[must_use]
    pub fn constraints(&self) -> BTreeSet<String> {
        self.invconset.keys().cloned().collect()
    }

    pub fn constraint_roots(&self) -> BTreeSet<String> {
        self.eprime.cons.keys().cloned().collect()
    }

    #[must_use]
    pub fn constraint_scope(&self, con: &String) -> BTreeSet<VarValPair> {
        let lit = self.invconset.get(con).expect("IE: Bad constraint name");

        let lits = self.varlits_in_con.get(lit).expect("IE: Bad constraint");
        let puzlits = lits
            .iter()
            .flat_map(|l| self.direct_or_ordered_lit_to_varvalpair(l))
            .collect_vec();

        BTreeSet::from_iter(puzlits)
    }

    pub fn filter_out_constraint(&mut self, con: &str) {
        assert!(
            self.eprime.cons.contains_key(con),
            "Filtered constraint is not present: {con}"
        );
        let mut new_conset_lits = BTreeSet::new();
        for l in &self.conset_lits {
            let puzvars = self.invlitmap.get(l).unwrap();
            if !puzvars.iter().all(|p| p.var().name() == con) {
                new_conset_lits.insert(*l);
            }
        }
        eprintln!(
            "Removing {}: {} -> {}",
            con,
            self.conset_lits.len(),
            new_conset_lits.len()
        );
        self.conset_lits = new_conset_lits;
    }

    #[must_use]
    pub fn get_matrix_indices(&self, var: &str) -> Option<Vec<i64>> {
        let mut domain: Option<Vec<i64>> = None;
        for key in self.domainmap.keys() {
            if key.name() == var {
                let indices = key.indices();
                if let Some(mut current_domain) = domain {
                    for i in 0..current_domain.len() {
                        current_domain[i] = max(current_domain[i], indices[i]);
                    }
                    domain = Some(current_domain);
                } else {
                    domain = Some(indices.clone());
                }
            }
        }
        domain
    }
}

struct ParsedEprimeData {
    vars: BTreeSet<String>,
    auxvars: BTreeSet<String>,
    cons: BTreeMap<String, String>,
    factvars: BTreeMap<String, String>,
    kind: Option<String>,
    info: Vec<String>,
    decs: Vec<String>,
}

fn parse_eprime_file(in_path: &PathBuf) -> anyhow::Result<ParsedEprimeData> {
    info!(target: "parser", "reading DIMACS {:?}", in_path);

    let mut vars: BTreeSet<String> = BTreeSet::new();
    let mut puzzle: BTreeSet<String> = BTreeSet::new();

    let mut auxvars: BTreeSet<String> = BTreeSet::new();

    let mut cons: BTreeMap<String, String> = BTreeMap::new();

    let mut factvars: BTreeMap<String, String> = BTreeMap::new();

    let mut info: Vec<String> = Vec::new();
    let mut decs: Vec<String> = Vec::new();

    let mut kind: Option<String> = None;

    let conmatch = Regex::new(r#"\$#CON (.*) "(.*)" *$"#).unwrap();

    let file = File::open(in_path)?;
    let reader = io::BufReader::new(file);

    let mut all_names = HashSet::new();

    for line in reader.lines() {
        let line = line?;

        if line.contains("$#") {
            debug!(target: "parser", "line {:?}", line);
            let parts: Vec<&str> = line.split_whitespace().collect();

            if line.starts_with("$#VAR") {
                let v = parts[1].to_string();
                info!(target: "parser", "Found VAR: '{}'", v);

                if all_names.contains(&v) {
                    bail!(format!("{v} defined twice"));
                }
                all_names.insert(v.clone());

                vars.insert(v);
            } else if line.starts_with("$#PUZZLE") {
                let v = parts[1].to_string();
                info!(target: "parser", "Found PUZZLE: '{}'", v);

                if all_names.contains(&v) {
                    bail!(format!("{v} defined twice"));
                }
                all_names.insert(v.clone());

                puzzle.insert(v);
            } else if line.starts_with("$#CON") {
                info!(target: "parser", "{}", line);
                let captures = conmatch
                    .captures(&line)
                    .context(format!("Malformed $#CON line: {line}"))?;

                let con_name = captures.get(1).unwrap().as_str().to_string();
                let con_value = captures.get(2).unwrap().as_str().to_string();

                info!(target: "parser", "Found CON: '{}' '{}'", con_name, con_value);

                if all_names.contains(&con_name) {
                    bail!(format!("{con_name} defined twice"));
                }
                all_names.insert(con_name.clone());

                if cons.contains_key(&con_name) {
                    bail!(format!("{} defined twice", con_name));
                }
                safe_insert(&mut cons, con_name, con_value)?;
            } else if line.starts_with("$#AUX") {
                let v = parts[1].to_string();
                info!(target: "parser", "Found Aux VAR: '{}'", v);

                if all_names.contains(&v) {
                    bail!(format!("{v} defined twice"));
                }
                all_names.insert(v.clone());

                auxvars.insert(v);
            } else if line.starts_with("$#KIND") {
                let v = parts[1].to_string();
                if kind.is_some() {
                    bail!("Cannot have two 'KIND' statements");
                }
                kind = Some(v);
            } else if line.starts_with("$#INFO") {
                // Collect the rest of the line after $#INFO as an info string
                let info_string = line.strip_prefix("$#INFO").unwrap_or("").trim().to_string();
                info!(target: "parser", "Found INFO: '{}'", info_string);
                info.push(info_string);
            } else if line.starts_with("$#DEC ") {
                let dec_string = line.strip_prefix("$#DEC ").unwrap_or("").trim().to_string();
                info!(target: "parser", "Found DEC: '{}'", dec_string);
                decs.push(dec_string);
            } else if line.starts_with("$#REVEAL ") {
                if parts.len() != 3 {
                    bail!(format!(
                        "Invalid format, should be $#REVEAL <orig> <reveal> : {line} > {parts:?}"
                    ));
                }

                let key = parts[1].to_owned();
                let value = parts[2].to_owned();

                if !vars.contains(&key) {
                    bail!(format!(
                        "{key} from a REVEAL must be first be defined as a VAR"
                    ));
                }

                if all_names.contains(&value) {
                    bail!(format!("{value} defined twice"));
                }
                all_names.insert(value.clone());

                safe_insert(&mut factvars, key, value)?;
            } else {
                bail!(format!("Do not understand line '{line}'"));
            }
        }

        for name in &all_names {
            for other in &all_names {
                if name != other && (name.starts_with(other) || other.starts_with(name)) {
                    bail!(format!(
                        "Cannot have one name be a prefix of another: {name} and {other}"
                    ));
                }
            }
        }
    }

    info!(target: "parser", "Names parsed from ESSENCE': vars: {:?} auxvars: {:?} cons {:?}", vars, auxvars, cons);

    Ok(ParsedEprimeData {
        vars,
        auxvars,
        cons,
        factvars,
        kind,
        info,
        decs,
    })
}

fn parse_eprime(in_path: &PathBuf, eprimeparam: &PathBuf) -> anyhow::Result<PuzzleParse> {
    let parsed_eprime = parse_eprime_file(in_path)?;
    let params = read_essence_param(eprimeparam)?;

    let mut puzzleparse = PuzzleParse::new_from_eprime(
        parsed_eprime.vars,
        parsed_eprime.auxvars,
        parsed_eprime.cons,
        parsed_eprime.factvars,
        params,
        parsed_eprime.kind,
        parsed_eprime.info,
    );
    puzzleparse.eprime.decs = parsed_eprime.decs;
    Ok(puzzleparse)
}

type DimacsMaps = (
    BTreeMap<PuzLit, Lit>,
    BTreeMap<PuzVar, HashSet<Lit>>,
    BTreeMap<Lit, PuzVar>,
);

fn read_dimacs_to_maps(in_path: &PathBuf) -> anyhow::Result<DimacsMaps> {
    let dvarmatch = Regex::new(r"c Var '(.*)' direct represents '(.*)' with '(.*)'").unwrap();
    let ovarmatch = Regex::new(r"c Var '(.*)' order represents '(.*)' with '(.*)'").unwrap();

    let file = File::open(in_path)?;
    let reader = io::BufReader::new(file);

    let mut litmap = BTreeMap::new();
    let mut order_encoding_map: BTreeMap<PuzVar, HashSet<Lit>> = BTreeMap::new();
    let mut inv_order_encoding_map = BTreeMap::new();

    for line in reader.lines() {
        let line = line?;
        if line.starts_with("c Var") {
            let dmatch = dvarmatch.captures(&line);
            let omatch = ovarmatch.captures(&line);
            if !(dmatch.is_some() || omatch.is_some()) {
                bail!("Failed to parse '{:?}'", line);
            }

            if let Some(match_) = dmatch {
                let litval = match_[3].parse::<i64>().unwrap();

                if !match_[1].starts_with("aux") && litval != 9_223_372_036_854_775_807 {
                    let satlit = Lit::from_ipasir(
                        i32::try_from(litval)
                            .with_context(|| format!("Number too large: {litval}"))?,
                    )?;
                    let varid = crate::problem::util::parsing::parse_savile_row_name(&match_[1])
                        .with_context(|| {
                            format!("Failed parsing savile row name {}", &match_[1])
                        })?;
                    if let Some(varid) = varid {
                        let puzlit = PuzLit::new_eq(VarValPair::new(
                            &varid,
                            match_[2].parse::<i64>().unwrap(),
                        ));
                        safe_insert(&mut litmap, puzlit, satlit)?;
                    }
                }
            } else {
                let match_ = omatch.unwrap();
                let litval = match_[3].parse::<i64>().unwrap();
                info!(target: "parser", "matches: {:?}", match_);
                if !match_[1].starts_with("aux") && litval != 9_223_372_036_854_775_807 {
                    let satlit = Lit::from_ipasir(i32::try_from(litval)?)?;
                    let varid = crate::problem::util::parsing::parse_savile_row_name(&match_[1])
                        .with_context(|| {
                            format!("Failed parsing savile row name {}", &match_[1])
                        })?;

                    if let Some(varid) = varid {
                        order_encoding_map
                            .entry(varid.clone())
                            .or_default()
                            .insert(satlit);
                        order_encoding_map
                            .entry(varid.clone())
                            .or_default()
                            .insert(-satlit);
                        if let Some(val) = inv_order_encoding_map.get(&satlit)
                            && *val != varid
                        {
                            bail!("{} used for two variables: {} {}", satlit, val, varid);
                        }
                        safe_insert(&mut inv_order_encoding_map, satlit, varid.clone())?;
                        safe_insert(&mut inv_order_encoding_map, -satlit, varid.clone())?;
                    }
                }
            }
        }
    }

    Ok((litmap, order_encoding_map, inv_order_encoding_map))
}

fn update_puzzle_parse_with_maps(
    dimacs: &mut PuzzleParse,
    litmap: BTreeMap<PuzLit, Lit>,
    order_encoding_map: BTreeMap<PuzVar, HashSet<Lit>>,
    inv_order_encoding_map: BTreeMap<Lit, PuzVar>,
) -> anyhow::Result<()> {
    // Update litmap
    dimacs.litmap = litmap;

    // Update order encoding maps
    dimacs.order_encoding_map = order_encoding_map;
    dimacs.inv_order_encoding_map = inv_order_encoding_map;

    // Rebuild order_encoding_all_lits from order_encoding_map
    dimacs.order_encoding_all_lits = BTreeSet::new();
    for lits in dimacs.order_encoding_map.values() {
        for &lit in lits {
            dimacs.order_encoding_all_lits.insert(lit);
        }
    }

    Ok(())
}

fn read_dimacs(in_path: &PathBuf, dimacs: &mut PuzzleParse) -> anyhow::Result<()> {
    let (litmap, order_encoding_map, inv_order_encoding_map) = read_dimacs_to_maps(in_path)?;
    update_puzzle_parse_with_maps(dimacs, litmap, order_encoding_map, inv_order_encoding_map)
}

pub fn parse_essence(eprimein: &PathBuf, eprimeparamin: &PathBuf) -> anyhow::Result<PuzzleParse> {
    //let mut litmap = BTreeMap::new();
    //let mut varlist = Vec::new();

    let tdir = tempfile::Builder::new()
        .prefix(".demystify-")
        .tempdir_in(".")
        .unwrap();

    let eprime = tdir.path().join(eprimein.file_name().unwrap());
    let eprimeparam = tdir.path().join(eprimeparamin.file_name().unwrap());

    fs::copy(eprimein, &eprime)?;
    fs::copy(eprimeparamin, &eprimeparam)?;

    info!("Parsing Essence in TempDir: {tdir:?}");

    let finaleprime: PathBuf;
    let finaleprimeparam: PathBuf;

    info!(target: "parser", "Handling {:?}", eprime);

    // Check if file extension is .essence
    let is_essence = eprime.extension().is_some_and(|ext| ext == "essence");

    // If input is essence, translate to essence' for savilerow
    if is_essence {
        info!(target: "parser", "Running {:?} {:?} through conjure", eprime, eprimeparam);
        let output = ProgramRunner::prepare("conjure", tdir.path())
            .arg("solve")
            .arg("-o")
            .arg(".")
            .arg(eprime.file_name().unwrap())
            .arg(eprimeparam.file_name().unwrap())
            .output()
            .expect("Failed to execute command");

        if !output.status.success() {
            bail!(format!(
                "conjure failed\n{}\n{}",
                String::from_utf8_lossy(&output.stdout),
                String::from_utf8_lossy(&output.stderr)
            ));
        }

        finaleprime = tdir.path().join("model000001.eprime");

        let option_param = fs::read_dir(tdir.path())
            .unwrap()
            .filter_map(Result::ok)
            .find(|d| d.path().extension().and_then(|s| s.to_str()) == Some("param"))
            .map(|d| d.path());

        if let Some(fname) = option_param {
            finaleprimeparam = fname;
        } else {
            bail!("Could not find 'param' file generated by SavileRow");
        }
    } else {
        finaleprime = eprime.clone();
        finaleprimeparam = eprimeparam.clone();
    }

    info!(target: "parser", "Running savilerow on {:?} {:?}", finaleprime, finaleprimeparam);

    let makedimacs = ProgramRunner::prepare("savilerow", tdir.path())
        .arg("-in-eprime")
        .arg(finaleprime.file_name().unwrap())
        .arg("-in-param")
        .arg(finaleprimeparam.file_name().unwrap())
        .arg("-sat-output-mapping")
        .arg("-sat")
        .arg("-sat-family")
        .arg("lingeling")
        .arg("-S0")
        .arg("-O0")
        .arg("-reduce-domains")
        .arg("-aggregate")
        .output()
        .expect("Failed to find 'savilerow' -- have you installed savilerow and conjure?");

    if !makedimacs.status.success() {
        bail!(
            "savilerow failed. The most likely reason for this is your file is malformed.\n{}\n{}",
            String::from_utf8_lossy(&makedimacs.stdout),
            String::from_utf8_lossy(&makedimacs.stderr)
        );
    }

    let original_input_path = PathBuf::from(&eprime);

    // Need to put '.dimacs' on the end in this slightly horrible way.
    let in_dimacs_path = PathBuf::from(finaleprimeparam.to_str().unwrap().to_owned() + ".dimacs");

    let mut eprimeparse = parse_eprime(&original_input_path, &finaleprimeparam)?;

    eprimeparse.satinstance =
        instances::SatInstance::<BasicVarManager>::from_dimacs_path(&in_dimacs_path)
            .context("reading dimacs")?;

    eprimeparse.cnf = Some(Arc::new(eprimeparse.satinstance.clone().into_cnf().0));

    read_dimacs(&in_dimacs_path, &mut eprimeparse).context("reading variable info from dimacs")?;

    eprimeparse.finalise().context("finalisation of parsing failed. The most likely reason for this is you gave a puzzle which has no solutions!")?;

    Ok(eprimeparse)
}

fn read_essence_param(
    eprimeparam: &PathBuf,
) -> anyhow::Result<BTreeMap<String, serde_json::value::Value>> {
    if eprimeparam.ends_with(".json") {
        info!(target: "parser", "Reading params {:?} as json", eprimeparam);
        let file = fs::File::open(eprimeparam).unwrap();
        let reader = BufReader::new(file);
        serde_json::from_reader(reader).context("Failed reading json param file")
    } else {
        pretty_print_essence(eprimeparam, "json")
    }
}

fn pretty_print_essence(
    file: &PathBuf,
    format: &str,
) -> anyhow::Result<BTreeMap<String, serde_json::value::Value>> {
    let tdir = tempfile::Builder::new()
        .prefix(".demystify-")
        .tempdir_in(".")
        .unwrap();
    let temp_file = tdir.path().join(file.file_name().unwrap());
    fs::copy(file, &temp_file)?;

    info!(target: "parser", "Pretty printing {:?} as {}", temp_file, format);
    let output = ProgramRunner::prepare("conjure", tdir.path())
        .arg("pretty")
        .arg("--output-format")
        .arg(format)
        .arg(temp_file.file_name().unwrap())
        .output()
        .expect("Failed to execute command");

    if !output.status.success() {
        bail!(format!(
            "Conjure pretty-printing failed\n{}\n{}",
            String::from_utf8_lossy(&output.stdout),
            String::from_utf8_lossy(&output.stderr)
        ));
    }

    serde_json::from_slice(&output.stdout).context("Failed to parse JSON produced by conjure")
}

#[cfg(test)]
mod tests {

    use test_log::test;

    use super::pretty_print_essence;

    use std::{collections::BTreeSet, path::PathBuf};

    #[test]
    fn test_parse_essence_binairo() {
        let eprime_path = "./tst/binairo.eprime";
        let eprimeparam_path = "./tst/binairo-1.param";

        let puz =
            crate::problem::util::test_utils::build_puzzleparse(eprime_path, eprimeparam_path);

        assert!(!puz.has_facts());

        assert!(!puz.eprime.has_param("q"));

        assert!(puz.eprime.has_param("n"));

        assert_eq!(puz.eprime.param_i64("n").unwrap(), 6);

        assert!(puz.eprime.has_param("start_grid"));

        assert!(puz.eprime.param_vec_i64("start_grid").is_err());

        let initial: Vec<Vec<i64>> = puz.eprime.param_vec_vec_i64("start_grid").unwrap();

        assert_eq!(initial[0], vec![2, 2, 2, 0, 0, 2]);
        assert_eq!(initial[5], vec![2, 0, 2, 2, 1, 1]);
    }

    #[test]
    fn test_parse_essence_minesweeper() {
        let eprime_path = "./tst/minesweeper.eprime";
        let eprimeparam_path = "./tst/minesweeperPrinted.param";

        let puz =
            crate::problem::util::test_utils::build_puzzleparse(eprime_path, eprimeparam_path);

        assert!(puz.has_facts());

        assert!(!puz.eprime.has_param("q"));

        assert!(puz.eprime.has_param("width"));

        assert_eq!(puz.eprime.param_i64("width").unwrap(), 5);
    }

    #[test]
    fn test_filter_constraint_binairo() {
        let eprime_path = "./tst/binairo.eprime";
        let eprimeparam_path = "./tst/binairo-1.param";

        let puz =
            crate::problem::util::test_utils::build_puzzleparse(eprime_path, eprimeparam_path);

        let mut filter1_puz = puz.clone();

        filter1_puz.filter_out_constraint("rowwhite");

        assert_eq!(puz.conset_lits.len() - filter1_puz.conset_lits.len(), 6);
    }

    #[test]
    #[should_panic]
    fn test_filter_constraint_fail_binairo() {
        let eprime_path = "./tst/binairo.eprime";
        let eprimeparam_path = "./tst/binairo-1.param";

        let puz =
            crate::problem::util::test_utils::build_puzzleparse(eprime_path, eprimeparam_path);

        let mut filter_fail_puz = puz.clone();

        filter_fail_puz.filter_out_constraint("row");
    }

    #[test]
    fn test_parse_essence_little() {
        let eprime_path = "./tst/little1.eprime";
        let eprimeparam_path = "./tst/little1.param";

        let puz =
            crate::problem::util::test_utils::build_puzzleparse(eprime_path, eprimeparam_path);

        assert_eq!(puz.eprime.vars.len(), 1);
        assert_eq!(puz.eprime.cons.len(), 1);
        assert_eq!(puz.eprime.auxvars.len(), 0);
        assert_eq!(puz.eprime.kind, Some("Tiny".to_string()));

        assert!(puz.eprime.has_param("n"));

        assert_eq!(puz.eprime.param_i64("n").unwrap(), 4);

        assert!(puz.eprime.param_bool("n").is_err());

        assert!(!puz.eprime.param_bool("b1").unwrap());
        assert!(puz.eprime.param_bool("b2").unwrap());

        assert_eq!(puz.eprime.param_vec_i64("l").unwrap(), vec![2, 4, 6, 8]);

        assert_eq!(
            puz.eprime.param_vec_string("l").unwrap(),
            vec!["2", "4", "6", "8"]
        );

        assert_eq!(
            puz.eprime.param_vec_vec_string("l2").unwrap(),
            vec![vec!["1", "2"], vec!["3", "4"]]
        );

        assert_eq!(
            puz.eprime.param_vec_string("lb").unwrap(),
            vec!["false", "false", "true", "false"]
        );

        assert_eq!(
            puz.eprime.param_vec_vec_string("lb2").unwrap(),
            vec![vec!["false", "true"], vec!["true", "false"]]
        );

        // These next two may become '3' at some point, when we do better
        // at rejecting useless constraints
        assert_eq!(puz.conset.len(), 4);
        assert_eq!(puz.conset_lits.len(), 4);
        assert_eq!(puz.varset_lits.len(), 4 * 4 * 2); // 4 variables, 4 domain values, 2 pos+neg lits
        let cons = puz.constraints();

        assert!(puz.conset_lits.iter().all(|l| puz.lit_is_con(l)));
        assert!(puz.varset_lits.iter().all(|l| !puz.lit_is_con(l)));
        assert!(puz.conset_lits.iter().all(|l| !puz.lit_is_var(l)));
        assert!(puz.varset_lits.iter().all(|l| puz.lit_is_var(l)));

        let scopes: Vec<_> = cons.iter().map(|c| (c, puz.constraint_scope(c))).collect();

        insta::assert_debug_snapshot!(scopes);
    }

    #[test]
    fn test_parse_sudoku_little() {
        let eprime_path = "./tst/little-sudoku.eprime";
        let eprimeparam_path = "./tst/little-sudoku.param";

        let puz =
            crate::problem::util::test_utils::build_puzzleparse(eprime_path, eprimeparam_path);

        assert_eq!(puz.eprime.vars.len(), 1);
        assert_eq!(puz.eprime.cons.len(), 1);
        assert_eq!(puz.eprime.auxvars.len(), 0);
        assert_eq!(puz.eprime.kind, Some("Sudoku".to_string()));

        assert!(puz.eprime.has_param("n"));

        assert_eq!(puz.eprime.param_i64("n").unwrap(), 3);

        let cons = puz.constraints();

        let scopes: Vec<_> = cons.iter().map(|c| (c, puz.constraint_scope(c))).collect();

        insta::assert_debug_snapshot!(scopes);
    }

    #[test]
    fn test_parse_sudoku_little_2() {
        let eprime_path = "./tst/little-sudoku-2.eprime";
        let eprimeparam_path = "./tst/little-sudoku-2.param";

        let puz =
            crate::problem::util::test_utils::build_puzzleparse(eprime_path, eprimeparam_path);

        assert_eq!(puz.eprime.vars.len(), 1);
        assert_eq!(puz.eprime.cons.len(), 1);
        assert_eq!(puz.eprime.auxvars.len(), 0);
        assert_eq!(puz.eprime.kind, Some("Sudoku".to_string()));

        assert!(puz.eprime.has_param("n"));

        assert_eq!(puz.eprime.param_i64("n").unwrap(), 3);

        let cons = puz.constraints();

        let scopes: Vec<_> = cons.iter().map(|c| (c, puz.constraint_scope(c))).collect();

        insta::assert_debug_snapshot!(scopes);
    }

    #[test]
    fn pretty_print() {
        let eprime_path = "./tst/binairo.eprime";
        let parse = pretty_print_essence(&PathBuf::from(eprime_path), "astjson");
        // Do not want to output the whole tree
        let k: BTreeSet<_> = parse.unwrap().keys().cloned().collect();
        insta::assert_debug_snapshot!(k);
    }

    use std::io::Write;

    #[test]
    fn test_parse_info_directives() {
        // Create a temporary eprime file with INFO directives
        let mut temp_file = tempfile::Builder::new()
            .prefix(".demystify-")
            .tempfile_in(".")
            .unwrap();
        writeln!(temp_file, "$#VAR x").unwrap();
        writeln!(temp_file, "$#VAR y").unwrap();
        writeln!(temp_file, "$#CON con1 \"x != y\"").unwrap();
        writeln!(temp_file, "$#KIND sudoku").unwrap();
        writeln!(temp_file, "$#INFO This is a test info message").unwrap();
        writeln!(temp_file, "$#INFO Another info message with spaces").unwrap();
        writeln!(temp_file, "$#INFO Info with special chars: !@#$%^&*()").unwrap();

        let path = temp_file.path().to_path_buf();

        // Parse the file
        let result = super::parse_eprime_file(&path);

        assert!(result.is_ok(), "Parsing should succeed");
        let parsed = result.unwrap();

        // Verify the info field contains our messages
        assert_eq!(parsed.info.len(), 3, "Should have 3 info messages");
        assert_eq!(parsed.info[0], "This is a test info message");
        assert_eq!(parsed.info[1], "Another info message with spaces");
        assert_eq!(parsed.info[2], "Info with special chars: !@#$%^&*()");

        // Verify other fields are still parsed correctly
        assert_eq!(parsed.vars.len(), 2);
        assert!(parsed.vars.contains("x"));
        assert!(parsed.vars.contains("y"));
        assert_eq!(parsed.cons.len(), 1);
        assert!(parsed.cons.contains_key("con1"));
        assert_eq!(parsed.kind, Some("sudoku".to_string()));
    }

    #[test]
    fn test_parse_empty_info() {
        // Create a temporary eprime file without INFO directives
        let mut temp_file = tempfile::Builder::new()
            .prefix(".demystify-")
            .tempfile_in(".")
            .unwrap();
        writeln!(temp_file, "$#VAR x").unwrap();
        writeln!(temp_file, "$#KIND puzzle").unwrap();

        let path = temp_file.path().to_path_buf();

        // Parse the file
        let result = super::parse_eprime_file(&path);

        assert!(result.is_ok(), "Parsing should succeed");
        let parsed = result.unwrap();

        // Verify the info field is empty
        assert_eq!(parsed.info.len(), 0, "Should have no info messages");
    }
}