0

I need to conduct some experiments using z3 and mathsat. I have already finished the experiments with mathsat. It takes a lot of time to write the input file for mathsat and I don't want to write the input files for z3 again. Mathsat supports generating 'smt' files from the 'msat' files. The converting command is shown below:

/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

My question is that can z3 recognize this 'smt' file?

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
Dingbao Xie
  • 716
  • 9
  • 21

1 Answers1

0

Z3 can read SMT 1.0 and 2.0 files. The format is defined at http://www.smtlib.org. If the formulas generated by MathSAT are compliant with the standard, then you should have no problems. Have you tried to use Z3 to read the generated files? If it didn't work, what was the error message produced by Z3?

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • I have tried, it didn't work on version 4.2. However, it can work on version 4.3 which is the latest version. I just wonder whether the result is correct. Although z3 v4.3 can work and print the result, does that mean it recognize this 'smt' file. Why z3 v4.2 didn't recognize this 'smt' file? – Dingbao Xie Jan 05 '13 at 03:48
  • Z3 v4.2 also has support for smt files. Could you add a link to the SMT file produced by MathSAT? – Leonardo de Moura Jan 05 '13 at 04:11
  • http://seg.nju.edu.cn/BACH/Demo/sample_100.smt Thanks for youe help. – Dingbao Xie Jan 05 '13 at 05:23
  • The file is not compliant with the SMT 1.0 standard. You must specify the logic. Add the line `:logic QF_LRA` before the line `:status unknown` and Z3 will accept the file. – Leonardo de Moura Jan 05 '13 at 07:44
  • Why z3 v4.3 can solve this 'smt' file when I don't add 'logic QF_LRA'? You mean that when this line is added, the 'smt' file is compliant with the SMT 1.0 standard? Thanks a lot for your help. – Dingbao Xie Jan 05 '13 at 08:01
  • Z3 v4.3 accepts more smt files that are not compliant with the standard. I didn't check if the rest of the file is compliant. The line I sent is part of the standard, and should be included. There may be other problems that will affect other smt solvers. – Leonardo de Moura Jan 05 '13 at 08:13
  • Okay, I know. Maybe I need to rewrite the problem using the input language of z3 to guarantee there is no compliant. – Dingbao Xie Jan 05 '13 at 08:17