Как да се отървете от решения с -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 или Infinities), 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