Z3 actually has a logic programming language inside it if you know how to look. This makes it one the easiest to pull off the shelf because Z3 has so much work put into it and excellent bindings. It also is perhaps one of the most declarative logic programming languages available with very cool strong theory support.
