I am working with SBV Solver in Haskell, specifically I am using the Rational type for the variables.
I want to solve linear problems for example:
solution1 = do
[x] <- sRationals ["x"]
constrain $ 5.%1 .<= x
The code works without problems, my problem is when I want to solve "trivial" cases of type 5 <= 4 If it works with Integers I have no problem, I can use the following code;
solution2 = do
xs <- sIntegers []
constrain $ (5 :: SInteger) .<= (5 :: SInteger)
This code works without problems
If I try to use the equivalent with Rationals:
solution3 = do
xs <- sRationals []
constrain $ (5.%1:: SRational) .<= (5.%1:: SRational)
solution3 doesn't work and it returns
*** 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
I can introduce a dummy variable.
solution = do
[dummy] <- sRationals ["dummy"]
constrain $ dummy .== 0.%1
constrain $ (5.%1:: SRational) .<= (5.%1:: SRational) dummy
It works too, but I want to know if it can be done without introducing this variable.
Of course I can solve the problem without the SBV Solver, but in the context in which this problem appears, it is easier for me to solve it from the solver
Thanks in advance and sorry for my English, I used google translate to help me
CodePudding user response：
This seems like a bug, I think the author of SBV forgot CRational in this pattern match:
I opened an issue: https://github.com/LeventErkok/sbv/issues/591