Z3 的检查点机制
Checkpoint mechanism for Z3
我计划使用 Microsoft Research 的 Z3 SMT 求解器做一些工作，它将 运行 在具有执行时间限制的计算服务器上进行。我预计该工作将超过此限制。该计算中心的推荐策略是使用 "checkpoints" 并调用一系列作业，每个作业都从前一个作业中获取检查点并继续工作。这样，没有进程 运行s 超过执行时间限制，因此其他用户也有机会 运行 他们的工作，但使用的计算时间总量可能超过超时单一工作。
Z3 是否支持读取和写入检查点？
"checkpoint"，我的意思是序列化 Z3 求解器内部状态（的一部分）的文件，这样如果 Z3 进程写入检查点并退出，然后第二个 Z3 进程是started 读取检查点文件，读回后新 Z3 进程的状态与先前进程的状态相同（因此求解器不会再次启动，而是从它停止的地方继续求解）。
作为替代方案，不是对整个求解器设置检查点，而是可以读取已学习子句的数据库（或 Z3 内部构建的其他推理数据库）吗？这可以通过使用已学习的子句扩充输入文件来执行某种形式的检查点，尽管它可能不如整个内部状态的 "real" 检查点那么有效。
不，Z3 没有实现所有这些内置目标的工具。Z3 目标和求解器对象可以通过 Z3_goal_to_string and Z3_solver_to_string 函数序列化为 SMT2 格式的字符串；这些可用于检查点，但它们不会保存在上次搜索开始之前不在目标或求解器中的任何已学习子句。
如果主要目标是重新开始复杂的交互，Z3 交互日志可能会有所帮助（参见 Z3_open_log）。这些日志可以重播，但同样不会保存学习的子句等。
我计划使用 Microsoft Research 的 Z3 SMT 求解器做一些工作，它将 运行 在具有执行时间限制的计算服务器上进行。我预计该工作将超过此限制。该计算中心的推荐策略是使用 "checkpoints" 并调用一系列作业，每个作业都从前一个作业中获取检查点并继续工作。这样，没有进程 运行s 超过执行时间限制，因此其他用户也有机会 运行 他们的工作，但使用的计算时间总量可能超过超时单一工作。
Z3 是否支持读取和写入检查点？
"checkpoint"，我的意思是序列化 Z3 求解器内部状态（的一部分）的文件，这样如果 Z3 进程写入检查点并退出，然后第二个 Z3 进程是started 读取检查点文件，读回后新 Z3 进程的状态与先前进程的状态相同（因此求解器不会再次启动，而是从它停止的地方继续求解）。
作为替代方案，不是对整个求解器设置检查点，而是可以读取已学习子句的数据库（或 Z3 内部构建的其他推理数据库）吗？这可以通过使用已学习的子句扩充输入文件来执行某种形式的检查点，尽管它可能不如整个内部状态的 "real" 检查点那么有效。
不，Z3 没有实现所有这些内置目标的工具。Z3 目标和求解器对象可以通过 Z3_goal_to_string and Z3_solver_to_string 函数序列化为 SMT2 格式的字符串；这些可用于检查点，但它们不会保存在上次搜索开始之前不在目标或求解器中的任何已学习子句。
如果主要目标是重新开始复杂的交互，Z3 交互日志可能会有所帮助（参见 Z3_open_log）。这些日志可以重播，但同样不会保存学习的子句等。