z3 -smt2 <filename> выводит только "sat" или "unsat". Я хотел бы, чтобы Z3 выводил модель, если ограничение выполнено, или ненадежное ядро, если не выполнено. Какие варианты Z3 мне следует использовать?
Как позволить командной строке z3 выводить режим (или ядро unsat), а не sat / unsat?
Ответы (1)
Для этого нет параметров командной строки, так как в SMTLIB2 это отдельные команды, (get-model) и (get-unsat-core), обе определяются только тогда, когда (check-sat) возвращает sat или unsat соответственно.
Параметры model и unsat-core должны быть включены независимо от того, используются ли те или иные команды, просто для того, чтобы решатель отслеживал правильную информацию, иначе команды (get-model) и (get-unsat-core) могут выйти из строя позже.
person
Christoph Wintersteiger
schedule
18.12.2015
Спасибо, Кристоф. В этом есть смысл.
- person zell; 18.12.2015
