[mballantyne]

My understanding is that Z3 is primarily an SMT solver (https://en.wikipedia.org/wiki/Satisfiability_modulo_theories), though it has also expanded to support queries beyond SMT.

SMT solvers excel at solving finite sets of equations involving finite or atomic data, like numbers, bitvectors, strings, and arrays of fixed length. They've been very successfully applied in software and hardware verification. They're also the essential tool for a big category of approaches to program synthesis.

This has some overlap with the sorts of numeric constraint solving available in prolog and with non-recursive prolog goals. Prolog however can express turing-complete computation with recursive goals, dynamically allocate data structures of unknown size, etc. that SMT cannot easily encode.

Z3 also has support for datalog-like queries. I don't know much about datalog, but my understanding is that it supports a more limited set of queries than prolog but can solve them more efficiently with a totally different algorithm than prolog's goal-directed depth first search.