Fwiw some of the later logic-programming work coming out of Prolog has produced languages with Prolog-like syntax but without statement order being significant, and guaranteed termination. This paradigm, Answer Set Programming (ASP), is also based on solvers, so has some relationship to SMT, but feels more like Prolog to program, e.g. it has negation-as-failure. My favorite implementation is from the University of Potsdam [1].
Imo it's a much nicer modeling language, especially for incremental formalization, in part because of implementing a nonmonotonic rather than classical logic. It also has a nice generative-programming style where you can define generative spaces via "choice rules", where the solver is explicitly given a free choice for some variables, subject to constraints, and returns a satisfying artifact/model. That allows using it to construct constrained generative systems (e.g. generative music [2], level generation [3]). But Z3 far outperforms ASP solvers on problems where variables range over large domains (like "32-bit integer") because of the MT part of SMT. There's some experimental work on trying to combine the approaches, using Z3 (or another SMT solver) as the solver backend for a logic-programming system [4], but I don't know how usable it is.
I'm not sure I'd set up an opposition between SAT solvers like Z3 on
one hand, and ASP on the other. I recommend to think of ASP (and other
approaches like CSP (constraint satisfaction problems)) as high-level
languages for solving combinatorial problems.
In this understanding,
high-level (ASP, CSP) contrasts with low-level (SAT and SMT) for
the same problem domain: just as with high- and low-level
programming languages like Java are compiled down to low-level programming languages like x86 machine code, high-level formalism like ASP, CSP, ... can be compiled down to low-level SAT/SMT.
SAT/SMT is the assembly
language of combinatorial problems because you have to state
explicitly all forbidden solutions using CNF (conjuncive normal
form). For examle if you have variables x, y and z, then the CNF
( x \/ y \/ not z ) /\ ( not x /\ not y )
has as models all maps from {x, y, z} to {0, 1} except {x=0, y=0,
z=1}, {x=1, y=1, z=1} and {x=1, y=1, z=0}. The problem with using CNFs to enumerate forbidden solutions is that the formulae can be long (just like assembler programs can be long). With high-level formalisms like ASP you often get a much more succinct specification.
With a
bit of squinting, you can even see first-order logic as a high-level
formalism that compiles down to propositional logic (via skolemisation,
resolution, unification, herbrand etc).
In some theoretical sense I agree with that view, but I don't think we're currently at that stage from a practical perspective. Today, the established ASP solvers have performance and expressivity tradeoffs relative to the established SMT solvers. There are some early experiments (like the one I linked) that aim to do things like use SMT solvers as an ASP backend, but they are very much research stage. And they are also (so far) a bit "messy", requiring source-level changes in order to take advantage of Z3, rather than being able to transparently "compile" general ASP programs to take advantage of efficient solvers.
Imo it's a much nicer modeling language, especially for incremental formalization, in part because of implementing a nonmonotonic rather than classical logic. It also has a nice generative-programming style where you can define generative spaces via "choice rules", where the solver is explicitly given a free choice for some variables, subject to constraints, and returns a satisfying artifact/model. That allows using it to construct constrained generative systems (e.g. generative music [2], level generation [3]). But Z3 far outperforms ASP solvers on problems where variables range over large domains (like "32-bit integer") because of the MT part of SMT. There's some experimental work on trying to combine the approaches, using Z3 (or another SMT solver) as the solver backend for a logic-programming system [4], but I don't know how usable it is.
[1] http://potassco.sourceforge.net/
[2] http://arxiv.org/abs/1006.4948
[3] http://pcgbook.com/wp-content/uploads/chapter08.pdf
[4] http://peace.eas.asu.edu/joolee/papers/aspmt-system-jelia.pd...