///|
pub(all) struct UnsatCoreReport {
  valid : Bool
  unsat : Bool
  assumptions : Array[Lit]
  core : Array[Lit]
  minimal : Bool
  solver_calls : Int
  message : String
} derive(Debug)

///|
fn unique_assumptions(assumptions : Array[Lit]) -> Array[Lit] {
  let result : Array[Lit] = []
  for assumption in assumptions {
    if !result.contains(assumption) {
      result.push(assumption)
    }
  }
  result
}

///|
fn assumptions_valid(cnf : Cnf, assumptions : Array[Lit]) -> Bool {
  for assumption in assumptions {
    if assumption.var_id < 1 || assumption.var_id > cnf.var_count {
      return false
    }
  }
  true
}

///|
fn cnf_with_assumptions(cnf : Cnf, assumptions : Array[Lit]) -> Cnf {
  let clauses = cnf.clauses.copy()
  for assumption in assumptions {
    clauses.push(Clause::unit(assumption))
  }
  Cnf::new(cnf.var_count, clauses)
}

///|
/// Solves a CNF under temporary literal assumptions.
///
/// The original CNF is not modified. Invalid variable identifiers produce an
/// undecided, unsatisfied result with an explanatory trace.
pub fn solve_with_assumptions(
  cnf : Cnf,
  assumptions : Array[Lit],
) -> SolveResult {
  let normalized = unique_assumptions(assumptions)
  if !assumptions_valid(cnf, normalized) {
    return {
      sat: false,
      decided: false,
      assignment: [],
      trace: ["invalid assumption variable"],
    }
  }
  solve(cnf_with_assumptions(cnf, normalized))
}

///|
fn without_assumption(assumptions : Array[Lit], removed : Int) -> Array[Lit] {
  let result : Array[Lit] = []
  for index = 0; index < assumptions.length(); index = index + 1 {
    if index != removed {
      result.push(assumptions[index])
    }
  }
  result
}

///|
/// Computes a deterministic deletion-minimal UNSAT core over assumptions.
///
/// "Minimal" means every returned literal is necessary: removing any one makes
/// the formula satisfiable. It does not claim minimum cardinality.
pub fn minimal_unsat_core(
  cnf : Cnf,
  assumptions : Array[Lit],
) -> UnsatCoreReport {
  let normalized = unique_assumptions(assumptions)
  if !assumptions_valid(cnf, normalized) {
    return {
      valid: false,
      unsat: false,
      assumptions: normalized,
      core: [],
      minimal: false,
      solver_calls: 0,
      message: "assumption variable is outside the CNF",
    }
  }
  let mut solver_calls = 1
  let initial = solve_with_assumptions(cnf, normalized)
  if initial.sat {
    return {
      valid: true,
      unsat: false,
      assumptions: normalized,
      core: [],
      minimal: false,
      solver_calls,
      message: "formula is satisfiable under assumptions",
    }
  }
  let mut core = normalized.copy()
  let mut index = 0
  while index < core.length() {
    let candidate = without_assumption(core, index)
    solver_calls = solver_calls + 1
    if !solve_with_assumptions(cnf, candidate).sat {
      core = candidate
    } else {
      index = index + 1
    }
  }
  {
    valid: true,
    unsat: true,
    assumptions: normalized,
    core,
    minimal: true,
    solver_calls,
    message: if core.length() == 0 {
      "base CNF is unsatisfiable without assumptions"
    } else {
      "deletion-minimal assumption core"
    },
  }
}

///|
pub fn UnsatCoreReport::to_json(self : UnsatCoreReport) -> String {
  let output = StringBuilder()
  output.write_string(
    "{\"valid\":\{self.valid},\"unsat\":\{self.unsat},\"minimal\":\{self.minimal},\"solver_calls\":\{self.solver_calls},\"core\":[",
  )
  for index = 0; index < self.core.length(); index = index + 1 {
    if index > 0 {
      output.write_char(',')
    }
    output.write_string("\{self.core[index].to_dimacs()}")
  }
  output.write_string("],\"message\":\"\{self.message}\"}")
  output.to_string()
}