Support and analysis limits
Zincite targets MiniZinc 2.10.1 .mzn models and assignment-only .dzn data.
The syntax reference lists accepted constructs
and differences between the specification and compiler. JSON data and solver
solution streams are not supported formatter/linter/query input formats. The
candidate checker separately accepts official FlatZinc-JSON. Code and literals must be UTF-8;
non-UTF-8 bytes in comments are preserved.
Versions and Rust support
Section titled “Versions and Rust support”Zincite 0.5.0 supports the current stable Rust toolchain. No separate minimum Rust version is promised. The command-line tools and library crates share the same release version. Formatting and interfaces may change in the 0.x series; review the release notes when upgrading.
What each command checks
Section titled “What each command checks”Parsing checks the written syntax. It does not resolve includes, check types or require a solve item. This allows the formatter to work on a model fragment, but a formatted fragment may still fail MiniZinc’s type checks.
Linting and semantic queries can read includes and establish facts such as which declaration a name refers to or which indices an array accepts. They do not evaluate arbitrary MiniZinc functions or establish that a model has a solution. Use MiniZinc for compilation and solving.
Data edits change the instance. Zincite reparses the candidate and, for model-backed construction, checks supported types and array shapes. Those checks do not establish satisfiability.
The candidate checker accepts MiniZinc 2.10.1 text FlatZinc and official FlatZinc-JSON. It checks the mathematical operations emitted by both the standard decomposition profile and the pinned Gecode library, including exact aliases and conditional set/float/MPFR registrations. The checker integration guide gives both offline compilation recipes; the coverage audit maps signatures to execution tests and include closures. Compiler elimination, domain tightening and source abort bodies limit what a source model can expose to applications.
Values include Booleans, checked signed 64-bit integers, compact finite integer
sets and finite binary64 floats. Integers use exact decimal strings in prepared
artifacts, Wasm assignments and reports; compiler JSON integers are parsed exactly.
Float absolute/relative tolerances default to 1e-9 each, with zero/zero for exact
comparison. Prepared models save both settings, and native, CLI and Wasm callers
can configure them. Arithmetic overflow and undefined/nonfinite results diagnose.
The checker reports all available violations and identifies unresolved values and blocked checks independently. Supported deterministic definitions calculate auxiliary values from known inputs, without choosing missing decisions. A complete valid report establishes feasibility of the compiled candidate; it establishes no optimality or equivalence to arbitrary MiniZinc source. External executable/DLL hooks and restart-history hooks receive located exclusion diagnostics. Search and propagation annotations supply metadata, never candidate values. Some global relations wait for all required operands, even when a partial conflict could be inferred mathematically. An incomplete report with no violations is therefore not evidence that a satisfying completion exists.
Checking starts no compiler, solver or network request. Both CLI forms can export
prepared models as versioned JSON and load them without parsing FlatZinc. The
parser-free Rust API and Wasm bindings use the
same loader and checking runtime. The graphical example
demonstrates ordinary edits. The
2026-10-28 performance report records
measurements for its named build and workload. The checker ships in Zincite 0.5.0
and the standalone zincite-check package.
Unknown facts and incomplete analysis
Section titled “Unknown facts and incomplete analysis”An unknown fact is sometimes the expected result. For example, a parameter
int: divisor; may get its value from a data file. A source-only check cannot
assume that it is nonzero. An unknown fact must not be used to justify an
automatic fix or turned into a known fact by negating a query filter.
A limitation means information needed by the analysis was unavailable or an operation is outside its supported analysis. Missing standard-library context is one example. Zincite reports a location and reason so you can distinguish that case from a check that completed without a finding.
| Result | How to read it |
|---|---|
| Lint warning | A selected rule found a likely mistake to review. The rule ID and message explain the concern. |
| Lint info | A selected rule proposes an alternative formulation. It does not change the exit status. |
| Lint limitation | Part of the analysis could not be completed. Use --show-limitations for details. |
Query with complete: false |
Available results are included, but the limitations list explains what is missing. |
| Checker invalid/incomplete | A known violation and unresolved work can coexist; read the independent completeness fields. |
| Input or query error | Fix the reported syntax, configuration, dependency or query problem before using the result. |
Lint exits 1 for warnings and 2 for errors; informational findings alone exit 0. Limitations alone do not change that status, so exit 0 does not mean all semantic checks completed. Semantic queries exit 1 for incomplete results and 2 for errors. Keep the completeness fields with a query result if another program will use it. See the exit-code table for all commands.
A missing row in a semantic query is not necessarily a negative answer. Filters keep only proven matches. If the type of a declaration is unknown, its absence from a query for integer declarations does not establish that it has some other type.
Performance
Section titled “Performance”Format on save uses a fresh formatter process. The project targets less than 100 ms at the 95th percentile for ordinary editing cases; large generated inputs can take longer. Performance measurements live in the repository reports and identify the builds, machines and inputs tested. See format on save for editor setup.
Coverage reports and planned work
Section titled “Coverage reports and planned work”The repository keeps corpus checks, lint coverage and query acceptance results, with the revisions and limitations tested. The developer scripts explain how to reproduce those checks.
The project brief and design plans describe unfinished work as well as current contracts. Use the command guides and references for implemented behavior; a planned capability is not available merely because it appears in a design document.