z3 - 与 z3 版本 4.8.4 相比，Z3_get_numeral_double API 在 z3 版本 4.8.10 中给出不同的结果

Question

一段时间以来，我们一直在使用 c++ binding z3 version 4.8.4 来满足约束条件。我们的约束也可以有浮点数/双精度来表示命题约束。样本约束将是：

CarModel=M1 表示 chasisLength=999999999999999999999999999999999999999999999999999999.0（假设 chasisLength 的测量单位非常小）

基于我们对 z3 公共 API 的理解，我们确定了一种在 z3 中使用 double 值初始化 real sort 变量并从 real sort z3::expr 中检索 double 值的方法。但是，我们的方式在 z3 版本中似乎并不一致。下面的 c++ 代码片段试图通过针对不同的 z3 版本（4.8.10 与 4.8.4）运行相同的代码片段来演示该问题。这是 Z3_get_numeral_double API 的已知问题吗？

还有一些更好的方法可以用双值初始化真正的排序 expr 并从真正的排序 z3 表达式中检索双精度值吗？

z3::context c;
z3::solver z3Solver(c);

z3::expr floatFam = c.real_const("Length");
std::string floatValue("999999999999999999999999999999999999999999999999999999"); // 9 repeated 54 times
char* endBuf = NULL;
const double doubleValue = strtod(floatValue.c_str(), &endBuf); // strtod return 1.0 * 10e+54
char buffer[100] = "";
sprintf_s(buffer, 100, "%.16g", doubleValue);
z3::expr floatValueExpr = c.real_val(buffer);
z3::expr lengthBoolFlag = c.bool_const("lengthConst");

z3Solver.add(lengthBoolFlag == (floatFam == floatValueExpr)); // assert that there is equivalencne relation between lengthConst=true and length=1.0 * 10e+54

z3::expr modelFam = c.int_const("ModelConst");
z3::expr value1 = c.int_val(1);
z3::expr value2 = c.int_val(2);
z3::expr value3 = c.int_val(3);

z3Solver.add((modelFam == value1) || (modelFam == value2) || (modelFam == value3)); // add assert to solver stating ModelConst can have three possible values 1, 2, 3
z3Solver.add(z3::implies((modelFam == value1), lengthBoolFlag)); // add assert stating if ModelConst=1 then lengthConst has be true
z3Solver.add(modelFam == value1); // assert ModelConst=1

z3::check_result satVerdict = z3Solver.check();

if (z3::sat == satVerdict)
{
    const z3::model z3Model = z3Solver.get_model();
    z3::expr realExpr = z3Model.eval(floatFam); // get the solution for length from the z3 model
    double z3DblValue = 0;
    if (realExpr.is_numeral(z3DblValue))
    {
        z3::expr numeratorExpr = realExpr.numerator(); // get the numerator expr from realExpr
        z3::expr denominatorExpr = realExpr.denominator(); // get the denominator expr from realExpr
        **double numerator = Z3_get_numeral_double(c, numeratorExpr); // When run with z3 version 4.8.10 this returns 9.999 * 10e+53 which is different what was set in the assert, however when run with z3 version 4.8.4 it returns 1.0 * 10e+54 which exactly what was set in the assert**
        double denominator = Z3_get_numeral_double(c, denominatorExpr); // this returns 1.0
        z3DblValue = numerator / denominator; // 9.999 * 10e+53 is retrieved as solution which violates implies and equivalence assert above
    }
}

标签： z3