使用Z3 C ++ API的浮点算法 [英] using floating point arithmetic with Z3 C++ APIs
问题描述
我正在尝试使用Z3解决非线性实数的问题.我需要Z3生成多个解决方案. 在问题领域，精确度不是关键问题.我只需要小数点后的一两个小数位即可.因此，我需要将Z3设置为不探索实数的所有搜索空间，以最大程度地减少找到多个解的时间.
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.
我正在尝试将实数替换为浮点数.我在c_api.c文件中阅读了fpa示例，但发现它让我有些困惑.
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";
，输出为:
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.
- 上面的代码转换有什么问题?
推荐答案
我不确定使用浮点数是否是解决问题的最佳方法.但是听起来您尝试了所有其他选项，但非线性正逐渐成为您的障碍.请注意，即使使用浮点数对问题进行建模，浮点算法也非常棘手，求解器可能很难找到令人满意的模型.此外，由于数值不稳定，解决方案可能与实际结果相去甚远.
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.
撇开所有这些，使用C api编写查询代码的正确方法是(假设我们使用32位单精度浮点数):
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;
}
运行时，将打印:
sat
x_times_y -> (fp #b0 #xbe #b10110110110101010000010)
y -> (fp #b0 #xb5 #b00000000000000000000000)
x -> (fp #b0 #x88 #b10110110110101010000010)
这些是单精度浮点数；例如，您可以在Wikipedia中阅读有关它们的信息.在更常规的表示法中，它们是:
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.
在向此类复杂的C代码投资之前，我衷心建议使用Python API，至少要了解求解器的功能.这是在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()
运行时，将打印:
[y = 1.32167303562164306640625,
x = 1.513233661651611328125*(2**121)]
也许不是您期望的那样，但这确实是一个有效的模型.
Perhaps not what you expected, but it is a valid model indeed.
仅是为了给您带来简单的感觉，这是使用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
摘要
请注意，浮点还存在与NaN/Infinity值有关的问题，因此您可能必须明确避免使用这些值. (这是Haskell表达式通过使用isFPPoint谓词所做的操作.用Python或C对其进行编码将需要更多代码，但肯定是可行的.)
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.)
应该强调的是，实际上，与Z3的任何其他绑定(Python，Haskell，Scala，还有您所拥有的东西)都将为您提供比C/C ++/Java更好的体验. (即使在SMTLib中直接编码也会更好.)
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.)
因此，我衷心建议使用一些更高级别的接口(Python是一个很好的接口:它很容易学习)，一旦您对模型及其工作方式充满信心，就可以开始在C语言中对其进行编码如有必要.
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.
这篇关于使用Z3 C ++ API的浮点算法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
