CHC solver: generalization

[kroening]

This adds generalization for loop invariants using the frequency of disjuncts in the candidate invariant for the frame where the inductiveness check has failed.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• 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

Base: 78.00% // Head: 78.01% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (c92a05c) compared to base (61577ae).
Patch coverage: 80.80% of modified lines in pull request are covered.

❗ Current head c92a05c differs from pull request most recent head 38aabd6. Consider uploading reports for the commit 38aabd6 to get more accurate results

Additional details and impacted files

@@            Coverage Diff            @@
##           develop    #7268    +/-   ##
=========================================
  Coverage    78.00%   78.01%            
=========================================
  Files         1621     1625     +4     
  Lines       187273   187407   +134     
=========================================
+ Hits        146089   146201   +112     
- Misses       41184    41206    +22     

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.cpp	65.46% <66.66%> (-0.01%)	⬇️
src/cprover/solver_types.cpp	76.92% <76.92%> (ø)
src/cprover/inductiveness.cpp	78.35% <78.35%> (ø)
src/cprover/solver.cpp	92.00% <81.81%> (+10.46%)	⬆️
src/cprover/generalization.cpp	84.21% <84.21%> (ø)
src/cprover/inductiveness.h	100.00% <100.00%> (ø)
src/cprover/propagate.cpp	74.28% <100.00%> (+0.75%)	⬆️
src/cprover/solver_types.h	93.10% <100.00%> (+4.21%)	⬆️
src/goto-instrument/unwind.cpp	100.00% <100.00%> (ø)
src/ansi-c/expr2c.cpp	67.27% <0.00%> (-0.05%)	⬇️
... and 2 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[tautschnig]

Comments describing what the methods are supposed to do would be really helpful.