1

最初のフェーズでは、制約のリストを収集します。次に、この「セッション」、つまりすべての制約と関連するすべての変数をファイルに保存して、第 2 段階で制約を読み戻してアサートしたり、それらの一部を否定したりできるようにします。主張する前に。

そのような「セッション」をファイルに保存し、それを読み戻すための最良の方法（高速で信頼性の高い方法）は何ですか? Z3_parse_smtlib2_file() API は正しい方法でしょうか? Z3_open_log() API を試しましたが、Z3_open_log() によって生成されたログ ファイルを読み取る API が見つかりません。z3_log_replay() はどうでしょう。この API はまだ公開されていないようです。

前もって感謝します。

AG

4

1 に答える 1

1

Z3_open_log() によって作成されたログ ファイルは、コマンド ライン オプション /log myfile を介して、Z3.exe (lib ではなくスタンドアロン インタープリター) で再生できます。今日の時点で、そのようなリプレイを可能にする API を Z3 ライブラリで見たことがありません。とりあえず、リプレイはデバッグ解析とみなされることは承知しております。

ただし、ライブラリをハックして (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 に答える