Я пытаюсь найти все возможные модели для некоторой теории первого порядка, используя Z3, решатель SMT, разработанный Microsoft Research. Вот минимальный рабочий пример:

(declare-const f Bool)
(assert (or (= f true) (= f false)))

В этом пропозициональном случае есть два удовлетворяющих задания:f->true а такжеf->false, Поскольку Z3 (и SMT-решатели в целом) будут пытаться найти только одну удовлетворительную модель, найти все решения напрямую невозможно.Вот Я нашел полезную команду под названием(next-sat), но, похоже, последняя версия Z3 больше не поддерживает это. Это немного неудачно для меня, и в целом я считаю, что команда весьма полезна. Есть ли другой способ сделать это?