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

[uenoku]

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:

circt/lib/Dialect/Synth/Transforms/FunctionalReduction.cpp

Lines 571 to 572 in 5e21c95

	// TODO: Refine equivalence classes based on counterexamples from SAT
	// solver

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.

[ankit-cybertron]

Hi @uenoku, I’d love to work on this!
had few quires, after a SAT result, is the model guaranteed to remain valid via satSolver->val(...) until the next solve() call? also
during splitting, can we buffer proved members separately and only push the remaining ones back into the worklist?

[uenoku]

Thanks!

Yes, that's guaranteed (We use IPASIR interface).
Z3's one is maybe buggy (because it's wrapper of SMT I wrote) but cadical should be more reliable.

I don't expect to mutate IR during this worklist iterations so you can buffer/cache proved pairs whatever you want.

[uenoku]

Note that for testing we want to intentionally cause conflicts of signature. Easiest thing is to allow zero bit signature size so that every value is in the same candidates.

[ankit-cybertron]

Thanks for the clarification. I will launch a PR