Can I get multiple models for a query like the following?
(set-logic LIA)
(set-option :produce-models true)
(declare-const x Int)
(assert (< x 20))
(check-sat)
(get-model)
Instead of just
sat
(
(define-fun x () Int 0)
)
I'd like to get 0, 1, -1, 2, ...
SMTLib language does not have a mechanism to retrieve "all-models." So, if you're bound to be using SMTLib only, you cannot do this; at least not easily.
However, most solvers (definitely including cvc4 and z3) can be scripted from higher-level languages. The idea is to make a check-sat call, and if you get a solution, you add an additional assertion that disallows that model, and query for a new one. See this answer for how to do this in z3, as scripted from Python: Trying to find all solutions to a boolean formula using Z3 in python. You can do the same from C/Java etc.; or use a higher-level binding that provides such a command out-of-the box.