z3 - z3 可以读取 MathSAT 的输出文件作为其输入文件吗？

Question

我需要使用 z3 和 mathsat 进行一些实验。我已经完成了 mathsat 的实验。为 mathsat 编写输入文件需要很多时间，我不想再次为 z3 编写输入文件。Mathsat 支持从“msat”文件生成“smt”文件。转换命令如下图：

/home/xdb/mathsat/mathsat-4.2.17-linux-x86_64/bin/mathsat -input=msat -output=smt -logic=QF_LRA /home/xdb/satcase/sample/sample.msat>>/home/xdb/satcase/sample/sample.smt   

我的问题是z3可以识别这个'smt'文件吗？

Answer 1

Z3 可以读取 SMT 1.0 和 2.0 文件。格式在http://www.smtlib.org中定义。如果 MathSAT 生成的公式符合标准，那么您应该没有问题。您是否尝试过使用 Z3 读取生成的文件？如果它不起作用，Z3 产生的错误信息是什么？