c++ - using floating point arithmetic with Z3 C++ APIs
问题描述
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:
- 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.
- What's wrong in the above code conversion?
解决方案
我不确定使用浮点数是否是解决问题的最佳方法。但听起来你尝试了所有其他选项,而非线性正在阻碍你。请注意,即使您使用浮点数对问题进行建模,浮点运算也非常棘手,求解器可能很难找到令人满意的模型。此外,由于数值不稳定性,解决方案可能与实际结果相去甚远。
使用 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
在投资如此复杂的 C 代码之前,我衷心推荐使用 Python API 至少了解求解器的能力。这是它在 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 对其进行编码需要更多代码,但肯定是可行的。)
应该强调的是,与使用 C/C++/Java 相比,任何其他与 Z3 的绑定(Python、Haskell、Scala 等)都会为您提供更好的体验。(即使在 SMTLib 中直接编码也会更好。)
所以,我衷心推荐使用一些更高级别的接口(Python 是一个很好的接口:它很容易学习),一旦你对模型及其工作方式有信心,你就可以在必要时开始用 C 编写相同的代码。
推荐阅读
- python - 用pickle-python序列化一个h2o模型
- javascript - Node-Red - 访问受密码保护的 SQLite 数据库
- java - Spliterator SORTED 特征行为
- rest - 如何通过 API 将组分配为 VSTS 中端点上的用户?
- java - Schedulers.elastic() 不使用早期生成的线程
- c# - 如何修复:避免非只读静态字段
- python - 谈存储在 MySQL 数据库中时 Django 中的时区
- php - PHP表单没有错误没有插入
- ios - URL Schemes:打开设备勿扰设置?
- java - XPATH:将 xml 节点插入另一个 XML 文档