Comments (3)
Another confusing output:
[merzifon]~>crackNum -f3+4 0.9375
Satisfiable. Model:
ENCODED = 0.938 :: FloatingPoint 3 4
6 543 210
S E3- S3-
Binary layout: 0 010 111
Hex layout: 17
Precision: 3 exponent bits, 3 significand bits
Sign: Positive
Exponent: -1 (Stored: 2, Bias: 3)
Classification: FP_NORMAL
Binary: 0b1.111p-1
Octal: 0o7.4p-3
Decimal: 0.938
Hex: 0xfp-4
Rounding mode: RNE: Round nearest ties to even.
Note: Conversion from "0.9375" was exact. No rounding happened.
Note that the "note" says the conversion was exact, but we see 0.938
printed, not 0.9375
. Again, this isn't incorrect. It's just terribly confusing.
from sbv.
Looking at the code, what we do is simply call show
for haskell types and bfToString 10 True False
for LibBF values.
Instead, we should call showFFloat
with a user given precision value. (Not sure if there's an equivalent of that in bfToString
.) This way we can control the output and make this much less confusing.
This is something we should do, but need a bit more digging to figure out exactly how to approach. For instance, it would be nice to add ...
at the end if the remaining digits aren't 0. Doable? Perhaps?
from sbv.
Triggering from sbv directly:
*Data.SBV> satWith z3{crackNum=True} $ \x -> x .== (0.9375 :: SFloatingPoint 3 4)
Satisfiable. Model:
s0 = 0.938 :: FloatingPoint 3 4
6 543 210
S E3- S3-
Binary layout: 0 010 111
Hex layout: 17
Precision: 3 exponent bits, 3 significand bits
Sign: Positive
Exponent: -1 (Stored: 2, Bias: 3)
Classification: FP_NORMAL
Binary: 0b1.111p-1
Octal: 0o7.4p-3
Decimal: 0.938
Hex: 0xfp-4
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
- Principle of least astonishment violated for symbolic types whose metric space type differs in representation HOT 9
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.