Separate file for Makefile based building of smt2_incremental directory

[thomasspriggs]

So that the .cpp files for incremental SMT2 solving can be
added/removed/renamed without triggering codeowner review of the
src/solvers directory.

• 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 #6415 (b00d8be) into develop (c4deb56) will increase coverage by 0.00%.
The diff coverage is 93.00%.

@@           Coverage Diff            @@
##           develop    #6415   +/-   ##
========================================
  Coverage    75.98%   75.99%           
========================================
  Files         1524     1524           
  Lines       164244   164280   +36     
========================================
+ Hits        124809   124845   +36     
  Misses       39435    39435           

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.cpp	66.31% <89.47%> (+0.22%)	⬆️
jbmc/src/java_bytecode/java_entry_point.cpp	89.52% <92.42%> (+0.16%)	⬆️
src/solvers/flattening/bv_pointers.cpp	82.88% <100.00%> (+0.32%)	⬆️
src/util/simplify_expr_int.cpp	84.21% <100.00%> (+0.06%)	⬆️

---

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 9892924...b00d8be. Read the comment docs.

[tautschnig]

If CODEOWNERS is what we're worried about, can't we just amend CODEOWNERS instead and list src/solvers/Makefile in there?

[thomasspriggs]

If CODEOWNERS is what we're worried about, can't we just amend CODEOWNERS instead and list src/solvers/Makefile in there?

That would also work. However it would grant code ownership to those listed against it for making build system changes for the other solvers. It would also mean keeping an additional list of people up to date in the CODEOWNERS file, rather than tying the list of people who can change what files are built for the smt2_incremental directory precisely to those who have code ownership of that directory.

[tautschnig]

That would also work. However it would grant code ownership to those listed against it for making build system changes for the other solvers. It would also mean keeping an additional list of people up to date in the CODEOWNERS file, rather than tying the list of people who can change what files are built for the smt2_incremental directory precisely to those who have code ownership of that directory.

I accept that there's some bureaucratic overhead in this, but then at least we're doing bureaucracy where bureaucracy belongs. Working around bureaucracy via a one-off Makefile hack is, well, a workaround. (And I'm not worried about granting code ownership to too many people on this occasion.)

An alternative fix is to introduce Makefiles for each subdirectory in solvers instead of this single big one. But then we should do this properly for all subdirectories.

[thomasspriggs]

This has been superseded by the codeowners change PR which has been merged.