SBV multi-SAT queries interact poorly with rationals

[robdockins]

Because the SBV multi-SAT procedure doesn't understand the semantics of a pair of integers as a rational number, it will enumerate different representatives of the same equivalence class of pairs of integers when asked a multi-SAT query involving rational numbers. These are normalized before being presented to the user, and it appears the solver is repeatedly returning the same assignment.

Cryptol> :set satNum=10
Cryptol> :set prover=sbv-z3
Cryptol> :sat (\x -> x == ratio 1 2)
Satisfiable
(\x -> x == ratio 1 2) (ratio 1 2) = True
(\x -> x == ratio 1 2) (ratio 1 2) = True
(\x -> x == ratio 1 2) (ratio 1 2) = True
(\x -> x == ratio 1 2) (ratio 1 2) = True
(\x -> x == ratio 1 2) (ratio 1 2) = True
(\x -> x == ratio 1 2) (ratio 1 2) = True
(\x -> x == ratio 1 2) (ratio 1 2) = True
(\x -> x == ratio 1 2) (ratio 1 2) = True
(\x -> x == ratio 1 2) (ratio 1 2) = True
(\x -> x == ratio 1 2) (ratio 1 2) = True
(Total Elapsed Time: 0.025s, using "Z3")
Cryptol> :set prover=w4-z3
Cryptol> :sat (\x -> x == ratio 1 2)
Satisfiable
(\x -> x == ratio 1 2) (ratio 1 2) = True
(Total Elapsed Time: 0.036s, using "z3")

The What4 backend controls its own loop for finding multiple assignments and computes its own blocking predicates using the equivalence relation for rationals, and thus will avoid other representatives of the same class. We should do the same for SBV.

[LeventErkok]

The newly released SBV 8.13 (https://hackage.haskell.org/package/sbv-8.13) has native support for SRational:

Prelude Data.SBV Data.SBV.Rational> allSat $ \x -> x .== 1 .% 2
Solution #1:
  s0 = 1 % 2 :: Rational
This is the only solution.

If you move to 8.13; you can map Cryptol's rationals to SBV's, and automatically handle this problem without lifting a finger!

[robdockins]

Neat!