using floating point arithmetic with Z3 C++ APIs

Question

I am trying to solve a problem of nonlinear real numbers using Z3. I need the Z3 to generate multiple solutions. In the problem domain, precision is not a critical issue; I need just one or two decimal digits after the decimal point. so, I need to set Z3 not to explore all the search space of real numbers to minimize the time to find multiple solutions.

I am trying to replace the real numbers with floating point numbers. I read the fpa example in the c_api.c file but I found it a little bit confusing for me.

for example, let me assume that I want to convert the reals in the following code:

config cfg;
cfg.set("auto_config", true);
context con(cfg);

expr x = con.real_const("x");
expr y = con.real_const("y");

solver sol(con);
sol.add(x*y > 10);
std::cout << sol.check() << "\n";
std::cout << sol.get_model() << "\n";

}

I tried the following code but it didn't work

config cfg;
cfg.set("auto_config", true);
context con(cfg);

expr sign = con.bv_const("sig", 1);
expr exp = con.bv_const("exp", 10);
expr sig = con.bv_const("sig", 10);


expr x = to_expr(con, Z3_mk_fpa_fp(con, sign, exp, sig));
expr y = to_expr(con, Z3_mk_fpa_fp(con, sign, exp, sig));

solver sol(con);
sol.add(x*y > 10);

std::cout << sol.check() << "\n";

and the output is:

Assertion failed: false, file c:\users\rehab\downloads\z3-master\z3-master\src\a
pi\c++\z3++.h, line 1199

My questions are:

1. Are there any detailed examples or code snippets about using fpa in C++ APIs? it is not clear to me how to convert the fpa example in the C API to C++ API.
2. What's wrong in the above code conversion?

Answer 1

I'm not sure if using floats is the best way to go for your problem. But sounds like you tried all other options and non-linearity is getting in your way. Note that even if you model your problem with floats, floating-point arithmetic is quite tricky and solver may have hard time finding satisfying models. Furthermore, solutions maybe way far off from actual results due to numerical instability.

Using C

Leaving all those aside, the correct way to code your query using the C api would be (assuming we use 32-bit single-precision floats):

#include <z3.h>

int main(void) {
    Z3_config  cfg = Z3_mk_config();
    Z3_context ctx = Z3_mk_context(cfg);
    Z3_solver  s   = Z3_mk_solver(ctx);

    Z3_solver_inc_ref(ctx, s);
    Z3_del_config(cfg);

    Z3_sort float_sort = Z3_mk_fpa_sort(ctx, 8, 24);

    Z3_symbol s_x = Z3_mk_string_symbol(ctx, "x");
    Z3_symbol s_y = Z3_mk_string_symbol(ctx, "y");
    Z3_ast      x = Z3_mk_const(ctx, s_x, float_sort);
    Z3_ast      y = Z3_mk_const(ctx, s_y, float_sort);

    Z3_symbol s_x_times_y = Z3_mk_string_symbol(ctx, "x_times_y");
    Z3_ast      x_times_y = Z3_mk_const(ctx, s_x_times_y, float_sort);

    Z3_ast c1 = Z3_mk_eq(ctx, x_times_y, Z3_mk_fpa_mul(ctx, Z3_mk_fpa_rne(ctx), x, y));

    Z3_ast c2 = Z3_mk_fpa_gt(ctx, x_times_y, Z3_mk_fpa_numeral_float(ctx, 10, float_sort));

    Z3_solver_assert(ctx, s, c1);
    Z3_solver_assert(ctx, s, c2);

    Z3_lbool result = Z3_solver_check(ctx, s);

    switch(result) {
        case Z3_L_FALSE: printf("unsat\n");
                         break;
        case Z3_L_UNDEF: printf("undef\n");
                         break;
        case Z3_L_TRUE:  { Z3_model m = Z3_solver_get_model(ctx, s);
                           if(m) Z3_model_inc_ref(ctx, m);
                           printf("sat\n%s\n", Z3_model_to_string(ctx, m));
                           break;
                         }
    }

    return 0;
}

When run, this prints:

sat
x_times_y -> (fp #b0 #xbe #b10110110110101010000010)
y -> (fp #b0 #xb5 #b00000000000000000000000)
x -> (fp #b0 #x88 #b10110110110101010000010)

These are single-precision floating point numbers; you can read about them in wikipedia for instance. In more conventional notation, they are:

x_times_y -> 1.5810592e19
y         -> 1.8014399e16
x         -> 877.6642

This is quite tricky to use, but what you have asked.

Using Python

I'd heartily recommend using the Python API to at least see what the solver is capable of before investing into such complicated C code. Here's how it would look in Python:

from z3 import *

x = FP('x', FPSort(8, 24))
y = FP('y', FPSort(8, 24))

s = Solver()
s.add(x*y > 10);
s.check()
print s.model()

When run, this prints:

[y = 1.32167303562164306640625,
 x = 1.513233661651611328125*(2**121)]

Perhaps not what you expected, but it is a valid model indeed.

Using Haskell

Just to give you a taste of simplicity, here's how the same problem can be expressed using the Haskell bindings (It's just a mere one liner!)

Prelude Data.SBV> sat $ \x y -> fpIsPoint x &&& fpIsPoint y &&& x * y .> (10::SFloat)
Satisfiable. Model:
  s0 = 5.1129496e28 :: Float
  s1 =  6.6554557e9 :: Float

Summary

Note that Floating-point also has issues regarding NaN/Infinity values, so you might have to avoid those explicitly. (This is what the Haskell expression did by using the isFPPoint predicate. Coding it in Python or C would require more code, but is surely doable.)

It should be emphasized that literally any other binding to Z3 (Python, Haskell, Scala, what have you) will give you a better experience than what you'll get with C/C++/Java. (Even direct coding in SMTLib would be nicer.)

So, I heartily recommend using some higher-level interface (Python is a good one: It is easy to learn), and once you are confident with the model and how it works, you can then start coding the same in C if necessary.