Sygus Comp 2018 Eval

---
name: sygus-comp-2018-eval
description: Evaluates syntax-guided synthesis solvers on their ability to generate correct programs or specifications across multiple domains, including general synthesis, conditional linear integer arithmetic, invariant generation, and programming by examples. Use when the user wants to benchmark on SyGuS-Comp 2018, or asks about evaluating this task. Reports correctness.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 1904.07146
  bibtex_key: [REDACTED]
  confidence: high
---

# sygus-comp-2018-eval

> SyGuS-Comp 2018: Results and Analysis — Alur et al. (2019) (arXiv:1904.07146, 2019)

## What this evaluates

Evaluates syntax-guided synthesis solvers on their ability to generate correct programs or specifications across multiple domains, including general synthesis, conditional linear integer arithmetic, invariant generation, and programming by examples.

## Datasets

- **SyGuS-Comp 2018** — total 1600; splits: test (-1)

## Metrics

- `correctness` **(primary)** — range: [0, 1]
  - Fraction of benchmarks for which the solver produces a solution that passes both syntactic grammar validation and semantic SMT verification within resource limits.

## Input / output format

**Input**: A benchmark instance specifying a target function, a grammar (or input/output examples/constraints), and semantic requirements.

**Output**: A synthesized expression or program that must conform to the specified grammar and satisfy all semantic constraints.

## Scoring recipe

```python
solved = 0
for bench in benchmarks:
    sol = solver.run(bench, time_limit=3600, mem_limit=128e9)
    if sol is None:
        continue
    if check_syntax(sol, bench.grammar) and check_semantics(sol, bench.constraints):
        solved += 1
return solved / len(benchmarks)
```

## Common pitfalls

- Solvers must pass both syntactic grammar checks and semantic SMT verification; failing either counts as incorrect.
- Resource limits are strict: 3600s wall-clock time and 128GB memory per run; exceeding either results in a timeout/oom failure.
- Benchmarks are divided into specialized tracks (CLIA, Inv, PBE, General); solvers often specialize, so cross-track comparison requires normalization.

## Evidence (verbatim from paper)

> The memory usage limit for each solver run was set to 128 GB, and the wall-clock time limit is set to 3600 seconds (thus, a solver that used all 4 cores could consume at most 14400 seconds of CPU time). The solutions that the solvers produced were checked for both syntactic and semantic correctness. That is, a first postprocessor checked that the produced expression adhered to the grammar specified in the given benchmark, and if this check passes, a second postprocessor checked that the solution adhered to semantic constraints given in the benchmark (by invoking an SMT solver).

## Citation

```bibtex
@misc{alur2019syguscomp2018,
  title={SyGuS-Comp 2018: Results and Analysis},
  author={Alur et al. (2019)},
  year={2019},
  note={arXiv:1904.07146}
}
```

- arXiv: 1904.07146