Adding large-step encoding for CHCs in CProver (no [required] changes to the solver) #8465
Conversation
yvizel
commented
Sep 22, 2024
yvizel
commented
- 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).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
yvizel
requested review from
kroening,
tautschnig and
peterschrammel
as code owners
There was a problem hiding this comment.
A bunch of comments that each apply in several more places. More generally, however, it would be great to have comments. At bare minimum there should be high-level design comments in some place that explain how the various pieces fit together. Also, we need tests that demonstrate the new feature.
| "(verbose)" | ||
|
|
||
|
|
There was a problem hiding this comment.
Nit pick: no need for extra blank line.
|
|
||
| #include "chc_db.h" | ||
|
|
||
| #include <iostream> |
There was a problem hiding this comment.
Is this a debugging left-over?
|
|
||
| for (auto & sp : m_db.get_state_preds()) | ||
| { | ||
| std::set<exprt> outgoing; |
There was a problem hiding this comment.
Only use std::set when ordering is important or needs to be stable, else use std::unordered_set.
| continue; | ||
| } | ||
| exprt func = to_function_application_expr(*r.head()).function(); | ||
| m_head_idx[func].insert(&r); |
There was a problem hiding this comment.
Please refrain from storing pointers into other data structures, this is prone to break (the code here really requires that m_clauses will never change once build_indices has been called. Either make copying cheap (like irept does), or else store the index into m_clauses (so that m_clauses can still be added to).
| m_head_idx[func].insert(&r); | ||
|
|
||
| std::vector<symbol_exprt> use; | ||
| r.used_relations(*this,std::back_inserter(use)); |
There was a problem hiding this comment.
I'd suggest that used_relations just return a std::vector<symbol_exprt> (which is cheap with copy elision).
|
|
||
| class cutpoint | ||
| { | ||
| friend class cutpoint_graph; |
There was a problem hiding this comment.
Why do we need friendhere?
| friend class cutpoint_graph; | ||
|
|
||
| const cutpoint_graph &m_graph; | ||
| unsigned m_id; |
There was a problem hiding this comment.
unsigned will hardly ever be the right type. Should it perhaps be std::size_t?
| const goto_programt::instructiont & m_inst; | ||
|
|
||
| typedef std::vector<cutpoint_edge_ptr> EdgeVec; | ||
| EdgeVec m_succ; |
There was a problem hiding this comment.
Use snake_case rather than CamelCase.
