При запуске следующего кода:
answer = do
-- elts is a list of the values we're trying to satisfy for
x <- doSomething
{- ... constraints and other stuff ... -}
query $ do cs <- checkSat
case cs of
Sat -> getValue x
Unsat -> error "Solver couldn't find a satisfiable solution"
DSat{} -> error "Unexpected dsat result!"
Unk -> error "Solver returned unknown!"
runSMT answer
-- output: one single satisfying solution
SBV/Z3 возвращает уникальное удовлетворительное решение. Как вместо этого получить список всех (возможно, до n) удовлетворяющих решений? Я знаю о sat по сравнению с allSat при запуске примеров hello-world, но я не уверен, как подключить его к более сложному контексту выше. Я также читал о extractModels (обратите внимание на множественное число), но документации по этому вопросу не так много.
В качестве альтернативы, есть ли способ получить случайное удовлетворительное решение для одной и той же проблемы, а не всегда одно и то же?
