Format, lint, query and check.

Format, lint and query MiniZinc source, then check supplied FlatZinc assignments in Rust or WebAssembly.

Zincite 0.5.0 · MiniZinc 2.10.1

Zincite helps you review and maintain MiniZinc models. The formatter takes care of layout, so an edit to a constraint produces a diff you can read. The linter checks conventions and looks for modelling concerns, such as mismatched array indices or expressions that may be undefined. Queries let you inspect the source and data when you have a more specific question.

The candidate checker evaluates supplied values against a compiled FlatZinc model. An application can prepare the model once, derive supported auxiliary values after each edit, and show structured violations or missing input.

The commands work without running a MiniZinc compiler or solver. They share a parser that keeps comments, spelling and source locations, so findings can point back to the model you are editing.

A staffing example

Suppose we are staffing three days. Each day has a required number of people and a number available. A fragment of the staffing model starts like this:

Formatting constraints

Before formatting

% Staff cannot be moved from one day to another.
constraint forall(d in Days)(staff[d]>=required[d]);
constraint forall(d in Days)(staff[d]<=available[d]);

After formatting

% Staff cannot be moved from one day to another.
constraint forall (d in Days) (
    staff[d] >= required[d]
);
constraint forall (d in Days) (
    staff[d] <= available[d]
);

zincite fmt staffing.mzn prints the formatted model. The quantifiers and bodies have room to be read separately; the names and comment stay intact. Add --write to apply the layout, or --check to check it in CI.

Linting constraint labels

Run the naming and constraint-label checks:

zincite lint --isolated --rules naming,missing-constraint-label staffing.mzn

This reports a missing-constraint-label warning at each constraint. A label such as constraint :: "Cover each day's demand" tells a reader what the first constraint means. Zincite leaves that wording to the modeller. The walkthrough shows the labelled version and explains the selected checks.

Querying staff shortages

Now consider the data:

required = [2, 3, 4];
available = [3, 4, 3];

There are ten staff-days available for nine staff-days of demand. But a spare person on day 1 cannot fill a gap on day 3. A short query makes that visible:

let required = items | filter(name("required")) | values | one;
let available = items | filter(name("available")) | values | one;
[
    (day: d, missing: required[d] - available[d])
    | d in index_set(required)
    where required[d] > available[d]
]

Save the data as staffing.dzn and the query as shortages.zq, then run:

zincite query --program-file shortages.zq staffing.dzn

The JSON report contains one row: day 3 is missing 1 person. This checks the literal arrays, which have the same indices in this example. It does not solve the model. The query gives us a concrete data problem to investigate before asking a solver for a roster.

Work through the complete example for the model, formatter output, lint feedback and query result.

Check candidate assignments

Given a compiled model and a candidate file, run:

zincite check delivery.fzn candidate.dzn

The integration guide supplies those files and follows valid, invalid and incomplete edits through the CLI, Rust API and WebAssembly runtime. The checker reports every available violation and completeness separately. MiniZinc compilation is a separate offline step; repeated checks start no solver.

Install Zincite

Install Zincite 0.5.0 with a current stable Rust toolchain:

cargo install --locked --version '=0.5.0' zincite

Formatting and interfaces may change in the 0.x series. Read the release notes when upgrading. The support guide explains language coverage and how to interpret incomplete analysis.

Guides

FormattingSee the layout choices, configure EditorConfig and set up format on save.

LintingChoose checks for conventions, arrays, domains or search, and review suggested fixes.

Queries and dataSelect source, follow declaration uses, build reports and make smaller data instances.

Candidate checkingComplete supported auxiliary values and report violations or missing input in Rust and WebAssembly.

The query guide explains expressions, comprehensions and collection order alongside MiniZinc source inspection. Zincite uses Zirql as its shared evaluator; the Zirql language guide provides further examples and background.