Как проверить, равен ли результат symTake конкретному списку?
Это мой код:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
import Grisette
x :: SymInteger
x = "x"
y :: SymInteger
y = "y"
numbers :: [SymInteger]
numbers = [x, y]
n :: SymInteger
n = "n"
result :: UnionM [SymInteger]
result = symTake n numbers
main :: IO ()
main = do
print $ result .== [1, 2]
Я хочу проверить, может ли result быть равным [1, 2]. Я могу проверить, может ли простой список целых символьных чисел быть равен [1, 2]. Например, я могу сделать это:
x :: SymInteger
x = "x"
y :: SymInteger
y = "y"
main :: IO ()
main = do
print $ [x, y] .== [1, 2]
Но я не могу найти способ сделать это с результатом symTake. Читая код/документацию в коде, кажется, что я не должен распаковывать [SymInteger] из UnionM, но тогда я не знаю, как проверить равенство.
Ответы 2
Я думаю, вы хотите:
print $ result .== mrgSingle [1, 2]
Проблема здесь в том, что применение symTake к списку [x,y] может привести к получению списка размером 0, 1 или 2, и в отличие от списка фиксированной длины numbers = [x,y] для этого требуется правильное представление UnionM. Чтобы сравнить UnionM с не-UnionM, вы должны использовать mrgSingle, чтобы подчеркнуть отсутствие союза.
Результат выглядит правдоподобно, хотя и немного усложнен:
> main
(&& (! (<= 0 (- n))) (&& (! (<= -1 (- n))) (&& (= x 1) (= y 2))))
Спасибо за ответ К.А.Бура. Поскольку я нечасто участвую в переполнении стека, мне не хватает необходимых очков репутации, чтобы опубликовать эту информацию в виде комментария.
Начиная с Grisette v0.5.0.0, функция symTake была переименована в mrgTake. Это изменение было сделано для установления более единообразного соглашения об именах в библиотеке:
- Функции с префиксом
sym*могут возвращать результаты без объединения. - Функции с префиксом
mrg*обычно возвращают результаты, заключенные в союз.
Это должно прояснить, что в этом сценарии вам нужно обернуть результаты в UnionM.
Спасибо, это имеет смысл! И я могу аналогично задать вопрос:
Right model <- solve (precise z3) $ result .== mrgSingle [1, 2]всем желающим.