[Rewriter] Always rewrite again when kind changes (#8007)

[Rewriter] Always rewrite again when kind changes (#8007)

Fixes cvc5/cvc5-projects#438. The rewriter
returned REWRITE_DONE prematurely when rewriting operators such as
bvand in certain cases. If only a single term was left after removing
duplicates from a bvand, the kind of the current node would change and
another pre-rewrite could apply, but the rewriter still returned
REWRITE_DONE. After adding an assertion in the rewriter that checks
that REWRITE_DONE implies that no other pre-rewrite applies, it was
discovered that not only the bit-vector rewriter has this issue, but
other rewriters, e.g., the Boolean rewriter, as well. This commit
changes our semantics for REWRITE_DONE to mean that no other rewrite
applies provided that the kind did not change. This makes it easier for
developers to decide when to return REWRITE_DONE, because it only
requires reasoning about rewrites that apply to a single kind.