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

【问题标题】：Can z3 read the outputfile of MathSAT as its inputfile?z3 可以读取 MathSAT 的输出文件作为其输入文件吗？
【发布时间】：2013-01-04 12:22:04
【问题描述】：

我需要使用 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'文件吗？

【问题讨论】：

标签： z3 smt mathsat

【解决方案1】：

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

【讨论】：

我试过了，4.2版不行。但是，它可以在最新版本 4.3 上运行。我只是想知道结果是否正确。虽然 z3 v4.3 可以工作并打印结果，但这是否意味着它可以识别这个“smt”文件。为什么 z3 v4.2 不能识别这个 'smt' 文件？
Z3 v4.2 还支持 smt 文件。您能否添加指向 MathSAT 生成的 SMT 文件的链接？
seg.nju.edu.cn/BACH/Demo/sample_100.smt 谢谢你的帮助。
该文件不符合 SMT 1.0 标准。您必须指定逻辑。在:status unknown 行之前添加:logic QF_LRA 行，Z3 将接受该文件。
为什么 z3 v4.3 在我不添加 'logic QF_LRA' 的情况下可以解决这个 'smt' 文件？您的意思是当添加此行时，“smt”文件符合 SMT 1.0 标准？非常感谢您的帮助。