Как избавиться от решений с -0.0 в SBV

Следующий код (с использованием SBV):

{-# LANGUAGE ScopedTypeVariables #-}
import Data.SBV
main :: IO ()
main = do
    res <- allSat zeros
    putStrLn $ show res

zeros :: Predicate
zeros = do
    z1 <- sDouble "Z1"
    constrain $ z1 .== 0.0
    return true

генерирует два решения:

Solution #1:
  Z1 = 0.0 :: SDouble
Solution #2:
  Z1 = -0.0 :: SDouble
Found 2 different solutions.

Как удалить неинтересное -0.0 решение? Я не могу использовать z1 ./= -0.0, потому что это также верно, когда z1 равно 0.0.


haskell smt
person MichalAntkiew    schedule 26.03.2015    source источник
comment
Чтобы распознать x=-0, вы можете сделать x==0 && (1/x)‹0   -  person augustss    schedule 26.03.2015
comment
Хороший вопрос. Моя первая реакция была signum (-0.0) (нет, возвращает ноль) и isNegativeZero (нет, нет экземпляра для SDouble).   -  person Thomas M. DuBuisson    schedule 26.03.2015
comment
Как сказал @augustss, переведенный на SBV: (x .== 0) &&& ((1 / x) .< 0)   -  person Thomas M. DuBuisson    schedule 26.03.2015
comment
К сожалению, добавление `(1/x)‹0` делает решение ужасно медленным.   -  person MichalAntkiew    schedule 26.03.2015

Ответы (2)


arrow_upward
3
arrow_downward

[Обновлено после выпуска SBV 4.4 на Hackage (http://hackage.haskell.org/package/sbv), что обеспечивает надлежащую поддержку.]

Предполагая, что у вас есть SBV >= 4.4, теперь вы можете сделать:

Prelude Data.SBV> allSat $ \z -> z .== (0::SDouble)
Solution #1:
  s0 = 0.0 :: Double
Solution #2:
  s0 = -0.0 :: Double
Found 2 different solutions.
Prelude Data.SBV> allSat $ \z -> z .== (0::SDouble) &&& bnot (isNegativeZeroFP z)
Solution #1:
  s0 = 0.0 :: Double
This is the only solution.
person alias    schedule 30.03.2015

arrow_upward
1
arrow_downward

Судя по комментариям, следующий код выдает только одно решение:

zeros :: Predicate
zeros = do
    z1 <- sDouble "Z1"
    constrain $ z1 .== 0.0 &&& ((1 / z1) .> 0)
    return true

Выход:

Solution #1:
  Z1 = 0.0 :: SDouble
This is the only solution.
person MichalAntkiew    schedule 26.03.2015
comment
SBV имеет несколько распознавателей для чисел с плавающей запятой: isFPPoint (распознает числа с плавающей запятой, т. е. без значений NaN или бесконечностей), isSNaN (который распознает числа NaN), и мы определенно можем добавить к ним isSNegativeZero/isSPositiveZero и т. д. В то же время приведенное выше решение является адекватным, но на самом деле оно требует больших затрат, поскольку оно включает в себя арифметику и сравнения для этого тривиального теста, который базовый решатель может реализовать гораздо эффективнее. Не стесняйтесь отправить заявку на странице SBV github, и я добавлю ее в следующем выпуске (github. com/LeventErkok/sbv/issues). - person alias; 26.03.2015
comment
Да, это действительно очень дорого. Я создал следующую функцию для определения вероятностей: probability :: String -> Symbolic SDouble probability varName = do { x <- sDouble varName; constrain $ x .>= 0.0 &&& x .<= 1 &&& ((1 / x) .> 0); return x } И даже тривиальная модель занимает намного больше времени, чем без части &&& ((1 / x) .> 0). Есть ли что-нибудь, что мы могли бы использовать непосредственно в SMT-Lib? - person MichalAntkiew; 26.03.2015
comment
Мне может быть достаточно добавить тест isPositive :: SDouble -> SBool как (fp.isPositive (_ FloatingPoint eb sb) Bool). - person MichalAntkiew; 26.03.2015
comment
Почему вы добавили это в качестве ограничения, если это так сильно замедляет решение? Просто отфильтруйте нежелательный результат, пока кто-нибудь не исправит SBV эффективным методом. - person Thomas M. DuBuisson; 26.03.2015
comment
@ThomasM.DuBuisson делает хороший вывод: хорошей альтернативой является извлечение результатов и отбрасывание результатов на стороне Haskell. Конечно, наличие предикатов — лучший выбор. Одна из целей SBV — сделать все доступным для пользователя, чтобы можно было писать произвольные программы для создания задач и обработки выходных моделей, поэтому я хотел бы знать, попробуете ли вы это и возникнут ли какие-либо проблемы. - person alias; 30.03.2015