Principle of least astonishment violated for symbolic types whose metric space type differs in representation

[andrew-wja]

Using GHC 9.6.5 and SBV 10.10

I have the following program which does not behave as I expect, and I suspect my thinking is wrong somewhere.

module Main where

import Data.SBV

constructQuery :: [Float] -> Symbolic ()
constructQuery values = do
    constrainedVars <- mapM construct $ zip [0..] values
    minimize "total" (sum constrainedVars)
    where 
        construct (index, value) = do
            introVar <- sFloat $ "variable_" ++ show index
            constrain $ introVar .== literal value
            return introVar

main = do
    result <- optimize Lexicographic $ constructQuery [12.2, 1.44, 3.7]
    print result

What I expect this program to do is to "solve" the trivial problem where the variables are all constrained to an exact value, and compute the sum of those values (this is a reduction for demonstration purposes from a larger problem where these variables are not so constrained).

ghci> main
Optimal model:
  variable_0 =       12.2 :: Float
  variable_1 =       1.44 :: Float
  variable_2 =        3.7 :: Float
  total      = 3247093842 :: Word32

What actually happens is that I see a Word32 value coming out when the type of the symbolic values is sFloat. I cannot seem to make the problem go away by putting in explicit types, and anyway ghci tells me the inferred types are correct. Help? Is this just a completely erroneous way of constructing sums of symbolic values? It gets no better if I explicitly use + on the list elements instead of a fold.

[andrew-wja]

What I suspect might be happening here is that I am asking for the sum of the string values of the character names to be minimized, given the types of the results. But in that case, how to construct the symbolic sum of the values?

[andrew-wja]

I think I can upgrade this to a bug -- the binary contents of that Word32 appear to contain the correct value (the sum of the floating point values). So SBV is coercing this result to Word32 erroneously.

[andrew-wja]

I can force out the right value with a lot of horrid hacks like so, but the sign bit appears to be incorrect in addition to the ergonomic problems

module Main where

import Data.SBV
import GHC.Float
import Data.Maybe (fromJust)
import Data.SBV.Internals

constructQuery :: [Float] -> Symbolic ()
constructQuery values = do
    constrainedVars <- mapM construct $ zip [0..] values
    minimize "total" (sum constrainedVars)
    where 
        construct (index, value) = do
            introVar <- sFloat $ "variable_" ++ show index
            constrain $ introVar .== literal value
            return introVar

main = do
    (LexicographicResult result@(Satisfiable _ model)) <- optimize Lexicographic $ constructQuery [12.2, 1.44, 3.7]
    print model
    let (RegularCV value) = fromJust $ getModelObjectiveValue "total" result
    print value
    print $ showType value
    let (CInteger v) = cvVal value
    print $ castWord32ToFloat $ fromIntegral v

main2 = do
    (LexicographicResult result@(Satisfiable _ model)) <- optimize Lexicographic $ constructQuery [0.0, 0.0, 0.0]
    print model
    let (RegularCV value) = fromJust $ getModelObjectiveValue "total" result
    print value
    print $ showType value
    let (CInteger v) = cvVal value
    print $ castWord32ToFloat $ fromIntegral v
    

This shows

ghci> main
SMTModel {modelObjectives = [("total",3247093842 :: Word32)], modelBindings = Nothing, modelAssocs = [("variable_0",12.2 :: Float),("variable_1",1.44 :: Float),("variable_2",3.7 :: Float),("total",3247093842 :: Word32)], modelUIFuns = []}
3247093842 :: Word32
"SWord32"
-17.34
ghci> 12.2 + 1.44 + 3.7
17.34
ghci> main2
SMTModel {modelObjectives = [("total",2147483648 :: Word32)], modelBindings = Nothing, modelAssocs = [("variable_0",-0.0 :: Float),("variable_1",-0.0 :: Float),("variable_2",-0.0 :: Float),("total",2147483648 :: Word32)], modelUIFuns = []}
2147483648 :: Word32
"SWord32"
-0.0

[LeventErkok]

When you optimize a quantity, what you're actually optimizing is its value in the optimization metric space. See https://hackage.haskell.org/package/sbv-10.10/docs/Data-SBV.html#t:MetricSpace

For most types the metric space is equivalent to the type itself. This is typically the case when the underlying solver (i.e., z3) supports optimization over that type. But there are certain types that the optimizer just doesn't support (Floats for instance), or you might want to have a different notion of a "metric" to optimize for given a custom data-type. This is the motivation for MetricSpace.

If you look at the MetricSpace instance for SFloat, you'll see that it's Word32: https://hackage.haskell.org/package/sbv-10.10/docs/src/Data.SBV.Core.Floating.html#line-555

The reason for this is twofold: (1) The underlying optimizer doesn't support optimizing floats. (2) You don't want NaN values to be part of the equation when maximizing.

So, the Word32 value you're seeing is the "metric space" value for the sum; not the total sum as a float itself. This can be confusing at times, so it's best to always separate your optimization goal in the metric space from the actual value. That is, write something like:

module Main where

import Data.SBV

constructQuery :: [Float] -> Symbolic ()
constructQuery values = do
    constrainedVars <- mapM construct $ zip [0..] values
    let s = sum constrainedVars
    sObserve "total" s
    minimize "total_metric" $ s
    where.
        construct (index, value) = do
            introVar <- sFloat $ "variable_" ++ show index
            constrain $ introVar .== literal value
            return introVar

main = do
    result <- optimize Lexicographic $ constructQuery [12.2, 1.44, 3.7]
    print result

This prints:

Optimal model:
  total        =      17.34 :: Float
  variable_0   =       12.2 :: Float
  variable_1   =       1.44 :: Float
  variable_2   =        3.7 :: Float
  total_metric = 3247093842 :: Word32

Making it clear the total is 17.34, and its metric space equivalent is 3247093842 :: Word32. Alternatively, you can also use the fromMetricSpace/toMetricSpace functions:

*Main> fromMetricSpace (3247093842 :: SWord32) :: SFloat
17.34 :: SFloat
*Main> toMetricSpace (17.34::SFloat)
3247093842 :: SWord32

Since metric-space is typically equivalent to itself for the typical use case of Real and Integer values, we usually skip this distinction. But when they are not (essentially floats and signed integers), you need to remember how optimization works over metric spaces and not over the actual type. For instance, the same is also true for signed integers:

*Main> optimize Lexicographic $ \(x::SInt8) -> minimize "metric_x" x
Optimal model:
  s0       = -128 :: Int8
  metric_x =    0 :: Word8

Note how the value of x is correctly minimized to -128, but its minimized metric value is 0. The underlying solver only optimizes bit-vectors as unsigned values, so SBV "adjusts" the value by transferring to/from the corresponding metric space.

There's some documentation here: https://hackage.haskell.org/package/sbv-10.10/docs/Data-SBV.html#g:54, but it can always be improved. PR's that improve documentation are always welcome, if you would like to submit a patch.

[andrew-wja]

Ah, this makes a lot of sense! I was starting to suspect it was a solver-related implementation constraint like this. Thank you for the detailed explanation, that is really helpful. I certainly think that this could benefit from some example code (perhaps this exact example) in the "Model Extraction" part of the documentation. I'll open a PR 😄

[LeventErkok]

I think we can do a little better here, and actually add extra "values" to the output when the metric space differs from the underlying type. I'm working on a patch as we speak. Let's see if that's more helpful. (You might want to hold off on your documentation PR till the new version is ready so it matches the latest code.)

[LeventErkok]

@andrew-wja

As of 88581bd, I think the output should be less confusing. For your original program, we now print:

*Main> main
Optimal model:
  total      =      17.34 :: Float
  variable_0 =       12.2 :: Float
  variable_1 =       1.44 :: Float
  variable_2 =        3.7 :: Float
  MS(total)  = 3247093842 :: Word32

Is this better? We can change the MS(total) (the metric space value of the total) notation if you can think of something better. Let me know.

[andrew-wja]

This is super, thank you!

I think the least astonishing choice for the symbolic type of a value defined by expressions in an optimization query is the symbolic correspondent of the type that would be inferred in Haskell for the concrete version of those statements. It's important to understand the practical implementation impact (ostensibly using a backend solver with native support for the types involved would result in a faster solve), and I think this change also makes that more visible; seeing extra "metric space" variables in your optimized model is a clear indicator that the optimizer you have chosen is not directly representing the types you're using.

👍 from me!

I think perhaps metric(total) is more obvious than MS(total) but that's just my personal preference 😄

[LeventErkok]

Cool. I pushed in a change and the output now is:

Optimal model:
  total                =      17.34 :: Float
  variable_0           =       12.2 :: Float
  variable_1           =       1.44 :: Float
  variable_2           =        3.7 :: Float
  toMetricSpace(total) = 3247093842 :: Word32

After all toMetricSpace is the name of the Haskell function you'd call anyhow; so the last line of the output is a valid Haskell equation.

I'm closing this ticket as resolved; though feel free to open others if you see other fishy behavior. I consider "usability" bugs just as important as functional bugs. Thanks.