Ubuntu Question posted in
The official Ubuntu documentation can be found here.

Ubuntu – 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?

Tags:

2

Answers


  1. 0

    The following C++ example might help:

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

//  https://github.com/Z3Prover/z3/blob/master/examples/c%2B%2B/example.cpp

#define LOG_Z3_CALLS

#ifdef LOG_Z3_CALLS
#define LOG_MSG(msg) Z3_append_log(msg)
#else
#define LOG_MSG(msg) ((void)0)
#endif

using namespace z3;


int main()
{
    std::cout << "Z3 C++ API examplen";

    context ctx;
    expr x = ctx.int_const("x");
    expr y = ctx.int_const("y");

    optimize opt(ctx);
    params p(ctx);
    p.set("priority", ctx.str_symbol("pareto"));
    opt.set(p);

    //  (assert(or (= x 3) (and (> x y) (= x 10))))
    opt.add((x == 3) || ((x > y) && (x == 10)));

    //  (assert(and (> x(-1000)) (< x 1000)))
    opt.add((x > -1000) && (x < 1000));
    //  (assert(and (> y(-1000)) (< y 1000)))
    opt.add((y > -1000) && (y < 1000));

    optimize::handle h1 = opt.minimize(x);
    optimize::handle h2 = opt.minimize(y);
    int64_t prevl1 = 0;
    int64_t prevl2 = 0;
    int64_t prevu1 = 0;
    int64_t prevu2 = 0;
    int64_t prevv1 = 0;
    int64_t prevv2 = 0;
    int unchanged = 0;
    while (true) {
        if (sat == opt.check()) {
            int64_t il1 = opt.lower(h1).as_int64();
            int64_t il2 = opt.lower(h2).as_int64();
            int64_t iu1 = opt.upper(h1).as_int64();
            int64_t iu2 = opt.upper(h2).as_int64();
            
            model m = opt.get_model();
            int64_t iv1 = m.eval(x).as_int64();
            int64_t iv2 = m.eval(y).as_int64();

            if ((il1 == prevl1) && (il2 == prevl2) &&
                (iu1 == prevu1) && (iu2 == prevu2) &&
                (iv1 == prevv1) && (iv2 == prevv2)) { 
                unchanged++;
            } else {
                prevl1 = il1;
                prevl2 = il2;
                prevu1 = iu1;
                prevu2 = iu2;
                prevv1 = iv1;
                prevv2 = iv2;
                unchanged = 0;
            }
            std::cout << x << ": " << iv1 << " [" << il1 << "; " << iu1 << "] " 
                      << y << ": " << iv2 << " [" << il2 << "; " << iu2 << "] n";

            if (unchanged > 10) {
                std::cout << "No more change?n";
                break;
            }
        }
        else {
            break;
        }
    }

    return 0;
}
    Login or Signup to reply.
  2. 0

    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 << x << ": " << 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
x: (- 999)

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

    Login or Signup to reply.
Please signup or login to give your own answer.

Back To Top
Search