Лог-файл формата SMT2

Question

Я пытаюсь изменить формат вывода файла журнала Z3 на формат SMT2 с помощью интерфейса JNI (Java). Эта проблема была помечена как решенная в выпуске # 867 , но метод, реализованный позже, изменился.

Согласно журналу изменений это должно быть возможно (в C) с solver.smtlib2_log = file сейчас. Однако я не могу установить этот параметр в Java, потому что он не существует для setParameter() или любой другой команды модуля решателя. Я что-то упускаю или это возможно только в не-JNI на данный момент?

Спасибо за вашу помощь.

Answer 1

Для всех, кому интересно, теперь работает smt2-logging, и вы можете использовать его двумя способами:

1. глобально: set_param ("solver.smtlib2_log", "log.smt2")

2. только решатель: solver.set ("smtlib2_log", "log.smt2")

, когда "log.smt2" находится в вашем файле журнала.