Skip to content

use a hash table in the expression formatter #5817

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 21, 2021
Merged

Conversation

kroening
Copy link
Member

This replaces the linear-time if-then-else construct by a logarithmic hash
table. The hash table could be extended at runtime.

  • 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.
  • 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
Copy link

codecov bot commented Feb 11, 2021

Codecov Report

Merging #5817 (3724dea) into develop (93bd022) will increase coverage by 0.00%.
The diff coverage is 92.40%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5817   +/-   ##
========================================
  Coverage    72.88%   72.88%           
========================================
  Files         1421     1421           
  Lines       154217   154269   +52     
========================================
+ Hits        112395   112441   +46     
- Misses       41822    41828    +6     
Impacted Files Coverage Δ
src/util/format_expr.cpp 85.77% <92.40%> (+0.77%) ⬆️

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 46de6f6...3724dea. Read the comment docs.

@kroening kroening marked this pull request as ready for review February 11, 2021 19:49
expr_mapt expr_map;

/// find the formatter for a given expression
const formattert &find_formatter(const exprt &);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this be const?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As-is now yes, but was contemplating to generate formatters on the fly.


private:
/// setup the expressions we can format
void setup();
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Possibly a matter of taste: Is there value in having this extra method as opposed to just doing all work directly in the constructor?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not a whole lot, it may convey a bit of information to the reader.

This replaces the linear-time if-then-else construct by a logarithmic hash
table.  The hash table could be extended at runtime.
@kroening kroening force-pushed the format_expr_configt branch from efd4697 to 3724dea Compare February 21, 2021 13:06
@kroening kroening merged commit 8ac57fd into develop Feb 21, 2021
@kroening kroening deleted the format_expr_configt branch February 21, 2021 18:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants