Retrieve the correct found objective values via the C-API

I am trying to find the boundary values of the variables in a formula. To do this I feed the formula to Z3 (version 4.8.9 - 64 bit on Ubuntu 22.04) and then use the objective criteria to either minimize or maximize the variables. By looking at the found objectives I get the result I am interested in. To embed this in my code, I need to do the same thing but then via the C-API but I can't seem to find the correct way to do this.

I'll start with an example in SMT2Lib: For instance, I have the following formula x == 3 || (x > y) && (y == 10). In SMT2Lib this would be:

(declare-const x Int)
(declare-const y Int)

(assert (or (= x 3) (and (> x y) (= y 10))))

To prevent having to deal with infinity I add the following assertions to limit the domains to (-1000,1000):

(assert (and (> x (- 1000)) (< x 1000)))
(assert (and (> y (- 1000)) (< y 1000)))

I want to minimize x and y (basically all variables) using the standard lexicographical ordering:

(minimize x)
(minimize y)

Checking satisfiability and retrieving the model yields the following result:

(check-sat)
sat
(get-model)
(model 
  (define-fun y () Int
    2)
  (define-fun x () Int
    3)
)

Please note that the returned model does not contain the minimal value for y for this example, but the objectives do always seem to return the correct values:

(get-objectives)
(objectives
 (x 3)
 (y (- 999))
)

The question now is, how can I actually get the found objectives via the C-API? The C-API has a method to retrieve the objectives (Z3_optimize_get_objectives) but this only seems to return the actual objectives (in this case (- x) and (- y)) and not the found values. What am I doing wrong?

Solution

You shouldn't really use lower/upper etc., but directly evaluate the values in the model you obtained. Here's the standard way of solving this problem, using C++:

#include <iostream>
#include "z3++.h"

using namespace std;

int main()
{
    z3::context ctx;
    z3::expr x = ctx.int_const("x");
    z3::expr y = ctx.int_const("y");

    z3::optimize opt(ctx);

    opt.add((x == 3) || ((x > y) && (x == 10)));
    opt.add((x > -1000) && (x < 1000));
    opt.add((y > -1000) && (y < 1000));

    opt.maximize(x);
    opt.minimize(y);

    z3::check_result res = opt.check();

    if (res == z3::sat) {
        std::cout << x << ": " << opt.get_model().eval(x) << endl;
        std::cout << y << ": " << opt.get_model().eval(y) << endl;
    } else {
       cout << "Result isn't sat: " << res << endl;
       return 1;
    }

    return 0;
}

Assuming the above is in a.cpp, compile it like this:

c++ a.cpp   -o a -lz3

Running it yields:

x: 10
y: (- 999)

which I believe is the solution you're looking for.

Note that you have to be careful if any of your objectives can become oo or -oo: If this is the case, then the values you'll get from opt.get_model().eval cannot be trusted. They're only valid if the assignment produces finite values to the variables in the model.

EDIT: As Patrick Trentin notes in the comments, you also have to be careful if your objective-values are not the same as model-variables. (Objectives are in general functions of model-variables.) In your case, there's a one-to-one correspondence; so you needn't worry so long as you know the optimal values are finite. But you could be led astray if the objective values become unbounded while the model variables remain finite, which wouldn't be trustable. (This can happen, for instance, if your objective value is independent of some of the variables you're querying, for instance.) Thanks to Patrick for point out this intricate detail.