Haskell中SBV求解器中无变量的平凡有理问题

Question

我在Haskell中使用SBV求解器，特别是我使用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)

solution3不工作，它返回

*** 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求解器的情况下解决这个问题，但是在这个问题出现的上下文中，用求解器来解决它对我来说更容易。

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

Answer 1

这看起来像是一个bug，我认为SBV的作者在这个模式匹配中忘记了CRational:

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

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