[RFC] Direct CVC4 to use ALL logics

[TGWDB]

Raising this PR with "[RFC]" since this could be a discussion. Earlier ideas about using ALL were argued against due to raising unknown results, but since these appear anyway with z3 and this change allows cvc4 to solve more problems and (maybe) produce less errors this seems worth considering.

This changes CVC4 to use ALL logics when solving. This has the
advantages that:

1. We will no longer receive errors when quantified expressions
   are sent to CVC4.
2. We may now solve more problems.
   The disadvantages are:
   A. Solving may take longer in some cases when quantifiers are
   not used.
   B. CVC4 can now (more easily?) report "unknown".
   Note that due to introducing quantifiers in expressions in
   prior commits/work, reporting of unknown is now handled and can
   be achieved with z3 already.

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

[martin-cs]

I would prefer setting the logic based on the contents of the formula. Maybe even outside of the construction of the smt2_conv because some formulae will not work with some solvers and it would be good to give meaningful error messages about this. I suspect QF_ABVFP is fine for most users and ABVFP will cover most of the rest but in unusual use-cases we can produce DT, NIA, NRA, UF' and S.

[codecov]

Codecov Report

Merging #6248 (cacd7ab) into develop (0002950) will increase coverage by 8.77%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #6248      +/-   ##
===========================================
+ Coverage    67.40%   76.18%   +8.77%     
===========================================
  Files         1157     1478     +321     
  Lines        95236   161670   +66434     
===========================================
+ Hits         64197   123165   +58968     
- Misses       31039    38505    +7466     

Flag	Coverage Δ
cproversmt2	?
regression	?
unit	?

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/util/string_container.cpp	52.94% <0.00%> (-47.06%)	⬇️
src/solvers/prop/prop.cpp	42.85% <0.00%> (-41.76%)	⬇️
src/solvers/flattening/boolbv_member.cpp	53.65% <0.00%> (-38.65%)	⬇️
src/cpp/cpp_storage_spec.cpp	65.00% <0.00%> (-35.00%)	⬇️
src/util/cmdline.h	66.66% <0.00%> (-33.34%)	⬇️
src/solvers/strings/array_pool.h	66.66% <0.00%> (-33.34%)	⬇️
src/solvers/strings/string_refinement.h	66.66% <0.00%> (-33.34%)	⬇️
...rs/strings/string_concatenation_builtin_function.h	0.00% <0.00%> (-33.34%)	⬇️
src/cbmc/c_test_input_generator.cpp	60.00% <0.00%> (-30.33%)	⬇️
src/analyses/local_cfg.h	75.00% <0.00%> (-25.00%)	⬇️
... and 1458 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 7e291a5...cacd7ab. Read the comment docs.

[TGWDB]

I would prefer setting the logic based on the contents of the formula. Maybe even outside of the construction of the smt2_conv because some formulae will not work with some solvers and it would be good to give meaningful error messages about this. I suspect QF_ABVFP is fine for most users and ABVFP will cover most of the rest but in unusual use-cases we can produce DT, NIA, NRA, UF' and S.

I agree that setting the correct logic for what we actually send to the solver is the correct approach. How to achieve this is (IMHO) it's own discussion and outside the scope of this PR (although we can start it here if it's of interest?). To argue for this PR and the chosen implementation decisions:

• We pick one logic now and use it regardless of what we send. Since we're sending quantified expressions, we should pick a logic that allows them.
• Since we set solver specific parameters in smt2_conv.cpp, this is the right place to set them for cvc4. Setting only this parameter somewhere else is inconsistent, and changing how we create solvers is a much larger point.

That said, I have no (good) argument to make that setting the logic to ALL and getting unknown as a result is a "better" error message than setting the logic to QF_AUFBV and reporting errors when we send quantifiers. However, I will note that there are examples (and I can probably dig one up if it's helpful) where using ALL can achieve a verification result (i.e. not error) but we have an error due to sending quantifiers if we don't change the logic.

[martin-cs]

If you have all the formula before you start adding things to the solver (which, in CBMC, you can do) then setting the logic correctly is not hard. Walk the formula and...

auto t = expr.type();
if (can_cast_type<bitvector_typet>(t)) {
  if (t.id() == ID_float_bv)) {
    add_to_logic(FP);
  } else {
    add_to_logic(BV);
  }
} else if (can_cast_type<array_typet>(t)) {
    add_to_logic(A);
} else if (can_cast_type<string_typet>(t)) {
    add_to_logic(S);
} else if (can_cast_type<array_typet>(t)) {
    add_to_logic(A);
} else if (t.id() == ID_integer) {
    if (expr.id() == ID_mult || expr.id() == ID_div || ...) {  // Maybe check for the multiply-by-consts special case
      add_to_logic(NIA);
    } else {
      add_to_logic(LIA);  // NIA must over-ride this
    }
} else if (t.id() == ID_real || t.id() == ID_rational) {
    // Same with NRA and LRA
} else if () {
    // Check for UF or maybe just add it along with A as a base
}

if (can_cast_expr<quantifier_exprt>(expr) {
  add_to_logic(Q);
}

[TGWDB]

If you have all the formula before you start adding things to the solver (which, in CBMC, you can do) then setting the logic correctly is not hard. Walk the formula and...

This requires some changes to how the conversion is done at the moment. Right now the logic is chosen and output before any of the formula is examined or converted. Not to disagree with the idea, but just to mentioned that this PR was aiming for a quick fix that solves some small issues.

[peterschrammel]

Fine with that for now if it solves a concrete issue.