Integrated and Formatted hex-readable flag for SMTChecker

[ChrisCates]

Description

As part of issue #4648.
I have integrated a --hex-readable flag for the SMT/Z3 Theorem checker.

Feel free to review anytime @chriseth and @ryan-shea.

Checklist

• Code compiles correctly
• All tests are passing
• New tests have been created which fail without the change (if possible)
• README / documentation was extended, if necessary
• Changelog entry (if change is visible to the user)
• Used meaningful commit messages

[codecov]

Codecov Report

Merging #5447 into develop will increase coverage by <.01%.
The diff coverage is 89.83%.

@@             Coverage Diff             @@
##           develop    #5447      +/-   ##
===========================================
+ Coverage    88.08%   88.09%   +<.01%     
===========================================
  Files          308      309       +1     
  Lines        31239    31294      +55     
  Branches      3749     3754       +5     
===========================================
+ Hits         27518    27567      +49     
  Misses        2467     2467              
- Partials      1254     1260       +6

Flag	Coverage Δ
#all	88.09% <89.83%> (ø)	⬆️
#syntax	28.95% <10.71%> (-0.04%)	⬇️

[ChrisCates]

Hmm... Despite code coverage increasing slightly... It seems to say the check has failed...?~

[axic]

For small numbers like all the above I think it would make more sense displaying them in decimal.

[axic]

Say for <= 65536 it definitely makes sense.

[ChrisCates]

Okay great! I will get you these changes later today!~
Thanks for being quick and responsive!~

[ChrisCates]

Hey, just want to confirm here.
65536 = 0x10000

We were originally going with:
16777216 = 0x1000000

Would you like it at:
4294967296 = 0x100000000

instead? Im pushing up changes right now.

[axic]

Ah never mind, decimal would be nice if it would use a power of 10 on the right hand side.

[ChrisCates]

Could you clarify with an example output? 😺

[ChrisCates]

If what I provided (with the revisions) are good to go.
Please let me know and I will squash the commits for you and we can merge it into develop.

Feel free to ping @chriseth or @ryan-shea if you find any other issues!~

[leonardoalt]

I'm not sure about the command line flag. I think the SMTChecker should use the precise hex readable format by default.

[ChrisCates]

I'm not sure about the command line flag. I think the SMTChecker should use the precise hex readable format by default.

Is there anything else you would like done @leonardoalt? If not, I can update the flag to be the inverse. True instead of false, then squash commits to finalize the PR.

[leonardoalt]

I actually have two comments here:

1. Truncated values are good for general readability but useless for the SMTChecker since it masks the actual counterexamples. I think truncation should rather be an internal flag, such that each module can decide what they want.

2. Given 1), I'm not sure we need the command line parameter.

@axic @chriseth thoughts?

[leonardoalt]

@ChrisCates Please modify the PR such that:

• The SMTChecker always uses formatNumberReadable
• formatNumberReadable takes a parameter (default false) that tells whether it should truncate
• No command line flag is used

Then I think it should be fine to merge!

[ChrisCates]

@leonardoalt, I have a question in regards to the parameter for formatNumberReadable().

In what cases does the parameter become true? Without the command line flag... I'm not sure in which contexts it will change.

Also, I assume the revised formatting would be something like:

template <class T>
inline std::string formatNumberReadable(T _value, bool readable = false)
{
if (readable == false) return formatNumber(_value);
...

Once this is clarified, I will push and squash commits.

I am also going to start a new PR to get unit tests for CommonData.h some time this weekend.

[ChrisCates]

Closing for #5476 instead.