Deprecate has_symbol [blocks: #6727]

[tautschnig]

This code does not permit configuration what kinds of symbols are to be
found. It had a single user within the code base, and even that one was
not a good use of it for it constructed a single-element set.

• 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]

Codecov Report

Merging #6766 (ea472cb) into develop (2e306c6) will increase coverage by 0.71%.
The diff coverage is 93.78%.

@@             Coverage Diff             @@
##           develop    #6766      +/-   ##
===========================================
+ Coverage    77.04%   77.75%   +0.71%     
===========================================
  Files         1594     1568      -26     
  Lines       185276   179656    -5620     
===========================================
- Hits        142748   139698    -3050     
+ Misses       42528    39958    -2570     

Impacted Files	Coverage Δ
src/goto-instrument/cover_basic_blocks.h	100.00% <ø> (ø)
src/goto-instrument/source_lines.h	100.00% <ø> (ø)
src/solvers/smt2_incremental/object_tracking.h	100.00% <ø> (ø)
..._incremental/smt2_incremental_decision_procedure.h	75.00% <ø> (ø)
src/util/find_symbols.h	0.00% <ø> (ø)
src/goto-programs/show_properties.cpp	64.42% <47.82%> (-5.82%)	⬇️
src/goto-checker/cover_goals_report_util.cpp	90.09% <68.96%> (-8.61%)	⬇️
...t/solvers/smt2_incremental/convert_expr_to_smt.cpp	99.87% <99.23%> (-0.13%)	⬇️
...ecode/java_virtual_functions/virtual_functions.cpp	100.00% <100.00%> (ø)
src/ansi-c/goto_check_c.cpp	91.47% <100.00%> (ø)
... and 49 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 b22ded7...ea472cb. Read the comment docs.

[kroening]

BTW, there may be a benefit to have a has_symbol facility. The disadvantage of building a set, just to check if there's a particular member, is the memory allocation.

How about designing some sufficiently broad 'symbol expression predicate', which could then be both to both find symbols and do the allocation-free 'has symbol'?

(The function, as is, should indeed be deprecated, as there are too many kinds of symbols.)

[tautschnig]

BTW, there may be a benefit to have a has_symbol facility. The disadvantage of building a set, just to check if there's a particular member, is the memory allocation.

As indicated in the (updated) commit message: I intend to address the performance concern in a follow-up commit for it will be a lot easier once the various find_symbols implementations are cleaned up (as is being done in #6727).

How about designing some sufficiently broad 'symbol expression predicate', which could then be both to both find symbols and do the allocation-free 'has symbol'?

Instead of the predicate I'm now using an enum for it may be difficult for a predicate to work as it would need context.

[tautschnig]

As indicated in the (updated) commit message: I intend to address the performance concern in a follow-up commit for it will be a lot easier once the various find_symbols implementations are cleaned up (as is being done in #6727).

This improvement is now included in #6727 (commit with subject "Make find_symbols implementations uniform").

[tautschnig]

Closing as #6727 has the full story and the commit of this PR alone is not as meaningful.