Skip to content

rename post_process to finish_eager_conversion #6551

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
Jan 12, 2022

Conversation

kroening
Copy link
Member

This renames a set of solver methods from post_process to
finish_eager_conversion. The term 'post processing' may be used either in
lazy or eager solving. The new name clarifies that this is about an eager
conversion.

  • 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/
  • 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 Dec 27, 2021

Codecov Report

Merging #6551 (72d0ed0) into develop (e4c5999) will not change coverage.
The diff coverage is 100.00%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #6551   +/-   ##
========================================
  Coverage    75.98%   75.98%           
========================================
  Files         1578     1578           
  Lines       181058   181058           
========================================
  Hits        137579   137579           
  Misses       43479    43479           
Impacted Files Coverage Δ
src/goto-cc/gcc_cmdline.cpp 74.80% <ø> (ø)
src/solvers/flattening/bv_pointers.h 100.00% <ø> (ø)
src/solvers/prop/prop_conv_solver.h 42.85% <ø> (ø)
src/solvers/refinement/bv_refinement.h 83.33% <ø> (ø)
src/solvers/flattening/arrays.h 93.75% <100.00%> (ø)
src/solvers/flattening/boolbv.h 62.50% <100.00%> (ø)
src/solvers/flattening/boolbv_quantifier.cpp 90.90% <100.00%> (ø)
src/solvers/flattening/bv_pointers.cpp 83.06% <100.00%> (ø)
src/solvers/flattening/equality.h 88.88% <100.00%> (ø)
src/solvers/lowering/functions.h 50.00% <100.00%> (ø)
... and 3 more

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 9b72a5c...72d0ed0. Read the comment docs.

@@ -35,6 +35,9 @@ class prop_conv_solvert : public conflict_providert,

virtual ~prop_conv_solvert() = default;

// non-iterative eager conversion
virtual void finish_eager_conversion();
Copy link
Collaborator

Choose a reason for hiding this comment

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

Just curious: this used to be protected. Why is making it public the right thing to do?

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, I am thinking about the use of this for an eager conversion, say to Dimacs, or something else.
Right now, we trigger the "finishing" by calling dec_solve, which then doesn't actually do solving, but returns an error, which we then ignore. It would be clearer to feed the constraints to the decision procedure, and then call finish_eager_conversion, and then be done.

@kroening kroening removed their assignment Dec 29, 2021
@kroening kroening mentioned this pull request Dec 29, 2021
5 tasks
This renames a set of solver methods from post_process to
finish_eager_conversion.  The term 'post processing' may be used either in
lazy or eager solving.  The new name clarifies that this is about an eager
conversion.
@kroening kroening force-pushed the rename_postprocessing branch from d31fcce to 72d0ed0 Compare January 4, 2022 22:50
@kroening kroening merged commit 7c44c10 into develop Jan 12, 2022
@kroening kroening deleted the rename_postprocessing branch January 12, 2022 15:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants