Add CVC5 Parsing Support #540

baierd · 2025-10-28T15:59:38Z

This PR adds support for parsing to CVC5.

Should only be merged after PR539.

…erm, as it creates new distinct terms when parsing

…ier parsing)

…d precondition about named terms (as they are currently not handled)

…code more readable

… to register their free counterparts

…as not every solver can do that!) for int and bv arrays

…nor modifications from 0d463c8

baierd · 2025-10-28T20:31:22Z

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.

…char when defining expressions and re-substitute the terms later on (only works for Mathsat most likely, but no other solver returns something like this!)

baierd · 2025-10-29T08:14:23Z

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.

…check this error + improve dumping by properly using function return and input types for our smtlib2 output

…needed (UFs fail for double declaration, variables actually work) and only declare UFs once, even if used multiple times, when dumping

…ables and UFs are not allowed to be defined twice)

…-const before adding them to the input if known already

…tionsTest.java

…ntry as checkstyle thinks WRONGLY that we use only the keys

daniel-raffler

Looks good so far! Some of the preprocessing could be simplified by using the Tokenizer as was done in #474

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java

…rom internal output before adding to the input

…allows symbols to be parsed multiple times

…re lenient parsing, reuse symbols etc. and remove all imprecise SMTLIB2 insertions and now unneeded methods

…m terms

baierd · 2025-11-02T11:18:22Z

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.

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java

baierd · 2025-11-02T13:04:54Z

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 · 2025-11-02T13:55:08Z

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.

baierd

Note: this has PR 539 already merged in. It makes sense to review PR 539 first.

BaierD added 15 commits October 27, 2025 19:24

Add incomplete (crude) implementation for CVC5 parser

fc74781

Enable CVC5 parser tests

2fa2ea6

Disable a slow test for CVC5

a5a90b7

CVC5 parser: add substitution to known (cached) terms for the final t…

844b362

…erm, as it creates new distinct terms when parsing

CVC5 parser: add some assertions before substituting terms at the end

3b58ca2

CVC5 parser: add UF parsing with additional assertions (TODO: Quantif…

025f97a

…ier parsing)

CVC5 parser: add info about quantifier/bound variable handling and ad…

71dee39

…d precondition about named terms (as they are currently not handled)

CVC5 parser: refactor UF handling and unpack applied UFs before caching

13e130d

CVC5: improve retrieval method for free vars from cache for bound vars

69cafaf

CVC5: only use static imports for the 3 precondition methods to make …

95d1de5

…code more readable

CVC5: refactor return in creator method getFreeVariableFromCache()

da72300

CVC5: use a custom visitor to visit all bound variables after parsing…

4900b2f

… to register their free counterparts

Add tests for multi-dimensional arrays not based on parsing SMTLIB2 (…

55e572e

…as not every solver can do that!) for int and bv arrays

CVC5 parser: apply checkstyle suggestion

d13c807

CVC5 Model: add improved array evaluation from Daniel Raffler with mi…

df00d8d

…nor modifications from 0d463c8

baierd self-assigned this Oct 28, 2025

baierd added this to the Release 6.0.0 milestone Oct 28, 2025

baierd added enhancement CVC5 labels Oct 28, 2025

BaierD added 5 commits October 28, 2025 17:02

Merge branch 'fix_cvc5_array_model' into use_new_cvc5_parser

20be8ed

CVC5 Parser: clean up error messages and add more doc for them

c7f8be3

CVC5 Model: format

fd562b3

Merge branch 'fix_cvc5_array_model' into use_new_cvc5_parser

d8f934a

CVC5 parser: improve doc location and text for an error

8cbd003

CVC5 parser: replace all expressions using dot (e.g .def_ ) as first …

d56b3e9

…char when defining expressions and re-substitute the terms later on (only works for Mathsat most likely, but no other solver returns something like this!)

baierd requested review from daniel-raffler and kfriedberger October 28, 2025 20:58

CVC5 parser: use substring method with less arguments

de7bddd

BaierD added 11 commits October 29, 2025 17:01

CVC5: add creator method to get all cached variables and UFs

0591f8e

CVC5: allow parsing to skip double declarations and add constants to …

3db56cf

…check this error + improve dumping by properly using function return and input types for our smtlib2 output

CVC5 parser: only add declarations from the cache if they are really …

37cab0d

…needed (UFs fail for double declaration, variables actually work) and only declare UFs once, even if used multiple times, when dumping

CVC5: add CVC5 to more strict test category for parsing test

3b3b1e7

CVC5: move newly added set of internal UF names and add doc

2689404

CVC5: refactor parsing to be more readable and understandable

686ef7f

CVC5 parser: remove allowed invoke error msg, as it fails later (vari…

ad5ab63

…ables and UFs are not allowed to be defined twice)

CVC5 parser: also check for present declarations present with declare…

3ae018b

…-const before adding them to the input if known already

CVC5 parser: add to more strict test branch in SolverFormulaIODeclara…

93c5582

…tionsTest.java

Use (_.getKey(), _.getValue()) when building new map instead of the e…

c7b57bd

…ntry as checkstyle thinks WRONGLY that we use only the keys

Simplify usage of stream in CVC5FormulaManager.java

3d0c1e5

daniel-raffler requested changes Oct 30, 2025

View reviewed changes

BaierD added 9 commits October 31, 2025 20:56

CVC5 Parser: don't use replace(), but substring() to remove newline f…

0e114e3

…rom internal output before adding to the input

CVC5 Parser: improve named term TODO w infos from Daniel Raffler

3651299

CVC5 Parser: remove unneeded check for push/pop and add a note instead

7ec9162

CVC5 Parser: switch parser tests for CVC5 into lenient category that …

0e1e957

…allows symbols to be parsed multiple times

CVC5 Parser: rework implementation by using CVC5s options to allow mo…

d77198f

…re lenient parsing, reuse symbols etc. and remove all imprecise SMTLIB2 insertions and now unneeded methods

CVC5FormulaManager reorder methods

bb41939

CVC5FormulaCreator clean up unused methods and consts

98ff665

CVC5FormulaManager simplify used methods and doc

a94d613

CVC5FormulaManager improve JavaDoc for generation of declarations fro…

43a2413

…m terms

baierd changed the title ~~Draft: Add CVC5 Parsing Support~~ Add CVC5 Parsing Support Nov 1, 2025

daniel-raffler reviewed Nov 2, 2025

View reviewed changes

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java Show resolved Hide resolved

CVC5 parser: add more doc for options used

55de80f

daniel-raffler reviewed Nov 2, 2025

View reviewed changes

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java Show resolved Hide resolved

CVC5 parser: make JavaDoc of parser creation more descriptive

b8b6483

baierd commented Nov 4, 2025

View reviewed changes

Add CVC5 Parsing Support #540

Are you sure you want to change the base?

Add CVC5 Parsing Support #540

Uh oh!

Conversation

baierd commented Oct 28, 2025

Uh oh!

baierd commented Oct 28, 2025

Uh oh!

baierd commented Oct 29, 2025

Uh oh!

daniel-raffler left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

baierd commented Nov 2, 2025

Uh oh!

Uh oh!

Uh oh!

baierd commented Nov 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

baierd commented Nov 2, 2025

Uh oh!

baierd left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

2 participants

baierd commented Nov 2, 2025 •

edited

Loading