Есть ли способ получить все удовлетворяющие задания, используя синтаксис SMTLIB2?
Я использую решатели Z3 и CVC4.
Как получить все удовлетворяющие задания в SMTLIB2?
Ответы (1)
Хотя нет способа сделать это в «чистом» SMTLIB2, то есть только с одним файлом и без внешнего ввода, если у вас есть приложение, которое может взаимодействовать с решателем, для этого есть стандартный прием. Вы запускаете решатель в интерактивном режиме, где можете по одной посылать ему команды SMTLIB2, а затем взаимодействовать с ним следующим образом (псевдокод):
def get_all_assignments(instance):
create solver in interactive mode
for each declaration, assertion, etc. in instance:
send assertion to solver
let response := None
while response is not UNSAT:
send command '(check-sat)' to solver and get response
if response is SAT:
send command '(get-model)' to solver and get model
print model
send the solver a new assertion which is the negation of the model
По сути, каждый раз, когда вы находите удовлетворительное задание, вы добавляете в свою модель новое ограничение, которое не позволяет решателю снова найти это задание, и просите его выполнить повторное решение. Когда решатель возвращает UNSAT, вы знаете, что нашли все подходящие задания.
Дополнительную информацию по этой теме и реализациям для Z3 см. в Z3: поиск всех удовлетворяющих моделей и Z3py: проверка всех решений уравнения.
person
mtrberzi
schedule
18.11.2015
