Z3 C++, как разобрать smt-конкуренцию unsat core экземпляры

Question

Я пытаюсь использовать Z3 с C++ api (версия Z3 4.1.0.0), а именно, я пытаюсь разобрать экземпляры с ненасильной основной дорожки smt-конкурента. я написал (на примерах) следующий код:

context c; 
Z3_ast f; 
f = Z3_parse_smtlib2_file(c, "smtlib_uc/QF_IDL/queens_bench/n_queen/queen3-1.smt2.uc.smt2", 0, 0, 0, 0, 0, 0); 
expr r = to_expr(c, f); 
solver s(c); 
s.add(r); 
std::cout << s << "\n"; 

, но я получаю следующее сообщение об ошибке:

(ошибка «строка 1 столбец 34: Ошибка настройки ': продуцируют-unsat-сердечники' , значение параметра не может быть изменен после инициализации ")

(ошибка„строка 220 столбец 15: unsat конструкция сердечника не включена, используйте команду (параметр установлен-: производство-unsat сердечников истинно)“)

непредвиденная ошибка: Ошибка синтаксического анализа

ли кто-нибудь знает, как преодолеть эту ошибку?

Answer 1

Z3_parse_smtlib* функции предназначены только для разбора формул; поэтому с ними не будет работать много вариантов.

Вы можете просто удалить строку (set-option :produce-unsat-cores true) во входном файле и установить эту опцию при инициализации context. Вы можете получить ненадежное ядро ​​с помощью Z3_solver_get_unsat_core.

Если вы не хотите изменять входные файлы, вместо этого вы должны использовать двоичный код Z3. Эти параметры будут успешно проанализированы двоичным кодом Z3.