Сбой Z3 даже после установки интерактивного режима в True - PullRequest
Новая
       12

Сбой Z3 даже после установки интерактивного режима в True

0 голосов
/ 06 июля 2019

Я использую Java API Z3 для решения файла smt, используя метод parseSMT2File(). Однако, даже если я установлю params.add("interactive-mode", true), а затем solver.setParameters(params), Z3 выдаст следующую ошибку: 

Exception in thread "main" com.microsoft.z3.Z3Exception: (error "line 276 column 23: model is not available")
(error "line 277 column 26: model is not available")
(error "line 279 column 15: command is only available in interactive mode, use command (set-option :interactive-mode true)")
(error "line 280 column 16: model is not available")

1 Ответ

2 голосов
/ 07 июля 2019

parseSMT2File() только анализирует утверждения из файла и возвращает их как одно выражение.Он не запускает много команд, включая check-sat, т. Е. Вы должны вызывать check() для решателя, к которому вы добавили утверждение.

...