Solver submission: cvc5 #64

hansjoergschurr · 2024-05-27T19:46:01Z

Thank you for running the competition.

github-actions · 2024-05-27T19:46:37Z

Summary of modified submissions

cvc5

15 authors
website: https://cvc5.github.io/
Participations
- UnsatCore
  - Arith
    - all
  - Bitvec
    - all
  - Equality
    - all
  - Equality+LinearArith
    - all
  - Equality+MachineArith
    - all
  - Equality+NonLinearArith
    - all
  - FPArith
    - all
  - QF_Bitvec
    - all
  - QF_Datatypes
    - all
  - QF_Equality
    - all
  - QF_Equality+Bitvec
    - all
  - QF_Equality+LinearArith
    - all
  - QF_Equality+NonLinearArith
    - all
  - QF_FPArith
    - all
  - QF_LinearIntArith
    - all
  - QF_LinearRealArith
    - all
  - QF_NonLinearIntArith
    - all
  - QF_NonLinearRealArith
    - all
  - QF_Strings
    - all
- SingleQuery
  - Arith
    - all
  - Bitvec
    - all
  - Equality
    - all
  - Equality+LinearArith
    - all
  - Equality+MachineArith
    - all
  - Equality+NonLinearArith
    - all
  - FPArith
    - all
  - QF_Bitvec
    - all
  - QF_Datatypes
    - all
  - QF_Equality
    - all
  - QF_Equality+Bitvec
    - all
  - QF_Equality+LinearArith
    - all
  - QF_Equality+NonLinearArith
    - all
  - QF_FPArith
    - all
  - QF_LinearIntArith
    - all
  - QF_LinearRealArith
    - all
  - QF_NonLinearIntArith
    - all
  - QF_NonLinearRealArith
    - all
  - QF_Strings
    - all
- ModelValidation
  - QF_ADT+BitVec
    - all
  - QF_ADT+LinArith
    - all
  - QF_Bitvec
    - all
  - QF_Datatypes
    - all
  - QF_Equality
    - all
  - QF_Equality+Bitvec
    - all
  - QF_Equality+LinearArith
    - all
  - QF_Equality+NonLinearArith
    - all
  - QF_FPArith
    - all
  - QF_LinearIntArith
    - all
  - QF_LinearRealArith
    - all
  - QF_NonLinearIntArith
    - all
  - QF_NonLinearRealArith
    - all
- Incremental
  - Arith
    - all
  - Bitvec
    - all
  - Equality
    - all
  - Equality+LinearArith
    - all
  - Equality+MachineArith
    - all
  - Equality+NonLinearArith
    - all
  - FPArith
    - all
  - QF_Bitvec
    - all
  - QF_Equality
    - all
  - QF_Equality+Bitvec
    - all
  - QF_Equality+Bitvec+Arith
    - all
  - QF_Equality+LinearArith
    - all
  - QF_Equality+NonLinearArith
    - all
  - QF_FPArith
    - all
  - QF_LinearIntArith
    - all
  - QF_LinearRealArith
    - all
  - QF_NonLinearIntArith
    - all

bobot · 2024-05-31T13:21:08Z

Can you take a look at the incremental prover, it seems to answer unknown for trivial benchmarks? (The trivial benchmarks for incremental track are perhaps too trivial). You can download the tested artifact at the bottom of https://github.com/SMT-COMP/smt-comp.github.io/actions/runs/9318591743 .

hansjoergschurr · 2024-05-31T17:07:39Z

The script for the incremental track does not expect the benchmark to given by filename, but to be written to stdin by the trace executor.
However, when I take a look at unpack/8419bf673461e61631e85a1811bc572ddd71e50d7549ec35088e17e800298170/bin/starexec_run_default in the test artifact, I get the impression that the called command is simply our starexec_run_default script, not a wrapper around the trace executor.

hansjoergschurr · 2024-05-31T20:39:08Z

Thanks to this issue, however, I noticed that I gave the wrong command for the incremental track. I updated that now.

bobot · 2024-06-04T07:29:05Z

Oh yes thank you I forgot that part, the TestSolver need improvement for incremental track.

hansjoergschurr · 2024-06-05T19:07:42Z

I removed the cloud track from this pull request, since there is now a dedicated pull request for the cloud track: #84

#84: Create cvc5-cloud #74: Draft STP submission #70: draft yicesQS submission #68: Create STP-CNFLS #66: Yices2 SMTCOMP 2024 Submission #65: Z3-alpha draft PR #64: Solver submission: cvc5 #63: submission iProver #61: OSTRICH 1.4 #60: SMT-RAT submission #57: Amaya's submission for SMT-COMP 2024 #55: plat-smt submission #54: Add 2024 Bitwuzla submission. #53: 2024 solver participant submission: OpenSMT #52: Z3-Noodler submission #51: Submission Colibri #45: Submission for smtinterpol #42: Adding Algaroba to SMTCOMP 2024

martinjonas · 2024-06-10T21:55:10Z

@hansjoergschurr We have executed the latest version of cvc5 on a randomly chosen subset of 20 single-query benchmarks from each logic where it participates. The benchmarks are also scrambled by the competition scrambler (with seed 1). You can find the results here: https://www.fi.muni.cz/~xjonas/smtcomp/cvc5.table.html#/table

Quick explanation:

Green status means that the result agrees with the (set-info :status _) annotation from the benchmark.
Blue status means that the benchmark has annotation (set-info :status unknown).
By clicking on the result (e.g. false, true, ABORTED, …) you can see the command-line arguments with which your solver was called and its output on the benchmark.
By clicking on the benchmark name (i.e., *scrambled*.yml), you can see the details of the benchmark including its contents (by clicking on the file link in input_files) and the name of the original bennchmark before scrambling (e.g., # original_files: 'non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/583_ph7.smt2').

Please check whether there are some discrepancies, such as missing/extra logics, unexpected aborts or unknowns, and similar. If you update the solver, let me know and I can execute further test runs. We still have plenty of time for several follow-up test runs.

martinjonas · 2024-06-12T08:42:22Z

@hansjoergschurr Here are also results of the test run on a small subset of incremental benchmarks: https://www.fi.muni.cz/~xjonas/smtcomp/cvc5_inc.table.html#/table

The status column has the following meaning:

DONE (X correct): the solver terminated successfully and correctly decided X (check-sat) queries before that.
SOMETHING_ELSE (X correct) (e.g., TIMEOUT (10 correct) or ABORTED (10 correct)): The solver did not terminate successfully, but correctly decided X (check-sat) queries before it crashed or was killed.
WRONG: There was at least one answer to (check-sat) that did not agree with the status specified in the benchmark.

Again, if there are discrepancies (missing/extra logics, unexpected results), please let me know.

martinjonas · 2024-06-13T10:12:44Z

@hansjoergschurr We have finished test runs of model-validation and unsat-core generation tracks. You can find the results here:

As before, you can click on the status of the benchmark to see the output of your solver. If you find any discrepancies or extra/missing logics, please let me know.

Note that we selected only SAT benchmarks for model validation and only UNSAT for unsat-core generation. As a result of that, some logics do not contain any benchmarks. So do not be surprised if you have subscribed to one of these logics and you do not have any result for it. In particular, the logics are:

For model-generation: QF_UFFP, QF_UFBVDT, QF_UFDTNIA, QF_NIRA.

For unsat-core: UFBVDT, FPLRA, QF_AUFBVFP, QF_ABVFPLRA, QF_UFBVDT, QF_UFDTNIA, QF_UFDT, QF_NIA, QF_SNIA.

hansjoergschurr · 2024-06-13T23:51:43Z

Thank you for running the tests. The interface is really convenient to use.

The json file now contains links to the Zenodo record.

bobot · 2024-06-14T08:48:35Z

In the test run the checking of some model using dolmen failed
cvc5.zip.

It is mainly non-standardized part:

How to write algebraic number
How to define, the undefined values of a selector

For scrambled158502.rsmt2, the problem is that a symbol is defined using a symbol defined later. I think it is not compliant with the standard but I'm not sure (@Gbury?).

Gbury · 2024-06-17T15:32:40Z

After a bit of reading, it's not clear whether this is compliant with the standard (but it's not clear that it is not compliant either), mainly because the standard for models is quite imprecise. The most relevant quote I could find was:

[In]: (define-fun f ((x1 σ1) · · · (xn σn)) σ t)
The term t is expected, although not required, to be a value when f is a constant (i.e., when n = 0).

In such cases, i.e. the definition of a non-function value in a model, dolmen tries and evaluate the term into a value[1], which in this case fails because no value for x23 can be found at that point in time.

I'd argue that it's better for solvers to produce models in topological order, because 1) it makes it far easier to check, but also 2) I think it makes more sense: indeed, in the rest of the standard, typechecking of terms follows the regular scoping rules, and in particular terms cannot refer to constants declared later (that's why we have dedicated define-fun-rec commands, which are allowed in models) and 3) it is a good guard against accidental infinite recursive values (such as an infinite list) which I'm not sure we want to allow (and would probably make dolmen loop infinitely in the current state). If we ever decide to allow recursive/infinite values, then from the implementation perspective, it would be reasonable to allow out-of-order definitions though.

[1]: Note that this is the case for non-function values; in the case of functions, the body is only evaluated at each call site, so this gives a bit more freedom.

Gbury · 2024-06-17T15:36:52Z

For the part about defining the undefined values of a selector, here is the syntax currently accepted by dolmen :

As can be seen it is possible to use different definitions for different instances of a polymorphic selector if needed (even if the example only defines one for the Int case).

EDIT: the syntax is the same as the one presented in the link in @bobot 's answer above

Add cvc5 preliminary version

79efed8

bobot added the submission Submissions for SMT-COMP label May 28, 2024

hansjoergschurr and others added 2 commits May 28, 2024 10:49

Remove cvc5 from parallel track

8d3ba8a

Merge branch 'master' into comp24/cvc5

c3dc7bc

Fix command for incremental track

6f9e1ab

Remove cvc5 from the cloud track

6f3be7e

Use Zenodo release

269c1f8

martinjonas merged commit 12225b0 into SMT-COMP:master Jun 18, 2024
5 checks passed

Gbury mentioned this pull request Jul 26, 2024

Order of definitions in models SMT-LIB/SMT-LIB-2#26

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Solver submission: cvc5 #64

Solver submission: cvc5 #64

hansjoergschurr commented May 27, 2024

github-actions bot commented May 27, 2024 •

edited

Loading

cvc5

bobot commented May 31, 2024

hansjoergschurr commented May 31, 2024 •

edited

Loading

hansjoergschurr commented May 31, 2024

bobot commented Jun 4, 2024

hansjoergschurr commented Jun 5, 2024 •

edited

Loading

martinjonas commented Jun 10, 2024

martinjonas commented Jun 12, 2024

martinjonas commented Jun 13, 2024

hansjoergschurr commented Jun 13, 2024

bobot commented Jun 14, 2024

Gbury commented Jun 17, 2024 •

edited

Loading

Gbury commented Jun 17, 2024 •

edited

Loading

Solver submission: cvc5 #64

Solver submission: cvc5 #64

Conversation

hansjoergschurr commented May 27, 2024

github-actions bot commented May 27, 2024 • edited Loading

cvc5

bobot commented May 31, 2024

hansjoergschurr commented May 31, 2024 • edited Loading

hansjoergschurr commented May 31, 2024

bobot commented Jun 4, 2024

hansjoergschurr commented Jun 5, 2024 • edited Loading

martinjonas commented Jun 10, 2024

martinjonas commented Jun 12, 2024

martinjonas commented Jun 13, 2024

hansjoergschurr commented Jun 13, 2024

bobot commented Jun 14, 2024

Gbury commented Jun 17, 2024 • edited Loading

Gbury commented Jun 17, 2024 • edited Loading

github-actions bot commented May 27, 2024 •

edited

Loading

hansjoergschurr commented May 31, 2024 •

edited

Loading

hansjoergschurr commented Jun 5, 2024 •

edited

Loading

Gbury commented Jun 17, 2024 •

edited

Loading

Gbury commented Jun 17, 2024 •

edited

Loading