[Synth][FunctionalReduction] Refine equiv class candidates using counterexamples

When the SAT solver returns SAT, the resulting model provides a counterexample that distinguishes two nodes previously thought to be equivalent. This counterexample can be used to refine the entire set of candidates through resimulation: https://github.com/llvm/circt/blob/5e21c9594ca4bd4545fd8b4d8a07a6c6c68eb0c9/lib/Dialect/Synth/Transforms/FunctionalReduction.cpp#L571-L572

This is quite effective to reduce the number of SAT calls.
So certainly the API change would be:

  struct CexPattern {
    DenseMap<Value, bool> inputAssignment;
  };

  FailureOr<CexPattern> extractCounterexample();
  DenseMap<Value, bool> simulateSinglePattern(const CexPattern &pattern);
  void refineCandidateClass(SmallVector<std::pair<Value, bool>> &members,
                            const DenseMap<Value, bool> &bitValues,
                            SmallVector<SmallVector<std::pair<Value, bool>>> &newClasses);

and changing the verification loop from the current:

  for (member in class.drop_front())
    verifyEquivalence(representative, member);

into a worklist:

  SmallVector<SmallVector<Value>> pending = {members};
  while (!pending.empty()) {
    auto cls = pending.pop_back_val();
    if (cls.size() <= 1) continue;

    Value repr = chooseRepresentative(cls);
    SmallVector<Value> proved{repr};
    SmallVector<Value> disproved;

    for (Value member : drop_front(cls)) {
      switch (verifyEquivalence(repr, member)) {
      case Proved:
        proved.push_back(member);
        break;
      case Disproved: {
        auto cex = extractCounterexample();
        auto eval = simulateSinglePattern(*cex);
        SmallVector<SmallVector<Value>> split;
        refineCandidateClass(cls, eval, split);
        pending.append(split.begin(), split.end());
        goto next_class;
      }
      case Unknown:
        // Give up a member. 
      }
    }

    recordProvenClass(proved);
  next_class:;
  }

This is a rough sketch so there might be a better way to implement this.

Start in lib/Dialect/Synth/Transforms/FunctionalReduction.cpp at the counterexample handling around lines 571-572 and inspect the current verification loop. Trace verifyEquivalence and the proposed CexPattern, simulateSinglePattern, and refineCandidateClass APIs before choosing an implementation approach. Done means counterexamples resimulate and split candidate classes, reducing unnecessary SAT calls.