[Refactor] New SMT backend: Remove X-macro implementation from smt_bit_vector_theory

[NlightNFotis]

Hello,

The aim of this PR is to provide some structural changes and fixes to some issues identified
in the new SMT backend we have been working on for some time.

More explicitly:

• Remove the X-macro based implementation of relational operators in the smt_bit_vector_theory, so that the implementation is consistent with the approach taken for the arithmetic operators.

Attention:

This PR has been based on #6614 and assumes that gets in first. As such, some of the earlier commits here don't correspond to the scope of the work being done.

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

[codecov]

Codecov Report

Merging #6615 (290f022) into develop (57e7b2c) will increase coverage by 0.05%.
The diff coverage is 100.00%.

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

@@             Coverage Diff             @@
##           develop    #6615      +/-   ##
===========================================
+ Coverage    76.65%   76.71%   +0.05%     
===========================================
  Files         1579     1577       -2     
  Lines       181294   181503     +209     
===========================================
+ Hits        138973   139232     +259     
+ Misses       42321    42271      -50     

Impacted Files	Coverage Δ
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	48.99% <100.00%> (+12.26%)	⬆️
...solvers/smt2_incremental/smt_bit_vector_theory.cpp	100.00% <100.00%> (ø)
...t/solvers/smt2_incremental/convert_expr_to_smt.cpp	100.00% <100.00%> (ø)
...solvers/smt2_incremental/smt_bit_vector_theory.cpp	100.00% <100.00%> (ø)
src/util/exception_utils.cpp	90.56% <0.00%> (-3.78%)	⬇️
src/goto-programs/initialize_goto_model.cpp	83.13% <0.00%> (-2.41%)	⬇️
src/util/bitvector_expr.cpp	93.93% <0.00%> (-0.66%)	⬇️
src/util/bitvector_expr.h	92.60% <0.00%> (-0.40%)	⬇️
src/util/simplify_expr_int.cpp	84.86% <0.00%> (-0.23%)	⬇️
src/solvers/flattening/boolbv.cpp	80.39% <0.00%> (-0.12%)	⬇️
... and 10 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 637f138...8e9a74a. Read the comment docs.

[thomasspriggs]

A few nit picks -

• I would have separated the final removal of the .def and macro definitions into a separate commits, given that you already separated each of the individual operations.
• Using the word "Remove" in the commit title misses the point of what the commits are doing. They are refactoring the implementation to not use macros, not removing functionality.
• Needs the clang-format / linting failure fixing.

This all looks fine otherwise.