CODEWITHSUNDEEP
z3
Daniel Binkele-Raible
Daniel Binkele-Raible

Reputation: 11

Missing model when solving Exists-Expression

I was setting up an example using the Java-API (along the lines of the provided Z3 Java examples):

Context ctx = new Context();

        int size = 1;
        IntExpr[] xs = new IntExpr[size];
        Symbol[] names = new Symbol[size];

        for (int j = 0; j < size; j++) {
            names[j] = ctx.mkSymbol("x_" + Integer.toString(j));
            xs[j] = (IntExpr) ctx.mkConst(names[j], ctx.getIntSort());
        }

        BoolExpr body_const = ctx.mkEq(xs[0], ctx.mkInt(3));
        BoolExpr exists = ctx.mkExists(xs, body_const, 1, null, null,
                null, null);

        Solver s = ctx.mkSolver();
        s.add(exists);
        if (s.check() != Status.SATISFIABLE)
            throw new IllegalStateException();
        Model model = s.getModel();

        System.out.println("---> " + model);

I wonder why the model is empty! Shouldn't it simply state that xs[0] is 3?

Upvotes: 0

Views: 121

Answers (1)

alias
alias

Reputation: 30428

The entire Java program is just clutter in this context. Essentially, you're asking the solver the following SMTLib question:

(assert (exists ((x_0 Int)) (= x_0 3)))
(check-sat)
(get-model)

When run, the above prints:

sat
(
)

That is, it is indeed satisfiable, but there's no model to display. Because SMT solvers do not display values of existentially quantified variables like this. The model only contains values that are declared at the top-level. So, instead, you need to ask something like:

(declare-const x_0 Int)
(assert (= x_0 3))
(check-sat)
(get-model)

to which you'll get the model:

sat
(
  (define-fun x_0 () Int
    3)
)

Hope that helps out. So, if the Java program you gave is indeed what you intended, then the output is correct; by design you do not get the values of "existentially" quantified variables from an SMT solver. If you want to get them, make them top-level variables instead.

Upvotes: 1

Related Questions