Submission

Type: object
No Additional Properties

root name

Name

Type: string

root contributors

Contributors

Type: array

Must contain a minimum of 1 items

No Additional Items

Each item of this array must be:

root contributors Contributor
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"
}

root contributors Contributor name

Name

Type: string

root contributors Contributor website

Website

Default: null

root contributors Contributor website anyOf item 0
Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

root contributors Contributor website anyOf item 1
Type: null

root contacts

Contacts

Type: array

Must contain a minimum of 1 items

No Additional Items

Each item of this array must be:

root contacts NameEmail
Type: object

Name and valide email "name <email>"
Example:

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

root contacts NameEmail name

Name

Type: string

root contacts NameEmail email

Email

Type: string

root archive
Default: null

root archive anyOf Archive
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.

root archive anyOf Archive url

Url

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

root archive anyOf Archive h
Default: null

root archive anyOf Archive h anyOf Hash
Type: object
No Additional Properties

root archive anyOf Archive h anyOf item 1
Type: null
root archive anyOf item 1
Type: null

root command
Default: null

Fields command given in participations have priority over this one

root command anyOf Command
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"
}

root command anyOf Command binary

Binary

Type: string

root command anyOf Command arguments

Arguments

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

Each item of this array must be:

root command anyOf Command arguments arguments items
Type: string

root command anyOf Command compa_starexec

Compa Starexec

Type: boolean Default: false

Used only for internal tests
root command anyOf item 1
Type: null

root website

Website

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

root system_description

System Description

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

root solver_type
Type: enum (of string)

Must be one of:

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

root participations
Type: array
No Additional Items

Each item of this array must be:

root participations Participation
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

root participations Participation tracks

Tracks

Type: array
No Additional Items

Each item of this array must be:

root participations Participation tracks Track
Type: enum (of string)

Must be one of:

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

root participations Participation logics
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:

root participations Participation logics Logic
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"

root participations Participation divisions

Divisions

Type: array Default: []
No Additional Items

Each item of this array must be:

root participations Participation divisions Division
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"

root participations Participation archive
Default: null

root participations Participation archive anyOf Archive
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.

root participations Participation archive anyOf Archive url

Url

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

root participations Participation archive anyOf item 1
Type: null

root participations Participation command
Default: null

root participations Participation command anyOf Command
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"
}

root participations Participation command anyOf Command arguments

Arguments

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

Each item of this array must be:

root participations Participation command anyOf Command arguments arguments items
Type: string

root participations Participation command anyOf Command compa_starexec

Compa Starexec

Type: boolean Default: false

Used only for internal tests
root participations Participation command anyOf item 1
Type: null

root participations Participation experimental

Experimental

Type: boolean Default: false

root seed

Seed

Default: null

root seed anyOf item 0
Type: integer
root seed anyOf item 1
Type: null

root competitive

Competitive

Type: boolean Default: true