Próbuję pobrać wszystkie możliwe modele dla teorii pierwszego rzędu przy użyciu Z3, solvera SMT opracowanego przez Microsoft Research. Oto minimalny przykład pracy:

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

W tym przypadku istnieją dwa zadowalające zadania:f->true if->false. Ponieważ Z3 (i ogólnie rozwiązania SMT) będą próbować znaleźć tylko jeden zadowalający model, znalezienie wszystkich rozwiązań nie jest możliwe bezpośrednio.Tutaj Znalazłem przydatne polecenie o nazwie(next-sat), ale wydaje się, że najnowsza wersja Z3 już tego nie obsługuje. Jest to dla mnie trochę niefortunne i generalnie uważam, że polecenie jest całkiem przydatne. Czy jest inny sposób, aby to zrobić?