c++ - 我在使用 z3 :timeout correctly with C++ interface for Linux?

Question

在此示例中，我尝试使用 C++ 接口(interface)让 z3 求解器在 0.1 秒后超时(分解两个素数的 32 位乘积)。它适用于 Windows (VC++ 2013)，但不适用于 Linux (CentOS 6.5)，在 Linux (CentOS 6.5) 上，求解器运行完成大约需要 2.5 秒(调试构建)。 This post表明命令行超时仅在 2012 年的 Windows 上支持 z3 v3.2，但这应该在下一个版本中修复 - 根据 RELEASE_NOTES，我们使用的是 z3 v4.4。我是否正确使用了 C++ 接口(interface)的超时功能，或者这在 Linux 上不受支持？

(注意:此代码示例使用来自 here 的 concat 定义。TEST、EXPECT_EQ 和 EXPECT_TRUE 宏是 gtest 测试宏，应该是不言自明的。)

    TEST(Z3Basic, Factorize32BitWithTimeout) {
    try {
        context c;
        solver s(c);

        expr x = c.bv_const("x", 16);
        expr y = c.bv_const("y", 16);
        expr prod = c.bv_val(0xc4f7d27bll, 32);

        expr pad = c.bv_val(0, 16);

        params p(c);
        p.set(":timeout", 100u);
        s.set(p);
        expr conjecture = prod == concat(pad, x) * concat(pad, y);
        s.add(conjecture);
        check_result r = s.check();
        EXPECT_EQ(unknown, r);
        if (r == sat)
            std::cout << s.get_model() << "\n";
    }
    catch (exception ex) {
        EXPECT_TRUE(false) << "Exception thrown: " << ex << "\n";
    }

}

在 Windows 调试中，这会在大约 210 毫秒内运行整个测试，并通过一个未知的返回码。在 Linux 上，它运行到完成并失败:

[ RUN      ] Z3Basic.Factorize32BitWithTimeout
/home/dave_local/Projects/trunk/CoreApp/z3Interface/UnitTests/TestZ3.cpp:492: Failure
Value of: r
  Actual: sat
Expected: unknown
(define-fun y () (_ BitVec 16)
  #xd279)
(define-fun x () (_ BitVec 16)
  #xef93)
[  FAILED  ] Z3Basic.Factorize32BitWithTimeout (2565 ms)

有什么建议/信息吗？

Answer 1

绝对支持通过 API 超时。也许你的 Linux 机器上的 100ms 太多了？你能试试更小的超时吗？

如果仍然失败，您能否提交一份错误报告以及一个简短的、独立的、可重现的测试用例？谢谢!