Испытание выполнимости по отношению к фиксированной частичной модели

Question

Предположим, что я утвердил некоторую формулу P и, проверив выполнимость, полученную из Z3 частичной модели для него, назовем ее M .

Теперь можно ли проверить, можно ли удовлетворить другую формулу Q , расширив, если необходимо, текущую модель M .То есть я хочу проверить, являются ли формулы P и Q выполнимыми, но фиксируя значения, которые были назначены текущей частичной моделью.

В качестве альтернативы, можно ли попросить Z3«Завершить» конкретную частичную модель?(То есть я все еще хочу получить частичные модели; но в некоторых случаях я хотел бы иметь возможность расширить частичную модель, чтобы затем я мог оценить некоторую произвольную формулу Q , которая может содержать константы/ функции, не назначенные текущей моделью)

Answer 1

Будет ли работать в вашей ситуации проверка P , извлечение частичной модели M , построение формулы N , которая является просто сочетанием равенств, назначенных в M , затем проверьте N и Q ?Это должно быть непосредственно реализовано с использованием API, но, вероятно, в меньшей степени с текстовым интерфейсом.