///|
fn valid_pos_for_spec(spec : TruthSpec, solution : PosSolution) -> Bool {
  if solution.input_count != spec.input_count {
    return false
  }
  for clause in solution.selected {
    let cube = clause.zero_cube
    if cube.width != spec.input_count ||
      cube.value < 0 ||
      cube.wildcard < 0 ||
      (cube.value & cube.wildcard) != 0 ||
      (cube.value | cube.wildcard) >= 1 << spec.input_count {
      return false
    }
  }
  true
}

///|
/// Compare a POS result with the cared truth-table rows using canonical BDDs.
/// Build literal OR clauses and their AND directly, without complement SOP
/// selection or row evaluation. A result with a different width returns false.
pub fn verify_pos_with_bdd(spec : TruthSpec, solution : PosSolution) -> Bool {
  if !valid_pos_for_spec(spec, solution) {
    return false
  }
  let manager = BddManager::new(spec.input_count).unwrap()
  let mut expected = 0
  let mut care = 0
  for row in 0..<(1 << spec.input_count) {
    if !contains(spec.dont_cares, row) {
      let term = bdd_row_term(manager, row, spec.input_count)
      care = manager.apply(Or, care, term).unwrap()
      if contains(spec.on_set, row) {
        expected = manager.apply(Or, expected, term).unwrap()
      }
    }
  }
  let mut actual = 1
  for clause in solution.selected {
    let pattern = clause.pattern().to_array()
    let mut sum = 0
    for position in 0.. SatEquivalence {
  if !valid_pos_for_spec(spec, solution) {
    return InvalidInput
  }
  let mut actual = @sat.BoolExpr::Constant(true)
  for clause in solution.selected {
    let pattern = clause.pattern().to_array()
    let mut sum = @sat.BoolExpr::Constant(false)
    for position in 0.. formula
    None => return InvalidInput
  }
  let report = formula.solve(config)
  match report.outcome {
    @sat.SatOutcome::Satisfiable(model) => {
      let inputs : Array[Bool] = []
      for index in 0.. Equivalent
    @sat.SatOutcome::Unknown => Unknown(report.stats)
  }
}