introduce z3-prover to solve constraint (#10921)

Co-authored-by: Andy Lok <[email protected]>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Co-authored-by: BohuTANG <[email protected]>
Co-authored-by: everpcpc <[email protected]>

Author: 5 people

.gitignore

@@ -65,3 +65,6 @@ benchmark/clickbench/results
 
 # direnv test files
 .envrc
+
+# z3
+**/.z3-trace