z3能否读取MathSAT的输出文件作为其输入文件？

我需要使用z3和mathsat进行一些实验。我已经完成了mathsat的实验。编写mathsat的输入文件需要很长时间，我不想再为z3编写输入文件。 Mathsat支持从'msat'文件生成'smt'文件。转换命令如下所示：z3能否读取MathSAT的输出文件作为其输入文件？

/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'文件吗？

来源

2013-01-04 Dingbao Xie

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

来源

2013-01-04 14:38:49

我已经试过了，它在4.2版本上无法使用。但是，它可以在最新版本的4.3版上运行。我只是想知道结果是否正确。虽然z3 v4.3可以工作并打印结果，这是否意味着它可以识别这个'smt'文件。为什么z3 v4.2不能识别这个'smt'文件？ –

Z3 v4.2也支持smt文件。你可以添加一个由MathSAT生成的SMT文件的链接吗？ –

http://seg.nju.edu.cn/BACH/Demo/sample_100.smt感谢您的帮助。 –

z3能否读取MathSAT的输出文件作为其输入文件？

回答

相关问题