293 cvc5 interpolation

[RSoegtrop]

Implements CVC5 Interpolation, following the Definition of Craig-Interpolation.

[RSoegtrop]

I needed to disable following Tests because CVC5s getInterpolant did not terminate:

• InterpolatingProverTest

  • simpleInterpolation
  • bigSeqInterpolationTest

• SolverFormulaWithAssumptionsTest:

  • basicAssumptionsTest

[baierd]

So there is 1 test failing iff the internal assertions of getInterpolant() for CVC5 are active. To be concrete, its only this line assert solverP.checkSat().isSat() : "Interpolant does not follow Craig Interpolation"; thats problematic. If you comment out this line, the test runs fine.
My suggestion is to disable this line for now, extract the problem and send it to the CVC5 devs.

[kfriedberger]

From my side, the code looks valid, under the assumption that CVC5 provides valid interpolants.
PR approved!

Future work:

• Some unit tests should be analyzed in detail whether CVC5 can be improved.
• Testing of interpolation on larger SMT queries should be done, e.g., within CPAchecker with predicate analysis or impact algorithm.

[kfriedberger]

I published a preliminary development-version of JavaSMT including PR (CVC5-interpolation) into Ivy. It is available with version 4.0.3-59-g6a56e821. For testing, it can be added as dependency into CPAchecker (simply change the version number in CPAchecker's lib/ivy.xml and build CPAchecker).

A first look at benchmark results from SV-COMP shows some solved files with CVC5 and predicate analysis, but there is room for improvement. The JavaSMT-bindings from this PR seem to work well.

[kfriedberger]

I did a quick benchmark on predicate analysis with CPAchecker, with integer-based formula-encoding (no bitvectors!).

Result are here:

• all files: https://www.cip.ifi.lmu.de/~friedber/CPAchecker/cvc5interpolation/
• main table: https://www.cip.ifi.lmu.de/~friedber/CPAchecker/cvc5interpolation/results.2023-09-03_13-33-23.table.html

The interesting thing might be the quantile plot:

In short:
CVC5 provides some useful interpolants, but fails on several tasks, such that there are less false results (plot-line starts not as far left as other solvers) and there are less solved tasks (plot-line does not reach as far to the right as other solvers).

There are several cases where the analysis reports a repeated counterexample path when using CVC5. This might be caused by invalid interpolants and needs to be checked in detail.
For example:

• file: bitvector/byte_add-1.yml
• command line: scripts/cpa.sh -heap 13000M -noout -benchmark -stack 50M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop counterexample.export.allowImpreciseCounterexamples=true -predicateAnalysis -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop solver.solver=CVC5 -timelimit 900s -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 ../sv-benchmarks/c/bitvector/byte_add-1.i
• error in the log: Error: Refinement failed: Counterexample could not be ruled out and was found again

[kfriedberger]

Analysis of a problematic task from last benchmark execution, including a comparison of MathSAT5 and CVC5

I used the following example, because the input file is quite short and simple:

scripts/cpa.sh -predicateAnalysis \
    -setprop cpa.predicate.encodeBitvectorAs=INTEGER \
    -setprop solver.solver=CVC5 -stats \
    -spec ../sv-benchmarks/c/properties/unreach-call.prp -32 \
    ../sv-benchmarks/c/loop-new/count_by_1.i

The refinement failed error comes from repeated counterexamples and is caused by invalid interpolant sequences in CPAchecker.

A specific interpolation query was suspicious, coming from three input formulas. The query appears when unroling the loop in the program once. Shorted/simplified formulas given here (see unit test added in 7a1676e):

• 0: i3=0
• 1: i3<1000 & i4=i3+1
• 2: i4>1000

CPAchecker (especially predicate analysis) requires sequential interpolants for the refinement. For the given formulas, the interpolation query should be [0]/[1]/[2] (three partitions resulting in two interpolants). The default interpolation strategy of CPAchecker does not query such interpolants (due to historic reasons), but queries two interpolants for [0]/[1,2] and [0,1]/[2].

For those two queries, MathSAT5 produces i3<=0 und i4<=1. CVC5 produces true und i4=1. While the response from MathSAT5 is a valid sequence of interpolant, the response from CVC5 is not. The reason is the new internal proof that is used by CVC5 to generate interpolants.

In general, querying individual interpolants from a sequence of formulas is not the best way to go (nicely documented nearly 7 years ago), and CPAchecker has already an option, such that the problematic query is avoided: cpa.predicate.refinement.strategy=SEQ (instead of SEQ_CPACHECKER.

New benchmark results

A new benchmark show better results and avoids this problem:

• table (CVC5 with interpolation strategy, SEQ_CPACHECKER vs. SEQ vs. SEQ mit Bugfix fba562e): https://www.cip.ifi.lmu.de/~friedber/CPAchecker/cvc5interpolation/results.2023-09-11_07-52-56.table.html#/
• main table (updated): https://www.cip.ifi.lmu.de/~friedber/CPAchecker/cvc5interpolation/results.2023-09-11_07-52-10.table.html#/

The latest data of CVC5 is "dark-blue".

However CVC5 still has some other issues with interpolation:

• exception about formulas of invalid formula type: CVC5ApiException: expecting a Boolean subexpression (fixed with fba562e and already included in the latest benchmark)
• exception about UF-usage in interpolation: CVC5ApiException: Function terms are only supported with higher-order logic. Try adding the logic prefix HO_. (changed or new option required?)
• several timeouts on quite simple files (optimization required)

Those problems might not be within the scope of this PR.

[kfriedberger]

Is there anything left to do before merging? I would like to merge this PR soon.