Basic CHC Encoding

[kroening]

• 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

Merging #6807 (8a1533b) into develop (e46d2f3) will increase coverage by 0.00%.
The diff coverage is 72.70%.

❗ Current head 8a1533b differs from pull request most recent head da2d84f. Consider uploading reports for the commit da2d84f to get more accurate results

@@            Coverage Diff            @@
##           develop    #6807    +/-   ##
=========================================
  Coverage    77.01%   77.01%            
=========================================
  Files         1594     1594            
  Lines       184436   184954   +518     
=========================================
+ Hits        142038   142438   +400     
- Misses       42398    42516   +118     

Impacted Files	Coverage Δ
src/util/pointer_expr.h	87.83% <ø> (+3.19%)	⬆️
src/goto-instrument/horn_encoding.cpp	72.27% <72.22%> (+72.27%)	⬆️
.../goto-instrument/goto_instrument_parse_options.cpp	70.00% <100.00%> (+0.60%)	⬆️
src/util/mathematical_expr.h	89.56% <100.00%> (+0.78%)	⬆️
src/util/pointer_expr.cpp	81.55% <100.00%> (+6.80%)	⬆️

---

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 e46d2f3...da2d84f. Read the comment docs.

[tautschnig]

1. I'm fine with the first two commits (those adding new constructors).
2. I find "substitute_symbols" very confusing as we already have "replace_symbolt". Merriam-Webster says "replace" and "substitute" are synonyms.
3. I don't have the necessary background to comment on the CHC encoder, but not having any tests does not seem appropriate.

[kroening]

2. The key difference is that the subsitute_symbols does consider bindings. This is needed in most cases, but too much of a change to do to replace_symbols.

[kroening]

3. Now with tests.

[tautschnig]

3. Now with tests.

Thank you!

[tautschnig]

2. The key difference is that the subsitute_symbols does consider bindings. This is needed in most cases, but too much of a change to do to replace_symbols.

It may well be that having two separate implementations is the right thing to have, but then their names need to be sufficiently clear to avoid any confusion.

Also, I would expect the new code to handle all binding_exprt (it's missing array_comprehension_exprt - with #6810 one could just use if(can_cast_expr<binding_exprt>(...) or expr_try_dynamic_cast<binding_exprt> to avoid this problem), and the existing code in std_expr.cpp to be removed.

[kroening]

'substitute' is the common term for replacing a variable by an expression; 'replace' is the unusual one. We will likely gradually replace (uh) 'replace_symbol' by 'substitute_symbol', since we need that awareness of bindings.

https://en.wikipedia.org/wiki/Substitution_(logic)

I've added the array_comprehension case.

[tautschnig]

'substitute' is the common term for replacing a variable by an expression; 'replace' is the unusual one. We will likely gradually replace (uh) 'replace_symbol' by 'substitute_symbol', since we need that awareness of bindings.

https://en.wikipedia.org/wiki/Substitution_(logic)

But then the current state of affairs is that we have address_of_exprt, which replace_symbolt gets right, but substitute_symbol does not. At the same time, replace_symbolt does not know about bound symbols when substitute_symbol does. We, therefore, have two implementations the names of which are synonyms, their features are orthogonal, and neither of them really works on the current code base.

I've added the array_comprehension case.

Thank you!

[kroening]

Right, we'll need to manage the transition.
How about adding binding-awareness to replace_symbol(...)?

[tautschnig]

Right, we'll need to manage the transition. How about adding binding-awareness to replace_symbol(...)?

This would help avoid confusion, and then we could still introduce a (thin) wrapper substitute_symbol with the API proposed in this PR that just uses replace_symbol under the hood? That wrapper would, among other things, help fix up terminology.

[kroening]

No, we want to get rid of replace_symbol in the longer term -- so that should be a wrapper around substitute_symbol.

[kroening]

@tautschnig -- shall we go for that?

[kroening]

Now without the offending commit.

[peterschrammel]

📖 A bit of documentation would be helpful for the next reader.