Revert "chore(planner): remove z3"

[zhang2014]

Reverts #15663

---

This change is 

[github-actions]

This pull request's title is not fulfill the requirements. @zhang2014 please update it 🙏.

Valid format:

fix(query): fix group by string bug
  ^         ^---------------------^
  |         |
  |         +-> Summary in present tense.
  |
  +-------> Type: rfc, feat, fix, refactor, ci, docs, chore

Valid types:

• rfc: this PR proposes a new RFC
• feat: this PR introduces a new feature to the codebase
• fix: this PR patches a bug in codebase
• refactor: this PR changes the code base without new features or bugfix
• ci: this PR changes build/testing/ci steps
• docs: this PR changes the documents or websites
• chore: this PR only has small changes that no need to record

[github-actions]

At least one test kind must be checked in the PR description.
@zhang2014 please update it 🙏.

[github-actions]

Pull request description must contain CLA like the following:

I hereby agree to the terms of the CLA available at: https://docs.databend.com/dev/policies/cla/

## Summary

Summary about this PR

- Close #issue

[github-actions]

At least one type of change must be checked in the PR description.
@zhang2014 please update it 🙏.