SMT solver is a SAT solver + decision procedure
A SAT solver is a solver for a decision problem: the SAT problem is a decision problem. Additionally, this decision problem is "self-reducible":
The SAT problem is self-reducible, that is, each algorithm which correctly answers if an instance of SAT is solvable can be used to find a satisfying assignment
— (wikipedia)
This means that SAT solvers can also give the satisfying assignment, in addition to deciding the problem.
TL;DR SMT solvers solve a generalization of the SAT problem, depending on the types/constraints allowed in the theory. Furthermore, they also allow encoding of higher level type-relationships than the SAT encodings allow.
A SAT solver usually deals with many single boolean variables, that are related only through the clauses/constraints of the CNF. A QF_BV (quantifier-free bitvector) theory SMT solver is basically a SAT solver + more information about the relationships. For example, a QF_BV SMT solver is reducible to SAT1. So why use a QF_BF SMT solver? The the major advantage is that in SAT, an integer is represented by different variables, that at first glance might appear unrelated. A SAT solver would spend much time relearning simple relationships, like $(A = B) \wedge (B = C) \implies (A = C)$ on an integer level, while the SMT solver knows that the individual bits are related this way from the outset, because the QF_BV SMT language is on an integer level (fixed bit-width). Thus a QF_BV SMT solver can reason on the integer level, in addition to the bit level.
- See Beaver SMT solver which can even output the equivalent SAT problem that would need to be solved.
While the QF_BV SMT solver has this advantage over a SAT solver, I don't think this is a complexity advantage: they both essentially equivalent and take exponential time to solve their worst-case problems. But practically, a QF_BV SMT solver might be much quicker due to this extra knowledge. See my answer to Limits of SMT solvers, for an example of something considered "hard" that (current) QF_BV SMT solvers and SAT solvers would both choke on.
There are also SMT solvers that try to solve even tougher problems than Boolean Satisfiability (for example allowing types and constraints on reals, or allowing quantifiers); obviously these are theoretically at least as slow as a SAT solver. These SMT solvers are a solving a generalization of the SAT problem; instead of using binary variables, each "theory" allows relationships/constraints over different domains, such as reals, or quantified (for-all) constraints.
Theorem prover
A automated theorem prover is a solver that given some sort of proof system, some assumptions, and a goal to prove, will "fill in the gaps" between the assumptions and the goal. It will also have some sort of verifier to check proofs (which runs quickly). A theorem prover can rely on a SAT solver to fill in the blanks; in fact, if $P=NP$ and there is a practical algorithm to solve NP-complete problems, one can potentially prove almost all useful provable things (in reasonable time):
But such changes may pale in significance compared to the revolution an efficient method for solving NP-complete problems would cause in mathematics itself. According to Stephen Cook, [19]
...it would transform mathematics by allowing a computer to find a formal proof of any theorem which has a proof of a reasonable length, since formal proofs can easily be recognized in polynomial time. Example problems may well include all of the CMI prize problems.
— (wikipedia)
[19]: Cook, Stephen (April 2000). The P versus NP Problem. Clay Mathematics Institute (PDF).
The reason this would work is because "formal proofs can easily be recognized in polynomial time" via the verifier, and $P=NP$ would imply that that problems that can be verified in polynomial time can be answered in polynomial time as well.
But for now, automated theorem mostly provers use heuristics or exponential time algorithms (but are still helpful).
Constraint solver
These are usually reformulations of the SAT/SMT solvers into other languages. If you've ever use any SAT/SMT solvers to solve a problem, you can really get to love the non-deterministic ability of the solvers. That is, instead of telling the computer how to do something, you tell it what you want, ie. what properties you want the output to have, and a SAT/SMT solver will in a non-deterministic "fill it in", without bothering you with the implementation details. This sort of programming paradigm is very appealing, and is called constraint programming, and to run, it must use a constraint solver (which might use a SAT/SMT solver in the backend, depending on the types and constraints it allows you to use).
But I see people calling Z3 a theorem prover. So I don't know how to dishtinguish those terms.
AFAIK, Z3 is a suite of many tools, including a SMT solver, several theorem proving/model checking languages, and more.
And what is the most general term for all of them?
I think the generalization of the satisfiability problem is Satisfiability Modulo Theories, and so "SMT solver" would be the most general of all of these. However, not all actual SMT solver implementations solve all the theories, so this doesn't mean that all SMT solvers are equally general.
