1

在第一阶段，我收集了一个约束列表。然后，我想存储这个“会话”，即所有约束，但所有相关变量也存储在一个文件中，以便我可以在第二阶段读回约束并断言它们，甚至否定其中一些在断言之前。

将这样的“会话”存储在文件中并将其读回的最佳方式（快速且可靠）是什么？Z3_parse_smtlib2_file() API 会是正确的方法吗？我已经尝试过 Z3_open_log() API，但我没有找到读取 Z3_open_log() 生成的日志文件的 API。那么 z3_log_replay() 呢？这个 API 似乎还没有公开。

提前致谢。

股份公司

4

1 回答 1

1

Z3_open_log() 创建的日志文件可以通过命令行选项 /log myfile 使用 Z3.exe（独立解释器，而不是 lib）重播。到今天为止，我还没有在 Z3 库中看到任何允许这种重放的 API。暂时我已经明白replay被认为是debug分析了。

但是，您可以破解该库（只需在 z3_replayer.h 中公开 z3_replayer 类）并使用它来重放任何日志文件，这很容易。下面给出了我的小可行性证明的源代码，据我所知，它工作正常。我认为能够做到这一点非常好，因为有时我需要重播会话以进行调试。能够从文件中重播它是件好事，而不是从我的整个程序中重播，这有点重。

任何反馈都将非常受欢迎。我也很想知道这个功能是否可以集成到库中。

AG。

#include <fstream>
#include <iostream>
#include "api/z3_replayer.h"


int main(int argc, char * argv[])
{
   const char * filename = argv[1];
   std::ifstream in(filename);
   if (in.bad() || in.fail()) {
       std::cerr << "Error: failed to open file: " << filename << "\n";
       exit(EXIT_FAILURE);
}
    z3_replayer r(in);
    r.parse();

    Z3_context ctx = reinterpret_cast<Z3_context>(r.get_obj(0));

    check(ctx,Z3_L_TRUE); // this function is taken from the c examples 

    return 0;
}
于 2013-05-06T18:57:51.797 回答