z3 - What isthe best way to replay a "session" -

in first phase, collect list of constraints. then, store "session", i.e. constraints associated variables in file can, in second phase, read constraints , assert them, or negate of them before asserting.

what best way (fast , reliable) store such "session" in file, , read ? z3_parse_smtlib2_file() api right way ? have tried z3_open_log() api, don't find api read log file generated z3_open_log(). , z3_log_replay(). api not seem exposed yet.

thanks in advance.

ag

the log file created z3_open_log() can replayed z3.exe (stand alone interpreter, not lib) through command line option /log myfile. of today, haven't seen api in z3 library allows such replay. time being, have understood replay deemed debug analysis.

however, can hack library (just expose z3_replayer class in z3_replayer.h) , use replay log file, quite easy. source code of little feasibility-proof given below, , working fine far know. think nice able because need replay session debugging purpose. able replay file, rather whole program bit heavy.

any feedback welcome. interested know whether functionality integrated in lib, or not.

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 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); // function taken c examples       return 0; }