Gecode::FlatZinc::Capture::parse and parse_string capture owning model records without constructing a FlatZincSpace, posting a registry constraint, applying restart state, creating search, or solving. This is the parser boundary for the separate compiler/checker described in FLATZINC-DESIGN.md. A Complete capture does not certify that an optimization backend supports the model.
Public boundary and semantics
Include gecode/flatzinc/capture.hh when linking the native FlatZinc parser library. Include capture-records.hh for the configuration-independent types used by a standalone compiler or checker. The latter requires only the C++ standard library. Public record types and namespaces are identical through both headers. Parser entry points have the native FlatZinc shared-library export policy.
The result owns a shared_ptr<const Records>. Expressions, variable specifications, domains, annotations, source names and output entries contain no AST, stream, parser, registry or Space pointers. They survive input/parser destruction. Separate capture calls have independent state. Failed calls publish diagnostics and no partial records. Locations report the parser's reduction/end line, not an exact source start span; generated declaration-domain rows are located at the completed declaration boundary.
raw_variables and raw_domains are copied at the end of the declaration list, before processing any explicit constraint. Their reference keys are (Type, index), with separate integer, Boolean, float and set namespaces. The combined vector position is not an entity key. A declaration alias refers to an earlier slot in its own namespace. Its extra declared restrictions remain explicit domain predicates; assigned literals remain literals. Arrays reuse variable slots for aliases and introduce fixed slots for literal elements. Parameters are expanded into their typed values, including named parameters in variable-array initializers.
raw_constraints retains every explicit predicate's identifier, ordered typed arguments and annotations. Unknown ordinary predicates are retained; the compiler must reject predicates outside its semantic whitelist. A predicate declaration supplies no executable definition and does not confer support on a registry plugin. Native restart-state predicates beginning gecode_on_restart_ return Unsupported because their stateful meaning is outside this capture contract.
variables, domains, constraints and coverage are derived audit records. Integer and Boolean reference equalities are normalized into aliases; restrictions on the merged slot become synthesized domains. Each explicit raw predicate has exactly one coverage entry, either retained or an alias equality. Alias resolution uses path compression and final canonical targets, preventing repeated old references from repeatedly walking a descending equality chain. Float/set equalities remain explicit. The authoritative compiler input is the raw set of variables, declaration domains and predicates; consumers need not trust or reproduce the normalization.
SolveGoal preserves satisfaction, minimization or maximization and the original typed variable/literal objective. Constant and parameter objectives never become the legacy zero-valued dummy objective. Output uses original source-slot references, before printer shrinking. Scalar output is a typed reference. Array output keeps the legacy arrayNd text fragments and the positional array of references; typed output_array dimension sets remain in declaration annotations. Output dimensions are checked against array length, including empty arrays, with checked products. Calls preserve positional argument structure: f([a,b]) is distinct from f(a,b).
Dialect and limits
The implementation accepts the existing textual grammar with capture-specific guards. It is not a new general MiniZinc or FlatZinc-JSON parser. Parameter declaration annotations are explicitly rejected; the upstream grammar forbids them, so they cannot be silently omitted from the capture. Native integer limits still bound integer literals and storage indices; decimal, hexadecimal and explicit octal tokens are consumed completely. Decimal 010 means ten and 0o10 means eight. Floats are parsed using the classic locale; nonfinite values and nonzero literals that underflow to zero fail. Finite binary64 rounding remains the float record representation. Explicit integer sets are sorted and deduplicated without changing their membership semantics.
Input must be valid UTF-8 and contain no embedded NUL. Annotation strings decode named C escapes, including newline, tab, backslash and escaped quotes; numeric and unknown escapes explicitly return Unsupported. Strings are retained as values, not executed. The source preflight counts bracket/parenthesis nesting while respecting comments and escaped strings.
Defaults cap input at 16 MiB, variables at one million, each declared/captured array at one million elements, raw predicates plus declaration-domain predicates at one million, and nesting at 64. Input size/nesting are checked before invoking the C parser. Declared bulk dimensions and internal integer index limits are checked before corresponding bulk storage. Explicit initializer lists are bounded by input size while parsing, then their exact variable/record counts are checked; these are not a byte-exact allocator quota or a parsing wall-clock deadline. Declaration-domain limits also apply during generation. Nonpositive or out-of-range array references, invalid alias namespaces, selected unsafe built-in signatures, incorrect initializer types/counts and malformed output annotations fail before publication. Arbitrary predicate type checking belongs to the independent compiler.
Normal syntax, semantic and explicit-resource failures clean parser-owned variable specifications, constraints, output ASTs and scanner state. The generated parser has capture-only semantic destructors for discarded grammar values and capture actions release temporary initializers after ownership transfer. Allocation failure may propagate std::bad_alloc; deterministic allocator-failure injection and a strong cleanup guarantee for exceptions interrupting arbitrary C-parser reductions are not implemented.
The existing FlatZinc::parse entry points have a null capture bridge. Their native posting, equality normalization, objective convention, scanner behavior and printer ownership path are retained. Capture does not intercept posted actors or require a FlatZincSpace layout change.
Verification and regeneration
test/flatzinc-capture/capture.cpp is a standalone assertion-based test outside the legacy test/flatzinc/ registration glob. It checks all four variable namespaces; literal/alias/domain preservation; holey/empty domains and arrays; min/max literal and variable goals; output ordering and alias positions; annotation call/string structure; reification retention; unknown predicates; registry noninvocation; arity/type/reference/UTF-8/limit failures; exception-enabled streams; every truncated prefix of a complete model; repeated failed captures; and concurrent captures. A separate case exercises the unchanged native parser and confirms actual integer propagation. Passing these tests establishes parser-record correctness, not backend parity or solve performance.
Local validation on macOS arm64 / AppleClang 17 passed 236 capture checks, 32 captures across four concurrent threads, and the native-parser compatibility assertion. The normal executable used C++17, -O1 -g -Wall -Wextra -pedantic. A separate Debug static build compiled every linked Gecode source (support, kernel, search, integer, set, float, minimodel, driver, FlatZinc/parser/scanner) with -fsanitize=address,undefined -fno-omit-frame-pointer; the capture/test sources used the same instrumentation and the complete panel passed with sanitizer errors fatal. Build and test artifacts are local to build/flatzinc-capture*. LeakSanitizer was disabled on this platform; the macOS leaks utility could not obtain the child task port, so no leak-detector pass is claimed. Linux leak detection and allocator fault injection remain additional verification gates. These runs made no timing or throughput claim.
The checked-in parser is generated with GNU Bison 3.8.2. The scanner uses Flex 2.6.4 (Apple flex-35). Regenerate from the repository root:
Only trailing whitespace and extra terminal blank lines are normalized after generation; no generated parser/scanner logic is edited. The local Bison bootstrap used the official bison-3.8.2.tar.gz archive with SHA-256 06c9e13bdf7eb24d4ceb6b59205a4f67c2c7e7213119644430fe82fbd14a0abb, verified against the GNU release announcement. No system toolchain was replaced.
The upstream FlatZinc specification defines parameter substitution, declaration aliases, predicate calls, literal objectives, annotations and output conventions. This implementation's unsupported syntax and resource limits above are additional explicit restrictions. Compiler support and end-to-end solve checks are separate gates.
Generated by
1.18.0