A randomised test-generation and differential-testing framework for Savile Row, a constraint modelling compiler for the Essence Prime language.

The tool generates thousands of unique, seeded Essence Prime models, runs them through Savile Row with multiple solver backends, and flags crashes and solver disagreements.

1. Requirements
2. Getting Savile Row
3. Quick Start
4. Project Layout
5. The Fuzzer (fuzz.py)
6. The Generator (eprime-gen)
7. Known Limitations
8. Extending the Generator
9. Licence

Savile Row is not included in this repository. Download it from the official site and build it before running the fuzzer.

# Download from https://www-users.york.ac.uk/peter.nightingale/savilerow/
# (Linux build used during development: savilerow-1.11.1-linux.tar.gz)

tar xf savilerow-1.11.1-linux.tar.gz

# Build the JAR (requires Java 15+ and javac on PATH)
cd savilerow-1.11.1-linux
./compile.sh
cd ..

To add OR-Tools CP-SAT as a differential-testing backend:

./setup-ortools.sh

This downloads OR-Tools and extracts it next to the fuzzer. fuzz.py automatically searches or-tools_*/bin/fzn-cp-sat at startup and passes -or-tools-bin <path> to Savile Row — no modification to the SR distribution is needed.

Either add the savilerow wrapper script to your PATH, or pass its location explicitly to fuzz.py via --sr-path:

export PATH="$PWD/savilerow-1.11.1-linux:$PATH"

# or
python3 fuzz.py --sr-path ./savilerow-1.11.1-linux/savilerow --diff-test -n 100

# 1. Clone this repository
git clone <repo-url>
cd <repo>

# 2. Obtain and build Savile Row (see above)

# 3. Run 200 differential tests (Minion vs SAT, seeds 0–199)
python3 fuzz.py --diff-test -n 200

# 4. Run 1000 tests and save any failures to fuzz-out/
python3 fuzz.py --diff-test -n 1000 --keep-failures -o fuzz-out/

# 5. Just generate 10 model/param pairs into ./out/ (no solving)
python3 -m eprime_gen -n 10 -o out/

.
├── fuzz.py                     # Main fuzzer entry point
├── setup-ortools.sh            # Downloads and installs OR-Tools CP-SAT solver
├── eprime-gen/                 # Random EPrime model generator (Python package)
│   └── eprime_gen/
│       ├── __init__.py         # Public API: generate_model, GenConfig, print_model, print_param
│       ├── ast_nodes.py        # AST node dataclasses for all EPrime constructs
│       ├── generator.py        # Random model generator (Generator class, GenConfig)
│       ├── printer.py          # AST → EPrime source text
│       └── cli.py              # python -m eprime_gen command-line interface
├── fuzz-out/                   # Saved failure artefacts (created by --keep-failures)
└── CLAUDE.md                   # Developer notes (architecture, known bugs, feature backlog)

Crash detection (default): runs each model through one SR backend and flags any Java exception or internal error in the output.

Differential testing (--diff-test): runs each model through two or more SR backends (Minion, SAT, Chuffed, OR-Tools CP-SAT) and flags:

• any backend crashing with a Java exception
• SAT/UNSAT disagreement between backends
• objective-value disagreement between backends (when an objective is present)

Differential testing is the more powerful mode — it catches bugs where one backend silently produces a wrong answer rather than crashing.

python3 fuzz.py [options]

Options:
  -n, --count N          Number of tests (default: 200)
  --seed N               Starting seed; test i uses seed+i (default: 0)
  --sr-path PATH         Path to the savilerow script (auto-detected if on PATH)
  --timeout N            Seconds per SR invocation (default: 30)
  --workers N            Parallel workers; use 1 for sequential (default: 1)
  --depth N              Max expression depth (default: 5)
  --finds N              Max decision variables per model (default: 5)
  --givens N             Max given parameters per model (default: 3)
  --constraints N        Max top-level constraints per model (default: 6)
  --keep-failures        Save failing model/param/log files to --output
  -o, --output DIR       Directory for saved failures (default: fuzz-crashes/)
  -v, --verbose          Print a line for every test, not just findings

Differential testing:
  --diff-test            Enable differential mode
  --backends B1,B2,...   Backends to compare: minion, sat, chuffed, or-tools (default: minion,sat)

# 1000 sequential differential tests, seeds 0–999
python3 fuzz.py --diff-test -n 1000 --workers 1

# Start from a different seed range (to extend coverage)
python3 fuzz.py --diff-test -n 1000 --seed 1000

# Save all crash/disagreement artefacts
python3 fuzz.py --diff-test -n 1000 --keep-failures -o fuzz-out/

# Include Chuffed as a third backend
python3 fuzz.py --diff-test --backends minion,sat,chuffed -n 500

# Include OR-Tools CP-SAT (requires ./setup-ortools.sh first)
python3 fuzz.py --diff-test --backends minion,sat,or-tools -n 500

# Crash-detection only (no differential comparison)
python3 fuzz.py -n 500 --keep-failures

Each finding is printed immediately as it is discovered:

[  104/1000] CRASH  seed=103
          [minion] java.lang.ArrayIndexOutOfBoundsException: Index 14 out of bounds for length 4
          [minion] at savilerow.expression.Circuit.simplify(Circuit.java:76)

[  806/1000] DIFF-SAT  seed=805
          [minion] sat=False
          [sat] sat=True  obj=29
          saved → fuzz-out/diff_disagree_sat_seed805.eprime

A summary is printed at the end:

Done in 367.4s  (0.37s/test)
  pass=988  crash=11  disagree_sat=1  disagree_obj=0  timeout=0  skip=0

11 CRASH(ES) — seeds: [103, 306, 442, ...]
1 DISAGREEMENT(S) — seeds: [805]

With --keep-failures, disagreements are saved as three files per finding:

To reproduce a specific finding manually:

savilerow fuzz-out/diff_disagree_sat_seed805.eprime \
          fuzz-out/diff_disagree_sat_seed805.param -run-solver

The generator produces fully self-consistent Essence Prime model/parameter pairs by building a random AST and printing it to EPrime source text. Every model is deterministic given its seed.

from eprime_gen import generate_model, GenConfig, print_model, print_param

# Generate with default settings
model, param_values = generate_model(seed=42)
print(print_model(model))
print(print_param(model.givens, param_values))

# Customise generation
cfg = GenConfig(
    max_depth=5,
    max_find_vars=6,
    max_given_params=3,
    max_constraints=8,
    feat_circuit=0.0,    # disable circuit constraints
    feat_gcc=0.8,        # increase gcc frequency
)
model, param_values = generate_model(seed=0, cfg=cfg)

All fields are optional and have sensible defaults.

Size limits:

Feature weights (set to 0.0 to disable, higher = more frequent):

The generator can also be used standalone to write model/param files to disk:

# Generate 5 pairs into ./out/ with seed 42
python3 -m eprime_gen -n 5 --seed 42 -o out/

# Generate and immediately run through Savile Row
python3 -m eprime_gen -n 10 -o out/ --run-sr \
    --sr-path /path/to/savilerow

# Larger, deeper models
python3 -m eprime_gen -n 20 --depth 6 --finds 8 --constraints 10 -o out/

The generator follows a three-layer design:

GenConfig  ──►  Generator.generate()  ──►  Model AST
                     │
                     ▼
              _gen_bool / _gen_int / _gen_array
              (recursive, depth-bounded, scope-aware)
                     │
                     ▼
              printer.model() / printer.param()
                     │
                     ▼
              EPrime source text (.eprime / .param)

ast_nodes.py defines dataclasses for every EPrime construct: domains (IntRangeDomain, BoolDomain, MatrixDomain, CompositeIntDomain), expressions (BinOp, FuncCall, Quantifier, Comprehension, …), and top-level declarations (FindDecl, GivenDecl, Model, …).

generator.py builds random ASTs. The Scope object tracks which variables are in scope and their types. The three core methods (_gen_int, _gen_bool, _gen_array) build weighted choice lists from the GenConfig feature weights and the current scope, then recurse.

printer.py converts AST nodes to EPrime source text via a single expr() dispatch function and a model() top-level function.

cd eprime-gen
python -m pytest tests/ -v

Roughly 10% of generated models are rejected by Savile Row with a clean error message. These are intentional — the generator does not filter them out because they exercise error-handling paths. The most common cause:

• factorial on a decision variable (~9%): EPrime requires factorial arguments to be ground (parameter/constant only).

To add a new EPrime language feature:

1. Add an AST node in eprime_gen/ast_nodes.py if the existing nodes (FuncCall, BinOp, etc.) cannot represent it.

2. Add a printer case in eprime_gen/printer.py inside expr() (and _needs_parens() if the new node needs parenthesisation when nested).

3. Add a feat_X weight to GenConfig in eprime_gen/generator.py.

4. Add generation logic in _gen_bool, _gen_int, or _gen_array:

   • Add "my_feature" to the choices list and its weight to weights (guarded by the feature flag and any scope preconditions).
   • Add the corresponding if pick == "my_feature": ... handler.

5. Verify by running a quick generation check:

   from eprime_gen import generate_model, GenConfig
   from eprime_gen.printer import model as print_model
   cfg = GenConfig()
   found = sum(1 for s in range(500)
               if "my_func(" in print_model(generate_model(seed=s, cfg=cfg)[0]))
   print(f"Found in {found}/500 seeds")

6. Update CLAUDE.md to move the feature from "missing" to "implemented".

Features already implemented and available to copy as examples:

BSD 3-Clause — see LICENSE.