Search code examples
smtformal-methodssatisfiabilitycvc4

Produce multiple models for CVC4 SMT queries

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, ...

Solution

  • 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.