在 Z3 C++ API 中使用浮点运算

Question

我正在尝试使用 Z3 解决非线性实数问题。我需要 Z3 来生成多个解决方案。在问题域中，精度不是关键问题；我只需要小数点后一位或两位小数。因此，我需要将 Z3 设置为不探索所有实数搜索 space，以最大限度地减少寻找多个解决方案的时间。

我正在尝试用浮点数替换实数。我阅读了 c_api.c 文件中的 fpa 示例，但我发现它有点令人困惑。

例如，假设我想在以下代码中转换实数：

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";

}

我尝试了下面的代码，但没有用

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";

输出为：

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

我的问题是：

是否有任何关于在 C++ API 中使用 fpa 的详细示例或代码片段？我不清楚如何将 C API 中的 fpa 示例转换为 C++ API.
上面的代码转换有什么问题吗？

Answer 1

我不确定使用浮点数是否是解决您问题的最佳方法。但听起来你尝试了所有其他选项，非线性正在阻碍你。请注意，即使您使用浮点数对问题建模，浮点运算也非常棘手，求解器可能很难找到令人满意的模型。此外，由于数值不稳定，解决方案可能与实际结果相去甚远。

使用 C

抛开所有这些，使用 C api 编写查询代码的正确方法是（假设我们使用 32 位单精度浮点数）：

#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;
}

当运行时，打印：

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

这些是单精度浮点数；例如，您可以在维基百科中阅读有关它们的信息。在更传统的表示法中，它们是：

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

这使用起来很棘手，但是你问的是什么。

使用Python

我衷心推荐使用 Python API 至少在投资于如此复杂的 C 代码之前了解求解器的功能。这是 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()

当运行时，打印：

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

也许不是你所期望的，但它确实是一个有效的模型。

使用Haskell

只是为了让您体验一下简单性，以下是如何使用 Haskell 绑定来表达相同的问题（这只是一行！）

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

总结

请注意，浮点数也有关于 NaN/Infinity 值的问题，因此您可能必须明确避免这些问题。（这就是 Haskell 表达式通过使用 isFPPoint 谓词所做的事情。用 Python 或 C 编写它需要更多代码，但肯定是可行的。）

应该强调的是，从字面上看，与 Z3 的任何其他绑定（Python、Haskell、Scala，你有什么）会给你带来比 C/C++/Java。（即使在 SMTLib 中直接编码也会更好。）

所以，我衷心推荐使用一些更高级别的界面（Python 是一个很好的界面：它很容易学习），一旦您对模型及其工作方式充满信心，您就可以如有必要，开始在 C 中编写相同的代码。

在 Z3 C++ API 中使用浮点运算

using floating point arithmetic with Z3 C++ APIs

c++

floating-point

z3

使用 C

使用Python

使用Haskell

总结