Submission

Type: object
No Additional Properties

Name

Type: string

Contributors

Type: array

Must contain a minimum of 1 items

No Additional Items

Each item of this array must be:

Type: object

Contributors in the developement of the solver. If only name is provided,
it can be directly given.

No Additional Properties
Examples:

"Jane Smith"
{
    "name": "Jane Smith",
    "website": "http://jane.smith.name"
}

Name

Type: string

Website

Default: null

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

Contacts

Type: array

Must contain a minimum of 1 items

No Additional Items

Each item of this array must be:

Type: object

Name and valide email "name <email>"


Example:

"Jane Smith <jane.smith@edu.world>"

Name

Type: string

Email

Type: string

Default: null

Type: object

The url must be record from http://zenodo.org for the final submission. So
the hash is not required because zenodo records are immutable.

The hash can be used if you want to be sure of the archive used during the
test runs.

Url

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

Default: null

Type: object
No Additional Properties

Type: null
Type: null

Default: null

Fields command given in participations have priority over this one

Type: object

Command with its arguments to run after the extraction of the archive.

The path are relative to the directory in which the archive is unpacked.

The input file is added at the end of the list of arguments.

Two forms are accepted, using a dictionnary (separate binary and arguments) or a list ([binary]+arguments).

The command run in the given environment
https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#computing-environment-on-competition-machines

No Additional Properties
Examples:

[
    "relative_cmd",
    "default_command_line"
]
{
    "arguments": [
        "default_command_line"
    ],
    "binary": "relative_cmd"
}

Binary

Type: string

Arguments

Type: array of string Default: []
No Additional Items

Each item of this array must be:

Compa Starexec

Type: boolean Default: false

Used only for internal tests

Type: null

Website

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

System Description

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

Type: enum (of string)

Must be one of:

  • "wrapped"
  • "derived"
  • "Standalone"
  • "Portfolio"

Type: array
No Additional Items

Each item of this array must be:

Type: object

tracks: select the participation tracks
divisions: add all the logics of those divisions in each track
logics: add all the specified logics in each selected track it exists

aws_repository should be used only in conjunction with Cloud and Parallel track

archive and command should not be used with Cloud and Parallel track. They superseed the one given at the root.

No Additional Properties

Tracks

Type: array
No Additional Items

Each item of this array must be:

Type: enum (of string)

Must be one of:

  • "UnsatCore"
  • "SingleQuery"
  • "ProofExhibition"
  • "ModelValidation"
  • "Incremental"
  • "Cloud"
  • "Parallel"
  • "UnsatCoreValidation"

Type: array Default: []

Can be a list of logics or a regexp matched on all the existing logics

No Additional Items

Each item of this array must be:

Type: enum (of string)

Must be one of:

  • "ABV"
  • "ABVFP"
  • "ABVFPLRA"
  • "ALIA"
  • "ANIA"
  • "AUFBV"
  • "AUFBVDTLIA"
  • "AUFBVDTNIA"
  • "AUFBVDTNIRA"
  • "AUFBVFP"
  • "AUFDTLIA"
  • "AUFDTLIRA"
  • "AUFDTNIRA"
  • "AUFFPDTNIRA"
  • "AUFLIA"
  • "AUFLIRA"
  • "AUFNIA"
  • "AUFNIRA"
  • "BV"
  • "BVFP"
  • "BVFPLRA"
  • "FP"
  • "FPLRA"
  • "LIA"
  • "LRA"
  • "NIA"
  • "NRA"
  • "QF_ABV"
  • "QF_ABVFP"
  • "QF_ABVFPLRA"
  • "QF_ALIA"
  • "QF_ANIA"
  • "QF_AUFBV"
  • "QF_AUFBVFP"
  • "QF_AUFBVLIA"
  • "QF_AUFBVNIA"
  • "QF_AUFLIA"
  • "QF_AUFNIA"
  • "QF_AX"
  • "QF_BV"
  • "QF_BVFP"
  • "QF_BVFPLRA"
  • "QF_BVLRA"
  • "QF_DT"
  • "QF_FP"
  • "QF_FPLRA"
  • "QF_IDL"
  • "QF_LIA"
  • "QF_LIRA"
  • "QF_LRA"
  • "QF_NIA"
  • "QF_NIRA"
  • "QF_NRA"
  • "QF_RDL"
  • "QF_S"
  • "QF_SLIA"
  • "QF_SNIA"
  • "QF_UF"
  • "QF_UFBV"
  • "QF_UFBVDT"
  • "QF_UFBVLIA"
  • "QF_UFDT"
  • "QF_UFDTLIA"
  • "QF_UFDTLIRA"
  • "QF_UFDTNIA"
  • "QF_UFFP"
  • "QF_UFFPDTNIRA"
  • "QF_UFIDL"
  • "QF_UFLIA"
  • "QF_UFLRA"
  • "QF_UFNIA"
  • "QF_UFNRA"
  • "UF"
  • "UFBV"
  • "UFBVDT"
  • "UFBVFP"
  • "UFBVLIA"
  • "UFDT"
  • "UFDTLIA"
  • "UFDTLIRA"
  • "UFDTNIA"
  • "UFDTNIRA"
  • "UFFPDTNIRA"
  • "UFIDL"
  • "UFLIA"
  • "UFLRA"
  • "UFNIA"
  • "UFNIRA"
  • "UFNRA"

Divisions

Type: array Default: []
No Additional Items

Each item of this array must be:

Type: enum (of string)

Must be one of:

  • "Arith"
  • "Bitvec"
  • "Equality"
  • "Equality+LinearArith"
  • "Equality+MachineArith"
  • "Equality+NonLinearArith"
  • "FPArith"
  • "QF_ADT+BitVec"
  • "QF_ADT+LinArith"
  • "QF_Bitvec"
  • "QF_Datatypes"
  • "QF_Equality"
  • "QF_Equality+Bitvec"
  • "QF_Equality+Bitvec+Arith"
  • "QF_Equality+LinearArith"
  • "QF_Equality+NonLinearArith"
  • "QF_FPArith"
  • "QF_LinearIntArith"
  • "QF_LinearRealArith"
  • "QF_NonLinearIntArith"
  • "QF_NonLinearRealArith"
  • "QF_Strings"

Default: null

Type: object

The url must be record from http://zenodo.org for the final submission. So
the hash is not required because zenodo records are immutable.

The hash can be used if you want to be sure of the archive used during the
test runs.

Url

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

Default: null

Type: object

Command with its arguments to run after the extraction of the archive.

The path are relative to the directory in which the archive is unpacked.

The input file is added at the end of the list of arguments.

Two forms are accepted, using a dictionnary (separate binary and arguments) or a list ([binary]+arguments).

The command run in the given environment
https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#computing-environment-on-competition-machines

No Additional Properties
Examples:

[
    "relative_cmd",
    "default_command_line"
]
{
    "arguments": [
        "default_command_line"
    ],
    "binary": "relative_cmd"
}

Arguments

Type: array of string Default: []
No Additional Items

Each item of this array must be:

Compa Starexec

Type: boolean Default: false

Used only for internal tests

Experimental

Type: boolean Default: false

Seed

Default: null

Type: integer
Type: null

Competitive

Type: boolean Default: true