Может ли z3 прочитать выходной файл MathSAT как его входной файл?

Question

Может ли z3 прочитать выходной файл MathSAT как его входной файл?

Мне нужно провести несколько экспериментов с использованием z3 и mathsat. Я уже закончил эксперименты с mathsat. Написание входного файла для mathsat занимает много времени, и я не хочу снова записывать входные файлы для z3. Mathsat поддерживает создание файлов smt из файлов msat. Команда преобразования показана ниже:

/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'?

0

z3 smt

Источник

user1831451 04 янв '13 в 12:22

1 ответ

Решение

Другие вопросы по тегам z3 smt

user841416 04 янв '13 в 14:38 2013-01-04 14:38 · Accepted Answer · 2013-01-04 14:38

Z3 может читать файлы SMT 1.0 и 2.0. Формат определяется по адресу http://www.smtlib.org/. Если формулы, сгенерированные MathSAT, соответствуют стандарту, у вас не должно возникнуть проблем. Вы пытались использовать Z3 для чтения сгенерированных файлов? Если это не сработало, что за сообщение об ошибке выдает Z3?