Comments (9)
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.
from sbv.
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.)
from sbv.
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.
from sbv.
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?
from sbv.
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.
from sbv.
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
from sbv.
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 😄
from sbv.
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.
from sbv.
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 😄
from sbv.
Related Issues (20)
- SBV->C: Support arbitrary size bit-vectors, and in general all(?) SBV types HOT 10
- Create `NonEmpty` instances for `EqSymbolic`, `OrdSymbolic`, `Mergeable`, etc.
- Set support for cvc5 HOT 1
- ExtractIO HOT 1
- Zombie process fixes HOT 5
- Tower example
- Q: Results of 'wpProveWith' HOT 2
- Generating `Num (SBV a)` instances "generically" HOT 10
- CFP case missing in the Eq instance for CVal HOT 5
- Unsound term simplification for ite with SFloatingPoint HOT 2
- FAQ: best practices for records? HOT 4
- Explore `Iso` instances
- Consider removing `Num a => Num (SBV a)` instance
- Make OptimizeResult type dependent on OptimizeStyle HOT 3
- Ranges over SIntegers HOT 4
- Let 'optimize' return variable values HOT 2
- Using uninterpreted functions in a quantified formula will not declare it in the top-level HOT 10
- Soft Question: Best approach for fixed size symbolic arrays HOT 13
- `checkSatWith` in analogy to `satWith` HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from sbv.