如何访问钻头爆破时使用的变量映射？

Question

我正在修改一个使用Z3(特别是Python API)来解决bitvector约束的工具.我需要使用一个特定的外部SAT求解器而不是内部的Z3求解器,所以我首先使用这个策略进行爆破

Then('simplify', 'bit-blast', 'tseitin-cnf')

之后我可以相对容易地将子句转储到DIMACS文件中.问题是将得到的命题模型映射回原始约束的模型:据我所知,Python API没有提供访问对应于策略的模型转换器的方法.这是真的？如果是这样,是否可以使用不同的API完成,或者是否有更简单的方法？基本上我只需要知道最终CNF子句中的命题变量如何与原始的bitvector变量相对应.

Answer 1

这听起来很特殊。最简单的可能是您检测 goal2sat 转换（并重新编译 Z3）以将转换表保存在文件中。我认为通过 API 公开的任何功能都不会为您提供此信息。