2

我在 Haskell 中使用SBV Solver，特别是我使用 Rational 类型作为变量。

我想解决线性问题，例如：

 solution1 = do 
    [x] <- sRationals ["x"]
    constrain $ 5.%1  .<= x

代码工作没有问题，我的问题是当我想解决类型 5 <= 4 的“琐碎”情况如果它与整数一起工作我没有问题，我可以使用以下代码；

solution2 = do 
    xs <- sIntegers []
    constrain $ (5 :: SInteger) .<= (5 :: SInteger)

此代码可以正常工作

如果我尝试将等价物与 Rationals 一起使用：

solution3 = do 
   xs <- sRationals []
   constrain $ (5.%1:: SRational)  .<= (5.%1:: SRational)

解决方案3不起作用并返回

*** Exception: SBV.liftCV2: impossible, incompatible args received: (5 % 1 :: Rational,5 % 1 :: Rational)
CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/Concrete.hs:337:74 in sbv-8.15-6kqa1q33xxwHQg8FGWAWlC:Data.SBV.Core.Concrete

我可以引入一个虚拟变量。

solution = do 
    [dummy] <- sRationals ["dummy"]
    constrain $ dummy .== 0.%1
    constrain $ (5.%1:: SRational)  .<= (5.%1:: SRational) + dummy

它也可以，但我想知道是否可以在不引入此变量的情况下完成。

我当然可以不使用 SBV Solver 解决问题，但是在出现此问题的上下文中，我更容易从求解器中解决它

提前感谢，对不起我的英语，我用谷歌翻译来帮助我

4

1 回答 1

4

这似乎是一个错误，我认为 SBV 的作者在此模式匹配中忘记了 CRational：

https://github.com/LeventErkok/sbv/blob/cfaa40b8c8ff8e1b7ff9ab71304654f6f531ba72/Data/SBV/Core/Concrete.hs#L324-L336

我打开了一个问题：https ://github.com/LeventErkok/sbv/issues/591

于 2021-09-02T16:31:19.273 回答