Add CVC5 Parsing Support

[baierd]

This PR adds support for parsing to CVC5.

Should only be merged after PR539.

[baierd]

The last remaining problem is that MathSAT5 output can't be parsed in general, as MathSAT5 splits up the query and uses a . in the beginning of its intermediate variables, e.g.:

(set-info :source |printed by MathSAT|)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun q () Bool)
(declare-fun u () Bool)
(define-fun .def_15 () Int (* (- 1) c))
(define-fun .def_16 () Int (+ b .def_15))
(define-fun .def_17 () Int (+ a .def_16))
(define-fun .def_19 () Bool (= .def_17 0))
(define-fun .def_27 () Bool (= .def_19 q))
(define-fun .def_28 () Bool (not .def_27))
(define-fun .def_23 () Bool (<= b a))
(define-fun .def_29 () Bool (and .def_23 .def_28))
(define-fun .def_11 () Bool (= a b))
(define-fun .def_34 () Bool (and .def_11 .def_29))
(define-fun .def_30 () Bool (or u .def_29))
(define-fun .def_31 () Bool (and q .def_30))
(define-fun .def_35 () Bool (and .def_31 .def_34))
(assert .def_35)

We should ask the CVC5 devs to allow this, and or add a re-substitution procedure.

[baierd]

The last remaining problem is that MathSAT5 output can't be parsed in general, as MathSAT5 splits up the query and uses a . in the beginning of its intermediate variables, e.g.:

(set-info :source |printed by MathSAT|)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun q () Bool)
(declare-fun u () Bool)
(define-fun .def_15 () Int (* (- 1) c))
(define-fun .def_16 () Int (+ b .def_15))
(define-fun .def_17 () Int (+ a .def_16))
(define-fun .def_19 () Bool (= .def_17 0))
(define-fun .def_27 () Bool (= .def_19 q))
(define-fun .def_28 () Bool (not .def_27))
(define-fun .def_23 () Bool (<= b a))
(define-fun .def_29 () Bool (and .def_23 .def_28))
(define-fun .def_11 () Bool (= a b))
(define-fun .def_34 () Bool (and .def_11 .def_29))
(define-fun .def_30 () Bool (or u .def_29))
(define-fun .def_31 () Bool (and q .def_30))
(define-fun .def_35 () Bool (and .def_31 .def_34))
(assert .def_35)

We should ask the CVC5 devs to allow this, and or add a re-substitution procedure.

I've now added a re-substitution for MathSAT5s output. Still, we should look into either modifying the output of MathSAT, ask the MathSAT devs to change this, use the alternative dump function of MathSAT, or ask the CVC5 devs to allow this.

[baierd]

I started some experiments to see how well MathSAT and Bitwuzla output works with CVC5. I can also start Z3 once we know how that went.

[baierd]

I started some experiments to see how well MathSAT and Bitwuzla output works with CVC5. I can also start Z3 once we know how that went.

Results show only a few parsing related errors (but not all that much has been parsed): results.2025-11-02_13-29-47.table.html cvc5Parser.integration-imc.2025-11-02_13-00-50.logfiles.zip

The main problem is the missing FP to IEEE-BV support for CVC5 in general. (See PR 514). With an additional complication in the parser for this operation (e.g. for MathSAT5 to CVC5):

Exception in thread "main" java.lang.IllegalArgumentException: Error parsing with CVC5: Symbol 'fp.as_ieee_bv' not declared as a variable
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5FormulaManager.parseCVC5(CVC5FormulaManager.java:164)
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5FormulaManager.parseImpl(CVC5FormulaManager.java:88)
	at org.sosy_lab.java_smt.solvers.cvc5.CVC5FormulaManager.parseImpl(CVC5FormulaManager.java:38)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.parse(AbstractFormulaManager.java:330)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.translateFrom(AbstractFormulaManager.java:488)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.translateFrom(FormulaManagerView.java:1907)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.SeparateInterpolatingProverEnvironment.convertToItp(SeparateInterpolatingProverEnvironment.java:122)

Commandline to trigger: bin/cpachecker --no-output-files --heap 2000M --bmc-interpolation --option imc.fallBack=false --option solver.solver=MATHSAT5 --option solver.interpolationSolver=CVC5 --option cpa.predicate.memoryAllocationsAlwaysSucceed=true --timelimit 60s --stats --spec test/programs/benchmarks/properties/unreach-call.prp --32 test/programs/benchmarks/float-benchs/inv_Newton.c.p+cfa-reducer.c

Triggering SMTLIB2: cvc5.parse.fp_to_bv.smt2.txt (Remove the .txt at the end!)

Another problem is that some symbols are still parsed multiple times:

Exception in thread "main" java.lang.IllegalArgumentException: <string>:11:14: symbol '|main::nondet@3|' already defined at line 2 column 14
	at org.sosy_lab.java_smt.solvers.bitwuzla.api.BitwuzlaNativeJNI.Parser_parse__SWIG_0(Native Method)
	at org.sosy_lab.java_smt.solvers.bitwuzla.api.Parser.parse(Unknown Source)
	at org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaFormulaManager.parseImpl(BitwuzlaFormulaManager.java:126)
	at org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaFormulaManager.parseImpl(BitwuzlaFormulaManager.java:28)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.parse(AbstractFormulaManager.java:330)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.translateFrom(AbstractFormulaManager.java:488)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.translateFrom(FormulaManagerView.java:1907)

SMTLIB2: cvc5.parse.extra.variable.smt2.txt (Remove the .txt at the end!)

[baierd]

Note: the second parsing problem is a Bitwuzla problem ;D I opened a issue.

Seems like the parser works besides the FP to IEEE BV issue. We can tackle that later, as we might have to contact the devs for this. I opened a issue for this.

@kfriedberger this is now ready for review.