Sygus Comp 2016 Eval

---
name: sygus-comp-2016-eval
description: Evaluates syntax-guided program synthesis solvers on their ability to generate correct programs from logical constraints and grammars. It probes capabilities in conditional linear integer arithmetic, invariant generation, and programming-by-example with bit-vectors and strings. Use when the user wants to benchmark on SyGuS-Comp 2016, or asks about evaluating this task. Reports number_of_benchmarks_solved.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 1611.07627
  bibtex_key: alur2016syguscomp
  confidence: high
---

# sygus-comp-2016-eval

> SyGuS-Comp 2016: Results and Analysis — Alur et al. (2016) (arXiv:1611.07627, 2016)

## What this evaluates

Evaluates syntax-guided program synthesis solvers on their ability to generate correct programs from logical constraints and grammars. It probes capabilities in conditional linear integer arithmetic, invariant generation, and programming-by-example with bit-vectors and strings.

## Datasets

- **SyGuS-Comp 2016** — total 1307; splits: General (309), Conditional Linear Integer Arithmetic (73), Invariant Synthesis (67), Programming By Example (858)

## Metrics

- `number_of_benchmarks_solved` **(primary)** — range: percent
  - Count of benchmarks for which the solver produces a correct program within the time limit, divided by the total number of benchmarks in the track, expressed as a percentage.
- `time_to_solve` — range: other
  - Wall-clock time to solve a benchmark, classified into pseudo-logarithmic buckets: [0,1), [1,3), [3,10), [10,30), [30,100), [100,300), [300,1000), [1000,3600), >3600 seconds.
- `expression_size` — range: other
  - Number of nodes in the SyGuS parse-tree of the generated expression, classified into pseudo-logarithmic buckets: [1,10), [10,30), [30,100), [100,300), [300,1000), >1000.

## Input / output format

**Input**: Logical constraints (e.g., pre/post conditions, invariants, or input-output examples) and a function grammar defining the valid program structure.

**Output**: A synthesized program/expression that satisfies the constraints, represented as a SyGuS parse tree.

## Scoring recipe

```python
def compute_metrics(predictions, gold_specs, times, parse_trees, time_limit=3600):
    solved = 0
    for pred, spec, t, tree in zip(predictions, gold_specs, times, parse_trees):
        if pred is not None and verify(pred, spec) and t <= time_limit:
            solved += 1
    solve_rate = (solved / len(gold_specs)) * 100
    time_bucket = classify_pseudo_log(t, [0,1,3,10,30,100,300,1000,3600])
    size_bucket = classify_pseudo_log(len(tree.nodes), [1,10,30,100,300,1000])
    return solve_rate, time_bucket, size_bucket
```

## Common pitfalls

- Time comparisons use pseudo-logarithmic buckets rather than absolute seconds, which can mask performance differences within the same bucket.
- Expression size is measured by parse-tree node count, which may not reflect actual runtime efficiency or code quality.
- Solvers may terminate without producing a result or produce incorrect results; the evaluation counts these as unsolved, but the time bound may still be reported as the termination time.

## Evidence (verbatim from paper)

> The primary criterion for winning a track was the number of benchmarks solved, but we also analyzed the time to solve and the the size of the generated expressions. Both where classified using a pseudo-logarithmic scale as follows.

## Citation

```bibtex
@misc{alur2016syguscomp,
  title={SyGuS-Comp 2016: Results and Analysis},
  author={Alur et al. (2016)},
  year={2016},
  note={arXiv:1611.07627}
}
```

- arXiv: 1611.07627