Documentation for decreases clauses

[SaswatPadhi]

Related to #6149.

Thanks to @LongPham7 for an initial draft!

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• n/a Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #6332 (12b22c0) into develop (aeba3f0) will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #6332   +/-   ##
========================================
  Coverage    75.89%   75.89%           
========================================
  Files         1515     1515           
  Lines       163972   163972           
========================================
  Hits        124444   124444           
  Misses       39528    39528           

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 38d945a...12b22c0. Read the comment docs.

[feliperodri]

@SaswatPadhi can we close #6149 after merging this PR? The only initial documentation missing will be assigns clause for loops, correct?

[SaswatPadhi]

@SaswatPadhi can we close #6149 after merging this PR? The only initial documentation missing will be assigns clause for loops, correct?

I think we can close it after this + assigns clause documentation is merged. I would push the assigns clause documentation to #6249

[SaswatPadhi]

I have addressed all prior comments and fixed some build issues (with the new binary_search regression test).

Keeping this PR open for one final review from @jimgrundy.

[jimgrundy]

I would suggest cutting the material after "strict lexicographic comparison". Maybe hyperlink off "lexicographic comparison" to the article you linked earlier, and you can skip the explanation of how you implement a lexicographic compare. If people know what one is already they don't need to see this code. If they don't, they might be better off reading the code. But, if you like it, then I'm OK with it.

[SaswatPadhi]

Okay, I could remove it. I wasn't sure if end users would be familiar with exactly what lexicographic comparison on ordered tuples would mean. I didn't want to point them to research papers just for that, but I guess they could Google it if they are unsure :)

[jimgrundy]

This works because we use "long long" values to avoid overflow. But, we can do the computation another way and avoid overflow while using fewer bits, which might give better solver performance. Take a look at this article for a nice clear way to express the algorithm without the extra bits: Extra, Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken. Now, since the use of int for the arguments and long long for the computation should mean this is correct (are there machines for which int is the same size as long long?) then I'm fine with leaving this as is, but I think you might like the version in this article better anyway

[SaswatPadhi]

Thanks! :D Great point!

Now, since the use of int for the arguments and long long for the computation should mean this is correct (are there machines for which int is the same size as long long?)

It's correct (verified) only on 64-bit Windows and Linux machines -- the CBMC CI machines & my machine.
I originally had long, and that failed because on Windows int == long, apparently! Then I changed to long long and both Windows + Linux were happy. But that's still fragile -- even long long could be the same as int on some platform.

I implemented the change. The verification time with MiniSAT remains the same (~2.7s), but the number of variables in the SAT formula goes from ~12900 down to ~7700.